diff options
Diffstat (limited to 'pretyping/evarutil.ml')
| -rw-r--r-- | pretyping/evarutil.ml | 127 |
1 files changed, 62 insertions, 65 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index fafce268..130e23b8 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evarutil.ml 11127 2008-06-14 15:39:46Z herbelin $ *) +(* $Id: evarutil.ml 11309 2008-08-06 10:30:35Z herbelin $ *) open Util open Pp @@ -374,42 +374,41 @@ let restrict_upon_filter evd evi evk p args = else evd,evk,args -exception Dependency_error of identifier +let collect_vars c = + let rec collrec acc c = + match kind_of_term c with + | Var id -> list_add_set id acc + | _ -> fold_constr collrec acc c + in + collrec [] c -module EvkOrd = -struct - type t = Term.existential_key - let compare = Pervasives.compare -end +type clear_dependency_error = +| OccurHypInSimpleClause of identifier option +| EvarTypingBreak of existential -module EvkSet = Set.Make(EvkOrd) +exception ClearDependencyError of identifier * clear_dependency_error -let rec check_and_clear_in_constr evdref c ids hist = +let rec check_and_clear_in_constr 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 *) + evars) *) let check id' = if List.mem id' ids then - raise (Dependency_error id') + raise (ClearDependencyError (id',err)) in match kind_of_term c with - | ( Rel _ | Meta _ | Sort _ ) -> c - - | ( Const _ | Ind _ | Construct _ ) -> - let vars = Environ.vars_of_global (Global.env()) c in - List.iter check vars; c + | Var id' -> + check id'; c - | Var id' -> - check id'; mkVar id' + | ( Const _ | Ind _ | Construct _ ) -> + let vars = Environ.vars_of_global (Global.env()) c in + List.iter check vars; c | Evar (evk,l as ev) -> if Evd.is_defined_evar !evdref ev then (* If evk is already defined we replace it by its definition *) - let nc = nf_evar (evars_of !evdref) c in - (check_and_clear_in_constr evdref nc ids hist) - else if EvkSet.mem evk hist then - (* Loop detection => do nothing *) - c + let nc = whd_evar (evars_of !evdref) c in + (check_and_clear_in_constr 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 @@ -418,16 +417,32 @@ let rec check_and_clear_in_constr evdref c ids hist = removed *) let evi = Evd.find (evars_of !evdref) evk in let ctxt = Evd.evar_filtered_context evi in - let (nhyps,nargs,rids) = + let (nhyps,nargs,rids) = List.fold_right2 (fun (rid,ob,c as h) a (hy,ar,ri) -> - match kind_of_term a with - | Var id -> if List.mem id ids then (hy,ar,id::ri) else (h::hy,a::ar,ri) - | _ -> (h::hy,a::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) (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 + | rid' :: _ -> (hy,ar,(rid,List.assoc rid ri)::ri) + | _ -> + (* No dependency at all, we can keep this ev's context hyp *) + (h::hy,a::ar,ri)) ctxt (Array.to_list l) ([],[],[]) in - (* nconcl must be computed ids (non instanciated hyps) *) - let nconcl = check_and_clear_in_constr evdref (evar_concl evi) rids (EvkSet.add evk hist) 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) + with ClearDependencyError (rid,err) -> + raise (ClearDependencyError (List.assoc rid rids,err)) in 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 @@ -435,24 +450,19 @@ let rec check_and_clear_in_constr evdref c ids hist = let (evk',_) = destEvar ev' in mkEvar(evk', Array.of_list nargs) - | _ -> map_constr (fun c -> check_and_clear_in_constr evdref c ids hist) c + | _ -> map_constr (check_and_clear_in_constr evdref err ids) c let clear_hyps_in_evi evdref hyps concl ids = - (* clear_evar_hyps erases hypotheses ids in hyps, checking if some + (* 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 = try check_and_clear_in_constr evdref concl ids EvkSet.empty - with Dependency_error id' -> error (string_of_id id' ^ " is used in conclusion") in - let (nhyps,_) = - let check_context (id,ob,c) = - try - (id, - (match ob with - None -> None - | Some b -> Some (check_and_clear_in_constr evdref b ids EvkSet.empty)), - check_and_clear_in_constr evdref c ids EvkSet.empty) - with Dependency_error id' -> error (string_of_id id' ^ " is used in hypothesis " - ^ string_of_id id) + let nconcl = + check_and_clear_in_constr evdref (OccurHypInSimpleClause None) ids concl in + let nhyps = + let check_context (id,ob,c) = + 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) in let check_value vk = match !vk with @@ -469,6 +479,7 @@ let clear_hyps_in_evi evdref hyps concl ids = in (nhyps,nconcl) + (* 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 *) @@ -883,7 +894,7 @@ let rec invert_definition env evd (evk,argsv as ev) rhs = and evar_define env (evk,_ as ev) rhs evd = try let (evd',body) = invert_definition env evd ev rhs in - if occur_meta body then error "Meta cannot occur in evar body"; + 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 error_occur_check env (evars_of evd) evk body; @@ -1057,22 +1068,7 @@ let check_evars env initial_sigma evd c = if not (Evd.mem initial_sigma evk) then let (loc,k) = evar_source evk evd in let evi = nf_evar_info sigma (Evd.find sigma evk) in - let explain = - let f (_,_,t1,t2) = - (try head_evar t1 = evk with Failure _ -> false) - or (try head_evar t2 = evk with Failure _ -> false) in - let check_several c inst = - let _,argsv = destEvar c in - let l = List.filter (eq_constr inst) (Array.to_list argsv) in - let n = List.length l in - (* Maybe should we select one instead of failing ... *) - if n >= 2 then Some (SeveralInstancesFound n) else None in - match List.filter f (snd (extract_all_conv_pbs evd)) with - | (_,_,t1,t2)::_ -> - if isEvar t2 then check_several t2 t1 - else check_several t1 t2 - | [] -> None - in error_unsolvable_implicit loc env sigma evi k explain + error_unsolvable_implicit loc env sigma evi k None | _ -> iter_constr proc_rec c in proc_rec c @@ -1183,11 +1179,12 @@ let split_tycon loc env evd tycon = if cur = 0 then let evd', (x, dom, rng) = real_split c in evd, (Anonymous, - Some (Some (init, 0), dom), - Some (Some (init, 0), rng)) + Some (None, dom), + Some (None, rng)) else - evd, (Anonymous, None, Some (Some (init, pred cur), c))) - + evd, (Anonymous, None, + Some (if cur = 1 then None,c else Some (init, pred cur), c))) + let valcon_of_tycon x = match x with | Some (None, t) -> Some t |