Minor fixes

common/theories/Transform.v

@@ -23,13 +23,14 @@ Module Transform.
   Section Opt.
      Context {env env' : Type}.
      Context {term term' : Type}.
+     Context {value value' : Type}.
      Notation program' := (program env' term').
      Notation program := (program env term).
-     Context {eval :  program -> term -> Prop}.
-     Context {eval' : program' -> term' -> Prop}.
+     Context {eval :  program -> value -> Prop}.
+     Context {eval' : program' -> value' -> Prop}.
 
      Definition preserves_eval pre (transform : forall p : program, pre p -> program')
-      (obseq : forall p : program, pre p -> program' -> term -> term' -> Prop) :=
+      (obseq : forall p : program, pre p -> program' -> value -> value' -> Prop) :=
       forall p v (pr : pre p),
         eval p v ->
         let p' := transform p pr in
@@ -41,7 +42,7 @@ Module Transform.
       transform : forall p : program, pre p -> program';
       post : program' -> Prop;
       correctness : forall input (p : pre input), post (transform input p);
-      obseq : forall p : program, pre p -> program' -> term -> term' -> Prop;
+      obseq : forall p : program, pre p -> program' -> value -> value' -> Prop;
       preservation : preserves_eval pre transform obseq }.
 
     Definition run (x : t) (p : program) (pr : pre x p) : program' :=
@@ -50,19 +51,20 @@ Module Transform.
   End Opt.
   Arguments t : clear implicits.
 
-  Definition self_transform env term eval eval' := t env env term term eval eval'.
+  Definition self_transform env term eval eval' := t env env term term term term eval eval'.
 
   Section Comp.
     Context {env env' env'' : Type}.
     Context {term term' term'' : Type}.
-    Context {eval : program env term -> term -> Prop}.
-    Context {eval' : program env' term' -> term' -> Prop}.
-    Context {eval'' : program env'' term'' -> term'' -> Prop}.
+    Context {value value' value'' : Type}.
+    Context {eval : program env term -> value -> Prop}.
+    Context {eval' : program env' term' -> value' -> Prop}.
+    Context {eval'' : program env'' term'' -> value'' -> Prop}.
 
     Local Obligation Tactic := idtac.
-    Program Definition compose (o : t env env' term term' eval eval') (o' : t env' env'' term' term'' eval' eval'')
+    Program Definition compose (o : t env env' term term' _ _ eval eval') (o' : t env' env'' term' term'' _ _ eval' eval'')
       (hpp : (forall p, o.(post) p -> o'.(pre) p))
-      : t env env'' term term'' eval eval'' :=
+      : t env env'' term term'' _ _ eval eval'' :=
       {|
         name := (o.(name) ^ " -> " ^ o'.(name))%bs;
         transform p hp := run o' (run o p hp) (hpp _ (o.(correctness) _ hp));

erasure-plugin/Makefile.plugin.local

@@ -1,3 +1,4 @@
+CAMLFLAGS :=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 CAMLFLAGS+=-open Metacoq_template_plugin
 CAMLFLAGS+=-w -8 # Non-exhaustive matches due to translation of comparison to int
 CAMLFLAGS+=-w -20 # Unused arguments

erasure-plugin/theories/ETransform.v

@@ -195,7 +195,7 @@ Qed.
 
 Local Obligation Tactic := try solve [ eauto ].
 
-Program Definition erase_transform {guard : abstract_guard_impl} : Transform.t _ _ PCUICAst.term EAst.term
+Program Definition erase_transform {guard : abstract_guard_impl} : Transform.t _ _ PCUICAst.term EAst.term PCUICAst.term EAst.term
   eval_pcuic_program (eval_eprogram_env EWcbvEval.default_wcbv_flags) :=
  {| name := "erasure";
     pre p :=
@@ -327,7 +327,7 @@ End PCUICEnv.
 Import EWcbvEval (WcbvFlags, with_prop_case, with_guarded_fix).
 
 Program Definition guarded_to_unguarded_fix {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} {efl : EEnvFlags} (wguard : with_guarded_fix) :
-  Transform.t _ _ EAst.term EAst.term
+  Transform.t _ _ EAst.term EAst.term _ _
     (eval_eprogram_env fl) (eval_eprogram_env (EWcbvEval.switch_unguarded_fix fl)) :=
   {| name := "switching to unguarded fixpoints";
     transform p pre := p;
@@ -356,7 +356,7 @@ Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogr
   (GlobalContextMap.make p.1 (wf_glob_fresh p.1 (proj1 hwf)), p.2).
 
 Program Definition rebuild_wf_env_transform {fl : EWcbvEval.WcbvFlags} {efl} (with_exp : bool) :
-  Transform.t _ _ EAst.term EAst.term (eval_eprogram fl) (eval_eprogram_env fl) :=
+  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram fl) (eval_eprogram_env fl) :=
   {| name := "rebuilding environment lookup table";
      pre p := wf_eprogram efl p /\ (with_exp ==> EEtaExpanded.expanded_eprogram_cstrs p);
      transform p pre := rebuild_wf_env p (proj1 pre);
@@ -378,7 +378,7 @@ Qed.
 
 Program Definition remove_params_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
   (efl := all_env_flags):
-  Transform.t _ _ EAst.term EAst.term (eval_eprogram_env fl) (eval_eprogram fl) :=
+  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
   {| name := "stripping constructor parameters";
     transform p pre := ERemoveParams.strip_program p;
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
@@ -414,7 +414,7 @@ Qed.
 
 Program Definition remove_params_fast_optimization {fl : EWcbvEval.WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false}
   (efl := all_env_flags) :
-  Transform.t _ _ EAst.term EAst.term (eval_eprogram_env fl) (eval_eprogram fl) :=
+  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
   {| name := "stripping constructor parameters (faster?)";
     transform p _ := (ERemoveParams.Fast.strip_env p.1, ERemoveParams.Fast.strip p.1 [] p.2);
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
@@ -456,7 +456,7 @@ Qed.
 Import EOptimizePropDiscr EWcbvEval.
 
 Program Definition remove_match_on_box_trans {fl : WcbvFlags} {wcon : with_constructor_as_block = false} {efl : EEnvFlags} {hastrel : has_tRel} {hastbox : has_tBox} :
-  Transform.t _ _  EAst.term EAst.term (eval_eprogram_env fl) (eval_eprogram (disable_prop_cases fl)) :=
+  Transform.t _ _  EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram (disable_prop_cases fl)) :=
   {| name := "optimize_prop_discr";
     transform p _ := remove_match_on_box_program p ;
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
@@ -492,7 +492,7 @@ From MetaCoq.Erasure Require Import EInlineProjections.
 
 Program Definition inline_projections_optimization {fl : WcbvFlags} {wcon : EWcbvEval.with_constructor_as_block = false} (efl := switch_no_params all_env_flags)
   {hastrel : has_tRel} {hastbox : has_tBox} :
-  Transform.t _ _ EAst.term EAst.term (eval_eprogram_env fl) (eval_eprogram fl) :=
+  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) :=
   {| name := "primitive projection inlining";
     transform p _ := EInlineProjections.optimize_program p ;
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
@@ -528,7 +528,7 @@ From MetaCoq.Erasure Require Import EConstructorsAsBlocks.
 
 Program Definition constructors_as_blocks_transformation {efl : EEnvFlags}
   {has_app : has_tApp} {has_rel : has_tRel} {hasbox : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = false} :
-  Transform.t _ _ EAst.term EAst.term (eval_eprogram_env target_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
+  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env target_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
   {| name := "transforming to constuctors as blocks";
     transform p _ := EConstructorsAsBlocks.transform_blocks_program p ;
     pre p := wf_eprogram_env efl p /\ EEtaExpanded.expanded_eprogram_env_cstrs p;
@@ -568,7 +568,7 @@ From MetaCoq.Erasure Require Import EImplementBox.
 
 Program Definition implement_box_transformation {efl : EEnvFlags}
   {has_app : has_tApp} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} :
-  Transform.t _ _ EAst.term EAst.term (eval_eprogram block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
+  Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram block_wcbv_flags) (eval_eprogram block_wcbv_flags) :=
   {| name := "transforming to constuctors as blocks";
     transform p _ := EImplementBox.implement_box_program p ;
     pre p := wf_eprogram efl p ;

erasure-plugin/theories/Erasure.v

@@ -42,7 +42,7 @@ Axiom assume_preservation_template_program_env_expansion :
 
 (** We kludge the normalization assumptions by parameterizing over a continuation of "what will be done to the program later" as well as what properties we'll need of it *)
 
-Program Definition eta_expand K : Transform.t _ _ Ast.term Ast.term
+Program Definition eta_expand K : Transform.t _ _ Ast.term Ast.term _ _
   eval_template_program_env eval_template_program :=
   {| name := "eta expand cstrs and fixpoints";
       pre := fun p => ∥ wt_template_program_env p ∥ /\ K (eta_expand_global_env p.1) ;
@@ -59,7 +59,7 @@ Next Obligation.
 Qed.
 
 Program Definition verified_lambdabox_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
- Transform.t _ _ EAst.term EAst.term
+ Transform.t _ _ EAst.term EAst.term _ _
    (EProgram.eval_eprogram_env {| with_prop_case := true; with_guarded_fix := true; with_constructor_as_block := false |})
    (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) :=
   (* Simulation of the guarded fixpoint rules with a single unguarded one:
@@ -99,7 +99,7 @@ Qed.
 
 Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
  Transform.t _ _
-  PCUICAst.term EAst.term
+  PCUICAst.term EAst.term _ _
   PCUICTransform.eval_pcuic_program
   (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) :=
   (* a bunch of nonsense for normalization preconditions *)
@@ -117,10 +117,10 @@ Program Definition verified_erasure_pipeline {guard : abstract_guard_impl} (efl
 Import EGlobalEnv EWellformed.
 
 Definition transform_compose
-  {env env' env'' term term' term'' : Type}
+  {env env' env'' term term' term'' value value' value'' : Type}
   {eval eval' eval''}
-  (o : t env env' term term' eval eval')
-  (o' : t env' env'' term' term'' eval' eval'')
+  (o : t env env' term term' value value' eval eval')
+  (o' : t env' env'' term' term'' value' value'' eval' eval'')
   (pre : forall p, post o p -> pre o' p) :
   forall x p1, exists p3,
     transform (compose o o' pre) x p1 = transform o' (transform o x p1) p3.
@@ -138,7 +138,7 @@ Qed.
 
 Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
  Transform.t _ _
-  Ast.term PCUICAst.term
+  Ast.term PCUICAst.term _ _
   TemplateProgram.eval_template_program
    PCUICTransform.eval_pcuic_program :=
   (* a bunch of nonsense for normalization preconditions *)
@@ -159,7 +159,7 @@ Program Definition pre_erasure_pipeline {guard : abstract_guard_impl} (efl := EW
 
 Program Definition erasure_pipeline {guard : abstract_guard_impl} (efl := EWellformed.all_env_flags) :
  Transform.t _ _
-  Ast.term EAst.term
+  Ast.term EAst.term _ _
   TemplateProgram.eval_template_program
   (EProgram.eval_eprogram {| with_prop_case := false; with_guarded_fix := false; with_constructor_as_block := true |}) :=
   pre_erasure_pipeline ▷

erasure-plugin/theories/ErasureCorrectness.v

@@ -25,11 +25,11 @@ Import Transform.
 Import EWcbvEval.
 
 Lemma transform_compose_assoc
-  {env env' env'' env''' term term' term'' term''' : Type}
+  {env env' env'' env''' term term' term'' term''' value value' value'' value''' : Type}
   {eval eval' eval'' eval'''}
-  (o : t env env' term term' eval eval')
-  (o' : t env' env'' term' term'' eval' eval'')
-  (o'' : t env'' env''' term'' term''' eval'' eval''')
+  (o : t env env' term term' value value' eval eval')
+  (o' : t env' env'' term' term'' value' value'' eval' eval'')
+  (o'' : t env'' env''' term'' term''' value'' value''' eval'' eval''')
   (prec : forall p, post o p -> pre o' p)
   (prec' : forall p, post o' p -> pre o'' p) :
   forall x p1,
@@ -43,11 +43,11 @@ Proof.
 Qed.
 
 Lemma obseq_compose_assoc
-  {env env' env'' env''' term term' term'' term''' : Type}
+  {env env' env'' env''' term term' term'' term''' value value' value'' value''' : Type}
   {eval eval' eval'' eval'''}
-  (o : t env env' term term' eval eval')
-  (o' : t env' env'' term' term'' eval' eval'')
-  (o'' : t env'' env''' term'' term''' eval'' eval''')
+  (o : t env env' term term' value value' eval eval')
+  (o' : t env' env'' term' term'' value' value'' eval' eval'')
+  (o'' : t env'' env''' term'' term''' value'' value''' eval'' eval''')
   (prec : forall p, post o p -> pre o' p)
   (prec' : forall p, post o' p -> pre o'' p) :
   forall x p1 p2 v1 v2, obseq (compose o (compose o' o'' prec') prec) x p1 p2 v1 v2 <->
@@ -438,7 +438,7 @@ Module ETransformPresFO.
     Context {env env' : Type}.
     Context {eval : program env EAst.term -> EAst.term -> Prop}.
     Context {eval' : program env' EAst.term -> EAst.term -> Prop}.
-    Context (o : Transform.t _ _ _ _ eval eval').
+    Context (o : Transform.t _ _ _ _ _ _ eval eval').
     Context (firstorder_value : program env EAst.term -> Prop).
     Context (firstorder_value' : program env' EAst.term -> Prop).
     Context (compile_fo_value : forall p : program env EAst.term, o.(pre) p ->
@@ -453,7 +453,7 @@ Module ETransformPresFO.
     Context {env env' : Type}.
     Context {eval : program env EAst.term -> EAst.term -> Prop}.
     Context {eval' : program env' EAst.term -> EAst.term -> Prop}.
-    Context (o : Transform.t _ _ _ _ eval eval').
+    Context (o : Transform.t _ _ _ _ _ _ eval eval').
     Context (firstorder_value : program env EAst.term -> Prop).
     Context (firstorder_value' : program env' EAst.term -> Prop).
 
@@ -478,7 +478,7 @@ Module ETransformPresFO.
     Context (firstorder_value : program env EAst.term -> Prop).
     Context (firstorder_value' : program env' EAst.term -> Prop).
     Context (firstorder_value'' : program env'' EAst.term -> Prop).
-    Context (o : Transform.t _ _ _ _ eval eval') (o' : Transform.t _ _ _ _ eval' eval'').
+    Context (o : Transform.t _ _ _ _ _ _ eval eval') (o' : Transform.t _ _ _ _ _ _ eval' eval'').
     Context compile_fo_value compile_fo_value'
       (oext : t o firstorder_value firstorder_value' compile_fo_value)
       (o'ext : t o' firstorder_value' firstorder_value'' compile_fo_value')
@@ -909,9 +909,8 @@ Section PCUICExpandLets.
   Proof.
     rewrite /PCUICFirstorder.firstorder_type /PCUICFirstorder.firstorder_env.
     pose proof (trans_decompose_app t).
-    destruct decompose_app. rewrite H. cbn.
-    destruct t0 => //. intros hd => /=.
-    destruct ind.
+    destruct decompose_app. rewrite {}H. cbn.
+    case: t0 => //; case => /= kn _ _ hd.
     destruct plookup_env eqn:hp => //.
     destruct b => //.
     eapply hd in hp. rewrite hp //.

erasure/theories/EProgram.v

@@ -55,10 +55,11 @@ Module TransformExt.
   Section Opt.
     Context {env env' env'' : Type}.
     Context {term term' term'' : Type}.
-    Context {eval : program env term -> term -> Prop}.
-    Context {eval' : program env' term' -> term' -> Prop}.
-    Context {eval'' : program env'' term'' -> term'' -> Prop}.
-    Context (o : Transform.t env env' term term' eval eval').
+    Context {value value' value'' : Type}.
+    Context {eval : program env term -> value -> Prop}.
+    Context {eval' : program env' term' -> value' -> Prop}.
+    Context {eval'' : program env'' term'' -> value'' -> Prop}.
+    Context (o : Transform.t env env' term term' value value' eval eval').
     Context (extends : program env term -> program env term -> Prop).
     Context (extends' : program env' term' -> program env' term' -> Prop).
 
@@ -70,17 +71,18 @@ Module TransformExt.
   Section Comp.
     Context {env env' env'' : Type}.
     Context {term term' term'' : Type}.
-    Context {eval : program env term -> term -> Prop}.
-    Context {eval' : program env' term' -> term' -> Prop}.
-    Context {eval'' : program env'' term'' -> term'' -> Prop}.
+    Context {value value' value'' : Type}.
+    Context {eval : program env term -> value -> Prop}.
+    Context {eval' : program env' term' -> value' -> Prop}.
+    Context {eval'' : program env'' term'' -> value'' -> Prop}.
     Context {extends : program env term -> program env term -> Prop}.
     Context {extends' : program env' term' -> program env' term' -> Prop}.
     Context {extends'' : program env'' term'' -> program env'' term'' -> Prop}.
 
     Local Obligation Tactic := idtac.
     #[global]
-    Instance compose (o : Transform.t env env' term term' eval eval')
-      (o' : Transform.t env' env'' term' term'' eval' eval'')
+    Instance compose (o : Transform.t env env' term term' value value' eval eval')
+      (o' : Transform.t env' env'' term' term'' value' value'' eval' eval'')
       (oext : t o extends extends')
       (o'ext : t o' extends' extends'')
       (hpp : (forall p, o.(post) p -> o'.(pre) p))

pcuic/Makefile.plugin.local

@@ -1,2 +1,4 @@
+
+CAMLFLAGS :=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 CAMLFLAGS+=-open Metacoq_template_plugin -open Metacoq_checker_plugin
 CAMLFLAGS+=-w -33 # Unused opens

pcuic/theories/PCUICEtaExpand.v

@@ -5,7 +5,7 @@ From MetaCoq.Common Require Import config.
 From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTyping
   PCUICReduction PCUICProgram PCUICLiftSubst PCUICCSubst PCUICUnivSubst.
 
-(* todo move *)
+(* move *)
 Lemma All_fold_tip {A : Type} (P : list A -> A -> Type) {x} : All_fold P [x] -> P [] x.
 Proof.
   intros a; now depelim a.

safechecker-plugin/Makefile.plugin.local

@@ -1,3 +1,4 @@
+CAMLFLAGS :=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 CAMLFLAGS+=-open Metacoq_template_plugin
 CAMLFLAGS+=-w -8 # Non-exhaustive matches due to translation of comparison to int
 CAMLFLAGS+=-w -20 # Unused arguments

template-coq/Makefile.plugin.local

@@ -1,3 +1,7 @@
+CAMLPKGS+=-package stdlib-shims
+INSTALLDEFAULTROOT=MetaCoq/Template
+
+CAMLFLAGS :=-thread -bin-annot -strict-sequence -w -a+1..3-4+5..8-9+10..26-27+28..39-40-41-42+43-44-45+46..47-48+49..57-58+59..66-67-68+69-70
 CAMLFLAGS+=-w -20 # Unused argument (produced by extraction)
 CAMLFLAGS+=-w -33 # Unused opens
 CAMLFLAGS+=-w -32 # Unused value
@@ -7,7 +11,5 @@ CAMLFLAGS+=-w -34 # Unused type
 CAMLFLAGS+=-w -60 # Unused module
 # CAMLFLAGS+=-w -8 # Non-exhaustive pattern-matchings (BEWARE, just for extracted code)
 CAMLFLAGS+=-bin-annot # For merlin
-CAMLPKGS+=-package stdlib-shims
-INSTALLDEFAULTROOT=MetaCoq/Template
 
 .PHONY: META

template-coq/theories/TemplateProgram.v

@@ -47,7 +47,7 @@ Definition make_template_program_env {cf : checker_flags} (p : template_program)
 (** We kludge the normalization assumptions by parameterizing over a continuation of "what will be done to the program later" as well as what properties we'll need of it *)
 
 Program Definition build_template_program_env {cf : checker_flags} K :
-  Transform.t global_env GlobalEnvMap.t Ast.term Ast.term eval_template_program eval_template_program_env  :=
+  Transform.t global_env GlobalEnvMap.t Ast.term Ast.term Ast.term Ast.term eval_template_program eval_template_program_env  :=
   {| name := "rebuilding environment lookup table";
      pre p := ∥ wt_template_program p ∥ /\ forall pf, K (GlobalEnvMap.make p.1 (wt_template_program_fresh p pf)) : Prop ;
      transform p pre := make_template_program_env p (proj1 pre);

template-pcuic/theories/PCUICTransform.v

@@ -34,7 +34,7 @@ Local Obligation Tactic := idtac.
 (** We kludge the normalization assumptions by parameterizing over a continuation of "what will be done to the program later" as well as what properties we'll need of it *)
 
 Program Definition template_to_pcuic_transform {cf : checker_flags} K :
-  Transform.t Ast.Env.global_env global_env_ext_map Ast.term term
+  Transform.t Ast.Env.global_env global_env_ext_map Ast.term term Ast.term term
   eval_template_program eval_pcuic_program :=
  {| name := "template to pcuic";
     pre p := ∥ wt_template_program p ∥ /\ EtaExpand.expanded_program p /\ K (trans_global (Ast.Env.empty_ext p.1)) ;