diff options
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 561 |
1 files changed, 300 insertions, 261 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 2db77837..5d6ca2ca 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml 14641 2011-11-06 11:59:10Z herbelin $ *) - open Pp open Util open Names @@ -51,7 +49,8 @@ type evar_info = { evar_body : evar_body; evar_filter : bool list; evar_source : hole_kind located; - evar_extra : Dyn.t option} + evar_candidates : constr list option; (* if not None, list of allowed instances *) + evar_extra : Store.t } let make_evar hyps ccl = { evar_concl = ccl; @@ -59,7 +58,8 @@ let make_evar hyps ccl = { evar_body = Evar_empty; evar_filter = List.map (fun _ -> true) (named_context_of_val hyps); evar_source = (dummy_loc,InternalHole); - evar_extra = None + evar_candidates = None; + evar_extra = Store.empty } let evar_concl evi = evi.evar_concl @@ -81,10 +81,10 @@ let eq_evar_info ei1 ei2 = ei1.evar_body = ei2.evar_body (* spiwack: Revised hierarchy : - - ExistentialMap ( Maps of existential_keys ) - - EvarInfoMap ( .t = evar_info ExistentialMap.t ) - - EvarMap ( .t = EvarInfoMap.t * sort_constraints ) - - evar_map (exported) + - ExistentialMap ( Maps of existential_keys ) + - EvarInfoMap ( .t = evar_info ExistentialMap.t * evar_info ExistentialMap ) + - EvarMap ( .t = EvarInfoMap.t * sort_constraints ) + - evar_map (exported) *) module ExistentialMap = Intmap @@ -93,72 +93,95 @@ module ExistentialSet = Intset (* This exception is raised by *.existential_value *) exception NotInstantiatedEvar +(* Note: let-in contributes to the instance *) +let make_evar_instance sign args = + let rec instrec = function + | (id,_,_) :: sign, c::args when isVarId id c -> instrec (sign,args) + | (id,_,_) :: sign, c::args -> (id,c) :: instrec (sign,args) + | [],[] -> [] + | [],_ | _,[] -> anomaly "Signature and its instance do not match" + in + instrec (sign,args) + +let instantiate_evar sign c args = + let inst = make_evar_instance sign args in + if inst = [] then c else replace_vars inst c + module EvarInfoMap = struct - type t = evar_info ExistentialMap.t + type t = evar_info ExistentialMap.t * evar_info ExistentialMap.t - let empty = ExistentialMap.empty + let empty = ExistentialMap.empty, ExistentialMap.empty - let to_list evc = (* Workaround for change in Map.fold behavior *) + let is_empty (d,u) = ExistentialMap.is_empty d && ExistentialMap.is_empty u + + let has_undefined (_,u) = not (ExistentialMap.is_empty u) + + let to_list (def,undef) = + (* Workaround for change in Map.fold behavior in ocaml 3.08.4 *) let l = ref [] in - ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) evc; + ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) def; + ExistentialMap.iter (fun evk x -> l := (evk,x)::!l) undef; !l - let dom evc = ExistentialMap.fold (fun evk _ acc -> evk::acc) evc [] - let find evc k = ExistentialMap.find k evc - let remove evc k = ExistentialMap.remove k evc - let mem evc k = ExistentialMap.mem k evc - let fold = ExistentialMap.fold - let exists evc f = ExistentialMap.fold (fun k v b -> b || f k v) evc false + let undefined_list (def,undef) = + (* Order is important: needs ocaml >= 3.08.4 from which "fold" is a + "fold_left" *) + ExistentialMap.fold (fun evk evi l -> (evk,evi)::l) undef [] + + let undefined_evars (def,undef) = (ExistentialMap.empty,undef) + let defined_evars (def,undef) = (def,ExistentialMap.empty) + + let find (def,undef) k = + try ExistentialMap.find k def + with Not_found -> ExistentialMap.find k undef + let find_undefined (def,undef) k = ExistentialMap.find k undef + let remove (def,undef) k = + (ExistentialMap.remove k def,ExistentialMap.remove k undef) + let mem (def,undef) k = + ExistentialMap.mem k def || ExistentialMap.mem k undef + let fold (def,undef) f a = + ExistentialMap.fold f def (ExistentialMap.fold f undef a) + let fold_undefined (def,undef) f a = + ExistentialMap.fold f undef a + let exists_undefined (def,undef) f = + ExistentialMap.fold (fun k v b -> b || f k v) undef false + + let add (def,undef) evk newinfo = + if newinfo.evar_body = Evar_empty then + (def,ExistentialMap.add evk newinfo undef) + else + (ExistentialMap.add evk newinfo def,undef) - let add evd evk newinfo = ExistentialMap.add evk newinfo evd + let add_undefined (def,undef) evk newinfo = + assert (newinfo.evar_body = Evar_empty); + (def,ExistentialMap.add evk newinfo undef) - let equal = ExistentialMap.equal + let map f (def,undef) = (ExistentialMap.map f def, ExistentialMap.map f undef) - let define evd evk body = + let define (def,undef) evk body = let oldinfo = - try find evd evk - with Not_found -> error "Evd.define: cannot define undeclared evar" in + try ExistentialMap.find evk undef + with Not_found -> + try ExistentialMap.find evk def + with Not_found -> + anomaly "Evd.define: cannot define undeclared evar" in let newinfo = { oldinfo with evar_body = Evar_defined body } in match oldinfo.evar_body with - | Evar_empty -> ExistentialMap.add evk newinfo evd - | _ -> anomaly "Evd.define: cannot define an evar twice" - - let is_evar sigma evk = mem sigma evk + | Evar_empty -> + (ExistentialMap.add evk newinfo def,ExistentialMap.remove evk undef) + | _ -> + anomaly "Evd.define: cannot define an evar twice" - let is_defined sigma evk = - let info = find sigma evk in - not (info.evar_body = Evar_empty) + let is_evar = mem + let is_defined (def,undef) evk = ExistentialMap.mem evk def + let is_undefined (def,undef) evk = ExistentialMap.mem evk undef (*******************************************************************) (* Formerly Instantiate module *) - let is_id_inst inst = - let is_id (id,c) = match kind_of_term c with - | Var id' -> id = id' - | _ -> false - in - List.for_all is_id inst - - (* Vérifier que les instances des let-in sont compatibles ?? *) - let instantiate_sign_including_let sign args = - let rec instrec = function - | ((id,b,_) :: sign, c::args) -> (id,c) :: (instrec (sign,args)) - | ([],[]) -> [] - | ([],_) | (_,[]) -> - anomaly "Signature and its instance do not match" - in - instrec (sign,args) - - let instantiate_evar sign c args = - let inst = instantiate_sign_including_let sign args in - if is_id_inst inst then - c - else - replace_vars inst c - (* Existentials. *) let existential_type sigma (n,args) = @@ -184,160 +207,38 @@ module EvarInfoMap = struct end -(*******************************************************************) -(* Constraints for sort variables *) -(*******************************************************************) - -type sort_var = Univ.universe - -type sort_constraint = - | DefinedSort of sorts (* instantiated sort var *) - | SortVar of sort_var list * sort_var list (* (leq,geq) *) - | EqSort of sort_var - -module UniverseMap = - Map.Make (struct type t = Univ.universe let compare = compare end) - -type sort_constraints = sort_constraint UniverseMap.t - -let rec canonical_find u scstr = - match UniverseMap.find u scstr with - EqSort u' -> canonical_find u' scstr - | c -> (u,c) - -let whd_sort_var scstr t = - match kind_of_term t with - Sort(Type u) -> - (try - match canonical_find u scstr with - _, DefinedSort s -> mkSort s - | _ -> t - with Not_found -> t) - | _ -> t - -let rec set_impredicative u s scstr = - match UniverseMap.find u scstr with - | DefinedSort s' -> - if family_of_sort s = family_of_sort s' then scstr - else failwith "sort constraint inconsistency" - | EqSort u' -> - UniverseMap.add u (DefinedSort s) (set_impredicative u' s scstr) - | SortVar(_,ul) -> - (* also set sorts lower than u as impredicative *) - UniverseMap.add u (DefinedSort s) - (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul) - -let rec set_predicative u s scstr = - match UniverseMap.find u scstr with - | DefinedSort s' -> - if family_of_sort s = family_of_sort s' then scstr - else failwith "sort constraint inconsistency" - | EqSort u' -> - UniverseMap.add u (DefinedSort s) (set_predicative u' s scstr) - | SortVar(ul,_) -> - UniverseMap.add u (DefinedSort s) - (List.fold_left (fun g u' -> set_impredicative u' s g) scstr ul) - -let var_of_sort = function - Type u -> u - | _ -> assert false - -let is_sort_var s scstr = - match s with - Type u -> - (try - match canonical_find u scstr with - _, DefinedSort _ -> false - | _ -> true - with Not_found -> false) - | _ -> false - -let new_sort_var cstr = - let u = Termops.new_univ() in - (u, UniverseMap.add u (SortVar([],[])) cstr) - - -let set_leq_sort (u1,(leq1,geq1)) (u2,(leq2,geq2)) scstr = - let rec search_rec (is_b, betw, not_betw) u1 = - if List.mem u1 betw then (true, betw, not_betw) - else if List.mem u1 not_betw then (is_b, betw, not_betw) - else if u1 = u2 then (true, u1::betw,not_betw) else - match UniverseMap.find u1 scstr with - EqSort u1' -> search_rec (is_b,betw,not_betw) u1' - | SortVar(leq,_) -> - let (is_b',betw',not_betw') = - List.fold_left search_rec (false,betw,not_betw) leq in - if is_b' then (true, u1::betw', not_betw') - else (false, betw', not_betw') - | DefinedSort _ -> (false,betw,u1::not_betw) in - let (is_betw,betw,_) = search_rec (false, [], []) u1 in - if is_betw then - UniverseMap.add u1 (SortVar(leq1@leq2,geq1@geq2)) - (List.fold_left - (fun g u -> UniverseMap.add u (EqSort u1) g) scstr betw) - else - UniverseMap.add u1 (SortVar(u2::leq1,geq1)) - (UniverseMap.add u2 (SortVar(leq2, u1::geq2)) scstr) - -let set_leq s1 s2 scstr = - let u1 = var_of_sort s1 in - let u2 = var_of_sort s2 in - let (cu1,c1) = canonical_find u1 scstr in - let (cu2,c2) = canonical_find u2 scstr in - if cu1=cu2 then scstr - else - match c1,c2 with - (EqSort _, _ | _, EqSort _) -> assert false - | SortVar(leq1,geq1), SortVar(leq2,geq2) -> - set_leq_sort (cu1,(leq1,geq1)) (cu2,(leq2,geq2)) scstr - | _, DefinedSort(Prop _ as s) -> set_impredicative u1 s scstr - | _, DefinedSort(Type _) -> scstr - | DefinedSort(Type _ as s), _ -> set_predicative u2 s scstr - | DefinedSort(Prop _), _ -> scstr - -let set_sort_variable s1 s2 scstr = - let u = var_of_sort s1 in - match s2 with - Prop _ -> set_impredicative u s2 scstr - | Type _ -> set_predicative u s2 scstr - -let pr_sort_cstrs g = - let l = UniverseMap.fold (fun u c l -> (u,c)::l) g [] in - str "SORT CONSTRAINTS:" ++ fnl() ++ - prlist_with_sep fnl (fun (u,c) -> - match c with - EqSort u' -> Univ.pr_uni u ++ str" == " ++ Univ.pr_uni u' - | DefinedSort s -> Univ.pr_uni u ++ str " := " ++ print_sort s - | SortVar(leq,geq) -> - str"[" ++ hov 0 (prlist_with_sep spc Univ.pr_uni geq) ++ - str"] <= "++ Univ.pr_uni u ++ brk(0,0) ++ str"<= [" ++ - hov 0 (prlist_with_sep spc Univ.pr_uni leq) ++ str"]") - l - module EvarMap = struct - type t = EvarInfoMap.t * sort_constraints - let empty = EvarInfoMap.empty, UniverseMap.empty + type t = EvarInfoMap.t * (Univ.UniverseLSet.t * Univ.universes) + let empty = EvarInfoMap.empty, (Univ.UniverseLSet.empty, Univ.initial_universes) + let is_empty (sigma,_) = EvarInfoMap.is_empty sigma + let has_undefined (sigma,_) = EvarInfoMap.has_undefined sigma let add (sigma,sm) k v = (EvarInfoMap.add sigma k v, sm) - let dom (sigma,_) = EvarInfoMap.dom sigma + let add_undefined (sigma,sm) k v = (EvarInfoMap.add_undefined sigma k v, sm) let find (sigma,_) = EvarInfoMap.find sigma + let find_undefined (sigma,_) = EvarInfoMap.find_undefined sigma let remove (sigma,sm) k = (EvarInfoMap.remove sigma k, sm) let mem (sigma,_) = EvarInfoMap.mem sigma let to_list (sigma,_) = EvarInfoMap.to_list sigma - let fold f (sigma,_) = EvarInfoMap.fold f sigma + let undefined_list (sigma,_) = EvarInfoMap.undefined_list sigma + let undefined_evars (sigma,sm) = (EvarInfoMap.undefined_evars sigma, sm) + let defined_evars (sigma,sm) = (EvarInfoMap.defined_evars sigma, sm) + let fold (sigma,_) = EvarInfoMap.fold sigma + let fold_undefined (sigma,_) = EvarInfoMap.fold_undefined sigma let define (sigma,sm) k v = (EvarInfoMap.define sigma k v, sm) let is_evar (sigma,_) = EvarInfoMap.is_evar sigma let is_defined (sigma,_) = EvarInfoMap.is_defined sigma + let is_undefined (sigma,_) = EvarInfoMap.is_undefined sigma let existential_value (sigma,_) = EvarInfoMap.existential_value sigma let existential_type (sigma,_) = EvarInfoMap.existential_type sigma let existential_opt_value (sigma,_) = EvarInfoMap.existential_opt_value sigma let progress_evar_map (sigma1,sm1 as x) (sigma2,sm2 as y) = not (x == y) && - (EvarInfoMap.exists sigma1 - (fun k v -> v.evar_body = Evar_empty && - (EvarInfoMap.find sigma2 k).evar_body <> Evar_empty) - || not (UniverseMap.equal (=) sm1 sm2)) - - let merge e e' = fold (fun n v sigma -> add sigma n v) e' e + (EvarInfoMap.exists_undefined sigma1 + (fun k v -> assert (v.evar_body = Evar_empty); + EvarInfoMap.is_defined sigma2 k)) + let merge e e' = fold e' (fun n v sigma -> add sigma n v) e + let add_constraints (sigma, (us, sm)) cstrs = + (sigma, (us, Univ.merge_constraints cstrs sm)) end (*******************************************************************) @@ -372,8 +273,7 @@ let map_fl f cfl = { cfl with rebus=f cfl.rebus } (e.g. the solution [P] to [?X u v = P u v] can be eta-expanded twice) *) -type instance_constraint = - IsSuperType | IsSubType | ConvUpToEta of int | UserGiven +type instance_constraint = IsSuperType | IsSubType | Conv (* Status of the unification of the type of an instance against the type of the meta it instantiates: @@ -441,7 +341,6 @@ let progress_evar_map d1 d2 = (* spiwack: tentative. It might very well not be the semantics we want for merging evar_map *) let merge d1 d2 = { -(* d1 with evars = EvarMap.merge d1.evars d2.evars*) evars = EvarMap.merge d1.evars d2.evars ; conv_pbs = List.rev_append d1.conv_pbs d2.conv_pbs ; last_mods = ExistentialSet.union d1.last_mods d2.last_mods ; @@ -449,27 +348,34 @@ let merge d1 d2 = { } let add d e i = { d with evars=EvarMap.add d.evars e i } let remove d e = { d with evars=EvarMap.remove d.evars e } -let dom d = EvarMap.dom d.evars let find d e = EvarMap.find d.evars e +let find_undefined d e = EvarMap.find_undefined d.evars e let mem d e = EvarMap.mem d.evars e (* spiwack: this function loses information from the original evar_map it might be an idea not to export it. *) let to_list d = EvarMap.to_list d.evars +let undefined_list d = EvarMap.undefined_list d.evars +let undefined_evars d = { d with evars=EvarMap.undefined_evars d.evars } +let defined_evars d = { d with evars=EvarMap.defined_evars d.evars } (* spiwack: not clear what folding over an evar_map, for now we shall simply fold over the inner evar_map. *) -let fold f d a = EvarMap.fold f d.evars a +let fold f d a = EvarMap.fold d.evars f a +let fold_undefined f d a = EvarMap.fold_undefined d.evars f a let is_evar d e = EvarMap.is_evar d.evars e let is_defined d e = EvarMap.is_defined d.evars e +let is_undefined d e = EvarMap.is_undefined d.evars e let existential_value d e = EvarMap.existential_value d.evars e let existential_type d e = EvarMap.existential_type d.evars e let existential_opt_value d e = EvarMap.existential_opt_value d.evars e +let add_constraints d e = {d with evars= EvarMap.add_constraints d.evars e} + (*** /Lifting... ***) (* evar_map are considered empty disregarding histories *) let is_empty d = - d.evars = EvarMap.empty && + EvarMap.is_empty d.evars && d.conv_pbs = [] && Metamap.is_empty d.metas @@ -484,11 +390,11 @@ let subst_evar_info s evi = evar_body = subst_evb evi.evar_body } let subst_evar_defs_light sub evd = - assert (UniverseMap.is_empty (snd evd.evars)); + assert (Univ.is_initial_universes (snd (snd evd.evars))); assert (evd.conv_pbs = []); { evd with metas = Metamap.map (map_clb (subst_mps sub)) evd.metas; - evars = ExistentialMap.map (subst_evar_info sub) (fst evd.evars), snd evd.evars + evars = EvarInfoMap.map (subst_evar_info sub) (fst evd.evars), (snd evd.evars) } let subst_evar_map = subst_evar_defs_light @@ -507,9 +413,12 @@ let empty = { metas=Metamap.empty } -let evars_reset_evd ?(with_conv_pbs=false) evd d = +let has_undefined evd = + EvarMap.has_undefined evd.evars + +let evars_reset_evd ?(with_conv_pbs=false) evd d = {d with evars = evd.evars; - conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs} + conv_pbs = if with_conv_pbs then evd.conv_pbs else d.conv_pbs } let add_conv_pb pb d = {d with conv_pbs = pb::d.conv_pbs} let evar_source evk d = (EvarMap.find d.evars evk).evar_source @@ -522,7 +431,7 @@ let define evk body evd = | [] -> evd.last_mods | _ -> ExistentialSet.add evk evd.last_mods } -let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = +let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter ?candidates evd = let filter = if filter = None then List.map (fun _ -> true) (named_context_of_val hyps) @@ -532,13 +441,14 @@ let evar_declare hyps evk ty ?(src=(dummy_loc,InternalHole)) ?filter evd = filter) in { evd with - evars = EvarMap.add evd.evars evk + evars = EvarMap.add_undefined evd.evars evk {evar_hyps = hyps; evar_concl = ty; evar_body = Evar_empty; evar_filter = filter; evar_source = src; - evar_extra = None} } + evar_candidates = candidates; + evar_extra = Store.empty } } let is_defined_evar evd (evk,_) = EvarMap.is_defined evd.evars evk @@ -547,14 +457,6 @@ let is_undefined_evar evd c = match kind_of_term c with | Evar ev -> not (is_defined_evar evd ev) | _ -> false -let undefined_evars evd = - let evars = - EvarMap.fold (fun evk evi sigma -> if evi.evar_body = Evar_empty then - EvarMap.add sigma evk evi else sigma) - evd.evars EvarMap.empty - in - { evd with evars = evars } - (* extracts conversion problems that satisfy predicate p *) (* Note: conv_pbs not satisying p are stored back in reverse order *) let extract_conv_pbs evd p = @@ -588,21 +490,84 @@ let evar_list evd c = | _ -> fold_constr evrec acc c in evrec [] c +let collect_evars c = + let rec collrec acc c = + match kind_of_term c with + | Evar (evk,_) -> ExistentialSet.add evk acc + | _ -> fold_constr collrec acc c + in + collrec ExistentialSet.empty c + (**********************************************************) (* Sort variables *) -let new_sort_variable ({ evars = (sigma,sm) } as d)= - let (u,scstr) = new_sort_var sm in - (Type u,{ d with evars = (sigma,scstr) } ) -let is_sort_variable {evars=(_,sm)} s = - is_sort_var s sm -let whd_sort_variable {evars=(_,sm)} t = whd_sort_var sm t -let set_leq_sort_variable ({evars=(sigma,sm)}as d) u1 u2 = - { d with evars = (sigma, set_leq u1 u2 sm) } -let define_sort_variable ({evars=(sigma,sm)}as d) u s = - { d with evars = (sigma, set_sort_variable u s sm) } -let pr_sort_constraints {evars=(_,sm)} = pr_sort_cstrs sm - +let new_univ_variable ({ evars = (sigma,(us,sm)) } as d) = + let u = Termops.new_univ_level () in + let us' = Univ.UniverseLSet.add u us in + ({d with evars = (sigma, (us', sm))}, Univ.make_universe u) + +let new_sort_variable d = + let (d', u) = new_univ_variable d in + (d', Type u) + +let is_sort_variable {evars=(_,(us,_))} s = match s with Type u -> true | _ -> false +let whd_sort_variable {evars=(_,sm)} t = t + +let univ_of_sort = function + | Type u -> u + | Prop Pos -> Univ.type0_univ + | Prop Null -> Univ.type0m_univ + +let is_eq_sort s1 s2 = + if s1 = s2 then None + else + let u1 = univ_of_sort s1 and u2 = univ_of_sort s2 in + if u1 = u2 then None + else Some (u1, u2) + +let is_univ_var_or_set u = + Univ.is_univ_variable u || u = Univ.type0_univ + +let set_leq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = + match is_eq_sort s1 s2 with + | None -> d + | Some (u1, u2) -> + match s1, s2 with + | Prop c, Prop c' -> + if c = Null && c' = Pos then d + else (raise (Univ.UniverseInconsistency (Univ.Le, u1, u2))) + | Type u, Prop c -> + if c = Pos then + add_constraints d (Univ.enforce_geq Univ.type0_univ u Univ.empty_constraint) + else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)) + | _, Type u -> + if is_univ_var_or_set u then + add_constraints d (Univ.enforce_geq u2 u1 Univ.empty_constraint) + else raise (Univ.UniverseInconsistency (Univ.Le, u1, u2)) + +let is_univ_level_var us u = + match Univ.universe_level u with + | Some u -> Univ.UniverseLSet.mem u us + | None -> false + +let set_eq_sort ({evars = (sigma, (us, sm))} as d) s1 s2 = + match is_eq_sort s1 s2 with + | None -> d + | Some (u1, u2) -> + match s1, s2 with + | Prop c, Type u when is_univ_level_var us u -> + add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint) + | Type u, Prop c when is_univ_level_var us u -> + add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint) + | Type u, Type v when (is_univ_level_var us u) || (is_univ_level_var us v) -> + add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint) + | Prop c, Type u when is_univ_var_or_set u && + Univ.check_eq sm u1 u2 -> d + | Type u, Prop c when is_univ_var_or_set u && Univ.check_eq sm u1 u2 -> d + | Type u, Type v when is_univ_var_or_set u && is_univ_var_or_set v -> + add_constraints d (Univ.enforce_eq u1 u2 Univ.empty_constraint) + | _, _ -> raise (Univ.UniverseInconsistency (Univ.Eq, u1, u2)) + (**********************************************************) (* Accessing metas *) @@ -700,7 +665,6 @@ let meta_with_name evd id = strbrk "\" occurs more than once in clause.") -(* spiwack: we should try and replace this List.fold_left by a Metamap.fold. *) let meta_merge evd1 evd2 = {evd2 with metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) @@ -712,7 +676,7 @@ let retract_coercible_metas evd = let mc,ml = Metamap.fold (fun n v (mc,ml) -> match v with - | Clval (na,(b,(UserGiven,CoerceToType as s)),typ) -> + | Clval (na,(b,(Conv,CoerceToType as s)),typ) -> (n,b.rebus,s)::mc, Metamap.add n (Cltyp (na,typ)) ml | v -> mc, Metamap.add n v ml) @@ -725,7 +689,7 @@ let rec list_assoc_in_triple x = function let subst_defined_metas bl c = let rec substrec c = match kind_of_term c with - | Meta i -> substrec (list_assoc_in_triple i bl) + | Meta i -> substrec (list_assoc_snd_in_triple i bl) | _ -> map_constr substrec c in try Some (substrec c) with Not_found -> None @@ -754,9 +718,7 @@ let pr_instance_status (sc,typ) = begin match sc with | IsSubType -> str " [or a subtype of it]" | IsSuperType -> str " [or a supertype of it]" - | ConvUpToEta 0 -> mt () - | UserGiven -> mt () - | ConvUpToEta n -> str" [or an eta-expansion up to " ++ int n ++ str" of it]" + | Conv -> mt () end ++ begin match typ with | CoerceToType -> str " [up to coercion]" @@ -788,49 +750,126 @@ let pr_decl ((id,b,_),ok) = | Some c -> str (if ok then "(" else "{") ++ pr_id id ++ str ":=" ++ print_constr c ++ str (if ok then ")" else "}") +let pr_evar_source = function + | QuestionMark _ -> str "underscore" + | CasesType -> str "pattern-matching return predicate" + | BinderType (Name id) -> str "type of " ++ Nameops.pr_id id + | BinderType Anonymous -> str "type of anonymous binder" + | ImplicitArg (c,(n,ido),b) -> + let id = Option.get ido in + str "parameter " ++ pr_id id ++ spc () ++ str "of" ++ + spc () ++ print_constr (constr_of_global c) + | InternalHole -> str "internal placeholder" + | TomatchTypeParameter (ind,n) -> + nth n ++ str " argument of type " ++ print_constr (mkInd ind) + | GoalEvar -> str "goal evar" + | ImpossibleCase -> str "type of impossible pattern-matching clause" + | MatchingVar _ -> str "matching variable" + let pr_evar_info evi = - let decls = List.combine (evar_context evi) (evar_filter evi) in - let phyps = prlist_with_sep pr_spc pr_decl (List.rev decls) in + let phyps = + try + let decls = List.combine (evar_context evi) (evar_filter evi) in + prlist_with_sep pr_spc pr_decl (List.rev decls) + with Invalid_argument _ -> str "Ill-formed filtered context" in let pty = print_constr evi.evar_concl in let pb = match evi.evar_body with | Evar_empty -> mt () | Evar_defined c -> spc() ++ str"=> " ++ print_constr c in - hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") - -let pr_evar_map_t (evars,cstrs as sigma) = + let src = str "(" ++ pr_evar_source (snd evi.evar_source) ++ str ")" in + hov 2 + (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]" ++ + spc() ++ src) + +let compute_evar_dependency_graph (sigma:evar_map) = + (* Compute the map binding ev to the evars whose body depends on ev *) + fold (fun evk evi acc -> + let deps = + match evar_body evi with + | Evar_empty -> ExistentialSet.empty + | Evar_defined c -> collect_evars c in + ExistentialSet.fold (fun evk' acc -> + let tab = try ExistentialMap.find evk' acc with Not_found -> [] in + ExistentialMap.add evk' ((evk,evi)::tab) acc) deps acc) + sigma ExistentialMap.empty + +let evar_dependency_closure n sigma = + let graph = compute_evar_dependency_graph sigma in + let order a b = fst a < fst b in + let rec aux n l = + if n=0 then l + else + let l' = + list_map_append (fun (evk,_) -> + try ExistentialMap.find evk graph with Not_found -> []) l in + aux (n-1) (list_uniquize (Sort.list order (l@l'))) in + aux n (undefined_list sigma) + +let pr_evar_map_t depth sigma = + let (evars,(uvs,univs)) = sigma.evars in + let pr_evar_list l = + h 0 (prlist_with_sep pr_fnl + (fun (ev,evi) -> + h 0 (str(string_of_existential ev) ++ + str"==" ++ pr_evar_info evi)) l) in let evs = - if evars = EvarInfoMap.empty then mt () + if EvarInfoMap.is_empty evars then mt () else - str"EVARS:"++brk(0,1)++ - h 0 (prlist_with_sep pr_fnl - (fun (ev,evi) -> - h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) - (EvarMap.to_list sigma))++fnl() + match depth with + | None -> + (* Print all evars *) + str"EVARS:"++brk(0,1)++pr_evar_list (to_list sigma)++fnl() + | Some n -> + (* Print all evars *) + str"UNDEFINED EVARS"++ + (if n=0 then mt() else str" (+level "++int n++str" closure):")++ + brk(0,1)++ + pr_evar_list (evar_dependency_closure n sigma)++fnl() + and svs = + if Univ.UniverseLSet.is_empty uvs then mt () + else str"UNIVERSE VARIABLES:"++brk(0,1)++ + h 0 (prlist_with_sep pr_fnl + (fun u -> Univ.pr_uni_level u) (Univ.UniverseLSet.elements uvs))++fnl() and cs = - if cstrs = UniverseMap.empty then mt () - else pr_sort_cstrs cstrs++fnl() - in evs ++ cs + if Univ.is_initial_universes univs then mt () + else str"UNIVERSES:"++brk(0,1)++ + h 0 (Univ.pr_universes univs)++fnl() + in evs ++ svs ++ cs + +let print_env_short env = + let pr_body n = function None -> pr_name n | Some b -> str "(" ++ pr_name n ++ str " := " ++ print_constr b ++ str ")" in + let pr_named_decl (n, b, _) = pr_body (Name n) b in + let pr_rel_decl (n, b, _) = pr_body n b in + let nc = List.rev (named_context env) in + let rc = List.rev (rel_context env) in + str "[" ++ prlist_with_sep pr_spc pr_named_decl nc ++ str "]" ++ spc () ++ + str "[" ++ prlist_with_sep pr_spc pr_rel_decl rc ++ str "]" let pr_constraints pbs = h 0 - (prlist_with_sep pr_fnl (fun (pbty,_,t1,t2) -> - print_constr t1 ++ spc() ++ - str (match pbty with - | Reduction.CONV -> "==" - | Reduction.CUMUL -> "<=") ++ - spc() ++ print_constr t2) pbs) - -let pr_evar_map evd = + (prlist_with_sep pr_fnl + (fun (pbty,env,t1,t2) -> + print_env_short env ++ spc () ++ str "|-" ++ spc () ++ + print_constr t1 ++ spc() ++ + str (match pbty with + | Reduction.CONV -> "==" + | Reduction.CUMUL -> "<=") ++ + spc() ++ print_constr t2) pbs) + +let pr_evar_map_constraints evd = + if evd.conv_pbs = [] then mt() + else pr_constraints evd.conv_pbs++fnl() + +let pr_evar_map allevars evd = let pp_evm = - if evd.evars = EvarMap.empty then mt() else - pr_evar_map_t evd.evars++fnl() in - let cstrs = - if evd.conv_pbs = [] then mt() else + if EvarMap.is_empty evd.evars then mt() else + pr_evar_map_t allevars evd++fnl() in + let cstrs = if evd.conv_pbs = [] then mt() else str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in let pp_met = - if evd.metas = Metamap.empty then mt() else + if Metamap.is_empty evd.metas then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd.metas in v 0 (pp_evm ++ cstrs ++ pp_met) |