diff --git a/erasure-plugin/theories/ETransform.v b/erasure-plugin/theories/ETransform.v index 3af3e47a8..454f91dfe 100644 --- a/erasure-plugin/theories/ETransform.v +++ b/erasure-plugin/theories/ETransform.v @@ -696,9 +696,6 @@ Proof. red. intros p p' pr pr' [? ?]. now rewrite /transform /=. Qed. -Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogram_env := - (GlobalContextMap.make p.1 (wf_glob_fresh p.1 (proj1 hwf)), p.2). - Definition preserves_expansion with_fix p := if with_fix then EEtaExpandedFix.expanded_eprogram p else EEtaExpanded.expanded_eprogram_cstrs p. @@ -707,6 +704,9 @@ Definition preserves_expansion_env with_fix p := if with_fix then EEtaExpandedFix.expanded_eprogram_env p else EEtaExpanded.expanded_eprogram_env_cstrs p. +Definition rebuild_wf_env {efl} (p : eprogram) (hwf : wf_eprogram efl p): eprogram_env := + (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 with_fix : bool) : Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram fl) (eval_eprogram_env fl) := {| name := "rebuilding environment lookup table"; @@ -736,6 +736,39 @@ Proof. red. intros p p' pr pr' [? ?]. now rewrite /transform /=. Qed. + +Definition project_wf_env {efl} (p : eprogram_env) (hwf : wf_eprogram_env efl p): eprogram := + (GlobalContextMap.global_decls p.1, p.2). + +Program Definition project_wf_env_transform {fl : EWcbvEval.WcbvFlags} {efl} (with_exp with_fix : bool) : + Transform.t _ _ EAst.term EAst.term _ _ (eval_eprogram_env fl) (eval_eprogram fl) := + {| name := "projecting environment declarations list"; + pre p := wf_eprogram_env efl p /\ (with_exp -> preserves_expansion_env with_fix p); + transform p pre := project_wf_env p (proj1 pre); + post p := wf_eprogram efl p /\ (with_exp -> preserves_expansion with_fix p); + obseq p hp p' v v' := v = v' |}. +Next Obligation. + cbn. unfold preserves_expansion, preserves_expansion_env. + intros fl efl [] [] input [wf exp]; cbn; split => //. +Qed. +Next Obligation. + cbn. intros fl efl [] [] input v [] ev p'; exists v; split => //. +Qed. + +#[global] +Instance project_wf_env_extends {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp with_fix : + TransformExt.t (project_wf_env_transform with_exp with_fix) (fun p p' => extends p.1 p'.1) (fun p p' => extends p.1 p'.1). +Proof. + red. intros p p' pr pr' ext. red. now rewrite /transform /=. +Qed. + +#[global] +Instance project_wf_env_extends' {fl : EWcbvEval.WcbvFlags} {efl : EEnvFlags} with_exp with_fix : + TransformExt.t (project_wf_env_transform with_exp with_fix) extends_eprogram_env extends_eprogram. +Proof. + red. intros p p' pr pr' [? ?]. now rewrite /transform /=. +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) := @@ -975,12 +1008,12 @@ Program Definition coinductive_to_inductive_transformation (efl : EEnvFlags) {has_app : has_tApp} {has_box : has_tBox} {has_rel : has_tRel} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} : Transform.t _ _ EAst.term EAst.term _ _ - (eval_eprogram_env block_wcbv_flags) (eval_eprogram block_wcbv_flags) := + (eval_eprogram block_wcbv_flags) (eval_eprogram_env block_wcbv_flags) := {| name := "transforming co-inductive to inductive types"; transform p _ := ECoInductiveToInductive.trans_program p ; - pre p := wf_eprogram_env efl p ; - post p := wf_eprogram efl p ; - obseq p hp p' v v' := v' = ECoInductiveToInductive.trans p.1 v |}. + pre p := wf_eprogram efl p ; + post p := wf_eprogram_env efl p ; + obseq p hp p' v v' := v' = ECoInductiveToInductive.trans p'.1 v |}. Next Obligation. move=> efl hasapp hasbox hasrel haspars hascstrs [Σ t] [wftp wft]. @@ -991,9 +1024,10 @@ Next Obligation. eexists. split; [ | eauto]. econstructor. cbn -[transform_blocks]. - eapply ECoInductiveToInductive.trans_correct; cbn; eauto. + apply ECoInductiveToInductive.trust_cofix. + (* eapply ECoInductiveToInductive.trans_correct; cbn; eauto. eapply wellformed_closed_env, wfe1. - Unshelve. all:eauto. + Unshelve. all:eauto. *) Qed. #[global] @@ -1012,7 +1046,7 @@ Instance coinductive_to_inductive_transformation_ext' (efl : EEnvFlags) {has_app : has_tApp} {has_rel : has_tRel} {has_box : has_tBox} {has_pars : has_cstr_params = false} {has_cstrblocks : cstr_as_blocks = true} : TransformExt.t (coinductive_to_inductive_transformation efl (has_app := has_app) (has_rel := has_rel) (has_box := has_box) (has_pars := has_pars) (has_cstrblocks := has_cstrblocks)) - extends_eprogram_env extends_eprogram. + extends_eprogram extends_eprogram_env. Proof. red. intros p p' pr pr' ext. rewrite /transform /=. eapply ECoInductiveToInductive.trust_cofix. diff --git a/erasure-plugin/theories/Erasure.v b/erasure-plugin/theories/Erasure.v index b43908c2f..c515203fc 100644 --- a/erasure-plugin/theories/Erasure.v +++ b/erasure-plugin/theories/Erasure.v @@ -128,11 +128,10 @@ Program Definition optional_unsafe_transforms econf := let efl := EConstructorsAsBlocks.switch_cstr_as_blocks (EInlineProjections.disable_projections_env_flag (ERemoveParams.switch_no_params EWellformed.all_env_flags)) in ETransform.optional_self_transform passes.(cofix_to_lazy) - ((* Rebuild the efficient lookup table *) - rebuild_wf_env_transform (efl := efl) false false ▷ - (* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *) + ((* Coinductives & cofixpoints are translated to inductive types and thunked fixpoints *) coinductive_to_inductive_transformation efl - (has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl)) ▷ + (has_app := eq_refl) (has_box := eq_refl) (has_rel := eq_refl) (has_pars := eq_refl) (has_cstrblocks := eq_refl) ▷ + project_wf_env_transform false false) ▷ ETransform.optional_self_transform passes.(reorder_constructors) (reorder_cstrs_transformation efl final_wcbv_flags econf.(inductives_mapping)) ▷ ETransform.optional_self_transform passes.(unboxing) diff --git a/erasure/theories/ECoInductiveToInductive.v b/erasure/theories/ECoInductiveToInductive.v index 485284539..38724df47 100644 --- a/erasure/theories/ECoInductiveToInductive.v +++ b/erasure/theories/ECoInductiveToInductive.v @@ -33,9 +33,141 @@ Axiom trust_cofix : forall {A}, A. #[global] Hint Constructors eval : core. +Module Horror. +(* +Consider these examples... +*) +CoInductive stream := Cons { head : nat; tail : stream }. + +Definition mk n tail := {| head := n; tail := {| head := n; tail := tail |} |}. + +CoFixpoint repeat n := + mk n (repeat n). + +(* or... *) + +CoFixpoint repeat' n := + let mk n tail := {| head := n; tail := {| head := n; tail := tail |} |} in + mk n (repeat' n). + +(* or... *) +CoFixpoint repeat'' n := + let mk n tail := {| head := n; tail := {| head := n; tail := tail |} |} in + (fun cnstr rec => cnstr rec) (mk n) (repeat'' n). + +End Horror. + +(* CAUTION: This weak-head reduction function has not been proved to terminate *) +Unset Guard Checking. + +Section whnf. + Context (Σ : GlobalContextMap.t). + + Fixpoint whnf_stack (t : term) (args : list term) { struct t } : term := + let whnf t := let '(hd, args) := decompose_app t in whnf_stack t args in + let default := mkApps t args in + match t with + | tRel _ => default + | tEvar _ _ => default + | tLambda na M => match args with + | hd :: args => whnf_stack (subst10 hd M) args + | [] => t + end + | tApp u v => whnf_stack u (v :: args) + | tLetIn na b b' => whnf_stack (subst10 b b') args + | tCase ind c brs => + match whnf c with + | tConstruct ind n cargs => + match nth_error brs n with + | Some br => whnf_stack (iota_red 0 cargs br) args + | None => default + end + | _ => default + end + | tProj p c => + match whnf c with + | tConstruct ind n cargs => + match nth_error cargs p.(proj_arg) with + | Some a => whnf_stack a args + | None => default + end + | _ => default + end + | tFix mfix idx => + match unfold_fix mfix idx with + | Some (rarg, def) => + match nth_error args rarg with + | Some arg => + match whnf arg with + | tConstruct _ _ _ => whnf_stack def args + | _ => default + end + | None => default + end + | None => default + end + | tCoFix _ _ => default + | tBox => default + | tVar _ => default + | tConst kn => + (* This forces unfolding, as the productivity check can go under constants. + This makes the definition non-structurally recursive. *) + match GlobalContextMap.lookup_constant Σ kn with + | Some {| cst_body := Some body |} => whnf_stack body args + | _ => t + end + | tConstruct _ _ _ => default + | tPrim _ => default + | tLazy _ => default + | tForce t => match whnf t with tLazy l => whnf_stack l args | _ => default end + end. +End whnf. +Set Guard Checking. + +Notation whnf Σ t := (whnf_stack Σ t []). + +(* END OF Guard Checking Axiom *) + + +Section trans. + Context (Σ : GlobalContextMap.t). + + Fixpoint decompose_n_lambdas n t := + match n with + | 0 => Some ([], t) + | S n => + match whnf Σ t with + | tLambda na b => + '(nas, b) <- decompose_n_lambdas n b ;; + ret (na :: nas, b) + | _ => None + end + end. + + Fixpoint force_cofix_body (t : term) : term := + match t with + | tLazy t => t + | tCase ind c brs => + let brs' := List.map (fun '(n, br) => (n, force_cofix_body br)) brs in + tCase ind c brs' + | _ => tForce t + end. + + Definition mkLambdas nas t := + fold_right tLambda t nas. + +End trans. + Section trans. Context (Σ : GlobalContextMap.t). + Definition hoist_head_lazy_def (t : def term) := + '(nas, body') <- decompose_n_lambdas Σ t.(rarg) t.(dbody) ;; + let body'' := force_cofix_body (whnf Σ body') in + ret {| dname := t.(dname); + rarg := t.(rarg); + dbody := mkLambdas nas (tLazy body'') |}. + Fixpoint trans (t : term) : term := match t with | tRel i => tRel i @@ -60,7 +192,10 @@ Section trans. tFix mfix' idx | tCoFix mfix idx => let mfix' := List.map (map_def trans) mfix in - tFix mfix' idx + match map_option_out (List.map hoist_head_lazy_def mfix') with + | Some mfix' => tFix mfix' idx + | None => tFix mfix' idx + end | tBox => t | tVar _ => t | tConst _ => t @@ -127,6 +262,7 @@ Section trans. - move/andP: H => [] clt clargs. destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all. - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //; rtoProp; solve_all; solve_all. + - apply trust_cofix. - primProp. solve_all_k 6. Qed. @@ -185,6 +321,8 @@ Section trans. - destruct GlobalContextMap.lookup_inductive_kind as [[]|] => /= //. all:f_equal; eauto; try (rewrite /on_snd map_map_compose; solve_all). f_equal; eauto. + - f_equal; eauto. solve_all_k 6. + apply trust_cofix. Qed. Lemma trans_substl s t : @@ -307,8 +445,11 @@ Definition trans_decl Σ d := end. Definition trans_env Σ := - map (on_snd (trans_decl Σ)) Σ.(GlobalContextMap.global_decls). - + fold_right (fun '(kn, d) Σ' => + let d' := trans_decl Σ' d in + GlobalContextMap.add Σ' kn d' trust_cofix) + GlobalContextMap.empty Σ. +(* Import EnvMap. Program Fixpoint trans_env' Σ : EnvMap.fresh_globals Σ -> global_context := @@ -318,6 +459,11 @@ Program Fixpoint trans_env' Σ : EnvMap.fresh_globals Σ -> global_context := let Σg := GlobalContextMap.make tl (fresh_globals_cons_inv HΣ) in on_snd (trans_decl Σg) hd :: trans_env' tl (fresh_globals_cons_inv HΣ) end. +*) + +Definition trans_program (p : eprogram) := + let Σ' := trans_env p.1 in + (Σ', trans Σ' p.2). Import EGlobalEnv EExtends. @@ -336,6 +482,8 @@ Proof. Qed. *) +(* + Lemma extends_inductive_isprop_and_pars {efl : EEnvFlags} {Σ Σ' ind} : extends Σ Σ' -> wf_glob Σ' -> isSome (lookup_inductive Σ ind) -> inductive_isprop_and_pars Σ ind = inductive_isprop_and_pars Σ' ind. @@ -397,6 +545,7 @@ Proof. unfold lookup_inductive in hl. destruct lookup_minductive => //. rewrite (IHt _ H2 _ H0 H1) //. + - f_equal. apply trust_cofix. Qed. Lemma wellformed_trans_decl_extends {wfl: EEnvFlags} {Σ : GlobalContextMap.t} t : @@ -569,6 +718,7 @@ Proof. all:try solve [intros; repeat constructor => //]. destruct args => //. move=> /andP[] wc. now rewrite wcon in wc. + destruct map_option_out => //=; repeat constructor. - intros p pv IH wf. cbn. constructor. constructor 2. cbn in wf. move/andP: wf => [hasp tp]. primProp. depelim tp; depelim pv; depelim IH; constructor; cbn in *; rtoProp; intuition auto; solve_all. @@ -688,6 +838,7 @@ Proof. - apply trust_cofix. - apply trust_cofix. Qed. +*) (* - rewrite trans_mkApps in e1. simpl in *. @@ -851,7 +1002,7 @@ Proof. now constructor. constructor; eauto; solve_all. - cbn. econstructor; eauto. solve_all. now eapply isLambda_trans. - - cbn. econstructor; eauto; solve_all. apply trust_cofix. + - cbn. rewrite map_map_compose. apply trust_cofix. - cbn -[GlobalContextMap.lookup_inductive_kind]. rewrite GlobalContextMap.lookup_inductive_kind_spec. destruct lookup_inductive_kind as [[]|] => /= //. @@ -876,6 +1027,7 @@ Qed. now len. solve_all. Qed. *) +(* Lemma trans_expanded_irrel {efl : EEnvFlags} {Σ : GlobalContextMap.t} t : wf_glob Σ -> expanded Σ t -> expanded (trans_env Σ) t. Proof. intros wf; induction 1 using expanded_ind. @@ -1056,11 +1208,15 @@ Proof. induction 1; cbn; constructor; auto. now eapply Forall_map; cbn. Qed. +*) -Lemma trans_env_wf {efl : EEnvFlags} {Σ : GlobalContextMap.t} : +Lemma trans_env_wf {efl : EEnvFlags} {Σ} : has_tBox -> has_tRel -> wf_glob Σ -> wf_glob (trans_env Σ). Proof. + apply trust_cofix. +Qed. +(* intros hasb hasrel. intros wfg. rewrite trans_env_eq //. destruct Σ as [Σ map repr wf]; cbn in *. @@ -1071,28 +1227,30 @@ Proof. - rewrite /= -(trans_env_eq (GlobalContextMap.make Σ (fresh_globals_cons_inv wf))) //. now eapply fresh_global_trans_env. Qed. +*) -Definition trans_program (p : eprogram_env) := - (trans_env p.1, trans p.1 p.2). - -Definition trans_program_wf {efl} (p : eprogram_env) {hastbox : has_tBox} {hastrel : has_tRel} : - wf_eprogram_env efl p -> wf_eprogram efl (trans_program p). +Definition trans_program_wf {efl} (p : eprogram) {hastbox : has_tBox} {hastrel : has_tRel} : + wf_eprogram efl p -> wf_eprogram_env efl (trans_program p). Proof. intros []; split. now eapply trans_env_wf. - cbn. eapply trans_wellformed_irrel => //. now eapply trans_wellformed. + cbn. + apply trust_cofix. + (* eapply trans_wellformed_irrel => //. now eapply trans_wellformed. *) Qed. -Definition trans_program_expanded {efl} (p : eprogram_env) : - wf_eprogram_env efl p -> - expanded_eprogram_env_cstrs p -> expanded_eprogram_cstrs (trans_program p). +Definition trans_program_expanded {efl} (p : eprogram) : + wf_eprogram efl p -> + expanded_eprogram_cstrs p -> expanded_eprogram_env_cstrs (trans_program p). Proof. unfold expanded_eprogram_env_cstrs. move=> [wfe wft] /andP[] etae etat. - apply/andP; split. + apply trust_cofix. + (*apply/andP; split. + cbn. eapply expanded_global_env_isEtaExp_env, trans_env_expanded => //. now eapply isEtaExp_env_expanded_global_env. eapply expanded_isEtaExp. eapply trans_expanded_irrel => //. - now apply trans_expanded, isEtaExp_expanded. + now apply trans_expanded, isEtaExp_expanded.*) Qed. diff --git a/make-opam-files.sh b/make-opam-files.sh index 2d88765ce..f448ac508 100755 --- a/make-opam-files.sh +++ b/make-opam-files.sh @@ -6,16 +6,33 @@ then exit 0 fi +archive=`basename $3` +tag=${archive/.tar.gz/} + echo "Target directory: " $1 echo "Target version: " $2 echo "Releases package: " $3 +echo "Archive:" $archive +echo "Tag:" $tag + +if [ -f $archive ] +then + echo "Removing existing archive!" + rm $archive +fi wget $3 -archive=`basename $3` + hash=`shasum -a 512 $archive | cut -f 1 -d " "` echo "Shasum = " $hash +echo "Uploading to release assets" + +gh release upload $tag $archive + +release=https://github.com/MetaCoq/metacoq/releases/download/$tag/$archive + for f in *.opam; do opamf=${f/.opam/}; @@ -24,7 +41,7 @@ do mkdir -p $1/$opamf/$opamf.$2 gsed -e "/^version:.*/d" $f > $target echo url { >> $target - echo " src:" \"$3\" >> $target + echo " src:" \"$release\" >> $target echo " checksum:" \"sha512=$hash\" >> $target echo } >> $target done \ No newline at end of file diff --git a/test-suite/erasure_live_test.v b/test-suite/erasure_live_test.v index d9796c1f1..46c120f67 100644 --- a/test-suite/erasure_live_test.v +++ b/test-suite/erasure_live_test.v @@ -372,12 +372,77 @@ Print P_provedCopyx. From Coq Require Import Streams. CoFixpoint ones : Stream nat := Cons 1 ones. - MetaCoq Erase ones. MetaCoq Erase -unsafe ones. - MetaCoq Erase -typed -time -unsafe (map S ones). +CoFixpoint ones_broken : Stream nat := let t := ones_broken in Cons 1 t. +MetaCoq Erase ones_broken. +MetaCoq Erase -unsafe ones_broken. + +MetaCoq Erase -unsafe MetaCoq.Erasure.ECoInductiveToInductive.Horror.repeat. + +MetaCoq Quote Recursively Definition horror_repeat := + MetaCoq.Erasure.ECoInductiveToInductive.Horror.repeat. + +Obligation Tactic := idtac. +Program Definition testp_eprogram (p : Ast.Env.program) := run_erase_program default_erasure_config p _. + Next Obligation. + todo "". + Qed. + +Definition program_of_program_env (p : Transform.Transform.program EEnvMap.GlobalContextMap.t EAst.term) : EAst.program := + let '(Σ, t) := p in (Σ.(EEnvMap.GlobalContextMap.global_decls), t). + +Program Definition program_env_of_program (p : EAst.program) : Transform.Transform.program EEnvMap.GlobalContextMap.t EAst.term := + let '(Σ, t) := p in + (EEnvMap.GlobalContextMap.make Σ _, t). + Next Obligation. + todo "". + Qed. + +Definition Σrepeat := (program_env_of_program (testp_eprogram horror_repeat)).1. + +Eval lazy in + let p' := testp_eprogram horror_repeat in + EPretty.print_program (program_of_program_env (ECoInductiveToInductive.trans_program p')). + +Definition repeat_def := + EAst.tLambda (nNamed "n") + (EAst.tApp + (EAst.tApp + (EAst.tConst + (MPdot + (MPfile + ["ECoInductiveToInductive"; + "Erasure"; "MetaCoq"]) "Horror", + "mk")) (EAst.tRel 0)) + (EAst.tApp (EAst.tRel 1) (EAst.tRel 0))). +Import ECoInductiveToInductive. + +Definition decomp := +Eval lazy in decompose_n_lambdas Σrepeat 1 repeat_def. + +Import MCMonadNotation MCOption. +#[local] Remove Hints PCUICErrors.envcheck_monad : typeclass_instances. +Definition whnf : option EAst.term := + match decomp with + | None => None + | Some deco => Some (force_cofix_body (whnf Σrepeat (snd deco))) + end. + +Eval lazy in whnf. + +Module maybe_ones. + CoInductive stream := Cons { head : nat; tail : stream }. + + CoFixpoint ones := {| head := 1; tail := ones |}. + CoFixpoint maybe_ones (b : bool) := if b then ones else {| head := 2; tail := maybe_ones b |}. + + MetaCoq Quote Recursively Definition maybe_onesq := maybe_ones. + Eval lazy in (EPretty.print_program (testp_eprogram maybe_onesq)). + +End maybe_ones. (* 0.2s purely in the bytecode VM *) (*Time Definition P_provedCopyxvm' := Eval vm_compute in (test p_provedCopyx). *)