From 0672c92921e45b942fa8a75c45457b8c7b32565d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 12 Dec 2018 14:15:35 -0500 Subject: Make unify_pattern' a bit stricter This way we have access to the hypothesis that the types are in the evar map, when doing the proofs --- src/Experiments/NewPipeline/Rewriter.v | 3 ++- src/Experiments/NewPipeline/nbe_rewrite_head.out | 14 ++++++++------ 2 files changed, 10 insertions(+), 7 deletions(-) diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v index 6937a8076..1acc614eb 100644 --- a/src/Experiments/NewPipeline/Rewriter.v +++ b/src/Experiments/NewPipeline/Rewriter.v @@ -780,8 +780,9 @@ Module Compilers. := match p, e return forall T, (unification_resultT' p evm -> option T) -> option T with | pattern.Wildcard t', _ => fun T k - => (tro <- type.try_make_transport_cps (@base.try_make_transport_cps) value _ _; + => (tro <- type.try_make_transport_cps (@base.try_make_transport_cps) value (type_of_rawexpr e) (pattern.type.subst_default t' evm); (tr <- tro; + _ <- pattern.type.subst t' evm; (* ensure that we did not fall into the default case *) (k (tr (value_of_rawexpr e))))%option)%cps | pattern.Ident t pidc, rIdent known _ idc _ _ => fun T k diff --git a/src/Experiments/NewPipeline/nbe_rewrite_head.out b/src/Experiments/NewPipeline/nbe_rewrite_head.out index a60bdfeb4..cbd282f50 100644 --- a/src/Experiments/NewPipeline/nbe_rewrite_head.out +++ b/src/Experiments/NewPipeline/nbe_rewrite_head.out @@ -408,7 +408,8 @@ 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) @@ -465,11 +466,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 (_, _, (_, (_, _, (_, _)), (_, (_, _))), (_, _), @@ -478,7 +479,8 @@ 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 -- cgit v1.2.3