X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=19f9e359e85aff4844fc66a3f00812f0e864acf7;hb=59895ae358dff2a57a9fd1ea6924690a0862e036;hp=1eb2a495d4624bed0709830af6386c4a25e5ec10;hpb=36243ef64310a9ea2e51a0295744ab5de7abe055;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 1eb2a495d..19f9e359e 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -160,8 +160,8 @@ EXTEND
 	let to_spec id = GrafiteAst.Ident id in
 	GrafiteAst.Decompose (loc, List.rev_map to_spec types, what, idents)
     | IDENT "demodulate" -> GrafiteAst.Demodulate loc
-    | IDENT "discriminate"; t = tactic_term ->
-        GrafiteAst.Discriminate (loc, t)
+    | IDENT "destruct"; t = tactic_term ->
+        GrafiteAst.Destruct (loc, t)
     | IDENT "elim"; what = tactic_term; using = using;
       (num, idents) = intros_spec ->
 	GrafiteAst.Elim (loc, what, using, num, idents)
@@ -191,8 +191,6 @@ EXTEND
     | IDENT "goal"; n = int ->
         GrafiteAst.Goal (loc, n)
     | IDENT "id" -> GrafiteAst.IdTac loc
-    | IDENT "injection"; t = tactic_term ->
-        GrafiteAst.Injection (loc, t)
     | IDENT "intro"; ident = OPT IDENT ->
         let idents = match ident with None -> [] | Some id -> [id] in
         GrafiteAst.Intros (loc, Some 1, idents)
@@ -233,6 +231,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 ->
@@ -240,7 +240,7 @@ 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 ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to " ; t' = tactic_term -> 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 ->
@@ -325,6 +325,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)
       ]
@@ -383,8 +384,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
@@ -558,13 +565,23 @@ 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 ->
        let uris = List.map UriManager.uri_of_string uris in
         GrafiteAst.Default (loc,what,uris)
+    | IDENT "relation" ; aeq = tactic_term ; "on" ; a = tactic_term ;
+      refl = OPT [ IDENT "reflexivity" ; IDENT "proved" ; IDENT "by" ;
+                   refl = tactic_term -> refl ] ;
+      sym = OPT [ IDENT "symmetry" ; IDENT "proved" ; IDENT "by" ;
+                   sym = tactic_term -> sym ] ;
+      trans = OPT [ IDENT "transitivity" ; IDENT "proved" ; IDENT "by" ;
+                   trans = tactic_term -> trans ] ;
+      "as" ; id = IDENT ->
+       GrafiteAst.Relation (loc,id,a,aeq,refl,sym,trans)
   ]];
   lexicon_command: [ [
       IDENT "alias" ; spec = alias_spec ->