diff options
| -rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v | 95 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v | 4 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 50 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesGood.v | 4 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterRulesInterpGood.v | 4 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf1.v | 37 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/RewriterWf2.v | 39 | ||||
| -rw-r--r-- | src/Experiments/NewPipeline/nbe_rewrite_head.out | 14 |
8 files changed, 82 insertions, 165 deletions
diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v index 37db3be83..43c8eb813 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.v @@ -1120,13 +1120,13 @@ def to_type_var(name, ty): 'type': name, 'type.type base.type': name})[ty] -retcode += addnewline((r"""%sDefinition type_vars {t} (idc : ident t) : list type - := match idc with - | %s - end%%type. -""" % (indent1, - '\n | '.join('@' + pctor + ' => [' + '; '.join(to_type_var(n, t) for n, t in named_ttype) + ']' - for pctor, named_ttype in zip(pctors_with_args, named_ttypes)))).replace('\n', '\n' + indent1)) +#retcode += addnewline((r"""%sDefinition type_vars {t} (idc : ident t) : list type +# := match idc with +# | %s +# end%%type. +#""" % (indent1, +# '\n | '.join('@' + pctor + ' => [' + '; '.join(to_type_var(n, t) for n, t in named_ttype) + ']' +# for pctor, named_ttype in zip(pctors_with_args, named_ttypes)))).replace('\n', '\n' + indent1)) retcode += addnewline((r"""%sDefinition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm) := match idc in ident t return type_of_list (arg_types idc) -> %sident.ident (pattern.type.subst_default t evm) with @@ -2164,87 +2164,6 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f: | @fancy_addm => [] end%type. - Definition type_vars {t} (idc : ident t) : list type - := match idc with - | @Literal t => [type.base (base.type.type_base t)] - | @Nat_succ => [] - | @Nat_pred => [] - | @Nat_max => [] - | @Nat_mul => [] - | @Nat_add => [] - | @Nat_sub => [] - | @nil t => [type.base t] - | @cons t => [type.base t] - | @pair A B => [type.base A; type.base B] - | @fst A B => [type.base A; type.base B] - | @snd A B => [type.base A; type.base B] - | @prod_rect A B T => [type.base A; type.base B; type.base T] - | @bool_rect T => [type.base T] - | @nat_rect P => [type.base P] - | @nat_rect_arrow P Q => [type.base P; type.base Q] - | @list_rect A P => [type.base A; type.base P] - | @list_case A P => [type.base A; type.base P] - | @List_length T => [type.base T] - | @List_seq => [] - | @List_firstn A => [type.base A] - | @List_skipn A => [type.base A] - | @List_repeat A => [type.base A] - | @List_combine A B => [type.base A; type.base B] - | @List_map A B => [type.base A; type.base B] - | @List_app A => [type.base A] - | @List_rev A => [type.base A] - | @List_flat_map A B => [type.base A; type.base B] - | @List_partition A => [type.base A] - | @List_fold_right A B => [type.base A; type.base B] - | @List_update_nth T => [type.base T] - | @List_nth_default T => [type.base T] - | @Z_add => [] - | @Z_mul => [] - | @Z_pow => [] - | @Z_sub => [] - | @Z_opp => [] - | @Z_div => [] - | @Z_modulo => [] - | @Z_log2 => [] - | @Z_log2_up => [] - | @Z_eqb => [] - | @Z_leb => [] - | @Z_geb => [] - | @Z_of_nat => [] - | @Z_to_nat => [] - | @Z_shiftr => [] - | @Z_shiftl => [] - | @Z_land => [] - | @Z_lor => [] - | @Z_bneg => [] - | @Z_lnot_modulo => [] - | @Z_mul_split => [] - | @Z_add_get_carry => [] - | @Z_add_with_carry => [] - | @Z_add_with_get_carry => [] - | @Z_sub_get_borrow => [] - | @Z_sub_with_get_borrow => [] - | @Z_zselect => [] - | @Z_add_modulo => [] - | @Z_rshi => [] - | @Z_cc_m => [] - | @Z_cast => [] - | @Z_cast2 => [] - | @fancy_add => [] - | @fancy_addc => [] - | @fancy_sub => [] - | @fancy_subb => [] - | @fancy_mulll => [] - | @fancy_mullh => [] - | @fancy_mulhl => [] - | @fancy_mulhh => [] - | @fancy_rshi => [] - | @fancy_selc => [] - | @fancy_selm => [] - | @fancy_sell => [] - | @fancy_addm => [] - end%type. - Definition to_typed {t} (idc : ident t) (evm : EvarMap) : type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm) := match idc in ident t return type_of_list (arg_types idc) -> Compilers.ident.ident (pattern.type.subst_default t evm) with | @Literal t => fun arg => let '(v, _) := eta2r arg in @Compilers.ident.Literal _ v diff --git a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v index c877c3898..48ac11ce6 100644 --- a/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v +++ b/src/Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.v @@ -149,10 +149,12 @@ Module Compilers. : @eta_ident_cps T t idc f = f t idc. Proof. cbv [eta_ident_cps]; break_innermost_match; reflexivity. Qed. +(* Lemma is_simple_strip_types_iff_type_vars_nil {t} idc : Raw.ident.is_simple (@strip_types t idc) = true <-> type_vars idc = List.nil. Proof. destruct idc; cbn; intuition congruence. Qed. +*) Lemma unify_to_typed {t t' pidc idc} : forall v, @@ -200,6 +202,7 @@ Module Compilers. | progress Compilers.type.inversion_type ]. Qed. + (* Local Ltac solve_ex_or_eq := lazymatch goal with | [ |- ex _ ] => eexists; solve_ex_or_eq @@ -226,6 +229,7 @@ Module Compilers. | progress destruct_head'_or | solve_ex_or_eq ]. Qed. + *) End ident. End pattern. End Compilers. diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 767404e01..6937a8076 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -338,12 +338,12 @@ Module Compilers. | App s d f x => Raw.App (@to_raw _ _ to_raw_ident _ f) (@to_raw _ _ to_raw_ident _ x) end. - Fixpoint collect_vars {ident} {ident_collect_vars : forall t, ident t -> PositiveSet.t} + Fixpoint collect_vars {ident} {t} (p : @pattern ident t) : PositiveSet.t := match p with | Wildcard t => type.collect_vars t - | Ident t idc => ident_collect_vars t idc - | App s d f x => PositiveSet.union (@collect_vars _ ident_collect_vars _ x) (@collect_vars _ ident_collect_vars _ f) + | Ident t idc => type.collect_vars t + | App s d f x => PositiveSet.union (@collect_vars _ _ x) (@collect_vars _ _ f) end. Notation ident := ident.ident. @@ -471,7 +471,6 @@ Module Compilers. {raw_pident : Type} (strip_types : forall t, pident t -> raw_pident) (raw_pident_beq : raw_pident -> raw_pident -> bool) - (type_vars_of_pident : forall t, pident t -> list (type.type pattern.base.type)) (full_types : raw_pident -> Type) (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc)) @@ -704,13 +703,9 @@ Module Compilers. (@under_with_unification_resultT' _ _ x evm _ _ F) end. - Definition ident_collect_vars := (fun t idc => fold_right PositiveSet.union PositiveSet.empty (List.map pattern.type.collect_vars (type_vars_of_pident t idc))). - Definition with_unification_resultT {var t} (p : pattern t) (K : type -> Type) : Type := pattern.type.forall_vars - (@pattern.collect_vars - _ ident_collect_vars - t p) + (@pattern.collect_vars _ t p) (fun evm => @with_unification_resultT' var t p evm (K (pattern.type.subst_default t evm))). Definition unification_resultT {var t} (p : pattern t) : Type @@ -1182,6 +1177,10 @@ Module Compilers. := eta_ident_cps _ _ idc (fun t' idc' => assemble_identifier_rewriters' t' (rIdent true idc' #idc') (fun _ => id)). End with_do_again. End with_var. + Global Arguments rew_should_do_again {_ _ _ _ _ _} _. + Global Arguments rew_with_opt {_ _ _ _ _ _} _. + Global Arguments rew_under_lets {_ _ _ _ _ _} _. + Global Arguments rew_replacement {_ _ _ _ _ _} _. Section full. Context {var : type.type base.type -> Type}. @@ -1249,15 +1248,14 @@ Module Compilers. Coercion ptype_base' : base.type.base >-> ptype. Coercion type_base : base.type >-> type. Coercion ptype_base : pattern.base.type >-> ptype. - Local Notation ident_collect_vars := (@ident_collect_vars pattern.ident (@pattern.ident.type_vars)). - Local Notation collect_vars := (@pattern.collect_vars pattern.ident (@ident_collect_vars)). + Local Notation collect_vars := (@pattern.collect_vars pattern.ident). Local Notation with_unification_resultT' := (@with_unification_resultT' pattern.ident (@pattern.ident.arg_types) value). - Local Notation with_unification_resultT := (@with_unification_resultT pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) value). + Local Notation with_unification_resultT := (@with_unification_resultT pattern.ident (@pattern.ident.arg_types) value). Local Notation under_with_unification_resultT' := (@under_with_unification_resultT' pattern.ident (@pattern.ident.arg_types) value). - Local Notation under_with_unification_resultT := (@under_with_unification_resultT pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) value). - Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). - Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). - Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). + Local Notation under_with_unification_resultT := (@under_with_unification_resultT pattern.ident (@pattern.ident.arg_types) value). + Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types)). + Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types)). + Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types)). Definition make_base_Literal_pattern (t : base.type.base) : pattern t := Eval cbv [pattern.ident.of_typed_ident] in @@ -1493,14 +1491,14 @@ Module Compilers. Coercion ptype_base' : base.type.base >-> ptype. Coercion type_base : base.type >-> type. Coercion ptype_base : pattern.base.type >-> ptype. - Local Notation Build_rewrite_rule_data := (@Build_rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). + Local Notation Build_rewrite_rule_data := (@Build_rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types)). Local Notation Build_anypattern := (@pattern.Build_anypattern pattern.ident). - Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). - Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). - Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)). + Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types)). + Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types)). + Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pattern.ident (@pattern.ident.arg_types)). Definition pident_unify_unknown := @pattern.ident.unify. Definition invert_bind_args_unknown := @pattern.Raw.ident.invert_bind_args. - Local Notation assemble_identifier_rewriters := (@assemble_identifier_rewriters ident var (@pattern.ident.eta_ident_cps) (@pattern.ident) (@pattern.ident.arg_types) (@pattern.ident.unify) pident_unify_unknown pattern.Raw.ident (@pattern.ident.type_vars) (@pattern.Raw.ident.full_types) (@pattern.Raw.ident.invert_bind_args) invert_bind_args_unknown (@pattern.Raw.ident.type_of) (@pattern.Raw.ident.to_typed) pattern.Raw.ident.is_simple). + Local Notation assemble_identifier_rewriters := (@assemble_identifier_rewriters ident var (@pattern.ident.eta_ident_cps) (@pattern.ident) (@pattern.ident.arg_types) (@pattern.ident.unify) pident_unify_unknown pattern.Raw.ident (@pattern.Raw.ident.full_types) (@pattern.Raw.ident.invert_bind_args) invert_bind_args_unknown (@pattern.Raw.ident.type_of) (@pattern.Raw.ident.to_typed) pattern.Raw.ident.is_simple). Delimit Scope rewrite_scope with rewrite. Delimit Scope rewrite_opt_scope with rewrite_opt. @@ -1959,11 +1957,11 @@ Module Compilers. ]. Definition nbe_dtree' - := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 nbe_rewrite_rules. + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 nbe_rewrite_rules. Definition arith_dtree' - := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 (arith_rewrite_rules 0%Z (* dummy val *)). + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 (arith_rewrite_rules 0%Z (* dummy val *)). Definition arith_with_casts_dtree' - := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 arith_with_casts_rewrite_rules. + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 arith_with_casts_rewrite_rules. Definition nbe_dtree : decision_tree := Eval compute in invert_Some nbe_dtree'. Definition arith_dtree : decision_tree @@ -2186,11 +2184,11 @@ Z.mul @@ (?x >> 128, ?y >> 128) --> mulhh @@ (x, y) := []. Definition fancy_dtree' - := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_rewrite_rules. + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_rewrite_rules. Definition fancy_dtree : decision_tree := Eval compute in invert_Some fancy_dtree'. Definition fancy_with_casts_dtree' - := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq (@pattern.ident.type_vars) 100 fancy_with_casts_rewrite_rules. + := Eval compute in @compile_rewrites ident var pattern.ident (@pattern.ident.arg_types) pattern.Raw.ident (@pattern.ident.strip_types) pattern.Raw.ident.ident_beq 100 fancy_with_casts_rewrite_rules. Definition fancy_with_casts_dtree : decision_tree := Eval compute in invert_Some fancy_with_casts_dtree'. Definition fancy_default_fuel := Eval compute in List.length fancy_rewrite_rules. diff --git a/src/Experiments/NewPipeline/RewriterRulesGood.v b/src/Experiments/NewPipeline/RewriterRulesGood.v index 359459764..fd7facb3d 100644 --- a/src/Experiments/NewPipeline/RewriterRulesGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesGood.v @@ -80,7 +80,7 @@ Module Compilers. Section good. Context {var1 var2 : type -> Type}. - Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) var1 var2). + Local Notation rewrite_rules_goodT := (@Compile.rewrite_rules_goodT ident pattern.ident (@pattern.ident.arg_types) var1 var2). Lemma wf_rlist_rect_gen {ivar1 ivar2 A P} @@ -214,7 +214,7 @@ Module Compilers. end; (exists eq_refl); cbn [eq_rect]; - cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq]; + cbv [Compile.wf_deep_rewrite_ruleTP_gen Compile.wf_rewrite_rule_data_curried Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unif_rewrite_ruleTP_gen_curried Compile.wf_with_unification_resultT pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.wf_maybe_under_lets_expr Compile.wf_maybe_do_again_expr Compile.wf_with_unification_resultT pattern.type.under_forall_vars_relation Compile.with_unification_resultT' pattern.collect_vars pattern.type.collect_vars pattern.base.collect_vars PositiveSet.empty PositiveSet.elements Compile.under_type_of_list_relation_cps pattern.ident.arg_types pattern.type.subst_default pattern.base.subst_default PositiveSet.rev PositiveMap.empty Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.maybe_option_eq]; cbn [List.map List.fold_right PositiveSet.union PositiveSet.xelements List.rev List.app projT1 projT2 list_rect PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add PositiveMap.find orb]; repeat first [ progress intros | match goal with diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v index 88a4f6670..b002bfcb2 100644 --- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v +++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v @@ -99,12 +99,12 @@ Module Compilers. rewrite UnderLets.interp_splice, IHxs; reflexivity. Qed. - Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) (@pattern.ident.to_typed) (@ident_interp)). + Local Notation rewrite_rules_interp_goodT := (@Compile.rewrite_rules_interp_goodT ident pattern.ident (@pattern.ident.arg_types) (@pattern.ident.to_typed) (@ident_interp)). Local Ltac do_cbv0 := cbv [id Compile.rewrite_rules_interp_goodT_curried - Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related]. + Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compilers.pattern.type.lam_forall_vars_gen Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related]. Local Ltac do_cbv := do_cbv0; cbv [List.map List.fold_right List.rev list_rect orb List.app]. diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v index 967921da5..8d42eb8e5 100644 --- a/src/Experiments/NewPipeline/RewriterWf1.v +++ b/src/Experiments/NewPipeline/RewriterWf1.v @@ -801,7 +801,6 @@ Module Compilers. {raw_pident : Type} (strip_types : forall t, pident t -> raw_pident) (raw_pident_beq : raw_pident -> raw_pident -> bool) - (type_vars_of_pident : forall t, pident t -> list (type.type pattern.base.type)) (full_types : raw_pident -> Type) (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc)) @@ -848,9 +847,9 @@ Module Compilers. Local Notation unify_pattern' var := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown). Local Notation unify_pattern var := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown). Local Notation app_transport_with_unification_resultT'_cps := (@app_transport_with_unification_resultT'_cps pident pident_arg_types). - Local Notation app_with_unification_resultT_cps := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident). + Local Notation app_with_unification_resultT_cps := (@app_with_unification_resultT_cps pident pident_arg_types). Local Notation with_unification_resultT' := (@with_unification_resultT' pident pident_arg_types). - Local Notation with_unification_resultT := (@with_unification_resultT pident pident_arg_types type_vars_of_pident). + Local Notation with_unification_resultT := (@with_unification_resultT pident pident_arg_types). Local Notation unification_resultT' := (@unification_resultT' pident pident_arg_types). Local Notation unification_resultT := (@unification_resultT pident pident_arg_types). @@ -1453,14 +1452,14 @@ Module Compilers. Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident var1 var2). Local Notation reify_and_let_binds_cps1 := (@reify_and_let_binds_cps ident var1 reify_and_let_binds_base_cps1). Local Notation reify_and_let_binds_cps2 := (@reify_and_let_binds_cps ident var2 reify_and_let_binds_base_cps2). - Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types type_vars_of_pident). - Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). - Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). - Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types type_vars_of_pident). - Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types type_vars_of_pident). + Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types). + Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types). + Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types). + Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types). + Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types). + Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types). Local Notation deep_rewrite_ruleTP_gen1 := (@deep_rewrite_ruleTP_gen ident var1). Local Notation deep_rewrite_ruleTP_gen2 := (@deep_rewrite_ruleTP_gen ident var2). Local Notation preunify_types1 := (@preunify_types ident var1 pident). @@ -1923,7 +1922,7 @@ Module Compilers. (r1 : @rewrite_rule_data1 t p) (r2 : @rewrite_rule_data2 t p) : Prop - := wf_with_unif_rewrite_ruleTP_gen G (rew_replacement _ _ r1) (rew_replacement _ _ r2). + := wf_with_unif_rewrite_ruleTP_gen G (rew_replacement r1) (rew_replacement r2). Definition rewrite_rules_goodT (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) @@ -1956,7 +1955,7 @@ Module Compilers. (r1 : @rewrite_rule_data1 t p) (r2 : @rewrite_rule_data2 t p) : Prop - := wf_with_unif_rewrite_ruleTP_gen_curried G (rew_replacement _ _ r1) (rew_replacement _ _ r2). + := wf_with_unif_rewrite_ruleTP_gen_curried G (rew_replacement r1) (rew_replacement r2). Definition rewrite_rules_goodT_curried (rew1 : rewrite_rulesT1) (rew2 : rewrite_rulesT2) @@ -2002,9 +2001,9 @@ Module Compilers. {ident_interp_Proper : forall t, Proper (eq ==> type.eqv) (ident_interp t)}. Local Notation var := (type.interp base.interp) (only parsing). Local Notation expr := (@expr.expr base.type ident var). - Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types type_vars_of_pident). - Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types type_vars_of_pident). - Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types type_vars_of_pident). + Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types). + Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types). + Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types). Local Notation normalize_deep_rewrite_rule := (@normalize_deep_rewrite_rule ident var). Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var). @@ -2251,9 +2250,9 @@ Module Compilers. => related_sigT_by_eq (fun evm => @deep_rewrite_ruleTP_gen_good_relation - (rew_should_do_again _ _ r) (rew_with_opt _ _ r) (rew_under_lets _ _ r) (pattern.type.subst_default t evm)) + (rew_should_do_again r) (rew_with_opt r) (rew_under_lets r) (pattern.type.subst_default t evm)) fx gy) - (app_with_unification_resultT_cps (rew_replacement _ _ r) x _ (@Some _)) + (app_with_unification_resultT_cps (rew_replacement r) x _ (@Some _)) (app_with_unification_resultT_cps (pattern_default_interp p) y _ (@Some _)). Definition rewrite_rules_interp_goodT @@ -2269,7 +2268,7 @@ Module Compilers. := under_with_unification_resultT_relation_hetero (fun _ => value_interp_related) (fun evm => deep_rewrite_ruleTP_gen_good_relation) - (rew_replacement _ _ r) + (rew_replacement r) (pattern_default_interp p). Definition rewrite_rules_interp_goodT_curried diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v index 42720bd38..ec6142103 100644 --- a/src/Experiments/NewPipeline/RewriterWf2.v +++ b/src/Experiments/NewPipeline/RewriterWf2.v @@ -63,7 +63,6 @@ Module Compilers. {raw_pident : Type} (strip_types : forall t, pident t -> raw_pident) (raw_pident_beq : raw_pident -> raw_pident -> bool) - (type_vars_of_pident : forall t, pident t -> list (type.type pattern.base.type)) (full_types : raw_pident -> Type) (invert_bind_args invert_bind_args_unknown : forall t (idc : ident t) (pidc : raw_pident), option (full_types pidc)) @@ -116,18 +115,18 @@ Module Compilers. Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident var1 var2). Local Notation reify_and_let_binds_cps1 := (@reify_and_let_binds_cps ident var1 reify_and_let_binds_base_cps1). Local Notation reify_and_let_binds_cps2 := (@reify_and_let_binds_cps ident var2 reify_and_let_binds_base_cps2). - Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types type_vars_of_pident). - Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). - Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation rewrite_rulesT1 := (@rewrite_rulesT ident var1 pident pident_arg_types). + Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types). + Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). + Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple). Local Notation with_unification_resultT'1 := (@with_unification_resultT' ident var1 pident pident_arg_types). Local Notation with_unification_resultT'2 := (@with_unification_resultT' ident var2 pident pident_arg_types). - Local Notation with_unification_resultT1 := (@with_unification_resultT ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation with_unification_resultT2 := (@with_unification_resultT ident var2 pident pident_arg_types type_vars_of_pident). - Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types type_vars_of_pident). - Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types type_vars_of_pident). - Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types type_vars_of_pident). + Local Notation with_unification_resultT1 := (@with_unification_resultT ident var1 pident pident_arg_types). + Local Notation with_unification_resultT2 := (@with_unification_resultT ident var2 pident pident_arg_types). + Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types). + Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types). + Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types). + Local Notation with_unif_rewrite_ruleTP_gen2 := (@with_unif_rewrite_ruleTP_gen ident var2 pident pident_arg_types). Local Notation wf_rawexpr := (@wf_rawexpr ident var1 var2). (** TODO: Move Me up *) Local Notation unify_pattern'1 := (@unify_pattern' ident var1 pident pident_arg_types pident_unify pident_unify_unknown). @@ -136,12 +135,12 @@ Module Compilers. Local Notation unify_pattern2 := (@unify_pattern ident var2 pident pident_arg_types pident_unify pident_unify_unknown). Local Notation wf_unification_resultT' := (@wf_unification_resultT' ident pident pident_arg_types var1 var2). Local Notation wf_unification_resultT := (@wf_unification_resultT ident pident pident_arg_types var1 var2). - Local Notation wf_with_unification_resultT := (@wf_with_unification_resultT ident pident pident_arg_types type_vars_of_pident var1 var2). - Local Notation wf_with_unif_rewrite_ruleTP_gen := (@wf_with_unif_rewrite_ruleTP_gen ident pident pident_arg_types type_vars_of_pident var1 var2). + Local Notation wf_with_unification_resultT := (@wf_with_unification_resultT ident pident pident_arg_types var1 var2). + Local Notation wf_with_unif_rewrite_ruleTP_gen := (@wf_with_unif_rewrite_ruleTP_gen ident pident pident_arg_types var1 var2). Local Notation wf_deep_rewrite_ruleTP_gen := (@wf_deep_rewrite_ruleTP_gen ident var1 var2). - Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident (@value var1)). - Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident (@value var2)). - Local Notation wf_app_with_unification_resultT := (@wf_app_with_unification_resultT ident pident pident_arg_types type_vars_of_pident var1 var2). + Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps pident pident_arg_types (@value var1)). + Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps pident pident_arg_types (@value var2)). + Local Notation wf_app_with_unification_resultT := (@wf_app_with_unification_resultT ident pident pident_arg_types var1 var2). (* Because [proj1] and [proj2] in the stdlib are opaque *) Local Notation proj1 x := (let (a, b) := x in a). @@ -541,8 +540,8 @@ Module Compilers. = UnderLets.Base (rew [A] p in v). Proof. case p; reflexivity. Defined. - Local Notation rewrite_rules_goodT := (@rewrite_rules_goodT ident pident pident_arg_types type_vars_of_pident var1 var2). - Local Notation wf_rewrite_rule_data := (@wf_rewrite_rule_data ident pident pident_arg_types type_vars_of_pident var1 var2). + Local Notation rewrite_rules_goodT := (@rewrite_rules_goodT ident pident pident_arg_types var1 var2). + Local Notation wf_rewrite_rule_data := (@wf_rewrite_rule_data ident pident pident_arg_types var1 var2). Local Notation wf_reflect := (@wf_reflect ident var1 var2). Local Notation wf_reify := (@wf_reify ident var1 var2). @@ -750,8 +749,8 @@ Module Compilers. -> expr.wf G' e1 e2 -> UnderLets.wf (fun G' => expr.wf G') G (@do_again1 t e1) (@do_again2 t e2)). - Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree). - Local Notation assemble_identifier_rewriters var := (@assemble_identifier_rewriters ident var eta_ident_cps pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree). + Local Notation assemble_identifier_rewriters' var := (@assemble_identifier_rewriters' ident var pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree). + Local Notation assemble_identifier_rewriters var := (@assemble_identifier_rewriters ident var eta_ident_cps pident pident_arg_types pident_unify pident_unify_unknown raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple dtree). Lemma wf_assemble_identifier_rewriters' G t re1 e1 re2 e2 K1 K2 diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/Experiments/NewPipeline/nbe_rewrite_head.out index cbd282f50..a60bdfeb4 100644 --- a/src/Experiments/NewPipeline/nbe_rewrite_head.out +++ b/src/Experiments/NewPipeline/nbe_rewrite_head.out @@ -408,8 +408,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with pattern.type.unify_extracted_cps (((((unit -> '1%pbtype) -> (ℕ -> '1%pbtype -> '1%pbtype) -> ℕ -> '1%pbtype) -> - unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) -> - ℕ)%ptype + unit -> '1%pbtype) -> ℕ -> '1%pbtype -> '1%pbtype) -> ℕ)%ptype (((((unit -> P) -> (ℕ -> P -> P) -> ℕ -> P) -> unit -> P) -> ℕ -> P -> P) -> (projT1 args))%ptype option (fun x2 : option => x2) @@ -466,11 +465,11 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with (((((('1%pbtype -> '2%pbtype) -> (ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> ℕ -> '1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> - ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> - ℕ) -> '1%pbtype)%ptype + ℕ -> ('1%pbtype -> '2%pbtype) -> '1%pbtype -> '2%pbtype) -> ℕ) -> + '1%pbtype)%ptype ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) -> - P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> - P)%ptype option (fun x3 : option => x3) + P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> P)%ptype + option (fun x3 : option => x3) with | Some (_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _), @@ -479,8 +478,7 @@ match idc in (Compilers.ident t) return (Compile.value' true t) with type.type_beq base.type base.type.type_beq ((((((b -> b16) -> (ℕ -> (b -> b16) -> b -> b16) -> ℕ -> b -> b16) -> - b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) -> - b)%ptype + b -> b16) -> ℕ -> (b -> b16) -> b -> b16) -> ℕ) -> b)%ptype ((((((P -> Q) -> (ℕ -> (P -> Q) -> P -> Q) -> ℕ -> P -> Q) -> P -> Q) -> ℕ -> (P -> Q) -> P -> Q) -> (projT1 args)) -> P)%ptype |