summaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r--pretyping/evarutil.ml2027
1 files changed, 376 insertions, 1651 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 05b7e443..d286b98e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1,25 +1,48 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+open Errors
open Util
open Pp
open Names
-open Univ
open Term
+open Vars
+open Context
open Termops
open Namegen
-open Sign
open Pre_env
open Environ
open Evd
open Reductionops
open Pretype_errors
-open Retyping
+
+(** Combinators *)
+
+let evd_comb0 f evdref =
+ let (evd',x) = f !evdref in
+ evdref := evd';
+ x
+
+let evd_comb1 f evdref x =
+ let (evd',y) = f !evdref x in
+ evdref := evd';
+ y
+
+let evd_comb2 f evdref x y =
+ let (evd',z) = f !evdref x y in
+ evdref := evd';
+ z
+
+let e_new_global evdref x =
+ evd_comb1 (Evd.fresh_global (Global.env())) evdref x
+
+let new_global evd x =
+ Evd.fresh_global (Global.env()) evd x
(****************************************************)
(* Expanding/testing/exposing existential variables *)
@@ -37,48 +60,80 @@ let rec flush_and_check_evars sigma c =
| Some c -> flush_and_check_evars sigma c)
| _ -> map_constr (flush_and_check_evars sigma) c
-let nf_evar = Pretype_errors.nf_evar
-let j_nf_evar = Pretype_errors.j_nf_evar
-let jl_nf_evar = Pretype_errors.jl_nf_evar
-let jv_nf_evar = Pretype_errors.jv_nf_evar
-let tj_nf_evar = Pretype_errors.tj_nf_evar
+(* let nf_evar_key = Profile.declare_profile "nf_evar" *)
+(* let nf_evar = Profile.profile2 nf_evar_key Reductionops.nf_evar *)
+let nf_evar = Reductionops.nf_evar
+let j_nf_evar sigma j =
+ { uj_val = nf_evar sigma j.uj_val;
+ uj_type = nf_evar sigma j.uj_type }
+let j_nf_betaiotaevar sigma j =
+ { uj_val = nf_evar sigma j.uj_val;
+ uj_type = Reductionops.nf_betaiota sigma j.uj_type }
+let jl_nf_evar sigma jl = List.map (j_nf_evar sigma) jl
+let jv_nf_betaiotaevar sigma jl =
+ Array.map (j_nf_betaiotaevar sigma) jl
+let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
+let tj_nf_evar sigma {utj_val=v;utj_type=t} =
+ {utj_val=nf_evar sigma v;utj_type=t}
+
+let env_nf_evar sigma env =
+ process_rel_context
+ (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env
+
+let env_nf_betaiotaevar sigma env =
+ process_rel_context
+ (fun d e ->
+ push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
+
+let nf_evars_universes evm =
+ Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm)
+ (Evd.universe_subst evm)
+
+let nf_evars_and_universes evm =
+ let evm = Evd.nf_constraints evm in
+ evm, nf_evars_universes evm
+
+let e_nf_evars_and_universes evdref =
+ evdref := Evd.nf_constraints !evdref;
+ nf_evars_universes !evdref, Evd.universe_subst !evdref
+
+let nf_evar_map_universes evm =
+ let evm = Evd.nf_constraints evm in
+ let subst = Evd.universe_subst evm in
+ if Univ.LMap.is_empty subst then evm, nf_evar evm
+ else
+ let f = nf_evars_universes evm in
+ Evd.raw_map (fun _ -> map_evar_info f) evm, f
let nf_named_context_evar sigma ctx =
- Sign.map_named_context (Reductionops.nf_evar sigma) ctx
+ Context.map_named_context (nf_evar sigma) ctx
let nf_rel_context_evar sigma ctx =
- Sign.map_rel_context (Reductionops.nf_evar sigma) ctx
+ Context.map_rel_context (nf_evar sigma) ctx
let nf_env_evar sigma env =
let nc' = nf_named_context_evar sigma (Environ.named_context env) in
let rel' = nf_rel_context_evar sigma (Environ.rel_context env) in
push_rel_context rel' (reset_with_named_context (val_of_named_context nc') env)
-let nf_evar_info evc info =
- { info with
- evar_concl = Reductionops.nf_evar evc info.evar_concl;
- evar_hyps = map_named_val (Reductionops.nf_evar evc) info.evar_hyps;
- evar_body = match info.evar_body with
- | Evar_empty -> Evar_empty
- | Evar_defined c -> Evar_defined (Reductionops.nf_evar evc c) }
-let nf_evars evm =
- Evd.fold
- (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
- evm Evd.empty
-
-let nf_evars_undefined evm =
- Evd.fold_undefined
- (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi))
- evm (defined_evars evm)
-
-let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd
-let nf_evar_map_undefined evd = Evd.evars_reset_evd (nf_evars_undefined evd) evd
+let nf_evar_info evc info = map_evar_info (nf_evar evc) info
+
+let nf_evar_map evm =
+ Evd.raw_map (fun _ evi -> nf_evar_info evm evi) evm
+
+let nf_evar_map_undefined evm =
+ Evd.raw_map_undefined (fun _ evi -> nf_evar_info evm evi) evm
(*-------------------*)
(* Auxiliary functions for the conversion algorithms modulo evars
*)
-let has_undefined_evars_or_sorts evd t =
+(* A probably faster though more approximative variant of
+ [has_undefined (nf_evar c)]: instances are not substituted and
+ maybe an evar occurs in an instance and it would disappear by
+ instantiation *)
+
+let has_undefined_evars evd t =
let rec has_ev t =
match kind_of_term t with
| Evar (ev,args) ->
@@ -87,13 +142,12 @@ let has_undefined_evars_or_sorts evd t =
has_ev c; Array.iter has_ev args
| Evar_empty ->
raise NotInstantiatedEvar)
- | Sort s when is_sort_variable evd s -> raise Not_found
| _ -> iter_constr has_ev t in
try let _ = has_ev t in false
with (Not_found | NotInstantiatedEvar) -> true
let is_ground_term evd t =
- not (has_undefined_evars_or_sorts evd t)
+ not (has_undefined_evars evd t)
let is_ground_env evd env =
let is_ground_decl = function
@@ -101,9 +155,16 @@ let is_ground_env evd env =
| _ -> true in
List.for_all is_ground_decl (rel_context env) &&
List.for_all is_ground_decl (named_context env)
+
(* Memoization is safe since evar_map and environ are applicative
structures *)
-let is_ground_env = memo1_2 is_ground_env
+let memo f =
+ let m = ref None in
+ fun x y -> match !m with
+ | Some (x', y', r) when x == x' && y == y' -> r
+ | _ -> let r = f x y in m := Some (x, y, r); r
+
+let is_ground_env = memo is_ground_env
(* Return the head evar if any *)
@@ -125,35 +186,27 @@ let head_evar =
let whd_head_evar_stack sigma c =
let rec whrec (c, l as s) =
match kind_of_term c with
- | Evar (evk,args as ev) when Evd.is_defined sigma evk
- -> whrec (existential_value sigma ev, l)
+ | Evar (evk,args as ev) ->
+ let v =
+ try Some (existential_value sigma ev)
+ with NotInstantiatedEvar | Not_found -> None in
+ begin match v with
+ | None -> s
+ | Some c -> whrec (c, l)
+ end
| Cast (c,_,_) -> whrec (c, l)
- | App (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+ | App (f,args) -> whrec (f, args :: l)
| _ -> s
in
whrec (c, [])
-let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
-
-let noccur_evar env evd evk c =
- let rec occur_rec k c = match kind_of_term c with
- | Evar (evk',args' as ev') ->
- (match safe_evar_value evd ev' with
- | Some c -> occur_rec k c
- | None ->
- if evk = evk' then raise Occur else Array.iter (occur_rec k) args')
- | Rel i when i > k ->
- (match pi2 (Environ.lookup_rel (i-k) env) with
- | None -> ()
- | Some b -> occur_rec k (lift i b))
- | _ -> iter_constr_with_binders succ occur_rec k c
- in
- try occur_rec 0 c; true with Occur -> false
-
-let normalize_evar evd ev =
- match kind_of_term (whd_evar evd (mkEvar ev)) with
- | Evar (evk,args) -> (evk,args)
- | _ -> assert false
+let whd_head_evar sigma c =
+ let (f, args) = whd_head_evar_stack sigma c in
+ (** optim: don't reallocate if empty/singleton *)
+ match args with
+ | [] -> f
+ | [arg] -> mkApp (f, arg)
+ | _ -> mkApp (f, Array.concat args)
(**********************)
(* Creating new metas *)
@@ -161,94 +214,28 @@ let normalize_evar evd ev =
(* Generator of metavariables *)
let new_meta =
- let meta_ctr = ref 0 in
- Summary.declare_summary "meta counter"
- { Summary.freeze_function = (fun () -> !meta_ctr);
- Summary.unfreeze_function = (fun n -> meta_ctr := n);
- Summary.init_function = (fun () -> meta_ctr := 0) };
+ let meta_ctr = Summary.ref 0 ~name:"meta counter" in
fun () -> incr meta_ctr; !meta_ctr
let mk_new_meta () = mkMeta(new_meta())
-let collect_evars emap c =
- let rec collrec acc c =
- match kind_of_term c with
- | Evar (evk,_) ->
- if Evd.is_undefined emap evk then evk::acc
- else (* No recursion on the evar instantiation *) acc
- | _ ->
- fold_constr collrec acc c in
- list_uniquize (collrec [] c)
-
-let push_dependent_evars sigma emap =
- Evd.fold_undefined (fun ev {evar_concl = ccl} (sigma',emap') ->
- List.fold_left
- (fun (sigma',emap') ev ->
- (Evd.add sigma' ev (Evd.find emap' ev),Evd.remove emap' ev))
- (sigma',emap') (collect_evars emap' ccl))
- emap (sigma,emap)
-
-let push_duplicated_evars sigma emap c =
- let rec collrec (one,(sigma,emap) as acc) c =
- match kind_of_term c with
- | Evar (evk,_) when not (Evd.mem sigma evk) ->
- if List.mem evk one then
- let sigma' = Evd.add sigma evk (Evd.find emap evk) in
- let emap' = Evd.remove emap evk in
- (one,(sigma',emap'))
- else
- (evk::one,(sigma,emap))
- | _ ->
- fold_constr collrec acc c
- in
- snd (collrec ([],(sigma,emap)) c)
-
-(* replaces a mapping of existentials into a mapping of metas.
- Problem if an evar appears in the type of another one (pops anomaly) *)
-let evars_to_metas sigma (emap, c) =
- let emap = nf_evar_map_undefined emap in
- let sigma',emap' = push_dependent_evars sigma emap in
- let sigma',emap' = push_duplicated_evars sigma' emap' c in
- (* if an evar has been instantiated in [emap] (as part of typing [c])
- then it is instantiated in [sigma]. *)
- let repair_evars sigma emap =
- fold_undefined begin fun ev _ sigma' ->
- try
- let info = find emap ev in
- match evar_body info with
- | Evar_empty -> sigma'
- | Evar_defined body -> define ev body sigma'
- with Not_found -> sigma'
- end sigma sigma
- in
- let sigma' = repair_evars sigma' emap in
- let change_exist evar =
- let ty = nf_betaiota emap (existential_type emap evar) in
- let n = new_meta() in
- mkCast (mkMeta n, DEFAULTcast, ty) in
- let rec replace c =
- match kind_of_term c with
- | Evar (evk,_ as ev) when Evd.mem emap' evk -> change_exist ev
- | _ -> map_constr replace c in
- (sigma', replace c)
-
(* The list of non-instantiated existential declarations (order is important) *)
let non_instantiated sigma =
- let listev = Evd.undefined_list sigma in
- List.map (fun (ev,evi) -> (ev,nf_evar_info sigma evi)) listev
+ let listev = Evd.undefined_map sigma in
+ Evar.Map.smartmap (fun evi -> nf_evar_info sigma evi) listev
(************************)
(* Manipulating filters *)
(************************)
-let apply_subfilter filter subfilter =
- fst (List.fold_right (fun oldb (l,filter) ->
- if oldb then List.hd filter::l,List.tl filter else (false::l,filter))
- filter ([], List.rev subfilter))
-
-let extract_subfilter initial_filter refined_filter =
- snd (list_filter2 (fun b1 b2 -> b1) (initial_filter,refined_filter))
+let make_pure_subst evi args =
+ snd (List.fold_right
+ (fun (id,b,c) (args,l) ->
+ match args with
+ | a::rest -> (rest, (id,a)::l)
+ | _ -> anomaly (Pp.str "Instance does not match its signature"))
+ (evar_filtered_context evi) (Array.rev_to_list args,[]))
(**********************)
(* Creating new evars *)
@@ -256,12 +243,8 @@ let extract_subfilter initial_filter refined_filter =
(* Generator of existential names *)
let new_untyped_evar =
- let evar_ctr = ref 0 in
- Summary.declare_summary "evar counter"
- { Summary.freeze_function = (fun () -> !evar_ctr);
- Summary.unfreeze_function = (fun n -> evar_ctr := n);
- Summary.init_function = (fun () -> evar_ctr := 0) };
- fun () -> incr evar_ctr; existential_of_int !evar_ctr
+ let evar_ctr = Summary.ref 0 ~name:"evar counter" in
+ fun () -> incr evar_ctr; Evar.unsafe_of_int !evar_ctr
(*------------------------------------*
* functional operations on evar sets *
@@ -296,109 +279,145 @@ let new_untyped_evar =
* we have the property that u and phi(t) are convertible in env.
*)
+let subst2 subst vsubst c =
+ substl subst (replace_vars vsubst c)
+
let push_rel_context_to_named_context env typ =
(* compute the instances relative to the named context and rel_context *)
let ids = List.map pi1 (named_context env) in
let inst_vars = List.map mkVar ids in
let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
+ let replace_var_named_declaration id0 id (id',b,t) =
+ let id' = if Id.equal id0 id' then id else id' in
+ let vsubst = [id0 , mkVar id] in
+ let b = match b with
+ | None -> None
+ | Some c -> Some (replace_vars vsubst c)
+ in
+ id', b, replace_vars vsubst t
+ in
+ let replace_var_named_context id0 id env =
+ let nc = Environ.named_context env in
+ let nc' = List.map (replace_var_named_declaration id0 id) nc in
+ Environ.reset_with_named_context (val_of_named_context nc') env
+ in
+ let extract_if_neq id = function
+ | Anonymous -> None
+ | Name id' when id_ord id id' = 0 -> None
+ | Name id' -> Some id'
+ in
(* move the rel context to a named context and extend the named instance *)
(* with vars of the rel context *)
(* We do keep the instances corresponding to local definition (see above) *)
- let (subst, _, env) =
- Sign.fold_rel_context
- (fun (na,c,t) (subst, avoid, env) ->
- let id = next_name_away na avoid in
- let d = (id,Option.map (substl subst) c,substl subst t) in
- (mkVar id :: subst, id::avoid, push_named d env))
- (rel_context env) ~init:([], ids, env) in
- (named_context_val env, substl subst typ, inst_rels@inst_vars, subst)
+ let (subst, vsubst, _, env) =
+ Context.fold_rel_context
+ (fun (na,c,t) (subst, vsubst, avoid, env) ->
+ let id =
+ (* ppedrot: we want to infer nicer names for the refine tactic, but
+ keeping at the same time backward compatibility in other code
+ using this function. For now, we only attempt to preserve the
+ old behaviour of Program, but ultimately, one should do something
+ about this whole name generation problem. *)
+ if Flags.is_program_mode () then next_name_away na avoid
+ else next_ident_away (id_of_name_using_hdchar env t na) avoid
+ in
+ match extract_if_neq id na with
+ | Some id0 when not (is_section_variable id0) ->
+ (* spiwack: if [id<>id0], rather than introducing a new
+ binding named [id], we will keep [id0] (the name given
+ by the user) and rename [id0] into [id] in the named
+ context. Unless [id] is a section variable. *)
+ let subst = List.map (replace_vars [id0,mkVar id]) subst in
+ let vsubst = (id0,mkVar id)::vsubst in
+ let d = (id0, Option.map (subst2 subst vsubst) c, subst2 subst vsubst t) in
+ let env = replace_var_named_context id0 id env in
+ (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
+ | _ ->
+ (* spiwack: if [id0] is a section variable renaming it is
+ incorrect. We revert to a less robust behaviour where
+ the new binder has name [id]. Which amounts to the same
+ behaviour than when [id=id0]. *)
+ let d = (id,Option.map (subst2 subst vsubst) c,subst2 subst vsubst t) in
+ (mkVar id :: subst, vsubst, id::avoid, push_named d env)
+ )
+ (rel_context env) ~init:([], [], ids, env) in
+ (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
(*------------------------------------*
* Entry points to define new evars *
*------------------------------------*)
-let default_source = (dummy_loc,InternalHole)
+let default_source = (Loc.ghost,Evar_kinds.InternalHole)
-let new_pure_evar evd sign ?(src=default_source) ?filter ?candidates typ =
+let restrict_evar evd evk filter candidates =
+ let evk' = new_untyped_evar () in
+ let evd = Evd.restrict evk evk' filter ?candidates evd in
+ Evd.declare_future_goal evk' evd, evk'
+
+let new_pure_evar_full evd evi =
+ let evk = new_untyped_evar () in
+ let evd = Evd.add evd evk evi in
+ let evd = Evd.declare_future_goal evk evd in
+ (evd, evk)
+
+let new_pure_evar sign evd ?(src=default_source) ?filter ?candidates ?store ?naming ?(principal=false) typ =
+ let default_naming =
+ if principal then
+ (* waiting for a more principled approach
+ (unnamed evars, private names?) *)
+ Misctypes.IntroFresh (Names.Id.of_string "tmp_goal")
+ else
+ Misctypes.IntroAnonymous
+ in
+ let naming = Option.default default_naming naming in
let newevk = new_untyped_evar() in
- let evd = evar_declare sign newevk typ ~src ?filter ?candidates evd in
+ let evd = evar_declare sign newevk typ ~src ?filter ?candidates ?store ~naming evd in
+ let evd =
+ if principal then Evd.declare_principal_goal newevk evd
+ else Evd.declare_future_goal newevk evd
+ in
(evd,newevk)
-let new_evar_instance sign evd typ ?src ?filter ?candidates instance =
+let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance =
assert (not !Flags.debug ||
- list_distinct (ids_of_named_context (named_context_of_val sign)));
- let evd,newevk = new_pure_evar evd sign ?src ?filter ?candidates typ in
+ List.distinct (ids_of_named_context (named_context_of_val sign)));
+ let evd,newevk = new_pure_evar sign evd ?src ?filter ?candidates ?store ?naming ?principal typ in
(evd,mkEvar (newevk,Array.of_list instance))
(* [new_evar] declares a new existential in an env env with type typ *)
(* Converting the env into the sign of the evar to define *)
-
-let new_evar evd env ?src ?filter ?candidates typ =
- let sign,typ',instance,subst = push_rel_context_to_named_context env typ in
- let candidates = Option.map (List.map (substl subst)) candidates in
+let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+ let sign,typ',instance,subst,vsubst = push_rel_context_to_named_context env typ in
+ let candidates = Option.map (List.map (subst2 subst vsubst)) candidates in
let instance =
match filter with
| None -> instance
- | Some filter -> list_filter_with filter instance in
- new_evar_instance sign evd typ' ?src ?filter ?candidates instance
+ | Some filter -> Filter.filter_list filter instance in
+ new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance
-let new_type_evar ?src ?filter evd env =
- let evd', s = new_sort_variable evd in
- new_evar evd' env ?src ?filter (mkSort s)
+let new_type_evar env evd ?src ?filter ?naming ?principal rigid =
+ let evd', s = new_sort_variable rigid evd in
+ let evd', e = new_evar env evd' ?src ?filter ?naming ?principal (mkSort s) in
+ evd', (e, s)
- (* The same using side-effect *)
-let e_new_evar evdref env ?(src=(dummy_loc,InternalHole)) ?filter ?candidates ty =
- let (evd',ev) = new_evar !evdref env ~src:src ?filter ?candidates ty in
- evdref := evd';
- ev
+let e_new_type_evar env evdref ?src ?filter ?naming ?principal rigid =
+ let evd', c = new_type_evar env !evdref ?src ?filter ?naming ?principal rigid in
+ evdref := evd';
+ c
-(*------------------------------------*
- * Restricting existing evars *
- *------------------------------------*)
+let new_Type ?(rigid=Evd.univ_flexible) env evd =
+ let evd', s = new_sort_variable rigid evd in
+ evd', mkSort s
-let restrict_evar_key evd evk filter candidates =
- if filter = None && candidates = None then
- evd,evk
- else
- let evi = Evd.find_undefined evd evk in
- let oldfilter = evar_filter evi in
- if filter = Some oldfilter && candidates = None then
- evd,evk
- else
- let filter =
- match filter with
- | None -> evar_filter evi
- | Some filter -> filter in
- let candidates =
- match candidates with None -> evi.evar_candidates | _ -> candidates in
- let ccl = evi.evar_concl in
- let sign = evar_hyps evi in
- let src = evi.evar_source in
- let evd,newevk = new_pure_evar evd sign ccl ~src ~filter ?candidates in
- let ctxt = snd (list_filter2 (fun b c -> b) (filter,evar_context evi)) in
- let id_inst = Array.of_list (List.map (fun (id,_,_) -> mkVar id) ctxt) in
- Evd.define evk (mkEvar(newevk,id_inst)) evd,newevk
-
-(* Restrict an applied evar and returns its restriction in the same context *)
-let restrict_applied_evar evd (evk,argsv) filter candidates =
- let evd,newevk = restrict_evar_key evd evk filter candidates in
- let newargsv = match filter with
- | None -> (* optim *) argsv
- | Some filter ->
- let evi = Evd.find evd evk in
- let subfilter = extract_subfilter (evar_filter evi) filter in
- array_filter_with subfilter argsv in
- evd,(newevk,newargsv)
-
-(* Restrict an evar in the current evar_map *)
-let restrict_evar evd evk filter candidates =
- fst (restrict_evar_key evd evk filter candidates)
+let e_new_Type ?(rigid=Evd.univ_flexible) env evdref =
+ let evd', s = new_sort_variable rigid !evdref in
+ evdref := evd'; mkSort s
-(* Restrict an evar in the current evar_map *)
-let restrict_instance evd evk filter argsv =
- match filter with None -> argsv | Some filter ->
- let evi = Evd.find evd evk in
- array_filter_with (extract_subfilter (evar_filter evi) filter) argsv
+ (* The same using side-effect *)
+let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?naming ?principal ty =
+ let (evd',ev) = new_evar env !evdref ~src:src ?filter ?candidates ?store ?naming ?principal ty in
+ evdref := evd';
+ ev
(* This assumes an evar with identity instance and generalizes it over only
the De Bruijn part of the context *)
@@ -410,176 +429,26 @@ let generalize_evar_over_rels sigma (ev,args) =
if isRel a then (mkNamedProd_or_LetIn d c,a::inst) else x)
(evi.evar_concl,[]) (Array.to_list args) sign
-(***************************************)
-(* Managing chains of local definitons *)
-(***************************************)
-
-(* Expand rels and vars that are bound to other rels or vars so that
- dependencies in variables are canonically associated to the most ancient
- variable in its family of aliased variables *)
-
-let compute_var_aliases sign =
- List.fold_right (fun (id,b,c) aliases ->
- match b with
- | Some t ->
- (match kind_of_term t with
- | Var id' ->
- let aliases_of_id =
- try Idmap.find id' aliases with Not_found -> [] in
- Idmap.add id (aliases_of_id@[t]) aliases
- | _ ->
- Idmap.add id [t] aliases)
- | None -> aliases)
- sign Idmap.empty
-
-let compute_rel_aliases var_aliases rels =
- snd (List.fold_right (fun (_,b,t) (n,aliases) ->
- (n-1,
- match b with
- | Some t ->
- (match kind_of_term t with
- | Var id' ->
- let aliases_of_n =
- try Idmap.find id' var_aliases with Not_found -> [] in
- Intmap.add n (aliases_of_n@[t]) aliases
- | Rel p ->
- let aliases_of_n =
- try Intmap.find (p+n) aliases with Not_found -> [] in
- Intmap.add n (aliases_of_n@[mkRel (p+n)]) aliases
- | _ ->
- Intmap.add n [lift n t] aliases)
- | None -> aliases))
- rels (List.length rels,Intmap.empty))
-
-let make_alias_map env =
- (* We compute the chain of aliases for each var and rel *)
- let var_aliases = compute_var_aliases (named_context env) in
- let rel_aliases = compute_rel_aliases var_aliases (rel_context env) in
- (var_aliases,rel_aliases)
-
-let lift_aliases n (var_aliases,rel_aliases as aliases) =
- if n = 0 then aliases else
- (var_aliases,
- Intmap.fold (fun p l -> Intmap.add (p+n) (List.map (lift n) l))
- rel_aliases Intmap.empty)
-
-let get_alias_chain_of aliases x = match kind_of_term x with
- | Rel n -> (try Intmap.find n (snd aliases) with Not_found -> [])
- | Var id -> (try Idmap.find id (fst aliases) with Not_found -> [])
- | _ -> []
-
-let normalize_alias_opt aliases x =
- match get_alias_chain_of aliases x with
- | [] -> None
- | a::_ when isRel a or isVar a -> Some a
- | [_] -> None
- | _::a::_ -> Some a
-
-let normalize_alias aliases x =
- match normalize_alias_opt aliases x with
- | Some a -> a
- | None -> x
-
-let normalize_alias_var var_aliases id =
- destVar (normalize_alias (var_aliases,Intmap.empty) (mkVar id))
-
-let extend_alias (_,b,_) (var_aliases,rel_aliases) =
- let rel_aliases =
- Intmap.fold (fun n l -> Intmap.add (n+1) (List.map (lift 1) l))
- rel_aliases Intmap.empty in
- let rel_aliases =
- match b with
- | Some t ->
- (match kind_of_term t with
- | Var id' ->
- let aliases_of_binder =
- try Idmap.find id' var_aliases with Not_found -> [] in
- Intmap.add 1 (aliases_of_binder@[t]) rel_aliases
- | Rel p ->
- let aliases_of_binder =
- try Intmap.find (p+1) rel_aliases with Not_found -> [] in
- Intmap.add 1 (aliases_of_binder@[mkRel (p+1)]) rel_aliases
- | _ ->
- Intmap.add 1 [lift 1 t] rel_aliases)
- | None -> rel_aliases in
- (var_aliases, rel_aliases)
-
-let expand_alias_once aliases x =
- match get_alias_chain_of aliases x with
- | [] -> None
- | l -> Some (list_last l)
-
-let rec expansions_of_var aliases x =
- match get_alias_chain_of aliases x with
- | [] -> [x]
- | a::_ as l when isRel a || isVar a -> x :: List.rev l
- | _::l -> x :: List.rev l
-
-let expansion_of_var aliases x =
- match get_alias_chain_of aliases x with
- | [] -> x
- | a::_ -> a
-
-let rec expand_vars_in_term_using aliases t = match kind_of_term t with
- | Rel _ | Var _ ->
- normalize_alias aliases t
- | _ ->
- map_constr_with_full_binders
- extend_alias expand_vars_in_term_using aliases t
-
-let expand_vars_in_term env = expand_vars_in_term_using (make_alias_map env)
-
-let free_vars_and_rels_up_alias_expansion aliases c =
- let acc1 = ref Intset.empty and acc2 = ref Idset.empty in
- let cache_rel = ref Intset.empty and cache_var = ref Idset.empty in
- let is_in_cache depth = function
- | Rel n -> Intset.mem (n-depth) !cache_rel
- | Var s -> Idset.mem s !cache_var
- | _ -> false in
- let put_in_cache depth = function
- | Rel n -> cache_rel := Intset.add (n-depth) !cache_rel
- | Var s -> cache_var := Idset.add s !cache_var
- | _ -> () in
- let rec frec (aliases,depth) c =
- match kind_of_term c with
- | Rel _ | Var _ as ck ->
- if is_in_cache depth ck then () else begin
- put_in_cache depth ck;
- let c = expansion_of_var aliases c in
- match kind_of_term c with
- | Var id -> acc2 := Idset.add id !acc2
- | Rel n -> if n >= depth+1 then acc1 := Intset.add (n-depth) !acc1
- | _ -> frec (aliases,depth) c end
- | Const _ | Ind _ | Construct _ ->
- acc2 := List.fold_right Idset.add (vars_of_global (Global.env()) c) !acc2
- | _ ->
- iter_constr_with_full_binders
- (fun d (aliases,depth) -> (extend_alias d aliases,depth+1))
- frec (aliases,depth) c
- in
- frec (aliases,0) c;
- (!acc1,!acc2)
-
(************************************)
(* Removing a dependency in an evar *)
(************************************)
type clear_dependency_error =
-| OccurHypInSimpleClause of identifier option
+| OccurHypInSimpleClause of Id.t option
| EvarTypingBreak of existential
-exception ClearDependencyError of identifier * clear_dependency_error
-
-open Store.Field
+exception ClearDependencyError of Id.t * clear_dependency_error
let cleared = Store.field ()
-let rec check_and_clear_in_constr evdref err ids c =
+exception Depends of Id.t
+
+let rec check_and_clear_in_constr env evdref err ids c =
(* returns a new constr where all the evars have been 'cleaned'
(ie the hypotheses ids have been removed from the contexts of
evars) *)
let check id' =
- if List.mem id' ids then
+ if Id.Set.mem id' ids then
raise (ClearDependencyError (id',err))
in
match kind_of_term c with
@@ -587,14 +456,14 @@ let rec check_and_clear_in_constr evdref err ids c =
check id'; c
| ( Const _ | Ind _ | Construct _ ) ->
- let vars = Environ.vars_of_global (Global.env()) c in
- List.iter check vars; c
+ let vars = Environ.vars_of_global env c in
+ Id.Set.iter check vars; c
| Evar (evk,l as ev) ->
if Evd.is_defined !evdref evk then
(* If evk is already defined we replace it by its definition *)
let nc = whd_evar !evdref c in
- (check_and_clear_in_constr evdref err ids nc)
+ (check_and_clear_in_constr env evdref err ids nc)
else
(* We check for dependencies to elements of ids in the
evar_info corresponding to e and in the instance of
@@ -603,1217 +472,93 @@ let rec check_and_clear_in_constr evdref err ids c =
removed *)
let evi = Evd.find_undefined !evdref evk in
let ctxt = Evd.evar_filtered_context evi in
- let (nhyps,nargs,rids) =
- List.fold_right2
- (fun (rid,ob,c as h) a (hy,ar,ri) ->
- (* Check if some id to clear occurs in the instance
- a of rid in ev and remember the dependency *)
- match
- List.filter (fun id -> List.mem id ids) (Idset.elements (collect_vars a))
- with
- | id :: _ -> (hy,ar,(rid,id)::ri)
- | _ ->
- (* Check if some rid to clear in the context of ev
- has dependencies in another hyp of the context of ev
- and transitively remember the dependency *)
- match List.filter (fun (id,_) -> occur_var_in_decl (Global.env()) id h) ri with
- | (_,id') :: _ -> (hy,ar,(rid,id')::ri)
- | _ ->
- (* No dependency at all, we can keep this ev's context hyp *)
- (h::hy,a::ar,ri))
- ctxt (Array.to_list l) ([],[],[]) in
+ let (rids,filter) =
+ List.fold_right2
+ (fun (rid, ob,c as h) a (ri,filter) ->
+ try
+ (* Check if some id to clear occurs in the instance
+ a of rid in ev and remember the dependency *)
+ let check id = if Id.Set.mem id ids then raise (Depends id) in
+ let () = Id.Set.iter check (collect_vars a) in
+ (* Check if some rid to clear in the context of ev
+ has dependencies in another hyp of the context of ev
+ and transitively remember the dependency *)
+ let check id _ =
+ if occur_var_in_decl (Global.env ()) id h
+ then raise (Depends id)
+ in
+ let () = Id.Map.iter check ri in
+ (* No dependency at all, we can keep this ev's context hyp *)
+ (ri, true::filter)
+ with Depends id -> (Id.Map.add rid id ri, false::filter))
+ ctxt (Array.to_list l) (Id.Map.empty,[]) in
(* Check if some rid to clear in the context of ev has dependencies
in the type of ev and adjust the source of the dependency *)
- let nconcl =
- try check_and_clear_in_constr evdref (EvarTypingBreak ev)
- (List.map fst rids) (evar_concl evi)
+ let _nconcl =
+ try
+ let nids = Id.Map.domain rids in
+ check_and_clear_in_constr env evdref (EvarTypingBreak ev) nids (evar_concl evi)
with ClearDependencyError (rid,err) ->
- raise (ClearDependencyError (List.assoc rid rids,err)) in
+ raise (ClearDependencyError (Id.Map.find rid rids,err)) in
- if rids = [] then c else begin
- let env = Sign.fold_named_context push_named nhyps ~init:(empty_env) in
- let ev'= e_new_evar evdref env ~src:(evar_source evk !evdref) nconcl in
- evdref := Evd.define evk ev' !evdref;
- let (evk',_) = destEvar ev' in
+ if Id.Map.is_empty rids then c
+ else
+ let origfilter = Evd.evar_filter evi in
+ let filter = Evd.Filter.apply_subfilter origfilter filter in
+ let evd,_ = restrict_evar !evdref evk filter None in
+ evdref := evd;
(* spiwack: hacking session to mark the old [evk] as having been "cleared" *)
let evi = Evd.find !evdref evk in
let extra = evi.evar_extra in
- let extra' = cleared.set true extra in
+ let extra' = Store.set extra cleared true in
let evi' = { evi with evar_extra = extra' } in
evdref := Evd.add !evdref evk evi' ;
(* spiwack: /hacking session *)
- mkEvar(evk', Array.of_list nargs)
- end
+ whd_evar !evdref c
- | _ -> map_constr (check_and_clear_in_constr evdref err ids) c
+ | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
-let clear_hyps_in_evi evdref hyps concl ids =
+let clear_hyps_in_evi_main env evdref hyps terms ids =
(* clear_hyps_in_evi erases hypotheses ids in hyps, checking if some
hypothesis does not depend on a element of ids, and erases ids in
the contexts of the evars occuring in evi *)
- let nconcl =
- check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in
+ let terms =
+ List.map (check_and_clear_in_constr env evdref (OccurHypInSimpleClause None) ids) terms in
let nhyps =
- let check_context (id,ob,c) =
+ let check_context ((id,ob,c) as decl) =
let err = OccurHypInSimpleClause (Some id) in
- (id, Option.map (check_and_clear_in_constr evdref err ids) ob,
- check_and_clear_in_constr evdref err ids c)
+ let ob' = Option.smartmap (fun c -> check_and_clear_in_constr env evdref err ids c) ob in
+ let c' = check_and_clear_in_constr env evdref err ids c in
+ if ob == ob' && c == c' then decl else (id, ob', c')
in
- let check_value vk =
- match !vk with
- | VKnone -> vk
- | VKvalue (v,d) ->
- if (List.for_all (fun e -> not (Idset.mem e d)) ids) then
- (* v does depend on any of ids, it's ok *)
- vk
- else
- (* v depends on one of the cleared hyps: we forget the computed value *)
- ref VKnone
+ let check_value vk = match force_lazy_val vk with
+ | None -> vk
+ | Some (_, d) ->
+ if (Id.Set.for_all (fun e -> not (Id.Set.mem e d)) ids) then
+ (* v does depend on any of ids, it's ok *)
+ vk
+ else
+ (* v depends on one of the cleared hyps:
+ we forget the computed value *)
+ dummy_lazy_val ()
in
remove_hyps ids check_context check_value hyps
in
- (nhyps,nconcl)
-
-(********************************)
-(* Managing pattern-unification *)
-(********************************)
-
-let rec expand_and_check_vars aliases = function
- | [] -> []
- | a::l when isRel a or isVar a ->
- let a = expansion_of_var aliases a in
- if isRel a or isVar a then a :: expand_and_check_vars aliases l
- else raise Exit
- | _ ->
- raise Exit
-
-module Constrhash = Hashtbl.Make
- (struct type t = constr
- let equal = eq_constr
- let hash = hash_constr
- end)
-
-let rec constr_list_distinct l =
- let visited = Constrhash.create 23 in
- let rec loop = function
- | h::t ->
- if Constrhash.mem visited h then false
- else (Constrhash.add visited h h; loop t)
- | [] -> true
- in loop l
-
-let get_actual_deps aliases l t =
- if occur_meta_or_existential t then
- (* Probably no restrictions on allowed vars in presence of evars *)
- l
- else
- (* Probably strong restrictions coming from t being evar-closed *)
- let (fv_rels,fv_ids) = free_vars_and_rels_up_alias_expansion aliases t in
- List.filter (fun c ->
- match kind_of_term c with
- | Var id -> Idset.mem id fv_ids
- | Rel n -> Intset.mem n fv_rels
- | _ -> assert false) l
-
-let remove_instance_local_defs evd evk args =
- let evi = Evd.find evd evk in
- let rec aux = function
- | (_,Some _,_)::sign, a::args -> aux (sign,args)
- | (_,None,_)::sign, a::args -> a::aux (sign,args)
- | [], [] -> []
- | _ -> assert false in
- aux (evar_filtered_context evi, args)
-
-(* Check if an applied evar "?X[args] l" is a Miller's pattern *)
-
-let find_unification_pattern_args env l t =
- if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
- let aliases = make_alias_map env in
- match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
- | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
- | _ -> None
- else
- None
-
-let is_unification_pattern_meta env nb m l t =
- (* Variables from context and rels > nb are implicitly all there *)
- (* so we need to be a rel <= nb *)
- if List.for_all (fun x -> isRel x && destRel x <= nb) l then
- match find_unification_pattern_args env l t with
- | Some _ as x when not (dependent (mkMeta m) t) -> x
- | _ -> None
- else
- None
-
-let is_unification_pattern_evar env evd (evk,args) l t =
- if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
- then
- let args = remove_instance_local_defs evd evk (Array.to_list args) in
- let n = List.length args in
- match find_unification_pattern_args env (args @ l) t with
- | Some l -> Some (list_skipn n l)
- | _ -> None
- else
- None
-
-let is_unification_pattern_pure_evar env evd (evk,args) t =
- is_unification_pattern_evar env evd (evk,args) [] t <> None
-
-let is_unification_pattern (env,nb) evd f l t =
- match kind_of_term f with
- | Meta m -> is_unification_pattern_meta env nb m l t
- | Evar ev -> is_unification_pattern_evar env evd ev l t
- | _ -> None
-
-(* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
- (pattern unification). It is assumed that l is made of rel's that
- are distinct and not bound to aliases. *)
-(* It is also assumed that c does not contain metas because metas
- *implicitly* depend on Vars but lambda abstraction will not reflect this
- dependency: ?X x = ?1 (?1 is a meta) will return \_.?1 while it should
- return \y. ?1{x\y} (non constant function if ?1 depends on x) (BB) *)
-let solve_pattern_eqn env l c =
- let c' = List.fold_right (fun a c ->
- let c' = subst_term (lift 1 a) (lift 1 c) in
- match kind_of_term a with
- (* Rem: if [a] links to a let-in, do as if it were an assumption *)
- | Rel n ->
- let d = map_rel_declaration (lift n) (lookup_rel n env) in
- mkLambda_or_LetIn d c'
- | Var id ->
- let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
- | _ -> assert false)
- l c in
- (* Warning: we may miss some opportunity to eta-reduce more since c'
- is not in normal form *)
- whd_eta c'
-
-(*****************************************)
-(* Refining/solving unification problems *)
-(*****************************************)
-
-(* Knowing that [Gamma |- ev : T] and that [ev] is applied to [args],
- * [make_projectable_subst ev args] builds the substitution [Gamma:=args].
- * If a variable and an alias of it are bound to the same instance, we skip
- * the alias (we just use eq_constr -- instead of conv --, since anyway,
- * only instances that are variables -- or evars -- are later considered;
- * morever, we can bet that similar instances came at some time from
- * the very same substitution. The removal of aliased duplicates is
- * useful to ensure the uniqueness of a projection.
-*)
-
-let make_projectable_subst aliases sigma evi args =
- let sign = evar_filtered_context evi in
- let evar_aliases = compute_var_aliases sign in
- let (_,full_subst,cstr_subst) =
- List.fold_right
- (fun (id,b,c) (args,all,cstrs) ->
- match b,args with
- | None, a::rest ->
- let a = whd_evar sigma a in
- let cstrs =
- let a',args = decompose_app_vect a in
- match kind_of_term a' with
- | Construct cstr ->
- let l = try Constrmap.find cstr cstrs with Not_found -> [] in
- Constrmap.add cstr ((args,id)::l) cstrs
- | _ -> cstrs in
- (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs)
- | Some c, a::rest ->
- let a = whd_evar sigma a in
- (match kind_of_term c with
- | Var id' ->
- let idc = normalize_alias_var evar_aliases id' in
- let sub = try Idmap.find idc all with Not_found -> [] in
- if List.exists (fun (c,_,_) -> eq_constr a c) sub then
- (rest,all,cstrs)
- else
- (rest,
- Idmap.add idc ((a,normalize_alias_opt aliases a,id)::sub) all,
- cstrs)
- | _ ->
- (rest,Idmap.add id [a,normalize_alias_opt aliases a,id] all,cstrs))
- | _ -> anomaly "Instance does not match its signature")
- sign (array_rev_to_list args,Idmap.empty,Constrmap.empty) in
- (full_subst,cstr_subst)
-
-let make_pure_subst evi args =
- snd (List.fold_right
- (fun (id,b,c) (args,l) ->
- match args with
- | a::rest -> (rest, (id,a)::l)
- | _ -> anomaly "Instance does not match its signature")
- (evar_filtered_context evi) (array_rev_to_list args,[]))
+ (nhyps,terms)
-(*------------------------------------*
- * operations on the evar constraints *
- *------------------------------------*)
-
-(* We have a unification problem Σ; Γ |- ?e[u1..uq] = t : s where ?e is not yet
- * declared in Σ but yet known to be declarable in some context x1:T1..xq:Tq.
- * [define_evar_from_virtual_equation ... Γ Σ t (x1:T1..xq:Tq) .. (u1..uq) (x1..xq)]
- * declares x1:T1..xq:Tq |- ?e : s such that ?e[u1..uq] = t holds.
- *)
-
-let define_evar_from_virtual_equation define_fun env evd t_in_env sign filter inst_in_env =
- let ty_t_in_env = Retyping.get_type_of env evd t_in_env in
- let evd,evar_in_env = new_evar_instance sign evd ty_t_in_env ~filter inst_in_env in
- let t_in_env = whd_evar evd t_in_env in
- let evd = define_fun env evd (destEvar evar_in_env) t_in_env in
- let ids = List.map pi1 (named_context_of_val sign) in
- let inst_in_sign = List.map mkVar (list_filter_with filter ids) in
- let evar_in_sign = mkEvar (fst (destEvar evar_in_env), Array.of_list inst_in_sign) in
- (evd,whd_evar evd evar_in_sign)
-
-(* We have x1..xq |- ?e1 : τ and had to solve something like
- * Σ; Γ |- ?e1[u1..uq] = (...\y1 ... \yk ... c), where c is typically some
- * ?e2[v1..vn], hence flexible. We had to go through k binders and now
- * virtually have x1..xq, y1'..yk' | ?e1' : τ' and the equation
- * Γ, y1..yk |- ?e1'[u1..uq y1..yk] = c.
- * [materialize_evar Γ evd k (?e1[u1..uq]) τ'] extends Σ with the declaration
- * of ?e1' and returns both its instance ?e1'[x1..xq y1..yk] in an extension
- * of the context of e1 so that e1 can be instantiated by
- * (...\y1' ... \yk' ... ?e1'[x1..xq y1'..yk']),
- * and the instance ?e1'[u1..uq y1..yk] so that the remaining equation
- * ?e1'[u1..uq y1..yk] = c can be registered
- *
- * Note that, because invert_definition does not check types, we need to
- * guess the types of y1'..yn' by inverting the types of y1..yn along the
- * substitution u1..uq.
- *)
-
-let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
- let evi1 = Evd.find_undefined evd evk1 in
- let env1,rel_sign = env_rel_context_chop k env in
- let sign1 = evar_hyps evi1 in
- let filter1 = evar_filter evi1 in
- let ids1 = List.map pi1 (named_context_of_val sign1) in
- let inst_in_sign = List.map mkVar (list_filter_with filter1 ids1) in
- let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
- List.fold_right (fun (na,b,t_in_env as d) (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
- let id = next_name_away na avoid in
- let evd,t_in_sign =
- define_evar_from_virtual_equation define_fun env evd t_in_env
- sign filter inst_in_env in
- let evd,b_in_sign = match b with
- | None -> evd,None
- | Some b ->
- let evd,b = define_evar_from_virtual_equation define_fun env evd b
- sign filter inst_in_env in
- evd,Some b in
- (push_named_context_val (id,b_in_sign,t_in_sign) sign,true::filter,
- (mkRel 1)::(List.map (lift 1) inst_in_env),
- (mkRel 1)::(List.map (lift 1) inst_in_sign),
- push_rel d env,evd,id::avoid))
- rel_sign
- (sign1,filter1,Array.to_list args1,inst_in_sign,env1,evd,ids1)
- in
- let evd,ev2ty_in_sign =
- define_evar_from_virtual_equation define_fun env evd ty_in_env
- sign2 filter2 inst2_in_env in
- let evd,ev2_in_sign =
- new_evar_instance sign2 evd ev2ty_in_sign ~filter:filter2 inst2_in_sign in
- let ev2_in_env = (fst (destEvar ev2_in_sign), Array.of_list inst2_in_env) in
- (evd, ev2_in_sign, ev2_in_env)
-
-let restrict_upon_filter evd evk p args =
- let newfilter = List.map p args in
- if List.for_all (fun id -> id) newfilter then
- None
- else
- let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
- Some (apply_subfilter oldfullfilter newfilter)
-
-(* Inverting constructors in instances (common when inferring type of match) *)
-
-let find_projectable_constructor env evd cstr k args cstr_subst =
- try
- let l = Constrmap.find cstr cstr_subst in
- let args = Array.map (lift (-k)) args in
- let l =
- List.filter (fun (args',id) ->
- (* is_conv is maybe too strong (and source of useless computation) *)
- (* (at least expansion of aliases is needed) *)
- array_for_all2 (is_conv env evd) args args') l in
- List.map snd l
- with Not_found ->
- []
-
-(* [find_projectable_vars env sigma y subst] finds all vars of [subst]
- * that project on [y]. It is able to find solutions to the following
- * two kinds of problems:
- *
- * - ?n[...;x:=y;...] = y
- * - ?n[...;x:=?m[args];...] = y with ?m[args] = y recursively solvable
- *
- * (see test-suite/success/Fixpoint.v for an example of application of
- * the second kind of problem).
- *
- * The seek for [y] is up to variable aliasing. In case of solutions that
- * differ only up to aliasing, the binding that requires the less
- * steps of alias reduction is kept. At the end, only one solution up
- * to aliasing is kept.
- *
- * [find_projectable_vars] also unifies against evars that themselves mention
- * [y] and recursively.
- *
- * In short, the following situations give the following solutions:
- *
- * problem evar ctxt soluce remark
- * z1; z2:=z1 |- ?ev[z1;z2] = z1 y1:A; y2:=y1 y1 \ thanks to defs kept in
- * z1; z2:=z1 |- ?ev[z1;z2] = z2 y1:A; y2:=y1 y2 / subst and preferring =
- * z1; z2:=z1 |- ?ev[z1] = z2 y1:A y1 thanks to expand_var
- * z1; z2:=z1 |- ?ev[z2] = z1 y1:A y1 thanks to expand_var
- * z3 |- ?ev[z3;z3] = z3 y1:A; y2:=y1 y2 see make_projectable_subst
- *
- * Remark: [find_projectable_vars] assumes that identical instances of
- * variables in the same set of aliased variables are already removed (see
- * [make_projectable_subst])
- *)
-
-type evar_projection =
-| ProjectVar
-| ProjectEvar of existential * evar_info * identifier * evar_projection
-
-exception NotUnique
-exception NotUniqueInType of (identifier * evar_projection) list
-
-let rec assoc_up_to_alias sigma aliases y yc = function
- | [] -> raise Not_found
- | (c,cc,id)::l ->
- let c' = whd_evar sigma c in
- if eq_constr y c' then id
- else
- if l <> [] then assoc_up_to_alias sigma aliases y yc l
- else
- (* Last chance, we reason up to alias conversion *)
- match (if c == c' then cc else normalize_alias_opt aliases c') with
- | Some cc when eq_constr yc cc -> id
- | _ -> if eq_constr yc c then id else raise Not_found
-
-let rec find_projectable_vars with_evars aliases sigma y subst =
- let yc = normalize_alias aliases y in
- let is_projectable idc idcl subst' =
- (* First test if some [id] aliased to [idc] is bound to [y] in [subst] *)
- try
- let id = assoc_up_to_alias sigma aliases y yc idcl in
- (id,ProjectVar)::subst'
- with Not_found ->
- (* Then test if [idc] is (indirectly) bound in [subst] to some evar *)
- (* projectable on [y] *)
- if with_evars then
- let idcl' = List.filter (fun (c,_,id) -> isEvar c) idcl in
- match idcl' with
- | [c,_,id] ->
- begin
- let (evk,argsv as t) = destEvar c in
- let evi = Evd.find sigma evk in
- let subst,_ = make_projectable_subst aliases sigma evi argsv in
- let l = find_projectable_vars with_evars aliases sigma y subst in
- match l with
- | [id',p] -> (id,ProjectEvar (t,evi,id',p))::subst'
- | _ -> subst'
- end
- | [] -> subst'
- | _ -> anomaly "More than one non var in aliases class of evar instance"
- else
- subst' in
- Idmap.fold is_projectable subst []
-
-(* [filter_solution] checks if one and only one possible projection exists
- * among a set of solutions to a projection problem *)
-
-let filter_solution = function
- | [] -> raise Not_found
- | (id,p)::_::_ -> raise NotUnique
- | [id,p] -> (mkVar id, p)
-
-let project_with_effects aliases sigma effects t subst =
- let c, p =
- filter_solution (find_projectable_vars false aliases sigma t subst) in
- effects := p :: !effects;
- c
-
-let rec find_solution_type evarenv = function
- | (id,ProjectVar)::l -> pi3 (lookup_named id evarenv)
- | [id,ProjectEvar _] -> (* bugged *) pi3 (lookup_named id evarenv)
- | (id,ProjectEvar _)::l -> find_solution_type evarenv l
- | [] -> assert false
-
-(* In case the solution to a projection problem requires the instantiation of
- * subsidiary evars, [do_projection_effects] performs them; it
- * also try to instantiate the type of those subsidiary evars if their
- * type is an evar too.
- *
- * Note: typing creates new evar problems, which induces a recursive dependency
- * with [define]. To avoid a too large set of recursive functions, we
- * pass [define] to [do_projection_effects] as a parameter.
- *)
-
-let rec do_projection_effects define_fun env ty evd = function
- | ProjectVar -> evd
- | ProjectEvar ((evk,argsv),evi,id,p) ->
- let evd = Evd.define evk (mkVar id) evd in
- (* TODO: simplify constraints involving evk *)
- let evd = do_projection_effects define_fun env ty evd p in
- let ty = whd_betadeltaiota env evd (Lazy.force ty) in
- if not (isSort ty) then
- (* Don't try to instantiate if a sort because if evar_concl is an
- evar it may commit to a univ level which is not the right
- one (however, regarding coercions, because t is obtained by
- unif, we know that no coercion can be inserted) *)
- let subst = make_pure_subst evi argsv in
- let ty' = replace_vars subst evi.evar_concl in
- let ty' = whd_evar evd ty' in
- if isEvar ty' then define_fun env evd (destEvar ty') ty else evd
- else
- evd
-
-(* Assuming Σ; Γ, y1..yk |- c, [invert_arg_from_subst Γ k Σ [x1:=u1..xn:=un] c]
- * tries to return φ(x1..xn) such that equation φ(u1..un) = c is valid.
- * The strategy is to imitate the structure of c and then to invert
- * the variables of c (i.e. rels or vars of Γ) using the algorithm
- * implemented by project_with_effects/find_projectable_vars.
- * It returns either a unique solution or says whether 0 or more than
- * 1 solutions is found.
- *
- * Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
- * Postcondition: if φ(x1..xn) is returned then
- * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
- *
- * The effects correspond to evars instantiated while trying to project.
- *
- * [invert_arg_from_subst] is used on instances of evars. Since the
- * evars are flexible, these instances are potentially erasable. This
- * is why we don't investigate whether evars in the instances of evars
- * are unifiable, to the contrary of [invert_definition].
- *)
-
-type projectibility_kind =
- | NoUniqueProjection
- | UniqueProjection of constr * evar_projection list
-
-type projectibility_status =
- | CannotInvert
- | Invertible of projectibility_kind
-
-let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
- let effects = ref [] in
- let rec aux k t =
- let t = whd_evar evd t in
- match kind_of_term t with
- | Rel i when i>k0+k -> aux' k (mkRel (i-k))
- | Var id -> aux' k t
- | _ -> map_constr_with_binders succ aux k t
- and aux' k t =
- try project_with_effects aliases evd effects t subst_in_env_extended_with_k_binders
- with Not_found ->
- match expand_alias_once aliases t with
- | None -> raise Not_found
- | Some c -> aux k c in
- try
- let c = aux 0 c_in_env_extended_with_k_binders in
- Invertible (UniqueProjection (c,!effects))
- with
- | Not_found -> CannotInvert
- | NotUnique -> Invertible NoUniqueProjection
-
-let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
- let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
- match res with
- | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
- ->
- CannotInvert
- | _ ->
- res
-
-let effective_projections =
- map_succeed (function Invertible c -> c | _ -> failwith"")
-
-let instance_of_projection f env t evd projs =
- let ty = lazy (nf_evar evd (Retyping.get_type_of env evd t)) in
- match projs with
- | NoUniqueProjection -> raise NotUnique
- | UniqueProjection (c,effects) ->
- (List.fold_left (do_projection_effects f env ty) evd effects, c)
-
-exception NotEnoughInformationToInvert
-
-let extract_unique_projections projs =
- List.map (function
- | Invertible (UniqueProjection (c,_)) -> c
- | _ ->
- (* For instance, there are evars with non-invertible arguments and *)
- (* we cannot arbitrarily restrict these evars before knowing if there *)
- (* will really be used; it can also be due to some argument *)
- (* (typically a rel) that is not inversible and that cannot be *)
- (* inverted either because it is needed for typing the conclusion *)
- (* of the evar to project *)
- raise NotEnoughInformationToInvert) projs
-
-let extract_candidates sols =
- try
- Some
- (List.map (function (id,ProjectVar) -> mkVar id | _ -> raise Exit) sols)
- with Exit ->
- None
-
-let filter_of_projection = function Invertible _ -> true | _ -> false
-
-let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
- let evi = Evd.find_undefined evd evk in
- let subst,_ = make_projectable_subst aliases evd evi argsv in
- let projs =
- array_map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
- Array.of_list (extract_unique_projections projs)
-
-(* Redefines an evar with a smaller context (i.e. it may depend on less
- * variables) such that c becomes closed.
- * Example: in "fun (x:?1) (y:list ?2[x]) => x = y :> ?3[x,y] /\ x = nil bool"
- * ?3 <-- ?1 no pb: env of ?3 is larger than ?1's
- * ?1 <-- list ?2 pb: ?2 may depend on x, but not ?1.
- * What we do is that ?2 is defined by a new evar ?4 whose context will be
- * a prefix of ?2's env, included in ?1's env.
- *
- * If "hyps |- ?e : T" and "filter" selects a subset hyps' of hyps then
- * [do_restrict_hyps evd ?e filter] sets ?e:=?e'[hyps'] and returns ?e'
- * such that "hyps' |- ?e : T"
- *)
-
-let filter_effective_candidates evi filter candidates =
- match filter with
- | None -> candidates
- | Some filter ->
- let ids = List.map pi1 (list_filter_with filter (evar_context evi)) in
- List.filter (fun a -> list_subset (Idset.elements (collect_vars a)) ids)
- candidates
-
-let filter_candidates evd evk filter candidates_update =
- let evi = Evd.find_undefined evd evk in
- let candidates = match candidates_update with
- | None -> evi.evar_candidates
- | Some _ -> candidates_update
- in
- match candidates with
- | None -> None
- | Some l ->
- let l' = filter_effective_candidates evi filter l in
- if List.length l = List.length l' && candidates_update = None then
- None
- else
- Some l'
-
-let closure_of_filter evd evk filter =
- let evi = Evd.find_undefined evd evk in
- let vars = collect_vars (nf_evar evd (evar_concl evi)) in
- let test (id,c,_) b = b || Idset.mem id vars || c <> None in
- let newfilter = List.map2 test (evar_context evi) filter in
- if newfilter = evar_filter evi then None else Some newfilter
-
-let restrict_hyps evd evk filter candidates =
- (* What to do with dependencies?
- Assume we have x:A, y:B(x), z:C(x,y) |- ?e:T(x,y,z) and restrict on y.
- - If y is in a non-erasable position in C(x,y) (i.e. it is not below an
- occurrence of x in the hnf of C), then z should be removed too.
- - If y is in a non-erasable position in T(x,y,z) then the problem is
- unsolvable.
- Computing whether y is erasable or not may be costly and the
- interest for this early detection in practice is not obvious. We let
- it for future work. In any case, thanks to the use of filters, the whole
- (unrestricted) context remains consistent. *)
- let candidates = filter_candidates evd evk (Some filter) candidates in
- let typablefilter = closure_of_filter evd evk filter in
- (typablefilter,candidates)
-
-exception EvarSolvedWhileRestricting of evar_map * constr
-
-let do_restrict_hyps evd (evk,args as ev) filter candidates =
- let filter,candidates = match filter with
- | None -> None,candidates
- | Some filter -> restrict_hyps evd evk filter candidates in
- match candidates,filter with
- | Some [], _ -> error "Not solvable."
- | Some [nc],_ ->
- let evd = Evd.define evk nc evd in
- raise (EvarSolvedWhileRestricting (evd,whd_evar evd (mkEvar ev)))
- | None, None -> evd,ev
- | _ -> restrict_applied_evar evd ev filter candidates
-
-(* [postpone_non_unique_projection] postpones equation of the form ?e[?] = c *)
-(* ?e is assumed to have no candidates *)
-
-let postpone_non_unique_projection env evd (evk,argsv as ev) sols rhs =
- let rhs = expand_vars_in_term env rhs in
- let filter =
- restrict_upon_filter evd evk
- (* Keep only variables that occur in rhs *)
- (* This is not safe: is the variable is a local def, its body *)
- (* may contain references to variables that are removed, leading to *)
- (* a ill-formed context. We would actually need a notion of filter *)
- (* that says that the body is hidden. Note that expand_vars_in_term *)
- (* expands only rels and vars aliases, not rels or vars bound to an *)
- (* arbitrary complex term *)
- (fun a -> not (isRel a || isVar a)
- || dependent a rhs || List.exists (fun (id,_) -> isVarId id a) sols)
- (Array.to_list argsv) in
- let filter = match filter with
- | None -> None
- | Some filter -> closure_of_filter evd evk filter in
- let candidates = extract_candidates sols in
- if candidates <> None then
- restrict_evar evd evk filter candidates
- else
- (* We made an approximation by not expanding a local definition *)
- let evd,ev = restrict_applied_evar evd ev filter None in
- let pb = (Reduction.CONV,env,mkEvar ev,rhs) in
- Evd.add_conv_pb pb evd
-
-(* [postpone_evar_evar] postpones an equation of the form ?e1[?1] = ?e2[?2] *)
-
-let postpone_evar_evar f env evd filter1 ev1 filter2 ev2 =
- (* Leave an equation between (restrictions of) ev1 andv ev2 *)
- try
- let evd,ev1' = do_restrict_hyps evd ev1 filter1 None in
- try
- let evd,ev2' = do_restrict_hyps evd ev2 filter2 None in
- add_conv_pb (Reduction.CONV,env,mkEvar ev1',mkEvar ev2') evd
- with EvarSolvedWhileRestricting (evd,ev2) ->
- (* ev2 solved on the fly *)
- f env evd ev1' ev2
- with EvarSolvedWhileRestricting (evd,ev1) ->
- (* ev1 solved on the fly *)
- f env evd ev2 ev1
-
-(* [solve_evar_evar f Γ Σ ?e1[u1..un] ?e2[v1..vp]] applies an heuristic
- * to solve the equation Σ; Γ ⊢ ?e1[u1..un] = ?e2[v1..vp]:
- * - if there are at most one φj for each vj s.t. vj = φj(u1..un),
- * we first restrict ?e2 to the subset v_k1..v_kq of the vj that are
- * inversible and we set ?e1[x1..xn] := ?e2[φk1(x1..xn)..φkp(x1..xn)]
- * (this is a case of pattern-unification)
- * - symmetrically if there are at most one ψj for each uj s.t.
- * uj = ψj(v1..vp),
- * - otherwise, each position i s.t. ui does not occur in v1..vp has to
- * be restricted and similarly for the vi, and we leave the equation
- * as an open equation (performed by [postpone_evar])
- *
- * Warning: the notion of unique φj is relative to some given class
- * of unification problems
- *
- * Note: argument f is the function used to instantiate evars.
- *)
-
-let are_canonical_instances args1 args2 env =
- let n1 = Array.length args1 in
- let n2 = Array.length args2 in
- let rec aux n = function
- | (id,_,c)::sign
- when n < n1 && isVarId id args1.(n) && isVarId id args2.(n) ->
- aux (n+1) sign
- | [] ->
- let rec aux2 n =
- n = n1 ||
- (isRelN (n1-n) args1.(n) && isRelN (n1-n) args2.(n) && aux2 (n+1))
- in aux2 n
- | _ -> false in
- n1 = n2 & aux 0 (named_context env)
-
-let filter_compatible_candidates conv_algo env evd evi args rhs c =
- let c' = instantiate_evar (evar_filtered_context evi) c args in
- let evd, b = conv_algo env evd Reduction.CONV rhs c' in
- if b then Some (c,evd) else None
-
-exception DoesNotPreserveCandidateRestriction
-
-let restrict_candidates conv_algo env evd filter1 (evk1,argsv1) (evk2,argsv2) =
- let evi1 = Evd.find evd evk1 in
- let evi2 = Evd.find evd evk2 in
- let cand1 = filter_candidates evd evk1 filter1 None in
- let cand2 = evi2.evar_candidates in
- match cand1, cand2 with
- | _, None -> cand1
- | None, Some _ -> raise DoesNotPreserveCandidateRestriction
- | Some l1, Some l2 ->
- let args1 = Array.to_list argsv1 in
- let args2 = Array.to_list argsv2 in
- let l1' = List.filter (fun c1 ->
- let c1' = instantiate_evar (evar_filtered_context evi1) c1 args1 in
- List.filter (fun c2 ->
- (filter_compatible_candidates conv_algo env evd evi2 args2 c1' c2
- <> None)) l2 <> []) l1 in
- if List.length l1 = List.length l1' then None else Some l1'
-
-exception CannotProject of bool list option
-
-(* Assume that FV(?n[x1:=t1..xn:=tn]) belongs to some set U.
- Can ?n be instantiated by a term u depending essentially on xi such that the
- FV(u[x1:=t1..xn:=tn]) are in the set U?
- - If ti is a variable, it has to be in U.
- - If ti is a constructor, its parameters cannot be erased even if u
- matches on it, so we have to discard ti if the parameters
- contain variables not in U.
- - If ti is rigid, we have to discard it if it contains variables in U.
-
- Note: when restricting as part of an equation ?n[x1:=t1..xn:=tn] = ?m[...]
- then, occurrences of ?m in the ti can be seen, like variables, as occurrences
- of subterms to eventually discard so as to be allowed to keep ti.
-*)
-
-let rec is_constrainable_in k (ev,(fv_rels,fv_ids) as g) t =
- let f,args = decompose_app_vect t in
- match kind_of_term f with
- | Construct (ind,_) ->
- let nparams =
- (fst (Global.lookup_inductive ind)).Declarations.mind_nparams
- in
- if nparams > Array.length args
- then true (* We don't try to be more clever *)
- else
- let params,_ = array_chop nparams args in
- array_for_all (is_constrainable_in k g) params
- | Ind _ -> array_for_all (is_constrainable_in k g) args
- | Prod (_,t1,t2) -> is_constrainable_in k g t1 && is_constrainable_in k g t2
- | Evar (ev',_) -> ev' <> ev (*If ev' needed, one may also try to restrict it*)
- | Var id -> Idset.mem id fv_ids
- | Rel n -> n <= k || Intset.mem n fv_rels
- | Sort _ -> true
- | _ -> (* We don't try to be more clever *) true
-
-let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
- let t = expansion_of_var aliases t in
- match kind_of_term t with
- | Var id -> Idset.mem id fv_ids
- | Rel n -> n <= k || Intset.mem n fv_rels
- | _ -> is_constrainable_in k (ev,fvs) t
-
-let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
- let filter1 =
- restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
- (Array.to_list argsv1)
- in
- let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
- let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
- let filter2 =
- restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
- (Array.to_list argsv2)
- in
- let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
- let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
- evd,ev1,ev2
-
-exception EvarSolvedOnTheFly of evar_map * constr
-
-let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2 as ev2) =
- (* Apply filtering on ev1 so that fvs(ev1) are in fvs(ev2). *)
- let fvs2 = free_vars_and_rels_up_alias_expansion aliases (mkEvar ev2) in
- let filter1 = restrict_upon_filter evd evk1
- (has_constrainable_free_vars evd aliases k2 evk2 fvs2)
- (Array.to_list argsv1) in
- (* Only try pruning on variable substitutions, postpone otherwise. *)
- (* Rules out non-linear instances. *)
- if is_unification_pattern_pure_evar env evd ev2 (mkEvar ev1) then
- try
- let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
- let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
- evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
- with
- | EvarSolvedWhileRestricting (evd,ev1) ->
- raise (EvarSolvedOnTheFly (evd,ev1))
- | DoesNotPreserveCandidateRestriction | NotEnoughInformationToInvert ->
- raise (CannotProject filter1)
- else
- raise (CannotProject filter1)
-
-let solve_evar_evar_l2r f g env evd aliases ev1 (evk2,_ as ev2) =
- try
- let evd,body = project_evar_on_evar g env evd aliases 0 ev1 ev2 in
- Evd.define evk2 body evd
- with EvarSolvedOnTheFly (evd,c) ->
- f env evd ev2 c
-
-let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 as ev2) =
- if are_canonical_instances args1 args2 env then
- (* If instances are canonical, we solve the problem in linear time *)
- let sign = evar_filtered_context (Evd.find evd evk2) in
- let id_inst = list_map_to_array (fun (id,_,_) -> mkVar id) sign in
- Evd.define evk2 (mkEvar(evk1,id_inst)) evd
- else
- let evd,ev1,ev2 =
- (* If an evar occurs in the instance of the other evar and the
- use of an heuristic is forced, we restrict *)
- if force then ensure_evar_independent g env evd ev1 ev2 else (evd,ev1,ev2) in
- let aliases = make_alias_map env in
- try solve_evar_evar_l2r f g env evd aliases ev1 ev2
- with CannotProject filter1 ->
- try solve_evar_evar_l2r f g env evd aliases ev2 ev1
- with CannotProject filter2 ->
- postpone_evar_evar f env evd filter1 ev1 filter2 ev2
-
-type conv_fun =
- env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
-
-let check_evar_instance evd evk1 body conv_algo =
- let evi = Evd.find evd evk1 in
- let evenv = evar_unfiltered_env evi in
- (* FIXME: The body might be ill-typed when this is called from w_merge *)
- let ty =
- try Retyping.get_type_of evenv evd body
- with e when Errors.noncritical e -> error "Ill-typed evar instance"
- in
- let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
- if b then evd else
- user_err_loc (fst (evar_source evk1 evd),"",
- str "Unable to find a well-typed instantiation")
-
-(* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
- * definitions. We try to unify the ti with the ui pairwise. The pairs
- * that don't unify are discarded (i.e. ?e is redefined so that it does not
- * depend on these args). *)
-
-let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
- if array_equal eq_constr argsv1 argsv2 then evd else
- (* Filter and restrict if needed *)
- let untypedfilter =
- restrict_upon_filter evd evk
- (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
- (List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
- let candidates = filter_candidates evd evk untypedfilter None in
- let filter = match untypedfilter with
- | None -> None
- | Some filter -> closure_of_filter evd evk filter in
- let evd,ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
- if fst ev1 = evk & can_drop then (* No refinement *) evd else
- (* either progress, or not allowed to drop, e.g. to preserve possibly *)
- (* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
- (* if e can depend on x until ?y is not resolved, or, conversely, we *)
- (* don't know if ?y has to be unified with ?y, until e is resolved *)
- let argsv2 = restrict_instance evd evk filter argsv2 in
- let ev2 = (fst ev1,argsv2) in
- (* Leave a unification problem *)
- Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev1,mkEvar ev2) evd
-
-(* If the evar can be instantiated by a finite set of candidates known
- in advance, we check which of them apply *)
-
-exception NoCandidates
-
-let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
- let evi = Evd.find evd evk in
- let args = Array.to_list argsv in
- match evi.evar_candidates with
- | None -> raise NoCandidates
- | Some l ->
- let l' =
- list_map_filter
- (filter_compatible_candidates conv_algo env evd evi args rhs) l in
- match l' with
- | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
- | [c,evd] ->
- (* solve_candidates might have been called recursively in the mean *)
- (* time and the evar been solved by the filtering process *)
- if Evd.is_undefined evd evk then Evd.define evk c evd else evd
- | l when List.length l < List.length l' ->
- let candidates = List.map fst l in
- restrict_evar evd evk None (Some candidates)
- | l -> evd
-
-(* We try to instantiate the evar assuming the body won't depend
- * on arguments that are not Rels or Vars, or appearing several times
- * (i.e. we tackle a generalization of Miller-Pfenning patterns unification)
- *
- * 1) Let "env |- ?ev[hyps:=args] = rhs" be the unification problem
- * 2) We limit it to a patterns unification problem "env |- ev[subst] = rhs"
- * where only Rel's and Var's are relevant in subst
- * 3) We recur on rhs, "imitating" the term, and failing if some Rel/Var is
- * not in the scope of ?ev. For instance, the problem
- * "y:nat |- ?x[] = y" where "|- ?1:nat" is not satisfiable because
- * ?1 would be instantiated by y which is not in the scope of ?1.
- * 4) We try to "project" the term if the process of imitation fails
- * and that only one projection is possible
- *
- * Note: we don't assume rhs in normal form, it may fail while it would
- * have succeeded after some reductions.
- *
- * This is the work of [invert_definition Γ Σ ?ev[hyps:=args] c]
- * Precondition: Σ; Γ, y1..yk |- c /\ Σ; Γ |- u1..un
- * Postcondition: if φ(x1..xn) is returned then
- * Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
- *)
-
-exception NotInvertibleUsingOurAlgorithm of constr
-exception NotEnoughInformationToProgress of (identifier * evar_projection) list
-exception NotEnoughInformationEvarEvar of constr
-exception OccurCheckIn of evar_map * constr
-
-let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
- let aliases = make_alias_map env in
- let evdref = ref evd in
- let progress = ref false in
- let evi = Evd.find evd evk in
- let subst,cstr_subst = make_projectable_subst aliases evd evi argsv in
-
- (* Projection *)
- let project_variable t =
- (* Evar/Var problem: unifiable iff variable projectable from ev subst *)
- try
- let sols = find_projectable_vars true aliases !evdref t subst in
- let c, p = match sols with
- | [] -> raise Not_found
- | [id,p] -> (mkVar id, p)
- | (id,p)::_::_ ->
- if choose then (mkVar id, p) else raise (NotUniqueInType sols)
- in
- let ty = lazy (Retyping.get_type_of env !evdref t) in
- let evd = do_projection_effects (evar_define conv_algo) env ty !evdref p in
- evdref := evd;
- c
- with
- | Not_found -> raise (NotInvertibleUsingOurAlgorithm t)
- | NotUniqueInType sols ->
- if not !progress then
- raise (NotEnoughInformationToProgress sols);
- (* No unique projection but still restrict to where it is possible *)
- (* materializing is necessary, but is restricting useful? *)
- let ty = find_solution_type (evar_env evi) sols in
- let sign = evar_filtered_context evi in
- let ty' = instantiate_evar sign ty (Array.to_list argsv) in
- let (evd,evar,(evk',argsv' as ev')) =
- materialize_evar (evar_define conv_algo) env !evdref 0 ev ty' in
- let ts = expansions_of_var aliases t in
- let test c = isEvar c or List.mem c ts in
- let filter = array_map_to_list test argsv' in
- let filter = apply_subfilter (evar_filter (Evd.find_undefined evd evk)) filter in
-
- let filter = closure_of_filter evd evk' filter in
- let candidates = extract_candidates sols in
- let evd =
- if candidates <> None then restrict_evar evd evk' filter candidates
- else
- let evd,ev'' = restrict_applied_evar evd ev' filter None in
- Evd.add_conv_pb (Reduction.CONV,env,mkEvar ev'',t) evd in
- evdref := evd;
- evar in
-
- let rec imitate (env',k as envk) t =
- let t = whd_evar !evdref t in
- match kind_of_term t with
- | Rel i when i>k ->
- (match pi2 (Environ.lookup_rel (i-k) env') with
- | None -> project_variable (mkRel (i-k))
- | Some b ->
- try project_variable (mkRel (i-k))
- with NotInvertibleUsingOurAlgorithm _ -> imitate envk (lift i b))
- | Var id ->
- (match pi2 (Environ.lookup_named id env') with
- | None -> project_variable t
- | Some b ->
- try project_variable t
- with NotInvertibleUsingOurAlgorithm _ -> imitate envk b)
- | Evar (evk',args' as ev') ->
- if evk = evk' then raise (OccurCheckIn (evd,rhs));
- (* Evar/Evar problem (but left evar is virtual) *)
- let aliases = lift_aliases k aliases in
- (try
- let ev = (evk,Array.map (lift k) argsv) in
- let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in
- evdref := evd;
- body
- with
- | EvarSolvedOnTheFly (evd,t) -> evdref:=evd; imitate envk t
- | CannotProject filter' ->
- if not !progress then
- raise (NotEnoughInformationEvarEvar t);
- (* Make the virtual left evar real *)
- let ty = get_type_of env' !evdref t in
- let (evd,evar'',ev'') =
- materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
- (* materialize_evar may instantiate ev' by another evar; adjust it *)
- let (evk',args' as ev') = normalize_evar evd ev' in
- let evd =
- (* Try to project (a restriction of) the left evar ... *)
- try
- let evd,body = project_evar_on_evar conv_algo env' evd aliases 0 ev'' ev' in
- Evd.define evk' body evd
- with
- | EvarSolvedOnTheFly _ -> assert false (* ev has no candidates *)
- | CannotProject filter'' ->
- (* ... or postpone the problem *)
- postpone_evar_evar (evar_define conv_algo) env' evd filter'' ev'' filter' ev' in
- evdref := evd;
- evar'')
- | _ ->
- progress := true;
- match
- let c,args = decompose_app_vect t in
- match kind_of_term c with
- | Construct cstr when noccur_between 1 k t ->
- (* This is common case when inferring the return clause of match *)
- (* (currently rudimentary: we do not treat the case of multiple *)
- (* possible inversions; we do not treat overlap with a possible *)
- (* alternative inversion of the subterms of the constructor, etc)*)
- (match find_projectable_constructor env evd cstr k args cstr_subst with
- | _::_ as l -> Some (List.map mkVar l)
- | _ -> None)
- | _ -> None
- with
- | Some l ->
- let ty = get_type_of env' !evdref t in
- let candidates =
- try
- let t =
- map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
- imitate envk t in
- t::l
- with e when Errors.noncritical e -> l in
- (match candidates with
- | [x] -> x
- | _ ->
- let (evd,evar'',ev'') =
- materialize_evar (evar_define conv_algo) env' !evdref k ev ty in
- evdref := restrict_evar evd (fst ev'') None (Some candidates);
- evar'')
- | None ->
- (* Evar/Rigid problem (or assimilated if not normal): we "imitate" *)
- map_constr_with_full_binders (fun d (env,k) -> push_rel d env, k+1)
- imitate envk t in
-
- let rhs = whd_beta evd rhs (* heuristic *) in
- let body = imitate (env,0) rhs in
- (!evdref,body)
-
-(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
- * an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
- * [define] tries to find an instance lhs such that
- * "lhs [hyps:=args]" unifies to rhs. The term "lhs" must be closed in
- * context "hyps" and not referring to itself.
- *)
-
-and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
- match kind_of_term rhs with
- | Evar (evk2,argsv2 as ev2) ->
- if evk = evk2 then
- solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
- else
- solve_evar_evar ~force:choose
- (evar_define conv_algo) conv_algo env evd ev ev2
- | _ ->
- try solve_candidates conv_algo env evd ev rhs
- with NoCandidates ->
- try
- let (evd',body) = invert_definition conv_algo choose env evd ev rhs in
- if occur_meta body then error "Meta cannot occur in evar body.";
- (* invert_definition may have instantiate some evars of rhs with evk *)
- (* so we recheck acyclicity *)
- if occur_evar evk body then raise (OccurCheckIn (evd',body));
- (* needed only if an inferred type *)
- let body = refresh_universes body in
-(* Cannot strictly type instantiations since the unification algorithm
- * does not unify applications from left to right.
- * e.g problem f x == g y yields x==y and f==g (in that order)
- * Another problem is that type variables are evars of type Type
- let _ =
- try
- let env = evar_env evi in
- let ty = evi.evar_concl in
- Typing.check env evd' body ty
- with e ->
- pperrnl
- (str "Ill-typed evar instantiation: " ++ fnl() ++
- pr_evar_map evd' ++ fnl() ++
- str "----> " ++ int ev ++ str " := " ++
- print_constr body);
- raise e in*)
- let evd' = Evd.define evk body evd' in
- check_evar_instance evd' evk body conv_algo
- with
- | NotEnoughInformationToProgress sols ->
- postpone_non_unique_projection env evd ev sols rhs
- | NotEnoughInformationEvarEvar t ->
- add_conv_pb (Reduction.CONV,env,mkEvar ev,t) evd
- | NotInvertibleUsingOurAlgorithm t ->
- error_not_clean env evd evk t (evar_source evk evd)
- | OccurCheckIn (evd,rhs) ->
- (* last chance: rhs actually reduces to ev *)
- let c = whd_betadeltaiota env evd rhs in
- match kind_of_term c with
- | Evar (evk',argsv2) when evk = evk' ->
- solve_refl
- (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
- env evd evk argsv argsv2
- | _ ->
- error_occur_check env evd evk rhs
-
-(* This code (i.e. solve_pb, etc.) takes a unification
- * problem, and tries to solve it. If it solves it, then it removes
- * all the conversion problems, and re-runs conversion on each one, in
- * the hopes that the new solution will aid in solving them.
- *
- * The kinds of problems it knows how to solve are those in which
- * the usable arguments of an existential var are all themselves
- * universal variables.
- * The solution to this problem is to do renaming for the Var's,
- * to make them match up with the Var's which are found in the
- * hyps of the existential, to do a "pop" for each Rel which is
- * not an argument of the existential, and a subst1 for each which
- * is, again, with the corresponding variable. This is done by
- * define
- *
- * Thus, we take the arguments of the existential which we are about
- * to assign, and zip them with the identifiers in the hypotheses.
- * Then, we process all the Var's in the arguments, and sort the
- * Rel's into ascending order. Then, we just march up, doing
- * subst1's and pop's.
- *
- * NOTE: We can do this more efficiently for the relative arguments,
- * by building a long substituend by hand, but this is a pain in the
- * ass.
- *)
+let clear_hyps_in_evi env evdref hyps concl ids =
+ match clear_hyps_in_evi_main env evdref hyps [concl] ids with
+ | (nhyps,[nconcl]) -> (nhyps,nconcl)
+ | _ -> assert false
-let status_changed lev (pbty,_,t1,t2) =
- (try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
- (try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
-
-let reconsider_conv_pbs conv_algo evd =
- let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
- List.fold_left
- (fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
- pbs
-
-(* Tries to solve problem t1 = t2.
- * Precondition: t1 is an uninstantiated evar
- * Returns an optional list of evars that were instantiated, or None
- * if the problem couldn't be solved. *)
-
-(* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
-let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1),t2) =
- try
- let t2 = whd_betaiota evd t2 in (* includes whd_evar *)
- let evd =
- match pbty with
- | Some true when isEvar t2 ->
- add_conv_pb (Reduction.CUMUL,env,mkEvar ev1,t2) evd
- | Some false when isEvar t2 ->
- add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
- | _ ->
- evar_define conv_algo ~choose env evd ev1 t2 in
- reconsider_conv_pbs conv_algo evd
- with e when precatchable_exception e ->
- (evd,false)
-
-(** The following functions return the set of evars immediately
- contained in the object, including defined evars *)
-
-let evars_of_term c =
- let rec evrec acc c =
- match kind_of_term c with
- | Evar (n, l) -> Intset.add n (Array.fold_left evrec acc l)
- | _ -> fold_constr evrec acc c
- in
- evrec Intset.empty c
+let clear_hyps2_in_evi env evdref hyps t concl ids =
+ match clear_hyps_in_evi_main env evdref hyps [t;concl] ids with
+ | (nhyps,[t;nconcl]) -> (nhyps,t,nconcl)
+ | _ -> assert false
(* spiwack: a few functions to gather evars on which goals depend. *)
let queue_set q is_dependent set =
- Intset.iter (fun a -> Queue.push (is_dependent,a) q) set
+ Evar.Set.iter (fun a -> Queue.push (is_dependent,a) q) set
let queue_term q is_dependent c =
queue_set q is_dependent (evars_of_term c)
@@ -1830,7 +575,7 @@ let process_dependent_evar q acc evm is_dependent e =
end (Environ.named_context_of_val evi.evar_hyps);
match evi.evar_body with
| Evar_empty ->
- if is_dependent then Intmap.add e None acc else acc
+ if is_dependent then Evar.Map.add e None acc else acc
| Evar_defined b ->
let subevars = evars_of_term b in
(* evars appearing in the definition of an evar [e] are marked
@@ -1838,14 +583,14 @@ let process_dependent_evar q acc evm is_dependent e =
non-dependent goal, then, unless they are reach from another
path, these evars are just other non-dependent goals. *)
queue_set q is_dependent subevars;
- if is_dependent then Intmap.add e (Some subevars) acc else acc
+ if is_dependent then Evar.Map.add e (Some subevars) acc else acc
let gather_dependent_evars q evm =
- let acc = ref Intmap.empty in
+ let acc = ref Evar.Map.empty in
while not (Queue.is_empty q) do
let (is_dependent,e) = Queue.pop q in
(* checks if [e] has already been added to [!acc] *)
- begin if not (Intmap.mem e !acc) then
+ begin if not (Evar.Map.mem e !acc) then
acc := process_dependent_evar q !acc evm is_dependent e
end
done;
@@ -1858,21 +603,6 @@ let gather_dependent_evars evm l =
(* /spiwack *)
-let evars_of_named_context nc =
- List.fold_right (fun (_, b, t) s ->
- Option.fold_left (fun s t ->
- Intset.union s (evars_of_term t))
- (Intset.union s (evars_of_term t)) b)
- nc Intset.empty
-
-let evars_of_evar_info evi =
- Intset.union (evars_of_term evi.evar_concl)
- (Intset.union
- (match evi.evar_body with
- | Evar_empty -> Intset.empty
- | Evar_defined b -> evars_of_term b)
- (evars_of_named_context (named_context_of_val evi.evar_hyps)))
-
(** The following functions return the set of undefined evars
contained in the object, the defined evars being traversed.
This is roughly a combination of the previous functions and
@@ -1884,25 +614,25 @@ let undefined_evars_of_term evd t =
| Evar (n, l) ->
let acc = Array.fold_left evrec acc l in
(try match (Evd.find evd n).evar_body with
- | Evar_empty -> Intset.add n acc
+ | Evar_empty -> Evar.Set.add n acc
| Evar_defined c -> evrec acc c
- with Not_found -> anomaly "undefined_evars_of_term: evar not found")
+ with Not_found -> anomaly ~label:"undefined_evars_of_term" (Pp.str "evar not found"))
| _ -> fold_constr evrec acc c
in
- evrec Intset.empty t
+ evrec Evar.Set.empty t
let undefined_evars_of_named_context evd nc =
List.fold_right (fun (_, b, t) s ->
Option.fold_left (fun s t ->
- Intset.union s (undefined_evars_of_term evd t))
- (Intset.union s (undefined_evars_of_term evd t)) b)
- nc Intset.empty
+ Evar.Set.union s (undefined_evars_of_term evd t))
+ (Evar.Set.union s (undefined_evars_of_term evd t)) b)
+ nc Evar.Set.empty
let undefined_evars_of_evar_info evd evi =
- Intset.union (undefined_evars_of_term evd evi.evar_concl)
- (Intset.union
+ Evar.Set.union (undefined_evars_of_term evd evi.evar_concl)
+ (Evar.Set.union
(match evi.evar_body with
- | Evar_empty -> Intset.empty
+ | Evar_empty -> Evar.Set.empty
| Evar_defined b -> undefined_evars_of_term evd b)
(undefined_evars_of_named_context evd
(named_context_of_val evi.evar_hyps)))
@@ -1919,21 +649,29 @@ let check_evars env initial_sigma sigma c =
if not (Evd.mem initial_sigma evk) then
let (loc,k) = evar_source evk sigma in
match k with
- | ImplicitArg (gr, (i, id), false) -> ()
- | _ ->
- let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in
- error_unsolvable_implicit loc env sigma evi k None)
+ | Evar_kinds.ImplicitArg (gr, (i, id), false) -> ()
+ | _ -> error_unsolvable_implicit loc env sigma evk None)
| _ -> iter_constr proc_rec c
in proc_rec c
-open Glob_term
+(* spiwack: this is a more complete version of
+ {!Termops.occur_evar}. The latter does not look recursively into an
+ [evar_map]. If unification only need to check superficially, tactics
+ do not have this luxury, and need the more complete version. *)
+let occur_evar_upto sigma n c =
+ let rec occur_rec c = match kind_of_term c with
+ | Evar (sp,_) when Evar.equal sp n -> raise Occur
+ | Evar e -> Option.iter occur_rec (existential_opt_value sigma e)
+ | _ -> iter_constr occur_rec c
+ in
+ try occur_rec c; false with Occur -> true
+
(****************************************)
(* Operations on value/type constraints *)
(****************************************)
-type type_constraint_type = (int * int) option * constr
-type type_constraint = type_constraint_type option
+type type_constraint = types option
type val_constraint = constr option
@@ -1954,14 +692,8 @@ type val_constraint = constr option
(* The empty type constraint *)
let empty_tycon = None
-let mk_tycon_type c = (None, c)
-let mk_abstr_tycon_type n c = (Some (n, n), c) (* First component is initial abstraction, second
- is current abstraction *)
-
(* Builds a type constraint *)
-let mk_tycon ty = Some (mk_tycon_type ty)
-
-let mk_abstr_tycon n ty = Some (mk_abstr_tycon_type n ty)
+let mk_tycon ty = Some ty
(* Constrains the value of a type *)
let empty_valcon = None
@@ -1969,24 +701,34 @@ let empty_valcon = None
(* Builds a value constraint *)
let mk_valcon c = Some c
-
-let idx = id_of_string "x"
+let idx = Namegen.default_dependent_ident
(* Refining an evar to a product *)
let define_pure_evar_as_product evd evk =
let evi = Evd.find_undefined evd evk in
- let evenv = evar_unfiltered_env evi in
+ let evenv = evar_env evi in
let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
- let evd1,dom = new_type_evar evd evenv ~filter:(evar_filter evi) in
+ let concl = whd_evar evd evi.evar_concl in
+ let s = destSort concl in
+ let evd1,(dom,u1) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
let evd2,rng =
let newenv = push_named (id, None, dom) evenv in
let src = evar_source evk evd1 in
- let filter = true::evar_filter evi in
- new_type_evar evd1 newenv ~src ~filter in
+ let filter = Filter.extend 1 (evar_filter evi) in
+ if is_prop_sort s then
+ (* Impredicative product, conclusion must fall in [Prop]. *)
+ new_evar newenv evd1 concl ~src ~filter
+ else
+ let evd3, (rng, srng) =
+ new_type_evar newenv evd1 univ_flexible_alg ~src ~filter in
+ let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
+ let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
+ evd3, rng
+ in
let prod = mkProd (Name id, dom, subst_var id rng) in
let evd3 = Evd.define evk prod evd2 in
- evd3,prod
+ evd3,prod
(* Refine an applied evar to a product and returns its instantiation *)
@@ -1995,7 +737,7 @@ let define_evar_as_product evd (evk,args) =
(* Quick way to compute the instantiation of evk with args *)
let na,dom,rng = destProd prod in
let evdom = mkEvar (fst (destEvar dom), args) in
- let evrngargs = array_cons (mkRel 1) (Array.map (lift 1) args) in
+ let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
let evrng = mkEvar (fst (destEvar rng), evrngargs) in
evd,mkProd (na, evdom, evrng)
@@ -2010,19 +752,19 @@ let define_evar_as_product evd (evk,args) =
let define_pure_evar_as_lambda env evd evk =
let evi = Evd.find_undefined evd evk in
- let evenv = evar_unfiltered_env evi in
+ let evenv = evar_env evi in
let typ = whd_betadeltaiota env evd (evar_concl evi) in
let evd1,(na,dom,rng) = match kind_of_term typ with
| Prod (na,dom,rng) -> (evd,(na,dom,rng))
| Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
- | _ -> error_not_product_loc dummy_loc env evd typ in
+ | _ -> error_not_product_loc Loc.ghost env evd typ in
let avoid = ids_of_named_context (evar_context evi) in
let id =
next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in
let newenv = push_named (id, None, dom) evenv in
- let filter = true::evar_filter evi in
+ let filter = Filter.extend 1 (evar_filter evi) in
let src = evar_source evk evd1 in
- let evd2,body = new_evar evd1 newenv ~src (subst1 (mkVar id) rng) ~filter in
+ let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
let lam = mkLambda (Name id, dom, subst_var id body) in
Evd.define evk lam evd2, lam
@@ -2030,7 +772,7 @@ let define_evar_as_lambda env evd (evk,args) =
let evd,lam = define_pure_evar_as_lambda env evd evk in
(* Quick way to compute the instantiation of evk with args *)
let na,dom,body = destLambda lam in
- let evbodyargs = array_cons (mkRel 1) (Array.map (lift 1) args) in
+ let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
let evbody = mkEvar (fst (destEvar body), evbodyargs) in
evd,mkLambda (na, dom, evbody)
@@ -2041,30 +783,29 @@ let rec evar_absorb_arguments env evd (evk,args as ev) = function
let evd,lam = define_pure_evar_as_lambda env evd evk in
let _,_,body = destLambda lam in
let evk = fst (destEvar body) in
- evar_absorb_arguments env evd (evk, array_cons a args) l
+ evar_absorb_arguments env evd (evk, Array.cons a args) l
(* Refining an evar to a sort *)
-let define_evar_as_sort evd (ev,args) =
- let evd, s = new_sort_variable evd in
- Evd.define ev (mkSort s) evd, s
+let define_evar_as_sort env evd (ev,args) =
+ let evd, u = new_univ_variable univ_rigid evd in
+ let evi = Evd.find_undefined evd ev in
+ let s = Type u in
+ let evd' = Evd.define ev (mkSort s) evd in
+ Evd.set_leq_sort env evd' (Type (Univ.super u)) (destSort evi.evar_concl), s
(* We don't try to guess in which sort the type should be defined, since
any type has type Type. May cause some trouble, but not so far... *)
let judge_of_new_Type evd =
- let evd', s = new_univ_variable evd in
- evd', Typeops.judge_of_type s
+ let evd', s = new_univ_variable univ_rigid evd in
+ evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }
(* Propagation of constraints through application and abstraction:
Given a type constraint on a functional term, returns the type
constraint on its domain and codomain. If the input constraint is
an evar instantiate it with the product of 2 new evars. *)
-let unlift_tycon init cur c =
- if cur = 1 then None, c
- else Some (init, pred cur), c
-
let split_tycon loc env evd tycon =
let rec real_split evd c =
let t = whd_betadeltaiota env evd c in
@@ -2081,35 +822,19 @@ let split_tycon loc env evd tycon =
in
match tycon with
| None -> evd,(Anonymous,None,None)
- | Some (abs, c) ->
- (match abs with
- None ->
- let evd', (n, dom, rng) = real_split evd c in
- evd', (n, mk_tycon dom, mk_tycon rng)
- | Some (init, cur) ->
- evd, (Anonymous, None, Some (unlift_tycon init cur c)))
-
-let valcon_of_tycon x =
- match x with
- | Some (None, t) -> Some t
- | _ -> None
-
-let lift_abstr_tycon_type n (abs, t) =
- match abs with
- None -> raise (Invalid_argument "lift_abstr_tycon_type: not an abstraction")
- | Some (init, abs) ->
- let abs' = abs + n in
- if abs' < 0 then raise (Invalid_argument "lift_abstr_tycon_type")
- else (Some (init, abs'), t)
-
-let lift_tycon_type n (abs, t) = (abs, lift n t)
-let lift_tycon n = Option.map (lift_tycon_type n)
-
-let pr_tycon_type env (abs, t) =
- match abs with
- None -> Termops.print_constr_env env t
- | Some (init, cur) -> str "Abstract (" ++ int init ++ str "," ++ int cur ++ str ") " ++ Termops.print_constr_env env t
+ | Some c ->
+ let evd', (n, dom, rng) = real_split evd c in
+ evd', (n, mk_tycon dom, mk_tycon rng)
+
+let valcon_of_tycon x = x
+let lift_tycon n = Option.map (lift n)
let pr_tycon env = function
None -> str "None"
- | Some t -> pr_tycon_type env t
+ | Some t -> Termops.print_constr_env env t
+
+let subterm_source evk (loc,k) =
+ let evk = match k with
+ | Evar_kinds.SubEvar (evk) -> evk
+ | _ -> evk in
+ (loc,Evar_kinds.SubEvar evk)