trace generation with "// by _;"

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 5b10a5465cc5fc9ad68889fc87a8236ad3bede2c..97dbb04868ebf2c76ebdbd55b491f6c5403aed8e 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -200,6 +200,7 @@ type ('term,'lazy_term) macro =
 type nmacro =
   | NCheck of loc * CicNotationPt.term
   | Screenshot of loc * string
+  | NAutoInteractive of loc * CicNotationPt.term auto_params
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)

diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml
index 66994a410baa3018fee4c2cf79d7435b0dd557a7..0e79c035d7b0dd9487e71dea28d38e0c0789aa68 100644 (file)
--- a/helm/software/components/grafite/grafiteAstPp.ml
+++ b/helm/software/components/grafite/grafiteAstPp.ml
@@ -98,10 +98,10 @@ let rec pp_ntactic ~map_unicode_to_tex =
   | NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
   | NSmartApply (_,t) -> "fixme"
   | NAuto (_,(None,flgs)) ->
-      "nauto" ^
+      "nautobatch" ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
   | NAuto (_,(Some l,flgs)) ->
-      "nauto" ^ " by " ^
+      "nautobatch" ^ " by " ^
          (String.concat "," (List.map CicNotationPp.pp_term l)) ^
         String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
   | NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index c44b70178fafd36a9069372807fa8e3dd4554a48..e8abb057295acf3a49dedc8e0b7df19e28fc1e2e 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -777,10 +777,11 @@ let eval_ng_tac tac =
            ) hyps,
           (text,prefix_len,concl))
        ) seqs)
-  | GrafiteAst.NAuto (_loc, (None,a)) -> NAuto.auto_tac ~params:(None,a)
+  | GrafiteAst.NAuto (_loc, (None,a)) -> 
+      NAuto.auto_tac ~params:(None,a) ?trace_ref:None
   | GrafiteAst.NAuto (_loc, (Some l,a)) ->
       NAuto.auto_tac
-       ~params:(Some List.map (fun x -> "",0,x) l,a)
+       ~params:(Some List.map (fun x -> "",0,x) l,a) ?trace_ref:None
   | GrafiteAst.NBranch _ -> NTactics.branch_tac ~force:false
   | GrafiteAst.NCases (_loc, what, where) ->
       NTactics.cases_tac 

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 3d5c662ca378447e94099f129925178cffbcbb3f..faa17124edd09053a0634267af03ae4fdb3acb35 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -128,6 +128,11 @@ let npunct_of_punct = function
   | G.Semicolon loc -> G.NSemicolon loc
   | G.Dot loc -> G.NDot loc
 ;;
+let cons_ntac t p = 
+  match t with
+  | G.NTactic(loc,[t]) -> G.NTactic(loc,[t;p])
+  | x -> x
+;;
 
 type by_continuation =
    BYC_done
