aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--_CoqProject3
-rw-r--r--src/Compilers/GeneralizeVar.v10
-rw-r--r--src/Compilers/GeneralizeVarWf.v36
-rw-r--r--src/Compilers/Z/GeneralizeVar.v15
-rw-r--r--src/Compilers/Z/GeneralizeVarInterp.v23
-rw-r--r--src/Compilers/Z/GeneralizeVarWf.v30
6 files changed, 88 insertions, 29 deletions
diff --git a/_CoqProject b/_CoqProject
index e8d3b792d..0752ce47e 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -161,6 +161,9 @@ src/Compilers/Z/CommonSubexpressionElimination.v
src/Compilers/Z/CommonSubexpressionEliminationInterp.v
src/Compilers/Z/CommonSubexpressionEliminationWf.v
src/Compilers/Z/FoldTypes.v
+src/Compilers/Z/GeneralizeVar.v
+src/Compilers/Z/GeneralizeVarInterp.v
+src/Compilers/Z/GeneralizeVarWf.v
src/Compilers/Z/HexNotationConstants.v
src/Compilers/Z/Inline.v
src/Compilers/Z/InlineConstAndOp.v
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.
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 21:16:18 +0000