diff options
| author |  Jason Gross <jgross@mit.edu> | 2018-12-12 14:15:35 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2018-12-12 14:15:35 -0500 |
| commit | 0672c92921e45b942fa8a75c45457b8c7b32565d (patch) | |
| tree | 0c79656d77300ba5d011aa8df27adb9ccc7d2d14 /src | |
| parent | 625b72507670750ba2545977ba49283c1431a8c3 (diff) | |
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
Diffstat (limited to 'src')
| -rw-r--r-- | src/Experiments/NewPipeline/Rewriter.v | 3 | ||||
| -rw-r--r-- | 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 |