src/ProgrammingLanguageReification.v

   1 (*********************************************************************************************************************************)
   2 (* ProgrammingLanguageReification                                                                                                *)
   3 (*                                                                                                                               *)
   4 (*   Reifications in ProgrammingLanguages.                                                                                       *)
   5 (*                                                                                                                               *)
   6 (*********************************************************************************************************************************)
   7
   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 MonoidalCategories_ch7_8.
  22 Require Import Coherence_ch7_8.
  23 Require Import Enrichment_ch2_8.
  24 Require Import RepresentableStructure_ch7_2.
  25 Require Import FunctorCategories_ch7_7.
  26
  27 Require Import Reification.
  28 Require Import NaturalDeduction.
  29 Require Import NaturalDeductionCategory.
  30 Require Import ProgrammingLanguage.
  31 Require Import Enrichments.
  32
  33 Section ProgrammingLanguageReification.
  34
  35   Definition TwoLevelLanguage `(Guest:ProgrammingLanguage) `(Host:ProgrammingLanguage)
  36     := Reification (TypesEnrichedInJudgments Guest) (TypesEnrichedInJudgments Host) [].
  37
  38   Inductive NLevelLanguage : forall (n:nat) `(PL:ProgrammingLanguage), Type :=
  39   | NLevelLanguage_zero : forall `(lang:ProgrammingLanguage),
  40                             NLevelLanguage O lang
  41   | NLevelLanguage_succ : forall `(L1:ProgrammingLanguage) `(L2:ProgrammingLanguage) n,
  42                             TwoLevelLanguage L1 L2 -> NLevelLanguage n L1 -> NLevelLanguage (S n) L2.
  43
  44   (*
  45   Definition OmegaLevelLanguage : Type :=
  46     { f : nat -> ProgrammingLanguage
  47     & forall n, TwoLevelLanguage (f n) (f (S n)) }.
  48     *)
  49
  50 End ProgrammingLanguageReification.
  51
  52 (*
  53   Structure ProgrammingLanguage :=
  54   { plsmme_t       : Type
  55   ; plsmme_judg    : Type
  56   ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
  57   ; plsmme_rule    : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
  58   ; plsmme_pl      : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
  59   ; plsmme_smme    : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
  60   }.
  61   Coercion plsmme_pl   : ProgrammingLanguage >-> ProgrammingLanguage.
  62   Coercion plsmme_smme : ProgrammingLanguage >-> SurjectiveMonicMonoidalEnrichment.
  63 *)