]> matita.cs.unibo.it Git - helm.git/commitdiff
New syntax and semantics for the rewriting steps that make the pretty-printed
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 15:06:26 +0000 (15:06 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 30 Nov 2006 15:06:26 +0000 (15:06 +0000)
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.

helm/software/components/grafite/grafiteAst.ml
helm/software/components/grafite/grafiteAstPp.ml
helm/software/components/grafite_parser/grafiteDisambiguate.ml
helm/software/components/grafite_parser/grafiteParser.ml
helm/software/components/tactics/declarative.ml
helm/software/components/tactics/declarative.mli
helm/software/matita/matita.lang
helm/software/matita/tests/decl.ma

index a4d357702925e86a5fb8b4b5e8d643e3b77f54fa..9c5d56024917795facba7653bc89d1019a192754 100644 (file)
@@ -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 ]
 
index f7325f54fb05b74689b1631c8e97399f31775355..f51cd0bcaf81ba03f5d57d7f51e732d36a78d757 100644 (file)
@@ -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 " "
index 4c2a631761679fb8a01fa808d93af4212cba4bf6..65371bc67a85f85ee8a29f30901442ad3857f7c8 100644 (file)
@@ -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
index d00f7de7cfa065215969c7e49e55f7ccc989b20f..fb0128edb0ceb63c423c53832d4eedb1681dd24a 100644 (file)
@@ -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:
index 7e276a8bcef73f63b273e9ed00ae3f61541f7d09..77276d92909866cfcba3c458c10f99eccc32f472 100644 (file)
@@ -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
 ;;
index 64147b778d55a4c90f9bda0ffef6243d1ea4515e..fae5c7dcf3263c67ea821e05a7cb8367fde6cceb 100644 (file)
@@ -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
index c41cc5fdc483250aa3edc867068ad6c807e586f4..f657ccbf166969fcc5e8816100574709e17fd0a6 100644 (file)
     <keyword>know</keyword>
     <keyword>case</keyword>             
     <keyword>obtain</keyword>           
+    <keyword>conclude</keyword>                 
     <keyword>done</keyword>             
 </keyword-list>
 
index 138e37e71fbbd941ad9c48559796071d5d7d0135..a9d083b64cc4eea3198120fbe7a5c7453c1b761f 100644 (file)
@@ -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.