@@ -237,8 +242,8 @@ EXTEND
   ];
   using: [ [ using = OPT [ IDENT "using"; t = tactic_term -> t ] -> using ] ];
   ntactic: [
-    [ IDENT "napply"; t = tactic_term -> G.NApply (loc, t)
-    | IDENT "napplyS"; t = tactic_term -> G.NSmartApply (loc, t)
+    [ IDENT "napply"; t = tactic_term -> G.NTactic(loc,[G.NApply (loc, t)])
+    | IDENT "napplyS"; t = tactic_term -> G.NTactic(loc,[G.NSmartApply(loc, t)])
     | IDENT "nassert";
        seqs = LIST0 [
         hyps = LIST0
@@ -248,46 +253,72 @@ EXTEND
             id,`Def (bo,ty)];
         SYMBOL <:unicode<vdash>>;
         concl = tactic_term -> (List.rev hyps,concl) ] ->
-         G.NAssert (loc, seqs)
-    | IDENT "nauto"; params = auto_params -> G.NAuto (loc, params)
-    | SYMBOL "/"; num = OPT NUMBER ; SYMBOL "/" ; 
-       (univ,params) = auto_params ->
-        let depth = match num with Some n -> n | None -> "1" in
-          G.NAuto (loc, (univ,["slir","";"depth",depth]@params))
+         G.NTactic(loc,[G.NAssert (loc, seqs)])
+    | IDENT "nauto"; params = auto_params -> 
+        G.NTactic(loc,[G.NAuto (loc, params)])
+    | SYMBOL "/"; num = OPT NUMBER ; 
+       params = nauto_params; SYMBOL "/" ; 
+       just = OPT [ IDENT "by"; by = 
+         [ univ = tactic_term_list1 -> `Univ univ
+         | SYMBOL "{"; SYMBOL "}" -> `EmptyUniv
+         | SYMBOL "_" -> `Trace ] -> by ] ->
+       let depth = match num with Some n -> n | None -> "1" in
+       (match just with
+       | None -> 
+          G.NTactic(loc,
+            [G.NAuto(loc,(None,["slir","";"depth",depth]@params))])
+       | Some (`Univ univ) ->
+          G.NTactic(loc,
+            [G.NAuto(loc,(Some univ,["slir","";"depth",depth]@params))])
+       | Some `EmptyUniv ->
+          G.NTactic(loc,
+            [G.NAuto(loc,(Some [],["slir","";"depth",depth]@params))])
+       | Some `Trace ->
+          G.NMacro(loc,
+             G.NAutoInteractive (loc, (None,["slir","";"depth",depth]@params))))
+    | IDENT "ncheck"; t = term -> G.NMacro(loc,G.NCheck (loc,t))
+    | IDENT "screenshot"; fname = QSTRING -> 
+        G.NMacro(loc,G.Screenshot (loc, fname))
     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
-        G.NCases (loc, what, where)
+        G.NTactic(loc,[G.NCases (loc, what, where)])
     | IDENT "nchange"; what = pattern_spec; "with"; with_what = tactic_term -> 
-        G.NChange (loc, what, with_what)
+        G.NTactic(loc,[G.NChange (loc, what, with_what)])
     | SYMBOL "@"; num = OPT NUMBER; l = LIST0 tactic_term -> 
-        G.NConstructor (loc,
-           (match num with None -> None | Some x -> Some (int_of_string x)),l)
-    | IDENT "ncut"; t = tactic_term -> G.NCut (loc, t)
+        G.NTactic(loc,[G.NConstructor (loc, (match num with None -> None | Some x -> Some (int_of_string x)),l)])
+    | IDENT "ncut"; t = tactic_term -> G.NTactic(loc,[G.NCut (loc, t)])
 (*  | IDENT "ndiscriminate"; t = tactic_term -> G.NDiscriminate (loc, t)
     | IDENT "nsubst"; t = tactic_term -> G.NSubst (loc, t) *)
-    | IDENT "ndestruct" -> G.NDestruct loc
+    | IDENT "ndestruct" -> G.NTactic(loc,[G.NDestruct loc])
     | IDENT "nelim"; what = tactic_term ; where = pattern_spec ->
-        G.NElim (loc, what, where)
+        G.NTactic(loc,[G.NElim (loc, what, where)])
     | IDENT "ngeneralize"; p=pattern_spec ->
-        G.NGeneralize (loc, p)
+        G.NTactic(loc,[G.NGeneralize (loc, p)])
     | IDENT "ninversion"; what = tactic_term ; where = pattern_spec ->
-        G.NInversion (loc, what, where)
-    | IDENT "nlapply"; t = tactic_term -> G.NLApply (loc, t)
+        G.NTactic(loc,[G.NInversion (loc, what, where)])
+    | IDENT "nlapply"; t = tactic_term -> G.NTactic(loc,[G.NLApply (loc, t)])
     | IDENT "nletin"; name = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term;
         where = pattern_spec ->
-        G.NLetIn (loc,where,t,name)
+        G.NTactic(loc,[G.NLetIn (loc,where,t,name)])
     | kind = nreduction_kind; p = pattern_spec ->
-        G.NReduce (loc, kind, p)
+        G.NTactic(loc,[G.NReduce (loc, kind, p)])
     | IDENT "nrewrite"; dir = direction; what = tactic_term ; where = pattern_spec ->  
-        G.NRewrite (loc, dir, what, where)
-    | IDENT "ntry"; tac = SELF -> G.NTry (loc,tac)
-    | IDENT "nrepeat"; tac = SELF -> G.NRepeat (loc,tac)
-    | LPAREN; l = LIST1 SELF; RPAREN -> G.NBlock (loc,l)
-    | IDENT "nassumption" -> G.NAssumption loc
-    | SYMBOL "#"; n=IDENT -> G.NIntro (loc,n)
-    | SYMBOL "#"; SYMBOL "_" -> G.NIntro (loc,"_")
-    | SYMBOL "*" -> G.NCase1 (loc,"_")
-    | SYMBOL "*"; n=IDENT ->
-        G.NCase1 (loc,n)
+        G.NTactic(loc,[G.NRewrite (loc, dir, what, where)])
+    | IDENT "ntry"; tac = SELF -> 
+        let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
+        G.NTactic(loc,[ G.NTry (loc,tac)])
+    | IDENT "nrepeat"; tac = SELF -> 
+        let tac = match tac with G.NTactic(_,[t]) -> t | _ -> assert false in
+        G.NTactic(loc,[ G.NRepeat (loc,tac)])
+    | LPAREN; l = LIST1 SELF; RPAREN -> 
+        let l = 
+          List.flatten 
+            (List.map (function G.NTactic(_,t) -> t | _ -> assert false) l) in
+        G.NTactic(loc,[G.NBlock (loc,l)])
+    | IDENT "nassumption" -> G.NTactic(loc,[ G.NAssumption loc])
+    | SYMBOL "#"; n=IDENT -> G.NTactic(loc,[ G.NIntro (loc,n)])
+    | SYMBOL "#"; SYMBOL "_" -> G.NTactic(loc,[ G.NIntro (loc,"_")])
+    | SYMBOL "*" -> G.NTactic(loc,[ G.NCase1 (loc,"_")])
+    | SYMBOL "*"; n=IDENT -> G.NTactic(loc,[ G.NCase1 (loc,n)])
     ]
   ];
   tactic: [
@@ -509,6 +540,16 @@ EXTEND
       params
    ]
 ];
+  nauto_params: [
+    [ params = 
+      LIST0 [
+         i = auto_fixed_param -> i,""
+       | i = auto_fixed_param ; SYMBOL "="; v = [ v = int ->
+              string_of_int v | v = IDENT -> v ] -> i,v ] ->
+      params
+   ]
+];
+
   inline_params:[
    [ params = LIST0 
       [ IDENT "prefix"; SYMBOL "="; prefix = QSTRING -> G.IPPrefix prefix  
@@ -673,12 +714,6 @@ EXTEND
         (params,name,typ,fields)
     ] ];
 
-    nmacro: [
-      [ [ IDENT "ncheck" ]; t = term -> G.NCheck (loc,t)
-      | [ IDENT "screenshot"]; fname = QSTRING -> G.Screenshot (loc, fname)
-      ]
-    ];
-    
     macro: [
       [ [ IDENT "check"   ]; t = term ->
           G.Check (loc, t)
@@ -943,10 +978,13 @@ EXTEND
     | tac = atomic_tactical LEVEL "loops"; punct = punctuation_tactical ->
         G.Tactic (loc, Some tac, punct)
     | punct = punctuation_tactical -> G.Tactic (loc, None, punct)
-    | tac = ntactic; SYMBOL "#" ; SYMBOL "#" ; punct = punctuation_tactical ->
-        G.NTactic (loc, [tac; npunct_of_punct punct])
+    | tac = ntactic; OPT [ SYMBOL "#" ; SYMBOL "#" ] ; 
+      punct = punctuation_tactical ->
+        cons_ntac tac (npunct_of_punct punct)
+(*
     | tac = ntactic; punct = punctuation_tactical ->
-        G.NTactic (loc, [tac; npunct_of_punct punct])
+        cons_ntac tac (npunct_of_punct punct)
+*)
     | SYMBOL "#" ; SYMBOL "#" ; punct = npunctuation_tactical ->
         G.NTactic (loc, [punct])
     | tac = non_punctuation_tactical; punct = punctuation_tactical ->
@@ -958,7 +996,6 @@ EXTEND
         punct = punctuation_tactical ->
           G.NTactic (loc, [nnon_punct_of_punct tac; npunct_of_punct punct])
     | mac = macro; SYMBOL "." -> G.Macro (loc, mac)
-    | mac = nmacro; SYMBOL "." -> G.NMacro (loc, mac)
     ]
   ];
   comment: [

diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml
index 6f49f7d36575b4c9d21cf9e66a768728d1bcda0d..7a33d6266da45052fc2a16328d60f8dcbf5ce5b8 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.ml
+++ b/helm/software/components/ng_tactics/nAuto.ml
@@ -1709,7 +1709,7 @@ let auto_tac ~params =
 ;;
 
 (* ========================= dispatching of auto/auto_paramod ============ *)
-let auto_tac ~params:(_,flags as params) =
+let auto_tac ~params:(_,flags as params) ?trace_ref =
   if List.mem_assoc "paramodulation" flags then 
     auto_paramod_tac ~params 
   else if List.mem_assoc "demod" flags then 
@@ -1719,7 +1719,7 @@ let auto_tac ~params:(_,flags as params) =
   else if List.mem_assoc "fast_paramod" flags then 
     NnAuto.fast_eq_check_tac ~params  
   else if List.mem_assoc "slir" flags then 
-    NnAuto.auto_tac ~params  
+    NnAuto.auto_tac ~params ?trace_ref
   else 
     auto_tac ~params
 ;;

diff --git a/helm/software/components/ng_tactics/nAuto.mli b/helm/software/components/ng_tactics/nAuto.mli
index 2e7394d8c8bdc3b40351238359363805481ecb9b..417adcd60fbd4069784040fc743d76c7735218ec 100644 (file)
--- a/helm/software/components/ng_tactics/nAuto.mli
+++ b/helm/software/components/ng_tactics/nAuto.mli
@@ -13,6 +13,7 @@
 
 val auto_tac:
   params:(NTacStatus.tactic_term list option * (string * string) list) -> 
+  ?trace_ref:CicNotationPt.term list ref ->
    's NTacStatus.tactic
 
 val group_by_tac:

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 39eb0baac01ac22eb6d0c480fba01b315233370e..c1b5c302f2b5a27147eff1c629c4558fca12f516 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1662,7 +1662,7 @@ let cleanup_trace s trace =
            | _ -> false) trace
 ;;
 
-let auto_tac ~params:(univ,flags) status =
+let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
   let oldstatus = status in
   let status = (status:> NTacStatus.tac_status) in
   let goals = head_goals status#stack in
@@ -1734,6 +1734,7 @@ let auto_tac ~params:(univ,flags) status =
                   | _ -> assert false
               in
               let s = s#set_stack stack in
+                trace_ref := trace;
                 oldstatus#set_status s 
   in
   let s = up_to depth depth in

diff --git a/helm/software/components/ng_tactics/nnAuto.mli b/helm/software/components/ng_tactics/nnAuto.mli
index 8f56541e3d95732e3cbd732e1e4cd556b3538623..2376a773ad3ad7db387e74e98bbe6d8b19ce80c1 100644 (file)
--- a/helm/software/components/ng_tactics/nnAuto.mli
+++ b/helm/software/components/ng_tactics/nnAuto.mli
@@ -29,6 +29,7 @@ val smart_apply_tac:
 
 val auto_tac:
   params:(NTacStatus.tactic_term list option * (string * string) list) -> 
+   ?trace_ref:CicNotationPt.term list ref -> 
    's NTacStatus.tactic
 
 val keys_of_type: 

diff --git a/helm/software/matita/matitaScript.ml b/helm/software/matita/matitaScript.ml
index 3a57745a48af9dcfd6ba76290cbd479c857b24de..4449d3b1df8757728de30a7aafef143700efb1ab 100644 (file)
--- a/helm/software/matita/matitaScript.ml
+++ b/helm/software/matita/matitaScript.ml
@@ -393,6 +393,31 @@ let eval_nmacro include_paths (buffer : GText.buffer) guistuff grafite_status us
       in
       guistuff.mathviewer#show_entry (`NCic (t,ctx,m,s));
       [status, parsed_text], "", parsed_text_length
+  | TA.NAutoInteractive (_loc, (None,a)) -> 
+      let trace_ref = ref [] in
+      let s = 
+        NnAuto.auto_tac 
+          ~params:(None,a) ~trace_ref script#grafite_status 
+      in
+      let depth = 
+        try List.assoc "depth" a
+        with Not_found -> ""
+      in
+      let trace = "/"^(if int_of_string depth > 1 then depth else "")^"/ by " in
+      let thms = 
+        match !trace_ref with
+        | [] -> "{}"
+        | thms -> 
+           String.concat ", "  
+             (HExtlib.filter_map (function 
+               | CicNotationPt.NRef r -> Some (NCicPp.r2s true r) 
+               | _ -> None) 
+             thms)
+      in
+      let rex = Pcre.regexp ~flags:[`MULTILINE] "\\A([\\n\\t\\r ]*).*\\Z" in
+      let nl = Pcre.replace ~rex ~templ:"$1" parsed_text in
+      [s, nl ^ trace ^ thms ^ ";"], "", parsed_text_length
+  | TA.NAutoInteractive (_, (Some _,_)) -> assert false
 
 let rec eval_macro include_paths (buffer : GText.buffer) guistuff grafite_status user_goal unparsed_text parsed_text script mac =
   let module MQ = MetadataQuery in