diff options
Diffstat (limited to 'contrib/subtac/subtac.ml')
| -rw-r--r-- | contrib/subtac/subtac.ml | 266 |
1 files changed, 159 insertions, 107 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 8bc310d5..a59ad6f5 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 9976 2007-07-12 11:58:30Z msozeau $ *) +(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *) open Global open Pp @@ -49,24 +49,41 @@ open Decl_kinds open Tacinterp open Tacexpr +let solve_tccs_in_type env id isevars evm c typ = + if not (evm = Evd.empty) then + let stmt_id = Nameops.add_suffix id "_stmt" in + let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in + (** Make all obligations transparent so that real dependencies can be sorted out by the user *) + let obls = Array.map (fun (id, t, l, op, d) -> (id, t, l, false, d)) obls in + match Subtac_obligations.add_definition stmt_id 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 id -> + | 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 - errorlabstrm "start_proof" (pr_id id ++ str " already exists"); + user_err_loc (loc,"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 evm, c, typ = + let evm, c, typ, _imps = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None in - let _ = Typeops.infer_type env c in - Command.start_proof id kind c hook + let c = solve_tccs_in_type env id isevars evm c typ in + Command.start_proof id kind c hook -let print_subgoals () = Options.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () +let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () let start_proof_and_print env isevars idopt k t hook = start_proof_com env isevars idopt k t hook; @@ -75,122 +92,157 @@ let start_proof_and_print env isevars idopt k t hook = let _ = Detyping.set_detype_anonymous (fun loc n -> RVar (loc, id_of_string ("Anonymous_REL_" ^ string_of_int n))) let assumption_message id = - Options.if_verbose message ((string_of_id id) ^ " is assumed") + Flags.if_verbose message ((string_of_id id) ^ " is assumed") -let declare_assumption env isevars idl is_coe k bl c = - if not (Pfedit.refining ()) then - let evm, c, typ = - Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None +let declare_assumption 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 [] (Command.generalize_constr_expr c bl) None in - List.iter (Command.declare_one_assumption is_coe k c) idl + let c = solve_tccs_in_type env id isevars evm c typ in + List.iter (Command.declare_one_assumption is_coe k c imps false false nl) idl else errorlabstrm "Command.Assumption" (str "Cannot declare an assumption while in proof editing mode.") -let vernac_assumption env isevars kind l = - List.iter (fun (is_coe,(idl,c)) -> declare_assumption env isevars idl is_coe kind [] c) l +let dump_definition (loc, id) s = + Flags.dump_string (Printf.sprintf "%s %d %s\n" s (fst (unloc loc)) (string_of_id id)) + +let dump_constraint ty ((loc, n), _, _) = + match n with + | Name id -> dump_definition (loc, id) 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 !Flags.dump then + List.iter (fun lid -> + if global then dump_definition lid "ax" + else dump_variable lid) idl; + declare_assumption 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"]; -(* check_required_library ["Coq";"Logic";"JMeq"]; *) - require_library "Coq.subtac.FixSub"; - require_library "Coq.subtac.Utils"; - require_library "Coq.Logic.JMeq"; + check_required_library ["Coq";"Program";"Tactics"]; let env = Global.env () in let isevars = ref (create_evar_defs Evd.empty) in try match command with - VernacDefinition (defkind, (locid, id), expr, hook) -> - (match expr with - ProveBody (bl, c) -> Subtac_pretyping.subtac_proof env isevars id bl c None - | DefineBody (bl, _, c, tycon) -> - Subtac_pretyping.subtac_proof env isevars id bl c tycon) - | VernacFixpoint (l, b) -> - let _ = trace (str "Building fixpoint") in - ignore(Subtac_command.build_recursive l b) - - | VernacStartTheoremProof (thkind, (locid, id), (bl, t), lettop, hook) -> - if not(Pfedit.refining ()) then - if lettop then - errorlabstrm "Subtac_command.StartProof" - (str "Let declarations can only be used in proof editing mode"); + | VernacDefinition (defkind, (_, id as lid), expr, hook) -> + check_fresh lid; + dump_definition lid "def"; + (match expr with + | ProveBody (bl, t) -> if Lib.is_modtype () then errorlabstrm "Subtac_command.StartProof" (str "Proof editing mode not supported in module types"); - start_proof_and_print env isevars (Some id) (Global, Proof thkind) (bl,t) hook - - - | VernacAssumption (stre,l) -> - vernac_assumption env isevars stre 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 -> - debug 2 (Himsg.explain_pattern_matching_error env exn); - raise e - - | Type_errors.TypeError (env, exn) as e -> - debug 2 (Himsg.explain_type_error env exn); - raise e - - | Pretype_errors.PretypeError (env, exn) as e -> - debug 2 (Himsg.explain_pretype_error env exn); - raise e + start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) + (fun _ _ -> ()) + | DefineBody (bl, _, c, tycon) -> + ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon)) + | VernacFixpoint (l, b) -> + List.iter (fun ((lid, _, _, _, _), _) -> + check_fresh lid; + dump_definition lid "fix") l; + let _ = trace (str "Building fixpoint") in + ignore(Subtac_command.build_recursive l b) - | (Stdpp.Exc_located (loc, e')) as e -> - debug 2 (str "Parsing exception: "); - (match e' with - | Type_errors.TypeError (env, exn) -> - debug 2 (Himsg.explain_type_error env exn); - raise e - - | Pretype_errors.PretypeError (env, exn) -> - debug 2 (Himsg.explain_pretype_error env exn); - raise e - - | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); - raise e) - - | e -> - msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); - raise e - - + | VernacStartTheoremProof (thkind, [Some id, (bl, t)], lettop, hook) -> + if !Flags.dump then dump_definition id "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 (glob, sup, is, props, pri) -> + if !Flags.dump then dump_constraint "inst" is; + ignore(Subtac_classes.new_instance ~global:glob sup is props pri) + + | VernacCoFixpoint (l, b) -> + List.iter (fun ((lid, _, _, _), _) -> dump_definition lid "cofix") l; + ignore(Subtac_command.build_corecursive l b) + + (*| 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 -> + debug 2 (Himsg.explain_pattern_matching_error env exn); + raise e + + | Type_errors.TypeError (env, exn) as e -> + debug 2 (Himsg.explain_type_error env exn); + raise e + + | Pretype_errors.PretypeError (env, exn) as e -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e + + | (Stdpp.Exc_located (loc, e')) as e -> + debug 2 (str "Parsing exception: "); + (match e' with + | Type_errors.TypeError (env, exn) -> + debug 2 (Himsg.explain_type_error env exn); + raise e + + | Pretype_errors.PretypeError (env, exn) -> + debug 2 (Himsg.explain_pretype_error env exn); + raise e + + | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); + raise e) + + | e -> + msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); + raise e |