X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=9f65555a4e80c8dc999fad607b484d55df5ef9cb;hb=bb49c457d64878ed9611656f620548b5151e5dbd;hp=bfc535a3c35f59b204ccd8d7706d7df3fb15d8af;hpb=17c5ad881e737bd2cba2e157f346a618fce87204;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index bfc535a3c..9f65555a4 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -69,6 +69,7 @@ let alias_spec = Grammar.Entry.create grammar "alias_spec"
 let macro = Grammar.Entry.create grammar "macro"
 let script = Grammar.Entry.create grammar "script"
 let statement = Grammar.Entry.create grammar "statement"
+let statements = Grammar.Entry.create grammar "statements"
 
 let return_term loc term = CicAst.AttributedTerm (`Loc loc, term)
 
@@ -116,7 +117,7 @@ let mk_binder_ast binder typ vars body =
     vars body
 
 EXTEND
-  GLOBAL: term term0 statement;
+  GLOBAL: term term0 statement statements;
   int: [
     [ num = NUM ->
         try
@@ -174,9 +175,10 @@ EXTEND
     [ defs = LIST1 [
         name = IDENT;
         args = LIST1 [
-          PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
-          ty = term; PAREN ")" ->
-            (names, ty)
+            PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ",";
+            SYMBOL ":"; ty = term; PAREN ")" ->
+              (names, Some ty)
+          | name = IDENT -> [name],None
         ];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
         ty = OPT [ SYMBOL ":" ; t = term -> t ];
@@ -194,6 +196,12 @@ EXTEND
                 list_of_binder binder ty 
                   (binder_of_arg_list binder final_term tl) l
           in
+          let args = 
+           List.map
+            (function
+                names,Some ty -> names,ty
+              | names,None -> names,CicAst.Implicit
+            ) args in
           let t1' = binder_of_arg_list `Lambda t1 args in
           let ty' = 
             match ty with 
@@ -278,6 +286,7 @@ EXTEND
       | n = substituted_name -> return_term loc n
       | i = NUM -> return_term loc (CicAst.Num (i, (fresh_num_instance ())))
       | IMPLICIT -> return_term loc CicAst.Implicit
+      | PLACEHOLDER -> return_term loc CicAst.UserInput
       | m = META;
         substs = [
           PAREN "["; substs = LIST0 meta_subst SEP SYMBOL ";" ; PAREN "]" ->
@@ -292,7 +301,7 @@ EXTEND
             return_term loc (CicAst.Meta (index, substs))
       | outtyp = OPT [ PAREN "["; typ = term; PAREN "]" -> typ ];
         "match"; t = term;
-        indty_ident = OPT [ SYMBOL ":"; id = IDENT -> id ];
+        indty_ident = OPT ["in" ; id = IDENT -> id ];
         "with";
         PAREN "[";
         patterns = LIST0 [
@@ -321,7 +330,8 @@ EXTEND
   reduction_kind: [
     [ [ IDENT "reduce" ] -> `Reduce
     | [ IDENT "simplify" ] -> `Simpl
-    | [ IDENT "whd" ] -> `Whd ]
+    | [ IDENT "whd" ] -> `Whd 
+    | [ IDENT "normalize" ] -> `Normalize ]
   ];
   tactic: [
     [ [ IDENT "absurd" ]; t = tactic_term ->
@@ -372,10 +382,10 @@ EXTEND
         let idents = match idents with None -> [] | Some idents -> idents in
         TacticAst.Intros (loc, num, idents)
     | [ IDENT "intro" ] ->
-        TacticAst.Intros (loc, None, [])
+        TacticAst.Intros (loc, Some 1, [])
     | [ IDENT "left" ] -> TacticAst.Left loc
-    | [ "let" | "Let" ];
-      t = tactic_term; "in"; where = IDENT ->
+    | [ IDENT "letin" ];
+       where = IDENT ; SYMBOL <:unicode<def>> ; t = tactic_term ->
         TacticAst.LetIn (loc, t, where)
     | kind = reduction_kind;
       pat = OPT [
@@ -388,6 +398,8 @@ EXTEND
         | None, terms -> TacticAst.Reduce (loc, kind, Some (terms, `Goal))
         | Some pat, [] -> fail loc "Missing term [list]"
         | Some pat, terms -> TacticAst.Reduce (loc, kind, Some (terms, pat)))
+    | kind = reduction_kind; where = IDENT ; IDENT "at" ; pat = term ->
+        TacticAst.ReduceAt (loc, kind, where, pat)
     | [ IDENT "reflexivity" ] ->
         TacticAst.Reflexivity loc
     | [ IDENT "replace" ];
@@ -468,14 +480,14 @@ EXTEND
       (params, ind_types)
   ] ];
 
-  macro: [[
-      [ IDENT "abort" ] -> TacticAst.Abort loc
-    | [ IDENT "quit"  ] -> TacticAst.Quit loc
+  macro: [
+    [ [ IDENT "quit"  ] -> TacticAst.Quit loc
+(*     | [ IDENT "abort" ] -> TacticAst.Abort loc *)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
-    | [ IDENT "undo"   ]; steps = OPT NUM ->
+(*     | [ IDENT "undo"   ]; steps = OPT NUM ->
         TacticAst.Undo (loc, int_opt steps)
     | [ IDENT "redo"   ]; steps = OPT NUM ->
-        TacticAst.Redo (loc, int_opt steps)
+        TacticAst.Redo (loc, int_opt steps) *)
     | [ IDENT "check"   ]; t = term ->
         TacticAst.Check (loc, t)
     | [ IDENT "hint" ] -> TacticAst.Hint loc
@@ -490,7 +502,8 @@ EXTEND
     | [ IDENT "whelp"; IDENT "hint" ] ; t = term -> 
         TacticAst.WHint (loc,t)
     | [ IDENT "print" ]; name = QSTRING -> TacticAst.Print (loc, name)
-  ]];
+    ]
+  ];
 
   alias_spec: [
     [ IDENT "id"; id = QSTRING; SYMBOL "="; uri = QSTRING ->
@@ -540,8 +553,7 @@ EXTEND
           let name,ty = 
             match defs with
             | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
-            | ((Cic.Name name,None),_,_) :: _ -> 
-                fail loc ("No type given for " ^ name)
+            | ((Cic.Name name,None),_,_) :: _ -> name,CicAst.Implicit
             | _ -> assert false 
           in
           let body = CicAst.Ident (name,None) in
@@ -586,6 +598,10 @@ EXTEND
     | com = comment -> TacticAst.Comment (loc, com)
     ]
   ];
+  statements: [
+    [ l = LIST0 [ statement ] -> l 
+    ]  
+  ];
 END
 
 let exc_located_wrapper f =
@@ -601,6 +617,9 @@ let parse_term stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse term0 stream))
 let parse_statement stream =
   exc_located_wrapper (fun () -> (Grammar.Entry.parse statement stream))
+let parse_statements stream =
+  exc_located_wrapper (fun () -> (Grammar.Entry.parse statements stream))
+  
 
 (**/**)