From 403b7486e9f2cb5583a2c8035cf419bbac982fb1 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 29 Nov 2006 21:44:42 +0000 Subject: [PATCH] The rewritingstep declarative command now takes also a list of arguments that are passed to paramodulation (after adding paramodulation=1 and timeout=3 if these parameters are not already forced by the user). --- helm/software/components/grafite/grafiteAst.ml | 3 ++- helm/software/components/grafite/grafiteAstPp.ml | 2 +- .../grafite_parser/grafiteDisambiguate.ml | 6 +++--- .../components/grafite_parser/grafiteParser.ml | 16 +++++++++++----- helm/software/components/tactics/declarative.ml | 15 ++++++++++++--- helm/software/components/tactics/declarative.mli | 2 +- 6 files changed, 30 insertions(+), 14 deletions(-) diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 26a65b531..a4d357702 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -98,7 +98,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | ExistsElim of loc * 'term * 'ident * 'term * 'ident * 'term | AndElim of loc * 'term * 'ident * 'term * 'ident * 'term | RewritingStep of - loc * 'term option * 'term * 'term option * Cic.name option + loc * 'term option * 'term * + [ `Term of 'term | `Auto of (string * string) list ] * Cic.name option type search_kind = [ `Locate | `Hint | `Match | `Elim ] diff --git a/helm/software/components/grafite/grafiteAstPp.ml b/helm/software/components/grafite/grafiteAstPp.ml index 98e57b5c4..f7325f54f 100644 --- a/helm/software/components/grafite/grafiteAstPp.ml +++ b/helm/software/components/grafite/grafiteAstPp.ml @@ -169,7 +169,7 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term | ExistsElim (_, term0, ident, term, ident1, term1) -> "by " ^ term_pp term0 ^ "let " ^ ident ^ ":" ^ term_pp term ^ "such that " ^ term_pp term1 ^ "(" ^ ident1 ^ ")" | AndElim (_, term, ident1, term1, ident2, term2) -> "by " ^ term_pp term ^ "we have " ^ term_pp term1 ^ " (" ^ ident1 ^ ") " ^ "and " ^ term_pp term2 ^ " (" ^ ident2 ^ ")" - | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id) + | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with `Auto params -> "_" ^ String.concat " " (List.map (fun (k,v) -> if v <> "" then k ^ "=" ^ v else k) params) | `Term term2 -> term_pp term2) ^ (match cont with None -> " done" | Some Cic.Anonymous -> "" | Some (Cic.Name id) -> " we proved " ^ id) | Case (_, id, args) -> "case" ^ id ^ String.concat " " diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml index ae4eac520..4c2a63176 100644 --- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml +++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml @@ -334,10 +334,10 @@ let disambiguate_tactic let metasenv,cic'= disambiguate_term context metasenv term2 in let metasenv,cic'' = match term3 with - None -> metasenv,None - | Some t -> + `Auto _ as t -> metasenv,t + | `Term t -> let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + metasenv,`Term t in metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont) diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml index b41ae8ebc..4c1ddffb2 100644 --- a/helm/software/components/grafite_parser/grafiteParser.ml +++ b/helm/software/components/grafite_parser/grafiteParser.ml @@ -133,9 +133,7 @@ EXTEND GrafiteAst.ApplyS (loc, t, params) | IDENT "assumption" -> GrafiteAst.Assumption loc - | IDENT "auto"; params = - LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> - string_of_int v | v = IDENT -> v ] -> i,v ] -> + | IDENT "auto"; params = auto_params -> GrafiteAst.Auto (loc,params) | IDENT "clear"; ids = LIST1 IDENT -> GrafiteAst.Clear (loc, ids) @@ -270,11 +268,19 @@ EXTEND | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> GrafiteAst.Case(loc,id,params) - | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params ] ; cont=rewriting_step_continuation -> GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont) - | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] ; cont=rewriting_step_continuation -> + | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> `Term t | SYMBOL "_" ; params = auto_params -> `Auto params ] ; + cont=rewriting_step_continuation -> GrafiteAst.RewritingStep(loc, None, t1, t2, cont) ] +]; + auto_params: [ + [ params = + LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int -> + string_of_int v | v = IDENT -> v ] -> i,v ] -> + params + ] ]; by_continuation: [ [ IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] -> BYC_weproved (ty,Some id,t1) diff --git a/helm/software/components/tactics/declarative.ml b/helm/software/components/tactics/declarative.ml index b1b38a949..7e276a8bc 100644 --- a/helm/software/components/tactics/declarative.ml +++ b/helm/software/components/tactics/declarative.ml @@ -148,9 +148,18 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude = CicTypeChecker.type_of_aux' metasenv context rhs CicUniv.empty_ugraph in let just = match just with - None -> - Tactics.auto ~dbd ~params:["paramodulation","1"; "timeout","3"] ~universe - | Some just -> Tactics.apply just + `Auto params -> + let params = + if not (List.exists (fun (k,_) -> k = "paramodulation") params) then + ("paramodulation","1")::params + else params in + let params = + if not (List.exists (fun (k,_) -> k = "timeout") params) then + ("timeout","3")::params + else params + in + Tactics.auto ~dbd ~params ~universe + | `Term just -> Tactics.apply just in match lhs with None -> diff --git a/helm/software/components/tactics/declarative.mli b/helm/software/components/tactics/declarative.mli index e9ec4f9df..64147b778 100644 --- a/helm/software/components/tactics/declarative.mli +++ b/helm/software/components/tactics/declarative.mli @@ -53,4 +53,4 @@ val andelim : val rewritingstep : dbd:HMysql.dbd -> universe:Universe.universe -> Cic.term option -> Cic.term -> - Cic.term option -> Cic.name option -> ProofEngineTypes.tactic + [ `Term of Cic.term | `Auto of (string * string) list ] -> Cic.name option -> ProofEngineTypes.tactic -- 2.39.2