X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=6e368d79bdbb13fd0ab4fbf7171fa765c96a057c;hb=8caaccfeb66f6a507e5fb3b4b221a360eb5428c8;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..6e368d79b 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
@@ -278,6 +279,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 "]" ->
@@ -321,7 +323,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,7 +375,7 @@ 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 ->
@@ -388,6 +391,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 +473,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 +495,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 ->
@@ -586,6 +592,10 @@ EXTEND
     | com = comment -> TacticAst.Comment (loc, com)
     ]
   ];
+  statements: [
+    [ l = LIST0 [ statement ] -> l 
+    ]  
+  ];
 END
 
 let exc_located_wrapper f =
@@ -601,6 +611,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))
+  
 
 (**/**)