From: Claudio Sacerdoti Coen Date: Thu, 30 Nov 2006 15:06:26 +0000 (+0000) Subject: New syntax and semantics for the rewriting steps that make the pretty-printed X-Git-Tag: 0.4.95@7852~761 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b309e9baa51822004379ce6364e138e5e803efe4;p=helm.git New syntax and semantics for the rewriting steps that make the pretty-printed proof similar to the input proof. Syntax: ((obtain id | conclude) lhs) = rhs done? Semantics: use conclude when working top-down and obtain to work bottom-up. done means that this was the last step. --- diff --git a/components/grafite/grafiteAst.ml b/components/grafite/grafiteAst.ml index a4d357702..9c5d56024 100644 --- a/components/grafite/grafiteAst.ml +++ b/components/grafite/grafiteAst.ml @@ -98,8 +98,9 @@ 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 of 'term | `Auto of (string * string) list ] * Cic.name option + loc * (string option * 'term) option * 'term * + [ `Term of 'term | `Auto of (string * string) list ] * + bool (* last step*) type search_kind = [ `Locate | `Hint | `Match | `Elim ] diff --git a/components/grafite/grafiteAstPp.ml b/components/grafite/grafiteAstPp.ml index f7325f54f..f51cd0bca 100644 --- a/components/grafite/grafiteAstPp.ml +++ b/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 `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) + | RewritingStep (_, term, term1, term2, cont) -> (match term with None -> " " | Some (None,term) -> "conclude " ^ term_pp term | Some (Some name,term) -> "obtain (" ^ name ^ ") " ^ 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) ^ (if cont then " done" else "") | Case (_, id, args) -> "case" ^ id ^ String.concat " " diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml index 4c2a63176..65371bc67 100644 --- a/components/grafite_parser/grafiteDisambiguate.ml +++ b/components/grafite_parser/grafiteDisambiguate.ml @@ -328,9 +328,9 @@ let disambiguate_tactic let metasenv,cic = match term1 with None -> metasenv,None - | Some t -> + | Some (start,t) -> let metasenv,t = disambiguate_term context metasenv t in - metasenv,Some t in + metasenv,Some (start,t) in let metasenv,cic'= disambiguate_term context metasenv term2 in let metasenv,cic'' = match term3 with diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml index d00f7de7c..fb0128edb 100644 --- a/components/grafite_parser/grafiteParser.ml +++ b/components/grafite_parser/grafiteParser.ml @@ -268,8 +268,8 @@ 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 -> `Term t | SYMBOL "_" ; params = auto_params' -> `Auto params ] ; cont=rewriting_step_continuation -> - GrafiteAst.RewritingStep(loc, Some termine, t1, t2, cont) + | start=[IDENT "conclude" -> None | IDENT "obtain" ; name = IDENT -> Some name] ; 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 (start,termine), t1, t2, cont) | 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) @@ -299,9 +299,8 @@ EXTEND ] ]; rewriting_step_continuation : [ - [ IDENT "done" -> None - | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id) - | -> Some Cic.Anonymous + [ IDENT "done" -> true + | -> false ] ]; atomic_tactical: diff --git a/components/tactics/declarative.ml b/components/tactics/declarative.ml index 7e276a8bc..77276d929 100644 --- a/components/tactics/declarative.ml +++ b/components/tactics/declarative.ml @@ -134,10 +134,10 @@ let existselim t id1 t1 id2 t2 = let andelim = existselim;; -let rewritingstep ~dbd ~universe lhs rhs just conclude = +let rewritingstep ~dbd ~universe lhs rhs just last_step = let aux ((proof,goal) as status) = let (curi,metasenv,proofbo,proofty) = proof in - let _,context,_ = CicUtil.lookup_meta goal metasenv in + let _,context,gty = CicUtil.lookup_meta goal metasenv in let eq,trans = match LibraryObjects.eq_URI () with None -> raise (ProofEngineTypes.Fail (lazy "You need to register the default equality first. Please use the \"default\" command")) @@ -161,68 +161,66 @@ let rewritingstep ~dbd ~universe lhs rhs just conclude = Tactics.auto ~dbd ~params ~universe | `Term just -> Tactics.apply just in - match lhs with - None -> - let plhs,prhs = - match - fst - (CicTypeChecker.type_of_aux' metasenv context (Cic.Rel 1) - CicUniv.empty_ugraph) - with - Cic.Appl [_;_;plhs;prhs] -> plhs,prhs - | _ -> assert false in - let last_hyp_name = - match context with - (Some (Cic.Name id,_))::_ -> id - | _ -> assert false - in - (match conclude with - None -> - ProofEngineTypes.apply_tactic - (Tacticals.thens - ~start:(Tactics.apply ~term:trans) - ~continuations: - [ Tactics.apply prhs ; - Tactics.apply (Cic.Rel 1) ; - Tacticals.then_ - ~start:(Tactics.clear ~hyps:[last_hyp_name]) - ~continuation:just]) status - | Some name -> - let mk_fresh_name_callback = - fun metasenv context _ ~typ -> - FreshNamesGenerator.mk_fresh_name ~subst:[] - metasenv context name ~typ - in - ProofEngineTypes.apply_tactic - (Tacticals.thens - ~start:(Tactics.cut ~mk_fresh_name_callback - (Cic.Appl [eq ; ty ; plhs ; rhs])) - ~continuations: - [ Tactics.clear ~hyps:[last_hyp_name] ; - Tacticals.thens - ~start:(Tactics.apply ~term:trans) - ~continuations: - [ Tactics.apply prhs ; - Tactics.apply (Cic.Rel 1) ; - Tacticals.then_ - ~start:(Tactics.clear ~hyps:[last_hyp_name]) - ~continuation:just] - ]) status) - | Some lhs -> - match conclude with - None -> ProofEngineTypes.apply_tactic just status - | Some name -> + let plhs,prhs,prepare = + match lhs with + None -> + let plhs,prhs = + match gty with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false + in + plhs,prhs, + (fun continuation -> + ProofEngineTypes.apply_tactic continuation status) + | Some (None,lhs) -> + let plhs,prhs = + match gty with + Cic.Appl [_;_;plhs;prhs] -> plhs,prhs + | _ -> assert false + in + (*CSC: manca check plhs convertibile con lhs *) + plhs,prhs, + (fun continuation -> + ProofEngineTypes.apply_tactic continuation status) + | Some (Some name,lhs) -> + let newmeta = CicMkImplicit.new_meta metasenv [] in + let irl = + CicMkImplicit.identity_relocation_list_for_metavariable context in + let plhs = lhs in + let prhs = Cic.Meta(newmeta,irl) in + plhs,prhs, + (fun continuation -> + let metasenv = (newmeta, context, ty)::metasenv in let mk_fresh_name_callback = - fun metasenv context _ ~typ -> - FreshNamesGenerator.mk_fresh_name ~subst:[] - metasenv context name ~typ + fun metasenv context _ ~typ -> + FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context + (Cic.Name name) ~typ in + let proof = curi,metasenv,proofbo,proofty in + let proof,goals = ProofEngineTypes.apply_tactic (Tacticals.thens - ~start: - (Tactics.cut ~mk_fresh_name_callback - (Cic.Appl [eq ; ty ; lhs ; rhs])) - ~continuations:[ Tacticals.id_tac ; just ]) status + ~start:(Tactics.cut ~mk_fresh_name_callback + (Cic.Appl [eq ; ty ; lhs ; prhs])) + ~continuations:[Tacticals.id_tac ; continuation]) (proof,goal) + in + let goals = + match goals with + [g1;g2] -> [g2;newmeta;g1] + | _ -> assert false + in + proof,goals) + in + let continuation = + if last_step then + (*CSC:manca controllo sul fatto che rhs sia convertibile con prhs*) + just + else + Tacticals.thens + ~start:(Tactics.apply ~term:(Cic.Appl [trans;ty;plhs;rhs;prhs])) + ~continuations:[just ; Tacticals.id_tac] + in + prepare continuation in ProofEngineTypes.mk_tactic aux ;; diff --git a/components/tactics/declarative.mli b/components/tactics/declarative.mli index 64147b778..fae5c7dcf 100644 --- a/components/tactics/declarative.mli +++ b/components/tactics/declarative.mli @@ -52,5 +52,7 @@ val andelim : Cic.term -> string -> Cic.term -> string -> Cic.term -> ProofEngineTypes.tactic val rewritingstep : - dbd:HMysql.dbd -> universe:Universe.universe -> Cic.term option -> Cic.term -> - [ `Term of Cic.term | `Auto of (string * string) list ] -> Cic.name option -> ProofEngineTypes.tactic + dbd:HMysql.dbd -> universe:Universe.universe -> + (string option * Cic.term) option -> Cic.term -> + [ `Term of Cic.term | `Auto of (string * string) list ] -> + bool (* last step *) -> ProofEngineTypes.tactic diff --git a/matita/matita.lang b/matita/matita.lang index c41cc5fdc..f657ccbf1 100644 --- a/matita/matita.lang +++ b/matita/matita.lang @@ -155,6 +155,7 @@ know case obtain + conclude done diff --git a/matita/tests/decl.ma b/matita/tests/decl.ma index 138e37e71..a9d083b64 100644 --- a/matita/tests/decl.ma +++ b/matita/tests/decl.ma @@ -129,7 +129,7 @@ assume p:nat. suppose (n=m) (H). suppose (S m = S p) (K). suppose (n = S p) (L). -obtain (S n) = (S m) by (eq_f ? ? ? ? ? H). +conclude (S n) = (S m) by (eq_f ? ? ? ? ? H). = (S p) by K. = n by (sym_eq ? ? ? L) done. @@ -142,7 +142,7 @@ assume p:nat. suppose (n=m) (H). suppose (S m = S p) (K). suppose (n = S p) (L). -obtain (S n) = (S m) by _. +conclude (S n) = (S m) by _. = (S p) by _. = n by _ done.