Multilanguage boundaries

.gitignore

@@ -16,4 +16,5 @@ Makefile.d
 _CoqProject
 .Makefile.coq.d
 .coq-native
-**/.DS_Store
+**/.DS_Store*.timing
+*.timing

src/Pyrosome/Lang/Multilanguages/Boundaries.v

@@ -0,0 +1,139 @@
+(* The boundary fragment of the source multilanguage: conversions between
+   the typed and the untyped language, and their defining equations. *)
+
+Set Implicit Arguments.
+
+From coqutil Require Import Datatypes.String.
+From Stdlib Require Import Lists.List.
+Import ListNotations.
+Open Scope string.
+Open Scope list.
+From Utils Require Import Utils.
+
+(* Compiler infrastructure. *)
+From Pyrosome Require Import Compilers.Compilers Elab.ElabCompilers.
+Import CompilerDefs.Notations. (* for `match # from <lang> with` compiler syntax *)
+
+From Pyrosome Require Import Theory.Core Elab.Elab
+  Tools.Matches
+  Tools.EGraph.TypeInference Tools.Resolution Tools.EGraph.ComputeWf.
+Import Core.Notations.
+
+From Stdlib Require derive.Derive.
+
+(* The language fragments that make up the two interoperating languages. *)
+From Pyrosome.Lang Require Import SimpleVSTLC.
+From Pyrosome.Lang Require Import UTLC.
+From Pyrosome.Lang Require Import BoolType.
+From Pyrosome.Lang Require Import SimpleVProd.
+
+
+(* Machinery for building the polymorphic (parameterized) versions of those fragments. *)
+From Pyrosome.Lang Require Import PolySubst SimpleVSubst.
+From Pyrosome.Lang Require Import PolyCompilerLangs PolyCompilersCPS PolyCompilers.
+From Pyrosome.Compilers Require Import Parameterizer.
+Import Pyrosome.Tools.UnElab.
+From Pyrosome.Lang.Multilanguages Require Export InteropLangs.
+
+(* The boundaries fragment: the two conversion forms [#"ttd"] (typed to
+   dynamic) and [#"dtt"] (dynamic to typed), with the equations describing
+   how they behave on each type former.  This is the natural embedding;
+   TODO: check whether the lump embedding can be simulated on top of it. *)
+Definition boundaries_def : lang :=
+  {[l/subst [exp_subst++value_subst]
+    [:| "G" : #"env",
+        "A" : #"ty",
+        "e" : #"exp" "G" "A"
+        -----------------------------------------------
+        #"ttd" "A" "e" : #"exp" "G" #"*"
+    ];
+    [:| "G" : #"env",
+        "A" : #"ty",
+        "e" : #"exp" "G" #"*"
+        -----------------------------------------------
+        #"dtt" "A" "e" : #"exp" "G" "A"
+    ];
+    [:= "G" : #"env",
+        "e" : #"exp" "G" #"*"
+        ----------------------------------------------- ("dtt star")
+        #"dtt" #"*" "e" =
+        "e" : #"exp" "G" #"*"
+    ];
+    [:= "G" : #"env",
+        "e" : #"exp" "G" #"*"
+        ----------------------------------------------- ("ttd star")
+        #"ttd" #"*" "e" =
+        "e" : #"exp" "G" #"*"
+    ];
+    [:= "G" : #"env"
+        ----------------------------------------------- ("dtt True")
+        #"dtt" #"bool" (#"ret" #"uT") =
+        #"ret" #"T" : #"exp" "G" #"bool"
+    ];
+    [:= "G" : #"env"
+        ----------------------------------------------- ("dtt False")
+        #"dtt" #"bool" (#"ret" #"uF") =
+        #"ret" #"F" : #"exp" "G" #"bool"
+    ];
+    [:= "G" : #"env"
+        ----------------------------------------------- ("ttd True")
+        #"ttd" #"bool" (#"ret" #"T") =
+        #"ret" #"uT" : #"exp" "G" #"*"
+    ];
+    [:= "G" : #"env"
+        ----------------------------------------------- ("ttd False")
+        #"ttd" #"bool" (#"ret" #"F") =
+        #"ret" #"uF" : #"exp" "G" #"*"
+    ];
+    [:= "G" : #"env",
+        "A" : #"ty",
+        "B" : #"ty",
+        "e" : #"exp" (#"ext" "G" #"*") #"*"
+        ----------------------------------------------- ("dtt func")
+        #"dtt" (#"->" "A" "B") (#"ret" (#"ulambda" "e")) =
+        #"ret" (#"lambda" "A" (#"dtt" "B" (#"uapp" (#"ret" (#"val_subst" #"wkn" (#"ulambda" "e"))) (#"ttd" "A" (#"ret" #"hd"))))) :
+        #"exp" "G" (#"->" "A" "B")
+    ];
+    [:= "G" : #"env",
+        "A" : #"ty",
+        "B" : #"ty",
+        "v" : #"val" "G" (#"->" "A" "B")
+        ----------------------------------------------- ("ttd func")
+        #"ttd" (#"->" "A" "B") (#"ret" "v") =
+        #"ret" (#"ulambda" (#"ttd" "B" (#"app" (#"ret" (#"val_subst" #"wkn" "v")) (#"dtt" "A" (#"ret" #"hd"))))) :
+        #"exp" "G" #"*"
+    ];
+    [:= "G" : #"env",
+        "e" : #"exp" (#"ext" "G" #"*") #"*"
+        ----------------------------------------------- ("dtt ulambda mismatch")
+        #"dtt" #"bool" (#"ret" (#"ulambda" "e")) =
+        #"Error" #"bool" : #"exp" "G" #"bool"
+    ];
+    [:= "G" : #"env",
+        "A" : #"ty",
+        "B" : #"ty"
+        ----------------------------------------------- ("dtt uT mismatch")
+        #"dtt" (#"->" "A" "B") (#"ret" #"uT") =
+        #"Error" (#"->" "A" "B") : #"exp" "G" (#"->" "A" "B")
+    ];
+    [:= "G" : #"env",
+        "A" : #"ty",
+        "B" : #"ty"
+        ----------------------------------------------- ("dtt uF mismatch")
+        #"dtt" (#"->" "A" "B") (#"ret" #"uF") =
+        #"Error" (#"->" "A" "B") : #"exp" "G" (#"->" "A" "B")
+    ]
+  ]}.
+Derive boundaries
+        in (elab_lang_ext (utlc ++
+                                stlc ++
+                                typed_bool ++
+                                untyped_bool ++
+                                error_t ++ star_type ++
+                                exp_subst++value_subst)
+                boundaries_def boundaries)
+        as boundaries_wf.
+Proof. auto_elab. Qed.
+#[local] Definition boundaries_entry :=
+  lang_entry (elab_lang_implies_wf boundaries_wf).
+#[export] Hint Resolve boundaries_entry : wf_lang_db.

src/Pyrosome/Lang/Multilanguages/InteropLangs.v

@@ -0,0 +1,136 @@
+(* The two multilanguage sources: [simple_interoperating_langs], the
+   simply-typed combination of STLC and UTLC with booleans, and
+   [polymorphic_interoperating_langs], its parameterized counterpart built
+   from the fragments in ParamFragments.v, plus the compiler embedding the
+   former into the latter at the empty type environment. *)
+
+Set Implicit Arguments.
+
+From coqutil Require Import Datatypes.String.
+From Stdlib Require Import Lists.List.
+Import ListNotations.
+Open Scope string.
+Open Scope list.
+From Utils Require Import Utils.
+
+(* Compiler infrastructure. *)
+From Pyrosome Require Import Compilers.Compilers Elab.ElabCompilers.
+Import CompilerDefs.Notations. (* for `match # from <lang> with` compiler syntax *)
+
+From Pyrosome Require Import Theory.Core Elab.Elab
+  Tools.Matches
+  Tools.EGraph.TypeInference Tools.Resolution Tools.EGraph.ComputeWf.
+Import Core.Notations.
+
+From Stdlib Require derive.Derive.
+
+(* The language fragments that make up the two interoperating languages. *)
+From Pyrosome.Lang Require Import SimpleVSTLC.
+From Pyrosome.Lang Require Import UTLC.
+From Pyrosome.Lang Require Import BoolType.
+From Pyrosome.Lang Require Import SimpleVProd.
+
+
+(* Machinery for building the polymorphic (parameterized) versions of those fragments. *)
+From Pyrosome.Lang Require Import PolySubst SimpleVSubst.
+From Pyrosome.Lang Require Import PolyCompilerLangs PolyCompilersCPS PolyCompilers.
+From Pyrosome.Compilers Require Import Parameterizer.
+Import Pyrosome.Tools.UnElab.
+From Pyrosome.Lang.Multilanguages Require Export ParamFragments.
+
+
+Definition simple_interoperating_langs :=
+  boolhuh ++
+    mif ++
+    utlc_bool ++
+    utlc ++
+    untyped_bool ++
+    star_type ++ error_t ++
+    typed_bool ++
+    stlc ++
+    exp_subst ++
+    value_subst.
+
+Definition polymorphic_interoperating_langs :=
+  boolhuh_ty_subst ++ boolhuh_parameterized ++
+    mif_ty_subst ++ mif_parameterized ++
+    utlc_bool_parameterized ++
+    utlc_ty_subst ++ utlc_parameterized ++
+    untyped_bool_ty_subst ++ untyped_bool_parameterized ++
+    star_type_ty_subst ++ error_t_ty_subst ++
+    star_type_parameterized ++ error_t_parameterized ++
+    typed_bool_ty_subst ++ typed_bool_parameterized ++
+    stlc_ty_subst ++ stlc_parameterized ++
+    (* The polymorphic base.  [poly] is not strictly needed here, since this
+       language has no type lambdas or type application, but it is included
+       so that the list extends directly to a polymorphic-to-polymorphic
+       compiler. *)
+    poly ++
+    exp_param_substs ++
+    exp_ty_subst ++
+    val_param_substs ++
+    val_ty_subst ++
+    env_ty_subst ++
+    ty_subst_lang ++
+    exp_parameterized ++ val_parameterized ++ ty_env_lang.
+
+
+Lemma simple_interoperating_langs_wf : wf_lang simple_interoperating_langs.
+Proof. prove_by_lang_db. Qed.
+#[local] Definition simple_interoperating_langs_entry := lang_entry simple_interoperating_langs_wf.
+#[export] Hint Resolve simple_interoperating_langs_entry : wf_lang_db.
+
+Lemma polymorphic_interoperating_langs_wf : wf_lang polymorphic_interoperating_langs.
+Proof. prove_by_lang_db. Qed.
+#[local] Definition polymorphic_interoperating_langs_entry := lang_entry polymorphic_interoperating_langs_wf.
+#[export] Hint Resolve polymorphic_interoperating_langs_entry : wf_lang_db.
+
+Local Notation compiler := (compiler string).
+
+Definition interoperating_langs_compiler_def : compiler :=
+  match # from simple_interoperating_langs with
+  | {{s#"ty"}} => {{s #"ty" #"ty_emp"}}
+  | {{s#"env"}} => {{s #"env" #"ty_emp"}}
+  | {{s#"sub" "G" "G'"}} => {{s #"sub" #"ty_emp" "G" "G'"}}
+  | {{e#"id" "G"}} => {{e @"id" @("D" := #"ty_emp")}}
+  | {{e#"cmp" "G1" "G2" "G3" "f" "g"}} => {{e @"cmp" @("D" := #"ty_emp") "f" "g"}}
+  | {{s#"val" "G" "A"}} => {{s #"val" #"ty_emp" "G" "A"}}
+  | {{e#"val_subst" "G" "G'" "g" "A" "v"}} => {{e @"val_subst" @("D" := #"ty_emp") "g" "v"}}
+  | {{e#"emp"}} => {{e @"emp" @("D" := #"ty_emp")}}
+  | {{e#"forget" "G"}} => {{e @"forget" @("D" := #"ty_emp")}}
+  | {{e#"ext" "G" "A"}} => {{e @"ext" @("D" := #"ty_emp") "G" "A"}}
+  | {{e#"snoc" "G" "G'" "g" "A" "v"}} => {{e @"snoc" @("D" := #"ty_emp") "g" "v"}}
+  | {{e#"wkn" "G" "A"}} => {{e @"wkn" @("D" := #"ty_emp")}}
+  | {{e#"hd" "G" "A"}} => {{e @"hd" @("D" := #"ty_emp")}}
+  | {{s#"exp" "G" "A"}} => {{s #"exp" #"ty_emp" "G" "A"}}
+  | {{e#"exp_subst" "G" "G'" "g" "A" "e"}} => {{e @"exp_subst" @("D" := #"ty_emp") "g" "e"}}
+  | {{e#"ret" "G" "A" "v"}} => {{e @"ret" @("D" := #"ty_emp") "v"}}
+  | {{e#"->" "t" "t'"}} => {{e @"->" @("D" := #"ty_emp") "t" "t'"}}
+  | {{e#"lambda" "G" "A" "B" "e"}} => {{e @"lambda" @("D" := #"ty_emp") "A" "e"}}
+  | {{e#"app" "G" "A" "B" "e" "e'"}} => {{e @"app" @("D" := #"ty_emp") "e" "e'"}}
+  | {{e#"bool"}} => {{e @"bool" @("D" := #"ty_emp")}}
+  | {{e#"T" "G"}} => {{e @"T" @("D" := #"ty_emp")}}
+  | {{e#"F" "G"}} => {{e @"F" @("D" := #"ty_emp")}}
+  | {{e#"if" "G" "A" "cond" "e2" "e3"}} => {{e @"if" @("D" := #"ty_emp") "cond" "e2" "e3"}}
+  | {{e#"*"}} => {{e @"*" @("D" := #"ty_emp")}}
+  | {{e#"Error" "G" "t"}} => {{e @"Error" @("D" := #"ty_emp") "t"}}
+  | {{e#"uT" "G"}} => {{e @"uT" @("D" := #"ty_emp")}}
+  | {{e#"uF" "G"}} => {{e @"uF" @("D" := #"ty_emp")}}
+  | {{e#"ulambda" "G" "e"}} => {{e @"ulambda" @("D" := #"ty_emp") "e"}}
+  | {{e#"uapp" "G" "e" "e'"}} => {{e @"uapp" @("D" := #"ty_emp") "e" "e'"}}
+  | {{e#"bool?" "G" "e"}} => {{e @"bool?" @("D" := #"ty_emp") "e"}}
+  | {{e#"mif" "G" "A" "cond" "e2" "e3"}} => {{e @"mif" @("D" := #"ty_emp") "cond" "e2" "e3"}}
+  end.
+
+Derive interoperating_langs_compiler
+        in (elab_preserving_compiler
+                    []
+                    polymorphic_interoperating_langs
+                    interoperating_langs_compiler_def
+                    interoperating_langs_compiler
+                    simple_interoperating_langs)
+        as interoperating_langs_compiler_preserving.
+Proof. auto_elab_compiler. Qed.
+#[local] Definition interoperating_langs_entry :=
+  cmp_entry (elab_compiler_implies_preserving interoperating_langs_compiler_preserving).
+#[export] Hint Resolve interoperating_langs_entry : preserving_db.