From fbe0d0cb97e8fb69a13448b8245d0c1da8f55009 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 30 Apr 2018 14:53:43 -0400 Subject: Revert "WIP on inductive base_value" This reverts commit e38faaac1d3996c61d396144e20b8bb41809a253. --- src/Experiments/PartialEvaluationWithLetIn.v | 71 ++++++++++++++++------------ 1 file changed, 42 insertions(+), 29 deletions(-) (limited to 'src') diff --git a/src/Experiments/PartialEvaluationWithLetIn.v b/src/Experiments/PartialEvaluationWithLetIn.v index 3e3976c4e..7b854af21 100644 --- a/src/Experiments/PartialEvaluationWithLetIn.v +++ b/src/Experiments/PartialEvaluationWithLetIn.v @@ -375,14 +375,15 @@ Module partial. (ident_Fst : forall A B, pident (#A * #B -> #A)%ptype) (ident_Snd : forall A B, pident (#A * #B -> #B)%ptype). - Inductive base_value : type -> Type := - | Ident {t} (idc : ident t) : base_value t - | App {s d} (f : base_value (s -> d)) (x : base_value s) : base_value d - | Expr {t} (st : abstract_domain' t) (e : @expr var t) : base_value t. - - Fixpoint abstraction_function {t : base.type} (v : base_value t) : abstract_domain' t. - Admitted. - (*refine + Fixpoint base_value (t : base.type) + := match t return Type with + | base.type.nat as t + => nat + | base.type.prod A B as t + => (abstract_domain' A * @expr var A + base_value A) * (abstract_domain' B * @expr var B + base_value B) + end%type. + + Fixpoint abstraction_function {t} : base_value t -> abstract_domain' t := match t return base_value t -> abstract_domain' t with | base.type.nat => fun v => abstract_interp_ident _ (ident_Literal v) @@ -398,24 +399,38 @@ Module partial. end in abstract_interp_ident _ (ident_Pair A B) sta stb - end.*) - - Fixpoint base_reify {t} (v : base_value t) : @expr var t - := match v in base_value t return expr t with - | Ident t idc => ###idc - | App s d f x => @base_reify _ f @ (@base_reify _ x) - | Expr t st e => match annotate _ st with - | None => e - | Some cst => ###cst @ e - end - end%expr. + end. + + Fixpoint base_reify {t} : base_value t -> @expr var t + := match t return base_value t -> expr t with + | base.type.nat + => fun v => expr.Ident (ident.wrap (ident_Literal v)) + | base.type.prod A B + => fun '(a, b) + => let ea := match a with + | inl (st, e) + => match annotate _ st with + | None => e + | Some cst => ###cst @ e + end%expr + | inr v => @base_reify _ v + end in + let eb := match b with + | inl (st, e) + => match annotate _ st with + | None => e + | Some cst => ###cst @ e + end%expr + | inr v => @base_reify _ v + end in + (#(ident_Pair A B) @ ea @ eb)%expr + end. Local Notation value := (@value base.type ident var base_value abstract_domain'). Context (half_interp : forall {t} (idc : pident t), parametric.half_interp UnderLets value t). - Fixpoint intersect_state_base_value {t} : abstract_domain' t -> base_value t -> base_value t. - Admitted. (* + Fixpoint intersect_state_base_value {t} : abstract_domain' t -> base_value t -> base_value t := match t return abstract_domain' t -> base_value t -> base_value t with | base.type.nat => update_literal_with_state | base.type.prod _ _ @@ -431,7 +446,7 @@ Module partial. | inr v => inr (@intersect_state_base_value _ stb v) end in (a', b') - end.*) + end. Definition intersect_state_value {t} : abstract_domain t -> value t -> value t @@ -446,10 +461,10 @@ Module partial. end. Local Notation reify := (@reify base.type ident var base_value abstract_domain' annotate bottom' (@abstraction_function) (@base_reify)). + Print reflect. Local Notation reflect := (@reflect base.type ident var base_value abstract_domain' annotate bottom' (@abstraction_function) (@base_reify)). - Fixpoint pinterp_base {t : parametric.base.type} : parametric.half_interp UnderLets value (type.base t) -> value (parametric.subst (type.base t)). - Admitted. (* + Fixpoint pinterp_base {t : parametric.base.type} : parametric.half_interp UnderLets value (type.base t) -> value (parametric.subst (type.base t)) := match t return parametric.half_interp UnderLets value (type.base t) -> value (parametric.subst (type.base t)) with | parametric.base.type.nat => fun v => inr v @@ -457,11 +472,9 @@ Module partial. => fun '(a, b) => inr (@pinterp_base A a, @pinterp_base B b) | parametric.base.type.var_with_subst subst => fun v => v - end.*) + end. - Fixpoint puninterp_base {t : parametric.base.type} : value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t)). - Print parametric.half_interp. - Admitted. (* + Fixpoint puninterp_base {t : parametric.base.type} : value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t)) := match t return value (parametric.subst (type.base t)) -> option (parametric.half_interp UnderLets value (type.base t)) with | parametric.base.type.nat => fun v @@ -480,7 +493,7 @@ Module partial. end | parametric.base.type.var_with_subst subst => @Some _ - end%option.*) + end%option. (* FIXME: naming; these are basically just fancy identity functions *) Fixpoint vinterp_arrow {t : type} : value t -> @type.interpM base.type UnderLets value t -- cgit v1.2.3