diff options
Diffstat (limited to 'plugins/subtac/subtac.ml')
| -rw-r--r-- | plugins/subtac/subtac.ml | 227 |
1 files changed, 227 insertions, 0 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml new file mode 100644 index 000000000..a8d69bdcf --- /dev/null +++ b/plugins/subtac/subtac.ml @@ -0,0 +1,227 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <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 *) +(************************************************************************) + +open Compat +open Global +open Pp +open Errors +open Util +open Names +open Sign +open Evd +open Term +open Termops +open Namegen +open Reductionops +open Environ +open Type_errors +open Typeops +open Libnames +open Classops +open List +open Recordops +open Evarutil +open Pretype_errors +open Glob_term +open Evarconv +open Pattern +open Vernacexpr + +open Subtac_coercion +open Subtac_utils +open Coqlib +open Printer +open Subtac_errors +open Eterm + +let require_library dirpath = + let qualid = (dummy_loc, qualid_of_dirpath (dirpath_of_string dirpath)) in + Library.require_library [qualid] None + +open Pp +open Ppconstr +open Decl_kinds +open Tacinterp +open Tacexpr + +let solve_tccs_in_type env id isevars evm c typ = + if not (Evd.is_empty evm) then + let stmt_id = Nameops.add_suffix id "_stmt" in + let obls, _, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in + match Subtac_obligations.add_definition stmt_id ~term:c' typ obls with + | Subtac_obligations.Defined cst -> constant_value (Global.env()) + (match cst with ConstRef kn -> kn | _ -> assert false) + | _ -> + errorlabstrm "start_proof" + (str "The statement obligations could not be resolved automatically, " ++ spc () ++ + str "write a statement definition first.") + else + let _ = Typeops.infer_type env c in c + + +let start_proof_com env isevars sopt kind (bl,t) hook = + let id = match sopt with + | Some (loc,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 + user_err_loc (loc,"start_proof",pr_id id ++ str " already exists"); + id + | None -> + next_global_ident_away (id_of_string "Unnamed_thm") + (Pfedit.get_all_proof_names ()) + in + let evm, c, typ, imps = + Subtac_pretyping.subtac_process ~is_type:true env isevars id [] (Topconstr.prod_constr_expr t bl) None + in + let c = solve_tccs_in_type env id isevars evm c typ in + Lemmas.start_proof id kind c (fun loc gr -> + Impargs.declare_manual_implicits (loc = Local) gr ~enriching:true [imps]; + hook loc gr) + +let start_proof_and_print env isevars idopt k t hook = + start_proof_com env isevars idopt k t hook; + Vernacentries.print_subgoals () + +let _ = Detyping.set_detype_anonymous (fun loc n -> GVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) + +let assumption_message id = + Flags.if_verbose message ((string_of_id id) ^ " is assumed") + +let declare_assumptions env isevars idl is_coe k bl c nl = + if not (Pfedit.refining ()) then + let id = snd (List.hd idl) in + let evm, c, typ, imps = + Subtac_pretyping.subtac_process env isevars id [] (Topconstr.prod_constr_expr c bl) None + in + let c = solve_tccs_in_type env id isevars evm c typ in + List.iter (Command.declare_assumption is_coe k c imps false nl) idl + else + errorlabstrm "Command.Assumption" + (str "Cannot declare an assumption while in proof editing mode.") + +let dump_constraint ty ((loc, n), _, _) = + match n with + | Name id -> Dumpglob.dump_definition (loc, id) false ty + | Anonymous -> () + +let dump_variable lid = () + +let vernac_assumption env isevars kind l nl = + let global = fst kind = Global in + List.iter (fun (is_coe,(idl,c)) -> + if Dumpglob.dump () then + List.iter (fun lid -> + if global then Dumpglob.dump_definition lid (not global) "ax" + else dump_variable lid) idl; + declare_assumptions env isevars idl is_coe kind [] c nl) l + +let check_fresh (loc,id) = + if Nametab.exists_cci (Lib.make_path id) or is_section_variable id then + user_err_loc (loc,"",pr_id id ++ str " already exists") + +let subtac (loc, command) = + check_required_library ["Coq";"Init";"Datatypes"]; + check_required_library ["Coq";"Init";"Specif"]; + let env = Global.env () in + let isevars = ref (create_evar_defs Evd.empty) in + try + match command with + | VernacDefinition (defkind, (_, id as lid), expr, hook) -> + check_fresh lid; + Dumpglob.dump_definition lid false "def"; + (match expr with + | ProveBody (bl, t) -> + start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) + (fun _ _ -> ()) + | DefineBody (bl, _, c, tycon) -> + ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) + | VernacFixpoint l -> + List.iter (fun ((lid, _, _, _, _), _) -> + check_fresh lid; + Dumpglob.dump_definition lid false "fix") l; + let _ = trace (str "Building fixpoint") in + ignore(Subtac_command.build_recursive l) + + | VernacStartTheoremProof (thkind, [Some id, (bl,t,guard)], lettop, hook) -> + if guard <> None then + error "Do not support building theorems as a fixpoint."; + Dumpglob.dump_definition id false "prf"; + if not(Pfedit.refining ()) then + if lettop then + errorlabstrm "Subtac_command.StartProof" + (str "Let declarations can only be used in proof editing mode"); + if Lib.is_modtype () then + errorlabstrm "Subtac_command.StartProof" + (str "Proof editing mode not supported in module types"); + check_fresh id; + start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook + + | VernacAssumption (stre,nl,l) -> + vernac_assumption env isevars stre l nl + + | VernacInstance (abst, glob, sup, is, props, pri) -> + dump_constraint "inst" is; + if abst then + error "Declare Instance not supported here."; + ignore(Subtac_classes.new_instance ~global:glob sup is props pri) + + | VernacCoFixpoint l -> + if Dumpglob.dump () then + List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "cofix") l; + ignore(Subtac_command.build_corecursive l) + + (*| VernacEndProof e -> + subtac_end_proof e*) + + | _ -> user_err_loc (loc,"", str ("Invalid Program command")) + with + | Typing_error e -> + msg_warning (str "Type error in Program tactic:"); + let cmds = + (match e with + | NonFunctionalApp (loc, x, mux, e) -> + str "non functional application of term " ++ + e ++ str " to function " ++ x ++ str " of (mu) type " ++ mux + | NonSigma (loc, t) -> + str "Term is not of Sigma type: " ++ t + | NonConvertible (loc, x, y) -> + str "Unconvertible terms:" ++ spc () ++ + x ++ spc () ++ str "and" ++ spc () ++ y + | IllSorted (loc, t) -> + str "Term is ill-sorted:" ++ spc () ++ t + ) + in msg_warning cmds + + | Subtyping_error e -> + msg_warning (str "(Program tactic) Subtyping error:"); + let cmds = + match e with + | UncoercibleInferType (loc, x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + | UncoercibleInferTerm (loc, x, y, tx, ty) -> + str "Uncoercible terms:" ++ spc () + ++ tx ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ x + ++ str "and" ++ spc() ++ ty ++ spc () ++ str "of" ++ spc () ++ str "type" ++ spc () ++ y + | UncoercibleRewrite (x, y) -> + str "Uncoercible terms:" ++ spc () + ++ x ++ spc () ++ str "and" ++ spc () ++ y + in msg_warning cmds + + | Cases.PatternMatchingError (env, exn) as e -> raise e + + | Type_errors.TypeError (env, exn) as e -> raise e + + | Pretype_errors.PretypeError (env, _, exn) as e -> raise e + + | (Loc.Exc_located (loc, Proof_type.LtacLocated (_,e')) | + Loc.Exc_located (loc, e') as e) -> raise e + + | e -> + (* msg_warning (str "Uncaught exception: " ++ Errors.print e); *) + raise e |