diff --git a/.gitignore b/.gitignore index f7d2b7bf..e7e65cac 100644 --- a/.gitignore +++ b/.gitignore @@ -16,4 +16,5 @@ Makefile.d _CoqProject .Makefile.coq.d .coq-native -**/.DS_Store \ No newline at end of file +**/.DS_Store*.timing +*.timing diff --git a/src/Pyrosome/Lang/Multilanguages/Boundaries.v b/src/Pyrosome/Lang/Multilanguages/Boundaries.v new file mode 100644 index 00000000..69570243 --- /dev/null +++ b/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 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. diff --git a/src/Pyrosome/Lang/Multilanguages/InteropLangs.v b/src/Pyrosome/Lang/Multilanguages/InteropLangs.v new file mode 100644 index 00000000..bc4fb484 --- /dev/null +++ b/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 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. diff --git a/src/Pyrosome/Lang/Multilanguages/ParamFragments.v b/src/Pyrosome/Lang/Multilanguages/ParamFragments.v new file mode 100644 index 00000000..71f1cfb4 --- /dev/null +++ b/src/Pyrosome/Lang/Multilanguages/ParamFragments.v @@ -0,0 +1,567 @@ +(* Parameterized (polymorphic) versions of the language fragments that make + up the two interoperating languages, together with the type-substitution + fragment each one needs, and the let/let-eta extension used by the + boundary compiler. Each fragment is registered in [wf_lang_db] so that + later files can discharge well-formedness by [prove_by_lang_db]. *) + +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 with` compiler syntax *) + +From Pyrosome Require Import Theory.Core Elab.Elab + Tools.Matches + Tools.EGraph.TypeInference Tools.EGraph.InjRuleGen 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. +From Pyrosome.Lang Require Import Let. + + +(* 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. + + +(* The target multilanguage is polymorphic, so every fragment that makes up + the two interoperating languages needs a parameterized version. The + helpers below abstract the shape of [stlc_parameterized] in PolyCompilers.v + so that a fragment with no dependencies beyond the substitution calculus + can be parameterized in one line. *) +Definition parameterize_wrapper (l : lang) : lang := + let ps := (elab_param "D" (l + ++ exp_ret + ++ exp_subst_base + ++ value_subst + ) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps l. +Local Definition evp'_general (l : lang) : lang := + let ps := (elab_param "D" (l ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (exp_ret ++ exp_subst_base ++ value_subst). +Ltac solve_parameterize_wrapper l := + change (exp_parameterized++val_parameterized) with (evp'_general l); + eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor + | now prove_by_lang_db.. + | vm_compute; exact I]. + +Definition typed_bool_parameterized := parameterize_wrapper typed_bool. +Lemma typed_bool_parameterized_wf + : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) + typed_bool_parameterized. +Proof. solve_parameterize_wrapper typed_bool. Qed. +#[local] Definition typed_bool_parameterized_entry := + lang_entry typed_bool_parameterized_wf. +#[export] Hint Resolve typed_bool_parameterized_entry : wf_lang_db. + +(* [stlc_parameterized] is already defined in PolyCompilers.v. *) + +(* The parameterizer does not generate the type-substitution equations, so + they are built separately as a small fragment for each parameterized + language. *) +Definition ty_subst_def_maker (parameterized_lang : lang) parameterized_dependencies := eqn_rules + type_subst_mode + (parameterized_dependencies ++ + 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 + ) + (hide_lang_implicits (parameterized_lang ++ parameterized_dependencies ++ + 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 + ) + parameterized_lang). + +Definition typed_bool_ty_subst_def := Eval vm_compute in ty_subst_def_maker typed_bool_parameterized []. +Derive typed_bool_ty_subst + in (elab_lang_ext (typed_bool_parameterized ++ + 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 + ) + typed_bool_ty_subst_def typed_bool_ty_subst) + as typed_bool_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition typed_bool_ty_subst_entry := + lang_entry (elab_lang_implies_wf typed_bool_ty_subst_wf). +#[export] Hint Resolve typed_bool_ty_subst_entry : wf_lang_db. + +Definition stlc_ty_subst_def := Eval vm_compute in ty_subst_def_maker stlc_parameterized []. +Derive stlc_ty_subst + in (elab_lang_ext (stlc_parameterized ++ + 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 + ) + stlc_ty_subst_def stlc_ty_subst) + as stlc_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition stlc_ty_subst_entry := + lang_entry (elab_lang_implies_wf stlc_ty_subst_wf). +#[export] Hint Resolve stlc_ty_subst_entry : wf_lang_db. + +Definition star_type_parameterized := parameterize_wrapper star_type. +Lemma star_type_parameterized_wf : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) star_type_parameterized. +Proof. solve_parameterize_wrapper star_type. Qed. +#[local] Definition star_type_parameterized_entry := + lang_entry star_type_parameterized_wf. +#[export] Hint Resolve star_type_parameterized_entry : wf_lang_db. + +Definition error_t_parameterized := parameterize_wrapper error_t. +Lemma error_t_parameterized_wf : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) error_t_parameterized. +Proof. solve_parameterize_wrapper error_t. Qed. +#[local] Definition error_t_parameterized_entry := + lang_entry error_t_parameterized_wf. +#[export] Hint Resolve error_t_parameterized_entry : wf_lang_db. + +Definition star_type_ty_subst_def := Eval vm_compute in ty_subst_def_maker star_type_parameterized []. +Derive star_type_ty_subst + in (elab_lang_ext (star_type_parameterized ++ + 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 + ) + star_type_ty_subst_def star_type_ty_subst) + as star_type_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition star_type_ty_subst_entry := + lang_entry (elab_lang_implies_wf star_type_ty_subst_wf). +#[export] Hint Resolve star_type_ty_subst_entry : wf_lang_db. + +Definition error_t_ty_subst_def := Eval vm_compute in ty_subst_def_maker error_t_parameterized []. +Derive error_t_ty_subst + in (elab_lang_ext (error_t_parameterized ++ + 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 + ) + error_t_ty_subst_def error_t_ty_subst) + as error_t_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition error_t_ty_subst_entry := + lang_entry (elab_lang_implies_wf error_t_ty_subst_wf). +#[export] Hint Resolve error_t_ty_subst_entry : wf_lang_db. + + +(* The fragments below depend on other fragments, so each needs its own + [evp'] witness naming that dependency chain; [parameterize_wrapper] and + [solve_parameterize_wrapper] only cover the dependency-free case. + TODO: generalize the parameterizing helpers to cover these as well. *) + +Definition utlc_parameterized := + let ps := (elab_param "D" (utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps utlc. +Local Definition evp'_utlc : lang := + let ps := (elab_param "D" (utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). +Lemma utlc_parameterized_wf + : wf_lang_ext ((star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) + utlc_parameterized. +Proof. + replace (star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_utlc. + - eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor (*TODO: include in t'*) + | now prove_by_lang_db.. + | vm_compute; exact I]. + - cbv; reflexivity. +Qed. +#[local] Definition utlc_parameterized_entry := + lang_entry utlc_parameterized_wf. +#[export] Hint Resolve utlc_parameterized_entry : wf_lang_db. + +Definition utlc_ty_subst_def := Eval vm_compute in ty_subst_def_maker utlc_parameterized (star_type_parameterized ++ error_t_parameterized). +Derive utlc_ty_subst + in (elab_lang_ext ( + utlc_parameterized ++ + star_type_ty_subst ++ error_t_ty_subst ++ + star_type_parameterized ++ error_t_parameterized ++ + 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 + ) + utlc_ty_subst_def utlc_ty_subst) + as utlc_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition utlc_ty_subst_entry := + lang_entry (elab_lang_implies_wf utlc_ty_subst_wf). +#[export] Hint Resolve utlc_ty_subst_entry : wf_lang_db. + +Definition untyped_bool_parameterized := + let ps := (elab_param "D" (untyped_bool ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps untyped_bool. +Local Definition evp'_untyped_bool : lang := + let ps := (elab_param "D" (untyped_bool ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). +Lemma untyped_bool_parameterized_wf + : wf_lang_ext ((star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) + untyped_bool_parameterized. +Proof. + replace (star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_untyped_bool. + - eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor (*TODO: include in t'*) + | now prove_by_lang_db.. + | vm_compute; exact I]. + - cbv; reflexivity. +Qed. +#[local] Definition untyped_bool_parameterized_entry := + lang_entry untyped_bool_parameterized_wf. +#[export] Hint Resolve untyped_bool_parameterized_entry : wf_lang_db. + +Definition untyped_bool_ty_subst_def := Eval vm_compute in ty_subst_def_maker untyped_bool_parameterized (star_type_parameterized ++ error_t_parameterized). +Derive untyped_bool_ty_subst + in (elab_lang_ext ( + untyped_bool_parameterized ++ + star_type_ty_subst ++ error_t_ty_subst ++ + star_type_parameterized ++ error_t_parameterized ++ + 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 + ) + untyped_bool_ty_subst_def untyped_bool_ty_subst) + as untyped_bool_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition untyped_bool_ty_subst_entry := + lang_entry (elab_lang_implies_wf untyped_bool_ty_subst_wf). +#[export] Hint Resolve untyped_bool_ty_subst_entry : wf_lang_db. + +Definition boolhuh_parameterized := + let ps := (elab_param "D" (boolhuh ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps boolhuh. +Local Definition evp'_boolhuh : lang := + let ps := (elab_param "D" (boolhuh ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). +Lemma boolhuh_parameterized_wf + : wf_lang_ext ((untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) + boolhuh_parameterized. +Proof. + replace (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_boolhuh. + - eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor (*TODO: include in t'*) + | now prove_by_lang_db.. + | vm_compute; exact I]. + - cbv; reflexivity. +Qed. +#[local] Definition boolhuh_parameterized_entry := + lang_entry boolhuh_parameterized_wf. +#[export] Hint Resolve boolhuh_parameterized_entry : wf_lang_db. + +Definition boolhuh_ty_subst_def := Eval vm_compute in ty_subst_def_maker boolhuh_parameterized (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized). +Derive boolhuh_ty_subst + in (elab_lang_ext ( (* add all dependencies with their ty_subst versions and the current parameterized lang *) + boolhuh_parameterized ++ + untyped_bool_ty_subst ++ + untyped_bool_parameterized ++ + utlc_ty_subst ++ + utlc_parameterized ++ + star_type_ty_subst ++ error_t_ty_subst ++ + star_type_parameterized ++ error_t_parameterized ++ + 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 + ) + boolhuh_ty_subst_def boolhuh_ty_subst) + as boolhuh_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition boolhuh_ty_subst_entry := + lang_entry (elab_lang_implies_wf boolhuh_ty_subst_wf). +#[export] Hint Resolve boolhuh_ty_subst_entry : wf_lang_db. + +(* [utlc_bool] introduces no new syntax, so it needs no ty_subst fragment. *) +Definition utlc_bool_parameterized := + let ps := (elab_param "D" (utlc_bool ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps utlc_bool. +Local Definition evp'_utlc_bool : lang := + let ps := (elab_param "D" (utlc_bool ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). +Lemma utlc_bool_parameterized_wf + : wf_lang_ext ((untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) + utlc_bool_parameterized. +Proof. + replace (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_utlc_bool. + - eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor (*TODO: include in t'*) + | now prove_by_lang_db.. + | vm_compute; exact I]. + - cbv; reflexivity. +Qed. +#[local] Definition utlc_bool_parameterized_entry := + lang_entry utlc_bool_parameterized_wf. +#[export] Hint Resolve utlc_bool_parameterized_entry : wf_lang_db. + +Definition mif_parameterized := + let ps := (elab_param "D" (mif ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps mif. +Local Definition evp'_mif : lang := + let ps := (elab_param "D" (mif ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). +Lemma mif_parameterized_wf + : wf_lang_ext ((untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) + mif_parameterized. +Proof. + replace (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_mif. + - eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor + | now prove_by_lang_db.. + | vm_compute; exact I]. + - cbv; reflexivity. +Qed. +#[local] Definition mif_parameterized_entry := + lang_entry mif_parameterized_wf. +#[export] Hint Resolve mif_parameterized_entry : wf_lang_db. + +Definition mif_ty_subst_def := Eval vm_compute in ty_subst_def_maker mif_parameterized (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized). +Derive mif_ty_subst + in (elab_lang_ext ( (* add all dependencies with their ty_subst versions and the current parameterized lang *) + mif_parameterized ++ + untyped_bool_ty_subst ++ + untyped_bool_parameterized ++ + utlc_ty_subst ++ + utlc_parameterized ++ + star_type_ty_subst ++ error_t_ty_subst ++ + star_type_parameterized ++ error_t_parameterized ++ + 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 + ) + mif_ty_subst_def mif_ty_subst) + as mif_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition mif_ty_subst_entry := + lang_entry (elab_lang_implies_wf mif_ty_subst_wf). +#[export] Hint Resolve mif_ty_subst_entry : wf_lang_db. + +Definition prod_parameterized := parameterize_wrapper prod. +Lemma prod_parameterized_wf + : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) + prod_parameterized. +Proof. solve_parameterize_wrapper prod. Qed. +#[local] Definition prod_parameterized_entry := + lang_entry prod_parameterized_wf. +#[export] Hint Resolve prod_parameterized_entry : wf_lang_db. +Definition prod_ty_subst_def := Eval vm_compute in ty_subst_def_maker prod_parameterized []. +Derive prod_ty_subst + in (elab_lang_ext (prod_parameterized ++ + 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 + ) + prod_ty_subst_def prod_ty_subst) + as prod_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition prod_ty_subst_entry := + lang_entry (elab_lang_implies_wf prod_ty_subst_wf). +#[export] Hint Resolve prod_ty_subst_entry : wf_lang_db. + + +(* ------------------------------------------------------------------ *) +(* The let extension (Let.v) and a one-rule eta law for it. + + These are part of the target multilanguage so that the boundary compiler + can let-bind its argument -- a variable is a value, so [STLC-beta] applies + to it -- and so that [let e (ret hd)] collapses back to [e]. *) + +Definition let_eta_def : lang := + {[l/subst [exp_subst++value_subst] + [:= "G" : #"env", + "A" : #"ty", + "e" : #"exp" "G" "A" + ----------------------------------------------- ("let eta") + #"let" "e" (#"ret" #"hd") = "e" : #"exp" "G" "A" + ] ]}. + +Definition let_eta := + Eval vm_compute in + infer_lang_ext_simple_incr 10 100 (let_lang ++ exp_subst ++ value_subst) let_eta_def. + +Lemma let_eta_wf : wf_lang_ext (let_lang ++ exp_subst ++ value_subst) let_eta. +Proof. compute_wf_lang. Qed. +#[local] Definition let_eta_entry := lang_entry let_eta_wf. +#[export] Hint Resolve let_eta_entry : wf_lang_db. + +Definition let_parameterized := parameterize_wrapper let_lang. +Lemma let_parameterized_wf + : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) + let_parameterized. +Proof. solve_parameterize_wrapper let_lang. Qed. +#[local] Definition let_parameterized_entry := + lang_entry let_parameterized_wf. +#[export] Hint Resolve let_parameterized_entry : wf_lang_db. + +Definition let_ty_subst_def := Eval vm_compute in ty_subst_def_maker let_parameterized []. +Derive let_ty_subst + in (elab_lang_ext (let_parameterized ++ + 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 + ) + let_ty_subst_def let_ty_subst) + as let_ty_subst_wf. +Proof. auto_elab. Qed. +#[local] Definition let_ty_subst_entry := + lang_entry (elab_lang_implies_wf let_ty_subst_wf). +#[export] Hint Resolve let_ty_subst_entry : wf_lang_db. + +(* [let_eta] introduces no new syntax, so (like [utlc_bool]) it needs no + ty_subst fragment. *) +Definition let_eta_parameterized := + let ps := (elab_param "D" (let_eta ++ let_lang ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps let_eta. +Local Definition evp'_let_eta : lang := + let ps := (elab_param "D" (let_eta ++ let_lang ++ exp_ret ++ exp_subst_base + ++ value_subst) + [("sub", Some 2); + ("ty", Some 0); + ("env", Some 0); + ("val",Some 2); + ("exp",Some 2)]) in + parameterize_lang "D" {{s #"ty_env"}} + ps (let_lang ++ exp_ret ++ exp_subst_base ++ value_subst). +Lemma let_eta_parameterized_wf + : wf_lang_ext ((let_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) + let_eta_parameterized. +Proof. + replace (let_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_let_eta. + - eapply parameterize_lang_preserving_ext; + try typeclasses eauto; + [repeat t'; constructor + | now prove_by_lang_db.. + | vm_compute; exact I]. + - cbv; reflexivity. +Qed. +#[local] Definition let_eta_parameterized_entry := + lang_entry let_eta_parameterized_wf. +#[export] Hint Resolve let_eta_parameterized_entry : wf_lang_db. diff --git a/src/Pyrosome/Lang/Multilanguages/PolyBoundaries.v b/src/Pyrosome/Lang/Multilanguages/PolyBoundaries.v index 1261f56d..c55574ca 100644 --- a/src/Pyrosome/Lang/Multilanguages/PolyBoundaries.v +++ b/src/Pyrosome/Lang/Multilanguages/PolyBoundaries.v @@ -1,3 +1,13 @@ +(* Stage G: the polymorphic boundaries. + + [boundaries] and its type-casing rules, re-derived at an arbitrary type + environment by the parameterizer, extended with the two quantifier + boundary rules of Matthews and Findler; then the poly -> poly compiler + into [target_multilanguage] and its preservation proof. + + The structure mirrors SimpleMultilangCompiler.v (the unparameterized + version of the same compiler); see README.md for the file layout. *) + Set Implicit Arguments. Require Import Datatypes.String Lists.List. @@ -7,33 +17,31 @@ Open Scope list. From Utils Require Import Utils. (* imports for compilers *) -(* copied from LinearCPS.v *) From Pyrosome Require Import Compilers.Compilers Elab.ElabCompilers. -Import CompilerDefs.Notations. (* for `match # from high_level_multilanguage with` *) -(* CompilerDefs, for preserving_compiler_ext, is already imported. Prolly through something else. *) +Import CompilerDefs.Notations. (* for the `match # from _ with` compiler notation *) From Pyrosome Require Import Theory.Core Elab.Elab Tools.Matches Tools.EGraph.TypeInference Tools.Resolution Tools.EGraph.ComputeWf. Import Core.Notations. -Require Coq.derive.Derive. +From Stdlib Require derive.Derive. (* import the relevant language fragments *) -From Pyrosome.Lang Require Import SimpleVSTLC. -From Pyrosome.Lang Require Import UTLC. -From Pyrosome.Lang Require Import BoolType. +From Pyrosome.Lang Require Import SimpleVSTLC. +From Pyrosome.Lang Require Import UTLC. +From Pyrosome.Lang Require Import BoolType. From Pyrosome.Lang Require Import SimpleVProd. -From Pyrosome.Lang.Multilanguages Require Import SimpleBoundaries. +From Pyrosome.Lang.Multilanguages Require Import SimpleBoundaries. (* imports for polymorphism *) From Pyrosome.Lang Require Import PolySubst SimpleVSubst. -From Pyrosome.Lang Require Import PolyCompilers. (* for parameterizing existing languages*) +From Pyrosome.Lang Require Import PolyCompilerLangs PolyCompilersCPS PolyCompilers. (* for parameterizing existing languages*) From Pyrosome.Compilers Require Import Parameterizer. Import Pyrosome.Tools.UnElab. -Definition boundaries_parameterized := +Definition boundaries_parameterized := let ps := (elab_param "D" (boundaries ++ stlc ++ typed_bool ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) [("sub", Some 2); ("ty", Some 0); @@ -42,7 +50,7 @@ Definition boundaries_parameterized := ("exp",Some 2)]) in parameterize_lang "D" {{s #"ty_env"}} ps boundaries. -Local Definition evp'_boundaries : lang := +Local Definition evp'_boundaries : lang := let ps := (elab_param "D" (boundaries ++ stlc ++ typed_bool ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) [("sub", Some 2); ("ty", Some 0); @@ -54,44 +62,35 @@ Local Definition evp'_boundaries : lang := Lemma boundaries_parameterized_wf (* this is necessary *) : wf_lang_ext ((stlc_parameterized ++ typed_bool_parameterized ++ untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) boundaries_parameterized. -Proof. +Proof. replace (stlc_parameterized ++ typed_bool_parameterized ++ untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_boundaries. - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor - | now prove_by_lang_db.. - | vm_compute; exact I]. - - cbv; reflexivity. -Qed. + try typeclasses eauto; + [ repeat t'; constructor + | now prove_by_lang_db.. + | vm_compute; exact I ]. + - cbv; reflexivity. +Qed. #[local] Definition boundaries_parameterized_entry := lang_entry boundaries_parameterized_wf. #[export] Hint Resolve boundaries_parameterized_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. - -(* Lemma boundaries_parameterized_wf_2 : *) -(* wf_lang (boundaries_parameterized ++ polymorphic_interoperating_langs). *) -(* Proof. prove_by_lang_db. Qed. *) +(* [polymorphic_interoperating_langs_wf] lives in InteropLangs.v. *) Definition boundaries_ty_subst_def := Eval vm_compute in ty_subst_def_maker boundaries_parameterized (stlc_parameterized ++ typed_bool_parameterized ++ untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized). Derive boundaries_ty_subst - SuchThat (elab_lang_ext + in (elab_lang_ext (boundaries_parameterized ++ polymorphic_interoperating_langs) boundaries_ty_subst_def boundaries_ty_subst) - As boundaries_ty_subst_wf. -Proof. auto_elab. Qed. + as boundaries_ty_subst_wf. +Proof. auto_elab. Qed. #[local] Definition boundaries_ty_subst_entry := lang_entry (elab_lang_implies_wf boundaries_ty_subst_wf). #[export] Hint Resolve boundaries_ty_subst_entry : wf_lang_db. Definition poly_boundaries_def : lang := (* Matthews and Findler figure 11, page 12:33 *) - {[l/subst [exp_subst++value_subst] + {[l/subst [exp_subst++value_subst] [:= "D" : #"ty_env", "G" : #"env" "D", "A" : #"ty" (#"ty_ext" "D"), (* tau in Matthews and Findler *) @@ -100,7 +99,7 @@ Definition poly_boundaries_def : lang := (* Matthews and Findler figure 11, page #"dtt" (#"All" "A") "e" = #"ret" (#"Lam" (#"dtt" "A" (#"exp_ty_subst" #"ty_wkn" "e"))) : #"exp" "D" "G" (#"All" "A") - ]; + ]; [:= "D" : #"ty_env", "G" : #"env" "D", "A" : #"ty" (#"ty_ext" "D"), (* tau in Matthews and Findler *) @@ -108,25 +107,22 @@ Definition poly_boundaries_def : lang := (* Matthews and Findler figure 11, page ----------------------------------------------- ("ttd forall") #"ttd" (#"All" "A") "e" = #"ttd" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "A") (#"@" "e" #"*") : #"exp" "D" "G" #"*" - ] + ] ]}. Derive poly_boundaries - SuchThat (elab_lang_ext (boundaries_ty_subst ++ + in (elab_lang_ext (boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs) poly_boundaries_def poly_boundaries) - As poly_boundaries_wf. + as poly_boundaries_wf. Proof. auto_elab. Qed. #[local] Definition poly_boundaries_entry := lang_entry (elab_lang_implies_wf poly_boundaries_wf). #[export] Hint Resolve poly_boundaries_entry : wf_lang_db. -(* Aight so the problem you were having had to do with names and prove_by_lang_db. I think the moral solution is to add ty_subst to all the wf proofs for ty_subst langs above. But whatever I did works enough it looks like. *) - - (* Matthews and Findler have lump cancellation as a rule. But, we don't need that rule, (I think) because we've collapsed the Lump and TST types! *) Definition lump_cancellation_term_unelab := - {{e #"ttd" #"*" (#"dtt" #"*" "e") }}. + {{e #"ttd" #"*" (#"dtt" #"*" "e") }}. Derive lump_cancellation_term in ( elab_term (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs) @@ -136,9 +132,10 @@ Derive lump_cancellation_term lump_cancellation_term_unelab lump_cancellation_term {{s #"exp" "D" "G" (#"*" "D") }} - ) as lump_cancellation_term_wf. + ) as lump_cancellation_term_wf. Proof. - solve_elab_term_or_sort (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs). + solve_elab_term_or_sort + (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs). Qed. Lemma lump_cancellation_holds : @@ -151,7 +148,8 @@ Lemma lump_cancellation_holds : {{e "e" }} lump_cancellation_term. Proof. - assert (wf_lang (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs)) by prove_by_lang_db; by_reduction. + assert (wf_lang (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs)) by prove_by_lang_db. + by_reduction. Qed. @@ -172,7 +170,7 @@ Lemma polymorphic_interoperating_langs_compiler_preserving : polymorphic_interoperating_langs_compiler polymorphic_interoperating_langs. Proof. - apply id_compiler_preserving; [ typeclasses eauto | prove_by_lang_db ]. + apply id_compiler_preserving; [ typeclasses eauto | prove_by_lang_db ]. Qed. #[local] Definition polymorphic_interoperating_langs_compiler_entry := cmp_entry polymorphic_interoperating_langs_compiler_preserving. @@ -183,7 +181,7 @@ Definition dtt_forall_partial_eval_ctx := Eval vm_compute in Rule.get_ctx (named_list_lookup default poly_boundaries "dtt forall"). Definition dtt_forall_partial_eval_term_def := - {{e #"ret" (#"Lam" (#"dtt" "A" (#"exp_ty_subst" #"ty_wkn" "e"))) }}. + {{e #"ret" (#"Lam" (#"dtt" "A" (#"exp_ty_subst" #"ty_wkn" "e"))) }}. Derive dtt_forall_partial_eval_term in ( elab_term (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs) @@ -191,9 +189,10 @@ Derive dtt_forall_partial_eval_term dtt_forall_partial_eval_term_def dtt_forall_partial_eval_term {{s #"exp" "D" "G" (#"All" "D" "A") }} - ) as dtt_forall_partial_eval_term_wf. + ) as dtt_forall_partial_eval_term_wf. Proof. - solve_elab_term_or_sort (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs). + solve_elab_term_or_sort + (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs). Qed. Definition ttd_forall_partial_eval_ctx := @@ -208,9 +207,10 @@ Derive ttd_forall_partial_eval_term ttd_forall_partial_eval_term_def ttd_forall_partial_eval_term {{s #"exp" "D" "G" (#"*" "D") }} - ) as ttd_forall_partial_eval_term_wf. + ) as ttd_forall_partial_eval_term_wf. Proof. - solve_elab_term_or_sort (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs). + solve_elab_term_or_sort + (poly_boundaries ++ boundaries_ty_subst ++ boundaries_parameterized ++ polymorphic_interoperating_langs). Qed. Fixpoint forall_partial_eval (program : term) : term := @@ -226,16 +226,339 @@ Fixpoint forall_partial_eval (program : term) : term := (* poly to poly compiler *) Definition poly_multilang_compiler_def : compiler := match # from boundaries_parameterized with - | {{e #"dtt" "D" "G" "A" "e"}} => {{e #"app" (#".2" {trec_boundaries_unelab}) "e" }} - | {{e #"ttd" "D" "G" "A" "e"}} => {{e #"app" (#".1" {trec_boundaries_unelab}) "e" }} + | {{e #"dtt" "D" "G" "A" "e"}} => + {{e #"let" "e" (#"app" (#".2" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }} + | {{e #"ttd" "D" "G" "A" "e"}} => + {{e #"let" "e" (#"app" (#".1" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }} (* we don't need a type variable case, since it's the same as the old compiler! *) end. -(* Derive poly_multilang_compiler *) -(* SuchThat (elab_preserving_compiler *) -(* interoperating_langs_compiler *) -(* target_multilanguage *) -(* poly_multilang_compiler_def *) -(* poly_multilang_compiler *) -(* boundaries) *) -(* As poly_multilang_compiler_preserving. *) -(* Proof. solve_multilang_compiler. Qed. *) +(* ------------------------------------------------------------------ *) +(* Stage G: the poly -> poly compiler. + + The source language is [boundaries_parameterized]; its ambient prefix is + [polymorphic_interoperating_langs] (that is the language + [boundaries_parameterized_wf] extends, up to the fragments' ty_subst + rules). So the prefix compiler is + [polymorphic_interoperating_langs_compiler], the *identity* compiler on + [polymorphic_interoperating_langs] -- NOT [interoperating_langs_compiler], + which has the *simple* (unparameterized) interoperating languages as its + source and would not typecheck here. The target is + [target_multilanguage], which contains [polymorphic_interoperating_langs] + as a suffix, so the identity prefix compiler is target-valid. + + As in SimpleMultilangCompiler.v, the two cases are elaborated by hand + from the [typerec] term; here it has to be re-elaborated at a general + type environment "D" (that file's [trec_boundaries] lives at + #"ty_emp"). *) + +Derive trec_boundaries_poly + in ( elab_term target_multilanguage + [("A", {{s #"ty" "D"}}); ("G", {{s #"env" "D"}}); ("D", {{s #"ty_env"}})] + trec_boundaries_unelab + trec_boundaries_poly + {{s #"val" "D" "G" + (#"prod" "D" + (#"->" "D" "A" (#"*" "D")) + (#"->" "D" (#"*" "D") "A")) }} + ) as trec_boundaries_poly_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +(* The compiled bodies let-bind the source argument "e" and apply the + boundary function to [#"ret" #"hd"], so that [STLC-beta] (which needs a + value argument) fires; ["let eta"] then collapses the residual + [#"let" "e" (#"ret" #"hd")]. Elaborated individually, as in + SimpleMultilangCompiler.v. *) + +Definition poly_dtt_case_unelab := + {{e #"let" "e" (#"app" (#".2" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }}. + +Derive poly_dtt_case_tgt + in ( elab_term target_multilanguage + [("e", {{s #"exp" "D" "G" (#"*" "D")}}); + ("A", {{s #"ty" "D"}}); + ("G", {{s #"env" "D"}}); + ("D", {{s #"ty_env"}})] + poly_dtt_case_unelab + poly_dtt_case_tgt + {{s #"exp" "D" "G" "A"}} + ) as poly_dtt_case_tgt_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +Definition poly_ttd_case_unelab := + {{e #"let" "e" (#"app" (#".1" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }}. + +Derive poly_ttd_case_tgt + in ( elab_term target_multilanguage + [("e", {{s #"exp" "D" "G" "A"}}); + ("A", {{s #"ty" "D"}}); + ("G", {{s #"env" "D"}}); + ("D", {{s #"ty_env"}})] + poly_ttd_case_unelab + poly_ttd_case_tgt + {{s #"exp" "D" "G" (#"*" "D")}} + ) as poly_ttd_case_tgt_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +(* NOTE: the entries must be in the SAME ORDER as the term rules of + [boundaries_parameterized] (["dtt"] before ["ttd"]); see the note in + SimpleMultilangCompiler.v. Compilation is by name lookup, so the order + changes no compiled term. *) +Definition poly_multilang_compiler + : @CompilerDefs.compiler string (Term.term string) (Term.sort string) := + [("dtt", term_case ["e"; "A"; "G"; "D"] poly_dtt_case_tgt); + ("ttd", term_case ["e"; "A"; "G"; "D"] poly_ttd_case_tgt)]. + +Lemma poly_dtt_case_wf + : wf_term target_multilanguage + [("e", {{s #"exp" "D" "G" (#"*" "D")}}); + ("A", {{s #"ty" "D"}}); + ("G", {{s #"env" "D"}}); + ("D", {{s #"ty_env"}})] + poly_dtt_case_tgt {{s #"exp" "D" "G" "A"}}. +Proof. pose proof target_multilanguage_wf. compute_term_wf. Qed. + +Lemma poly_ttd_case_wf + : wf_term target_multilanguage + [("e", {{s #"exp" "D" "G" "A"}}); + ("A", {{s #"ty" "D"}}); + ("G", {{s #"env" "D"}}); + ("D", {{s #"ty_env"}})] + poly_ttd_case_tgt {{s #"exp" "D" "G" (#"*" "D")}}. +Proof. pose proof target_multilanguage_wf. compute_term_wf. Qed. + +(* ------------------------------------------------------------------ *) +(* Per-equation machinery, as in SimpleMultilangCompiler.v. Each compiled + equation is discharged by [by_reduction_fwd], that file's forward-only + e-graph tactic (every target rule used left-to-right only); the same + reasons for forward-only saturation apply here. *) + +Definition PCMP := poly_multilang_compiler ++ polymorphic_interoperating_langs_compiler. + +Definition pbrule (n:string) := + named_list_lookup (Rule.sort_rule [] []) boundaries_parameterized n. +Definition pgctx n := match pbrule n with Rule.term_eq_rule c _ _ _ => compile_ctx PCMP c | _ => [] end. +Definition pgsrt n := match pbrule n with Rule.term_eq_rule _ _ _ t => compile_sort PCMP t | _ => default end. +Definition pglhs n := match pbrule n with Rule.term_eq_rule _ e _ _ => compile PCMP e | _ => default end. +Definition pgrhs n := match pbrule n with Rule.term_eq_rule _ _ e _ => compile PCMP e | _ => default end. + +(* ------------------------------------------------------------------ *) +(* One [eq_term] lemma per equation of [boundaries_parameterized]. *) + +Definition pc_dtt_star := Eval vm_compute in pgctx "dtt star". +Definition ps_dtt_star := Eval vm_compute in pgsrt "dtt star". +Definition pl_dtt_star := Eval vm_compute in pglhs "dtt star". +Definition pr_dtt_star := Eval vm_compute in pgrhs "dtt star". +(* Provable because the compiler let-binds "e": the beta-redex has a value + (the variable [#"hd"]) as its argument, and ["let eta"] collapses the + residual [#"let" "e" (#"ret" #"hd")] back to "e". *) +Lemma peq_dtt_star : eq_term target_multilanguage pc_dtt_star ps_dtt_star pl_dtt_star pr_dtt_star. +Proof. unfold pc_dtt_star, ps_dtt_star, pl_dtt_star, pr_dtt_star. by_reduction_fwd. Qed. + +Definition pc_ttd_star := Eval vm_compute in pgctx "ttd star". +Definition ps_ttd_star := Eval vm_compute in pgsrt "ttd star". +Definition pl_ttd_star := Eval vm_compute in pglhs "ttd star". +Definition pr_ttd_star := Eval vm_compute in pgrhs "ttd star". +(* As "dtt star", through the [#".1"] projection. *) +Lemma peq_ttd_star : eq_term target_multilanguage pc_ttd_star ps_ttd_star pl_ttd_star pr_ttd_star. +Proof. unfold pc_ttd_star, ps_ttd_star, pl_ttd_star, pr_ttd_star. by_reduction_fwd. Qed. + +Definition pc_dtt_True := Eval vm_compute in pgctx "dtt True". +Definition ps_dtt_True := Eval vm_compute in pgsrt "dtt True". +Definition pl_dtt_True := Eval vm_compute in pglhs "dtt True". +Definition pr_dtt_True := Eval vm_compute in pgrhs "dtt True". +Lemma peq_dtt_True : eq_term target_multilanguage pc_dtt_True ps_dtt_True pl_dtt_True pr_dtt_True. +Proof. unfold pc_dtt_True, ps_dtt_True, pl_dtt_True, pr_dtt_True. by_reduction_fwd. Qed. + +Definition pc_dtt_False := Eval vm_compute in pgctx "dtt False". +Definition ps_dtt_False := Eval vm_compute in pgsrt "dtt False". +Definition pl_dtt_False := Eval vm_compute in pglhs "dtt False". +Definition pr_dtt_False := Eval vm_compute in pgrhs "dtt False". +Lemma peq_dtt_False : eq_term target_multilanguage pc_dtt_False ps_dtt_False pl_dtt_False pr_dtt_False. +Proof. unfold pc_dtt_False, ps_dtt_False, pl_dtt_False, pr_dtt_False. by_reduction_fwd. Qed. + +Definition pc_ttd_True := Eval vm_compute in pgctx "ttd True". +Definition ps_ttd_True := Eval vm_compute in pgsrt "ttd True". +Definition pl_ttd_True := Eval vm_compute in pglhs "ttd True". +Definition pr_ttd_True := Eval vm_compute in pgrhs "ttd True". +Lemma peq_ttd_True : eq_term target_multilanguage pc_ttd_True ps_ttd_True pl_ttd_True pr_ttd_True. +Proof. unfold pc_ttd_True, ps_ttd_True, pl_ttd_True, pr_ttd_True. by_reduction_fwd. Qed. + +Definition pc_ttd_False := Eval vm_compute in pgctx "ttd False". +Definition ps_ttd_False := Eval vm_compute in pgsrt "ttd False". +Definition pl_ttd_False := Eval vm_compute in pglhs "ttd False". +Definition pr_ttd_False := Eval vm_compute in pgrhs "ttd False". +Lemma peq_ttd_False : eq_term target_multilanguage pc_ttd_False ps_ttd_False pl_ttd_False pr_ttd_False. +Proof. unfold pc_ttd_False, ps_ttd_False, pl_ttd_False, pr_ttd_False. by_reduction_fwd. Qed. + +Definition pc_dtt_func := Eval vm_compute in pgctx "dtt func". +Definition ps_dtt_func := Eval vm_compute in pgsrt "dtt func". +Definition pl_dtt_func := Eval vm_compute in pglhs "dtt func". +Definition pr_dtt_func := Eval vm_compute in pgrhs "dtt func". +(* Proved below, after the hop lemmas. *) + +Definition pc_ttd_func := Eval vm_compute in pgctx "ttd func". +Definition ps_ttd_func := Eval vm_compute in pgsrt "ttd func". +Definition pl_ttd_func := Eval vm_compute in pglhs "ttd func". +Definition pr_ttd_func := Eval vm_compute in pgrhs "ttd func". +(* Proved below, after the hop lemmas. *) + +(* ------------------------------------------------------------------ *) +(* The two ["func"] equations, in TWO HOPS (see SimpleMultilangCompiler.v + for the full diagnosis): the ["typerec func"] rewrite strictly grows the + term, and [egraph_reducing_equal] restarts saturation from the smallest + extracted representative, so it never runs in the same round as the rest. + [PI1] / [PJ1] are the compiled left-hand sides with the [#"typerec"] at + [#"->" "A" "B"] replaced by its ["typerec func"] reduct. *) + +Definition PTRECv X := {{e #"typerec" {X} {boundary_sigma} #"bstar" #"bbool" + (#"bfunc" {tva} {tvb} {ovar 1} {ovar 0}) }}. + +Definition PI1_unelab := + {{e #"let" (#"ret" (#"ulambda" "e")) + (#"app" (#".2" (#"ret" (#"val_subst" #"wkn" + (#"bfunc" "A" "B" {PTRECv {{e "A"}} } {PTRECv {{e "B"}} })))) + (#"ret" #"hd")) }}. + +Derive PI1 in (elab_term target_multilanguage pc_dtt_func PI1_unelab PI1 ps_dtt_func) + as PI1_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +Definition PJ1_unelab := + {{e #"let" (#"ret" "v") + (#"app" (#".1" (#"ret" (#"val_subst" #"wkn" + (#"bfunc" "A" "B" {PTRECv {{e "A"}} } {PTRECv {{e "B"}} })))) + (#"ret" #"hd")) }}. + +Derive PJ1 in (elab_term target_multilanguage pc_ttd_func PJ1_unelab PJ1 ps_ttd_func) + as PJ1_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +(* hop 1: ["typerec func"] only. *) +Lemma peq_dtt_func_hop1 + : eq_term target_multilanguage pc_dtt_func ps_dtt_func pl_dtt_func PI1. +Proof. unfold pl_dtt_func, pc_dtt_func, ps_dtt_func. by_reduction_fwd. Qed. + +(* hop 2: ["bfunc def"], STLC-beta, ["bool?-func"], ["mif false"], substitution. *) +Lemma peq_dtt_func_hop2 + : eq_term target_multilanguage pc_dtt_func ps_dtt_func PI1 pr_dtt_func. +Proof. unfold pr_dtt_func, pc_dtt_func, ps_dtt_func. by_reduction_fwd. Qed. + +Lemma peq_ttd_func_hop1 + : eq_term target_multilanguage pc_ttd_func ps_ttd_func pl_ttd_func PJ1. +Proof. unfold pl_ttd_func, pc_ttd_func, ps_ttd_func. by_reduction_fwd. Qed. + +Lemma peq_ttd_func_hop2 + : eq_term target_multilanguage pc_ttd_func ps_ttd_func PJ1 pr_ttd_func. +Proof. unfold pr_ttd_func, pc_ttd_func, ps_ttd_func. by_reduction_fwd. Qed. + +Lemma peq_dtt_func : eq_term target_multilanguage pc_dtt_func ps_dtt_func pl_dtt_func pr_dtt_func. +Proof. eapply eq_term_trans; [apply peq_dtt_func_hop1 | apply peq_dtt_func_hop2]. Qed. + +Lemma peq_ttd_func : eq_term target_multilanguage pc_ttd_func ps_ttd_func pl_ttd_func pr_ttd_func. +Proof. eapply eq_term_trans; [apply peq_ttd_func_hop1 | apply peq_ttd_func_hop2]. Qed. + +Definition pc_dtt_ulambda_mismatch := Eval vm_compute in pgctx "dtt ulambda mismatch". +Definition ps_dtt_ulambda_mismatch := Eval vm_compute in pgsrt "dtt ulambda mismatch". +Definition pl_dtt_ulambda_mismatch := Eval vm_compute in pglhs "dtt ulambda mismatch". +Definition pr_dtt_ulambda_mismatch := Eval vm_compute in pgrhs "dtt ulambda mismatch". +Lemma peq_dtt_ulambda_mismatch : eq_term target_multilanguage pc_dtt_ulambda_mismatch ps_dtt_ulambda_mismatch pl_dtt_ulambda_mismatch pr_dtt_ulambda_mismatch. +Proof. unfold pc_dtt_ulambda_mismatch, ps_dtt_ulambda_mismatch, pl_dtt_ulambda_mismatch, pr_dtt_ulambda_mismatch. by_reduction_fwd. Qed. + +Definition pc_dtt_uT_mismatch := Eval vm_compute in pgctx "dtt uT mismatch". +Definition ps_dtt_uT_mismatch := Eval vm_compute in pgsrt "dtt uT mismatch". +Definition pl_dtt_uT_mismatch := Eval vm_compute in pglhs "dtt uT mismatch". +Definition pr_dtt_uT_mismatch := Eval vm_compute in pgrhs "dtt uT mismatch". +(* Closed by the explicit-argument [#"bfunc"] plus the forward-only filter: + ["typerec func"] instantiates [#"bfunc"] in one rewrite, so ["bfunc def"] + unfolds an already-instantiated body and the eager [#"mif"] / [#"bool?"] + check reduces to [#"Error"]. *) +Lemma peq_dtt_uT_mismatch : eq_term target_multilanguage pc_dtt_uT_mismatch ps_dtt_uT_mismatch pl_dtt_uT_mismatch pr_dtt_uT_mismatch. +Proof. unfold pc_dtt_uT_mismatch, ps_dtt_uT_mismatch, pl_dtt_uT_mismatch, pr_dtt_uT_mismatch. by_reduction_fwd. Qed. + +Definition pc_dtt_uF_mismatch := Eval vm_compute in pgctx "dtt uF mismatch". +Definition ps_dtt_uF_mismatch := Eval vm_compute in pgsrt "dtt uF mismatch". +Definition pl_dtt_uF_mismatch := Eval vm_compute in pglhs "dtt uF mismatch". +Definition pr_dtt_uF_mismatch := Eval vm_compute in pgrhs "dtt uF mismatch". +(* As "dtt uT mismatch". *) +Lemma peq_dtt_uF_mismatch : eq_term target_multilanguage pc_dtt_uF_mismatch ps_dtt_uF_mismatch pl_dtt_uF_mismatch pr_dtt_uF_mismatch. +Proof. unfold pc_dtt_uF_mismatch, ps_dtt_uF_mismatch, pl_dtt_uF_mismatch, pr_dtt_uF_mismatch. by_reduction_fwd. Qed. + +Definition pc_exp_subst_dtt := Eval vm_compute in pgctx "exp_subst dtt". +Definition ps_exp_subst_dtt := Eval vm_compute in pgsrt "exp_subst dtt". +Definition pl_exp_subst_dtt := Eval vm_compute in pglhs "exp_subst dtt". +Definition pr_exp_subst_dtt := Eval vm_compute in pgrhs "exp_subst dtt". +(* The three typerec cases are constants with one-step substitution rules + ("val_subst bstar"/"bbool"/"bfunc"), so [#"exp_subst"] does not have to be + pushed through the whole typerec body. *) +Lemma peq_exp_subst_dtt : eq_term target_multilanguage pc_exp_subst_dtt ps_exp_subst_dtt pl_exp_subst_dtt pr_exp_subst_dtt. +Proof. unfold pc_exp_subst_dtt, ps_exp_subst_dtt, pl_exp_subst_dtt, pr_exp_subst_dtt. by_reduction_fwd. Qed. + +Definition pc_exp_subst_ttd := Eval vm_compute in pgctx "exp_subst ttd". +Definition ps_exp_subst_ttd := Eval vm_compute in pgsrt "exp_subst ttd". +Definition pl_exp_subst_ttd := Eval vm_compute in pglhs "exp_subst ttd". +Definition pr_exp_subst_ttd := Eval vm_compute in pgrhs "exp_subst ttd". +(* As "exp_subst dtt". *) +Lemma peq_exp_subst_ttd : eq_term target_multilanguage pc_exp_subst_ttd ps_exp_subst_ttd pl_exp_subst_ttd pr_exp_subst_ttd. +Proof. unfold pc_exp_subst_ttd, ps_exp_subst_ttd, pl_exp_subst_ttd, pr_exp_subst_ttd. by_reduction_fwd. Qed. + +(* ------------------------------------------------------------------ *) +(* All 13 equations of [boundaries_parameterized] are discharged above, so + the whole-compiler theorem is assembled from them by hand, as in + SimpleMultilangCompiler.v: [compute_preserving_compiler] is not usable, + since its [eq_term_oracle] would re-run the e-graph on every equation, + including the two ["func"] ones that only converge when split into hops. + + [ppct] is [CompilerDefs.preserving_compiler_term] restated with the + [map fst c = cargs] side condition as an explicit (computational) + premise; the constructor as stated cannot be applied, since unifying + [map fst ?c] with the literal argument list of a [term_case] is not a + unification problem Coq can solve. + + [boundaries_parameterized] is a computed term, not a literal list, so the + constructors cannot see its cons cells; force it to a literal first. *) +Definition boundaries_parameterized_lit := Eval vm_compute in boundaries_parameterized. +Lemma boundaries_parameterized_lit_eq + : boundaries_parameterized = boundaries_parameterized_lit. +Proof. vm_compute. reflexivity. Qed. + +Lemma ppct + : forall cmp l n c args e t cargs, + preserving_compiler_ext target_multilanguage + polymorphic_interoperating_langs_compiler cmp l -> + map fst c = cargs -> + Model.wf_term (Model := core_model target_multilanguage) + (compile_ctx (cmp ++ polymorphic_interoperating_langs_compiler) c) e + (compile_sort (cmp ++ polymorphic_interoperating_langs_compiler) t) -> + preserving_compiler_ext target_multilanguage + polymorphic_interoperating_langs_compiler ((n, term_case cargs e)::cmp) + ((n, term_rule c args t) :: l). +Proof. intros; subst; constructor; auto. Qed. + +Ltac solve_poly_boundary_case := + solve [ exact poly_dtt_case_wf | exact poly_ttd_case_wf + | exact peq_dtt_star | exact peq_ttd_star + | exact peq_dtt_True | exact peq_dtt_False + | exact peq_ttd_True | exact peq_ttd_False + | exact peq_dtt_func | exact peq_ttd_func + | exact peq_dtt_ulambda_mismatch + | exact peq_dtt_uT_mismatch | exact peq_dtt_uF_mismatch + | exact peq_exp_subst_dtt | exact peq_exp_subst_ttd ]. + +Lemma poly_multilang_compiler_preserving + : preserving_compiler_ext target_multilanguage + polymorphic_interoperating_langs_compiler poly_multilang_compiler + boundaries_parameterized. +Proof. + rewrite boundaries_parameterized_lit_eq. + unfold boundaries_parameterized_lit, poly_multilang_compiler. + repeat lazymatch goal with + | |- CompilerDefs.preserving_compiler_ext _ _ _ => + first [ eapply ppct; [ | vm_compute; reflexivity | ] + | constructor ] + end. + all: solve_poly_boundary_case. +Qed. diff --git a/src/Pyrosome/Lang/Multilanguages/README.md b/src/Pyrosome/Lang/Multilanguages/README.md new file mode 100644 index 00000000..e337a96b --- /dev/null +++ b/src/Pyrosome/Lang/Multilanguages/README.md @@ -0,0 +1,62 @@ +# Multilanguages + +A multi-language system: a typed language (STLC with booleans, products, +polymorphism) and an untyped language (UTLC with booleans) interoperating through +boundary terms, compiled to a single target that implements the boundaries by +type-directed case analysis (`typerec`), plus a partial evaluator that eliminates +`typerec` from compiled programs. + +## Files (in dependency order) + +| File | Contents | +|---|---| +| `ParamFragments.v` | Language fragments parameterized over a type environment (`typed_bool`, `star_type`, `error_t`, `utlc`, `untyped_bool`, `boolhuh`, `utlc_bool`, `mif`, `prod`, `let`) and their `*_ty_subst` languages. | +| `InteropLangs.v` | `simple_interoperating_langs`, `polymorphic_interoperating_langs`, and the identity-style `interoperating_langs_compiler` between them. | +| `Boundaries.v` | The `boundaries` language: `dtt`/`ttd` boundary terms and the 13 equations governing them (value-restricted `dtt func`, the mismatch-to-`Error` rules, substitution rules). | +| `TypeCasing.v` | The `type_casing` language (value-level `typerec` with `star`/`bool`/`func` cases and its substitution rules); `source_multilanguage` and `target_multilanguage_pre`. | +| `TrecTerms.v` | `boundary_cases` (the named case values `bstar`, `bbool`, `bfunc` with their substitution/definition rules), `target_multilanguage`, and the `trec_boundaries` term implementing the boundaries by `typerec`. | +| `SimpleMultilangCompiler.v` | `simple_multilang_compiler` (compiles `dtt`/`ttd` to `trec_boundaries`) and `simple_multilang_compiler_preserving`, assembled from one `eq_term` lemma per boundary equation. | +| `SimpleBoundaries.v` | `Require Export` shim over the six files above. | +| `PolyBoundaries.v` | The parameterized (polymorphic) boundaries, `poly_multilang_compiler`, and `poly_multilang_compiler_preserving`. | +| `TyperecPartialEval.v` | The partial evaluator `elim_typerec` and its metatheory: `can_eliminate_typerec`, `partial_eval_preserves_equality`, `partial_eval_wf_in_target`, `partial_eval_wf_in_no_typerec_lang`, `compiled_partial_eval_wf`. | + +Every theorem in the folder is `Qed` and closed under the global context. + +## Design notes + +- **Boundaries are on expressions; the compiler let-binds.** `dtt G A e` compiles to + `let e (app (.2 (exp_subst wkn TREC)) (ret hd))`, so STLC beta (which needs `ret v`) + fires on the bound value. The target therefore includes `let` with a one-rule + `let_eta` (`let e (ret hd) = e`). +- **`typerec` is value-level.** An expression-level `typerec` applied to a stuck + `typerec A` at a type variable cannot be reduced by STLC beta, and the boundary + equations are then provably unequal. The `func` case is a value open in two type + variables and two term variables, instantiated by substitution. +- **Named case values.** The three cases are the constants `bstar`/`bbool`/`bfunc` + of `boundary_cases`, with `bfunc` taking its type and recursive-result arguments + explicitly. Substitution passes through a `typerec` in one rewrite step instead of + being pushed through the case bodies. +- **Forward-only e-graph saturation.** The per-equation lemmas use + `by_reduction'` with every rule oriented left-to-right; with all rules reversible + the saturation is dominated by backward rewrites and the `func` equations do not + terminate in reasonable time. +- **Two hops for the `func` equations.** The e-graph reducer restarts from the + smallest extracted term whenever the weight drops, so a term-growing first step + (`typerec func`) is discarded. Those lemmas go through an explicit intermediate + term with `eq_term_trans`. +- **Conservativity for the partial evaluator.** `partial_eval_wf_in_no_typerec_lang` + needs sort equalities of the full target to be derivable in the `typerec`-free + sublanguage. `Theory/Conservativity.v` provides this for any extension whose new + rules live above a closed stratum of sort names (here `{ty_env, env, ty, ty_sub}`), + with the side condition decided by `vm_compute`. + +## Building + +Build single files with the absolute target, one Coq process at a time: + +``` +touch .Makefile.coq.d && make -f Makefile.coq /root/pyrosome-ai/src/Pyrosome/Lang/Multilanguages/.vo +``` + +Approximate times: stages A-E about 20 minutes together; `SimpleMultilangCompiler.v` +and `PolyBoundaries.v` about an hour each; `TyperecPartialEval.v` about 5 minutes. diff --git a/src/Pyrosome/Lang/Multilanguages/SimpleBoundaries.v b/src/Pyrosome/Lang/Multilanguages/SimpleBoundaries.v index 7044c64b..3be7fb08 100644 --- a/src/Pyrosome/Lang/Multilanguages/SimpleBoundaries.v +++ b/src/Pyrosome/Lang/Multilanguages/SimpleBoundaries.v @@ -1,999 +1,4 @@ -Set Implicit Arguments. - -Require Import Datatypes.String Lists.List. -Import ListNotations. -Open Scope string. -Open Scope list. -From Utils Require Import Utils. - -(* imports for compilers *) -(* copied from LinearCPS.v *) -From Pyrosome Require Import Compilers.Compilers Elab.ElabCompilers. -Import CompilerDefs.Notations. (* for `match # from high_level_multilanguage with` *) -(* CompilerDefs, for preserving_compiler_ext, is already imported. Prolly through something else. *) - -From Pyrosome Require Import Theory.Core Elab.Elab - Tools.Matches - Tools.EGraph.TypeInference Tools.Resolution Tools.EGraph.ComputeWf. -Import Core.Notations. - -Require Coq.derive.Derive. - -(* import the relevant language fragments *) -From Pyrosome.Lang Require Import SimpleVSTLC. -From Pyrosome.Lang Require Import UTLC. -From Pyrosome.Lang Require Import BoolType. -From Pyrosome.Lang Require Import SimpleVProd. - - -(* imports for polymorphism *) -From Pyrosome.Lang Require Import PolySubst SimpleVSubst. -From Pyrosome.Lang Require Import PolyCompilerLangs PolyCompilersCPS PolyCompilers. (* for parameterizing existing languages*) -From Pyrosome.Compilers Require Import Parameterizer. -Import Pyrosome.Tools.UnElab. - - - -(* Our target multilanguage without boundaries will be polymorphic. So, we need to make polymorphic versions of all the fragments that constitute the two interoperating languages. *) -(* NOTE: the following helpers are abstracted from the definition of stlc_parameterized in PolyCompilers.v *) -Definition parameterize_wrapper (l : lang) : lang := - let ps := (elab_param "D" (l - ++ exp_ret - ++ exp_subst_base - ++ value_subst - ) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps l. -Local Definition evp'_general (l : lang) : lang := - let ps := (elab_param "D" (l ++ exp_ret ++ exp_subst_base - ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps (exp_ret ++ exp_subst_base ++ value_subst). -Ltac solve_parameterize_wrapper l := (* deleted comments in equivalent code from PolyCompilers.v*) - change (exp_parameterized++val_parameterized) with (evp'_general l); - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor - | now prove_by_lang_db.. - | vm_compute; exact I]. - -Definition typed_bool_parameterized := parameterize_wrapper typed_bool. -Lemma typed_bool_parameterized_wf - : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) - typed_bool_parameterized. -Proof. solve_parameterize_wrapper typed_bool. Qed. -#[local] Definition typed_bool_parameterized_entry := - lang_entry typed_bool_parameterized_wf. -#[export] Hint Resolve typed_bool_parameterized_entry : wf_lang_db. - -(* NOTE: stlc_parameterized already exists in PolyCompilers.v *) - -(* the parameterizer does not do the type substitutions, so we have do do those manually as a small fragment. *) -Definition ty_subst_def_maker (parameterized_lang : lang) parameterized_dependencies := eqn_rules - type_subst_mode - (parameterized_dependencies ++ - 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 - ) - (hide_lang_implicits (parameterized_lang ++ parameterized_dependencies ++ - 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 - ) - parameterized_lang). - -Definition typed_bool_ty_subst_def := Eval vm_compute in ty_subst_def_maker typed_bool_parameterized []. -Derive typed_bool_ty_subst - SuchThat (elab_lang_ext (typed_bool_parameterized ++ - 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 - ) - typed_bool_ty_subst_def typed_bool_ty_subst) - As typed_bool_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition typed_bool_ty_subst_entry := - lang_entry (elab_lang_implies_wf typed_bool_ty_subst_wf). -#[export] Hint Resolve typed_bool_ty_subst_entry : wf_lang_db. - -Definition stlc_ty_subst_def := Eval vm_compute in ty_subst_def_maker stlc_parameterized []. -Derive stlc_ty_subst - SuchThat (elab_lang_ext (stlc_parameterized ++ - 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 - ) - stlc_ty_subst_def stlc_ty_subst) - As stlc_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition stlc_ty_subst_entry := - lang_entry (elab_lang_implies_wf stlc_ty_subst_wf). -#[export] Hint Resolve stlc_ty_subst_entry : wf_lang_db. - -Definition star_type_parameterized := parameterize_wrapper star_type. -Lemma star_type_parameterized_wf : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) star_type_parameterized. -Proof. solve_parameterize_wrapper star_type. Qed. -#[local] Definition star_type_parameterized_entry := - lang_entry star_type_parameterized_wf. -#[export] Hint Resolve star_type_parameterized_entry : wf_lang_db. - -Definition error_t_parameterized := parameterize_wrapper error_t. -Lemma error_t_parameterized_wf : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) error_t_parameterized. -Proof. solve_parameterize_wrapper error_t. Qed. -#[local] Definition error_t_parameterized_entry := - lang_entry error_t_parameterized_wf. -#[export] Hint Resolve error_t_parameterized_entry : wf_lang_db. - -Definition star_type_ty_subst_def := Eval vm_compute in ty_subst_def_maker star_type_parameterized []. -Derive star_type_ty_subst - SuchThat (elab_lang_ext (star_type_parameterized ++ - 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 - ) - star_type_ty_subst_def star_type_ty_subst) - As star_type_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition star_type_ty_subst_entry := - lang_entry (elab_lang_implies_wf star_type_ty_subst_wf). -#[export] Hint Resolve star_type_ty_subst_entry : wf_lang_db. - -Definition error_t_ty_subst_def := Eval vm_compute in ty_subst_def_maker error_t_parameterized []. -Derive error_t_ty_subst - SuchThat (elab_lang_ext (error_t_parameterized ++ - 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 - ) - error_t_ty_subst_def error_t_ty_subst) - As error_t_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition error_t_ty_subst_entry := - lang_entry (elab_lang_implies_wf error_t_ty_subst_wf). -#[export] Hint Resolve error_t_ty_subst_entry : wf_lang_db. - - - -(* TODO from this point on, try to generalize the parameterizing function and combine it with what's above *) - -Definition utlc_parameterized := - let ps := (elab_param "D" (utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base - ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps utlc. -(* for some reason need to redo the evp functions for these languages. think it has to do with the dependencies. *) -Local Definition evp'_utlc : lang := - let ps := (elab_param "D" (utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base - ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps (star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). -Lemma utlc_parameterized_wf - : wf_lang_ext ((star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) - utlc_parameterized. -Proof. - replace (star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_utlc. - - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor (*TODO: include in t'*) - | now prove_by_lang_db.. - | vm_compute; exact I]. - - cbv; reflexivity. -Qed. -#[local] Definition utlc_parameterized_entry := - lang_entry utlc_parameterized_wf. -#[export] Hint Resolve utlc_parameterized_entry : wf_lang_db. - -Definition utlc_ty_subst_def := Eval vm_compute in ty_subst_def_maker utlc_parameterized (star_type_parameterized ++ error_t_parameterized). -Derive utlc_ty_subst - SuchThat (elab_lang_ext ( - utlc_parameterized ++ - star_type_ty_subst ++ error_t_ty_subst ++ - star_type_parameterized ++ error_t_parameterized ++ - 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 - ) - utlc_ty_subst_def utlc_ty_subst) - As utlc_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition utlc_ty_subst_entry := - lang_entry (elab_lang_implies_wf utlc_ty_subst_wf). -#[export] Hint Resolve utlc_ty_subst_entry : wf_lang_db. - -Definition untyped_bool_parameterized := - let ps := (elab_param "D" (untyped_bool ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base - ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps untyped_bool. -Local Definition evp'_untyped_bool : lang := - let ps := (elab_param "D" (untyped_bool ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base - ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps (star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). -Lemma untyped_bool_parameterized_wf - : wf_lang_ext ((star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) - untyped_bool_parameterized. -Proof. - replace (star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_untyped_bool. - - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor (*TODO: include in t'*) - | now prove_by_lang_db.. - | vm_compute; exact I]. - - cbv; reflexivity. -Qed. -#[local] Definition untyped_bool_parameterized_entry := - lang_entry untyped_bool_parameterized_wf. -#[export] Hint Resolve untyped_bool_parameterized_entry : wf_lang_db. - -Definition untyped_bool_ty_subst_def := Eval vm_compute in ty_subst_def_maker untyped_bool_parameterized (star_type_parameterized ++ error_t_parameterized). -Derive untyped_bool_ty_subst - SuchThat (elab_lang_ext ( - untyped_bool_parameterized ++ - star_type_ty_subst ++ error_t_ty_subst ++ - star_type_parameterized ++ error_t_parameterized ++ - 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 - ) - untyped_bool_ty_subst_def untyped_bool_ty_subst) - As untyped_bool_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition untyped_bool_ty_subst_entry := - lang_entry (elab_lang_implies_wf untyped_bool_ty_subst_wf). -#[export] Hint Resolve untyped_bool_ty_subst_entry : wf_lang_db. - -Definition boolhuh_parameterized := - let ps := (elab_param "D" (boolhuh ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps boolhuh. -Local Definition evp'_boolhuh : lang := - let ps := (elab_param "D" (boolhuh ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps (untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). -Lemma boolhuh_parameterized_wf - : wf_lang_ext ((untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) - boolhuh_parameterized. -Proof. - replace (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_boolhuh. - - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor (*TODO: include in t'*) - | now prove_by_lang_db.. - | vm_compute; exact I]. - - cbv; reflexivity. -Qed. -#[local] Definition boolhuh_parameterized_entry := - lang_entry boolhuh_parameterized_wf. -#[export] Hint Resolve boolhuh_parameterized_entry : wf_lang_db. - -Definition boolhuh_ty_subst_def := Eval vm_compute in ty_subst_def_maker boolhuh_parameterized (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized). -Derive boolhuh_ty_subst - SuchThat (elab_lang_ext ( (* add all dependencies with their ty_subst versions and the current parameterized lang *) - boolhuh_parameterized ++ - untyped_bool_ty_subst ++ - untyped_bool_parameterized ++ - utlc_ty_subst ++ - utlc_parameterized ++ - star_type_ty_subst ++ error_t_ty_subst ++ - star_type_parameterized ++ error_t_parameterized ++ - 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 - ) - boolhuh_ty_subst_def boolhuh_ty_subst) - As boolhuh_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition boolhuh_ty_subst_entry := - lang_entry (elab_lang_implies_wf boolhuh_ty_subst_wf). -#[export] Hint Resolve boolhuh_ty_subst_entry : wf_lang_db. - -(* NOTE: utlc_bool does not need a ty_subst lang because there is no new syntax in utlc_bool *) -Definition utlc_bool_parameterized := - let ps := (elab_param "D" (utlc_bool ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps utlc_bool. -Local Definition evp'_utlc_bool : lang := - let ps := (elab_param "D" (utlc_bool ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps (untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). -Lemma utlc_bool_parameterized_wf - : wf_lang_ext ((untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) - utlc_bool_parameterized. -Proof. - replace (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_utlc_bool. - - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor (*TODO: include in t'*) - | now prove_by_lang_db.. - | vm_compute; exact I]. - - cbv; reflexivity. -Qed. -#[local] Definition utlc_bool_parameterized_entry := - lang_entry utlc_bool_parameterized_wf. -#[export] Hint Resolve utlc_bool_parameterized_entry : wf_lang_db. - -Definition mif_parameterized := - let ps := (elab_param "D" (mif ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps mif. -Local Definition evp'_mif : lang := - let ps := (elab_param "D" (mif ++ untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst) - [("sub", Some 2); - ("ty", Some 0); - ("env", Some 0); - ("val",Some 2); - ("exp",Some 2)]) in - parameterize_lang "D" {{s #"ty_env"}} - ps (untyped_bool ++ utlc ++ star_type ++ error_t ++ exp_ret ++ exp_subst_base ++ value_subst). -Lemma mif_parameterized_wf - : wf_lang_ext ((untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) ++ ty_env_lang) - mif_parameterized. -Proof. - replace (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized ++ exp_parameterized ++ val_parameterized) with evp'_mif. - - eapply parameterize_lang_preserving_ext; - try typeclasses eauto; - [repeat t'; constructor - | now prove_by_lang_db.. - | vm_compute; exact I]. - - cbv; reflexivity. -Qed. -#[local] Definition mif_parameterized_entry := - lang_entry mif_parameterized_wf. -#[export] Hint Resolve mif_parameterized_entry : wf_lang_db. - -Definition mif_ty_subst_def := Eval vm_compute in ty_subst_def_maker mif_parameterized (untyped_bool_parameterized ++ utlc_parameterized ++ star_type_parameterized ++ error_t_parameterized). -Derive mif_ty_subst - SuchThat (elab_lang_ext ( (* add all dependencies with their ty_subst versions and the current parameterized lang *) - mif_parameterized ++ - untyped_bool_ty_subst ++ - untyped_bool_parameterized ++ - utlc_ty_subst ++ - utlc_parameterized ++ - star_type_ty_subst ++ error_t_ty_subst ++ - star_type_parameterized ++ error_t_parameterized ++ - 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 - ) - mif_ty_subst_def mif_ty_subst) - As mif_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition mif_ty_subst_entry := - lang_entry (elab_lang_implies_wf mif_ty_subst_wf). -#[export] Hint Resolve mif_ty_subst_entry : wf_lang_db. - -(* NOTE: this makes the compiler take forever. why? name stuff? unfolding everything doesn't make it work -Definition simple_typed_fragment := typed_bool ++ stlc. -Hint Unfold simple_typed_fragment : auto_elab. - -Definition simple_untyped_fragment := mif ++ utlc_bool ++ boolhuh ++ untyped_bool ++ utlc ++ error_t ++ star_type. -Hint Unfold simple_untyped_fragment : auto_elab. - -Definition simple_interoperating_langs := - simple_untyped_fragment ++ - simple_typed_fragment ++ - exp_subst ++ value_subst. -Hint Unfold simple_interoperating_langs : auto_elab. - -Definition polymorphic_typed_fragment := - typed_bool_ty_subst ++ typed_bool_parameterized ++ - stlc_ty_subst ++ stlc_parameterized. -Hint Unfold polymorphic_typed_fragment : auto_elab. - -Definition polymorphic_untyped_fragment := - boolhuh_ty_subst ++ boolhuh_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. -Hint Unfold polymorphic_untyped_fragment : auto_elab. - -Definition polymorphic_interoperating_langs := - polymorphic_typed_fragment ++ - polymorphic_untyped_fragment ++ - 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. -Hint Unfold polymorphic_interoperating_langs : auto_elab. -*) - - -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 ++ - (* all polymorphic base stuff. Don't need poly because we don't have type lambdas or type application. but we might as well add it now bc we'll extend this list with polymorphic stuff for the 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. - - -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 - SuchThat (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. - - - -(* Now the multilanguages *) - -(* First, we define the boundaries fragment. To me, it seems like this is the natural embedding. TODO: see if you can, as Dustin said, simulate the lump embedding. *) -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", - "v" : #"val" "G" #"*" - ----------------------------------------------- ("dtt func") - #"dtt" (#"->" "A" "B") (#"ret" "v") = - #"ret" (#"lambda" "A" (#"dtt" "B" (#"uapp" (#"ret" (#"val_subst" #"wkn" "v")) (#"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 - SuchThat (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. - -(* now we define the type casing fragment for the target multilanguage without boundaries. First, some helpers. *) -Fixpoint ty_wkn_n n := - match n with - | 0 => {{e #"ty_id"}} - | 1 => {{e #"ty_wkn"}} - | S n' => {{e #"ty_cmp" #"ty_wkn" {ty_wkn_n n'} }} - end. - -Definition ty_ovar n := - match n with - | 0 => {{e #"ty_hd"}} (* bc ty_subst ty_id ty_hd is just ty_hd *) - | S _ => {{e #"ty_subst" {ty_wkn_n n} #"ty_hd" }} - end. - -(* This is for the semantic rule for arrow. It's the type of (#"app" (#"@" "e3" "t1") (#"typerec" "t1" "sigma" "e1" "e2" "e3")). This type has a type variable, and we are going to substitute it with t2. The derivation for this is on page 32 of your UROP notebook *) -Definition A_var := {{e #"ty_subst" (#"ty_snoc" (#"ty_cmp" #"ty_wkn" (#"ty_snoc" #"ty_id" "t1")) #"ty_hd") (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma")) }}. - -(* One thing to immediately note is that the type signature on e3 is modified from the type signature in Harper and Morrisett. It is equivalent, since it is just the change of some arrows and quantifiers that don't change bindings. This is helpful in pyrosome because it makes the first appearance of sigma in the signature substitution-less, because now that sigma is only under one All and we substitute it with only one variable (there are no other variables in sigma and if there are any others in the environment we want to conserve them), so we can actually leave sigma as is -- that first variable in sigma get bound by the All, as desired. If you write the substitution for the second type out on paper, it looks like [0/0]. Why can't we do the same trick there? That's because pyrosome does entire-environment substitutions. Since we have two extra variables, we must also include those in the substitution. The reason this is not the identity is the same reason the first sigma would not have been the identity had we not done this trick: even though we substitute the first variable in sigma with the first additional All variable, we have another variable in the environment now (the second All in the case of the unmodified version of the rule in Harper and Morrisett) and so we must account for it (it would have had a {ty_wkn_n 1} there). *) -Definition type_casing_def : lang := - {[l - [:| "D" : #"ty_env", - "G" : #"env" "D", - "mu" : #"ty" "D", (* is mu *) - "sigma" : #"ty" (#"ty_ext" "D"), (* this is sigma. it has a variable (hence the ext *) - "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma"), (* substitute identity type for all except the last (which is A), which we change to star *) - "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma"), - "e3" : #"exp" "D" "G" (#"All" (#"->" "sigma" (#"All" (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma"))))) (* look at arrow case in 134 *) - ----------------------------------------------- - #"typerec" "mu" "sigma" "e1" "e2" "e3" - : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" "mu") "sigma") (* verbose way of writing the [u/t]sigma in the rule on 134, verbose in that its the _full_ substitution *) - ]; - [:= "D" : #"ty_env", - "G" : #"env" "D", - "sigma" : #"ty" (#"ty_ext" "D"), - "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma"), - "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma"), - "e3" : #"exp" "D" "G" (#"All" (#"->" "sigma" (#"All" (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma"))))) - ----------------------------------------------- ("typerec star") - #"typerec" #"*" "sigma" "e1" "e2" "e3" - = "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma") - ]; - [:= "D" : #"ty_env", - "G" : #"env" "D", - "sigma" : #"ty" (#"ty_ext" "D"), - "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma"), - "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma"), - "e3" : #"exp" "D" "G" (#"All" (#"->" "sigma" (#"All" (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma"))))) - ----------------------------------------------- ("typerec bool") - #"typerec" #"bool" "sigma" "e1" "e2" "e3" - = "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma") - ]; - [:= "D" : #"ty_env", - "G" : #"env" "D", - "sigma" : #"ty" (#"ty_ext" "D"), - "t1" : #"ty" "D", - "t2" : #"ty" "D", - "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma"), - "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma"), - "e3" : #"exp" "D" "G" (#"All" (#"->" "sigma" (#"All" (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma"))))) - ----------------------------------------------- ("typerec func") (* trec-fn on page 135 *) - #"typerec" (#"->" "t1" "t2") "sigma" "e1" "e2" "e3" - = #"app" (@"@" @("A" := {A_var}) (#"app" (#"@" "e3" "t1") (#"typerec" "t1" "sigma" "e1" "e2" "e3")) "t2") (#"typerec" "t2" "sigma" "e1" "e2" "e3") - : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" (#"->" "t1" "t2")) "sigma") - ]; - [:= "D" : #"ty_env", - "G" : #"env" "D", - "G'" : #"env" "D", - "g" : #"sub" "D" "G'" "G", - "mu" : #"ty" "D", - "sigma" : #"ty" (#"ty_ext" "D"), - "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma"), - "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma"), - "e3" : #"exp" "D" "G" (#"All" (#"->" "sigma" (#"All" (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma"))))) - ----------------------------------------------- ("exp_subst typerec") - #"exp_subst" "g" (#"typerec" "mu" "sigma" "e1" "e2" "e3") - = #"typerec" "mu" "sigma" (#"exp_subst" "g" "e1") (#"exp_subst" "g" "e2") (#"exp_subst" "g" "e3") - : #"exp" "D" "G'" (#"ty_subst" (#"ty_snoc" #"ty_id" "mu") "sigma") - ]; - [:= "D" : #"ty_env", - "D'" : #"ty_env", - "G" : #"env" "D", - "g" : #"ty_sub" "D'" "D", - "mu" : #"ty" "D", - "sigma" : #"ty" (#"ty_ext" "D"), - "e1" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"*") "sigma"), - "e2" : #"exp" "D" "G" (#"ty_subst" (#"ty_snoc" #"ty_id" #"bool") "sigma"), - "e3" : #"exp" "D" "G" (#"All" (#"->" "sigma" (#"All" (#"->" (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {ty_ovar 0}) "sigma") (#"ty_subst" (#"ty_snoc" {ty_wkn_n 2} (#"->" {ty_ovar 1} {ty_ovar 0})) "sigma"))))) - ----------------------------------------------- ("ty_subst typerec") - #"exp_ty_subst" "g" (#"typerec" "mu" "sigma" "e1" "e2" "e3") - = #"typerec" (#"ty_subst" "g" "mu") (#"ty_subst" (#"ty_snoc" (#"ty_cmp" #"ty_wkn" "g") #"ty_hd") "sigma") (#"exp_ty_subst" "g" "e1") (#"exp_ty_subst" "g" "e2") (#"exp_ty_subst" "g" "e3") - : #"exp" "D'" (#"env_ty_subst" "g" "G") (#"ty_subst" "g" (#"ty_subst" (#"ty_snoc" #"ty_id" "mu") "sigma")) - ] - ]}. -Derive type_casing - SuchThat (elab_lang_ext ( - stlc_ty_subst ++ - typed_bool_ty_subst ++ - star_type_ty_subst ++ error_t_ty_subst ++ - typed_bool_parameterized ++ - stlc_parameterized ++ - star_type_parameterized ++ error_t_parameterized ++ - poly ++ (* needed for #"All" *) - (* base polymorphic stuff *) - 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 - ) - type_casing_def type_casing) - As type_casing_wf. -Proof. auto_elab. Qed. -#[local] Definition type_casing_entry := - lang_entry (elab_lang_implies_wf type_casing_wf). -#[export] Hint Resolve type_casing_entry : wf_lang_db. - -Definition source_multilanguage := - boundaries ++ simple_interoperating_langs. -Hint Unfold source_multilanguage : auto_elab. - -Definition prod_parameterized := parameterize_wrapper prod. -Lemma prod_parameterized_wf - : wf_lang_ext ((exp_parameterized ++ val_parameterized) ++ ty_env_lang) - prod_parameterized. -Proof. solve_parameterize_wrapper prod. Qed. -#[local] Definition prod_parameterized_entry := - lang_entry prod_parameterized_wf. -#[export] Hint Resolve prod_parameterized_entry : wf_lang_db. -Definition prod_ty_subst_def := Eval vm_compute in ty_subst_def_maker prod_parameterized []. -Derive prod_ty_subst - SuchThat (elab_lang_ext (prod_parameterized ++ - 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 - ) - prod_ty_subst_def prod_ty_subst) - As prod_ty_subst_wf. -Proof. auto_elab. Qed. -#[local] Definition prod_ty_subst_entry := - lang_entry (elab_lang_implies_wf prod_ty_subst_wf). -#[export] Hint Resolve prod_ty_subst_entry : wf_lang_db. - -Definition target_multilanguage := - prod_ty_subst ++ prod_parameterized ++ - type_casing ++ - polymorphic_interoperating_langs. -Hint Unfold target_multilanguage : auto_elab. - - - -(* deriving the terms used in the compiler *) -Fixpoint wkn_n n := - match n with - | 0 => {{e #"id"}} - | 1 => {{e #"wkn"}} - | S n' => - {{e #"cmp" #"wkn" {wkn_n n'} }} - end. - -Definition ovar n := {{e #"val_subst" {wkn_n n} #"hd" }}. - -(* (* it seems this is still needed *) *) -(* (* replaced by assert (wf_lang target_multilanguage) by prove_by_lang_db. *) *) -(* (* gonna comment this out to see if it's still needed *) *) -(* Lemma target_multilanguage_wf : wf_lang target_multilanguage. *) -(* Proof. prove_by_lang_db. Qed. *) -(* #[local] Definition target_multilanguage_entry := *) -(* lang_entry target_multilanguage_wf. *) -(* #[export] Hint Resolve target_multilanguage_entry : wf_lang_db. *) - -Ltac derive_elab_term := (* no longer used *) - assert (wf_lang target_multilanguage) by prove_by_lang_db; - unshelve (repeat t); t'. (* repeat t then unshelve; then on the unshelved do t'. *) - -Ltac solve_eq_sort_disj := (* no longer used *) - right; compute_eq_compilation; sort_cong; repeat by_reduction. - -Ltac solve_elab_term_or_sort language := - assert (wf_lang language) by prove_by_lang_db; - (* NOTE: the by_reduction below seems to me redundant given the def of solve_eq_sort_disj, but it's necessary for trec_boundaries and for both elab_term goals in the compiler *) - (* the elab_term goals in the compiler were goals that I had to do out of order. Wonder if that has to do with it? *) - (* and now that I think about it, the way I was doing the elab_term goals in trec_boundaries was doing the last one first. Then the rest went through. So it does seem like an order thing... but this solves it? *) - unshelve (repeat t; decompose_sort_eq; repeat by_reduction; by_reduction); compute_term_wf. - -(* tactic to see if progress can be made on an elab_term goal. unused, but keeping because it's a good example of pyrosome workflow. *) -Ltac quick_goal_match := - lazymatch goal with - | |- elab_term _ _ (con ?s _) (con ?s _) _ => - idtac "can go further" - | |- elab_term _ _ (con ?s _) (con ?s' _) _ => - fail "cannot go further" - | |- _ => idtac "neither case" - end. - -Definition trec_star_case_unelab := - {{e #"pair" - (#"ret" (#"lambda" #"*" (#"ret" #"hd"))) - (#"ret" (#"lambda" #"*" (#"ret" #"hd"))) }}. -Derive trec_star_case - in ( elab_term target_multilanguage - [("G", {{s #"env" #"ty_emp"}})] - trec_star_case_unelab - trec_star_case - {{s #"exp" #"ty_emp" "G" - (#"prod" #"ty_emp" - (#"->" #"ty_emp" (#"*" #"ty_emp") (#"*" #"ty_emp")) - (#"->" #"ty_emp" (#"*" #"ty_emp") (#"*" #"ty_emp")) - ) - }} - ) as trec_star_case_wf. -Proof. solve_elab_term_or_sort target_multilanguage. Qed. (* used to be derive_elab_term *) - -Definition trec_bool_case_unelab := - {{e #"pair" - (#"ret" (#"lambda" #"bool" (#"if" (#"ret" #"hd") (#"ret" #"uT") (#"ret" #"uF")))) - (#"ret" (#"lambda" #"*" (#"mif" (#"ret" #"hd") (#"ret" #"T") (#"ret" #"F")))) }}. -Derive trec_bool_case - in ( elab_term target_multilanguage - [("G", {{s #"env" #"ty_emp"}})] - trec_bool_case_unelab - trec_bool_case - {{s #"exp" #"ty_emp" "G" - (#"prod" #"ty_emp" - (#"->" #"ty_emp" (#"bool" #"ty_emp") (#"*" #"ty_emp")) - (#"->" #"ty_emp" (#"*" #"ty_emp") (#"bool" #"ty_emp")) - ) - }} - ) as trec_bool_case_wf. -Proof. solve_elab_term_or_sort target_multilanguage. Qed. (* used to be derive_elab_term *) - -Derive trec_func_case_sort - in (elab_sort target_multilanguage - [("G", {{s #"env" #"ty_emp"}})] - {{s #"exp" #"ty_emp" "G" - (#"All" - (#"->" (#"prod" (#"->" {ty_ovar 0} #"*") (#"->" #"*" {ty_ovar 0})) - (#"All" - (#"->" (#"prod" (#"->" {ty_ovar 0} #"*") (#"->" #"*" {ty_ovar 0})) - (#"prod" (#"->" (#"->" {ty_ovar 1} {ty_ovar 0}) #"*") (#"->" #"*" (#"->" {ty_ovar 1} {ty_ovar 0}))))))) }} - trec_func_case_sort - ) - as trec_func_case_sort_wf. -Proof. solve_elab_term_or_sort target_multilanguage. Qed. (* used to be derive_elab_term *) - -Definition trec_func_case_unelab := - {{e #"ret" (#"Lam" (#"ret" (#"lambda" (#"prod" (#"->" {ty_ovar 0} #"*") (#"->" #"*" {ty_ovar 0})) (#"ret" (#"Lam" (#"ret" (#"lambda" (#"prod" (#"->" {ty_ovar 0} #"*") (#"->" #"*" {ty_ovar 0})) (#"pair" (#"ret" (#"lambda" (#"->" {ty_ovar 1} {ty_ovar 0}) (#"ret" (#"ulambda" (#"app" (#".1" (#"ret" {ovar 2})) (#"app" (#"ret" {ovar 1}) (#"app" (#".2" (#"ret" {ovar 3})) (#"ret" {ovar 0})))))))) (#"ret" (#"lambda" #"*" (#"ret" (#"lambda" {ty_ovar 1} (#"app" (#".2" (#"ret" {ovar 2})) (#"uapp" (#"ret" {ovar 1}) (#"app" (#".1" (#"ret" {ovar 3})) (#"ret" {ovar 0})))) ) ))))))))))) }}. -Derive trec_func_case - in ( elab_term target_multilanguage - [("G", {{s #"env" #"ty_emp"}})] - trec_func_case_unelab - trec_func_case - trec_func_case_sort - ) as trec_func_case_wf. -Proof. solve_elab_term_or_sort target_multilanguage. Qed. - -Definition trec_boundaries_unelab := - {{e #"typerec" "A" (#"prod" (#"->" {ty_ovar 0} #"*") (#"->" #"*" {ty_ovar 0})) - {trec_star_case_unelab} - {trec_bool_case_unelab} - {trec_func_case_unelab} }}. -Derive trec_boundaries - in ( elab_term target_multilanguage - [("A", {{s #"ty" #"ty_emp"}}); ("G", {{s #"env" #"ty_emp"}})] - trec_boundaries_unelab - trec_boundaries - {{s #"exp" #"ty_emp" "G" - (#"prod" #"ty_emp" - (#"->" #"ty_emp" "A" (#"*" #"ty_emp")) - (#"->" #"ty_emp" (#"*" #"ty_emp") "A")) }} - ) as trec_boundaries_wf. -Proof. solve_elab_term_or_sort target_multilanguage. Qed. - - - -(* simple to poly compiler *) -Definition simple_multilang_compiler_def : compiler := - match # from boundaries with - | {{e #"dtt" "G" "A" "e"}} => {{e @"app" @("D" := #"ty_emp") - (#".2" {trec_boundaries_unelab}) "e" }} - | {{e #"ttd" "G" "A" "e"}} => {{e @"app" @("D" := #"ty_emp") - (#".1" {trec_boundaries_unelab}) "e" }} - end. - -Ltac solve_multilang_compiler := - unshelve (setup_elab_compiler; - match goal with - | |- elab_term _ _ _ _ _ => solve_elab_term_or_sort target_multilanguage - | |- _ => shelve - end); - unshelve (apply TODO (*TODO: the bug fix may have caused this to no longer terminate Automation.by_reduction*)); - match goal with - | |- wf_term _ _ _ _ => compute_term_wf - | |- _ => solve_wf_ctx - end. - -Derive simple_multilang_compiler - SuchThat (elab_preserving_compiler - interoperating_langs_compiler - target_multilanguage - simple_multilang_compiler_def - simple_multilang_compiler - boundaries) - As simple_multilang_compiler_preserving. -Proof. solve_multilang_compiler. Qed. -#[local] Definition simple_multilang_compiler_entry := - cmp_entry (elab_compiler_implies_preserving simple_multilang_compiler_preserving). -#[export] Hint Resolve simple_multilang_compiler_entry : preserving_db. - -(* -Require Import Pyrosome.Tools.EGraph.TypeInference. -(* you _could_ do it with egraphs if you mark which things are injective for the target lang (see STLC), and then do it with egraphs. (that's what this def is for) *) -Definition multilang_compiler' := - Eval vm_compute in - (infer_compiler_simple - target_multilanguage - shared_fragment_compiler - multilang_compiler_def - (boundaries ++ uif) -\ []). -(* above will have succeeded if we don't see @ or ?. If that succeeds, then we can throw out the old tactics and only use the computational tactics *) -(* Print multilang_compiler'. *) - *) - - - +(* Compatibility shim: the development formerly in this file is split across + the stage files re-exported below; see README.md for the layout. *) +From Pyrosome.Lang.Multilanguages Require Export + ParamFragments InteropLangs Boundaries TypeCasing TrecTerms SimpleMultilangCompiler. diff --git a/src/Pyrosome/Lang/Multilanguages/SimpleMultilangCompiler.v b/src/Pyrosome/Lang/Multilanguages/SimpleMultilangCompiler.v new file mode 100644 index 00000000..f8b4a93d --- /dev/null +++ b/src/Pyrosome/Lang/Multilanguages/SimpleMultilangCompiler.v @@ -0,0 +1,377 @@ +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. + +(* imports for compilers *) +From Pyrosome Require Import Compilers.Compilers Elab.ElabCompilers. +Import CompilerDefs.Notations. + +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. + +(* import the relevant language fragments *) +From Pyrosome.Lang Require Import SimpleVSTLC. +From Pyrosome.Lang Require Import UTLC. +From Pyrosome.Lang Require Import BoolType. +From Pyrosome.Lang Require Import SimpleVProd. + +(* imports for polymorphism *) +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 TrecTerms. + +Local Notation compiler := + (@CompilerDefs.compiler string (Term.term string) (Term.sort string)). + +(* ------------------------------------------------------------------ *) +(* The compiler, as originally written (unelaborated). Kept for + documentation: the two target terms below are its elaboration. *) +Definition simple_multilang_compiler_def : compiler := + match # from boundaries with + | {{e #"dtt" "G" "A" "e"}} => + {{e #"let" "e" (#"app" (#".2" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }} + | {{e #"ttd" "G" "A" "e"}} => + {{e #"let" "e" (#"app" (#".1" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }} + end. + +(* ------------------------------------------------------------------ *) +(* The elaborated compiler. + + The two cases are elaborated individually, on top of [trec_boundaries], + the already-elaborated typerec term from TrecTerms.v; the computational + route [infer_compiler_simple_autoinj 4 target_multilanguage ...] does not + apply to this compiler. + + The compiled body binds the source argument ["e"] with [#"let"] and + applies the boundary function to [#"ret" #"hd"]. A variable is a value, + so [STLC-beta] fires, which is what makes the ["dtt star"]/["ttd star"] + equations provable (via the ["let eta"] rule). *) + +Definition dtt_case_unelab := + {{e #"let" "e" (#"app" (#".2" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }}. + +Derive dtt_case_tgt + in ( elab_term target_multilanguage + [("e", {{s #"exp" #"ty_emp" "G" (#"*" #"ty_emp")}}); + ("A", {{s #"ty" #"ty_emp"}}); + ("G", {{s #"env" #"ty_emp"}})] + dtt_case_unelab + dtt_case_tgt + {{s #"exp" #"ty_emp" "G" "A"}} + ) as dtt_case_tgt_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +Definition ttd_case_unelab := + {{e #"let" "e" (#"app" (#".1" (#"ret" (#"val_subst" #"wkn" {trec_boundaries_unelab}))) + (#"ret" #"hd")) }}. + +Derive ttd_case_tgt + in ( elab_term target_multilanguage + [("e", {{s #"exp" #"ty_emp" "G" "A"}}); + ("A", {{s #"ty" #"ty_emp"}}); + ("G", {{s #"env" #"ty_emp"}})] + ttd_case_unelab + ttd_case_tgt + {{s #"exp" #"ty_emp" "G" (#"*" #"ty_emp")}} + ) as ttd_case_tgt_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +(* The entries must be in the SAME ORDER as the term rules of [boundaries], + whose name list is [... ; "dtt"; "exp_subst ttd"; "ttd"], i.e. ["dtt"] + comes first. With the opposite order [preserving_compiler_ext] cannot be + assembled at all (the [term] constructor tries to unify ["dtt"] with + ["ttd"]). Compilation itself is by name lookup, so the order does not + change any compiled term. *) +Definition simple_multilang_compiler : compiler := + [("dtt", term_case ["e"; "A"; "G"] dtt_case_tgt); + ("ttd", term_case ["e"; "A"; "G"] ttd_case_tgt)]. + +(* ------------------------------------------------------------------ *) +(* The two term-constructor obligations of [preserving_compiler_ext]. *) + +Lemma dtt_case_wf + : wf_term target_multilanguage + [("e", {{s #"exp" #"ty_emp" "G" (#"*" #"ty_emp")}}); + ("A", {{s #"ty" #"ty_emp"}}); + ("G", {{s #"env" #"ty_emp"}})] + dtt_case_tgt {{s #"exp" #"ty_emp" "G" "A"}}. +Proof. pose proof target_multilanguage_wf. compute_term_wf. Qed. + +Lemma ttd_case_wf + : wf_term target_multilanguage + [("e", {{s #"exp" #"ty_emp" "G" "A"}}); + ("A", {{s #"ty" #"ty_emp"}}); + ("G", {{s #"env" #"ty_emp"}})] + ttd_case_tgt {{s #"exp" #"ty_emp" "G" (#"*" #"ty_emp")}}. +Proof. pose proof target_multilanguage_wf. compute_term_wf. Qed. + +(* ------------------------------------------------------------------ *) +(* One [eq_term] lemma per boundary equation, each discharged by the e-graph + reducer. + + [norev] makes every rule of the target language usable LEFT-TO-RIGHT only. + Forward-only saturation is essential here: with rules also applied + backwards the search is dominated by backward rewrites, and the + ["exp_subst"] and ["typerec func"] equations do not converge within any + practical budget. It is also what closes the two mismatch equations at + [#"->"], where the eager [#"bool?"] check must reduce to [#"Error"]. + + [by_reduction_fwd] is [Automation.by_reduction'] under that filter, with + the well-formedness side conditions discharged: the context by + [solve_wf_ctx] and the two [wf_term] goals by [compute_term_wf], whose + first goal is [assumption] on [wf_lang target_multilanguage] -- hence the + [pose proof]. It is exported for reuse by PolyBoundaries.v. *) + +Definition norev : string * Rule.rule string -> bool := fun _ => false. + +Ltac by_reduction_fwd := + pose proof target_multilanguage_wf; + Automation.by_reduction' norev Automation.empty_inj_rules; + [ solve_wf_ctx | compute_term_wf | compute_term_wf ]. + +(* ------------------------------------------------------------------ *) +(* The three [#"typerec"] cases are the value constants [#"bstar"] / + [#"bbool"] / [#"bfunc"] of [boundary_cases], whose substitution rules are + one-step rewrites; that is what lets the two ["exp_subst"] equations go + through without per-case helper lemmas. *) + +Definition CMP := simple_multilang_compiler ++ interoperating_langs_compiler. + +Definition brule (n:string) := named_list_lookup (Rule.sort_rule [] []) boundaries n. +Definition gctx n := match brule n with Rule.term_eq_rule c _ _ _ => compile_ctx CMP c | _ => [] end. +Definition gsrt n := match brule n with Rule.term_eq_rule _ _ _ t => compile_sort CMP t | _ => default end. +Definition glhs n := match brule n with Rule.term_eq_rule _ e _ _ => compile CMP e | _ => default end. +Definition grhs n := match brule n with Rule.term_eq_rule _ _ e _ => compile CMP e | _ => default end. + +Definition c_dtt_star := Eval vm_compute in gctx "dtt star". +Definition s_dtt_star := Eval vm_compute in gsrt "dtt star". +Definition l_dtt_star := Eval vm_compute in glhs "dtt star". +Definition r_dtt_star := Eval vm_compute in grhs "dtt star". +(* Provable because the compiler let-binds "e": the beta-redex has a value + (the variable [#"hd"]) as its argument, and ["let eta"] collapses the + residual [#"let" "e" (#"ret" #"hd")] back to ["e"]. *) +Lemma eq_dtt_star : eq_term target_multilanguage c_dtt_star s_dtt_star l_dtt_star r_dtt_star. +Proof. unfold c_dtt_star, s_dtt_star, l_dtt_star, r_dtt_star. by_reduction_fwd. Qed. + +Definition c_ttd_star := Eval vm_compute in gctx "ttd star". +Definition s_ttd_star := Eval vm_compute in gsrt "ttd star". +Definition l_ttd_star := Eval vm_compute in glhs "ttd star". +Definition r_ttd_star := Eval vm_compute in grhs "ttd star". +(* As "dtt star", via the other projection. *) +Lemma eq_ttd_star : eq_term target_multilanguage c_ttd_star s_ttd_star l_ttd_star r_ttd_star. +Proof. unfold c_ttd_star, s_ttd_star, l_ttd_star, r_ttd_star. by_reduction_fwd. Qed. + +Definition c_dtt_True := Eval vm_compute in gctx "dtt True". +Definition s_dtt_True := Eval vm_compute in gsrt "dtt True". +Definition l_dtt_True := Eval vm_compute in glhs "dtt True". +Definition r_dtt_True := Eval vm_compute in grhs "dtt True". +Lemma eq_dtt_True : eq_term target_multilanguage c_dtt_True s_dtt_True l_dtt_True r_dtt_True. +Proof. unfold c_dtt_True, s_dtt_True, l_dtt_True, r_dtt_True. by_reduction_fwd. Qed. + +Definition c_dtt_False := Eval vm_compute in gctx "dtt False". +Definition s_dtt_False := Eval vm_compute in gsrt "dtt False". +Definition l_dtt_False := Eval vm_compute in glhs "dtt False". +Definition r_dtt_False := Eval vm_compute in grhs "dtt False". +Lemma eq_dtt_False : eq_term target_multilanguage c_dtt_False s_dtt_False l_dtt_False r_dtt_False. +Proof. unfold c_dtt_False, s_dtt_False, l_dtt_False, r_dtt_False. by_reduction_fwd. Qed. + +Definition c_ttd_True := Eval vm_compute in gctx "ttd True". +Definition s_ttd_True := Eval vm_compute in gsrt "ttd True". +Definition l_ttd_True := Eval vm_compute in glhs "ttd True". +Definition r_ttd_True := Eval vm_compute in grhs "ttd True". +Lemma eq_ttd_True : eq_term target_multilanguage c_ttd_True s_ttd_True l_ttd_True r_ttd_True. +Proof. unfold c_ttd_True, s_ttd_True, l_ttd_True, r_ttd_True. by_reduction_fwd. Qed. + +Definition c_ttd_False := Eval vm_compute in gctx "ttd False". +Definition s_ttd_False := Eval vm_compute in gsrt "ttd False". +Definition l_ttd_False := Eval vm_compute in glhs "ttd False". +Definition r_ttd_False := Eval vm_compute in grhs "ttd False". +Lemma eq_ttd_False : eq_term target_multilanguage c_ttd_False s_ttd_False l_ttd_False r_ttd_False. +Proof. unfold c_ttd_False, s_ttd_False, l_ttd_False, r_ttd_False. by_reduction_fwd. Qed. + +Definition c_dtt_func := Eval vm_compute in gctx "dtt func". +Definition s_dtt_func := Eval vm_compute in gsrt "dtt func". +Definition l_dtt_func := Eval vm_compute in glhs "dtt func". +Definition r_dtt_func := Eval vm_compute in grhs "dtt func". +(* Proved below, after the hop lemmas. *) + +Definition c_ttd_func := Eval vm_compute in gctx "ttd func". +Definition s_ttd_func := Eval vm_compute in gsrt "ttd func". +Definition l_ttd_func := Eval vm_compute in glhs "ttd func". +Definition r_ttd_func := Eval vm_compute in grhs "ttd func". +(* Proved below, after the hop lemmas. *) + +(* ------------------------------------------------------------------ *) +(* The two ["func"] equations, each proved in TWO HOPS through an explicit + intermediate term. + + The two compiled sides are not mismatched; what the e-graph cannot do in + one go is the ["typerec func"] rewrite, which strictly GROWS the term. + [egraph_reducing_equal] restarts saturation from the extracted (smallest) + representative as soon as a weight decrease is observed, so a + term-growing first step is discarded: the [#"typerec"] node is re-created + un-unfolded at every restart and the remaining work (["bfunc def"], + STLC-beta, ["bool?-func"], ["mif false"], the substitution laws) never + runs in the same round. Supplying the once-unfolded term as an explicit + intermediate splits the equation into two hops that each converge. + + [I1] / [J1] are the compiled left-hand sides with + [#"typerec" (#"->" "A" "B") ...] replaced by its ["typerec func"] reduct + [#"bfunc" "A" "B" TREC["A"] TREC["B"]]. *) + +Definition TRECv X := {{e #"typerec" {X} {boundary_sigma} #"bstar" #"bbool" + (#"bfunc" {tva} {tvb} {ovar 1} {ovar 0}) }}. + +Definition I1_unelab := + {{e #"let" (#"ret" (#"ulambda" "e")) + (#"app" (#".2" (#"ret" (#"val_subst" #"wkn" + (#"bfunc" "A" "B" {TRECv {{e "A"}} } {TRECv {{e "B"}} })))) + (#"ret" #"hd")) }}. + +Derive I1 in (elab_term target_multilanguage c_dtt_func I1_unelab I1 s_dtt_func) + as I1_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +Definition J1_unelab := + {{e #"let" (#"ret" "v") + (#"app" (#".1" (#"ret" (#"val_subst" #"wkn" + (#"bfunc" "A" "B" {TRECv {{e "A"}} } {TRECv {{e "B"}} })))) + (#"ret" #"hd")) }}. + +Derive J1 in (elab_term target_multilanguage c_ttd_func J1_unelab J1 s_ttd_func) + as J1_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. + +(* hop 1: ["typerec func"] only. *) +Lemma eq_dtt_func_hop1 + : eq_term target_multilanguage c_dtt_func s_dtt_func l_dtt_func I1. +Proof. unfold l_dtt_func, c_dtt_func, s_dtt_func. by_reduction_fwd. Qed. + +(* hop 2: ["bfunc def"], STLC-beta, ["bool?-func"], ["mif false"], substitution. *) +Lemma eq_dtt_func_hop2 + : eq_term target_multilanguage c_dtt_func s_dtt_func I1 r_dtt_func. +Proof. unfold r_dtt_func, c_dtt_func, s_dtt_func. by_reduction_fwd. Qed. + +Lemma eq_ttd_func_hop1 + : eq_term target_multilanguage c_ttd_func s_ttd_func l_ttd_func J1. +Proof. unfold l_ttd_func, c_ttd_func, s_ttd_func. by_reduction_fwd. Qed. + +Lemma eq_ttd_func_hop2 + : eq_term target_multilanguage c_ttd_func s_ttd_func J1 r_ttd_func. +Proof. unfold r_ttd_func, c_ttd_func, s_ttd_func. by_reduction_fwd. Qed. + +Lemma eq_dtt_func : eq_term target_multilanguage c_dtt_func s_dtt_func l_dtt_func r_dtt_func. +Proof. eapply eq_term_trans; [apply eq_dtt_func_hop1 | apply eq_dtt_func_hop2]. Qed. + +Lemma eq_ttd_func : eq_term target_multilanguage c_ttd_func s_ttd_func l_ttd_func r_ttd_func. +Proof. eapply eq_term_trans; [apply eq_ttd_func_hop1 | apply eq_ttd_func_hop2]. Qed. + +Definition c_dtt_ulambda_mismatch := Eval vm_compute in gctx "dtt ulambda mismatch". +Definition s_dtt_ulambda_mismatch := Eval vm_compute in gsrt "dtt ulambda mismatch". +Definition l_dtt_ulambda_mismatch := Eval vm_compute in glhs "dtt ulambda mismatch". +Definition r_dtt_ulambda_mismatch := Eval vm_compute in grhs "dtt ulambda mismatch". +Lemma eq_dtt_ulambda_mismatch : eq_term target_multilanguage c_dtt_ulambda_mismatch s_dtt_ulambda_mismatch l_dtt_ulambda_mismatch r_dtt_ulambda_mismatch. +Proof. unfold c_dtt_ulambda_mismatch, s_dtt_ulambda_mismatch, l_dtt_ulambda_mismatch, r_dtt_ulambda_mismatch. by_reduction_fwd. Qed. + +Definition c_dtt_uT_mismatch := Eval vm_compute in gctx "dtt uT mismatch". +Definition s_dtt_uT_mismatch := Eval vm_compute in gsrt "dtt uT mismatch". +Definition l_dtt_uT_mismatch := Eval vm_compute in glhs "dtt uT mismatch". +Definition r_dtt_uT_mismatch := Eval vm_compute in grhs "dtt uT mismatch". +(* Closed by the explicit-argument [#"bfunc"] plus the forward-only filter: + ["typerec func"] instantiates [#"bfunc"] in one rewrite + (["ty_subst bfunc"] + ["val_subst bfunc"]), so ["bfunc def"] unfolds an + already-instantiated body and the eager [#"mif"] / [#"bool?"] check + reduces to [#"Error"]. *) +Lemma eq_dtt_uT_mismatch : eq_term target_multilanguage c_dtt_uT_mismatch s_dtt_uT_mismatch l_dtt_uT_mismatch r_dtt_uT_mismatch. +Proof. unfold c_dtt_uT_mismatch, s_dtt_uT_mismatch, l_dtt_uT_mismatch, r_dtt_uT_mismatch. by_reduction_fwd. Qed. + +Definition c_dtt_uF_mismatch := Eval vm_compute in gctx "dtt uF mismatch". +Definition s_dtt_uF_mismatch := Eval vm_compute in gsrt "dtt uF mismatch". +Definition l_dtt_uF_mismatch := Eval vm_compute in glhs "dtt uF mismatch". +Definition r_dtt_uF_mismatch := Eval vm_compute in grhs "dtt uF mismatch". +(* As "dtt uT mismatch". *) +Lemma eq_dtt_uF_mismatch : eq_term target_multilanguage c_dtt_uF_mismatch s_dtt_uF_mismatch l_dtt_uF_mismatch r_dtt_uF_mismatch. +Proof. unfold c_dtt_uF_mismatch, s_dtt_uF_mismatch, l_dtt_uF_mismatch, r_dtt_uF_mismatch. by_reduction_fwd. Qed. + +Definition c_exp_subst_dtt := Eval vm_compute in gctx "exp_subst dtt". +Definition s_exp_subst_dtt := Eval vm_compute in gsrt "exp_subst dtt". +Definition l_exp_subst_dtt := Eval vm_compute in glhs "exp_subst dtt". +Definition r_exp_subst_dtt := Eval vm_compute in grhs "exp_subst dtt". +(* The three typerec cases are constants with one-step substitution rules + ("val_subst bstar"/"bbool"/"bfunc"), so this reduces directly. *) +Lemma eq_exp_subst_dtt : eq_term target_multilanguage c_exp_subst_dtt s_exp_subst_dtt l_exp_subst_dtt r_exp_subst_dtt. +Proof. unfold c_exp_subst_dtt, s_exp_subst_dtt, l_exp_subst_dtt, r_exp_subst_dtt. by_reduction_fwd. Qed. + +Definition c_exp_subst_ttd := Eval vm_compute in gctx "exp_subst ttd". +Definition s_exp_subst_ttd := Eval vm_compute in gsrt "exp_subst ttd". +Definition l_exp_subst_ttd := Eval vm_compute in glhs "exp_subst ttd". +Definition r_exp_subst_ttd := Eval vm_compute in grhs "exp_subst ttd". +(* As "exp_subst dtt". *) +Lemma eq_exp_subst_ttd : eq_term target_multilanguage c_exp_subst_ttd s_exp_subst_ttd l_exp_subst_ttd r_exp_subst_ttd. +Proof. unfold c_exp_subst_ttd, s_exp_subst_ttd, l_exp_subst_ttd, r_exp_subst_ttd. by_reduction_fwd. Qed. + +(* ------------------------------------------------------------------ *) +(* All 13 boundary equations are discharged above, so the whole-compiler + theorem is assembled from them by hand. [compute_preserving_compiler] + is NOT usable: its [eq_term_oracle] would re-run the e-graph on every + equation, including the two ["func"] ones that only converge when split + into the two hops above. + + [pct] is [CompilerDefs.preserving_compiler_term] restated with the + [map fst c = cargs] side condition as an explicit (computational) + premise: the constructor as stated cannot be applied, since unifying + [map fst ?c] with the literal argument list of a [term_case] is not a + unification problem Coq can solve. *) +Lemma pct + : forall cmp l n c args e t cargs, + preserving_compiler_ext (tgt_Model := core_model target_multilanguage) + interoperating_langs_compiler cmp l -> + map fst c = cargs -> + Model.wf_term (Model := core_model target_multilanguage) + (compile_ctx (cmp ++ interoperating_langs_compiler) c) e + (compile_sort (cmp ++ interoperating_langs_compiler) t) -> + preserving_compiler_ext (tgt_Model := core_model target_multilanguage) + interoperating_langs_compiler ((n, term_case cargs e)::cmp) + ((n, term_rule c args t) :: l). +Proof. intros; subst; constructor; auto. Qed. + +Ltac solve_boundary_case := + solve [ exact dtt_case_wf | exact ttd_case_wf + | exact eq_dtt_star | exact eq_ttd_star + | exact eq_dtt_True | exact eq_dtt_False + | exact eq_ttd_True | exact eq_ttd_False + | exact eq_dtt_func | exact eq_ttd_func + | exact eq_dtt_ulambda_mismatch + | exact eq_dtt_uT_mismatch | exact eq_dtt_uF_mismatch + | exact eq_exp_subst_dtt | exact eq_exp_subst_ttd ]. + +Lemma simple_multilang_compiler_preserving + : preserving_compiler_ext (tgt_Model := core_model target_multilanguage) + interoperating_langs_compiler simple_multilang_compiler boundaries. +Proof. + unfold boundaries, simple_multilang_compiler. + repeat lazymatch goal with + | |- preserving_compiler_ext _ _ _ => + first [ eapply pct; [ | vm_compute; reflexivity | ] + | constructor ] + end. + all: solve_boundary_case. +Qed. + +#[local] Definition simple_multilang_compiler_entry := + cmp_entry simple_multilang_compiler_preserving. +#[export] Hint Resolve simple_multilang_compiler_entry : preserving_db. diff --git a/src/Pyrosome/Lang/Multilanguages/TrecTerms.v b/src/Pyrosome/Lang/Multilanguages/TrecTerms.v new file mode 100644 index 00000000..bd9d23c6 --- /dev/null +++ b/src/Pyrosome/Lang/Multilanguages/TrecTerms.v @@ -0,0 +1,254 @@ +(* The boundary case constants [#"bstar"], [#"bbool"] and [#"bfunc"] that + [#"typerec"] recurses with, the full [target_multilanguage] they complete, + and [trec_boundaries], the derived coercion pair at an arbitrary type. *) + +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 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. +From Pyrosome Require Import Tools.EGraph.InjRuleGen. + +(* 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 TypeCasing. + + +(* Helpers for de Bruijn-style value variables in the derived terms. *) +Fixpoint wkn_n n := + match n with + | 0 => {{e #"id"}} + | 1 => {{e #"wkn"}} + | S n' => + {{e #"cmp" #"wkn" {wkn_n n'} }} + end. + +Definition ovar n := {{e #"val_subst" {wkn_n n} #"hd" }}. + +Ltac solve_eq_sort_disj := + right; compute_eq_compilation; sort_cong; repeat by_reduction. + +(* Discharges an [elab_term] (or the sort side condition of one) in + [language]. The trailing [by_reduction] after the [repeat by_reduction] + is load-bearing: the leaves left over from the repeat are order-sensitive, + and one further round closes them. *) +Ltac solve_elab_term_or_sort language := + assert (wf_lang language) by prove_by_lang_db; + unshelve (repeat t; decompose_sort_eq; repeat by_reduction; by_reduction); compute_term_wf. + +(* Diagnostic: reports whether an [elab_term] goal can be decomposed + further. Unused, but kept as an example of the Pyrosome workflow. *) +Ltac quick_goal_match := + lazymatch goal with + | |- elab_term _ _ (con ?s _) (con ?s _) _ => + idtac "can go further" + | |- elab_term _ _ (con ?s _) (con ?s' _) _ => + fail "cannot go further" + | |- _ => idtac "neither case" + end. + + +(* ------------------------------------------------------------------ *) +(* The three boundary cases, as value constants. + + Each case is a constant with a defining equation rather than a derived + term plugged directly into [#"typerec"]. This matters for substitution: + pushing a substitution -- a term substitution, for the + ["exp_subst dtt"] / ["exp_subst ttd"] equations, or the type substitution + produced by ["typerec func"] -- through a derived term means traversing + its whole body, which is far beyond what the e-graph can do, whereas a + constant absorbs it in a single rewrite from its ["val_subst"] / + ["ty_subst"] equation. *) + +(* [P X] is [sigma[X]] for the concrete [sigma] used by the boundaries, + [sigma] being [prod (arrow ty_hd star) (arrow star ty_hd)]. *) +Definition P X := {{e #"prod" (#"->" {X} #"*") (#"->" #"*" {X}) }}. +Definition boundary_sigma := Eval compute in P {{e #"ty_hd"}}. + +Definition Pa := Eval compute in P tva. +Definition Pb := Eval compute in P tvb. +Definition Pab := Eval compute in P {{e #"->" {tva} {tvb} }}. + +(* [#"bfunc"] takes its instantiation as explicit arguments: the two types + and the two recursive results. This is what makes ["typerec func"] cheap: + the instantiating type substitution it produces is absorbed by + ["ty_subst bfunc"] in one rewrite instead of being pushed through the + whole wrapper body. *) +Definition bfunc_ty := Eval compute in P {{e #"->" "t1" "t2"}}. +Definition bfunc_sort := + {{s #"val" "D" "G" {bfunc_ty} }}. + +Definition bstar_body := + {{e #"pair_val" (#"lambda" #"*" (#"ret" #"hd")) (#"lambda" #"*" (#"ret" #"hd")) }}. + +Definition bbool_body := + {{e #"pair_val" + (#"lambda" #"bool" (#"if" (#"ret" #"hd") (#"ret" #"uT") (#"ret" #"uF"))) + (#"lambda" #"*" (#"mif" (#"ret" #"hd") (#"ret" #"T") (#"ret" #"F"))) }}. + +(* The two wrappers. The recursive results are the explicit arguments + ["c1"] / ["c2"], weakened under the three binders that separate them from + the environment [G], and the two types are the arguments ["t1"] / ["t2"] + rather than bound type variables. *) +Definition c1w := {{e #"val_subst" {wkn_n 3} "c1" }}. +Definition c2w := {{e #"val_subst" {wkn_n 3} "c2" }}. + +Definition bfunc_body := + {{e #"pair_val" + (#"lambda" (#"->" "t1" "t2") + (#"ret" (#"ulambda" + (#"let" (#"app" (#"ret" {ovar 1}) + (#"let" (#"ret" {ovar 0}) + (#"app" (#".2" (#"ret" {c1w})) (#"ret" {ovar 0})))) + (#"app" (#".1" (#"ret" {c2w})) (#"ret" {ovar 0})))))) + (#"lambda" #"*" + (#"mif" (#"bool?" (#"ret" {ovar 0})) + (#"Error" (#"->" "t1" "t2")) + (#"ret" (#"lambda" "t1" + (#"let" (#"uapp" (#"ret" {ovar 1}) + (#"let" (#"ret" {ovar 0}) + (#"app" (#".1" (#"ret" {c1w})) (#"ret" {ovar 0})))) + (#"app" (#".2" (#"ret" {c2w})) (#"ret" {ovar 0}))))))) }}. + +Definition boundary_cases_def : lang := + {[l + [:| "D" : #"ty_env", "G" : #"env" "D" + ----------------------------------------------- + #"bstar" : #"val" "D" "G" {P {{e #"*"}} } + ]; + [:| "D" : #"ty_env", "G" : #"env" "D" + ----------------------------------------------- + #"bbool" : #"val" "D" "G" {P {{e #"bool"}} } + ]; + [:| "D" : #"ty_env", "G" : #"env" "D", + "t1" : #"ty" "D", "t2" : #"ty" "D", + "c1" : #"val" "D" "G" {P {{e "t1"}} }, + "c2" : #"val" "D" "G" {P {{e "t2"}} } + ----------------------------------------------- + #"bfunc" "t1" "t2" "c1" "c2" : {bfunc_sort} + ]; + [:= "D" : #"ty_env", "G" : #"env" "D", "G'" : #"env" "D", + "g" : #"sub" "D" "G'" "G" + ----------------------------------------------- ("val_subst bstar") + #"val_subst" "g" #"bstar" = #"bstar" : #"val" "D" "G'" {P {{e #"*"}} } + ]; + [:= "D" : #"ty_env", "G" : #"env" "D", "G'" : #"env" "D", + "g" : #"sub" "D" "G'" "G" + ----------------------------------------------- ("val_subst bbool") + #"val_subst" "g" #"bbool" = #"bbool" : #"val" "D" "G'" {P {{e #"bool"}} } + ]; + [:= "D" : #"ty_env", "G" : #"env" "D", "G'" : #"env" "D", + "g" : #"sub" "D" "G'" "G", + "t1" : #"ty" "D", "t2" : #"ty" "D", + "c1" : #"val" "D" "G" {P {{e "t1"}} }, + "c2" : #"val" "D" "G" {P {{e "t2"}} } + ----------------------------------------------- ("val_subst bfunc") + #"val_subst" "g" (#"bfunc" "t1" "t2" "c1" "c2") + = #"bfunc" "t1" "t2" (#"val_subst" "g" "c1") (#"val_subst" "g" "c2") + : #"val" "D" "G'" {bfunc_ty} + ]; + [:= "D" : #"ty_env", "D'" : #"ty_env", "G" : #"env" "D", + "g" : #"ty_sub" "D'" "D" + ----------------------------------------------- ("ty_subst bstar") + #"val_ty_subst" "g" #"bstar" = #"bstar" + : #"val" "D'" (#"env_ty_subst" "g" "G") {P {{e #"*"}} } + ]; + [:= "D" : #"ty_env", "D'" : #"ty_env", "G" : #"env" "D", + "g" : #"ty_sub" "D'" "D" + ----------------------------------------------- ("ty_subst bbool") + #"val_ty_subst" "g" #"bbool" = #"bbool" + : #"val" "D'" (#"env_ty_subst" "g" "G") {P {{e #"bool"}} } + ]; + [:= "D" : #"ty_env", "G" : #"env" "D" + ----------------------------------------------- ("bstar def") + #"bstar" = {bstar_body} : #"val" "D" "G" {P {{e #"*"}} } + ]; + [:= "D" : #"ty_env", "G" : #"env" "D" + ----------------------------------------------- ("bbool def") + #"bbool" = {bbool_body} : #"val" "D" "G" {P {{e #"bool"}} } + ]; + [:= "D" : #"ty_env", "D'" : #"ty_env", "G" : #"env" "D", + "g" : #"ty_sub" "D'" "D", + "t1" : #"ty" "D", "t2" : #"ty" "D", + "c1" : #"val" "D" "G" {P {{e "t1"}} }, + "c2" : #"val" "D" "G" {P {{e "t2"}} } + ----------------------------------------------- ("ty_subst bfunc") + #"val_ty_subst" "g" (#"bfunc" "t1" "t2" "c1" "c2") + = #"bfunc" (#"ty_subst" "g" "t1") (#"ty_subst" "g" "t2") + (#"val_ty_subst" "g" "c1") (#"val_ty_subst" "g" "c2") + : #"val" "D'" (#"env_ty_subst" "g" "G") + {P {{e #"->" (#"ty_subst" "g" "t1") (#"ty_subst" "g" "t2")}} } + ]; + [:= "D" : #"ty_env", "G" : #"env" "D", + "t1" : #"ty" "D", "t2" : #"ty" "D", + "c1" : #"val" "D" "G" {P {{e "t1"}} }, + "c2" : #"val" "D" "G" {P {{e "t2"}} } + ----------------------------------------------- ("bfunc def") + #"bfunc" "t1" "t2" "c1" "c2" = {bfunc_body} : {bfunc_sort} + ] + ]}. + +Definition boundary_cases := + Eval vm_compute in + infer_lang_ext_simple_incr 10 100 target_multilanguage_pre boundary_cases_def. + +Lemma boundary_cases_wf : wf_lang_ext target_multilanguage_pre boundary_cases. +Proof. compute_wf_lang. Qed. +#[local] Definition boundary_cases_entry := lang_entry boundary_cases_wf. +#[export] Hint Resolve boundary_cases_entry : wf_lang_db. + +Definition target_multilanguage := boundary_cases ++ target_multilanguage_pre. +Hint Unfold target_multilanguage : auto_elab. + +Lemma target_multilanguage_wf : wf_lang target_multilanguage. +Proof. prove_by_lang_db. Qed. +#[local] Definition target_multilanguage_entry := + lang_entry target_multilanguage_wf. +#[export] Hint Resolve target_multilanguage_entry : wf_lang_db. + +(* ------------------------------------------------------------------ *) +(* [trec_boundaries] is the [#"typerec"] value applied to the three boundary + case constants: the pair of coercions between a type [A] and the dynamic + type, built by recursion on [A]. *) +Definition trec_boundaries_unelab := + {{e #"typerec" "A" {boundary_sigma} #"bstar" #"bbool" + (#"bfunc" {tva} {tvb} {ovar 1} {ovar 0}) }}. + +Definition trec_boundaries_sort := + {{s #"val" #"ty_emp" "G" + (#"prod" #"ty_emp" + (#"->" #"ty_emp" "A" (#"*" #"ty_emp")) + (#"->" #"ty_emp" (#"*" #"ty_emp") "A")) }}. + +Derive trec_boundaries + in ( elab_term target_multilanguage + [("A", {{s #"ty" #"ty_emp"}}); ("G", {{s #"env" #"ty_emp"}})] + trec_boundaries_unelab + trec_boundaries + trec_boundaries_sort + ) as trec_boundaries_wf. +Proof. solve_elab_term_or_sort target_multilanguage. Qed. diff --git a/src/Pyrosome/Lang/Multilanguages/TypeCasing.v b/src/Pyrosome/Lang/Multilanguages/TypeCasing.v new file mode 100644 index 00000000..23c7da66 --- /dev/null +++ b/src/Pyrosome/Lang/Multilanguages/TypeCasing.v @@ -0,0 +1,274 @@ +(* The type-casing fragment: [#"typerec"], a value-level recursor over + types, and the languages it sits on top of. Also assembles + [source_multilanguage] and [target_multilanguage_pre], the target + multilanguage minus the boundary case constants added in TrecTerms.v. *) + +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 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. +From Pyrosome Require Import Tools.EGraph.InjRuleGen. + +(* 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 Boundaries. + +(* The type-casing fragment of the target multilanguage (the multilanguage + without boundary forms). First, some helpers for building type + substitutions and de Bruijn-style type variables. *) +Fixpoint ty_wkn_n n := + match n with + | 0 => {{e #"ty_id"}} + | 1 => {{e #"ty_wkn"}} + | S n' => {{e #"ty_cmp" #"ty_wkn" {ty_wkn_n n'} }} + end. + +Definition ty_ovar n := + match n with + | 0 => {{e #"ty_hd"}} (* bc ty_subst ty_id ty_hd is just ty_hd *) + | S _ => {{e #"ty_subst" {ty_wkn_n n} #"ty_hd" }} + end. + +(* ------------------------------------------------------------------ *) +(* Value-level typerec. + + [#"typerec"] returns a [#"val"], not an [#"exp"], and its function case + is a *value* obtained by substituting the two recursive results into a + single value variable ["v3"] that abstracts over two type variables and + two term variables. + + The value level is what makes the fragment usable: an expression-level + formulation would have ["typerec func"] apply [#"app"] to the expressions + [#"typerec" "t1" ...] / [#"typerec" "t2" ...], which are stuck when the + type is a metavariable, so [STLC-beta] -- which needs a [#"ret" "v"] + argument -- could never apply and the boundary equations at type + [#"->" "A" "B"] would not be provable. *) + +(* [sigma] instantiated at [X] (X : ty D), i.e. sigma[X] *) +Definition Sg X := {{e #"ty_subst" (#"ty_snoc" #"ty_id" {X}) "sigma" }}. +(* [sigma] instantiated at [X], under two extra type variables + (X : ty (ty_ext (ty_ext D))) *) +Definition S2 X := {{e #"ty_subst" (#"ty_snoc" {ty_wkn_n 2} {X}) "sigma" }}. +(* the two extra type variables *) +Definition tva := Eval compute in ty_ovar 1. +Definition tvb := Eval compute in ty_ovar 0. +(* [G] weakened by the two extra type variables *) +Definition G2 := {{e #"env_ty_subst" {ty_wkn_n 2} "G" }}. +Definition G2' := {{e #"env_ty_subst" {ty_wkn_n 2} "G'" }}. + +(* the sort of the function case, [v3] *) +Definition v3_env := {{e #"ext" (#"ext" {G2} {S2 tva}) {S2 tvb} }}. +Definition v3_env' := {{e #"ext" (#"ext" {G2'} {S2 tva}) {S2 tvb} }}. +Definition v3_sort := + {{s #"val" (#"ty_ext" (#"ty_ext" "D")) {v3_env} + {S2 {{e #"->" {tva} {tvb} }} } }}. + +(* the two type variables lift of a term substitution "g", then the two + term-variable lifts *) +Definition g_lift := + {{e #"snoc" (#"cmp" #"wkn" + (#"snoc" (#"cmp" #"wkn" (#"sub_ty_subst" {ty_wkn_n 2} "g")) #"hd")) #"hd" }}. +(* the two type variable lift of a type substitution "g" *) +Definition ty_lift1 g := {{e #"ty_snoc" (#"ty_cmp" #"ty_wkn" {g}) #"ty_hd" }}. +Definition ty_lift2 := Eval compute in ty_lift1 (ty_lift1 {{e "g"}}). + +Definition type_casing_rest_def : lang := + {[l + [:| "D" : #"ty_env", + "G" : #"env" "D", + "mu" : #"ty" "D", + "sigma" : #"ty" (#"ty_ext" "D"), + "v1" : #"val" "D" "G" {Sg {{e #"*"}} }, + "v2" : #"val" "D" "G" {Sg {{e #"bool"}} }, + "v3" : {v3_sort} + ----------------------------------------------- + #"typerec" "mu" "sigma" "v1" "v2" "v3" + : #"val" "D" "G" {Sg {{e "mu"}} } + ]; + [:= "D" : #"ty_env", + "G" : #"env" "D", + "sigma" : #"ty" (#"ty_ext" "D"), + "v1" : #"val" "D" "G" {Sg {{e #"*"}} }, + "v2" : #"val" "D" "G" {Sg {{e #"bool"}} }, + "v3" : {v3_sort} + ----------------------------------------------- ("typerec star") + #"typerec" #"*" "sigma" "v1" "v2" "v3" + = "v1" : #"val" "D" "G" {Sg {{e #"*"}} } + ]; + [:= "D" : #"ty_env", + "G" : #"env" "D", + "sigma" : #"ty" (#"ty_ext" "D"), + "v1" : #"val" "D" "G" {Sg {{e #"*"}} }, + "v2" : #"val" "D" "G" {Sg {{e #"bool"}} }, + "v3" : {v3_sort} + ----------------------------------------------- ("typerec bool") + #"typerec" #"bool" "sigma" "v1" "v2" "v3" + = "v2" : #"val" "D" "G" {Sg {{e #"bool"}} } + ]; + [:= "D" : #"ty_env", + "G" : #"env" "D", + "sigma" : #"ty" (#"ty_ext" "D"), + "t1" : #"ty" "D", + "t2" : #"ty" "D", + "v1" : #"val" "D" "G" {Sg {{e #"*"}} }, + "v2" : #"val" "D" "G" {Sg {{e #"bool"}} }, + "v3" : {v3_sort} + ----------------------------------------------- ("typerec func") + #"typerec" (#"->" "t1" "t2") "sigma" "v1" "v2" "v3" + = #"val_subst" + (#"snoc" (#"snoc" #"id" (#"typerec" "t1" "sigma" "v1" "v2" "v3")) + (#"typerec" "t2" "sigma" "v1" "v2" "v3")) + (#"val_ty_subst" (#"ty_snoc" (#"ty_snoc" #"ty_id" "t1") "t2") "v3") + : #"val" "D" "G" {Sg {{e #"->" "t1" "t2"}} } + ]; + [:= "D" : #"ty_env", + "D'" : #"ty_env", + "G" : #"env" "D", + "g" : #"ty_sub" "D'" "D", + "mu" : #"ty" "D", + "sigma" : #"ty" (#"ty_ext" "D"), + "v1" : #"val" "D" "G" {Sg {{e #"*"}} }, + "v2" : #"val" "D" "G" {Sg {{e #"bool"}} }, + "v3" : {v3_sort} + ----------------------------------------------- ("ty_subst typerec") + #"val_ty_subst" "g" (#"typerec" "mu" "sigma" "v1" "v2" "v3") + = #"typerec" (#"ty_subst" "g" "mu") + (#"ty_subst" (#"ty_snoc" (#"ty_cmp" #"ty_wkn" "g") #"ty_hd") "sigma") + (#"val_ty_subst" "g" "v1") (#"val_ty_subst" "g" "v2") + (#"val_ty_subst" {ty_lift2} "v3") + : #"val" "D'" (#"env_ty_subst" "g" "G") (#"ty_subst" "g" {Sg {{e "mu"}} }) + ] + ]}. + + +(* The ["val_subst typerec"] rule is elaborated separately: type inference + leaves the environment of ["v3"] as a hole here, because it is only + determined through the doubly-lifted substitution [g_lift], so this one + rule goes through [auto_elab] instead. *) +Definition val_subst_typerec_def : lang := + {[l + [:= "D" : #"ty_env", + "G" : #"env" "D", + "G'" : #"env" "D", + "g" : #"sub" "D" "G'" "G", + "mu" : #"ty" "D", + "sigma" : #"ty" (#"ty_ext" "D"), + "v1" : #"val" "D" "G" {Sg {{e #"*"}} }, + "v2" : #"val" "D" "G" {Sg {{e #"bool"}} }, + "v3" : {v3_sort} + ----------------------------------------------- ("val_subst typerec") + #"val_subst" "g" (#"typerec" "mu" "sigma" "v1" "v2" "v3") + = #"typerec" "mu" "sigma" (#"val_subst" "g" "v1") (#"val_subst" "g" "v2") + (#"val_subst" {g_lift} "v3") + : #"val" "D" "G'" {Sg {{e "mu"}} } + ] + ]}. +Definition TC_BASE := + stlc_ty_subst ++ + typed_bool_ty_subst ++ + star_type_ty_subst ++ error_t_ty_subst ++ + typed_bool_parameterized ++ + stlc_parameterized ++ + star_type_parameterized ++ error_t_parameterized ++ + poly ++ (* needed for #"All" *) + (* the polymorphic base *) + 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. + +(* [type_casing] is elaborated in two pieces. The five rules that type + inference resolves completely go through the computational pathway + ([infer_lang_ext_simple_incr] plus [compute_wf_lang]), which scales to the + whole fragment; the remaining rule, ["val_subst typerec"], is elaborated + by [auto_elab] on its own below. *) +Definition type_casing_rest := + Eval vm_compute in + infer_lang_ext_simple_incr 10 100 TC_BASE type_casing_rest_def. + +Lemma type_casing_rest_wf : wf_lang_ext TC_BASE type_casing_rest. +Proof. compute_wf_lang. Qed. +#[local] Definition type_casing_rest_entry := lang_entry type_casing_rest_wf. +#[export] Hint Resolve type_casing_rest_entry : wf_lang_db. + +Derive type_casing_vs + in (elab_lang_ext (type_casing_rest ++ TC_BASE) + val_subst_typerec_def type_casing_vs) + as type_casing_vs_wf. +(* [auto_elab] cannot be used directly here: its [cleanup_auto_elab] step is + not wrapped in [try], while some leaves of this rule need [by_reduction] + instead. The same steps are therefore run with the leaf tactics made + total. *) +Proof. + setup_elab_lang. + unshelve (eapply eq_term_rule; + [break_down_elab_ctx | break_elab_sort | try_break_elab_term | try_break_elab_term]). + all: try (try apply eq_term_refl; try by_reduction; try cleanup_auto_elab). +Qed. +#[local] Definition type_casing_vs_entry := + lang_entry (elab_lang_implies_wf type_casing_vs_wf). +#[export] Hint Resolve type_casing_vs_entry : wf_lang_db. + +Definition type_casing := type_casing_vs ++ type_casing_rest. + +Lemma type_casing_wf : wf_lang_ext TC_BASE type_casing. +Proof. + apply wf_lang_concat_hd. + unfold type_casing; rewrite <- app_assoc. + apply wf_lang_concat. + { apply wf_lang_concat; [ prove_by_lang_db | exact type_casing_rest_wf ]. } + { exact (elab_lang_implies_wf type_casing_vs_wf). } +Qed. +#[local] Definition type_casing_entry := lang_entry type_casing_wf. +#[export] Hint Resolve type_casing_entry : wf_lang_db. + +Definition source_multilanguage := + boundaries ++ simple_interoperating_langs. +Hint Unfold source_multilanguage : auto_elab. + +(* The target multilanguage *without* the boundary case constants; the full + [target_multilanguage] is [boundary_cases ++ target_multilanguage_pre], + defined in TrecTerms.v. *) +Definition target_multilanguage_pre := + let_eta_parameterized ++ let_ty_subst ++ let_parameterized ++ + prod_ty_subst ++ prod_parameterized ++ + type_casing ++ + polymorphic_interoperating_langs. +Hint Unfold target_multilanguage_pre : auto_elab. + +Lemma source_multilanguage_wf : wf_lang source_multilanguage. +Proof. prove_by_lang_db. Qed. +#[local] Definition source_multilanguage_entry := + lang_entry source_multilanguage_wf. +#[export] Hint Resolve source_multilanguage_entry : wf_lang_db. + +Lemma target_multilanguage_pre_wf : wf_lang target_multilanguage_pre. +Proof. prove_by_lang_db. Qed. +#[local] Definition target_multilanguage_pre_entry := + lang_entry target_multilanguage_pre_wf. +#[export] Hint Resolve target_multilanguage_pre_entry : wf_lang_db. diff --git a/src/Pyrosome/Lang/Multilanguages/TyperecPartialEval.v b/src/Pyrosome/Lang/Multilanguages/TyperecPartialEval.v index 6334ddd5..381e4f4d 100644 --- a/src/Pyrosome/Lang/Multilanguages/TyperecPartialEval.v +++ b/src/Pyrosome/Lang/Multilanguages/TyperecPartialEval.v @@ -8,7 +8,8 @@ From Utils Require Import Utils. (* imports for compilers *) (* copied from LinearCPS.v *) -From Pyrosome Require Import Compilers.Compilers Elab.ElabCompilers. +From Pyrosome Require Import Compilers.Compilers Compilers.SemanticsPreservingDef + Compilers.CompilerFacts Elab.ElabCompilers. Import CompilerDefs.Notations. (* for `match # from high_level_multilanguage with` *) (* CompilerDefs, for preserving_compiler_ext, is already imported. Prolly through something else. *) @@ -17,90 +18,172 @@ From Pyrosome Require Import Theory.Core Elab.Elab Tools.EGraph.TypeInference Tools.Resolution Tools.EGraph.ComputeWf. Import Core.Notations. -Require Coq.derive.Derive. - (* import the relevant language fragments *) -From Pyrosome.Lang Require Import SimpleVSTLC. -From Pyrosome.Lang Require Import UTLC. -From Pyrosome.Lang Require Import BoolType. +From Pyrosome.Lang Require Import SimpleVSTLC. +From Pyrosome.Lang Require Import UTLC. +From Pyrosome.Lang Require Import BoolType. From Pyrosome.Lang Require Import SimpleVProd. From Pyrosome.Lang.Multilanguages Require Import SimpleBoundaries. (* for induction on wfness of terms *) From Pyrosome.Theory Require Import WfCutElim CutFreeInd. +From Pyrosome.Theory Require Conservativity. (* imports for polymorphism *) From Pyrosome.Lang Require Import PolySubst SimpleVSubst. -From Pyrosome.Lang Require Import PolyCompilers. (* for parameterizing existing languages*) +From Pyrosome.Lang Require Import PolyCompilers PolyCompilerLangs PolyCompilersCPS. (* for parameterizing existing languages*) From Pyrosome.Compilers Require Import Parameterizer. Import Pyrosome.Tools.UnElab. -(* Now the compiler. Three parts: base identity compiler, then a first pass partial evaluation to get rid of #"All" in typerecs, and then a second pass to get rid of the boundaries *) +(* Partial evaluation of [#"typerec"] in the multilanguage target. + + [elim_typerec] rewrites every [#"typerec"] node whose type argument is a + *simple* type (built from [#"*"], [#"bool"] and [#"->"]) into the + corresponding case of the typerec, recursively. The file establishes: + - [can_eliminate_typerec]: every compiled source term only contains + typerecs at simple types; + - [elim_typerec_eq] / [partial_eval_preserves_equality]: the partial + evaluation is an equality in the target; + - [partial_eval_wf_in_no_typerec_lang] / [compiled_partial_eval_wf]: the + result is well typed in [target_multilanguage_without_typerec], the + target with the typerec rules removed. + See README.md in this directory for how this fits into the multilanguage + compiler pipeline. *) Local Notation compiler := (compiler string). Local Notation preserving_compiler_ext tgt cmp_pre cmp src := (* copied from Paramaterizer, 2523 *) (preserving_compiler_ext (tgt_Model:=core_model tgt) cmp_pre cmp src). -(* partial evaluator to get rid of type casing. *) -Definition func_partial_eval_ctx' := - Eval vm_compute in Rule.get_ctx (named_list_lookup default target_multilanguage "typerec func"). +(* ------------------------------------------------------------------ *) +(* Definitions of the partial evaluator. *) +(* ------------------------------------------------------------------ *) -Definition comp_t1_type := {{s #"exp" "D" "G" (#"ty_subst" "D" (#"ty_ext" "D") (#"ty_snoc" "D" "D" (#"ty_id" "D") "t1") "sigma") }}. +(* The arrow case, [fpe2], is read off from the ["typerec func"] rule itself: + it *is* the right-hand side of that rule with the two recursive + [#"typerec"] calls replaced by the variables ["comp_t1"]/["comp_t2"]. + It is deliberately not a separately elaborated copy of that right-hand + side: the two elaborations differ in the *implicit* environment/type + arguments of the outermost [#"val_subst"] (elaborating the rule simplifies + an [#"env_ty_subst"] away, elaborating a standalone term does not), so an + instance of the rule's right-hand side would not be an instance of the + standalone term, and the metatheory below could not be closed. ["sigma"] + occurs free in the right-hand side, so it must be part of the + substitution; otherwise [elim_typerec] of a closed term would have a free + variable in it. *) +Definition rule_parts (n : string) := + match named_list_lookup_err target_multilanguage n with + | Some (term_eq_rule c e1 e2 t) => (c,e1,e2,t) + | _ => ([],var "",var "",{{s #"X"}}) + end. +Definition R_star := Eval vm_compute in rule_parts "typerec star". +Definition R_bool := Eval vm_compute in rule_parts "typerec bool". +Definition R_func := Eval vm_compute in rule_parts "typerec func". +Definition R_star_c := Eval vm_compute in fst (fst (fst R_star)). +Definition R_bool_c := Eval vm_compute in fst (fst (fst R_bool)). +Definition R_func_c := Eval vm_compute in fst (fst (fst R_func)). +Definition R_func_r := Eval vm_compute in snd (fst R_func). +Definition R_func_t := Eval vm_compute in snd R_func. -Definition comp_t2_type := {{s #"exp" "D" "G" (#"ty_subst" "D" (#"ty_ext" "D") (#"ty_snoc" "D" "D" (#"ty_id" "D") "t2") "sigma") }}. +(* [#"val" D G (sigma[X])], the sort of [#"typerec"] at type [X]. *) +Definition Sgt (D G sigma X : term) : sort := + {{s #"val" {D} {G} (#"ty_subst" {D} (#"ty_ext" {D}) (#"ty_snoc" {D} {D} (#"ty_id" {D}) {X}) {sigma}) }}. -Definition func_partial_eval_ctx := Eval vm_compute in [("comp_t2", comp_t2_type); ("comp_t1", comp_t1_type); ("e3", named_list_lookup default func_partial_eval_ctx' "e3"); ("t2", named_list_lookup default func_partial_eval_ctx' "t2"); ("t1", named_list_lookup default func_partial_eval_ctx' "t1"); ("sigma", named_list_lookup default func_partial_eval_ctx' "sigma"); ("G", named_list_lookup default func_partial_eval_ctx' "G"); ("D", named_list_lookup default func_partial_eval_ctx' "D")]. +Fixpoint abstract_typerec (e : term) : term := + match e with + | con "typerec" [_;_;_;_;var "t1";_;_] => var "comp_t1" + | con "typerec" [_;_;_;_;var "t2";_;_] => var "comp_t2" + | con n l => con n (map abstract_typerec l) + | var x => var x + end. +Definition fpe2 := Eval vm_compute in abstract_typerec R_func_r. +Definition fpe2_ctx := Eval vm_compute in + ("comp_t2", Sgt {{e "D"}} {{e "G"}} {{e "sigma"}} {{e "t2"}}) + :: ("comp_t1", Sgt {{e "D"}} {{e "G"}} {{e "sigma"}} {{e "t1"}}) + :: (filter (fun p => negb (orb (eqb (fst p) "v1") (eqb (fst p) "v2"))) R_func_c). -Definition func_partial_eval_term_def := (* comp_t1 ie computation of type t1. cf substitution in meta_typerec *) - {{e #"app" (#"@" (#"app" (#"@" "e3" "t1") "comp_t1") "t2") "comp_t2" }}. +Lemma fpe2_ctx_wf : @Model.wf_ctx _ _ _ (core_model target_multilanguage) fpe2_ctx. +Proof. pose proof target_multilanguage_wf. solve_wf_ctx. Qed. -Derive func_partial_eval_term - in ( elab_term target_multilanguage - func_partial_eval_ctx - func_partial_eval_term_def - func_partial_eval_term - {{s #"exp" "D" "G" (#"ty_subst" "D" (#"ty_ext" "D") (#"ty_snoc" "D" "D" (#"ty_id" "D") (#"->" "D" "t1" "t2")) "sigma") }} - ) as func_partial_eval_term_wf. -Proof. solve_elab_term_or_sort target_multilanguage. Qed. +Lemma fpe2_wf : Core.wf_term target_multilanguage fpe2_ctx fpe2 R_func_t. +Proof. pose proof target_multilanguage_wf. compute_term_wf. Qed. -Fixpoint meta_typerec (D G mu sigma e1 e2 e3 : term) : term := +Definition MT_func (D G sigma t1 t2 r1 r2 v3 : term) : term := + fpe2[/[("comp_t2",r2);("comp_t1",r1);("v3",v3);("t2",t2);("t1",t1); + ("sigma",sigma);("G",G);("D",D)]/]. + +Fixpoint meta_typerec (D G mu sigma e1 e2 e3 : term) {struct mu} : term := match mu with - | {{e #"*" {_} }} => e1 - | {{e #"bool" {_} }} => e2 - | {{e #"->" {_} {t1} {t2} }} => - func_partial_eval_term [/ [ ("e3", e3); - ("t1", t1); - ("comp_t1", meta_typerec D G t1 sigma e1 e2 e3); - ("t2", t2); - ("comp_t2", meta_typerec D G t2 sigma e1 e2 e3); - ("G", G); - ("D", D) ] /] - | _ => mu + | var _ => mu + | con n l => + if eqb n "*" then e1 + else if eqb n "bool" then e2 + else if eqb n "->" then + match l with + | [t2;t1;_] => + MT_func D G sigma t1 t2 + (meta_typerec D G t1 sigma e1 e2 e3) + (meta_typerec D G t2 sigma e1 e2 e3) e3 + | _ => mu end + else mu end. Fixpoint elim_typerec (program : term) : term := match program with - | {{e #"typerec" {D} {G} {mu} {sigma} {e1} {e2} {e3} }} => meta_typerec D G mu sigma (elim_typerec e1) (elim_typerec e2) (elim_typerec e3) - | con n s => con n (map elim_typerec s) | var n => var n + | con n s => + if eqb n "typerec" + then match s with + | [e3;e2;e1;sigma;mu;G;D] => + meta_typerec D G mu sigma (elim_typerec e1) (elim_typerec e2) (elim_typerec e3) + | _ => con n (map elim_typerec s) + end + else con n (map elim_typerec s) end. -Fixpoint is_simple_type (mu : term) : Prop := +(* [is_simple_type] is indexed by the type environment: + [simple_type_at D mu] says that [mu] is built from [#"*"], + [#"bool"] and [#"->"] *at the type environment [D]*. Without that index + the arrow case of [typerec_elim_eq] is unprovable: the ["typerec func"] + rule instance needs the [#"->"] node's type-environment argument to be the + same term as the [#"typerec"] node's, and [target_multilanguage] has no + sort-injectivity principle to recover it. [is_simple_type] is the instance + at the empty type environment, which is where every *compiled* source type + lives ([compile_star] / [compile_bool] / [compile_arrow]). *) +Fixpoint simple_type_at (D mu : term) {struct mu} : Prop := match mu with - | {{e #"*" {_} }} => True - | {{e #"bool" {_} }} => True - | {{e #"->" {_} {t1} {t2} }} => is_simple_type t1 /\ is_simple_type t2 - | _ => False + | var _ => False + | con n l => + if eqb n "*" then match l with [D'] => D' = D | _ => False end + else if eqb n "bool" then match l with [D'] => D' = D | _ => False end + else if eqb n "->" then + match l with + | [t2;t1;D'] => D' = D /\ simple_type_at D t1 /\ simple_type_at D t2 + | _ => False end + else False end. +Definition is_simple_type (mu : term) : Prop := simple_type_at {{e #"ty_emp"}} mu. + +(* Stated so that the "typerec" case is selected by a + *boolean* test on the head name rather than by a nested pattern match. This + makes [all_typerecs_simple (con n s)] reducible when [n] is a variable known + to be different from "typerec", which is what the cheap (non-enumerating) + inversion below needs. It recurses into *every* argument of a [#"typerec"] + node, not just [e1], [e2], [e3]. The type argument is required to be + simple *at the node's own type environment*. *) +Definition typerec_mu_ok (n : string) (s : list term) : Prop := + if eqb n "typerec" + then match s with + | [_;_;_;_;mu;_;D] => simple_type_at D mu + | _ => True + end + else True. + Fixpoint all_typerecs_simple (program : term) : Prop := match program with - | {{e #"typerec" {D} {G} {mu} {sigma} {e1} {e2} {e3} }} => - is_simple_type mu /\ - all_typerecs_simple e1 /\ all_typerecs_simple e2 /\ all_typerecs_simple e3 - | con _ s => all all_typerecs_simple s | var _ => True + | con n s => typerec_mu_ok n s /\ all all_typerecs_simple s end. Ltac invert_wf_args := @@ -108,14 +191,219 @@ Ltac invert_wf_args := | H : ComputeWf.wf_args _ _ _ _ |- _ => inversion H; clear H end. +(* ------------------------------------------------------------------ *) +(* Cheap (reflective) language inversion. *) +(* *) +(* The cut-free induction [wf_term_cut_ind] hands us a hypothesis *) +(* [In (name, term_rule c' args t) l]. Destructing that membership *) +(* enumerates the whole language (193s / 6.5GB for *) +(* [source_multilanguage]). Instead we (a) turn the membership into a *) +(* *lookup* equation, which is cheap because the languages are *) +(* [all_fresh], and (b) restrict [name] to a handful of *) +(* candidates with a boolean [forallb] check over the language, *) +(* discharged once and for all by [vm_compute]. *) +(* ------------------------------------------------------------------ *) + +Local Notation CMP := (simple_multilang_compiler ++ interoperating_langs_compiler). + +Lemma in_lang_lookup (l : lang) n (r : rule) + : all_fresh l -> In (n,r) l -> named_list_lookup_err l n = Some r. +Proof. + intros Hf Hin. symmetry. + apply all_fresh_named_list_lookup_err_in; [ typeclasses eauto | exact Hf | exact Hin ]. +Qed. + +Lemma subst_sort_name_nil (t : sort) n sub + : t[/sub/] = scon n [] -> t = scon n []. +Proof. + destruct t; cbn; intro H; injection H as ? ?; subst. + destruct l; cbn in *; congruence. +Qed. + +(* a strong induction principle for terms *) +Section TermIndAll. + Context (P : term -> Prop) + (Hv : forall n, P (var n)) + (Hc : forall n l, all P l -> P (con n l)). + Fixpoint term_ind_all (e : term) : P e := + match e with + | var n => Hv n + | con n l => + Hc n l ((fix f (l : list term) : all P l := + match l with + | [] => I + | x::l' => conj (term_ind_all x) (f l') + end) l) + end. +End TermIndAll. + +(* every #"typerec" node's type argument is a variable, and its type + environment is the empty one (so that a substitution instance is simple + *at that node's own type environment*, which is what [typerec_mu_ok] + now demands) *) +Definition typerec_head_ok (s : list term) : bool := + match s with + | [_;_;_;_;mu;_;D] => + (match mu with var _ => true | _ => false end) && eqb D {{e #"ty_emp"}} + | _ => false + end. + +Fixpoint typerecs_are_var (e : term) : bool := + match e with + | var _ => true + | con n s => + (if eqb n "typerec" then typerec_head_ok s else true) + && (fix f (l : list term) : bool := + match l with [] => true | x::l' => typerecs_are_var x && f l' end) s + end. + +(* the variables used as the type argument of some #"typerec" node *) +Fixpoint typerec_mu_vars (e : term) : list string := + match e with + | var _ => [] + | con n s => + (if eqb n "typerec" + then match s with + | [_;_;_;_;var m;_;_] => [m] + | _ => [] + end + else []) + ++ (fix f (l : list term) : list string := + match l with [] => [] | x::l' => typerec_mu_vars x ++ f l' end) s + end. + +Lemma ats_lookup s n + : all (fun p => all_typerecs_simple (snd p)) s -> + all_typerecs_simple (term_subst_lookup s n). +Proof. + induction s as [| [m e] s IH]; cbn; [ intros _; exact I | ]. + intros [He Hs]. cbv [term_subst_lookup] in *; cbn. + destruct (eqb n m); [ exact He | apply IH; exact Hs ]. +Qed. + +(* The key substitution lemma: if every [#"typerec"] node of [b] has a + *variable* as its type argument, and every such variable is instantiated by + a simple type, then the instance [b[/s/]] has only simple typerecs. *) +Lemma ats_subst (b : term) (s : subst) + : Is_true (typerecs_are_var b) -> + all (fun p => all_typerecs_simple (snd p)) s -> + all (fun m => is_simple_type (term_subst_lookup s m)) (typerec_mu_vars b) -> + all_typerecs_simple b[/s/]. +Proof. + revert s. induction b using term_ind_all; intros sub Hv Hs Hm. + { cbn. apply ats_lookup; exact Hs. } + { cbn [term_subst term_var_map] in *. + cbn [typerecs_are_var typerec_mu_vars] in Hv, Hm. + apply andb_prop_elim in Hv; destruct Hv as [Hv1 Hv2]. + apply all_app in Hm; destruct Hm as [Hm1 Hm2]. + split. + { cbv [typerec_mu_ok] in *. + destruct (eqb n "typerec"); [ | exact I ]. + cbv [typerec_head_ok] in Hv1. + destruct l as [|a0 [|a1 [|a2 [|a3 [|a4 [|a5 [|a6 [|? ?]]]]]]]]; + try solve [ destruct Hv1 ]. + destruct a4 as [m|]; [ | destruct Hv1 ]. + cbn [andb] in Hv1. apply Is_true_eq_true in Hv1. + pose proof (eqb_spec a6 {{e #"ty_emp"}}) as Hsp; rewrite Hv1 in Hsp; subst a6. + cbn [map term_subst term_var_map]. + cbn in Hm1. destruct Hm1 as [Hm1 _]. exact Hm1. } + { clear Hm1 Hv1. + revert Hm2 Hv2. induction l as [|x l IH']; cbn; [ intros; exact I | ]. + intros Hm2 Hv2. apply andb_prop_elim in Hv2; destruct Hv2 as [Hx Hl]. + apply all_app in Hm2; destruct Hm2 as [Hmx Hml]. + destruct H as [Hpx Hpl]. + split; [ apply Hpx; assumption | apply IH'; assumption ]. } } +Qed. + +Lemma ats_default : all_typerecs_simple (@default term _). +Proof. vm_compute. tauto. Qed. + +Lemma ats_combine (args : list string) (l : list term) + : all all_typerecs_simple l -> + all (fun p => all_typerecs_simple (snd p)) (combine_r_padded args l). +Proof. + revert l; induction args as [|a args IH]; intros [|x l]; cbn; try tauto. + - intros _. split; [ apply ats_default | apply IH; exact I ]. + - intros [Hx Hl]. split; [ exact Hx | apply IH; exact Hl ]. +Qed. + +Lemma all_map A B (Q : B -> Prop) (f : A -> B) l + : all (fun x => Q (f x)) l -> all Q (map f l). +Proof. induction l; cbn; tauto. Qed. + +Lemma pargs_all (Q : term -> Prop) (c' : ctx) (s : list term) + : WfCutElim.P_args string (fun e (_ : sort) => Q e) s c' -> all Q s. +Proof. + revert s; induction c' as [| [n t] c' IH]; intros [|e s]; cbn; try tauto. + intros [H1 H2]; split; [ exact H2 | apply IH; exact H1 ]. +Qed. + +(* The reflective statement about the compiler: outside the two boundary + cases, no compiler case emits a [#"typerec"] at all. *) +Definition cmp_case_ok (p : string * @compiler_case string term sort) : bool := + match p with + | (n, term_case _ b) => + typerecs_are_var b + && (inb n ["dtt";"ttd"] || match typerec_mu_vars b with [] => true | _ => false end) + | _ => true + end. + +Lemma cmp_cases_ok : forallb cmp_case_ok CMP = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma compile_star : compile CMP (con "*" []) = {{e #"*" #"ty_emp" }}. +Proof. reflexivity. Qed. +Lemma compile_bool : compile CMP (con "bool" []) = {{e #"bool" #"ty_emp" }}. +Proof. reflexivity. Qed. +Lemma compile_arrow a b + : compile CMP (con "->" [b;a]) = con "->" [compile CMP b; compile CMP a; con "ty_emp" []]. +Proof. reflexivity. Qed. +Lemma compile_dtt s + : compile CMP (con "dtt" s) + = dtt_case_tgt[/combine_r_padded ["e";"A";"G"] (map (compile CMP) s)/]. +Proof. reflexivity. Qed. +Lemma compile_ttd s + : compile CMP (con "ttd" s) + = ttd_case_tgt[/combine_r_padded ["e";"A";"G"] (map (compile CMP) s)/]. +Proof. reflexivity. Qed. +Lemma lookup_A (a b c : term) + : term_subst_lookup (combine_r_padded ["e";"A";"G"] [a;b;c]) "A" = b. +Proof. reflexivity. Qed. + +Lemma sml_all_fresh : all_fresh source_multilanguage. +Proof. compute_all_fresh. Qed. + +Lemma sml_lookup n (r:rule) + : In (n,r) source_multilanguage -> named_list_lookup_err source_multilanguage n = Some r. +Proof. apply (in_lang_lookup source_multilanguage n r sml_all_fresh). Qed. + +Definition rule_ty_name_ok (p : string * rule) : bool := + match p with + | (n, term_rule _ _ (scon "ty" [])) => inb n ["*";"bool";"->"] + | _ => true + end. + +Lemma sml_ty_names : forallb rule_ty_name_ok source_multilanguage = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma sml_ty_rule_name : forall n c' args, + In (n, term_rule c' args (scon "ty" [])) source_multilanguage -> + n = "*" \/ n = "bool" \/ n = "->". +Proof. + intros n c' args Hin. + pose proof sml_ty_names as Hb. + rewrite forallb_forall in Hb. + specialize (Hb _ Hin). + cbv beta iota delta [rule_ty_name_ok] in Hb. + apply Is_true_eq_left in Hb. + autorewrite with utils in Hb. cbn in Hb. + intuition (subst; auto). +Qed. + Lemma no_sort_eqns_in_sml : Is_true (no_sort_eqns source_multilanguage). Proof. apply I. Qed. -Lemma source_multilanguage_wf : wf_lang source_multilanguage. -Proof. prove_by_lang_db. Qed. -#[local] Definition source_multilanguage_entry := - lang_entry source_multilanguage_wf. -#[export] Hint Resolve source_multilanguage_entry : wf_lang_db. +(* [source_multilanguage_wf] is proved in TypeCasing.v. *) Lemma ty_eq_sort_lemma : forall (t : sort), Core.wf_sort source_multilanguage [] t -> eq_sort source_multilanguage [] t {{s #"ty"}} <-> t = {{s #"ty" }}. Proof. @@ -128,7 +416,7 @@ Proof. | solve [ apply conj; intros; inversion H0; rewrite <- H7 in H1; inversion H1; [ reflexivity | pose proof source_multilanguage_wf; sort_cong ] ] ] - | .. ]); + | .. ]); destruct H0. Qed. @@ -136,22 +424,18 @@ Lemma ty_inversion_lemma' : forall (t : sort) (e : term), Core.wf_sort source_multilanguage [] t -> Core.wf_term source_multilanguage [] e t -> t = {{s #"ty" }} -> e = {{e #"*" }} \/ e = {{e #"bool" }} \/ (exists a b, Core.wf_term source_multilanguage [] a {{s #"ty" }} /\ Core.wf_term source_multilanguage [] b {{s #"ty" }} /\ e = {{e #"->" {a} {b} }} ). Proof. induction 2 using wf_term_cut_ind. - - unshelve (repeat (destruct H0; - [> first [ solve [ injection H0; intros HF; inversion HF ] - | solve [ inversion H0; intros Ht; inversion Ht ] - | shelve ] | .. ]); destruct H0). - + inversion H0; intros Ht; rewrite <- H5 in H1; repeat invert_wf_args. eauto. - + inversion H0; intros Ht; rewrite <- H5 in H1; repeat invert_wf_args. eauto. - + inversion H0; intros Ht; rewrite <- H5 in H1; repeat invert_wf_args. - rewrite <- H5 in H2; subst; destruct H2; repeat destruct H1. - right. right. eauto. - - inversion H0. + - intro Ht. apply subst_sort_name_nil in Ht; subst t. + destruct (sml_ty_rule_name H0) as [-> | [-> | ->]]; + apply sml_lookup in H0; vm_compute in H0; + injection H0; intros; subst. + all: repeat invert_wf_args; subst; eauto 10. + - destruct H0. - intros Ht; rewrite Ht in H1. - apply IHwf_term. + apply IHwf_term. + rewrite <- Ht in H1. apply eq_sort_sym in H1. apply ty_eq_sort_lemma in Ht; - [ eapply (eq_sort_wf_r source_multilanguage_wf wf_ctx_nil); apply H1 | apply H ]. + [ eapply (eq_sort_wf_r source_multilanguage_wf wf_ctx_nil); apply H1 | apply H ]. + apply ty_eq_sort_lemma; - [ eapply (eq_sort_wf_l source_multilanguage_wf wf_ctx_nil); apply H1 | apply H1 ]. + [ eapply (eq_sort_wf_l source_multilanguage_wf wf_ctx_nil); apply H1 | apply H1 ]. Qed. Lemma ty_inversion_lemma : forall (e : term), @@ -159,7 +443,7 @@ Lemma ty_inversion_lemma : forall (e : term), Proof. intros. eapply ty_inversion_lemma'. - assert (Core.wf_sort source_multilanguage {{c }} {{s #"ty" }}); - [ pose proof source_multilanguage_wf; compute_sort_wf | apply H0 ]. + [ pose proof source_multilanguage_wf; compute_sort_wf | apply H0 ]. - apply H. - reflexivity. Qed. @@ -170,57 +454,76 @@ Lemma compiled_types_are_simple : is_simple_type (compile (simple_multilang_compiler ++ interoperating_langs_compiler) e). Proof. induction 1 using wf_term_cut_ind. - - unshelve (repeat (destruct H; - [> first [ solve [ injection H; intros HF; inversion HF ] - | solve [ inversion H; intros Ht; inversion Ht ] - | shelve ] | .. ]); destruct H). - + inversion H; intros Ht; rewrite <- H4 in H0; repeat invert_wf_args; vm_compute; apply I. - + inversion H; intros Ht; rewrite <- H4 in H0; repeat invert_wf_args; vm_compute; apply I. - + inversion H. intros Ht. rewrite <- H4 in H0. repeat invert_wf_args. subst. destruct H1; repeat destruct H0. simpl in Ht. - cbv [apply_subst] in H2; simpl in H2; cbv [apply_subst] in H1; simpl in H1. - apply H1 in Ht. - assert (Ht2 : {{s #"ty"}} = {{s #"ty"}}) by reflexivity. - apply H2 in Ht2. - simpl. apply conj; assumption. - - inversion H. + - intro Ht. apply subst_sort_name_nil in Ht; subst t. + destruct (sml_ty_rule_name H) as [-> | [-> | ->]]; + apply sml_lookup in H; vm_compute in H; + injection H; intros; subst; repeat invert_wf_args; subst. + + rewrite compile_star; exact eq_refl. + + rewrite compile_bool; exact eq_refl. + + rewrite compile_arrow. + cbv [is_simple_type]; cbn [simple_type_at]; + cbn [WfCutElim.P_args] in H1; destruct H1 as [[_ Pe0] Pe]; + split; [ reflexivity | split; [ apply Pe0 | apply Pe ]; reflexivity ]. + - destruct H. - intros Ht; rewrite Ht in H0. apply ty_eq_sort_lemma in H0. + apply IHwf_term in H0. apply H0. + eapply (eq_sort_wf_l source_multilanguage_wf wf_ctx_nil). apply H0. Qed. -Ltac compute_match t := - let v := eval vm_compute in t in - change_no_check t with v. - +(* Every [#"typerec"] in the image of the compiler has a simple type + argument. *) Theorem can_eliminate_typerec : forall (t: sort) (e : term), Core.wf_term source_multilanguage [] e t -> - all_typerecs_simple (compile (simple_multilang_compiler ++ interoperating_langs_compiler) e). + all_typerecs_simple (compile (simple_multilang_compiler ++ interoperating_langs_compiler) e). Proof. induction 1 using wf_term_cut_ind. - - unshelve (repeat (destruct H; - [> first [ solve [ injection H; intros HF; inversion HF ] - | injection H; intros H6 H5 H4 H3; rewrite <- H4 in H1; rewrite <- H4 in H0; cbn [compile]; compute_match (named_list_lookup_err (simple_multilang_compiler ++ interoperating_langs_compiler) name); rewrite <- H3; repeat invert_wf_args; subst; destruct H1; repeat destruct H0; cbn [map combine_r_padded] ] - | .. ]); destruct H). - 1-2: simpl in H14; apply ty_inversion_lemma in H14; try reflexivity; - destruct H14 as [ HStar | [ HBool | HArrow ]]; - [ rewrite HStar; replace (compile (simple_multilang_compiler ++ interoperating_langs_compiler) {{e #"*"}}) with {{e #"*" #"ty_emp" }} by (vm_compute; reflexivity); cbn -[compile simple_multilang_compiler interoperating_langs_compiler]; repeat apply conj; apply I || assumption - | rewrite HBool; replace (compile (simple_multilang_compiler ++ interoperating_langs_compiler) {{e #"bool"}}) with {{e #"bool" #"ty_emp" }} by (vm_compute; reflexivity); cbn -[compile simple_multilang_compiler interoperating_langs_compiler]; repeat apply conj; apply I || assumption - | destruct HArrow as [ A [ B [ WfA [ WfB EAB ]]]]; cbn -[compile simple_multilang_compiler interoperating_langs_compiler]; apply compiled_types_are_simple in WfA; try reflexivity; apply compiled_types_are_simple in WfB; try reflexivity; repeat apply conj; try (apply I || assumption || rewrite EAB; apply conj; assumption) ]. - all: repeat apply conj; try assumption; apply I. Unshelve. - - inversion H. + - destruct (inb name ["dtt";"ttd"]) eqn:Hd. + 2:{ (* generic case: the compiler image of this rule has no #"typerec" *) + cbn [compile]. + destruct (named_list_lookup_err CMP name) as [[cargs b|cargs t0]|] eqn:Hl. + 2,3: apply ats_default. + assert (Hin : In (name, term_case cargs b) CMP) + by (apply named_list_lookup_err_in; symmetry; exact Hl). + pose proof cmp_cases_ok as Hb; rewrite forallb_forall in Hb; specialize (Hb _ Hin). + cbv [cmp_case_ok] in Hb. + apply andb_prop in Hb; destruct Hb as [Hvar Hmu]. + apply ats_subst. + + apply Is_true_eq_left; exact Hvar. + + apply ats_combine, all_map. eapply pargs_all; exact H1. + + rewrite Hd in Hmu; cbn in Hmu. + destruct (typerec_mu_vars b); [ exact I | discriminate ]. } + { (* the two boundary cases: the #"typerec" type argument is the + compiled source type, which is simple by compiled_types_are_simple *) + apply Is_true_eq_left in Hd; autorewrite with utils in Hd; cbn in Hd. + destruct Hd as [ Hd | [Hd | []]]; subst name. + all: apply sml_lookup in H; vm_compute in H; injection H; intros; subst. + all: repeat invert_wf_args; subst. + all: [> rewrite compile_dtt | rewrite compile_ttd ]. + all: apply ats_subst; + [ vm_compute; exact I + | apply ats_combine, all_map; eapply pargs_all; exact H1 + | ]. + all: cbn [map]. + all: match goal with |- all _ ?L => replace L with ["A"] by (vm_compute; reflexivity) end. + all: cbn [all]; split; [ | exact I ]. + all: rewrite lookup_A. + all: eapply compiled_types_are_simple; [ apply H10 | reflexivity ]. } + - destruct H. - apply IHwf_term. Qed. -Lemma target_multilanguage_wf : wf_lang target_multilanguage. -Proof. prove_by_lang_db. Qed. +(* ------------------------------------------------------------------ *) +(* Inversion for the target language. *) +(* ------------------------------------------------------------------ *) +(* [target_multilanguage_wf] is proved in TypeCasing.v. *) Lemma no_sort_eqns_in_tml : Is_true (no_sort_eqns target_multilanguage). Proof. apply I. Qed. Lemma ty_env_eq_sort_lemma_tml : forall (t : sort), Core.wf_sort target_multilanguage [] t -> eq_sort target_multilanguage [] t {{s #"ty_env"}} <-> t = {{s #"ty_env" }}. Proof. - intros t H. inversion H. vm_compute in H0. + intros t H. inversion H. vm_compute in H0. repeat (simpl in H0; destruct H0; [> first [ solve [ injection H0; intros HF; inversion HF ] | solve [ apply conj; inversion H0; intros; @@ -229,115 +532,453 @@ Proof. | solve [ apply conj; intros; inversion H0; rewrite <- H7 in H1; inversion H1; [ reflexivity | pose proof target_multilanguage_wf; sort_cong ] ] ] - | .. ]); + | .. ]); destruct H0. Qed. -Lemma ty_inversion_lemma_tml : forall (e ty_env : term), - Core.wf_term target_multilanguage [] e {{s #"ty" {ty_env} }} -> e = {{e #"*" {ty_env} }} \/ e = {{e #"bool" {ty_env} }} \/ (exists a b, Core.wf_term source_multilanguage [] a {{s #"ty" {ty_env} }} /\ Core.wf_term source_multilanguage [] b {{s #"ty" {ty_env} }} /\ e = {{e #"->" {ty_env} {a} {b} }} ). -Proof. Admitted. (* STATEMENT IS NOT RIGHT!! product types and All types *) +(* The seven term rules of [target_multilanguage] whose result sort is + [#"ty" _] are, by computation: + "prod", "*", "bool", "->", "All", "ty_hd", "ty_subst". + Note that the type-environment argument of the head constructor need not be + syntactically the [D] of the ascribed sort: [target_multilanguage] has no + sort equations, so a conversion step only tells us the two sorts have the + same *name*, not the same arguments. Hence every type-environment argument + is existentially quantified. [#"ty_hd"] is listed even though it cannot + occur at [D = #"ty_emp"]: at a general [D] it is a legitimate closed term of + sort [#"ty" (#"ty_ext" D')]. *) +Lemma tml_all_fresh : all_fresh target_multilanguage. +Proof. compute_all_fresh. Qed. -(* -(* OLD. Doesn't work for typerec because we don't have the inversion lemma and we have stuck terms with typerec *) -Theorem partial_eval_preserves_equality : - forall (t : sort) (e : term), +Lemma tml_lookup n (r:rule) + : In (n,r) target_multilanguage -> named_list_lookup_err target_multilanguage n = Some r. +Proof. apply (in_lang_lookup target_multilanguage n r tml_all_fresh). Qed. + +Definition tml_rule_ty_name_ok (p : string * rule) : bool := + match p with + | (n, term_rule _ _ (scon sn _)) => + if eqb sn "ty" + then inb n ["prod";"*";"bool";"->";"All";"ty_hd";"ty_subst"] + else true + | _ => true + end. + +Lemma tml_ty_names : forallb tml_rule_ty_name_ok target_multilanguage = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma tml_ty_rule_name : forall n c' args t, + In (n, term_rule c' args t) target_multilanguage -> + Parameterizer.sort_name t = "ty" -> + In n ["prod";"*";"bool";"->";"All";"ty_hd";"ty_subst"]. +Proof. + intros n c' args [sn sargs] Hin Hsn; cbn in Hsn; subst sn. + pose proof tml_ty_names as Hb. + rewrite forallb_forall in Hb. + specialize (Hb _ Hin). + apply Is_true_eq_left in Hb. + assert (Hb' : Is_true (inb n ["prod";"*";"bool";"->";"All";"ty_hd";"ty_subst"])) + by exact Hb. + autorewrite with utils in Hb'. exact Hb'. +Qed. + +(* Generalized over the sort's arguments: [target_multilanguage] has no sort + equations, so the conversion case of the cut-free induction only preserves + the sort *name*. *) +Lemma ty_inversion_lemma_tml' : forall (t : sort) (e : term), Core.wf_term target_multilanguage [] e t -> - (* would need to say there are _no_ typerecs at all. that's a bit strong for what I had in mind. *) - Core.eq_term target_multilanguage [] t e (elim_typerec e). + Parameterizer.sort_name t = "ty" -> + (exists D, e = {{e #"*" {D} }}) + \/ (exists D, e = {{e #"bool" {D} }}) + \/ (exists D a b, e = {{e #"->" {D} {a} {b} }}) + \/ (exists D a b, e = {{e #"prod" {D} {a} {b} }}) + \/ (exists D a, e = {{e #"All" {D} {a} }}) + \/ (exists D, e = {{e #"ty_hd" {D} }}) + \/ (exists D D' g a, e = {{e #"ty_subst" {D} {D'} {g} {a} }}). Proof. induction 1 using wf_term_cut_ind. - - vm_compute in H. pose proof target_multilanguage_wf as tml_wf. - unshelve (repeat (destruct H; - [> first [ solve [ injection H; intros HF; inversion HF ] - | inversion H; rewrite <- H4 in H0; repeat invert_wf_args; - subst; destruct H1; repeat destruct H0; - setup_eq_terms; repeat eq_term_and_sort_solver ] - | .. ]); destruct H). - + (* we need a type inversion lemma! *) admit. - - inversion H. - - eq_term_and_sort_solver. -Admitted. - *) - -(* Ltac compile_on := Transparent compile; Transparent simple_multilang_compiler; Transparent interoperating_langs_compiler. *) - -(* Ltac compile_off := Opaque compile; Opaque simple_multilang_compiler; Opaque interoperating_langs_compiler. *) - - -Ltac do_substitutions := simpl; cbv [term_subst_lookup named_list_lookup]; simpl. -Ltac setup_eq_terms := - cbn [elim_typerec map]; do_substitutions; simpl in *; cbv [term_subst_lookup named_list_lookup] in *; simpl in *. -Ltac crush_eqs := do_substitutions; eauto using eq_term_conv. -Ltac sv := - match goal with - | |- eq_term _ _ _ (con "typerec" _) _ => shelve - | |- eq_term _ _ _ (con ?s _) (con ?s _) => term_cong; crush_eqs - | |- eq_sort _ _ (scon ?s _) (scon ?s _) => sort_cong; crush_eqs - | |- _ \/ _ => left - | |- _ => eapply eq_term_conv; crush_eqs - end. + - intro Hsn. + assert (Hsn' : Parameterizer.sort_name t = "ty") + by (destruct t; exact Hsn). + pose proof (tml_ty_rule_name H Hsn') as Hn. + cbn in Hn. + repeat (destruct Hn as [Hn | Hn]; [ subst name | ]); [ | | | | | | | destruct Hn ]. + all: apply tml_lookup in H; vm_compute in H; injection H; intros; subst. + all: repeat invert_wf_args; subst. + all: eauto 12. + - destruct H. + - intro Hsn. apply IHwf_term. + apply (sort_names_equal target_multilanguage_wf no_sort_eqns_in_tml wf_ctx_nil) in H0. + rewrite H0; exact Hsn. +Qed. -Ltac contains_var t := - first - [ is_var t - | lazymatch t with - | con ?n ?s => - first [ contains_var n | contains_var s ] - | scon ?n ?s => - first [ contains_var n | contains_var s ] - | cons ?n ?s => - first [ contains_var n | contains_var s ] - end - ]. - -Ltac act_depending_on_var e := - tryif contains_var e then - idtac - (* let x := fresh "c" in set (x := compile (simple_multilang_compiler ++ interoperating_langs_compiler) e) in * *) - else - vm_compute in e. - -Ltac generalize_compiles := - repeat match goal with - | H : context[compile (simple_multilang_compiler ++ interoperating_langs_compiler) ?e] |- _ => act_depending_on_var e - end. +Lemma ty_inversion_lemma_tml : forall (e ty_env : term), + Core.wf_term target_multilanguage [] e {{s #"ty" {ty_env} }} -> + (exists D, e = {{e #"*" {D} }}) + \/ (exists D, e = {{e #"bool" {D} }}) + \/ (exists D a b, e = {{e #"->" {D} {a} {b} }}) + \/ (exists D a b, e = {{e #"prod" {D} {a} {b} }}) + \/ (exists D a, e = {{e #"All" {D} {a} }}) + \/ (exists D, e = {{e #"ty_hd" {D} }}) + \/ (exists D D' g a, e = {{e #"ty_subst" {D} {D'} {g} {a} }}). +Proof. + intros e ty_env H. eapply ty_inversion_lemma_tml'; [ exact H | reflexivity ]. +Qed. -Ltac collapse_match := +(* ------------------------------------------------------------------ *) +(* Metatheory of [elim_typerec]: it is an equality in the target. *) +(* *) +(* [Implicit Arguments] is off in this block: the lemmas below are *) +(* applied with positional arguments. *) +(* ------------------------------------------------------------------ *) +Unset Implicit Arguments. +Local Notation wf_ctx' c := (@Model.wf_ctx _ _ _ (core_model target_multilanguage) c). +Local Notation wf_subst' s c := (@Model.wf_subst _ _ _ (core_model target_multilanguage) [] s c). +Local Notation wf_args' s c := (@Model.wf_args _ _ _ (core_model target_multilanguage) [] s c). +Local Notation eq_subst' c s1 s2 := (@Model.eq_subst _ _ _ (core_model target_multilanguage) [] c s1 s2). +Local Notation eq_args' c s1 s2 := (@Model.eq_args _ _ _ (core_model target_multilanguage) [] c s1 s2). + +Ltac to_core := cbv beta iota zeta delta [Model.wf_term Model.eq_term core_model] in *. +Ltac norm_sort_goal := + to_core; + match goal with + | |- Core.wf_term ?l ?c ?e ?T => let T' := eval vm_compute in T in change (Core.wf_term l c e T') + | |- Core.eq_term ?l ?c ?T ?A ?B => + let T' := eval vm_compute in T in + let A' := eval vm_compute in A in + let B' := eval vm_compute in B in change (Core.eq_term l c T' A' B') + end. +Ltac norm_sort_only := + to_core; match goal with - | |- context[match ?t with _ => _ end] => - let t' := eval vm_compute in t in - change t with t'; compute_match t' + | |- Core.wf_term ?l ?c ?e ?T => let T' := eval vm_compute in T in change (Core.wf_term l c e T') + | |- Core.eq_term ?l ?c ?T ?A ?B => let T' := eval vm_compute in T in change (Core.eq_term l c T' A B) end. -Ltac collapse_match_in H := - cbv [compile_sort] in H; +Ltac norm_wf_hyp H := + to_core; match type of H with - | context[match ?t with _ => _ end] => - let t' := eval vm_compute in t in - change t with t' in H + | Core.wf_term ?l ?c ?e ?T => let T' := eval vm_compute in T in change (Core.wf_term l c e T') in H end. -Ltac collapse_match_in_hyps := - repeat match goal with - | H : eq_term _ _ _ _ _ |- _ => - progress (repeat collapse_match_in H; cbv iota in H; cbv [map combine_r_padded] in H) - | _ => idtac - end. +Ltac norm_eq_hyp H := + match type of H with + | Core.eq_term ?l ?c ?T ?A ?B => + let T' := eval vm_compute in T in + let A' := eval vm_compute in A in + let B' := eval vm_compute in B in + change (Core.eq_term l c T' A' B') in H + end. -Ltac remove_compile_sorts := - cbv [compile_sort]; repeat collapse_match; collapse_match_in_hyps. -Ltac setup_eq_goal H H0 H1 name := - injection H; intros Hsort Hargs H4 Hname; rewrite <- H4 in H0; cbn [compile]; - compute_match (named_list_lookup_err (simple_multilang_compiler ++ interoperating_langs_compiler) name); rewrite <- Hname; - repeat invert_wf_args; subst; destruct H1; repeat destruct H0; - remove_compile_sorts; cbv [map combine_r_padded]. +Lemma R_star_lookup : named_list_lookup_err target_multilanguage "typerec star" + = Some (term_eq_rule R_star_c (snd (fst (fst R_star))) (snd (fst R_star)) (snd R_star)). +Proof. vm_compute. reflexivity. Qed. +Lemma R_bool_lookup : named_list_lookup_err target_multilanguage "typerec bool" + = Some (term_eq_rule R_bool_c (snd (fst (fst R_bool))) (snd (fst R_bool)) (snd R_bool)). +Proof. vm_compute. reflexivity. Qed. +Lemma R_func_lookup : named_list_lookup_err target_multilanguage "typerec func" + = Some (term_eq_rule R_func_c (snd (fst (fst R_func))) R_func_r R_func_t). +Proof. vm_compute. reflexivity. Qed. + +Lemma tml_eq_rule_ctx_wf name c' e1 e2 t : + In (name, term_eq_rule c' e1 e2 t) target_multilanguage -> wf_ctx' c'. +Proof. + intro Hin. pose proof (rule_in_wf _ _ target_multilanguage_wf Hin) as Hr. + rewrite app_nil_r in Hr. inversion Hr; subst; assumption. +Qed. -Ltac first_pass := - do_substitutions; simpl in *; cbv [term_subst_lookup named_list_lookup_err] in *; simpl in *; sv; sv; sv; sv. +Lemma eq_by_rule (name : string) (c' : ctx) (t:sort) e1 e2 (s : subst) + : named_list_lookup_err target_multilanguage name = Some (term_eq_rule c' e1 e2 t) -> + wf_subst' s c' -> + Core.eq_term target_multilanguage [] t[/s/] e1[/s/] e2[/s/]. +Proof. + intros Hl Hs. + assert (In (name, term_eq_rule c' e1 e2 t) target_multilanguage) + by (apply named_list_lookup_err_in; symmetry; exact Hl). + eapply eq_term_subst. + - eapply eq_term_by; eauto. + - apply eq_subst_refl; exact Hs. + - eapply tml_eq_rule_ctx_wf; eauto. +Qed. + +Lemma wf_by_rule (name : string) (c' : ctx) (t:sort) args (s : list term) + : named_list_lookup_err target_multilanguage name = Some (term_rule c' args t) -> + wf_args' s c' -> + Core.wf_term target_multilanguage [] (con name s) t[/with_names_from c' s/]. +Proof. + intros Hl Hs. eapply wf_term_by; [ | exact Hs ]. + apply named_list_lookup_err_in; symmetry; exact Hl. +Qed. + + +Lemma simple_type_wf D (HD : Core.wf_term target_multilanguage [] D {{s #"ty_env"}}) + : forall mu, simple_type_at D mu -> Core.wf_term target_multilanguage [] mu {{s #"ty" {D} }}. +Proof. + induction mu using term_ind_all; [ intros [] | ]. + cbn [simple_type_at]. intro Hs. + pose proof (eqb_spec n "*") as Hn1; destruct (eqb n "*"); [ subst n | ]. + { destruct l as [|D' [|? ?]]; try contradiction. cbn in Hs. subst D'. + pose proof (wf_by_rule "*" [("D", {{s #"ty_env"}})] {{s #"ty" "D"}} [] [D] + ltac:(vm_compute; reflexivity)) as Hb. + norm_sort_goal. apply Hb. to_core. + econstructor; [ norm_sort_goal; exact HD | econstructor ]. } + pose proof (eqb_spec n "bool") as Hn2; destruct (eqb n "bool"); [ subst n | ]. + { destruct l as [|D' [|? ?]]; try contradiction. cbn in Hs. subst D'. + pose proof (wf_by_rule "bool" [("D", {{s #"ty_env"}})] {{s #"ty" "D"}} [] [D] + ltac:(vm_compute; reflexivity)) as Hb. + norm_sort_goal. apply Hb. to_core. + econstructor; [ norm_sort_goal; exact HD | econstructor ]. } + pose proof (eqb_spec n "->") as Hn3; destruct (eqb n "->"); [ subst n | contradiction ]. + destruct l as [|t2 [|t1 [|D' [|? ?]]]]; try contradiction. + destruct Hs as [HD' [Hs1 Hs2]]. subst D'. + cbn [all] in H. destruct H as [IH2 [IH1 _]]. + pose proof (wf_by_rule "->" [("t'", {{s #"ty" "D"}});("t", {{s #"ty" "D"}});("D", {{s #"ty_env"}})] + {{s #"ty" "D"}} ["t'";"t"] [t2;t1;D] + ltac:(vm_compute; reflexivity)) as Hb. + norm_sort_goal. apply Hb. to_core. + econstructor; [ norm_sort_goal; apply IH2; exact Hs2 | ]. + econstructor; [ norm_sort_goal; apply IH1; exact Hs1 | ]. + econstructor; [ norm_sort_goal; exact HD | econstructor ]. +Qed. + + +Lemma meta_typerec_arrow D G sigma X t1 t2 e1 e2 e3 + : meta_typerec D G (con "->" [t2;t1;X]) sigma e1 e2 e3 + = MT_func D G sigma t1 t2 (meta_typerec D G t1 sigma e1 e2 e3) + (meta_typerec D G t2 sigma e1 e2 e3) e3. +Proof. reflexivity. Qed. + + +Section TyperecElim. + Context (D G sigma v1 v2 v3 : term) + (HD : Core.wf_term target_multilanguage [] D {{s #"ty_env"}}) + (HG : Core.wf_term target_multilanguage [] G {{s #"env" {D} }}) + (Hsig : Core.wf_term target_multilanguage [] sigma {{s #"ty" (#"ty_ext" {D}) }}) + (Hv1 : Core.wf_term target_multilanguage [] v1 (Sgt D G sigma {{e #"*" {D} }})) + (Hv2 : Core.wf_term target_multilanguage [] v2 (Sgt D G sigma {{e #"bool" {D} }})) + (Hv3 : Core.wf_term target_multilanguage [] v3 ((named_list_lookup default R_func_c "v3") + [/[("sigma",sigma);("G",G);("D",D)]/])). + + Ltac wf_solve := norm_sort_goal; cbv [Sgt] in *; assumption. + + Lemma base_subst_wf : wf_subst' [("v3",v3);("v2",v2);("v1",v1);("sigma",sigma);("G",G);("D",D)] R_star_c. + Proof. + cbv [R_star_c]. repeat apply Model.wf_subst_cons. + all: try apply Model.wf_subst_nil. + all: wf_solve. + Qed. + + Lemma base_subst_wf_b : wf_subst' [("v3",v3);("v2",v2);("v1",v1);("sigma",sigma);("G",G);("D",D)] R_bool_c. + Proof. + cbv [R_bool_c]. repeat apply Model.wf_subst_cons. + all: try apply Model.wf_subst_nil. + all: wf_solve. + Qed. + + Lemma func_subst_wf t1 t2 + (Ht1 : Core.wf_term target_multilanguage [] t1 {{s #"ty" {D} }}) + (Ht2 : Core.wf_term target_multilanguage [] t2 {{s #"ty" {D} }}) + : wf_subst' [("v3",v3);("v2",v2);("v1",v1);("t2",t2);("t1",t1);("sigma",sigma);("G",G);("D",D)] R_func_c. + Proof. + cbv [R_func_c]. repeat apply Model.wf_subst_cons. + all: try apply Model.wf_subst_nil. + all: wf_solve. + Qed. + + Theorem typerec_elim_eq : forall mu, simple_type_at D mu -> + Core.eq_term target_multilanguage [] (Sgt D G sigma mu) + (con "typerec" [v3;v2;v1;sigma;mu;G;D]) + (meta_typerec D G mu sigma v1 v2 v3). + Proof. + induction mu using term_ind_all; [ intros [] | ]. + cbn [simple_type_at]. intro Hs. + pose proof (eqb_spec n "*") as Hn1; destruct (eqb n "*"); [ subst n | ]. + { destruct l as [|D' [|? ?]]; try contradiction. cbn in Hs; subst D'. + pose proof (eq_by_rule _ _ _ _ _ _ R_star_lookup base_subst_wf) as Hq. + norm_eq_hyp Hq. cbv [Sgt meta_typerec]. exact Hq. } + pose proof (eqb_spec n "bool") as Hn2; destruct (eqb n "bool"); [ subst n | ]. + { destruct l as [|D' [|? ?]]; try contradiction. cbn in Hs; subst D'. + pose proof (eq_by_rule _ _ _ _ _ _ R_bool_lookup base_subst_wf_b) as Hq. + norm_eq_hyp Hq. cbv [Sgt meta_typerec]. exact Hq. } + pose proof (eqb_spec n "->") as Hn3; destruct (eqb n "->"); [ subst n | contradiction ]. + destruct l as [|t2 [|t1 [|D' [|? ?]]]]; try contradiction. + destruct Hs as [HD' [Hs1 Hs2]]; subst D'. + cbn [all] in H; destruct H as [IH2 [IH1 _]]. + assert (Ht1 : Core.wf_term target_multilanguage [] t1 {{s #"ty" {D} }}) + by (apply (simple_type_wf D HD); exact Hs1). + assert (Ht2 : Core.wf_term target_multilanguage [] t2 {{s #"ty" {D} }}) + by (apply (simple_type_wf D HD); exact Hs2). + pose proof (eq_by_rule _ _ _ _ _ _ R_func_lookup (func_subst_wf t1 t2 Ht1 Ht2)) as Hq. + norm_eq_hyp Hq. + rewrite meta_typerec_arrow. + eapply eq_term_trans; [ | ]. + 2:{ (* fpe2[/sa/] = fpe2[/sb/] *) + pose proof (eq_term_subst (l:=target_multilanguage) (c:=[]) (c':=fpe2_ctx) + (s1:=[("comp_t2", con "typerec" [v3;v2;v1;sigma;t2;G;D]); + ("comp_t1", con "typerec" [v3;v2;v1;sigma;t1;G;D]); + ("v3",v3);("t2",t2);("t1",t1);("sigma",sigma);("G",G);("D",D)]) + (s2:=[("comp_t2", meta_typerec D G t2 sigma v1 v2 v3); + ("comp_t1", meta_typerec D G t1 sigma v1 v2 v3); + ("v3",v3);("t2",t2);("t1",t1);("sigma",sigma);("G",G);("D",D)]) + (t:=R_func_t) (e1:=fpe2) (e2:=fpe2)) as Hsub. + cbv [MT_func]. + apply Hsub; [ apply eq_term_refl; apply fpe2_wf | | apply fpe2_ctx_wf ]. + cbv [fpe2_ctx]. repeat apply Model.eq_subst_cons. + all: try apply Model.eq_subst_nil. + all: to_core. + all: try (norm_sort_only; solve [ apply eq_term_refl; cbv [Sgt] in *; assumption ]). + all: norm_sort_only. + - cbv [Sgt] in IH1. apply IH1; exact Hs1. + - cbv [Sgt] in IH2. apply IH2; exact Hs2. } + exact Hq. + Qed. +End TyperecElim. + +Lemma eq_args_elim : forall c' s, + WfCutElim.P_args string + (fun e t => all_typerecs_simple e -> Core.eq_term target_multilanguage [] t e (elim_typerec e)) s c' -> + all all_typerecs_simple s -> + eq_args' c' (map elim_typerec s) s. +Proof. + induction c' as [|[n t] c' IH]; intros [|e s]; cbn [WfCutElim.P_args map all]; try tauto. + - intros _ _. apply Model.eq_args_nil. + - intros [Hp Hpe] [Ha Has]. apply Model.eq_args_cons. + + apply IH; assumption. + + apply eq_term_sym. apply Hpe. exact Ha. +Qed. + +Lemma pargs_len : forall (P : term -> sort -> Prop) c' s, + WfCutElim.P_args string P s c' -> length s = length c'. +Proof. + induction c' as [|[n t] c' IH]; intros [|e s]; cbn [WfCutElim.P_args length]; try tauto. + intros [Hp _]; f_equal; apply IH; exact Hp. +Qed. -Ltac solve_eq_goal := - with_strategy opaque [compile simple_multilang_compiler interoperating_langs_compiler] first_pass; with_strategy transparent [compile simple_multilang_compiler interoperating_langs_compiler] simpl; repeat sv. +Lemma elim_typerec_con7 (D G mu sigma e1 e2 e3 : term) : + elim_typerec (con "typerec" [e3;e2;e1;sigma;mu;G;D]) + = meta_typerec D G mu sigma (elim_typerec e1) (elim_typerec e2) (elim_typerec e3). +Proof. reflexivity. Qed. + + +Theorem elim_typerec_eq : forall (t : sort) (e : term), + Core.wf_term target_multilanguage [] e t -> + all_typerecs_simple e -> + Core.eq_term target_multilanguage [] t e (elim_typerec e). +Proof. + induction 1 using wf_term_cut_ind. + - intro Hats. + pose proof (eqb_spec name "typerec") as Hn; destruct (eqb name "typerec") eqn:Hnb. + 2:{ + assert (Helim : elim_typerec (con name s) = con name (map elim_typerec s)) + by (cbn [elim_typerec]; rewrite Hnb; reflexivity). + rewrite Helim. apply eq_term_sym. + eapply term_con_congruence; + [ exact H | right; reflexivity | exact target_multilanguage_wf | ]. + apply eq_args_elim; [ exact H1 | ]. destruct Hats as [_ Hall]; exact Hall. } + subst name. assert (Hin := H). + apply tml_lookup in H. vm_compute in H. injection H as Hc' Hargs Ht. subst. + assert (Hlen : length s = 7) by (rewrite (pargs_len _ _ _ H1); reflexivity). + destruct s as [|e3 [|e2 [|e1 [|sg [|mu [|Gv [|Dv [|? ?]]]]]]]]; + cbn [length] in Hlen; try discriminate Hlen. + (destruct H1 as [[[[[[[_ IHD] IHG] IHmu] IHsg] IH1] IH2] IH3]). + (destruct Hats as [Hsimple [Ha3 [Ha2 [Ha1 [Hasg [Hamu [HaG [HaD _]]]]]]]]). + inversion H0 as [|? ? ? ? ? W3 H0a]; subst; clear H0. + inversion H0a as [|? ? ? ? ? W2 H0b]; subst; clear H0a. + inversion H0b as [|? ? ? ? ? W1 H0c]; subst; clear H0b. + inversion H0c as [|? ? ? ? ? Wsg H0d]; subst; clear H0c. + inversion H0d as [|? ? ? ? ? Wmu H0e]; subst; clear H0d. + inversion H0e as [|? ? ? ? ? WG H0f]; subst; clear H0e. + inversion H0f as [|? ? ? ? ? WD H0g]; subst; clear H0f. + norm_wf_hyp W3. norm_wf_hyp W2. norm_wf_hyp W1. + norm_wf_hyp Wsg. norm_wf_hyp Wmu. norm_wf_hyp WG. norm_wf_hyp WD. + assert (Hnil : wf_ctx' (@nil (string * sort))) by constructor. + rewrite elim_typerec_con7. + eapply eq_term_trans + with (e12 := con "typerec" [elim_typerec e3; elim_typerec e2; elim_typerec e1; sg; mu; Gv; Dv]). + { eapply term_con_congruence; + [ exact Hin | right; vm_compute; reflexivity | exact target_multilanguage_wf | ]. + repeat apply Model.eq_args_cons. + all: try apply Model.eq_args_nil. + all: try (norm_sort_only; solve [ apply eq_term_refl; assumption ]). + all: norm_sort_only. + - apply IH1; exact Ha1. + - apply IH2; exact Ha2. + - apply IH3; exact Ha3. } + assert (E1 : Core.wf_term target_multilanguage [] (elim_typerec e1) + (Sgt Dv Gv sg {{e #"*" {Dv} }})) + by (cbv [Sgt]; eapply eq_term_wf_r; + try typeclasses eauto; try exact target_multilanguage_wf; try exact Hnil; + norm_sort_only; apply IH1; exact Ha1). + assert (E2 : Core.wf_term target_multilanguage [] (elim_typerec e2) + (Sgt Dv Gv sg {{e #"bool" {Dv} }})) + by (cbv [Sgt]; eapply eq_term_wf_r; + try typeclasses eauto; try exact target_multilanguage_wf; try exact Hnil; + norm_sort_only; apply IH2; exact Ha2). + assert (E3 : Core.wf_term target_multilanguage [] (elim_typerec e3) + ((named_list_lookup default R_func_c "v3") + [/[("sigma",sg);("G",Gv);("D",Dv)]/])) + by (norm_sort_only; eapply eq_term_wf_r; + try typeclasses eauto; try exact target_multilanguage_wf; try exact Hnil; + norm_sort_only; apply IH3; exact Ha3). + norm_sort_only. + pose proof (typerec_elim_eq Dv Gv sg _ _ _ WD WG Wsg E1 E2 E3 mu Hsimple) as Hfin. + cbv [Sgt] in Hfin. exact Hfin. + - destruct H. + - intro Hats. eapply eq_term_conv; [ apply IHwf_term; exact Hats | exact H0 ]. +Qed. +Set Implicit Arguments. + + +Local Notation semantics_preserving tgt cmp := + (semantics_preserving (tgt_Model := core_model tgt) + (compile cmp) + (compile_sort cmp) + (compile_ctx cmp) + (compile_args cmp) + (compile_subst cmp)). + +(* ------------------------------------------------------------------ *) +(* Semantics preservation of the source-to-target compiler. *) +(* ------------------------------------------------------------------ *) + +(* The interoperation compiler, as a compiler into the full target with an + empty prefix. *) +Lemma interop_preserving_tml + : preserving_compiler_ext target_multilanguage [] + interoperating_langs_compiler simple_interoperating_langs. +Proof. + eapply preserving_compiler_embed. + 1: apply (elab_compiler_implies_preserving interoperating_langs_compiler_preserving). + compute_incl. +Qed. + +(* The whole simple-multilanguage compiler, with an empty prefix. *) +Lemma source_multilanguage_compiler_preserving + : preserving_compiler_ext target_multilanguage [] + (simple_multilang_compiler ++ interoperating_langs_compiler) + source_multilanguage. +Proof. + unfold source_multilanguage. + eapply compiler_append. + all: first [ typeclasses eauto + | apply simple_multilang_compiler_preserving + | apply interop_preserving_tml + | apply incl_refl + | compute_all_fresh + | apply source_multilanguage_wf ]. +Qed. + +Lemma sml_semantics_preserving + : semantics_preserving target_multilanguage + (simple_multilang_compiler ++ interoperating_langs_compiler) + source_multilanguage. +Proof. + apply inductive_implies_semantic; try typeclasses eauto; + eauto using ModelImpls.core_model_ok; try reflexivity. + 1: apply ModelImpls.core_model_ok; try typeclasses eauto. + 1: solve [prove_by_lang_db]. + 1: solve [prove_by_lang_db]. + apply source_multilanguage_compiler_preserving. +Qed. Lemma eq_sort_sml_implies_eq_sort_tml : forall (t t' : sort), @@ -345,12 +986,13 @@ Lemma eq_sort_sml_implies_eq_sort_tml : eq_sort target_multilanguage [] (compile_sort (simple_multilang_compiler ++ interoperating_langs_compiler) t) (compile_sort (simple_multilang_compiler ++ interoperating_langs_compiler) t'). -Proof. Admitted. - -(* Restore the old behavior because the new one broke this proof*) -Ltac compute_match t ::= - let v := eval vm_compute in t in - replace t with v by (vm_compute; reflexivity). +Proof. + intros t t' H. + pose proof (proj1 sml_semantics_preserving) as Hs. + unfold sort_eq_preserving_sem in Hs. + cbv beta iota zeta delta [core_model] in Hs. + apply (Hs []); eauto with lang_core utils. +Qed. Theorem partial_eval_preserves_equality : forall (t: sort) (e : term), @@ -361,34 +1003,433 @@ forall (t: sort) (e : term), (compile (simple_multilang_compiler ++ interoperating_langs_compiler) e) (elim_typerec (compile (simple_multilang_compiler ++ interoperating_langs_compiler) e)). Proof. - induction 1 using wf_term_cut_ind. - - vm_compute in H. pose proof target_multilanguage_wf as tml_wf. - unshelve (repeat (destruct H; - [> first [ solve [ injection H; intros HF; inversion HF ] - | shelve ] - | .. ]); destruct H). - 1-2: admit. - all: setup_eq_goal H H0 H1 name; solve_eq_goal. - - inversion H. - - apply eq_sort_sml_implies_eq_sort_tml in H0. sv. -Admitted. + intros t e H. + apply elim_typerec_eq. + - (* the compiled term is well-typed in the target *) + pose proof (proj1 (proj2 (proj2 (proj2 (proj2 sml_semantics_preserving))))) as Hw. + unfold term_wf_preserving_sem in Hw. + specialize (Hw [] e t H ltac:(constructor)). + cbv beta iota zeta delta [core_model] in Hw. + cbn [compile_ctx] in Hw. exact Hw. + - (* every typerec it contains has a simple type argument *) + eapply can_eliminate_typerec; exact H. +Qed. + +(* Well-typedness of the partially evaluated term, in the *full* target. + The sublanguage version ([partial_eval_wf_in_no_typerec_lang]) is proved + at the end of the file; it needs the conservativity argument below, so it + does not follow directly from this corollary. *) +Corollary partial_eval_wf_in_target : forall (t : sort) (e : term), + Core.wf_term target_multilanguage [] e t -> + all_typerecs_simple e -> + Core.wf_term target_multilanguage [] (elim_typerec e) t. +Proof. + intros t e H Hats. + eapply eq_term_wf_r; + try typeclasses eauto; + try exact target_multilanguage_wf; + try (constructor; fail); + apply elim_typerec_eq; assumption. +Qed. Definition target_multilanguage_without_typerec := - prod_ty_subst ++ prod_parameterized ++ (* can we also get rid of these? idt we partially evaluate that away but I think we could *) + boundary_cases ++ + let_eta_parameterized ++ let_ty_subst ++ let_parameterized ++ + (* [prod_ty_subst]/[prod_parameterized] are kept: they are not what the + partial evaluator removes, though in principle they could also be + eliminated. *) + prod_ty_subst ++ prod_parameterized ++ polymorphic_interoperating_langs. Lemma target_multilanguage_without_typerec_wf : wf_lang target_multilanguage_without_typerec. -Proof. prove_by_lang_db. Qed. +Proof. + unfold target_multilanguage_without_typerec. + apply wf_lang_concat; [ prove_by_lang_db | ]. + (* [boundary_cases] does not mention [#"typerec"], so it is still an + extension of the typerec-free target. *) + compute_wf_lang. +Qed. #[local] Definition target_multilanguage_without_typerec_entry := lang_entry target_multilanguage_without_typerec_wf. #[export] Hint Resolve target_multilanguage_without_typerec_entry : wf_lang_db. +(* The [all_typerecs_simple] hypothesis of the theorems below is necessary: + [elim_typerec] only removes a [#"typerec"] node whose type argument is a + *simple* type ([meta_typerec] falls through to [| _ => mu] otherwise), so a + term containing [#"typerec" D G "A" ...] at a type variable or at an + [#"All"] type is left unchanged, and still mentions [#"typerec"], which is + not a constructor of [target_multilanguage_without_typerec]. + + [partial_eval_wf_in_no_typerec_lang] and [compiled_partial_eval_wf] are + stated and proved at the end of the file. *) + +(* ================================================================== *) +(* Metatheory: the partially evaluated term lives in the typerec-free *) +(* sublanguage. *) +(* ================================================================== *) +(* ------------------------------------------------------------------ *) +(* [no_typerec]: a syntactic check that a term mentions no [#"typerec"] *) +(* ------------------------------------------------------------------ *) +Fixpoint no_typerec (e : term) : bool := + match e with + | var _ => true + | con n s => + negb (eqb n "typerec") + && (fix f (l : list term) : bool := + match l with [] => true | x::l' => no_typerec x && f l' end) s + end. + +Lemma no_typerec_unfold n s + : no_typerec (con n s) = negb (eqb n "typerec") && forallb no_typerec s. +Proof. + cbn [no_typerec]. f_equal; induction s; cbn; congruence. +Qed. + +Lemma forallb_of_all (f : term -> bool) l + : all (fun x => f x = true) l -> forallb f l = true. +Proof. induction l; cbn; [ reflexivity | ]. intros [H1 H2]. rewrite H1; auto. Qed. + +Lemma all_of_forallb (f : term -> bool) l + : forallb f l = true -> all (fun x => f x = true) l. +Proof. + induction l; cbn; [ tauto | ]. + intro H. apply andb_prop in H. destruct H. split; auto. +Qed. + +Lemma no_typerec_lookup (s : subst) n + : all (fun p => no_typerec (snd p) = true) s -> + no_typerec (term_subst_lookup s n) = true. +Proof. + induction s as [| [m e] s IH]; cbn; [ intros _; reflexivity | ]. + intros [He Hs]. cbv [term_subst_lookup] in *; cbn. + destruct (eqb n m); [ exact He | apply IH; exact Hs ]. +Qed. + +Lemma no_typerec_subst (b : term) (s : subst) + : no_typerec b = true -> + all (fun p => no_typerec (snd p) = true) s -> + no_typerec b[/s/] = true. +Proof. + revert s; induction b using term_ind_all; intros sub Hb Hs. + { cbn. apply no_typerec_lookup; exact Hs. } + rewrite no_typerec_unfold in Hb. apply andb_prop in Hb. destruct Hb as [Hn Hl]. + change ((con n l)[/sub/]) with (con n (map (term_subst sub) l)). + rewrite no_typerec_unfold, Hn; cbn [andb]. + apply forallb_of_all. apply all_map. + apply all_of_forallb in Hl. + clear Hn. revert Hl H. induction l as [|x l IHl]; cbn; [ tauto | ]. + intros [Hx Hl] [Hpx Hpl]. + split; [ apply Hpx; assumption | apply IHl; assumption ]. +Qed. + +(* ------------------------------------------------------------------ *) +(* Terms at "type-level" sorts contain no typerec *) +(* ------------------------------------------------------------------ *) +Definition strat_names : list string := ["ty_env";"env";"ty";"ty_sub"]. + +Definition strat_rule_ok (p : string * rule) : bool := + match snd p with + | term_rule c' _ t => + if inb (Parameterizer.sort_name t) strat_names + then negb (eqb (fst p) "typerec") + && forallb (fun q => inb (Parameterizer.sort_name (snd q)) strat_names) c' + else true + | _ => true + end. + +Lemma inb_string_true_iff (n : string) (l : list string) : inb n l = true <-> In n l. +Proof. + induction l as [|a l IH]; cbv [inb] in *; cbn [existsb In] in *. + { split; [ discriminate | tauto ]. } + pose proof (eqb_spec n a) as Hs; destruct (eqb n a). + { cbn [orb]. split; [ intros _; left; symmetry; exact Hs | intros _; reflexivity ]. } + cbn [orb]. rewrite IH. split; [ tauto | ]. + intros [He | He]; [ congruence | exact He ]. +Qed. + +Lemma strat_ok : forallb strat_rule_ok target_multilanguage = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma sort_name_subst (t : sort) (s : subst) + : Parameterizer.sort_name t[/s/] = Parameterizer.sort_name t. +Proof. destruct t; reflexivity. Qed. + +Lemma pargs_all_named (Q : term -> Prop) (R : string -> Prop) (c' : ctx) (s : list term) + : WfCutElim.P_args string (fun e t => R (Parameterizer.sort_name t) -> Q e) s c' -> + all (fun p => R (Parameterizer.sort_name (snd p))) c' -> + all Q s. +Proof. + revert s; induction c' as [| [n t] c' IH]; intros [|e s]; cbn; try tauto. + intros [H1 H2] [Hr Hrs]. split. + - apply H2. rewrite sort_name_subst. exact Hr. + - apply IH; assumption. +Qed. + +Lemma stratum_no_typerec : forall (e : term) (t : sort), + Core.wf_term target_multilanguage [] e t -> + In (Parameterizer.sort_name t) strat_names -> + no_typerec e = true. +Proof. + induction 1 using wf_term_cut_ind. + - rewrite sort_name_subst. intro Hn. + pose proof strat_ok as Hb. rewrite forallb_forall in Hb. + specialize (Hb _ H). cbn [strat_rule_ok fst snd] in Hb. + assert (Hin : inb (Parameterizer.sort_name t) strat_names = true) + by (apply inb_string_true_iff; exact Hn). + rewrite Hin in Hb. + apply andb_prop in Hb. destruct Hb as [Hnm Hc]. + rewrite no_typerec_unfold, Hnm. cbn [andb]. + apply forallb_of_all. + eapply pargs_all_named with (R := fun m => In m strat_names); [ exact H1 | ]. + rewrite forallb_forall in Hc. + clear - Hc. induction c' as [|p c' IH]; cbn [all]; [ exact I | ]. + split. + + apply inb_string_true_iff. apply Hc. left; reflexivity. + + apply IH. intros x Hx. apply Hc. right; exact Hx. + - destruct H. + - intro Hn. apply IHwf_term. + apply (sort_names_equal target_multilanguage_wf no_sort_eqns_in_tml wf_ctx_nil) in H0. + rewrite H0; exact Hn. +Qed. + +Ltac in_strat := vm_compute; repeat first [ left; reflexivity | right ]. + +Lemma simple_type_no_typerec (D : term) (HD : no_typerec D = true) + : forall mu, simple_type_at D mu -> no_typerec mu = true. +Proof. + induction mu using term_ind_all; [ intros [] | ]. + cbn [simple_type_at]. intro Hs. + rewrite no_typerec_unfold. + pose proof (eqb_spec n "*") as Hn1; destruct (eqb n "*"); [ subst n | ]. + { destruct l as [|D' [|? ?]]; try contradiction. cbn in Hs. subst D'. + cbn [forallb]. rewrite HD. reflexivity. } + pose proof (eqb_spec n "bool") as Hn2; destruct (eqb n "bool"); [ subst n | ]. + { destruct l as [|D' [|? ?]]; try contradiction. cbn in Hs. subst D'. + cbn [forallb]. rewrite HD. reflexivity. } + pose proof (eqb_spec n "->") as Hn3; destruct (eqb n "->"); [ subst n | ]. + { destruct l as [|t2 [|t1 [|D' [|? ?]]]]; try contradiction. + destruct Hs as [HD' [Hs1 Hs2]]. subst D'. + cbn [all] in H. destruct H as [IH2 [IH1 _]]. + cbn [forallb]. rewrite HD, (IH1 Hs1), (IH2 Hs2). reflexivity. } + destruct Hs. +Qed. + +Lemma no_typerec_fpe2 : no_typerec fpe2 = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma meta_typerec_no_typerec (D G sigma e1 e2 e3 : term) + (HD : no_typerec D = true) (HG : no_typerec G = true) + (Hsg : no_typerec sigma = true) + (H1 : no_typerec e1 = true) (H2 : no_typerec e2 = true) (H3 : no_typerec e3 = true) + : forall mu, simple_type_at D mu -> + no_typerec (meta_typerec D G mu sigma e1 e2 e3) = true. +Proof. + induction mu using term_ind_all; [ intros [] | ]. + cbn [simple_type_at meta_typerec]. intro Hs. + pose proof (eqb_spec n "*") as Hn1; destruct (eqb n "*"); [ exact H1 | ]. + pose proof (eqb_spec n "bool") as Hn2; destruct (eqb n "bool"); [ exact H2 | ]. + pose proof (eqb_spec n "->") as Hn3; destruct (eqb n "->"); [ | destruct Hs ]. + destruct l as [|t2 [|t1 [|D' [|? ?]]]]; try contradiction. + destruct Hs as [HD' [Hs1 Hs2]]. subst D'. + cbn [all] in H. destruct H as [IH2 [IH1 _]]. + cbv [MT_func]. apply no_typerec_subst; [ exact no_typerec_fpe2 | ]. + cbn [all snd]. + repeat split. + - apply IH2; exact Hs2. + - apply IH1; exact Hs1. + - exact H3. + - eapply simple_type_no_typerec; [ exact HD | exact Hs2 ]. + - eapply simple_type_no_typerec; [ exact HD | exact Hs1 ]. + - exact Hsg. + - exact HG. + - exact HD. +Qed. + +Lemma elim_typerec_no_typerec : forall (t : sort) (e : term), + Core.wf_term target_multilanguage [] e t -> + all_typerecs_simple e -> + no_typerec (elim_typerec e) = true. +Proof. + induction 1 using wf_term_cut_ind. + - intro Hats. + pose proof (eqb_spec name "typerec") as Hn; destruct (eqb name "typerec") eqn:Hnb. + 2:{ + assert (Helim : elim_typerec (con name s) = con name (map elim_typerec s)) + by (cbn [elim_typerec]; rewrite Hnb; reflexivity). + rewrite Helim, no_typerec_unfold, Hnb; cbn [negb andb]. + apply forallb_of_all, all_map. + destruct Hats as [_ Hall]. + pose proof (pargs_all (fun e => all_typerecs_simple e -> no_typerec (elim_typerec e) = true) + c' s H1) as Hp. + clear - Hall Hp. revert Hall Hp. + induction s as [|x s IH]; cbn [all]; [ tauto | ]. + intros [Hx Hs] [Hpx Hps]; split; [ apply Hpx; exact Hx | apply IH; assumption ]. } + subst name. assert (Hin := H). + apply tml_lookup in H. vm_compute in H. injection H as Hc' Hargs Ht. subst. + assert (Hlen : length s = 7) by (rewrite (pargs_len _ _ _ H1); reflexivity). + destruct s as [|e3 [|e2 [|e1 [|sg [|mu [|Gv [|Dv [|? ?]]]]]]]]; + cbn [length] in Hlen; try discriminate Hlen. + (destruct H1 as [[[[[[[_ IHD] IHG] IHmu] IHsg] IH1] IH2] IH3]). + (destruct Hats as [Hsimple [Ha3 [Ha2 [Ha1 [Hasg [Hamu [HaG [HaD _]]]]]]]]). + inversion H0 as [|? ? ? ? ? W3 H0a]; subst; clear H0. + inversion H0a as [|? ? ? ? ? W2 H0b]; subst; clear H0a. + inversion H0b as [|? ? ? ? ? W1 H0c]; subst; clear H0b. + inversion H0c as [|? ? ? ? ? Wsg H0d]; subst; clear H0c. + inversion H0d as [|? ? ? ? ? Wmu H0e]; subst; clear H0d. + inversion H0e as [|? ? ? ? ? WG H0f]; subst; clear H0e. + inversion H0f as [|? ? ? ? ? WD H0g]; subst; clear H0f. + rewrite elim_typerec_con7. + assert (HD : no_typerec Dv = true) + by (eapply stratum_no_typerec; [ exact WD | in_strat ]). + assert (HG : no_typerec Gv = true) + by (eapply stratum_no_typerec; [ exact WG | in_strat ]). + assert (HS : no_typerec sg = true) + by (eapply stratum_no_typerec; [ exact Wsg | in_strat ]). + apply meta_typerec_no_typerec; try assumption. + + apply IH1; exact Ha1. + + apply IH2; exact Ha2. + + apply IH3; exact Ha3. + - destruct H. + - intro Hats. apply IHwf_term; exact Hats. +Qed. + +(* ------------------------------------------------------------------ *) +(* Transfer of typerec-free terms into the sublanguage *) +(* ------------------------------------------------------------------ *) +Definition sub_rule_ok (p : string * rule) : bool := + match snd p with + | term_rule _ _ _ => + eqb (fst p) "typerec" + || (match named_list_lookup_err target_multilanguage_without_typerec (fst p) with + | Some r => eqb r (snd p) + | None => false + end) + | _ => true + end. + +Lemma sub_rules_ok : forallb sub_rule_ok target_multilanguage = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma term_rule_transfer name c' args t + : In (name, term_rule c' args t) target_multilanguage -> + name <> "typerec" -> + In (name, term_rule c' args t) target_multilanguage_without_typerec. +Proof. + intros Hin Hne. + pose proof sub_rules_ok as Hb. rewrite forallb_forall in Hb. + specialize (Hb _ Hin). cbv [sub_rule_ok fst snd] in Hb. + pose proof (eqb_spec name "typerec") as Hsp. + destruct (eqb name "typerec"); [ contradiction | ]. + cbn [orb] in Hb. + destruct (named_list_lookup_err target_multilanguage_without_typerec name) as [r|] eqn:Hl; + [ | discriminate ]. + pose proof (eqb_spec r (term_rule c' args t)) as Hr. + destruct (eqb r (term_rule c' args t)); [ subst r | discriminate ]. + apply named_list_lookup_err_in. symmetry. exact Hl. +Qed. + +Section Conservativity. + Context (Hconserv : forall t t' : sort, + Core.eq_sort target_multilanguage [] t t' -> + Core.eq_sort target_multilanguage_without_typerec [] t t'). + + Lemma pargs_wf_args (c' : ctx) (s : list term) + : WfCutElim.P_args string + (fun e t => no_typerec e = true -> + Core.wf_term target_multilanguage_without_typerec [] e t) s c' -> + forallb no_typerec s = true -> + @Model.wf_args _ _ _ (core_model target_multilanguage_without_typerec) [] s c'. + Proof. + revert s; induction c' as [| [n t] c' IH]; intros [|e s]; cbn [WfCutElim.P_args]; + try tauto. + { intros _ _. constructor. } + intros [HP HPe] Hf. cbn [forallb] in Hf. apply andb_prop in Hf. destruct Hf as [He Hs]. + constructor. + - apply HPe; exact He. + - apply IH; assumption. + Qed. + + Lemma no_typerec_transfer : forall (t : sort) (e : term), + Core.wf_term target_multilanguage [] e t -> + no_typerec e = true -> + Core.wf_term target_multilanguage_without_typerec [] e t. + Proof. + induction 1 using wf_term_cut_ind. + - rewrite no_typerec_unfold. intro Hnt. + apply andb_prop in Hnt. destruct Hnt as [Hname Hargs]. + pose proof (eqb_spec name "typerec") as Hsp. + destruct (eqb name "typerec"); [ discriminate Hname | ]. + eapply Core.wf_term_by. + + apply term_rule_transfer; [ exact H | exact Hsp ]. + + apply pargs_wf_args; assumption. + - destruct H. + - intro Hnt. eapply Core.wf_term_conv; [ apply IHwf_term; exact Hnt | ]. + apply Hconserv; exact H0. + Qed. + + Theorem partial_eval_wf_in_no_typerec_lang_modulo : forall (t : sort) (e : term), + Core.wf_term target_multilanguage [] e t -> + all_typerecs_simple e -> + Core.wf_term target_multilanguage_without_typerec [] (elim_typerec e) t. + Proof. + intros t e H Hats. + apply no_typerec_transfer with (t := t). + - apply partial_eval_wf_in_target; assumption. + - eapply elim_typerec_no_typerec; eassumption. + Qed. +End Conservativity. + +(* ------------------------------------------------------------------ *) +(* Conservativity of the typerec extension for sort equality. *) +(* [target_multilanguage_without_typerec] contains every rule of *) +(* [target_multilanguage] whose sort is type-level ([ty_env], [env], *) +(* [ty], [ty_sub]); sorts only mention type-level terms, so a sort *) +(* equality in the full target is derivable in the sublanguage *) +(* (Theory/Conservativity.v, via the cut-free induction principle). *) + +Definition tml_stratum (n : string) : bool := inb n strat_names. + +Lemma tml_conservative_check : + @Conservativity.lang_conservative string _ tml_stratum target_multilanguage + target_multilanguage_without_typerec = true. +Proof. vm_compute. reflexivity. Qed. + +Lemma eq_sort_conservative_tml : forall t t', + eq_sort target_multilanguage [] t t' -> + eq_sort target_multilanguage_without_typerec [] t t'. +Proof. + apply (proj1 (@Conservativity.eq_conservative_check string _ _ _ _ _ + target_multilanguage_wf target_multilanguage_without_typerec_wf + tml_stratum tml_conservative_check [] + ltac:(constructor) ltac:(constructor))). +Qed. + +(* ------------------------------------------------------------------ *) +(* Final theorems. *) +(* ------------------------------------------------------------------ *) Theorem partial_eval_wf_in_no_typerec_lang : forall (t : sort) (e : term), Core.wf_term target_multilanguage [] e t -> + all_typerecs_simple e -> Core.wf_term target_multilanguage_without_typerec [] (elim_typerec e) t. -Proof. Admitted. +Proof. + apply partial_eval_wf_in_no_typerec_lang_modulo. + exact eq_sort_conservative_tml. +Qed. +(* The form in which the theorem above is meant to be used: for compiled + source terms the [all_typerecs_simple] hypothesis is discharged by + [can_eliminate_typerec]. *) +Corollary compiled_partial_eval_wf : forall (t t' : sort) (e : term), + Core.wf_term source_multilanguage [] e t -> + Core.wf_term target_multilanguage [] (compile CMP e) t' -> + Core.wf_term target_multilanguage_without_typerec [] + (elim_typerec (compile CMP e)) t'. +Proof. + intros t t' e Hsrc Htgt. + apply partial_eval_wf_in_no_typerec_lang; [ exact Htgt | ]. + eapply can_eliminate_typerec; exact Hsrc. +Qed. diff --git a/src/Pyrosome/Theory/Conservativity.v b/src/Pyrosome/Theory/Conservativity.v new file mode 100644 index 00000000..46ad777e --- /dev/null +++ b/src/Pyrosome/Theory/Conservativity.v @@ -0,0 +1,248 @@ +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. +From Pyrosome.Theory Require CutElim. +From Pyrosome.Theory Require Import Core CutFreeInd. + + +Section WithVar. + Context (V : Type) + {V_Eqb : Eqb V} + {V_Eqb_ok : Eqb_ok V_Eqb} + {V_default : WithDefault V}. + + Notation named_list := (@named_list V). + Notation named_map := (@named_map V). + Notation term := (@term V). + Notation var := (@var V). + Notation con := (@con V). + Notation ctx := (@ctx V). + Notation sort := (@sort V). + Notation subst := (@subst V). + Notation rule := (@rule V). + Notation lang := (@lang V). + + Definition sort_name (t : sort) : V := match t with scon n _ => n end. + + Definition ctx_in_stratum (P : V -> bool) (c : ctx) : bool := + forallb (fun p => P (sort_name (snd p))) c. + + Lemma sort_name_subst (s : subst) (t : sort) + : sort_name t[/s/] = sort_name t. + Proof. destruct t; reflexivity. Qed. + + Lemma ctx_in_stratum_cons P n t (c : ctx) + : ctx_in_stratum P ((n,t)::c) + = (P (sort_name t) && ctx_in_stratum P c)%bool. + Proof. reflexivity. Qed. + + Section Conservativity. + Context (l l' : lang) (wfl : wf_lang l) (wfl' : wf_lang l') (P : V -> bool). + + Hypothesis Hsort_rule : forall n c' args, + In (n, sort_rule c' args) l -> + In (n, sort_rule c' args) l' /\ ctx_in_stratum P c' = true. + Hypothesis Hsort_eq : forall n c' t1 t2, + In (n, sort_eq_rule c' t1 t2) l -> + In (n, sort_eq_rule c' t1 t2) l' /\ ctx_in_stratum P c' = true + /\ P (sort_name t1) = P (sort_name t2). + Hypothesis Hterm_rule : forall n c' args t, + In (n, term_rule c' args t) l -> P (sort_name t) = true -> + In (n, term_rule c' args t) l' /\ ctx_in_stratum P c' = true. + Hypothesis Hterm_eq : forall n c' e1 e2 t, + In (n, term_eq_rule c' e1 e2 t) l -> P (sort_name t) = true -> + In (n, term_eq_rule c' e1 e2 t) l' /\ ctx_in_stratum P c' = true. + + Section WithCtx. + Context (c : ctx) + (wfc : wf_ctx (Model:=core_model l) c) + (wfc' : wf_ctx (Model:=core_model l') c). + + Let P_sort t1 t2 := + CutElim.eq_sort V l' c t1 t2 /\ P (sort_name t1) = P (sort_name t2). + Let P_term t e1 e2 := + P (sort_name t) = true -> CutElim.eq_term V l' c t e1 e2. + Let P_subst c' s1 s2 := + ctx_in_stratum P c' = true -> CutElim.eq_subst V l' c c' s1 s2. + Let P_args c' s1 s2 := + ctx_in_stratum P c' = true -> CutElim.eq_args V l' c c' s1 s2. + + Lemma conservative_cut + : (forall t1 t2, eq_sort l c t1 t2 -> P_sort t1 t2) + /\ (forall t e1 e2, eq_term l c t e1 e2 -> P_term t e1 e2) + /\ (forall c' s1 s2, + eq_subst (Model:=core_model l) c c' s1 s2 -> P_subst c' s1 s2) + /\ (forall c' s1 s2, + eq_args (Model:=core_model l) c c' s1 s2 -> P_args c' s1 s2). + Proof. + apply (cut_ind V l wfl c wfc P_sort P_term P_subst P_args); + unfold P_sort, P_term, P_subst, P_args in *; + clear P_sort P_term P_subst P_args. + (* Hsort0 : sort_eq_by *) + { + intros c' name t1 t2 s1 s2 Hin Hsub IH. + pose proof (Hsort_eq _ _ _ _ Hin) as [Hin' [Hstrat Hhead]]. + split. + { eapply CutElim.eq_sort_by; eauto. } + { rewrite !sort_name_subst; auto. } + } + (* Hsort1 : sort_cong *) + { + intros c' name args s1 s2 Hin Hargs IH. + pose proof (Hsort_rule _ _ _ Hin) as [Hin' Hstrat]. + split. + { eapply CutElim.eq_sort_cong; eauto. } + { reflexivity. } + } + (* Hsort2 : trans *) + { + intros t1 t12 t2 _ [H1 E1] _ [H2 E2]. + split; [eapply CutElim.eq_sort_trans; eauto | congruence]. + } + (* Hsort3 : sym *) + { + intros t1 t2 _ [H1 E1]. + split; [eapply CutElim.eq_sort_sym; eauto | congruence]. + } + (* f : term_eq_by *) + { + intros c' name t e1 e2 s1 s2 Hin Hsub IH Hp. + rewrite sort_name_subst in Hp. + pose proof (Hterm_eq _ _ _ _ _ Hin Hp) as [Hin' Hstrat]. + eapply CutElim.eq_term_by; eauto. + } + (* f0 : term_cong *) + { + intros c' name t args s1 s2 Hin Hargs IH Hp. + rewrite sort_name_subst in Hp. + pose proof (Hterm_rule _ _ _ _ Hin Hp) as [Hin' Hstrat]. + eapply CutElim.eq_term_cong; eauto. + } + (* f01 : var *) + { + intros n t Hin _. + eapply CutElim.eq_term_var; eauto. + } + (* f1 : trans *) + { + intros t e1 e12 e2 _ IH1 _ IH2 Hp. + eapply CutElim.eq_term_trans; eauto. + } + (* f2 : sym *) + { + intros t e1 e2 _ IH Hp. + eapply CutElim.eq_term_sym; eauto. + } + (* f3 : conv *) + { + intros t t' _ [Hs E] e1 e2 _ IH Hp. + eapply CutElim.eq_term_conv; [ eapply IH; congruence | eauto ]. + } + (* f4 : subst nil *) + { + intros _; constructor. + } + (* f5 : subst cons *) + { + intros c' s1 s2 _ IH name t e1 e2 _ IHt Hstrat. + rewrite ctx_in_stratum_cons in Hstrat. + apply Bool.andb_true_iff in Hstrat as [Ht Hc']. + constructor; eauto. + apply IHt; rewrite sort_name_subst; auto. + } + (* f6 : args nil *) + { + intros _; constructor. + } + (* f7 : args cons *) + { + intros c' s1 s2 _ IH name t e1 e2 _ IHt Hstrat. + rewrite ctx_in_stratum_cons in Hstrat. + apply Bool.andb_true_iff in Hstrat as [Ht Hc']. + constructor; eauto. + apply IHt; rewrite sort_name_subst; auto. + } + Qed. + + End WithCtx. + + Theorem eq_conservative (c : ctx) + (wfc : wf_ctx (Model:=core_model l) c) + (wfc' : wf_ctx (Model:=core_model l') c) + : (forall t1 t2, eq_sort l c t1 t2 -> eq_sort l' c t1 t2) + /\ (forall t e1 e2, eq_term l c t e1 e2 -> P (sort_name t) = true -> + eq_term l' c t e1 e2). + Proof. + pose proof (conservative_cut c wfc) as [Hs [Ht _]]. + pose proof (core_iff_cut V l' wfl' c wfc') as [Cs [Ct _]]. + split. + - intros t1 t2 H; apply Cs; apply Hs; auto. + - intros t e1 e2 H Hp; apply Ct; apply Ht; auto. + Qed. + + End Conservativity. + + Definition rule_conservative (P : V -> bool) (l' : lang) (p : V * rule) : bool := + let (n, r) := p in + match r with + | sort_rule c' _ => (inb (n,r) l' && ctx_in_stratum P c')%bool + | sort_eq_rule c' t1 t2 => + (inb (n,r) l' && ctx_in_stratum P c' + && eqb (P (sort_name t1)) (P (sort_name t2)))%bool + | term_rule c' _ t => + if P (sort_name t) then (inb (n,r) l' && ctx_in_stratum P c')%bool else true + | term_eq_rule c' _ _ t => + if P (sort_name t) then (inb (n,r) l' && ctx_in_stratum P c')%bool else true + end. + + Definition lang_conservative P (l l' : lang) : bool := + forallb (rule_conservative P l') l. + + Lemma inb_true_In (x : V * rule) (L : lang) + : inb x L = true -> In x L. + Proof. + intro H. + apply (proj1 (inb_is_In x L)). + rewrite H; exact I. + Qed. + + Theorem eq_conservative_check (l l' : lang) (wfl : wf_lang l) (wfl' : wf_lang l') + (P : V -> bool) + : lang_conservative P l l' = true -> + forall c, wf_ctx (Model:=core_model l) c -> wf_ctx (Model:=core_model l') c -> + (forall t1 t2, eq_sort l c t1 t2 -> eq_sort l' c t1 t2) + /\ (forall t e1 e2, eq_term l c t e1 e2 -> P (sort_name t) = true -> + eq_term l' c t e1 e2). + Proof. + unfold lang_conservative. + intro Hall. + rewrite forallb_forall in Hall. + apply eq_conservative; auto. + - intros n c' args Hin. + specialize (Hall _ Hin); cbn in Hall. + apply Bool.andb_true_iff in Hall as [H1 H2]. + split; auto using inb_true_In. + - intros n c' t1 t2 Hin. + specialize (Hall _ Hin); cbn in Hall. + apply Bool.andb_true_iff in Hall as [Hall H3]. + apply Bool.andb_true_iff in Hall as [H1 H2]. + split; [auto using inb_true_In|]. + split; auto. + destruct (P (sort_name t1)), (P (sort_name t2)); + cbn in H3; congruence. + - intros n c' args t Hin Hp. + specialize (Hall _ Hin); cbn in Hall. + rewrite Hp in Hall. + apply Bool.andb_true_iff in Hall as [H1 H2]. + split; auto using inb_true_In. + - intros n c' e1 e2 t Hin Hp. + specialize (Hall _ Hin); cbn in Hall. + rewrite Hp in Hall. + apply Bool.andb_true_iff in Hall as [H1 H2]. + split; auto using inb_true_In. + Qed. + +End WithVar.