1 (*********************************************************************************************************************************)
2 (* ProgrammingLanguage *)
4 (* Basic assumptions about programming languages. *)
6 (*********************************************************************************************************************************)
8 Generalizable All Variables.
9 Require Import Preamble.
10 Require Import General.
11 Require Import Categories_ch1_3.
12 Require Import InitialTerminal_ch2_2.
13 Require Import Functors_ch1_4.
14 Require Import Isomorphisms_ch1_5.
15 Require Import ProductCategories_ch1_6_1.
16 Require Import OppositeCategories_ch1_6_2.
17 Require Import Enrichment_ch2_8.
18 Require Import Subcategories_ch7_1.
19 Require Import NaturalTransformations_ch7_4.
20 Require Import NaturalIsomorphisms_ch7_5.
21 Require Import BinoidalCategories.
22 Require Import PreMonoidalCategories.
23 Require Import MonoidalCategories_ch7_8.
24 Require Import Coherence_ch7_8.
25 Require Import Enrichment_ch2_8.
26 Require Import RepresentableStructure_ch7_2.
27 Require Import FunctorCategories_ch7_7.
29 Require Import NaturalDeduction.
31 Section Programming_Language.
33 Context {T : Type}. (* types of the language *)
35 Definition PLJudg := (Tree ??T) * (Tree ??T).
36 Definition sequent := @pair (Tree ??T) (Tree ??T).
37 Notation "cs |= ss" := (sequent cs ss) : pl_scope.
39 Context {Rule : Tree ??PLJudg -> Tree ??PLJudg -> Type}.
41 Notation "H /⋯⋯/ C" := (ND Rule H C) : pl_scope.
47 Class ProgrammingLanguage :=
48 { pl_eqv0 :> @ND_Relation PLJudg Rule
49 ; pl_snd :> @SequentND PLJudg Rule _ sequent
50 ; pl_cnd :> @ContextND PLJudg Rule T sequent pl_snd
51 ; pl_eqv1 :> @SequentND_Relation PLJudg Rule _ sequent pl_snd pl_eqv0
52 ; pl_eqv :> @ContextND_Relation PLJudg Rule _ sequent pl_snd pl_cnd pl_eqv0 pl_eqv1
54 Notation "pf1 === pf2" := (@ndr_eqv _ _ pl_eqv _ _ pf1 pf2) : temporary_scope3.
55 Coercion pl_eqv : ProgrammingLanguage >-> ContextND_Relation.
56 Coercion pl_cnd : ProgrammingLanguage >-> ContextND.
58 End Programming_Language.