]> matita.cs.unibo.it Git - helm.git/commitdiff
Much ado about nothing:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 14:46:36 +0000 (14:46 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 20 Apr 2007 14:46:36 +0000 (14:46 +0000)
 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

24 files changed:
components/acic_procedural/proceduralTypes.ml
components/grafite/grafiteAst.ml
components/grafite/grafiteAstPp.ml
components/grafite/grafiteAstPp.mli
components/grafite_engine/grafiteEngine.ml
components/grafite_parser/grafiteDisambiguate.ml
components/grafite_parser/grafiteParser.ml
components/tactics/fourierR.ml
components/tactics/proofEngineStructuralRules.ml
components/tactics/proofEngineStructuralRules.mli
components/tactics/ring.ml
components/tactics/tacticals.ml
components/tactics/tacticals.mli
components/tactics/tactics.ml
components/tactics/tactics.mli
components/tptp_grafite/tptp2grafite.ml
matita/help/C/sec_tacticals.xml
matita/library/nat/div_and_mod.ma
matita/library/nat/factorization.ma
matita/library/nat/minus.ma
matita/library/nat/orders.ma
matita/matitaGui.ml
matita/matitaMathView.ml
matita/matitaScript.ml

index b4d88169af438c267948b0c382114856ad2b9c05..8dac90f26bde2c20a7d9e0a5ebee5adcc986960e 100644 (file)
@@ -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 *****************************************************************)
 
index e8811830380cef794daf7f38c68348ae8a959dd8..d7b929de323fa12c0d6be8e37e4890ddeb8d5b02 100644 (file)
@@ -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
index d7ed16efd103aa6cdea44040794c135c4fac44ef..710761ed9a44537881a73c825f2618eb59ee7900 100644 (file)
@@ -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 =
index 7478883aa7fc11df76a0250c0d332e7838693873..35ade2b2399ddb6f19fb259f72b577637929fa9f 100644 (file)
@@ -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
 
index f85c13bbb84a1d9be4c76aed4e06ba003e2a0e57..08b88b95fbc1b5e32ce1c883b2f5a4ed1d2053d3 100644 (file)
@@ -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) ->
index 5748f0bbb0a6178bd1f87463d851fc3d992f8060..912abbcc38d0eadb1dc1235d35010309e719d3e8 100644 (file)
@@ -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) ->
index 3eb64d458fe2892a44f32af5bb1ce5e0af0db1fb..7b515472d2ef386385855a7d78abbf6543513618 100644 (file)
@@ -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)
     ]
   ];
index 4d4f305ae5684d134df97b137e3e7f90afb66c07..d9f0ce9a48f25e8eb9737ef51548b765dca72b30 100644 (file)
@@ -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_ 
index 3db6d4ff3970fde33c680a56634d6e362931ac5f..636ea07c0f3c67d36ba04ae3dc4057a6de4b14e5 100644 (file)
@@ -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))))
index f87a483253fcfcfd493057419b669e64089acabc..d8e9ed376ca948702ff0048b911ad9aa04d4c840 100644 (file)
@@ -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
index 0bc26514d45819ce8e4e2e026edf50c7f765519f..b2d3032706960ca8757588c695cdd16741f48ed2 100644 (file)
@@ -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
index 63b8e12b59a362ddafa4deb855bf215ecf6db5be..3e9c1db2cbb59f2db82f313b5b934f6058ea8657 100644 (file)
@@ -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"))
index a1b8ec7cd3e272af6f107344c81fc14620aec611..cdc3bac77f3557b4bc2b65ccb517892be45290e6 100644 (file)
@@ -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 *)
index 358de13038879ac647cd8e0c489cc3e3156c3d8e..fc1d4b7a3a1c33960f265b0e9cf969b422efc107 100644 (file)
@@ -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
index f95c736bb010c221f0d344e6f9483a955b3d1e27..6000a98ad3fed5cdbe7f168a100b647ca15451b8 100644 (file)
@@ -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
index 5abe88526b4836eb6afb9f5f14550c1d9341908a..3ed457d958dd64d25ee7d29ab111ad53574563c2 100644 (file)
@@ -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 [])@
index bab2ecf64bc47fb63fdf02a33ab060d53fe2b8c6..2f84ae73690c88b25e1b8f073c405d81f8262035 100644 (file)
        <entry/>
        <entry>|</entry>
        <entry><emphasis role="bold">do</emphasis> &nat;
-        &LCFtactical; <emphasis role="bold">end</emphasis>
+        &LCFtactical;
        </entry>
        <entry>&TODO;</entry>
       </row>
        <entry/>
        <entry>|</entry>
        <entry><emphasis role="bold">repeat</emphasis>
-        &LCFtactical; <emphasis role="bold">end</emphasis>
+        &LCFtactical;
        </entry>
        <entry>&TODO;</entry>
       </row>
index 65ba0e9e5127a77ed8c69bb13f50300a058e3213..537d3bcf0d11a4207f313f0103d069c1d9d87041 100644 (file)
@@ -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.
index 37a7045924540be5f718043bc79eba2c3c742842..826a2670a70a6c80822c2baeb4764962822af120 100644 (file)
@@ -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.
index 71c2cc20552a3c6474e93ab502232f3ed202e971..063ab636ee8e3dae8096ba74817f48f838a98d6d 100644 (file)
@@ -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.
index 8be62ae0b54b09267990bea8798358b746c3cebc..3257e2e1a623d1f348f9d149bba0a0c7478355e2 100644 (file)
@@ -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.
index 684e1fa2f3d40f9dc182326175f6db07fd0d5bc7..55db1774cde3e4818ae5bf468082b046a95afe8e 100644 (file)
@@ -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 _ =
index 4252014bd83115bfae8ad9927dfd88cabcef0967..3b4c566e2a9a42c50c80bf7011cf37eabe0831a2 100644 (file)
@@ -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);
index 8ab94d979b05e67a3e4aeef96067ef9c81db6b44..9eb1dbf69c608c9ba231d4e46f45f3ae78fb1f18 100644 (file)
@@ -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