From a3417bd94b857a7f96a2221ba5b79444823b2144 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 7 May 2010 21:21:01 +0000 Subject: [PATCH] trace generation with "// by _;" --- .../software/components/grafite/grafiteAst.ml | 1 + .../components/grafite/grafiteAstPp.ml | 4 +- .../grafite_engine/grafiteEngine.ml | 5 +- .../grafite_parser/grafiteParser.ml | 117 ++++++++++++------ helm/software/components/ng_tactics/nAuto.ml | 4 +- helm/software/components/ng_tactics/nAuto.mli | 1 + helm/software/components/ng_tactics/nnAuto.ml | 3 +- .../software/components/ng_tactics/nnAuto.mli | 1 + helm/software/matita/matitaScript.ml | 25 ++++ 9 files changed, 114 insertions(+), 47 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 5b10a5465..97dbb0486 100644 --- 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 66994a410..0e79c035d 100644 --- 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 c44b70178..e8abb0572 100644 --- 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 3d5c662ca..faa17124e 100644 --- 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>; 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> ; 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 6f49f7d36..7a33d6266 100644 --- 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 2e7394d8c..417adcd60 100644 --- 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 39eb0baac..c1b5c302f 100644 --- 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 8f56541e3..2376a773a 100644 --- 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 3a57745a4..4449d3b1d 100644 --- 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 -- 2.39.2