clean up hints for NaturalDeduction, split ProgrammingLanguage into multiple files

[coq-hetmet.git] / src / ProgrammingLanguageReification.v

diff --git a/src/ProgrammingLanguageReification.v b/src/ProgrammingLanguageReification.v
index 589f748..c1a06d8 100644 (file)
--- a/src/ProgrammingLanguageReification.v
+++ b/src/ProgrammingLanguageReification.v
@@ -28,12 +28,37 @@ Require Import Reification.
 Require Import NaturalDeduction.
 Require Import NaturalDeductionCategory.
 Require Import ProgrammingLanguage.
+Require Import ProgrammingLanguageCategory.
+Require Import Enrichments.
 
-Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
-| NLevelLanguage_zero : forall lang,    NLevelLanguage O lang
-| NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
-                          TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
+Section ProgrammingLanguageReification.
 
-Definition OmegaLevelLanguage : Type :=
-  { f : nat -> ProgrammingLanguageSMME
-  & forall n, TwoLevelLanguage (f n) (f (S n)) }.
+  Definition TwoLevelLanguage `(Guest:ProgrammingLanguage) `(Host:ProgrammingLanguage)
+    := Reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host) [].
+
+  Inductive NLevelLanguage : forall (n:nat) `(PL:ProgrammingLanguage), Type :=
+  | NLevelLanguage_zero : forall `(lang:ProgrammingLanguage),  
+                            NLevelLanguage O lang
+  | NLevelLanguage_succ : forall `(L1:ProgrammingLanguage) `(L2:ProgrammingLanguage) n,
+                            TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
+
+  (*
+  Definition OmegaLevelLanguage : Type :=
+    { f : nat -> ProgrammingLanguage
+    & forall n, TwoLevelLanguage (f n) (f (S n)) }.
+    *)
+
+End ProgrammingLanguageReification.
+
+(*
+  Structure ProgrammingLanguage :=
+  { plsmme_t       : Type
+  ; plsmme_judg    : Type
+  ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
+  ; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
+  ; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
+  ; plsmme_smme    : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
+  }.
+  Coercion plsmme_pl   : ProgrammingLanguage >-> ProgrammingLanguage.
+  Coercion plsmme_smme : ProgrammingLanguage >-> SurjectiveMonicMonoidalEnrichment.
+*)