diff options
-rw-r--r-- | contrib/xml/acic.ml | 6 | ||||
-rw-r--r-- | contrib/xml/acic2Xml.ml4 | 7 | ||||
-rw-r--r-- | interp/constrextern.ml | 3 | ||||
-rw-r--r-- | interp/topconstr.ml | 5 | ||||
-rw-r--r-- | interp/topconstr.mli | 2 | ||||
-rw-r--r-- | parsing/ppconstr.ml | 3 | ||||
-rw-r--r-- | parsing/termast.ml | 5 | ||||
-rw-r--r-- | pretyping/evarutil.ml | 6 | ||||
-rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
-rw-r--r-- | pretyping/evd.ml | 28 | ||||
-rw-r--r-- | pretyping/evd.mli | 5 | ||||
-rw-r--r-- | pretyping/indrec.ml | 2 | ||||
-rw-r--r-- | pretyping/instantiate.ml | 2 | ||||
-rw-r--r-- | pretyping/pretype_errors.ml | 4 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 8 | ||||
-rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 6 | ||||
-rw-r--r-- | proofs/proof_trees.mli | 7 | ||||
-rw-r--r-- | proofs/refiner.ml | 2 | ||||
-rw-r--r-- | toplevel/himsg.ml | 4 | ||||
-rw-r--r-- | translate/ppconstrnew.ml | 5 |
21 files changed, 71 insertions, 43 deletions
diff --git a/contrib/xml/acic.ml b/contrib/xml/acic.ml index 693b7cb3c..36541a57d 100644 --- a/contrib/xml/acic.ml +++ b/contrib/xml/acic.ml @@ -23,7 +23,7 @@ type 'constr context_entry = type 'constr hypothesis = identifier * 'constr context_entry type context = constr hypothesis list -type conjecture = int * context * constr +type conjecture = existential_key * context * constr type metasenv = conjecture list (* list of couples section path -- variables defined in that section *) @@ -51,7 +51,7 @@ and constructor = type aconstr = | ARel of id * int * id * identifier | AVar of id * uri - | AEvar of id * int * aconstr list + | AEvar of id * existential_key * aconstr list | ASort of id * sorts | ACast of id * aconstr * aconstr | AProds of (id * name * aconstr) list * aconstr @@ -71,7 +71,7 @@ and acoinductivefun = and explicit_named_substitution = id option * (uri * aconstr) list type acontext = (id * aconstr hypothesis) list -type aconjecture = id * int * acontext * aconstr +type aconjecture = id * existential_key * acontext * aconstr type ametasenv = aconjecture list type aobj = diff --git a/contrib/xml/acic2Xml.ml4 b/contrib/xml/acic2Xml.ml4 index b70ede2d8..4e64ca5d1 100644 --- a/contrib/xml/acic2Xml.ml4 +++ b/contrib/xml/acic2Xml.ml4 @@ -37,6 +37,8 @@ let rec find_last_id = | _::tl -> find_last_id tl ;; +let export_existential = string_of_int + let print_term ids_to_inner_sorts = let rec aux = let module A = Acic in @@ -53,7 +55,8 @@ let print_term ids_to_inner_sorts = X.xml_empty "VAR" ["uri", uri ; "id",id ; "sort",sort] | A.AEvar (id,n,l) -> let sort = Hashtbl.find ids_to_inner_sorts id in - X.xml_nempty "META" ["no",(string_of_int n) ; "id",id ; "sort",sort] + X.xml_nempty "META" + ["no",(export_existential n) ; "id",id ; "sort",sort] (List.fold_left (fun i t -> [< i ; X.xml_nempty "substitution" [] (aux t) >] @@ -231,7 +234,7 @@ let print_object uri ids_to_inner_sorts = (fun i (cid,n,canonical_context,t) -> [< i ; X.xml_nempty "Conjecture" - ["id", cid ; "no",(string_of_int n)] + ["id", cid ; "no",export_existential n] [< List.fold_left (fun i (hid,t) -> [< (match t with diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 58869667b..566752fda 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -103,9 +103,12 @@ let idopt_of_name = function | Anonymous -> None let extern_evar loc n = +(* msgerrnl (str "Warning: existential variable turned into meta-variable during externalization"); CPatVar (loc,(false,make_ident "META" (Some n))) +*) + CEvar (loc,n) let raw_string_of_ref = function | ConstRef kn -> diff --git a/interp/topconstr.ml b/interp/topconstr.ml index d2ef146bf..17a441020 100644 --- a/interp/topconstr.ml +++ b/interp/topconstr.ml @@ -437,6 +437,11 @@ type local_binder = | LocalRawDef of name located * constr_expr | LocalRawAssum of name located list * constr_expr +let rec local_binders_length = function + | [] -> 0 + | LocalRawDef _::bl -> 1 + local_binders_length bl + | LocalRawAssum (idl,_)::bl -> List.length idl + local_binders_length bl + (**********************************************************************) (* Functions on constr_expr *) diff --git a/interp/topconstr.mli b/interp/topconstr.mli index 55cd20290..071af9d37 100644 --- a/interp/topconstr.mli +++ b/interp/topconstr.mli @@ -135,6 +135,8 @@ type local_binder = | LocalRawDef of name located * constr_expr | LocalRawAssum of name located list * constr_expr +val local_binders_length : local_binder list -> int + (* Concrete syntax for modules and modules types *) type with_declaration_ast = diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml index b3118f7e7..742146053 100644 --- a/parsing/ppconstr.ml +++ b/parsing/ppconstr.ml @@ -279,7 +279,10 @@ let rec pr inherited a = | COrderedCase (_,_,_,_,_) -> anomaly "malformed if or destructuring let" | CHole _ -> str "?", latom +(* | CEvar (_,n) -> str "?" ++ int n, latom +*) + | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom | CCast (_,a,b) -> diff --git a/parsing/termast.ml b/parsing/termast.ml index 9cc66a37f..b4914583e 100644 --- a/parsing/termast.ml +++ b/parsing/termast.ml @@ -99,6 +99,11 @@ let ast_of_constant_ref sp = ope("CONST", [path_section dummy_loc sp]) let ast_of_existential_ref ev = +(* + let ev = + try int_of_string (string_of_id ev) + with _ -> warning "cannot find existential variable number"; 0 in +*) ope("EVAR", [num ev]) let ast_of_constructor_ref ((sp,tyi),n) = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 13ed8e8f6..bb1bfb67e 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -52,7 +52,7 @@ let filter_sign p sign x = (* Expanding existential variables (pretyping.ml) *) (* 1- whd_ise fails if an existential is undefined *) -exception Uninstantiated_evar of int +exception Uninstantiated_evar of existential_key let rec whd_ise sigma c = match kind_of_term c with @@ -92,7 +92,7 @@ let evar_env evd = Global.env_of_context evd.evar_hyps (* Generator of existential names *) let new_evar = let evar_ctr = ref 0 in - fun () -> incr evar_ctr; !evar_ctr + fun () -> incr evar_ctr; existential_of_int !evar_ctr let make_evar_instance env = fold_named_context @@ -212,7 +212,7 @@ type evar_constraint = conv_pb * constr * constr type evar_defs = { mutable evars : Evd.evar_map; mutable conv_pbs : evar_constraint list; - mutable history : (int * (loc * Rawterm.hole_kind)) list } + mutable history : (existential_key * (loc * Rawterm.hole_kind)) list } let create_evar_defs evd = { evars=evd; conv_pbs=[]; history=[] } let evars_of d = d.evars diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 9ba82bf1f..4747bf065 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -33,7 +33,7 @@ val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment (* Replacing all evars *) -exception Uninstantiated_evar of int +exception Uninstantiated_evar of existential_key val whd_ise : evar_map -> constr -> constr val whd_castappevar : evar_map -> constr -> constr diff --git a/pretyping/evd.ml b/pretyping/evd.ml index ee99bfb4b..66ec64ea1 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -15,7 +15,7 @@ open Sign (* The type of mappings for existential variables *) -type evar = int +type evar = existential_key type evar_body = | Evar_empty @@ -26,18 +26,20 @@ type evar_info = { evar_hyps : named_context; evar_body : evar_body} -type evar_map = evar_info Intmap.t +module Evarmap = Intmap -let empty = Intmap.empty +type evar_map = evar_info Evarmap.t -let to_list evc = Intmap.fold (fun ev x acc -> (ev,x)::acc) evc [] -let dom evc = Intmap.fold (fun ev _ acc -> ev::acc) evc [] -let map evc k = Intmap.find k evc -let rmv evc k = Intmap.remove k evc -let remap evc k i = Intmap.add k i evc -let in_dom evc k = Intmap.mem k evc +let empty = Evarmap.empty -let add evd ev newinfo = Intmap.add ev newinfo evd +let to_list evc = Evarmap.fold (fun ev x acc -> (ev,x)::acc) evc [] +let dom evc = Evarmap.fold (fun ev _ acc -> ev::acc) evc [] +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 add evd ev newinfo = Evarmap.add ev newinfo evd let define evd ev body = let oldinfo = map evd ev in @@ -47,7 +49,7 @@ let define evd ev body = evar_body = Evar_defined body} in match oldinfo.evar_body with - | Evar_empty -> Intmap.add ev newinfo evd + | Evar_empty -> Evarmap.add ev newinfo evd | _ -> anomaly "cannot define an isevar twice" (* The list of non-instantiated existential declarations *) @@ -67,6 +69,6 @@ let is_defined sigma ev = let evar_body ev = ev.evar_body -let id_of_existential ev = - id_of_string ("?" ^ string_of_int ev) +let string_of_existential ev = "?" ^ string_of_int ev +let existential_of_int ev = ev diff --git a/pretyping/evd.mli b/pretyping/evd.mli index f6a2bb43a..2ad83c16a 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -20,7 +20,7 @@ open Sign it was introduced ([evar_hyps]) and its definition ([evar_body]). [evar_info] is used to add any other kind of information. *) -type evar = int +type evar = existential_key type evar_body = | Evar_empty @@ -53,4 +53,5 @@ val is_defined : evar_map -> evar -> bool val evar_body : evar_info -> evar_body -val id_of_existential : evar -> identifier +val string_of_existential : evar -> string +val existential_of_int : int -> evar diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index ca25938b6..78c23ae61 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -71,7 +71,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind = let ci = make_default_case_info env RegularStyle ind in let depind = build_dependent_inductive env indf in let deparsign = (Anonymous,None,depind)::lnamesar in - let p = (* mkRel nbprod *) + let p = it_mkLambda_or_LetIn_name env' (appvect (mkRel ((if dep then nbargsprod else mip.mind_nrealargs) + nbprod), diff --git a/pretyping/instantiate.ml b/pretyping/instantiate.ml index 95ce7b6bf..358899098 100644 --- a/pretyping/instantiate.ml +++ b/pretyping/instantiate.ml @@ -47,7 +47,7 @@ let existential_type sigma (n,args) = let info = try Evd.map sigma n with Not_found -> - anomaly ("Evar ?"^string_of_int n^" was not declared") in + anomaly ("Evar "^(string_of_existential n)^" was not declared") in let hyps = info.evar_hyps in instantiate_evar hyps info.evar_concl (Array.to_list args) diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index ef96bfb04..8b913faa9 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -23,8 +23,8 @@ type pretype_error = (* Old Case *) | CantFindCaseType of constr (* Unification *) - | OccurCheck of int * constr - | NotClean of int * constr + | OccurCheck of existential_key * constr + | NotClean of existential_key * constr | UnsolvableImplicit of hole_kind (* Pretyping *) | VarNotFound of identifier diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index cb26d3078..6fd4fc05a 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,8 +24,8 @@ type pretype_error = (* Old Case *) | CantFindCaseType of constr (* Unification *) - | OccurCheck of int * constr - | NotClean of int * constr + | OccurCheck of existential_key * constr + | NotClean of existential_key * constr | UnsolvableImplicit of hole_kind (* Pretyping *) | VarNotFound of identifier @@ -74,9 +74,9 @@ val error_ill_typed_rec_body_loc : (*s Implicit arguments synthesis errors *) -val error_occur_check : env -> Evd.evar_map -> int -> constr -> 'b +val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b -val error_not_clean : env -> Evd.evar_map -> int -> constr -> 'b +val error_not_clean : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_unsolvable_implicit : loc -> env -> Evd.evar_map -> hole_kind -> 'b diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 55c7282c2..c578ceeca 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -50,7 +50,7 @@ val w_conv_x : wc -> constr -> constr -> bool val w_const_value : wc -> constant -> constr val w_defined_evar : wc -> existential_key -> bool -val instantiate : evar -> constr -> tactic +val instantiate : int -> constr -> tactic (* val instantiate_tac : tactic_arg list -> tactic *) diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 1ad520ec1..1e0abc02c 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -199,7 +199,7 @@ let pr_evd evd = prlist_with_sep pr_fnl (fun (ev,evd) -> let pe = pr_decl evd in - h 0 (pr_id (id_of_existential ev) ++ str"==" ++ pe)) + h 0 (str (string_of_existential ev) ++ str"==" ++ pe)) (Evd.to_list evd) let pr_decls decls = pr_evd decls @@ -212,7 +212,7 @@ let pr_evars = prlist_with_sep pr_fnl (fun (ev,evd) -> let pegl = pr_evgl_sign evd in - (pr_id (id_of_existential ev) ++ str " : " ++ pegl)) + (str (string_of_existential ev) ++ str " : " ++ pegl)) (* Print an enumerated list of existential variables *) let rec pr_evars_int i = function @@ -221,7 +221,7 @@ let rec pr_evars_int i = function let pegl = pr_evgl_sign evd in let pei = pr_evars_int (i+1) rest in (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++ - pr_id (id_of_existential ev) ++ str " : " ++ pegl)) ++ + str (string_of_existential ev) ++ str " : " ++ pegl)) ++ fnl () ++ pei let pr_subgoals_existential sigma = function diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli index 3181adb9b..70e0d8565 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.mli @@ -37,7 +37,8 @@ val is_tactic_proof : proof_tree -> bool of existential variables and a signature. *) val rc_of_gc : evar_map -> goal -> named_context sigma -val rc_add : named_context sigma -> int * goal -> named_context sigma +val rc_add : named_context sigma -> existential_key * goal -> + named_context sigma val get_hyps : named_context sigma -> named_context val get_env : named_context sigma -> env val get_gc : named_context sigma -> evar_map @@ -62,8 +63,8 @@ val pr_evc : named_context sigma -> std_ppcmds val prgl : goal -> std_ppcmds val pr_seq : goal -> std_ppcmds -val pr_evars : (int * goal) list -> std_ppcmds -val pr_evars_int : int -> (int * goal) list -> std_ppcmds +val pr_evars : (existential_key * goal) list -> std_ppcmds +val pr_evars_int : int -> (existential_key * goal) list -> std_ppcmds val pr_subgoals_existential : evar_map -> goal list -> std_ppcmds (* Gives the ast corresponding to a tactic argument *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 7ab2003e3..644380f3d 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -277,7 +277,7 @@ let extract_open_proof sigma pf = let meta_cnt = ref 0 in let rec f () = incr meta_cnt; - if in_dom sigma !meta_cnt then f () + if in_dom sigma (existential_of_int !meta_cnt) then f () else !meta_cnt in f in diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 9a6e3f326..e62df6e76 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -300,14 +300,14 @@ let explain_cant_find_case_type ctx c = hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe) let explain_occur_check ctx ev rhs = - let id = "?" ^ string_of_int ev in + let id = Evd.string_of_existential ev in let pt = prterm_env ctx rhs in str"Occur check failed: tried to define " ++ str id ++ str" with term" ++ brk(1,1) ++ pt let explain_not_clean ctx ev t = let c = mkRel (Intset.choose (free_rels t)) in - let id = "?" ^ string_of_int ev in + let id = Evd.string_of_existential ev in let var = prterm_env ctx c in str"Tried to define " ++ str id ++ str" with a term using variable " ++ var ++ spc () ++ diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml index a03207f25..5dd8e31c8 100644 --- a/translate/ppconstrnew.ml +++ b/translate/ppconstrnew.ml @@ -43,7 +43,7 @@ let lcast = 100 let lapp = 10 let lproj = 9 let ltop = (200,E) -let lsimple = (0,E) +let lsimple = (9,E) let prec_less child (parent,assoc) = if parent < 0 && child = lprod then true @@ -477,7 +477,10 @@ let rec pr inherited a = str "end"), latom | CHole _ -> str "_", latom +(* | CEvar (_,n) -> str "?" ++ int n, latom +*) + | CEvar (_,n) -> str (Evd.string_of_existential n), latom | CPatVar (_,(_,p)) -> str "?" ++ pr_patvar p, latom | CSort (_,s) -> pr_sort s, latom | CCast (_,a,b) -> |