From e11e617809bbf3757ddfcbd6ef6d28d20e14a4f0 Mon Sep 17 00:00:00 2001 From: maiorino Date: Tue, 3 Oct 2006 16:05:50 +0000 Subject: [PATCH] Some declarative tactics did not allow the "done" option in place of "(id)". Fixed. --- components/grafite/grafiteAst.ml | 4 ++-- components/grafite/grafiteAstPp.ml | 4 ++-- components/grafite_parser/grafiteParser.ml | 4 ++-- components/tactics/declarative.ml | 2 ++ components/tactics/declarative.mli | 4 ++-- 5 files changed, 10 insertions(+), 8 deletions(-) diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 6ab2b2fc6..e4b2cf24d 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -88,8 +88,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = (* Costruttori Aggiunti *) | Assume of loc * 'ident * 'term | Suppose of loc * 'term *'ident * 'term option - | By_term_we_proved of loc *'term option * 'term * 'ident * 'term option - | We_need_to_prove of loc * 'term * 'ident * 'term option + | By_term_we_proved of loc *'term option * 'term * 'ident option * 'term option + | We_need_to_prove of loc * 'term * 'ident option * 'term option | Bydone of loc * 'term option | We_proceed_by_induction_on of loc * 'term * 'term | Byinduction of loc * 'term * 'ident diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 547e28b3d..5644d33d3 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -158,9 +158,9 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Assume (_, ident , term) -> "assume" ^ ident ^ ":" ^ term_pp term | Suppose (_, term, ident,term1) -> "suppose" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1) | Bydone (_, term) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "done" - | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ "(" ^ident^ ")" ^ + | By_term_we_proved (_, term, term1, ident, term2) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we proved" ^ term_pp term1 ^ (match ident with None -> "" | Some ident -> "(" ^ident^ ")") ^ (match term2 with None -> " " | Some term2 -> term_pp term2) - | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ "(" ^ ident ^ ")" ^ (match term1 with None -> " " | Some term1 -> term_pp term1) + | We_need_to_prove (_, term, ident, term1) -> "we need to prove" ^ term_pp term ^ (match ident with None -> "" | Some ident -> "(" ^ ident ^ ")") ^ (match term1 with None -> " " | Some term1 -> term_pp term1) | We_proceed_by_induction_on (_, term, term1) -> "we proceed by induction on" ^ term_pp term ^ "to prove" ^ term_pp term1 | Byinduction (_, term, ident) -> "by induction hypothesis we know" ^ term_pp term ^ "(" ^ ident ^ ")" | Thesisbecomes (_, term) -> "the thesis becomes " ^ term_pp term diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 5c7d31223..6e108ce04 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -55,7 +55,7 @@ let default_associativity = Gramext.NonA type by_continuation = BYC_done - | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option + | BYC_weproved of CicNotationPt.term * string option * CicNotationPt.term option | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term @@ -263,7 +263,7 @@ EXTEND (floc,CicNotationParser.Parse_error "tactic_term expected here")) | LSome t -> GrafiteAst.AndElim (loc, t, id1, t1, id2, t2))) - | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; t1 = OPT [IDENT "or" ; IDENT "equivalently"; t' = tactic_term -> t']-> GrafiteAst.We_need_to_prove (loc, t, id, t1) | IDENT "we" ; IDENT "proceed" ; IDENT "by" ; IDENT "induction" ; "on" ; t=tactic_term ; "to" ; IDENT "prove" ; t1=tactic_term -> GrafiteAst.We_proceed_by_induction_on (loc, t, t1) diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index c7e5579f8..413a43fe3 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -46,6 +46,7 @@ let suppose t id ty = ;; let by_term_we_proved ~dbd t ty id ty' = +match id with None -> assert false | Some id -> let just = match t with None -> Tactics.auto ~dbd ~params:[] @@ -75,6 +76,7 @@ let bydone ~dbd t = ;; let we_need_to_prove t id ty = +match id with None -> assert false | Some id -> let aux status = let cont,cutted = match ty with diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli index e5a8a590c..3b02fb4d9 100644 --- a/components/tactics/declarative.mli +++ b/components/tactics/declarative.mli @@ -28,13 +28,13 @@ val assume : string -> Cic.term -> ProofEngineTypes.tactic val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic val by_term_we_proved : - dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string -> Cic.term option -> + dbd:HMysql.dbd -> Cic.term option -> Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic val bydone : dbd:HMysql.dbd -> Cic.term option -> ProofEngineTypes.tactic val we_need_to_prove : - Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic + Cic.term -> string option -> Cic.term option -> ProofEngineTypes.tactic val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic -- 2.39.2