X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=9373e54b43a1de051f743a2581220677abaf4df8;hb=92081320b50b03d6bf296552d2cae9e4b398f1be;hp=13ee7297eacec364ab468ce5b29209b36371c7e3;hpb=894b08ca7d14aa7e31c35f3acb3903a1c3472a27;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 13ee7297e..9373e54b4 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -53,6 +53,12 @@ let add_raw_attribute ~text t = Ast.AttributedTerm (`Raw text, t)
 let default_precedence = 50
 let default_associativity = Gramext.NonA
 
+type by_continuation =
+   BYC_done
+ | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_letsuchthat of string * CicNotationPt.term * string * CicNotationPt.term
+ | BYC_wehaveand of string * CicNotationPt.term * string * CicNotationPt.term
+
 EXTEND
   GLOBAL: term statement;
   arg: [
@@ -227,6 +233,8 @@ EXTEND
         GrafiteAst.Ring loc
     | IDENT "split" ->
         GrafiteAst.Split loc
+    | IDENT "subst" ->
+        GrafiteAst.Subst loc    
     | IDENT "symmetry" ->
         GrafiteAst.Symmetry loc
     | IDENT "transitivity"; t = tactic_term ->
@@ -234,16 +242,63 @@ 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 -> LSome t' | SYMBOL "_" -> LNone loc];
+      cont=by_continuation ->
+       let t' = match t with LNone _ -> None | LSome t -> Some t in
+       (match cont with
+           BYC_done -> GrafiteAst.Bydone (loc, t')
+	 | BYC_weproved (ty,id,t1) ->
+	    GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
+	 | BYC_letsuchthat (id1,t1,id2,t2) ->
+	    (match t with
+	        LNone floc ->
+                 raise (HExtlib.Localized
+		  (floc,CicNotationParser.Parse_error
+		    "tactic_term expected here"))
+              | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+	 | BYC_wehaveand (id1,t1,id2,t2) ->
+	    (match t with
+	        LNone floc ->
+                 raise (HExtlib.Localized
+		  (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 ; 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 "obtain" ; termine=tactic_term ; SYMBOL "=" ; t1=tactic_term ; IDENT "by" ; t2=[ t=tactic_term -> Some t | SYMBOL "_" -> None  ] ; 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  ->
+     GrafiteAst.RewritingStep(loc, None, t1, t2, cont)
+  ]
+];
+  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,id,t1)
+    | IDENT "done" -> BYC_done
+    | "let" ; id1 = IDENT ; SYMBOL ":" ; t1 = tactic_term ;
+      IDENT "such" ; IDENT "that" ; t2=tactic_term ; LPAREN ; id2 = IDENT ;
+      RPAREN -> BYC_letsuchthat (id1,t1,id2,t2)
+    | IDENT "we" ; IDENT "have" ; t1=tactic_term ; LPAREN ; id1=IDENT ; RPAREN ;
+      "and" ; t2=tactic_term ; LPAREN ; id2=IDENT ; RPAREN ->
+       BYC_wehaveand (id1,t1,id2,t2)
     ]
-  ];
+];
+  rewriting_step_continuation : [
+    [ IDENT "done" -> None
+    | IDENT "we" ; IDENT "proved" ; id=IDENT -> Some (Cic.Name id)
+    | -> Some Cic.Anonymous
+    ]
+];
   atomic_tactical:
     [ "sequence" LEFTA
       [ t1 = SELF; SYMBOL ";"; t2 = SELF ->
@@ -272,6 +327,7 @@ EXTEND
       | IDENT "solve";
         SYMBOL "["; tacs = LIST0 SELF SEP SYMBOL "|"; SYMBOL "]"->
           GrafiteAst.Solve (loc, tacs)
+      | IDENT "progress"; tac = SELF -> GrafiteAst.Progress (loc, tac)
       | LPAREN; tac = SELF; RPAREN -> tac
       | tac = tactic -> GrafiteAst.Tactic (loc, tac)
       ]
@@ -330,8 +386,14 @@ EXTEND
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
-       coercion = [ SYMBOL ":" -> false | SYMBOL ":"; SYMBOL ">" -> true ] ; 
-       ty = term -> (name,ty,coercion) 
+       coercion = [ 
+           SYMBOL ":" -> false,0 
+         | SYMBOL ":"; SYMBOL ">" -> true,0
+         | SYMBOL ":"; arity = int ; SYMBOL ">" -> true,arity
+       ]; 
+       ty = term -> 
+         let b,n = coercion in 
+         (name,ty,b,n) 
      ] SEP SYMBOL ";"; SYMBOL "}" -> 
       let params =
         List.fold_right
@@ -505,8 +567,9 @@ EXTEND
             ind_types
         in
         GrafiteAst.Obj (loc, Ast.Inductive (params, ind_types))
-    | IDENT "coercion" ; suri = URI ->
-        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true)
+    | IDENT "coercion" ; suri = URI ; arity = OPT int ->
+        let arity = match arity with None -> 0 | Some x -> x in
+        GrafiteAst.Coercion (loc, UriManager.uri_of_string suri, true, arity)
     | IDENT "record" ; (params,name,ty,fields) = record_spec ->
         GrafiteAst.Obj (loc, Ast.Record (params,name,ty,fields))
     | IDENT "default" ; what = QSTRING ; uris = LIST1 URI ->