X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Fgrafite_parser%2FgrafiteParser.ml;h=b2fb3616f6cc216866dd7a446b614e27ca7dd39c;hb=6a25db65c9a787daf7344e3b166b2d798b1ff1a5;hp=9373e54b43a1de051f743a2581220677abaf4df8;hpb=2499f5fdcf4dbfecc6f4fafe925b24ae76f14be8;p=helm.git

diff --git a/components/grafite_parser/grafiteParser.ml b/components/grafite_parser/grafiteParser.ml
index 9373e54b4..b2fb3616f 100644
--- a/components/grafite_parser/grafiteParser.ml
+++ b/components/grafite_parser/grafiteParser.ml
@@ -35,7 +35,8 @@ type 'a localized_option =
 
 type ast_statement =
   (CicNotationPt.term, CicNotationPt.term,
-   CicNotationPt.term GrafiteAst.reduction, CicNotationPt.obj, string)
+   CicNotationPt.term GrafiteAst.reduction, 
+   CicNotationPt.term CicNotationPt.obj, string)
     GrafiteAst.statement
 
 type statement =
@@ -55,18 +56,12 @@ let default_associativity = Gramext.NonA
 
 type by_continuation =
    BYC_done
- | BYC_weproved of CicNotationPt.term * string * CicNotationPt.term option
+ | BYC_weproved of CicNotationPt.term * string option * 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: [
-   [ LPAREN; names = LIST1 IDENT SEP SYMBOL ",";
-      SYMBOL ":"; ty = term; RPAREN -> names,ty
-   | name = IDENT -> [name],Ast.Implicit
-   ]
-  ];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   tactic_term: [ [ t = term LEVEL "90N" -> t ] ];
   ident_list0: [ [ LPAREN; idents = LIST0 IDENT; RPAREN -> idents ] ];
@@ -121,9 +116,15 @@ EXTEND
     | SYMBOL "<" -> `RightToLeft ]
   ];
   int: [ [ num = NUMBER -> int_of_string num ] ];
+  intros_names: [
+   [ idents = OPT ident_list0 ->
+      match idents with None -> [] | Some idents -> idents
+   ]
+  ];
   intros_spec: [
-    [ num = OPT [ num = int -> num ]; idents = OPT ident_list0 ->
-        let idents = match idents with None -> [] | Some idents -> idents in
+    [ OPT [ IDENT "names" ]; 
+      num = OPT [ num = int -> num ]; 
+      idents = intros_names ->
         num, idents
     ]
   ];
@@ -133,14 +134,17 @@ EXTEND
         GrafiteAst.Absurd (loc, t)
     | IDENT "apply"; t = tactic_term ->
         GrafiteAst.Apply (loc, t)
-    | IDENT "applyS"; t = tactic_term ->
-        GrafiteAst.ApplyS (loc, t)
-    | IDENT "assumption" ->
-        GrafiteAst.Assumption loc
-    | IDENT "auto"; params = 
+    | IDENT "applyS"; t = tactic_term ; params = 
         LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
           string_of_int v | v = IDENT -> v ] -> i,v ] ->
+        GrafiteAst.ApplyS (loc, t, params)
+    | IDENT "assumption" ->
+        GrafiteAst.Assumption loc
+    | IDENT "auto"; params = auto_params ->
         GrafiteAst.Auto (loc,params)
+    | IDENT "cases"; what = tactic_term;
+      (num, idents) = intros_spec ->
+	GrafiteAst.Cases (loc, what, idents)
     | IDENT "clear"; ids = LIST1 IDENT ->
         GrafiteAst.Clear (loc, ids)
     | IDENT "clearbody"; id = IDENT ->
@@ -160,8 +164,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 +195,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)
@@ -265,7 +267,7 @@ EXTEND
 		  (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']->
+    | IDENT "we" ; IDENT "need" ; "to" ; IDENT "prove" ; t = tactic_term ; id = OPT [ LPAREN ; id = IDENT ; RPAREN -> id ] ; 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)
@@ -276,27 +278,39 @@ 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 -> 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  ->
+    | 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)
   ]
+];
+  auto_params: [
+   [ params =
+      LIST0 [ i = IDENT -> i,"" | i = IDENT ; SYMBOL "="; v = [ v = int ->
+       string_of_int v | v = IDENT -> v ] -> i,v ] ->
+      params
+   ]
+];
+  auto_params': [
+   [ LPAREN; params = auto_params; RPAREN -> params
+   | -> []
+   ]
 ];
   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 "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,Some id,t1)
+    | IDENT "we" ; IDENT "proved" ; ty = tactic_term ; t1 = OPT [IDENT "that" ; IDENT "is" ; IDENT "equivalent" ; "to" ; t2 = tactic_term -> t2] ; 
+            IDENT "done" -> BYC_weproved (ty,None,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)
+      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
+    [ IDENT "done" -> true
+    | -> false
     ]
 ];
   atomic_tactical:
@@ -360,7 +374,7 @@ EXTEND
     ]
   ];
   inductive_spec: [ [
-    fst_name = IDENT; params = LIST0 [ arg=arg -> arg ];
+    fst_name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars;
     SYMBOL ":"; fst_typ = term; SYMBOL <:unicode<def>>; OPT SYMBOL "|";
     fst_constructors = LIST0 constructor SEP SYMBOL "|";
     tl = OPT [ "with";
@@ -382,7 +396,7 @@ EXTEND
   ] ];
   
   record_spec: [ [
-    name = IDENT; params = LIST0 [ arg = arg -> arg ] ;
+    name = IDENT; params = LIST0 CicNotationParser.protected_binder_vars ;
      SYMBOL ":"; typ = term; SYMBOL <:unicode<def>>; SYMBOL "{" ; 
      fields = LIST0 [ 
        name = IDENT ; 
@@ -407,6 +421,15 @@ EXTEND
   macro: [
     [ [ IDENT "check"   ]; t = term ->
         GrafiteAst.Check (loc, t)
+    | [ IDENT "inline"]; 
+        style = OPT [ IDENT "procedural" ];
+	suri = QSTRING; prefix = OPT QSTRING ->
+         let style = match style with 
+	    | None   -> GrafiteAst.Declarative
+	    | Some _ -> GrafiteAst.Procedural
+	 in
+	 let prefix = match prefix with None -> "" | Some prefix -> prefix in
+	 GrafiteAst.Inline (loc,style,suri,prefix)
     | [ IDENT "hint" ] -> GrafiteAst.Hint loc
     | [ IDENT "whelp"; "match" ] ; t = term -> 
         GrafiteAst.WMatch (loc,t)
@@ -549,8 +572,14 @@ EXTEND
         defs = CicNotationParser.let_defs -> 
           let name,ty = 
             match defs with
-            | ((Ast.Ident (name, None), Some ty),_,_) :: _ -> name,ty
-            | ((Ast.Ident (name, None), None),_,_) :: _ ->
+            | (params,(Ast.Ident (name, None), Some ty),_,_) :: _ ->
+                let ty =
+                 List.fold_right
+                  (fun var ty -> Ast.Binder (`Pi,var,ty)
+                  ) params ty
+                in
+                 name,ty
+            | (_,(Ast.Ident (name, None), None),_,_) :: _ ->
                 name, Ast.Implicit
             | _ -> assert false 
           in
@@ -575,6 +604,15 @@ EXTEND
     | 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 ->