diff options
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r-- | toplevel/command.ml | 701 |
1 files changed, 701 insertions, 0 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml new file mode 100644 index 00000000..b9a47781 --- /dev/null +++ b/toplevel/command.ml @@ -0,0 +1,701 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id: command.ml,v 1.116.2.1 2004/07/16 19:31:47 herbelin Exp $ *) + +open Pp +open Util +open Options +open Term +open Termops +open Declarations +open Entries +open Inductive +open Environ +open Reduction +open Tacred +open Declare +open Nametab +open Names +open Libnames +open Nameops +open Topconstr +open Library +open Libobject +open Constrintern +open Proof_type +open Tacmach +open Safe_typing +open Nametab +open Typeops +open Indtypes +open Vernacexpr +open Decl_kinds +open Pretyping +open Symbols + +let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b)) +let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b)) + +let rec abstract_rawconstr c = function + | [] -> c + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl + (abstract_rawconstr c bl) + +let rec prod_rawconstr c = function + | [] -> c + | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_rawconstr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],t,b)) idl + (prod_rawconstr c bl) + +let rec destSubCast c = match kind_of_term c with + | Lambda (x,t,c) -> + let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u) + | LetIn (x,b,t,c) -> + let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u) + | Cast (b,u) -> (b,u) + | _ -> assert false + +let rec adjust_conclusion a cs = function + | CProdN (loc,bl,c) -> CProdN (loc,bl,adjust_conclusion a cs c) + | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,adjust_conclusion a cs c) + | CHole loc -> + let (nar,name,params) = a in + if nar <> 0 then + user_err_loc (loc,"", + str "Cannot infer the non constant arguments of the conclusion of " + ++ pr_id cs); + let args = List.map (fun id -> CRef(Ident(loc,id))) params in + CAppExpl (loc,(None,Ident(loc,name)),List.rev args) + | c -> c + +(* Commands of the interface *) + +(* 1| Constant definitions *) + +let definition_message id = + if_verbose message ((string_of_id id) ^ " is defined") + +let constant_entry_of_com (bl,com,comtypopt,opacity) = + let sigma = Evd.empty in + let env = Global.env() in + match comtypopt with + None -> + let b = abstract_rawconstr com bl in + let j = judgment_of_rawconstr sigma env b in + { const_entry_body = j.uj_val; + const_entry_type = Some (Evarutil.refresh_universes j.uj_type); + const_entry_opaque = opacity } + | Some comtyp -> + (* We use a cast to avoid troubles with evars in comtyp *) + (* that can only be resolved knowing com *) + let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in + let (body,typ) = destSubCast (interp_constr sigma env b) in + { const_entry_body = body; + const_entry_type = Some typ; + const_entry_opaque = opacity } + +let red_constant_entry ce = function + | None -> ce + | Some red -> + let body = ce.const_entry_body in + { ce with const_entry_body = + reduction_of_redexp red (Global.env()) Evd.empty body } + +let declare_global_definition ident ce local = + let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in + if local = Local then + msg_warning (pr_id ident ++ str" is declared as a global definition"); + definition_message ident; + ConstRef kn + +let declare_definition ident (local,_) bl red_option c typopt hook = + let ce = constant_entry_of_com (bl,c,typopt,false) in + if bl<>[] && red_option <> None then + error "Evaluation under a local context not supported"; + let ce' = red_constant_entry ce red_option in + let r = match local with + | Local when Lib.sections_are_opened () -> + let c = + SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in + let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in + definition_message ident; + if Pfedit.refining () then + msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ + str" is not visible from current goals"); + VarRef ident + | (Global|Local) -> + declare_global_definition ident ce' local in + hook local r + +let syntax_definition ident c local onlyparse = + let c = snd (interp_aconstr [] [] c) in + let onlyparse = !Options.v7_only or onlyparse in + Syntax_def.declare_syntactic_definition local ident onlyparse c + +(* 2| Variable/Hypothesis/Parameter/Axiom declarations *) + +let assumption_message id = + if_verbose message ((string_of_id id) ^ " is assumed") + +let declare_one_assumption is_coe (local,kind) c (_,ident) = + let r = match local with + | Local when Lib.sections_are_opened () -> + let r = + declare_variable ident + (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in + assumption_message ident; + if is_verbose () & Pfedit.refining () then + msgerrnl (str"Warning: Variable " ++ pr_id ident ++ + str" is not visible from current goals"); + VarRef ident + | (Global|Local) -> + let (_,kn) = + declare_constant ident (ParameterEntry c, IsAssumption kind) in + assumption_message ident; + if local=Local & Options.is_verbose () then + msg_warning (pr_id ident ++ str" is declared as a parameter" ++ + str" because it is at a global level"); + ConstRef kn in + if is_coe then Class.try_add_new_coercion r local + +let declare_assumption idl is_coe k bl c = + let c = prod_rawconstr c bl in + let c = interp_type Evd.empty (Global.env()) c in + List.iter (declare_one_assumption is_coe k c) idl + +(* 3a| Elimination schemes for mutual inductive definitions *) + +open Indrec + +let non_type_eliminations = + [ (InProp,elimination_suffix InProp); + (InSet,elimination_suffix InSet) ] + +let declare_one_elimination ind = + let (mib,mip) = Global.lookup_inductive ind in + let mindstr = string_of_id mip.mind_typename in + let declare s c t = + let id = id_of_string s in + let kn = Declare.declare_internal_constant id + (DefinitionEntry + { const_entry_body = c; + const_entry_type = t; + const_entry_opaque = false }, + Decl_kinds.IsDefinition) in + definition_message id; + kn + in + let env = Global.env () in + let sigma = Evd.empty in + let elim_scheme = Indrec.build_indrec env sigma ind in + let npars = mip.mind_nparams in + let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in + let kelim = mip.mind_kelim in + (* in case the inductive has a type elimination, generates only one + induction scheme, the other ones share the same code with the + apropriate type *) + if List.mem InType kelim then + let elim = make_elim (new_sort_in_family InType) in + let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in + let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in + List.iter (fun (sort,suff) -> + let (t',c') = + Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort) + npars c t in + let _ = declare (mindstr^suff) c' (Some t') in ()) + non_type_eliminations + else (* Impredicative or logical inductive definition *) + List.iter + (fun (sort,suff) -> + if List.mem sort kelim then + let elim = make_elim (new_sort_in_family sort) in + let _ = declare (mindstr^suff) elim None in ()) + non_type_eliminations + +let declare_eliminations sp = + let mib = Global.lookup_mind sp in + if mib.mind_finite then + for i = 0 to Array.length mib.mind_packets - 1 do + declare_one_elimination (sp,i) + done + +(* 3b| Mutual Inductive definitions *) + +let minductive_message = function + | [] -> error "no inductive definition" + | [x] -> (pr_id x ++ str " is defined") + | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++ + spc () ++ str "are defined") + +let recursive_message v = + match Array.length v with + | 0 -> error "no recursive definition" + | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined") + | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ + spc () ++ str "are recursively defined") + +let corecursive_message v = + match Array.length v with + | 0 -> error "no corecursive definition" + | 1 -> (Printer.pr_global v.(0) ++ str " is corecursively defined") + | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++ + spc () ++ str "are corecursively defined") + +let interp_mutual lparams lnamearconstrs finite = + let allnames = + List.fold_left (fun acc (id,_,_,l) -> id::(List.map fst l)@acc) + [] lnamearconstrs in + if not (list_distinct allnames) then + error "Two inductive objects have the same name"; + let nparams = local_binders_length lparams + and sigma = Evd.empty + and env0 = Global.env() in + let env_params, params = + List.fold_left + (fun (env, params) d -> match d with + | LocalRawAssum ([_,na],(CHole _ as t)) -> + let t = interp_binder sigma env na t in + let d = (na,None,t) in + (push_rel d env, d::params) + | LocalRawAssum (nal,t) -> + let t = interp_type sigma env t in + let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in + let ctx = List.rev ctx in + (push_rel_context ctx env, ctx@params) + | LocalRawDef ((_,na),c) -> + let c = judgment_of_rawconstr sigma env c in + let d = (na, Some c.uj_val, c.uj_type) in + (push_rel d env,d::params)) + (env0,[]) lparams + in + (* Builds the params of the inductive entry *) + let params' = + List.map (fun (na,b,t) -> + let id = match na with + | Name id -> id + | Anonymous -> anomaly "Unnamed inductive variable" in + match b with + | None -> (id, LocalAssum t) + | Some b -> (id, LocalDef b)) params + in + let paramassums = + List.fold_right (fun d l -> match d with + (id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in + let indnames = + List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in + let nparamassums = List.length paramassums in + let (ind_env,ind_impls,arityl) = + List.fold_left + (fun (env, ind_impls, arl) (recname, _, arityc, _) -> + let arity = interp_type sigma env_params arityc in + let fullarity = it_mkProd_or_LetIn arity params in + let env' = Termops.push_rel_assum (Name recname,fullarity) env in + let argsc = compute_arguments_scope fullarity in + let ind_impls' = + if Impargs.is_implicit_args() then + let impl = Impargs.compute_implicits false env_params fullarity in + let paramimpl,_ = list_chop nparamassums impl in + let l = List.fold_right + (fun imp l -> if Impargs.is_status_implicit imp then + Impargs.name_of_implicit imp::l else l) paramimpl [] in + (recname,(l,impl,argsc))::ind_impls + else + (recname,([],[],argsc))::ind_impls in + (env', ind_impls', (arity::arl))) + (env0, [], []) lnamearconstrs + in + (* Names of parameters as arguments of the inductive type (defs removed) *) + let lparargs = + List.flatten + (List.map (function (id,LocalAssum _) -> [id] | _ -> []) params') in + let notations = + List.fold_right (fun (_,ntnopt,_,_) l -> option_cons ntnopt l) + lnamearconstrs [] in + let fs = States.freeze() in + (* Declare the notations for the inductive types pushed in local context*) + try + List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) + Metasyntax.add_notation_interpretation df ind_impls c None) notations; + let ind_env_params = push_rel_context params ind_env in + + let mispecvec = + List.map2 + (fun ar (name,_,_,lname_constr) -> + let constrnames, bodies = List.split lname_constr in + (* Compute the conclusions of constructor types *) + (* for inductive given in ML syntax *) + let nar = + List.length (fst (Reductionops.splay_arity env_params Evd.empty ar)) + in + let bodies = + List.map2 (adjust_conclusion (nar,name,lparargs)) + constrnames bodies + in + + (* Interpret the constructor types *) + let constrs = + List.map + (interp_type_with_implicits sigma ind_env_params + (paramassums,ind_impls)) + bodies + in + + (* Build the inductive entry *) + { mind_entry_params = params'; + mind_entry_typename = name; + mind_entry_arity = ar; + mind_entry_consnames = constrnames; + mind_entry_lc = constrs }) + (List.rev arityl) lnamearconstrs + in + States.unfreeze fs; + notations, { mind_entry_finite = finite; mind_entry_inds = mispecvec } + with e -> States.unfreeze fs; raise e + +let declare_mutual_with_eliminations isrecord mie = + let lrecnames = + List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in + let (_,kn) = declare_mind isrecord mie in + if_verbose ppnl (minductive_message lrecnames); + declare_eliminations kn; + kn + +(* Very syntactical equality *) +let eq_la d1 d2 = match d1,d2 with + | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') -> + List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal' + & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false) + | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') -> + id=id' & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false) + | _ -> false + +let extract_coe lc = + List.fold_right + (fun (addcoe,((_,(id:identifier)),t)) (l1,l2) -> + ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[]) + +let extract_coe_la_lc = function + | [] -> anomaly "Vernacentries: empty list of inductive types" + | ((_,id),ntn,la,ar,lc)::rest -> + let rec check = function + | [] -> [],[] + | ((_,id),ntn,la',ar,lc)::rest -> + if (List.length la = List.length la') && + (List.for_all2 eq_la la la') + then + let mcoes, mspec = check rest in + let coes, lc' = extract_coe lc in + (coes::mcoes,(id,ntn,ar,lc')::mspec) + else + error ("Parameters should be syntactically the same "^ + "for each inductive type") + in + let mcoes, mspec = check rest in + let coes, lc' = extract_coe lc in + (coes,la,(id,ntn,ar,lc'):: mspec) + +let build_mutual lind finite = + let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in + let notations,mie = interp_mutual lparams lnamearconstructs finite in + let kn = declare_mutual_with_eliminations false mie in + (* Declare the notations now bound to the inductive types *) + List.iter (fun (df,c,scope) -> + Metasyntax.add_notation_interpretation df [] c scope) notations; + List.iter + (fun id -> + Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes + +(* try to find non recursive definitions *) + +let list_chop_hd i l = match list_chop i l with + | (l1,x::l2) -> (l1,x,l2) + | _ -> assert false + +let collect_non_rec env = + let rec searchrec lnonrec lnamerec ldefrec larrec nrec = + try + let i = + list_try_find_i + (fun i f -> + if List.for_all (fun def -> not (occur_var env f def)) ldefrec + then i else failwith "try_find_i") + 0 lnamerec + in + let (lf1,f,lf2) = list_chop_hd i lnamerec in + let (ldef1,def,ldef2) = list_chop_hd i ldefrec in + let (lar1,ar,lar2) = list_chop_hd i larrec in + let newlnv = + try + match list_chop i nrec with + | (lnv1,_::lnv2) -> (lnv1@lnv2) + | _ -> [] (* nrec=[] for cofixpoints *) + with Failure "list_chop" -> [] + in + searchrec ((f,def,ar)::lnonrec) + (lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv + with Failure "try_find_i" -> + (List.rev lnonrec, + (Array.of_list lnamerec, Array.of_list ldefrec, + Array.of_list larrec, Array.of_list nrec)) + in + searchrec [] + +let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) = + let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef + and sigma = Evd.empty + and env0 = Global.env() + and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef) in + (* Build the recursive context and notations for the recursive types *) + let (rec_sign,rec_impls,arityl) = + List.fold_left + (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> + let arityc = prod_rawconstr arityc bl in + let arity = interp_type sigma env0 arityc in + let impl = + if Impargs.is_implicit_args() + then Impargs.compute_implicits false env0 arity + else [] in + let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in + (Environ.push_named (recname,None,arity) env, impls', arity::arl)) + (env0,[],[]) lnameargsardef in + let arityl = List.rev arityl in + let notations = + List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) + lnameargsardef [] in + + let recdef = + + (* Declare local notations *) + let fs = States.freeze() in + let def = + try + List.iter (fun (df,c,scope) -> (* No scope for tmp notation *) + Metasyntax.add_notation_interpretation df [] c None) notations; + List.map2 + (fun ((_,_,bl,_,def),_) arity -> + let def = abstract_rawconstr def bl in + interp_casted_constr_with_implicits + sigma rec_sign rec_impls def arity) + lnameargsardef arityl + with e -> + States.unfreeze fs; raise e in + States.unfreeze fs; def + in + + let (lnonrec,(namerec,defrec,arrec,nvrec)) = + collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in + let recvec = + Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in + let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in + let rec declare i fi = + let ce = + { const_entry_body = mkFix ((nvrec,i),recdecls); + const_entry_type = Some arrec.(i); + const_entry_opaque = false } in + let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in + (ConstRef kn) + in + (* declare the recursive definitions *) + let lrefrec = Array.mapi declare namerec in + if_verbose ppnl (recursive_message lrefrec); + (* The others are declared as normal definitions *) + let var_subst id = (id, global_reference id) in + let _ = + List.fold_left + (fun subst (f,def,t) -> + let ce = { const_entry_body = replace_vars subst def; + const_entry_type = Some t; + const_entry_opaque = false } in + let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in + warning ((string_of_id f)^" is non-recursively defined"); + (var_subst f) :: subst) + (List.map var_subst (Array.to_list namerec)) + lnonrec + in + List.iter (fun (df,c,scope) -> + Metasyntax.add_notation_interpretation df [] c scope) notations + +let build_corecursive lnameardef = + let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef + and sigma = Evd.empty + and env0 = Global.env() in + let fs = States.freeze() in + let (rec_sign,arityl) = + try + List.fold_left + (fun (env,arl) (recname,bl,arityc,_) -> + let arityc = prod_rawconstr arityc bl in + let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in + let arity = arj.utj_val in + let _ = declare_variable recname + (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in + (Environ.push_named (recname,None,arity) env, (arity::arl))) + (env0,[]) lnameardef + with e -> + States.unfreeze fs; raise e in + let arityl = List.rev arityl in + let recdef = + try + List.map (fun (_,bl,arityc,def) -> + let arityc = prod_rawconstr arityc bl in + let def = abstract_rawconstr def bl in + let arity = interp_constr sigma rec_sign arityc in + interp_casted_constr sigma rec_sign def arity) + lnameardef + with e -> + States.unfreeze fs; raise e + in + States.unfreeze fs; + let (lnonrec,(namerec,defrec,arrec,_)) = + collect_non_rec env0 lrecnames recdef arityl [] in + let recvec = + Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in + let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in + let rec declare i fi = + let ce = + { const_entry_body = mkCoFix (i, recdecls); + const_entry_type = Some (arrec.(i)); + const_entry_opaque = false } + in + let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in + (ConstRef kn) + in + let lrefrec = Array.mapi declare namerec in + if_verbose ppnl (corecursive_message lrefrec); + let var_subst id = (id, global_reference id) in + let _ = + List.fold_left + (fun subst (f,def,t) -> + let ce = { const_entry_body = replace_vars subst def; + const_entry_type = Some t; + const_entry_opaque = false } in + let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in + warning ((string_of_id f)^" is non-recursively defined"); + (var_subst f) :: subst) + (List.map var_subst (Array.to_list namerec)) + lnonrec + in () + +let build_scheme lnamedepindsort = + let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort + and sigma = Evd.empty + and env0 = Global.env() in + let lrecspec = + List.map + (fun (_,dep,indid,sort) -> + let ind = Nametab.global_inductive indid in + let (mib,mip) = Global.lookup_inductive ind in + (ind,mib,mip,dep,interp_elimination_sort sort)) + lnamedepindsort + in + let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in + let rec declare decl fi lrecref = + let decltype = Retyping.get_type_of env0 Evd.empty decl in + let decltype = Evarutil.refresh_universes decltype in + let ce = { const_entry_body = decl; + const_entry_type = Some decltype; + const_entry_opaque = false } in + let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in + ConstRef kn :: lrecref + in + let lrecref = List.fold_right2 declare listdecl lrecnames [] in + if_verbose ppnl (recursive_message (Array.of_list lrecref)) + +let rec generalize_rawconstr c = function + | [] -> c + | LocalRawDef (id,b)::bl -> mkLetInC(id,b,generalize_rawconstr c bl) + | LocalRawAssum (idl,t)::bl -> + List.fold_right (fun x b -> mkProdC([x],t,b)) idl + (generalize_rawconstr c bl) + +let start_proof id kind c hook = + let sign = Global.named_context () in + let sign = clear_proofs sign in + Pfedit.start_proof id kind sign c hook + +let start_proof_com sopt kind (bl,t) hook = + let id = match sopt with + | Some id -> + (* We check existence here: it's a bit late at Qed time *) + if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then + errorlabstrm "start_proof" (pr_id id ++ str " already exists"); + id + | None -> + next_global_ident_away false (id_of_string "Unnamed_thm") + (Pfedit.get_all_proof_names ()) + in + let env = Global.env () in + let c = interp_type Evd.empty env (generalize_rawconstr t bl) in + let _ = Typeops.infer_type env c in + start_proof id kind c hook + +let save id const kind hook = + let {const_entry_body = pft; + const_entry_type = tpo; + const_entry_opaque = opacity } = const in + let l,r = match kind with + | IsLocal when Lib.sections_are_opened () -> + let c = SectionLocalDef (pft, tpo, opacity) in + let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in + (Local, VarRef id) + | IsLocal -> + let k = IsDefinition in + let _,kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) + | IsGlobal k -> + let k = theorem_kind_of_goal_kind k in + let _,kn = declare_constant id (DefinitionEntry const, k) in + (Global, ConstRef kn) in + hook l r; + Pfedit.delete_current_proof (); + definition_message id + +let save_named opacity = + let id,(const,persistence,hook) = Pfedit.cook_proof () in + let const = { const with const_entry_opaque = opacity } in + save id const persistence hook + +let check_anonymity id save_ident = + if atompart_of_id id <> "Unnamed_thm" then + error "This command can only be used for unnamed theorem" +(* + message("Overriding name "^(string_of_id id)^" and using "^save_ident) +*) + +let save_anonymous opacity save_ident = + let id,(const,persistence,hook) = Pfedit.cook_proof () in + let const = { const with const_entry_opaque = opacity } in + check_anonymity id save_ident; + save save_ident const persistence hook + +let save_anonymous_with_strength kind opacity save_ident = + let id,(const,_,hook) = Pfedit.cook_proof () in + let const = { const with const_entry_opaque = opacity } in + check_anonymity id save_ident; + (* we consider that non opaque behaves as local for discharge *) + save save_ident const (IsGlobal (Proof kind)) hook + +let admit () = + let (id,k,typ,hook) = Pfedit.current_proof_statement () in +(* Contraire aux besoins d'interactivité... + if k <> IsGlobal (Proof Conjecture) then + error "Only statements declared as conjecture can be admitted"; +*) + let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in + hook Global (ConstRef kn); + Pfedit.delete_current_proof (); + assumption_message id + +let get_current_context () = + try Pfedit.get_current_goal_context () + with e when Logic.catchable_exception e -> + (Evd.empty, Global.env()) |