diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
| -rw-r--r-- | toplevel/vernacentries.ml | 134 |
1 files changed, 83 insertions, 51 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d384541f..35d202d9 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: vernacentries.ml 9017 2006-07-05 17:27:34Z herbelin $ i*) +(*i $Id: vernacentries.ml 9304 2006-10-28 09:58:16Z herbelin $ i*) (* Concrete syntax of the mathematical vernacular MV V2.6 *) @@ -20,6 +20,7 @@ open Term open Pfedit open Tacmach open Proof_trees +open Decl_mode open Constrintern open Prettyp open Printer @@ -93,7 +94,10 @@ let show_script () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts and evc = evc_of_pftreestate pts in - msgnl (print_treescript true evc (Global.named_context()) pf) + msgnl (print_treescript true evc pf) + +let show_thesis () = + msgnl (anomaly "TODO" ) let show_top_evars () = let pfts = get_pftreestate () in @@ -111,39 +115,19 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) () (* Simulate the Intro(s) tactic *) -let fresh_id_of_name avoid gl = function - Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl - | Name id -> Tactics.fresh_id avoid id gl - -let rec do_renum avoid gl = function - [] -> mt () - | [n] -> pr_id (fresh_id_of_name avoid gl n) - | n :: l -> - let id = fresh_id_of_name avoid gl n in - pr_id id ++ spc () ++ do_renum (id :: avoid) gl l - -(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair - ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *) -let decompose_prod_letins = - let rec prodec_rec l c = match kind_of_term c with - | Prod (x,t,c) -> prodec_rec ((x,t)::l) c - | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c - | Cast (c,_,_) -> prodec_rec l c - | _ -> l,c - in - prodec_rec [] - let show_intro all = let pf = get_pftreestate() in let gl = nth_goal_of_pftreestate 1 pf in - let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in - let nl = List.rev_map fst l in - if all then msgnl (hov 0 (do_renum [] gl nl)) - else try - let n = List.hd nl in - msgnl (pr_id (fresh_id_of_name [] gl n)) - with Failure "hd" -> message "" - + let l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in + if all + then + let lid = Tactics.find_intro_names l gl in + msgnl (hov 0 (prlist_with_sep spc pr_id lid)) + else + try + let n = list_last l in + msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl))) + with Failure "list_last" -> message "" let id_of_name = function | Names.Anonymous -> id_of_string "x" @@ -508,15 +492,14 @@ let vernac_end_section = Lib.close_section let vernac_end_segment id = check_no_pending_proofs (); - let o = - try Lib.what_is_opened () - with Not_found -> error "There is nothing to end." in - match o with - | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id - | _,Lib.OpenedModtype _ -> vernac_end_modtype id - | _,Lib.OpenedSection _ -> vernac_end_section id - | _ -> anomaly "No more opened things" - + let o = try Lib.what_is_opened () with + Not_found -> error "There is nothing to end." in + match o with + | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id + | _,Lib.OpenedModtype _ -> vernac_end_modtype id + | _,Lib.OpenedSection _ -> vernac_end_section id + | _ -> anomaly "No more opened things" + let vernac_require import _ qidl = let qidl = List.map qualid_of_reference qidl in Library.require_library qidl import @@ -553,6 +536,7 @@ let vernac_identity_coercion stre id qids qidt = let vernac_solve n tcom b = if not (refining ()) then error "Unknown command of the non proof-editing mode"; + Decl_mode.check_not_proof_mode "Unknown proof instruction"; begin if b then solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ())) @@ -563,7 +547,7 @@ let vernac_solve n tcom b = if subtree_solved () then begin Options.if_verbose msgnl (str "Subgoal proved"); make_focus 0; - reset_top_of_tree () + reset_top_of_script () end; print_subgoals(); if !pcoq <> None then (out_some !pcoq).solve n @@ -580,8 +564,35 @@ let vernac_set_end_tac tac = if not (refining ()) then error "Unknown command of the non proof-editing mode"; if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else () - (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) - + (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) + +(***********************) +(* Proof Language Mode *) + +let vernac_decl_proof () = + check_not_proof_mode "Already in Proof Mode"; + if tree_solved () then + error "Nothing left to prove here." + else + begin + Decl_proof_instr.go_to_proof_mode (); + print_subgoals () + end + +let vernac_return () = + match get_current_mode () with + Mode_tactic -> + Decl_proof_instr.return_from_tactic_mode (); + print_subgoals () + | Mode_proof -> + error "\"return\" is only used after \"escape\"." + | Mode_none -> + error "There is no proof to end." + +let vernac_proof_instr instr = + Decl_proof_instr.proof_instr instr; + print_subgoals () + (*****************************) (* Auxiliary file management *) @@ -789,6 +800,14 @@ let _ = optread=Pp_control.get_margin; optwrite=Pp_control.set_margin } +let _ = + declare_bool_option + { optsync=true; + optkey=SecondaryTable("Printing","Universes"); + optname="the printing of universes"; + optread=(fun () -> !Constrextern.print_universes); + optwrite=(fun b -> Constrextern.print_universes:=b) } + let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) @@ -1009,18 +1028,21 @@ let vernac_backtrack snum pnum naborts = for i = 1 to naborts do vernac_abort None done; undo_todepth pnum; vernac_backto snum; + Pp.flush_all(); (* there may be no proof in progress, even if no abort *) (try print_subgoals () with UserError _ -> ()) - (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *) -let vernac_focus = function - | None -> traverse_nth_goal 1; print_subgoals () - | Some n -> traverse_nth_goal n; print_subgoals () - +let vernac_focus gln = + check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; + match gln with + | None -> traverse_nth_goal 1; print_subgoals () + | Some n -> traverse_nth_goal n; print_subgoals () + (* Reset the focus to the top of the tree *) let vernac_unfocus () = - make_focus 0; reset_top_of_tree (); print_subgoals () + check_not_proof_mode "No focussing or Unfocussing in Proof Mode."; + make_focus 0; reset_top_of_script (); print_subgoals () let vernac_go = function | GoTo n -> Pfedit.traverse n;show_node() @@ -1039,7 +1061,7 @@ let apply_subproof f occ = f evc (Global.named_context()) pf let explain_proof occ = - msg (apply_subproof (print_treescript true) occ) + msg (apply_subproof (fun evd _ -> print_treescript true evd) occ) let explain_tree occ = msg (apply_subproof print_proof occ) @@ -1063,9 +1085,11 @@ let vernac_show = function msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names())) | ShowIntros all -> show_intro all | ShowMatch id -> show_match id + | ShowThesis -> show_thesis () | ExplainProof occ -> explain_proof occ | ExplainTree occ -> explain_tree occ + let vernac_check_guard () = let pts = get_pftreestate () in let pf = proof_of_pftreestate pts in @@ -1130,6 +1154,14 @@ let interp c = match c with | VernacSolve (n,tac,b) -> vernac_solve n tac b | VernacSolveExistential (n,c) -> vernac_solve_existential n c + (* MMode *) + + | VernacDeclProof -> vernac_decl_proof () + | VernacReturn -> vernac_return () + | VernacProofInstr stp -> vernac_proof_instr stp + + (* /MMode *) + (* Auxiliary file and library management *) | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias |