diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 16:08:02 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-27 20:41:04 +0200 |
| commit | 84544396cbbf34848be2240acf181b4d5f1f42d2 (patch) | |
| tree | 72d398f334bdc7b1c6a0ee333a05940c34780f12 /plugins/cc/ccalgo.ml | |
| parent | 0efba04058ba28889c83553224309be216873298 (diff) | |
Add a boolean to indicate the unfolding state of a primitive projection,
so as to reproduce correctly the reduction behavior of existing
projections, i.e. delta + iota. Make [projection] an abstract datatype
in Names.ml, most of the patch is about using that abstraction.
Fix unification.ml which tried canonical projections too early in
presence of primitive projections.
Diffstat (limited to 'plugins/cc/ccalgo.ml')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 50b647e44..5a4a435a5 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -425,15 +425,15 @@ and applist_proj c l = and applist_projection c l = match kind_of_term c with | Const c when Environ.is_projection (fst c) (Global.env()) -> + let p = Projection.make (fst c) false in (match l with | [] -> (* Expand the projection *) - let kn = fst c in let ty,_ = Typeops.type_of_constant (Global.env ()) c in - let pb = Environ.lookup_projection kn (Global.env()) in + let pb = Environ.lookup_projection p (Global.env()) in let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - it_mkLambda_or_LetIn (mkProj(kn,mkRel 1)) ctx + it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx | hd :: tl -> - applistc (mkProj (fst c, hd)) tl) + applistc (mkProj (p, hd)) tl) | _ -> applistc c l let rec canonize_name c = @@ -456,9 +456,10 @@ let rec canonize_name c = mkLetIn (na, func b,func t,func ct) | App (ct,l) -> mkApp (func ct,Array.smartmap func l) - | Proj(kn,c) -> - let canon_const = constant_of_kn (canonical_con kn) in - (mkProj (canon_const, func c)) + | Proj(p,c) -> + let p' = Projection.map (fun kn -> + constant_of_kn (canonical_con kn)) p in + (mkProj (p', func c)) | _ -> c (* rebuild a term from a pattern and a substitution *) |