From: maiorino Date: Thu, 27 Jul 2006 09:32:47 +0000 (+0000) Subject: New declarative commands (ast, pretty-printing and parsing only): X-Git-Tag: 0.4.95@7852~1142 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2135f4eb98004c55f67ae3fa52ca60d53a86d9f2;p=helm.git New declarative commands (ast, pretty-printing and parsing only): [obtain term] = term by term by term we have term (id) and term (id) we proceed by induction on term to prove term the thesis becomes term by induciton hypothesis we know term case id [(id:term)]* --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index 246df11c2..65e35634f 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -87,11 +87,18 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic = | Transitivity of loc * 'term (* Costruttori Aggiunti *) | Assume of loc * 'ident * 'term - | Suppose of loc * 'term *'ident - | By_term_we_proved of loc * 'term * 'term * 'ident - | We_need_to_prove of loc * 'term * 'ident - | Bydone of loc * '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 + | Bydone of loc * 'term option + | We_proceed_by_induction_on of loc * 'term * 'term + | Byinduction of loc * 'term * 'ident + | Thesisbecomes of loc * 'term + | Case of loc * string * (string * 'term) list + | Let1 of loc * 'ident * 'term * 'term + | Bywehave of loc * 'term option * 'term * 'ident * 'term * 'ident + | RewritingStep of loc * 'term option * 'term * 'term option + type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] @@ -109,7 +116,7 @@ type 'term macro = (** To be increased each time the command type below changes, used for "safe" * marshalling *) -let magic = 6 +let magic = 7 type 'obj command = | Default of loc * string * UriManager.uri list diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index 4a94152de..8f037f032 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/components/grafite/grafiteAstPp.ml @@ -154,8 +154,26 @@ let rec pp_tactic ~term_pp ~lazy_term_pp = | Split _ -> "split" | Symmetry _ -> "symmetry" | Transitivity (_, term) -> "transitivity " ^ term_pp term - - let pp_search_kind = function + (* Tattiche Aggiunte *) + | 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^ ")" ^ + (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_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 + | Let1 (_, ident, term, term1) -> "let" ^ ident ^ ":" ^ term_pp term ^ "such that" ^ term_pp term1 + | Bywehave (_, term, term1, ident, term2, ident1) -> "by" ^ (match term with None -> "_" | Some term -> term_pp term) ^ "we have" ^ term_pp term1 ^ "(" ^ ident ^ ")" ^ "and" ^ term_pp term2 ^ "(" ^ ident1 ^ ")" + | RewritingStep (_, term, term1, term2 ) -> (match term with None -> " " | Some term -> "obtain " ^ term_pp term) ^ "=" ^ term_pp term1 ^ (match term2 with None -> "_" | Some term2 -> term_pp term2 ) + | Case (_, id, args) -> + "case" ^ id ^ + String.concat " " + (List.map (function (id,term) -> "(" ^ id ^ ": " ^ term_pp term ^ ")") + args) + + let pp_search_kind = function | `Locate -> "locate" | `Hint -> "hint" | `Match -> "match" diff --git a/components/grafite_engine/grafiteEngine.ml b/components/grafite_engine/grafiteEngine.ml index 6dff5468d..c96de1896 100644 --- a/components/grafite_engine/grafiteEngine.ml +++ b/components/grafite_engine/grafiteEngine.ml @@ -156,13 +156,21 @@ let tactic_of_ast ast = | GrafiteAst.Transitivity (_, term) -> Tactics.transitivity term (* Implementazioni Aggiunte *) | GrafiteAst.Assume (_, id, t) -> Declarative.assume id t - | GrafiteAst.Suppose (_, t, id) -> Declarative.suppose t id - | GrafiteAst.By_term_we_proved (_, t, ty, id) -> - Declarative.by_term_we_proved t ty id - | GrafiteAst.We_need_to_prove (_, t, id) -> Declarative.we_need_to_prove t id - | GrafiteAst.Bydone (_, t) -> Declarative.bydone t + | GrafiteAst.Suppose (_, t, id, t1) -> Declarative.suppose t id t1 + | GrafiteAst.By_term_we_proved (_, t, ty, id, t1) -> + Declarative.by_term_we_proved t ty id t1 + | GrafiteAst.We_need_to_prove (_, t, id, t2) -> + Declarative.we_need_to_prove t id t2 + | GrafiteAst.Bydone (_, t) -> Declarative.bydone t + | GrafiteAst.We_proceed_by_induction_on (_, t, t1) -> + Declarative.we_proceed_by_induction_on t t1 + | GrafiteAst.Byinduction (_, t, id) -> Declarative.assume id t + | GrafiteAst.Thesisbecomes (_, t) -> Declarative.thesisbecomes t + | GrafiteAst.Let1 (_, id, t, t1) -> Declarative.let1 id t t1 + | GrafiteAst.Case (_,id,params) -> Declarative.case id params + | GrafiteAst.Bywehave(_,t,t1,id,t2,id1) -> Declarative.bywehave t t1 id t2 id1 + | GrafiteAst.RewritingStep (_,termine,t1,t2) -> Declarative.prova termine t1 t2 -(* maybe we only need special cases for apply and goal *) let classify_tactic tactic = match tactic with (* tactics that can't close the goal (return a goal we want to "select") *) diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 04521361d..2e7f1224f 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -1,4 +1,4 @@ -(* Copyright (C) 2005, HELM Team. +(* * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -255,19 +255,96 @@ let disambiguate_tactic | GrafiteAst.Assume (loc, id, term) -> let metasenv,cic = disambiguate_term context metasenv term in metasenv,GrafiteAst.Assume (loc, id, cic) - | GrafiteAst.Suppose (loc, term, id) -> - let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Suppose (loc, cic, id) + | GrafiteAst.Suppose (loc, term, id, term') -> + let metasenv,cic = disambiguate_term context metasenv term in + let metasenv,cic' = + match term' with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.Suppose (loc, cic, id, cic') | GrafiteAst.Bydone (loc,term) -> + let metasenv,cic = + match term with + None -> metasenv,None + |Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.Bydone (loc, cic) + | GrafiteAst.We_need_to_prove (loc,term,id,term') -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.Bydone (loc, cic) - | GrafiteAst.We_need_to_prove (loc,term,id) -> + let metasenv,cic' = + match term' with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.We_need_to_prove (loc,cic,id,cic') + | GrafiteAst.By_term_we_proved (loc,term,term',id,term'') -> + let metasenv,cic = + match term with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + let metasenv,cic' = disambiguate_term context metasenv term' in + let metasenv,cic'' = + match term'' with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id,cic'') + | GrafiteAst.We_proceed_by_induction_on (loc, term, term') -> let metasenv,cic = disambiguate_term context metasenv term in - metasenv,GrafiteAst.We_need_to_prove (loc,cic,id) - | GrafiteAst.By_term_we_proved (loc,term,term',id) -> + let metasenv,cic' = disambiguate_term context metasenv term' in + metasenv,GrafiteAst.We_proceed_by_induction_on (loc, cic, cic') + | GrafiteAst.Byinduction (loc, term, id) -> let metasenv,cic = disambiguate_term context metasenv term in - let metasenv,cic' = disambiguate_term context metasenv term' in - metasenv,GrafiteAst.By_term_we_proved (loc,cic,cic',id) + metasenv,GrafiteAst.Byinduction(loc, cic, id) + | GrafiteAst.Thesisbecomes (loc, term) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,GrafiteAst.Thesisbecomes (loc, cic) + | GrafiteAst.Let1 (loc, id, term, term1) -> + let metasenv,cic = disambiguate_term context metasenv term in + let metasenv,cic'= disambiguate_term context metasenv term1 in + metasenv,GrafiteAst.Let1(loc, id, cic, cic') + | GrafiteAst.Bywehave (loc, term, term1, id, term2, id1) -> + let metasenv,cic = + match term with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + let metasenv,cic'= disambiguate_term context metasenv term1 in + let metasenv,cic''= disambiguate_term context metasenv term2 in + metasenv,GrafiteAst.Bywehave(loc, cic, cic', id, cic'', id1) + | GrafiteAst.Case (loc, id, params) -> + let metasenv,params' = + List.fold_right + (fun (id,term) (metasenv,params) -> + let metasenv,cic = disambiguate_term context metasenv term in + metasenv,(id,cic)::params + ) params (metasenv,[]) + in + metasenv,GrafiteAst.Case(loc, id, params') + | GrafiteAst.RewritingStep (loc, term1, term2, term3) -> + let metasenv,cic = + match term1 with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + let metasenv,cic'= disambiguate_term context metasenv term2 in + let metasenv,cic'' = + match term3 with + None -> metasenv,None + | Some t -> + let metasenv,t = disambiguate_term context metasenv t in + metasenv,Some t in + metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'') + let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) = let uri = diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index 13ee7297e..5d6dac771 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -234,16 +234,40 @@ EXTEND (* Produzioni Aggiunte *) | IDENT "assume" ; id = IDENT ; SYMBOL ":" ; t = tactic_term -> GrafiteAst.Assume (loc, id, t) - | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> - GrafiteAst.Suppose (loc, t, id) - | IDENT "by" ; t = tactic_term ; IDENT "we" ; IDENT "proved" ; ty = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> - GrafiteAst.By_term_we_proved (loc, t, ty, id) - | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN -> - GrafiteAst.We_need_to_prove (loc, t, id) - | IDENT "by" ; t = tactic_term ; IDENT "done" -> - GrafiteAst.Bydone (loc, t) + | IDENT "suppose" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> t']-> + GrafiteAst.Suppose (loc, t, id, t1) + | IDENT "by" ; t = [t' = tactic_term -> Some t' | SYMBOL "_" -> None]; + cont=by_continuation -> + (match cont with + None -> GrafiteAst.Bydone (loc, t) + | Some (ty,id,t1) -> + GrafiteAst.By_term_we_proved(loc, t, ty, id, t1)) + | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; LPAREN ; id = IDENT ; RPAREN ; 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) + | IDENT "by" ; IDENT "induction" ; IDENT "hypothesis" ; IDENT "we" ; IDENT "know" ; t=tactic_term ; LPAREN ; id = IDENT ; RPAREN -> + GrafiteAst.Byinduction(loc, t, id) + | IDENT "the" ; IDENT "thesis" ; IDENT "becomes" ; t=tactic_term -> + GrafiteAst.Thesisbecomes(loc, t) + | IDENT "case" ; id = IDENT ; params=LIST0[LPAREN ; i=IDENT ; + SYMBOL":" ; t=tactic_term ; RPAREN -> i,t] -> + GrafiteAst.Case(loc,id,params) + | IDENT "let" ; id = IDENT ; SYMBOL ":" ; t = tactic_term ; IDENT "such" ; IDENT "that" ; t1=tactic_term -> + GrafiteAst.Let1 (loc, id, t, t1) + | IDENT "by" ; t=[t'=tactic_term->Some t'|SYMBOL "_"-> None] ; IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id=IDENT ; RPAREN ; IDENT "and" ; t2=tactic_term ; LPAREN ; id1=IDENT ; RPAREN -> + GrafiteAst.Bywehave (loc, t, t1, id, t2, id1) + | IDENT "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] -> + GrafiteAst.RewritingStep(loc, Some termine, t1, t2) + | SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None ] -> + GrafiteAst.RewritingStep(loc, None, t1, t2) + ] +]; + 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] -> Some (ty,id,t1) + | IDENT "done" -> None ] - ]; +]; atomic_tactical: [ "sequence" LEFTA [ t1 = SELF; SYMBOL ";"; t2 = SELF -> diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index a1c8cab69..1604d92d8 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -24,16 +24,16 @@ *) let assume id t = - Tacticals.then_ - ~start: - (Tactics.intros ~howmany:1 - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) - ~continuation: - (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) - (fun _ metasenv ugraph -> t,metasenv,ugraph)) + Tacticals.then_ + ~start: + (Tactics.intros ~howmany:1 + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id) ()) + ~continuation: + (Tactics.change ~pattern:(None,[id,Cic.Implicit (Some `Hole)],None) + (fun _ metasenv ugraph -> t,metasenv,ugraph)) ;; -let suppose t id = +let suppose t id ty = Tacticals.then_ ~start: (Tactics.intros ~howmany:1 @@ -43,20 +43,26 @@ let suppose t id = (fun _ metasenv ugraph -> t,metasenv,ugraph)) ;; -let by_term_we_proved t ty id = - Tacticals.thens - ~start: - (Tactics.cut ty - ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) - ~continuations: - [ Tacticals.id_tac ; Tactics.apply t ] +let by_term_we_proved t ty id ty' = + match t with + None -> assert false + | Some t -> + Tacticals.thens + ~start: + (Tactics.cut ty + ~mk_fresh_name_callback:(fun _ _ _ ~typ -> Cic.Name id)) + ~continuations: + [ Tacticals.id_tac ; Tactics.apply t ] ;; let bydone t = - (Tactics.apply ~term:t) + match t with + None -> assert false + | Some t -> + (Tactics.apply ~term:t) ;; -let we_need_to_prove t id = +let we_need_to_prove t id ty = let aux status = let proof,goals = ProofEngineTypes.apply_tactic @@ -73,3 +79,17 @@ let we_need_to_prove t id = in ProofEngineTypes.mk_tactic aux ;; + +let prova _ = assert false +;; +let bywehave _ = assert false +;; +let case _ = assert false +;; +let thesisbecomes _ = assert false +;; +let byinduction _ = assert false +;; +let we_proceed_by_induction_on _ = assert false +;; +let let1 _ = assert false diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli index 2e9d506ca..ba2eaaea4 100644 --- a/components/tactics/declarative.mli +++ b/components/tactics/declarative.mli @@ -24,7 +24,29 @@ *) val assume : string -> Cic.term -> ProofEngineTypes.tactic -val suppose : Cic.term -> string -> ProofEngineTypes.tactic -val by_term_we_proved : Cic.term -> Cic.term -> string -> ProofEngineTypes.tactic -val bydone : Cic.term -> ProofEngineTypes.tactic -val we_need_to_prove : Cic.term -> string -> ProofEngineTypes.tactic + +val suppose : Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic + +val by_term_we_proved : Cic.term option -> Cic.term -> string -> Cic.term option ->ProofEngineTypes.tactic + +val bydone : Cic.term option -> ProofEngineTypes.tactic + +val we_need_to_prove : + Cic.term -> string -> Cic.term option -> ProofEngineTypes.tactic + +val we_proceed_by_induction_on : Cic.term -> Cic.term -> ProofEngineTypes.tactic + +val byinduction : Cic.term -> string -> ProofEngineTypes.tactic + +val thesisbecomes : Cic.term -> ProofEngineTypes.tactic + +val case : string -> params:(string * Cic.term) list -> ProofEngineTypes.tactic + +val let1 : string -> Cic.term -> Cic.term -> ProofEngineTypes.tactic + +val bywehave : + Cic.term option -> Cic.term -> string -> Cic.term -> string -> + ProofEngineTypes.tactic + +val prova : + Cic.term option -> Cic.term -> Cic.term option -> ProofEngineTypes.tactic diff --git a/matita/matita.lang b/matita/matita.lang index 4b88fa91d..0dbfa4c78 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -127,7 +127,33 @@ transitivity unfold whd - + (* Tattiche Aggiunte *) + assume + suppose + by + we + prove + proved + need + proceed + induction + inductive + case + base + let + such + that + by + have + and + the + thesis + becomes + hypothesis + know + case + obtain + try