diff options
Diffstat (limited to 'pretyping/evd.ml')
-rw-r--r-- | pretyping/evd.ml | 522 |
1 files changed, 506 insertions, 16 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 7a3e7c02..c9f771c9 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,12 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: evd.ml,v 1.3.2.1 2004/07/16 19:30:44 herbelin Exp $ *) +(* $Id: evd.ml 8688 2006-04-07 15:08:12Z msozeau $ *) +open Pp open Util open Names +open Nameops open Term +open Termops open Sign +open Environ +open Libnames +open Mod_subst (* The type of mappings for existential variables *) @@ -23,12 +29,20 @@ type evar_body = type evar_info = { evar_concl : constr; - evar_hyps : named_context; + evar_hyps : named_context_val; evar_body : evar_body} +let evar_context evi = named_context_of_val evi.evar_hyps + +let eq_evar_info ei1 ei2 = + ei1 == ei2 || + eq_constr ei1.evar_concl ei2.evar_concl && + eq_named_context_val (ei1.evar_hyps) (ei2.evar_hyps) && + ei1.evar_body = ei2.evar_body + module Evarmap = Intmap -type evar_map = evar_info Evarmap.t +type evar_map1 = evar_info Evarmap.t let empty = Evarmap.empty @@ -38,28 +52,21 @@ let map evc k = Evarmap.find k evc let rmv evc k = Evarmap.remove k evc let remap evc k i = Evarmap.add k i evc let in_dom evc k = Evarmap.mem k evc +let fold = Evarmap.fold let add evd ev newinfo = Evarmap.add ev newinfo evd let define evd ev body = - let oldinfo = map evd ev in + let oldinfo = + try map evd ev + with Not_found -> error "Evd.define: cannot define undeclared evar" in let newinfo = { evar_concl = oldinfo.evar_concl; evar_hyps = oldinfo.evar_hyps; - evar_body = Evar_defined body} - in + evar_body = Evar_defined body} in match oldinfo.evar_body with | Evar_empty -> Evarmap.add ev newinfo evd - | _ -> anomaly "cannot define an isevar twice" - -(* The list of non-instantiated existential declarations *) - -let non_instantiated sigma = - let listev = to_list sigma in - List.fold_left - (fun l ((ev,evd) as d) -> - if evd.evar_body = Evar_empty then (d::l) else l) - [] listev + | _ -> anomaly "Evd.define: cannot define an isevar twice" let is_evar sigma ev = in_dom sigma ev @@ -68,7 +75,490 @@ let is_defined sigma ev = not (info.evar_body = Evar_empty) let evar_body ev = ev.evar_body +let evar_env evd = Global.env_of_context evd.evar_hyps let string_of_existential ev = "?" ^ string_of_int ev let existential_of_int ev = ev + +(*******************************************************************) +(* 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) = + let info = + try map sigma n + with Not_found -> + anomaly ("Evar "^(string_of_existential n)^" was not declared") in + let hyps = evar_context info in + instantiate_evar hyps info.evar_concl (Array.to_list args) + +exception NotInstantiatedEvar + +let existential_value sigma (n,args) = + let info = map sigma n in + let hyps = evar_context info in + match evar_body info with + | Evar_defined c -> + instantiate_evar hyps c (Array.to_list args) + | Evar_empty -> + raise NotInstantiatedEvar + +let existential_opt_value sigma ev = + try Some (existential_value sigma ev) + with NotInstantiatedEvar -> None + +(*******************************************************************) +(* 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 UniverseOrdered = struct + type t = Univ.universe + let compare = Pervasives.compare +end +module UniverseMap = Map.Make(UniverseOrdered) + +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 + +type evar_map = evar_map1 * sort_constraints +let empty = empty, UniverseMap.empty +let add (sigma,sm) k v = (add sigma k v, sm) +let dom (sigma,_) = dom sigma +let map (sigma,_) = map sigma +let rmv (sigma,sm) k = (rmv sigma k, sm) +let remap (sigma,sm) k v = (remap sigma k v, sm) +let in_dom (sigma,_) = in_dom sigma +let to_list (sigma,_) = to_list sigma +let fold f (sigma,_) = fold f sigma +let define (sigma,sm) k v = (define sigma k v, sm) +let is_evar (sigma,_) = is_evar sigma +let is_defined (sigma,_) = is_defined sigma +let existential_value (sigma,_) = existential_value sigma +let existential_type (sigma,_) = existential_type sigma +let existential_opt_value (sigma,_) = existential_opt_value sigma + +(*******************************************************************) +type open_constr = evar_map * constr + +(*******************************************************************) +(* The type constructor ['a sigma] adds an evar map to an object of + type ['a] *) +type 'a sigma = { + it : 'a ; + sigma : evar_map} + +let sig_it x = x.it +let sig_sig x = x.sigma + +(*******************************************************************) +(* Metamaps *) + +(*******************************************************************) +(* Constraints for existential variables *) +(*******************************************************************) + +type 'a freelisted = { + rebus : 'a; + freemetas : Intset.t } + +(* Collects all metavars appearing in a constr *) +let metavars_of c = + let rec collrec acc c = + match kind_of_term c with + | Meta mv -> Intset.add mv acc + | _ -> fold_constr collrec acc c + in + collrec Intset.empty c + +let mk_freelisted c = + { rebus = c; freemetas = metavars_of c } + +let map_fl f cfl = { cfl with rebus=f cfl.rebus } + + +(* Clausal environments *) + +type clbinding = + | Cltyp of name * constr freelisted + | Clval of name * constr freelisted * constr freelisted + +let map_clb f = function + | Cltyp (na,cfl) -> Cltyp (na,map_fl f cfl) + | Clval (na,cfl1,cfl2) -> Clval (na,map_fl f cfl1,map_fl f cfl2) + +(* name of defined is erased (but it is pretty-printed) *) +let clb_name = function + Cltyp(na,_) -> (na,false) + | Clval (na,_,_) -> (na,true) + +(***********************) + +module Metaset = Intset + +let meta_exists p s = Metaset.fold (fun x b -> b || (p x)) s false + +module Metamap = Intmap + +let metamap_to_list m = + Metamap.fold (fun n v l -> (n,v)::l) m [] + +(*************************) +(* Unification state *) + +type hole_kind = + | ImplicitArg of global_reference * (int * identifier option) + | BinderType of name + | QuestionMark + | CasesType + | InternalHole + | TomatchTypeParameter of inductive * int + +type conv_pb = Reduction.conv_pb +type evar_constraint = conv_pb * constr * constr +type evar_defs = + { evars : evar_map; + conv_pbs : evar_constraint list; + history : (existential_key * (loc * hole_kind)) list; + metas : clbinding Metamap.t } + +let subst_evar_defs sub evd = + { evd with + conv_pbs = + List.map (fun (k,t1,t2) ->(k,subst_mps sub t1,subst_mps sub t2)) + evd.conv_pbs; + metas = Metamap.map (map_clb (subst_mps sub)) evd.metas } + +let create_evar_defs sigma = + { evars=sigma; conv_pbs=[]; history=[]; metas=Metamap.empty } +let evars_of d = d.evars +let evars_reset_evd evd d = {d with evars = evd} +let reset_evd (sigma,mmap) d = {d with evars = sigma; metas=mmap} +let add_conv_pb pb d = +(* let (pbty,c1,c2) = pb in + pperrnl + (Termops.print_constr c1 ++ + (if pbty=Reduction.CUMUL then str " <="++ spc() + else str" =="++spc()) ++ + Termops.print_constr c2);*) + {d with conv_pbs = pb::d.conv_pbs} +let evar_source ev d = + try List.assoc ev d.history + with Not_found -> (dummy_loc, InternalHole) + +(* define the existential of section path sp as the constr body *) +let evar_define sp body isevars = + {isevars with evars = define isevars.evars sp body} + +let evar_declare hyps evn ty ?(src=(dummy_loc,InternalHole)) evd = + { evd with + evars = add evd.evars evn + {evar_hyps=hyps; evar_concl=ty; evar_body=Evar_empty}; + history = (evn,src)::evd.history } + +let is_defined_evar isevars (n,_) = is_defined isevars.evars n + +(* Does k corresponds to an (un)defined existential ? *) +let is_undefined_evar isevars c = match kind_of_term c with + | Evar ev -> not (is_defined_evar isevars ev) + | _ -> false + +let undefined_evars isevars = + let evd = + fold (fun ev evi sigma -> if evi.evar_body = Evar_empty then + add sigma ev evi else sigma) + isevars.evars empty + in + { isevars with evars = evd } + +(* extracts conversion problems that satisfy predicate p *) +(* Note: conv_pbs not satisying p are stored back in reverse order *) +let get_conv_pbs isevars p = + let (pbs,pbs1) = + List.fold_left + (fun (pbs,pbs1) pb -> + if p pb then + (pb::pbs,pbs1) + else + (pbs,pb::pbs1)) + ([],[]) + isevars.conv_pbs + in + {isevars with conv_pbs = pbs1}, + pbs + + +(**********************************************************) +(* Sort variables *) + +let new_sort_variable (sigma,sm) = + let (u,scstr) = new_sort_var sm in + (Type u,(sigma,scstr)) +let is_sort_variable (_,sm) s = + is_sort_var s sm +let whd_sort_variable (_,sm) t = whd_sort_var sm t +let set_leq_sort_variable (sigma,sm) u1 u2 = + (sigma, set_leq u1 u2 sm) +let define_sort_variable (sigma,sm) u s = + (sigma, set_sort_variable u s sm) +let pr_sort_constraints (_,sm) = pr_sort_cstrs sm + +(**********************************************************) +(* Accessing metas *) + +let meta_list evd = metamap_to_list evd.metas + +let meta_defined evd mv = + match Metamap.find mv evd.metas with + | Clval _ -> true + | Cltyp _ -> false + +let meta_fvalue evd mv = + match Metamap.find mv evd.metas with + | Clval(_,b,_) -> b + | Cltyp _ -> anomaly "meta_fvalue: meta has no value" + +let meta_ftype evd mv = + match Metamap.find mv evd.metas with + | Cltyp (_,b) -> b + | Clval(_,_,b) -> b + +let meta_declare mv v ?(name=Anonymous) evd = + { evd with metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas } + +let meta_assign mv v evd = + match Metamap.find mv evd.metas with + Cltyp(na,ty) -> + { evd with + metas = Metamap.add mv (Clval(na,mk_freelisted v, ty)) evd.metas } + | _ -> anomaly "meta_assign: already defined" + +(* If the meta is defined then forget its name *) +let meta_name evd mv = + try + let (na,def) = clb_name (Metamap.find mv evd.metas) in + if def then Anonymous else na + with Not_found -> Anonymous + +let meta_with_name evd id = + let na = Name id in + let (mvl,mvnodef) = + Metamap.fold + (fun n clb (l1,l2 as l) -> + let (na',def) = clb_name clb in + if na = na' then if def then (n::l1,l2) else (n::l1,n::l2) + else l) + evd.metas ([],[]) in + match mvnodef, mvl with + | _,[] -> + errorlabstrm "Evd.meta_with_name" + (str"No such bound variable " ++ pr_id id) + | ([n],_|_,[n]) -> + n + | _ -> + errorlabstrm "Evd.meta_with_name" + (str "Binder name \"" ++ pr_id id ++ + str"\" occurs more than once in clause") + + +let meta_merge evd1 evd2 = + {evd2 with + metas = List.fold_left (fun m (n,v) -> Metamap.add n v m) + evd2.metas (metamap_to_list evd1.metas) } + + +(**********************************************************) +(* Pretty-printing *) + +let pr_meta_map mmap = + let pr_name = function + Name id -> str"[" ++ pr_id id ++ str"]" + | _ -> mt() in + let pr_meta_binding = function + | (mv,Cltyp (na,b)) -> + hov 0 + (pr_meta mv ++ pr_name na ++ str " : " ++ + print_constr b.rebus ++ fnl ()) + | (mv,Clval(na,b,_)) -> + hov 0 + (pr_meta mv ++ pr_name na ++ str " := " ++ + print_constr b.rebus ++ fnl ()) + in + prlist pr_meta_binding (metamap_to_list mmap) + +let pr_idl idl = prlist_with_sep pr_spc pr_id idl + +let pr_evar_info evi = + let phyps = pr_idl (List.rev (ids_of_named_context (evar_context evi))) 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 sigma = + h 0 + (prlist_with_sep pr_fnl + (fun (ev,evi) -> + h 0 (str(string_of_existential ev)++str"=="++ pr_evar_info evi)) + (to_list sigma)) + +let pr_evar_defs evd = + let pp_evm = + if evd.evars = empty then mt() else + str"EVARS:"++brk(0,1)++pr_evar_map evd.evars++fnl() in + let n = List.length evd.conv_pbs in + let cstrs = + if n=0 then mt() else + str"=> " ++ int n ++ str" constraints" ++ fnl() ++ fnl() in + let pp_met = + if evd.metas = Metamap.empty then mt() else + str"METAS:"++brk(0,1)++pr_meta_map evd.metas in + v 0 (pp_evm ++ cstrs ++ pp_met) |