From: Claudio Sacerdoti Coen Date: Fri, 20 Apr 2007 14:46:36 +0000 (+0000) Subject: Much ado about nothing: X-Git-Tag: make_still_working~6367 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=50afaf262195266d156f594cff7e92a6e8898b3e;p=helm.git Much ado about nothing: 1) repeat tac end ==> repeat tac 2) do n tac end ==> do n tac 3) "goal n" finally dropped (deprecated, semantics no longer clear) 4) the AST (in grafiteAst) has been changed to better reflect the distinction between tactics (including h.o. tactics, i.e. tacticals), punctuational tinycals and non punctuation tinycals (i.e. skip, focus, unfocus) 5) all tacticals are now running properly in every condition; but tacticals argument (i.e. tactics occurring in tacticals) are disambiguated eagerly and not lazily (to be changed) WARNING: the code in proceduralTypes.ml has been commented out since I am not able to figure out how to fix it properly --- diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml index b4d88169a..8dac90f26 100644 --- a/helm/software/components/acic_procedural/proceduralTypes.ml +++ b/helm/software/components/acic_procedural/proceduralTypes.ml @@ -98,6 +98,7 @@ let mk_arel i b = Cic.ARel ("", "", i, b) (* grafite ast constructors *************************************************) +(* let floc = H.dummy_floc let mk_note str = G.Comment (floc, G.Note (floc, str)) @@ -201,6 +202,8 @@ and render_steps sep a = function render_steps sep (render_step (Some mk_dot) a p) ps let render_steps a = render_steps None a +*) +let render_steps sep a = assert false (* counting *****************************************************************) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index e88118303..d7b929de3 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -40,6 +40,20 @@ type 'lazy_term reduction = | `Whd ] type ('term, 'lazy_term, 'reduction, 'ident) tactic = + (* Higher order tactics (i.e. tacticals) *) + | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactic + | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic + | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list + (* sequential composition *) + | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic * + ('term, 'lazy_term, 'reduction, 'ident) tactic list + | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list + (* try a sequence of loc * tactic until one succeeds, fail otherwise *) + | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic + (* try a tactic and mask failures *) + | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic list + | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic + (* Real tactics *) | Absurd of loc * 'term | Apply of loc * 'term | ApplyS of loc * 'term * (string * string) list @@ -65,7 +79,6 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Fourier of loc | FwdSimpl of loc * string * 'ident list | Generalize of loc * ('term, 'lazy_term, 'ident) pattern * 'ident option - | Goal of loc * int (* change current goal, argument is goal number 1-based *) | IdTac of loc | Intros of loc * int option * 'ident list | Inversion of loc * 'term @@ -138,21 +151,7 @@ type ('term,'obj) command = | Print of loc * string | Qed of loc -type ('term, 'lazy_term, 'reduction, 'ident) tactical = - | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic - | Do of loc * int * ('term, 'lazy_term, 'reduction, 'ident) tactical - | Repeat of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical - | Seq of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list - (* sequential composition *) - | Then of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical * - ('term, 'lazy_term, 'reduction, 'ident) tactical list - | First of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list - (* try a sequence of loc * tactical until one succeeds, fail otherwise *) - | Try of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical - (* try a tactical and mask failures *) - | Solve of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical list - | Progress of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical - +type ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical = | Dot of loc | Semicolon of loc | Branch of loc @@ -160,20 +159,20 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactical = | Pos of loc * int list | Wildcard of loc | Merge of loc + +type ('term,'lazy_term,'reduction,'ident) non_punctuation_tactical = | Focus of loc * int list | Unfocus of loc | Skip of loc -let is_punctuation = - function - | Dot _ | Semicolon _ | Branch _ | Shift _ | Merge _ | Pos _ -> true - | _ -> false - type ('term, 'lazy_term, 'reduction, 'obj, 'ident) code = | Command of loc * ('term, 'obj) command | Macro of loc * 'term macro - | Tactical of loc * ('term, 'lazy_term, 'reduction, 'ident) tactical - * ('term, 'lazy_term, 'reduction, 'ident) tactical option(* punctuation *) + | Tactic of loc * ('term, 'lazy_term, 'reduction, 'ident) tactic option + * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical + | NonPunctuationTactical of loc + * ('term, 'lazy_term, 'reduction, 'ident) non_punctuation_tactical + * ('term, 'lazy_term, 'reduction, 'ident) punctuation_tactical type ('term, 'lazy_term, 'reduction, 'obj, 'ident) comment = | Note of loc * string diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index d7ed16efd..710761ed9 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -74,6 +74,21 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = let pp_reduction_kind = pp_reduction_kind ~term_pp in let pp_tactic_pattern = pp_tactic_pattern ~lazy_term_pp ~term_pp in function + (* Higher order tactics *) + | Do (_, count, tac) -> + sprintf "do %d %s" count (pp_tactic ~term_pp ~lazy_term_pp tac) + | Repeat (_, tac) -> "repeat " ^ pp_tactic ~term_pp ~lazy_term_pp tac + | Seq (_, tacs) -> pp_tactics ~term_pp ~lazy_term_pp ~sep:"; " tacs + | Then (_, tac, tacs) -> + sprintf "%s; [%s]" (pp_tactic ~term_pp ~lazy_term_pp tac) + (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) + | First (_, tacs) -> + sprintf "tries [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tacs) + | Try (_, tac) -> "try " ^ pp_tactic ~term_pp ~lazy_term_pp tac + | Solve (_, tac) -> + sprintf "solve [%s]" (pp_tactics ~term_pp ~lazy_term_pp ~sep:" | " tac) + | Progress (_, tac) -> "progress " ^ pp_tactic ~term_pp ~lazy_term_pp tac + (* First order tactics *) | Absurd (_, term) -> "absurd" ^ term_pp term | Apply (_, term) -> "apply " ^ term_pp term | ApplyS (_, term, params) -> @@ -120,7 +135,6 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Generalize (_, pattern, ident) -> sprintf "generalize %s%s" (pp_tactic_pattern pattern) (match ident with None -> "" | Some id -> " as " ^ id) - | Goal (_, n) -> "goal " ^ string_of_int n | Fail _ -> "fail" | Fourier _ -> "fourier" | IdTac _ -> "id" @@ -177,6 +191,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")") args) +and pp_tactics ~term_pp ~lazy_term_pp ~sep tacs = + String.concat sep (List.map (pp_tactic ~lazy_term_pp ~term_pp) tacs) + let pp_search_kind = function | `Locate -> "locate" | `Hint -> "hint" @@ -257,23 +274,8 @@ let pp_command ~term_pp ~obj_pp = function | Print (_,s) -> "print " ^ s | Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value -let rec pp_tactical ~term_pp ~lazy_term_pp = - let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in - let pp_tacticals = pp_tacticals ~lazy_term_pp ~term_pp in +let pp_punctuation_tactical ~term_pp ~lazy_term_pp = function - | Tactic (_, tac) -> pp_tactic tac - | Do (_, count, tac) -> - sprintf "do %d %s" count (pp_tactical ~term_pp ~lazy_term_pp tac) - | Repeat (_, tac) -> "repeat " ^ pp_tactical ~term_pp ~lazy_term_pp tac - | Seq (_, tacs) -> pp_tacticals ~sep:"; " tacs - | Then (_, tac, tacs) -> - sprintf "%s; [%s]" (pp_tactical ~term_pp ~lazy_term_pp tac) - (pp_tacticals ~sep:" | " tacs) - | First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs) - | Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac - | Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac) - | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac - | Dot _ -> "." | Semicolon _ -> ";" | Branch _ -> "[" @@ -281,21 +283,25 @@ let rec pp_tactical ~term_pp ~lazy_term_pp = | Pos (_, i) -> sprintf "%s:" (String.concat "," (List.map string_of_int i)) | Wildcard _ -> "*:" | Merge _ -> "]" + +let pp_non_punctuation_tactical ~term_pp ~lazy_term_pp = + function | Focus (_, goals) -> sprintf "focus %s" (String.concat " " (List.map string_of_int goals)) | Unfocus _ -> "unfocus" | Skip _ -> "skip" -and pp_tacticals ~term_pp ~lazy_term_pp ~sep tacs = - String.concat sep (List.map (pp_tactical~lazy_term_pp ~term_pp) tacs) - let pp_executable ~term_pp ~lazy_term_pp ~obj_pp = function | Macro (_, macro) -> pp_macro ~term_pp macro ^ "." - | Tactical (_, tac, Some punct) -> - pp_tactical ~lazy_term_pp ~term_pp tac - ^ pp_tactical ~lazy_term_pp ~term_pp punct - | Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac + | Tactic (_, Some tac, punct) -> + pp_tactic ~lazy_term_pp ~term_pp tac + ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + | Tactic (_, None, punct) -> + pp_punctuation_tactical ~lazy_term_pp ~term_pp punct + | NonPunctuationTactical (_, tac, punct) -> + pp_non_punctuation_tactical ~lazy_term_pp ~term_pp tac + ^ pp_punctuation_tactical ~lazy_term_pp ~term_pp punct | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ ".\n" let pp_comment ~term_pp ~lazy_term_pp ~obj_pp = diff --git a/helm/software/components/grafite/grafiteAstPp.mli b/helm/software/components/grafite/grafiteAstPp.mli index 7478883aa..35ade2b23 100644 --- a/helm/software/components/grafite/grafiteAstPp.mli +++ b/helm/software/components/grafite/grafiteAstPp.mli @@ -70,10 +70,10 @@ val pp_statement: GrafiteAst.statement -> string -val pp_tactical: +val pp_punctuation_tactical: term_pp:('term -> string) -> lazy_term_pp:('lazy_term -> string) -> ('term, 'lazy_term, 'term GrafiteAst.reduction, string) - GrafiteAst.tactical -> + GrafiteAst.punctuation_tactical -> string diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index f85c13bbb..08b88b95f 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -56,9 +56,29 @@ let namer_of names = end else FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context name ~typ -let tactic_of_ast status ast = +let rec tactic_of_ast status ast = let module PET = ProofEngineTypes in match ast with + (* Higher order tactics *) + | GrafiteAst.Do (loc, n, tactic) -> + Tacticals.do_tactic n (tactic_of_ast status tactic) + | GrafiteAst.Seq (loc, tactics) -> (* tac1; tac2; ... *) + Tacticals.seq (List.map (tactic_of_ast status) tactics) + | GrafiteAst.Repeat (loc, tactic) -> + Tacticals.repeat_tactic (tactic_of_ast status tactic) + | GrafiteAst.Then (loc, tactic, tactics) -> (* tac; [ tac1 | ... ] *) + Tacticals.thens + (tactic_of_ast status tactic) + (List.map (tactic_of_ast status) tactics) + | GrafiteAst.First (loc, tactics) -> + Tacticals.first (List.map (tactic_of_ast status) tactics) + | GrafiteAst.Try (loc, tactic) -> + Tacticals.try_tactic (tactic_of_ast status tactic) + | GrafiteAst.Solve (loc, tactics) -> + Tacticals.solve_tactics (List.map (tactic_of_ast status) tactics) + | GrafiteAst.Progress (loc, tactic) -> + Tacticals.progress_tactic (tactic_of_ast status tactic) + (* First order tactics *) | GrafiteAst.Absurd (_, term) -> Tactics.absurd term | GrafiteAst.Apply (_, term) -> Tactics.apply term | GrafiteAst.ApplyS (_, term, params) -> @@ -121,7 +141,6 @@ let tactic_of_ast status ast = | GrafiteAst.Generalize (_,pattern,ident) -> let names = match ident with None -> [] | Some id -> [id] in Tactics.generalize ~mk_fresh_name_callback:(namer_of names) pattern - | GrafiteAst.Goal (_, n) -> Tactics.set_goal n | GrafiteAst.IdTac _ -> Tactics.id | GrafiteAst.Intros (_, None, names) -> PrimitiveTactics.intros_tac ~mk_fresh_name_callback:(namer_of names) () @@ -192,11 +211,9 @@ let classify_tactic tactic = | GrafiteAst.Generalize _ | GrafiteAst.Elim _ | GrafiteAst.Cut _ - | GrafiteAst.Decompose _ -> true, true - (* tactics we don't want to reorder goals. I think only Goal needs this. *) - | GrafiteAst.Goal _ -> false, true + | GrafiteAst.Decompose _ -> true (* tactics like apply *) - | _ -> true, false + | _ -> false let reorder_metasenv start refine tactic goals current_goal always_opens_a_goal= let module PEH = ProofEngineHelpers in @@ -308,25 +325,21 @@ let apply_tactic ~disambiguate_tactic (text,prefix_len,tactic) (status, goal) = let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, goal in - let needs_reordering, always_opens_a_goal = classify_tactic tactic in + let always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast status tactic in let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in let after = ProofEngineTypes.goals_of_proof proof in let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in let proof, opened_goals = - if needs_reordering then begin - let uri, metasenv_after_tactic, t, ty, attrs = proof in - let reordered_metasenv, opened_goals = - reorder_metasenv - starting_metasenv - metasenv_after_refinement metasenv_after_tactic - opened goal always_opens_a_goal - in - let proof' = uri, reordered_metasenv, t, ty, attrs in - proof', opened_goals - end - else - proof, opened_goals + let uri, metasenv_after_tactic, t, ty, attrs = proof in + let reordered_metasenv, opened_goals = + reorder_metasenv + starting_metasenv + metasenv_after_refinement metasenv_after_tactic + opened goal always_opens_a_goal + in + let proof' = uri, reordered_metasenv, t, ty, attrs in + proof', opened_goals in let incomplete_proof = match status.GrafiteTypes.proof_status with @@ -345,26 +358,22 @@ let apply_atomic_tactical ~disambiguate_tactic ~patch (text,prefix_len,tactic) ( let metasenv_after_refinement = GrafiteTypes.get_proof_metasenv status in let proof = GrafiteTypes.get_current_proof status in let proof_status = proof, goal in - let needs_reordering, always_opens_a_goal = classify_tactic tactic in + let always_opens_a_goal = classify_tactic tactic in let tactic = tactic_of_ast status tactic in let tactic = patch tactic in let (proof, opened) = ProofEngineTypes.apply_tactic tactic proof_status in let after = ProofEngineTypes.goals_of_proof proof in let opened_goals, closed_goals = Tacticals.goals_diff ~before ~after ~opened in let proof, opened_goals = - if needs_reordering then begin - let uri, metasenv_after_tactic, t, ty, attrs = proof in - let reordered_metasenv, opened_goals = - reorder_metasenv - starting_metasenv - metasenv_after_refinement metasenv_after_tactic - opened goal always_opens_a_goal - in - let proof' = uri, reordered_metasenv, t, ty, attrs in - proof', opened_goals - end - else - proof, opened_goals + let uri, metasenv_after_tactic, t, ty, attrs = proof in + let reordered_metasenv, opened_goals = + reorder_metasenv + starting_metasenv + metasenv_after_refinement metasenv_after_tactic + opened goal always_opens_a_goal + in + let proof' = uri, reordered_metasenv, t, ty, attrs in + proof', opened_goals in let incomplete_proof = match status.GrafiteTypes.proof_status with @@ -481,126 +490,50 @@ let eval_coercion status ~add_composites uri arity baseuri = {status with GrafiteTypes.proof_status = GrafiteTypes.No_proof}, List.map fst compounds -let eval_tactical ~disambiguate_tactic status tac = - let apply_tactic = apply_tactic ~disambiguate_tactic in - let module MatitaStatus = - struct - type input_status = GrafiteTypes.status * ProofEngineTypes.goal - - type output_status = - GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list - - type tactic = input_status -> output_status - - let mk_tactic tac = tac - let apply_tactic tac = tac - let goals (_, opened, closed) = opened, closed - let get_stack (status, _) = GrafiteTypes.get_stack status - - let set_stack stack (status, opened, closed) = - GrafiteTypes.set_stack stack status, opened, closed - - let inject (status, _) = (status, [], []) - let focus goal (status, _, _) = (status, goal) - end - in -(* - let rec atomic_tactical_of_ast (text,prefix_len,tac) = - match tac with - | GrafiteAst.Tactic (loc, tactic) -> - cic_tactic_of_ast ~disambiguate_tactic (text,prefix_len,tactic) - (status,~-1) - | GrafiteAst.Seq (loc,tacticals) -> - Tacticals.seq - (List.map atomic_tactical_of_ast - (List.map (fun x -> text,prefix_len,x) tacticals)) - | _ -> assert false - in -*) - let module MatitaTacticals = Continuationals.Make(MatitaStatus) in - let tactical_of_ast l (text,prefix_len,tac) = - let apply_tactic t = apply_tactic (text, prefix_len, t) in - match tac with - | GrafiteAst.Tactic (loc, tactic) -> - MatitaTacticals.eval - (MatitaTacticals.Tactical - (MatitaTacticals.Tactic - (MatitaStatus.mk_tactic (apply_tactic tactic)))) -(* - | GrafiteAst.Seq (loc, tacticals) -> (* tac1; tac2; ... *) - assert (l > 0); - MatitaTacticals.seq ~tactics:(List.map (tactical_of_ast (l+1)) tacticals) - | GrafiteAst.Do (loc, n, tactical) -> - MatitaTacticals.do_tactic ~n ~tactic:(tactical_of_ast (l+1) tactical) -*) - | GrafiteAst.Repeat (loc, GrafiteAst.Tactic (_,tactical)) -> - MatitaTacticals.eval - (MatitaTacticals.Tactical - (MatitaTacticals.Tactic - (MatitaStatus.mk_tactic - (apply_atomic_tactical ~disambiguate_tactic - ~patch:(fun tactic -> Tacticals.repeat_tactic ~tactic) - (text,prefix_len,tactical))))) -(* - | GrafiteAst.Then (loc, tactical, tacticals) -> (* tac; [ tac1 | ... ] *) - assert (l > 0); - MatitaTacticals.thens ~start:(tactical_of_ast (l+1) tactical) - ~continuations:(List.map (tactical_of_ast (l+1)) tacticals) -*) - | GrafiteAst.First (loc, [GrafiteAst.Tactic (_,tacticals)]) -> - MatitaTacticals.eval - (MatitaTacticals.Tactical - (MatitaTacticals.Tactic - (MatitaStatus.mk_tactic - (apply_atomic_tactical ~disambiguate_tactic - ~patch:(fun tactic ->Tacticals.first ~tactics:["",tactic]) - (text,prefix_len,tacticals))))) - | GrafiteAst.Try (loc, GrafiteAst.Tactic (_,tactical)) -> - MatitaTacticals.eval - (MatitaTacticals.Tactical - (MatitaTacticals.Tactic - (MatitaStatus.mk_tactic - (apply_atomic_tactical ~disambiguate_tactic - ~patch:(fun tactic -> Tacticals.try_tactic ~tactic) - (text,prefix_len,tactical))))) - | GrafiteAst.Solve (loc, [GrafiteAst.Tactic (_,tacticals)]) -> - MatitaTacticals.eval - (MatitaTacticals.Tactical - (MatitaTacticals.Tactic - (MatitaStatus.mk_tactic - (apply_atomic_tactical ~disambiguate_tactic - ~patch:(fun tactic ->Tacticals.solve_tactics ~tactics:["",tactic]) - (text,prefix_len,tacticals))))) - | GrafiteAst.Progress (loc, GrafiteAst.Tactic (_,tactical)) -> - MatitaTacticals.eval - (MatitaTacticals.Tactical - (MatitaTacticals.Tactic - (MatitaStatus.mk_tactic - (apply_atomic_tactical ~disambiguate_tactic - ~patch:(fun tactic -> Tacticals.progress_tactic ~tactic) - (text,prefix_len,tactical))))) - | GrafiteAst.Skip _loc -> - MatitaTacticals.eval (MatitaTacticals.Tactical MatitaTacticals.Skip) - | GrafiteAst.Dot _loc -> - MatitaTacticals.eval (MatitaTacticals.Dot) - | GrafiteAst.Semicolon _loc -> - MatitaTacticals.eval (MatitaTacticals.Semicolon) - | GrafiteAst.Branch _loc -> - MatitaTacticals.eval MatitaTacticals.Branch - | GrafiteAst.Shift _loc -> - MatitaTacticals.eval MatitaTacticals.Shift - | GrafiteAst.Pos (_loc, i) -> - MatitaTacticals.eval (MatitaTacticals.Pos i) - | GrafiteAst.Merge _loc -> - MatitaTacticals.eval MatitaTacticals.Merge - | GrafiteAst.Focus (_loc, goals) -> - MatitaTacticals.eval (MatitaTacticals.Focus goals) - | GrafiteAst.Unfocus _loc -> - MatitaTacticals.eval MatitaTacticals.Unfocus - | GrafiteAst.Wildcard _loc -> - MatitaTacticals.eval MatitaTacticals.Wildcard - in - let status, _, _ = tactical_of_ast 0 tac (status, ~-1) in +module MatitaStatus = + struct + type input_status = GrafiteTypes.status * ProofEngineTypes.goal + + type output_status = + GrafiteTypes.status * ProofEngineTypes.goal list * ProofEngineTypes.goal list + + type tactic = input_status -> output_status + + let mk_tactic tac = tac + let apply_tactic tac = tac + let goals (_, opened, closed) = opened, closed + let get_stack (status, _) = GrafiteTypes.get_stack status + + let set_stack stack (status, opened, closed) = + GrafiteTypes.set_stack stack status, opened, closed + + let inject (status, _) = (status, [], []) + let focus goal (status, _, _) = (status, goal) + end + +module MatitaTacticals = Continuationals.Make(MatitaStatus) + +let tactic_of_ast' tac = + MatitaTacticals.Tactical (MatitaTacticals.Tactic (MatitaStatus.mk_tactic tac)) + +let punctuation_tactical_of_ast (text,prefix_len,punct) = + match punct with + | GrafiteAst.Dot _loc -> MatitaTacticals.Dot + | GrafiteAst.Semicolon _loc -> MatitaTacticals.Semicolon + | GrafiteAst.Branch _loc -> MatitaTacticals.Branch + | GrafiteAst.Shift _loc -> MatitaTacticals.Shift + | GrafiteAst.Pos (_loc, i) -> MatitaTacticals.Pos i + | GrafiteAst.Merge _loc -> MatitaTacticals.Merge + | GrafiteAst.Wildcard _loc -> MatitaTacticals.Wildcard + +let non_punctuation_tactical_of_ast (text,prefix_len,punct) = + match punct with + | GrafiteAst.Focus (_loc,goals) -> MatitaTacticals.Focus goals + | GrafiteAst.Unfocus _loc -> MatitaTacticals.Unfocus + | GrafiteAst.Skip _loc -> MatitaTacticals.Tactical MatitaTacticals.Skip + +let eval_tactical status tac = + let status, _, _ = MatitaTacticals.eval tac (status, ~-1) in let status = (* is proof completed? *) match status.GrafiteTypes.proof_status with | GrafiteTypes.Incomplete_proof @@ -879,12 +812,21 @@ let rec eval_command = {ec_go = fun ~disambiguate_command opts status } and eval_executable = {ee_go = fun ~disambiguate_tactic ~disambiguate_command ~disambiguate_macro opts status (text,prefix_len,ex) -> match ex with - | GrafiteAst.Tactical (_, tac, None) -> - eval_tactical ~disambiguate_tactic status (text,prefix_len,tac),[] - | GrafiteAst.Tactical (_, tac, Some punct) -> + | GrafiteAst.Tactic (_, Some tac, punct) -> + let tac = apply_tactic ~disambiguate_tactic (text,prefix_len,tac) in + let status = eval_tactical status (tactic_of_ast' tac) in + eval_tactical status + (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + | GrafiteAst.Tactic (_, None, punct) -> + eval_tactical status + (punctuation_tactical_of_ast (text,prefix_len,punct)),[] + | GrafiteAst.NonPunctuationTactical (_, tac, punct) -> let status = - eval_tactical ~disambiguate_tactic status (text,prefix_len,tac) in - eval_tactical ~disambiguate_tactic status (text,prefix_len,punct),[] + eval_tactical status + (non_punctuation_tactical_of_ast (text,prefix_len,tac)) + in + eval_tactical status + (punctuation_tactical_of_ast (text,prefix_len,punct)),[] | GrafiteAst.Command (_, cmd) -> eval_command.ec_go ~disambiguate_command opts status (text,prefix_len,cmd) | GrafiteAst.Macro (loc, macro) -> diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index 5748f0bbb..912abbcc3 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -105,7 +105,7 @@ let disambiguate_reduction_kind text prefix_len lexicon_status_ref = function | `Whd as kind -> kind ;; -let disambiguate_tactic +let rec disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tactic) = let disambiguate_term = @@ -116,7 +116,61 @@ let disambiguate_tactic disambiguate_reduction_kind text prefix_len lexicon_status_ref in let disambiguate_lazy_term = disambiguate_lazy_term text prefix_len lexicon_status_ref in + let disambiguate_tactic metasenv tac = + disambiguate_tactic lexicon_status_ref context metasenv (text,prefix_len,tac) + in match tactic with + (* Higher order tactics *) + | GrafiteAst.Progress (loc,tac) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,GrafiteAst.Progress (loc,tac) + | GrafiteAst.Solve (loc,tacl) -> + let metasenv,tacl = + List.fold_right + (fun tac (metasenv,tacl) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,tac::tacl + ) tacl (metasenv,[]) + in + metasenv,GrafiteAst.Solve (loc,tacl) + | GrafiteAst.Try (loc,tac) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,GrafiteAst.Try (loc,tac) + | GrafiteAst.First (loc,tacl) -> + let metasenv,tacl = + List.fold_right + (fun tac (metasenv,tacl) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,tac::tacl + ) tacl (metasenv,[]) + in + metasenv,GrafiteAst.First (loc,tacl) + | GrafiteAst.Seq (loc,tacl) -> + let metasenv,tacl = + List.fold_right + (fun tac (metasenv,tacl) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,tac::tacl + ) tacl (metasenv,[]) + in + metasenv,GrafiteAst.Seq (loc,tacl) + | GrafiteAst.Repeat (loc,tac) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,GrafiteAst.Repeat (loc,tac) + | GrafiteAst.Do (loc,n,tac) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,GrafiteAst.Do (loc,n,tac) + | GrafiteAst.Then (loc,tac,tacl) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + let metasenv,tacl = + List.fold_right + (fun tac (metasenv,tacl) -> + let metasenv,tac = disambiguate_tactic metasenv tac in + metasenv,tac::tacl + ) tacl (metasenv,[]) + in + metasenv,GrafiteAst.Then (loc,tac,tacl) + (* First order tactics *) | GrafiteAst.Absurd (loc, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Absurd (loc, cic) @@ -190,8 +244,6 @@ let disambiguate_tactic | GrafiteAst.Generalize (loc,pattern,ident) -> let pattern = disambiguate_pattern pattern in metasenv,GrafiteAst.Generalize (loc,pattern,ident) - | GrafiteAst.Goal (loc, g) -> - metasenv,GrafiteAst.Goal (loc, g) | GrafiteAst.IdTac loc -> metasenv,GrafiteAst.IdTac loc | GrafiteAst.Intros (loc, num, names) -> diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index 3eb64d458..7b515472d 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -194,8 +194,6 @@ EXTEND GrafiteAst.FwdSimpl (loc, hyp, idents) | IDENT "generalize"; p=pattern_spec; id = OPT ["as" ; id = IDENT -> id] -> GrafiteAst.Generalize (loc,p,id) - | IDENT "goal"; n = int -> - GrafiteAst.Goal (loc, n) | IDENT "id" -> GrafiteAst.IdTac loc | IDENT "intro"; ident = OPT IDENT -> let idents = match ident with None -> [] | Some id -> [id] in @@ -335,9 +333,9 @@ EXTEND (GrafiteAst.Then (loc, tac, tacs)) ] | "loops" RIGHTA - [ IDENT "do"; count = int; tac = SELF; IDENT "end" -> + [ IDENT "do"; count = int; tac = SELF -> GrafiteAst.Do (loc, count, tac) - | IDENT "repeat"; tac = SELF; IDENT "end" -> GrafiteAst.Repeat (loc, tac) + | IDENT "repeat"; tac = SELF -> GrafiteAst.Repeat (loc, tac) ] | "simple" NONA [ IDENT "first"; @@ -349,7 +347,7 @@ EXTEND GrafiteAst.Solve (loc, tacs) | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac) | LPAREN; tac = SELF; RPAREN -> tac - | tac = tactic -> GrafiteAst.Tactic (loc, tac) + | tac = tactic -> tac ] ]; punctuation_tactical: @@ -363,12 +361,11 @@ EXTEND | SYMBOL "." -> GrafiteAst.Dot loc ] ]; - tactical: + non_punctuation_tactical: [ "simple" NONA [ IDENT "focus"; goals = LIST1 int -> GrafiteAst.Focus (loc, goals) | IDENT "unfocus" -> GrafiteAst.Unfocus loc | IDENT "skip" -> GrafiteAst.Skip loc - | tac = atomic_tactical LEVEL "loops" -> tac ] ]; theorem_flavour: [ @@ -642,9 +639,11 @@ EXTEND ]]; executable: [ [ cmd = grafite_command; SYMBOL "." -> GrafiteAst.Command (loc, cmd) - | tac = tactical; punct = punctuation_tactical -> - GrafiteAst.Tactical (loc, tac, Some punct) - | punct = punctuation_tactical -> GrafiteAst.Tactical (loc, punct, None) + | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical -> + GrafiteAst.Tactic (loc, Some tac, punct) + | punct = punctuation_tactical -> GrafiteAst.Tactic (loc, None, punct) + | tac = non_punctuation_tactical; punct = punctuation_tactical -> + GrafiteAst.NonPunctuationTactical (loc, tac, punct) | mac = macro; SYMBOL "." -> GrafiteAst.Macro (loc, mac) ] ]; diff --git a/helm/software/components/tactics/fourierR.ml b/helm/software/components/tactics/fourierR.ml index 4d4f305ae..d9f0ce9a4 100644 --- a/helm/software/components/tactics/fourierR.ml +++ b/helm/software/components/tactics/fourierR.ml @@ -1161,7 +1161,7 @@ let rec fourier (s_proof,s_goal)= ~continuations: [PrimitiveTactics.apply_tac ~term:_Rinv_R1; Tacticals.first - ~tactics:[ "ring",Ring.ring_tac; "id", Tacticals.id_tac] + ~tactics:[Ring.ring_tac; Tacticals.id_tac] ]) ;(*Tacticals.id_tac*) Tacticals.then_ diff --git a/helm/software/components/tactics/proofEngineStructuralRules.ml b/helm/software/components/tactics/proofEngineStructuralRules.ml index 3db6d4ff3..636ea07c0 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.ml +++ b/helm/software/components/tactics/proofEngineStructuralRules.ml @@ -194,12 +194,3 @@ let rename ~froms ~tos = (curi, metasenv, pbo, pty, attrs), [goal] in PET.mk_tactic rename - -let set_goal n = - PET.mk_tactic - (fun (proof, goal) -> - let (_, metasenv, _, _, _) = proof in - if CicUtil.exists_meta n metasenv then - (proof, [n]) - else - raise (PET.Fail (lazy ("no such meta: " ^ string_of_int n)))) diff --git a/helm/software/components/tactics/proofEngineStructuralRules.mli b/helm/software/components/tactics/proofEngineStructuralRules.mli index f87a48325..d8e9ed376 100644 --- a/helm/software/components/tactics/proofEngineStructuralRules.mli +++ b/helm/software/components/tactics/proofEngineStructuralRules.mli @@ -29,6 +29,3 @@ val clear: hyps:string list -> ProofEngineTypes.tactic (* Warning: this tactic has no effect on the proof term. It just changes the name of an hypothesis in the current sequent *) val rename: froms:string list -> tos:string list -> ProofEngineTypes.tactic - - (* change the current goal to those referred by the given meta number *) -val set_goal: int -> ProofEngineTypes.tactic diff --git a/helm/software/components/tactics/ring.ml b/helm/software/components/tactics/ring.ml index 0bc26514d..b2d303270 100644 --- a/helm/software/components/tactics/ring.ml +++ b/helm/software/components/tactics/ring.ml @@ -486,10 +486,10 @@ let ring_tac status = ProofEngineTypes.apply_tactic (Tacticals.first ~tactics:[ - "reflexivity", EqualityTactics.reflexivity_tac ; - "exact t1'_eq_t1''", exact_tac ~term:t1'_eq_t1'' ; - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2'' ; - "exact sym_eqt su t1 ...", exact_tac + EqualityTactics.reflexivity_tac ; + exact_tac ~term:t1'_eq_t1'' ; + exact_tac ~term:t2'_eq_t2'' ; + exact_tac ~term:( Cic.Appl [mkConst HelmLibraryObjects.Logic.sym_eq_URI @@ -499,7 +499,7 @@ let ring_tac status = ] ; t1'_eq_t1'' ]) ; - "elim_type eqt su t1 ...", ProofEngineTypes.mk_tactic (fun status -> + ProofEngineTypes.mk_tactic (fun status -> let status' = (* status after 1st elim_type use *) let context = context_of_status status in let b,_ = (*TASSI : FIXME*) @@ -529,9 +529,8 @@ let ring_tac status = ProofEngineTypes.apply_tactic (Tacticals.first (* try to solve 1st subgoal *) ~tactics:[ - "exact t2'_eq_t2''", exact_tac ~term:t2'_eq_t2''; - "exact sym_eqt su t2 ...", - exact_tac + exact_tac ~term:t2'_eq_t2''; + exact_tac ~term:( Cic.Appl [mkConst HelmLibraryObjects.Logic.sym_eq_URI @@ -541,7 +540,6 @@ let ring_tac status = ] ; t2'_eq_t2'' ]) ; - "elim_type eqt su t2 ...", ProofEngineTypes.mk_tactic (fun status -> let status' = let context = context_of_status status in diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml index 63b8e12b5..3e9c1db2c 100644 --- a/helm/software/components/tactics/tacticals.ml +++ b/helm/software/components/tactics/tacticals.ml @@ -183,15 +183,14 @@ let seq ~tactics = (* Tacticals that cannot be implemented on top of tynycals *) let first ~tactics = - let rec first ~(tactics: (string * tactic) list) status = + let rec first ~(tactics: tactic list) status = info (lazy "in Tacticals.first"); match tactics with [] -> raise (PET.Fail (lazy "first: no tactics left")) - | (descr, tac)::tactics -> - info (lazy ("Tacticals.first IS TRYING " ^ descr)); + | tac::tactics -> try let res = PET.apply_tactic tac status in - info (lazy ("Tacticals.first: " ^ descr ^ " succedeed!!!")); + info (lazy ("Tacticals.first: succedeed!!!")); res with PET.Fail _ -> first ~tactics status @@ -230,18 +229,16 @@ let rec repeat_tactic ~tactic = (* This tries tactics until one of them solves the goal *) let solve_tactics ~tactics = - let rec solve_tactics ~(tactics: (string * tactic) list) status = + let rec solve_tactics ~(tactics: tactic list) status = info (lazy "in Tacticals.solve_tactics"); match tactics with - | (descr, currenttactic)::moretactics -> - info (lazy ("Tacticals.solve_tactics is trying " ^ descr)); + | currenttactic::moretactics -> (try let (proof, opened) as output_status = PET.apply_tactic currenttactic status in match opened with - | [] -> info (lazy ("Tacticals.solve_tactics: " ^ descr ^ - " solved the goal!!!")); + | [] -> info (lazy ("Tacticals.solve_tactics: solved the goal!!!")); output_status | _ -> info (lazy ("Tacticals.solve_tactics: try the next tactic")); raise (PET.Fail (lazy "Goal not solved")) diff --git a/helm/software/components/tactics/tacticals.mli b/helm/software/components/tactics/tacticals.mli index a1b8ec7cd..cdc3bac77 100644 --- a/helm/software/components/tactics/tacticals.mli +++ b/helm/software/components/tactics/tacticals.mli @@ -28,14 +28,14 @@ type tactic = ProofEngineTypes.tactic val id_tac : tactic val fail_tac: tactic -val first: tactics: (string * tactic) list -> tactic +val first: tactics: tactic list -> tactic val thens: start: tactic -> continuations: tactic list -> tactic val then_: start: tactic -> continuation: tactic -> tactic val seq: tactics: tactic list -> tactic (** "folding" of then_ *) val repeat_tactic: tactic: tactic -> tactic val do_tactic: n: int -> tactic: tactic -> tactic val try_tactic: tactic: tactic -> tactic -val solve_tactics: tactics: (string * tactic) list -> tactic +val solve_tactics: tactics: tactic list -> tactic val progress_tactic: tactic: tactic -> tactic (* TODO temporary *) diff --git a/helm/software/components/tactics/tactics.ml b/helm/software/components/tactics/tactics.ml index 358de1303..fc1d4b7a3 100644 --- a/helm/software/components/tactics/tactics.ml +++ b/helm/software/components/tactics/tactics.ml @@ -64,7 +64,6 @@ let rewrite = EqualityTactics.rewrite_tac let rewrite_simpl = EqualityTactics.rewrite_simpl_tac let right = IntroductionTactics.right_tac let ring = Ring.ring_tac -let set_goal = ProofEngineStructuralRules.set_goal let simpl = ReductionTactics.simpl_tac let split = IntroductionTactics.split_tac let subst = SubstTactic.subst_tac diff --git a/helm/software/components/tactics/tactics.mli b/helm/software/components/tactics/tactics.mli index f95c736bb..6000a98ad 100644 --- a/helm/software/components/tactics/tactics.mli +++ b/helm/software/components/tactics/tactics.mli @@ -1,4 +1,4 @@ -(* GENERATED FILE, DO NOT EDIT. STAMP:Mon Apr 16 17:26:20 CEST 2007 *) +(* GENERATED FILE, DO NOT EDIT. STAMP:Fri Apr 20 15:46:14 CEST 2007 *) val absurd : term:Cic.term -> ProofEngineTypes.tactic val apply : term:Cic.term -> ProofEngineTypes.tactic val applyS : @@ -47,7 +47,7 @@ val elim_type : ?depth:int -> ?using:Cic.term -> Cic.term -> ProofEngineTypes.tactic val exact : term:Cic.term -> ProofEngineTypes.tactic val exists : ProofEngineTypes.tactic -val fail : ProofEngineTypes.tactic +val fail : Tacticals.tactic val fold : reduction:ProofEngineTypes.lazy_reduction -> term:Cic.lazy_term -> @@ -59,7 +59,7 @@ val fwd_simpl : val generalize : ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic -val id : ProofEngineTypes.tactic +val id : Tacticals.tactic val intros : ?howmany:int -> ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type -> @@ -91,7 +91,6 @@ val rewrite_simpl : Cic.term -> string list -> ProofEngineTypes.tactic val right : ProofEngineTypes.tactic val ring : ProofEngineTypes.tactic -val set_goal : int -> ProofEngineTypes.tactic val simpl : pattern:ProofEngineTypes.lazy_pattern -> ProofEngineTypes.tactic val split : ProofEngineTypes.tactic val subst : ProofEngineTypes.tactic diff --git a/helm/software/components/tptp_grafite/tptp2grafite.ml b/helm/software/components/tptp_grafite/tptp2grafite.ml index 5abe88526..3ed457d95 100644 --- a/helm/software/components/tptp_grafite/tptp2grafite.ml +++ b/helm/software/components/tptp_grafite/tptp2grafite.ml @@ -246,35 +246,35 @@ let convert_ast statements context = function let o = PT.Theorem (`Theorem,name,f,None) in statements @ [ GA.Executable(floc,GA.Command(floc,GA.Obj(floc,o))); - GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, - GA.Intros (floc,None,[])),Some (GA.Dot(floc))))] @ + GA.Executable(floc,GA.Tactic(floc, Some + (GA.Intros (floc,None,[])),GA.Dot(floc)))] @ (if fv <> [] then (List.flatten (List.map (fun _ -> - [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, - GA.Exists floc),Some (GA.Branch floc))); - GA.Executable(floc,GA.Tactical(floc, - GA.Pos (floc,[2]),None))]) + [GA.Executable(floc,GA.Tactic(floc, Some + (GA.Exists floc),GA.Branch floc)); + GA.Executable(floc,GA.Tactic(floc, None, + (GA.Pos (floc,[2]))))]) fv)) else [])@ - [GA.Executable(floc,GA.Tactical(floc, GA.Tactic(floc, + [GA.Executable(floc,GA.Tactic(floc, Some ( if ueq_case then GA.Auto (floc,["paramodulation",""; "timeout",string_of_int !paramod_timeout]) else GA.Auto (floc,["depth",string_of_int !depth]) ), - Some (GA.Dot(floc)))); - GA.Executable(floc,GA.Tactical(floc, GA.Try(floc, - GA.Tactic (floc, GA.Assumption floc)), Some (GA.Dot(floc)))) + GA.Dot(floc))); + GA.Executable(floc,GA.Tactic(floc, Some (GA.Try(floc, + GA.Assumption floc)), GA.Dot(floc))) ]@ (if fv <> [] then (List.flatten (List.map (fun _ -> - [GA.Executable(floc,GA.Tactical(floc, GA.Shift floc, None)); - GA.Executable(floc,GA.Tactical(floc, GA.Skip floc,Some + [GA.Executable(floc,GA.Tactic(floc, None, GA.Shift floc)); + GA.Executable(floc,GA.NonPunctuationTactical(floc, GA.Skip floc, (GA.Merge floc)))]) fv)) else [])@ diff --git a/helm/software/matita/help/C/sec_tacticals.xml b/helm/software/matita/help/C/sec_tacticals.xml index bab2ecf64..2f84ae736 100644 --- a/helm/software/matita/help/C/sec_tacticals.xml +++ b/helm/software/matita/help/C/sec_tacticals.xml @@ -251,7 +251,7 @@ | do &nat; - &LCFtactical; end + &LCFtactical; &TODO; @@ -259,7 +259,7 @@ | repeat - &LCFtactical; end + &LCFtactical; &TODO; diff --git a/helm/software/matita/library/nat/div_and_mod.ma b/helm/software/matita/library/nat/div_and_mod.ma index 65ba0e9e5..537d3bcf0 100644 --- a/helm/software/matita/library/nat/div_and_mod.ma +++ b/helm/software/matita/library/nat/div_and_mod.ma @@ -215,11 +215,12 @@ qed. (* some properties of div and mod *) theorem div_times: \forall n,m:nat. ((S n)*m) / (S n) = m. intros. -apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O). -goal 15. (* ?11 is closed with the following tactics *) -apply div_mod_spec_div_mod. -unfold lt.apply le_S_S.apply le_O_n. -apply div_mod_spec_times. +apply (div_mod_spec_to_eq ((S n)*m) (S n) ? ? ? O); +[2: apply div_mod_spec_div_mod. + unfold lt.apply le_S_S.apply le_O_n. +| skip +| apply div_mod_spec_times +] qed. theorem div_n_n: \forall n:nat. O < n \to n / n = S O. diff --git a/helm/software/matita/library/nat/factorization.ma b/helm/software/matita/library/nat/factorization.ma index 37a704592..826a2670a 100644 --- a/helm/software/matita/library/nat/factorization.ma +++ b/helm/software/matita/library/nat/factorization.ma @@ -399,7 +399,6 @@ apply (not_eq_O_S (S m1)). rewrite > Hcut.rewrite < H1.rewrite < times_n_O.reflexivity. apply le_to_or_lt_eq.apply le_O_n. (* prova del cut *) -goal 20. apply (p_ord_aux_to_exp (S(S m1))). apply lt_O_nth_prime_n. assumption. diff --git a/helm/software/matita/library/nat/minus.ma b/helm/software/matita/library/nat/minus.ma index 71c2cc205..063ab636e 100644 --- a/helm/software/matita/library/nat/minus.ma +++ b/helm/software/matita/library/nat/minus.ma @@ -140,8 +140,8 @@ intros 2. apply (nat_elim2 (\lambda n,m.n \leq m \to n-m = O)). intros.simplify.reflexivity. intros.apply False_ind. -apply not_le_Sn_O. -goal 13.apply H. +apply not_le_Sn_O; +[2: apply H | skip]. intros. simplify.apply H.apply le_S_S_to_le. apply H1. qed. diff --git a/helm/software/matita/library/nat/orders.ma b/helm/software/matita/library/nat/orders.ma index 8be62ae0b..3257e2e1a 100644 --- a/helm/software/matita/library/nat/orders.ma +++ b/helm/software/matita/library/nat/orders.ma @@ -182,8 +182,8 @@ qed. theorem le_n_O_to_eq : \forall n:nat. n \leq O \to O=n. intro.elim n.reflexivity. apply False_ind. -apply not_le_Sn_O. -goal 17. apply H1. +apply not_le_Sn_O; +[2: apply H1 | skip]. qed. theorem le_n_O_elim: \forall n:nat.n \leq O \to \forall P: nat \to Prop. diff --git a/helm/software/matita/matitaGui.ml b/helm/software/matita/matitaGui.ml index 684e1fa2f..55db1774c 100644 --- a/helm/software/matita/matitaGui.ml +++ b/helm/software/matita/matitaGui.ml @@ -973,8 +973,8 @@ class gui () = if (MatitaScript.current ())#onGoingProof () then (MatitaScript.current ())#advance ~statement:("\n" - ^ GrafiteAstPp.pp_tactical ~term_pp:CicNotationPp.pp_term - ~lazy_term_pp:CicNotationPp.pp_term (A.Tactic (loc, ast))) + ^ GrafiteAstPp.pp_tactic ~term_pp:CicNotationPp.pp_term + ~lazy_term_pp:CicNotationPp.pp_term ast) () in let tac_w_term ast _ = diff --git a/helm/software/matita/matitaMathView.ml b/helm/software/matita/matitaMathView.ml index 4252014bd..3b4c566e2 100644 --- a/helm/software/matita/matitaMathView.ml +++ b/helm/software/matita/matitaMathView.ml @@ -303,9 +303,9 @@ object (self) "\n" ^ GrafiteAstPp.pp_executable ~term_pp:(fun s -> s) ~lazy_term_pp:(fun _ -> assert false) ~obj_pp:(fun _ -> assert false) - (GrafiteAst.Tactical (loc, - GrafiteAst.Tactic (loc, GrafiteAst.Reduce (loc, kind, pat)), - Some (GrafiteAst.Semicolon loc))) in + (GrafiteAst.Tactic (loc, + Some (GrafiteAst.Reduce (loc, kind, pat)), + GrafiteAst.Semicolon loc)) in (MatitaScript.current ())#advance ~statement () in connect_menu_item copy gui#copy; connect_menu_item normalize (reduction_action `Normalize); diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml index 8ab94d979..9eb1dbf69 100644 --- a/helm/software/matita/matitaScript.ml +++ b/helm/software/matita/matitaScript.ml @@ -60,14 +60,6 @@ let first_line s = String.sub s 0 nl_pos with Not_found -> s - (** creates a statement AST for the Goal tactic, e.g. "goal 7" *) -let goal_ast n = - let module A = GrafiteAst in - let loc = HExtlib.dummy_floc in - A.Executable (loc, A.Tactical (loc, - A.Tactic (loc, A.Goal (loc, n)), - Some (A.Dot loc))) - type guistuff = { mathviewer:MatitaTypes.mathViewer; urichooser: UriManager.uri list -> UriManager.uri list; @@ -255,10 +247,9 @@ let rec eval_macro include_paths (buffer : GText.buffer) guistuff lexicon_status | [uri] -> let suri = UriManager.string_of_uri uri in let ast loc = - TA.Executable (loc, (TA.Tactical (loc, - TA.Tactic (loc, - TA.Apply (loc, CicNotationPt.Uri (suri, None))), - Some (TA.Dot loc)))) in + TA.Executable (loc, (TA.Tactic (loc, + Some (TA.Apply (loc, CicNotationPt.Uri (suri, None))), + TA.Dot loc))) in let text = comment parsed_text ^ "\n" ^ pp_eager_statement_ast (ast HExtlib.dummy_floc) in