diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/heads.ml | 29 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 15 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 3 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 12 | ||||
| -rw-r--r-- | pretyping/recordops.mli | 2 |
5 files changed, 24 insertions, 37 deletions
diff --git a/pretyping/heads.ml b/pretyping/heads.ml index a3e4eb8971..e533930267 100644 --- a/pretyping/heads.ml +++ b/pretyping/heads.ml @@ -26,9 +26,8 @@ open Context.Named.Declaration the evaluation of [phi(0)] and the head of [h] is declared unknown). *) type rigid_head_kind = -| RigidParameter of Constant.t (* a Const without body *) -| RigidVar of variable (* a Var without body *) -| RigidType (* an inductive, a product or a sort *) +| RigidParameter of Constant.t (* a Const without body. Module substitution may instantiate it with something else. *) +| RigidOther (* a Var without body, inductive, product, sort, projection *) type head_approximation = | RigidHead of rigid_head_kind @@ -77,7 +76,7 @@ let kind_of_head env t = str ".")) | Construct _ | CoFix _ -> if b then NotImmediatelyComputableHead else ConstructorHead - | Sort _ | Ind _ | Prod _ -> RigidHead RigidType + | Sort _ | Ind _ | Prod _ -> RigidHead RigidOther | Cast (c,_,_) -> aux k l c b | Lambda (_,_,c) -> begin match l with @@ -89,9 +88,7 @@ let kind_of_head env t = | LetIn _ -> assert false | Meta _ | Evar _ -> NotImmediatelyComputableHead | App (c,al) -> aux k (Array.to_list al @ l) c b - | Proj (p,c) -> - (try on_subterm k (c :: l) b (constant_head (Projection.constant p)) - with Not_found -> assert false) + | Proj (p,c) -> RigidHead RigidOther | Case (_,_,c,_) -> aux k [] c true | Fix ((i,j),_) -> @@ -124,22 +121,16 @@ let kind_of_head env t = (* FIXME: maybe change interface here *) let compute_head = function | EvalConstRef cst -> - let env = Global.env() in - let cb = Environ.lookup_constant cst env in - let is_Def = function Declarations.Def _ -> true | _ -> false in - let body = - if not (Recordops.is_primitive_projection cst) && is_Def cb.Declarations.const_body - then Global.body_of_constant cst else None - in - (match body with - | None -> RigidHead (RigidParameter cst) - | Some (c, _) -> kind_of_head env c) + let env = Global.env() in + let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in + (match body with + | None -> RigidHead (RigidParameter cst) + | Some c -> kind_of_head env c) | EvalVarRef id -> (match Global.lookup_named id with | LocalDef (_,c,_) when not (Decls.variable_opacity id) -> kind_of_head (Global.env()) c - | _ -> - RigidHead (RigidVar id)) + | _ -> RigidHead RigidOther) let is_rigid env t = match kind_of_head env t with diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index cba1533da5..8c57fc2375 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -193,7 +193,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; solve_unification_constraints : bool; - use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } @@ -247,14 +246,14 @@ let apply_typeclasses env sigma frozen fail_evar = else sigma in sigma -let apply_inference_hook hook sigma frozen = match frozen with +let apply_inference_hook hook env sigma frozen = match frozen with | FrozenId _ -> sigma | FrozenProgress (lazy (_, pending)) -> Evar.Set.fold (fun evk sigma -> if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try - let sigma, c = hook sigma evk in + let sigma, c = hook env sigma evk in Evd.define evk c sigma with Exit -> sigma @@ -307,16 +306,16 @@ let check_evars_are_solved env sigma frozen = (* Try typeclasses, hooks, unification heuristics ... *) -let solve_remaining_evars flags env sigma init_sigma = +let solve_remaining_evars ?hook flags env sigma init_sigma = let frozen = frozen_and_pending_holes (init_sigma, sigma) in let sigma = if flags.use_typeclasses then apply_typeclasses env sigma frozen false else sigma in - let sigma = if Option.has_some flags.use_hook - then apply_inference_hook (Option.get flags.use_hook env) sigma frozen - else sigma + let sigma = match hook with + | None -> sigma + | Some hook -> apply_inference_hook hook env sigma frozen in let sigma = if flags.solve_unification_constraints then apply_heuristics env sigma false @@ -1075,14 +1074,12 @@ let ise_pretype_gen flags env sigma lvar kind c = let default_inference_flags fail = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = None; fail_evar = fail; expand_evars = true } let no_classes_no_fail_inference_flags = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = None; fail_evar = false; expand_evars = true } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 0f95d27528..2eaa77b822 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -35,7 +35,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr type inference_flags = { use_typeclasses : bool; solve_unification_constraints : bool; - use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } @@ -95,7 +94,7 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> with candidate and no other conversion problems that the one in [pending], however, it can contain more evars than the pending ones. *) -val solve_remaining_evars : inference_flags -> +val solve_remaining_evars : ?hook:inference_hook -> inference_flags -> env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map (** Checking evars and pending conversion problems are all solved, diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 4faa753dfb..fe9b69dbbc 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -106,16 +106,16 @@ let find_projection = function let prim_table = Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs" -let load_prim i (_,p) = - prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table +let load_prim i (_,(p,c)) = + prim_table := Cmap_env.add c p !prim_table let cache_prim p = load_prim 1 p -let subst_prim (subst,p) = subst_proj_repr subst p +let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c -let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p) +let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c) -let inPrim : Projection.Repr.t -> obj = +let inPrim : (Projection.Repr.t * Constant.t) -> obj = declare_object { (default_object "PRIMPROJS") with cache_function = cache_prim ; @@ -124,7 +124,7 @@ let inPrim : Projection.Repr.t -> obj = classify_function = (fun x -> Substitute x); discharge_function = discharge_prim } -let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p) +let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c)) let is_primitive_projection c = Cmap_env.mem c !prim_table diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 415b964168..3e43372b65 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -45,7 +45,7 @@ val find_projection_nparams : GlobRef.t -> int val find_projection : GlobRef.t -> struc_typ (** Sets up the mapping from constants to primitive projections *) -val declare_primitive_projection : Projection.Repr.t -> unit +val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit val is_primitive_projection : Constant.t -> bool |