From 8a8afc11df5dfe4755b7dd4344b6a27d198bd2e1 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 13 Nov 2017 15:36:38 -0500 Subject: Update GeneralizeVar to ensure Wf This will hopefully pave the way for not needing to prove Wf anywhere in the bounds pipeline. --- src/Compilers/GeneralizeVar.v | 10 ++++++++++ src/Compilers/GeneralizeVarWf.v | 36 +++++++---------------------------- src/Compilers/Z/GeneralizeVar.v | 15 +++++++++++++++ src/Compilers/Z/GeneralizeVarInterp.v | 23 ++++++++++++++++++++++ src/Compilers/Z/GeneralizeVarWf.v | 30 +++++++++++++++++++++++++++++ 5 files changed, 85 insertions(+), 29 deletions(-) create mode 100644 src/Compilers/Z/GeneralizeVar.v create mode 100644 src/Compilers/Z/GeneralizeVarInterp.v create mode 100644 src/Compilers/Z/GeneralizeVarWf.v (limited to 'src/Compilers') diff --git a/src/Compilers/GeneralizeVar.v b/src/Compilers/GeneralizeVar.v index 882d8137b..d73c3efd2 100644 --- a/src/Compilers/GeneralizeVar.v +++ b/src/Compilers/GeneralizeVar.v @@ -6,6 +6,7 @@ Require Import Crypto.Compilers.Named.InterpretToPHOAS. Require Import Crypto.Compilers.Named.Compile. Require Import Crypto.Compilers.Named.PositiveContext. Require Import Crypto.Compilers.Named.PositiveContext.Defaults. +Require Import Crypto.Compilers.Named.Wf. Require Import Crypto.Compilers.Syntax. (** N.B. This procedure only works when there are no nested lets, @@ -24,6 +25,15 @@ Section language. Definition GeneralizeVar {t} (e : @Syntax.expr base_type_code op (fun _ => FMapPositive.PositiveMap.key) t) : option (@Syntax.Expr base_type_code op (domain t -> codomain t)) := let e := compile e (default_names_for (fun _ => 1%positive) e) in + let e := match e with + | Some e + => match wf_unit (Context:=PContext _) empty e with + | Some PointedProp.trivial => Some e + | Some (PointedProp.inject _) => None + | None => None + end + | None => None + end in let e := option_map (InterpToPHOAS (Context:=fun var => PContext var) failb) e in e. End language. diff --git a/src/Compilers/GeneralizeVarWf.v b/src/Compilers/GeneralizeVarWf.v index 8d504eff0..9815d5092 100644 --- a/src/Compilers/GeneralizeVarWf.v +++ b/src/Compilers/GeneralizeVarWf.v @@ -5,7 +5,7 @@ Require Import Crypto.Compilers.Named.Context. Require Import Crypto.Compilers.Named.Syntax. Require Import Crypto.Compilers.Named.ContextDefinitions. Require Import Crypto.Compilers.Named.InterpretToPHOASWf. -Require Import Crypto.Compilers.Named.CompileWf. +Require Import Crypto.Compilers.Named.WfFromUnit. Require Import Crypto.Compilers.Named.PositiveContext. Require Import Crypto.Compilers.Named.PositiveContext.Defaults. Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties. @@ -44,12 +44,10 @@ Section language. Defined. Local Arguments Compile.compile : simpl never. - Lemma Wf_GeneralizeVar' - {var'} {make_var' : forall t, var' t} - {t} (e1 e2 : expr base_type_code op t) + Lemma Wf_GeneralizeVar + {t} (e1 : expr base_type_code op t) e' (He' : GeneralizeVar e1 = Some e') - (Hwf : wf (var2:=var') e1 e2) : Wf e'. Proof using base_type_code_lb. unfold GeneralizeVar, option_map in *. @@ -63,37 +61,17 @@ Section language. (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent) PositiveContextOk PositiveContextOk (failb _) (failb _) _ _); - eapply (wf_compile (ContextOk:=PositiveContextOk) (make_var':=fun t _ => make_var' t)); - try eassumption; - auto using name_list_unique_default_names_for. - Qed. - - Lemma Wf_GeneralizeVar - {t} (e : expr base_type_code op t) - e' - (He' : GeneralizeVar e = Some e') - (Hwf : wf e e) - : Wf e'. - Proof using base_type_code_lb. - eapply @Wf_GeneralizeVar'; eauto; intros; exact 1%positive. + [ revert v | revert v' ]; + refine (_ : Wf.Named.Wf _ e); + apply Wf_from_unit; auto using PositiveContextOk. Qed. - Lemma Wf_GeneralizeVar'_arrow - {var'} {make_var' : forall t, var' t} - {s d} (e1 e2 : expr base_type_code op (Arrow s d)) - e' - (He' : GeneralizeVar e1 = Some e') - (Hwf : wf (var2:=var') e1 e2) - : Wf e'. - Proof using base_type_code_lb. eapply @Wf_GeneralizeVar'; eassumption. Qed. - Lemma Wf_GeneralizeVar_arrow {s d} (e : expr base_type_code op (Arrow s d)) e' (He' : GeneralizeVar e = Some e') - (Hwf : wf e e) : Wf e'. Proof using base_type_code_lb. eapply Wf_GeneralizeVar; eassumption. Qed. End language. -Hint Resolve Wf_GeneralizeVar Wf_GeneralizeVar_arrow Wf_GeneralizeVar' Wf_GeneralizeVar'_arrow : wf. +Hint Resolve Wf_GeneralizeVar Wf_GeneralizeVar_arrow : wf. diff --git a/src/Compilers/Z/GeneralizeVar.v b/src/Compilers/Z/GeneralizeVar.v new file mode 100644 index 000000000..5431dd77a --- /dev/null +++ b/src/Compilers/Z/GeneralizeVar.v @@ -0,0 +1,15 @@ +(** * Generalize [var] in [exprf] *) +Require Import Coq.ZArith.BinInt. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.GeneralizeVar. +Require Import Crypto.Compilers.Z.Syntax. + +(** N.B. This procedure only works when there are no nested lets, + i.e., nothing like [let x := let y := z in w] in the PHOAS syntax + tree. This is a limitation of [compile]. *) + +Definition GeneralizeVar {t} (e : @Syntax.expr base_type op _ t) + : option (@Z.Syntax.Expr (domain t -> codomain t)) + := @GeneralizeVar base_type op base_type_beq internal_base_type_dec_bl + (fun _ t => Op (OpConst 0%Z) TT) + t e. diff --git a/src/Compilers/Z/GeneralizeVarInterp.v b/src/Compilers/Z/GeneralizeVarInterp.v new file mode 100644 index 000000000..a361e24fd --- /dev/null +++ b/src/Compilers/Z/GeneralizeVarInterp.v @@ -0,0 +1,23 @@ +Require Import Coq.ZArith.BinInt. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.GeneralizeVarInterp. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.GeneralizeVar. + +Definition InterpGeneralizeVar + {interp_base_type} + {interp_op} + {t} (e : Expr t) + (Hwf : Wf e) + e' + (He' : GeneralizeVar (e _) = Some e') + : forall v, Compilers.Syntax.Interp (interp_base_type:=interp_base_type) interp_op e' v + = Compilers.Syntax.Interp interp_op e v + := @InterpGeneralizeVar + base_type op base_type_beq internal_base_type_dec_bl + internal_base_type_dec_lb + (fun _ t => Op (OpConst 0%Z) TT) + interp_base_type + interp_op + t e Hwf e' He'. diff --git a/src/Compilers/Z/GeneralizeVarWf.v b/src/Compilers/Z/GeneralizeVarWf.v new file mode 100644 index 000000000..d0d97e3c9 --- /dev/null +++ b/src/Compilers/Z/GeneralizeVarWf.v @@ -0,0 +1,30 @@ +Require Import Coq.ZArith.BinInt. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.GeneralizeVarWf. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.GeneralizeVar. + +Definition Wf_GeneralizeVar + {t} (e1 : expr base_type op t) + e' + (He' : GeneralizeVar e1 = Some e') + : Wf e' + := @Wf_GeneralizeVar + base_type op base_type_beq internal_base_type_dec_bl + internal_base_type_dec_lb + (fun _ t => Op (OpConst 0%Z) TT) + t e1 e' He'. + +Definition Wf_GeneralizeVar_arrow + {s d} (e : expr base_type op (Arrow s d)) + e' + (He' : GeneralizeVar e = Some e') + : Wf e' + := @Wf_GeneralizeVar_arrow + base_type op base_type_beq internal_base_type_dec_bl + internal_base_type_dec_lb + (fun _ t => Op (OpConst 0%Z) TT) + s d e e' He'. + +Hint Resolve Wf_GeneralizeVar Wf_GeneralizeVar_arrow : wf. -- cgit v1.2.3