generate HTML templates using XSLT starting from a bunch of .src files

[helm.git] / helm / ocaml / cic_disambiguation / cicTextualParser2.ml

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 452593005d99f62d8f395001976e424349130025..d5f427c4f92f039367f722eceb4abf3bb0ce6b68 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -23,7 +23,7 @@
  * http://helm.cs.unibo.it/
  *)
 
-let debug = true
+let debug = false
 let debug_print s =
   if debug then begin
     prerr_endline "<NEW_TEXTUAL_PARSER>";
@@ -35,12 +35,17 @@ let debug_print s =
   * thus be interpreted differently than others *)
 let use_fresh_num_instances = false
 
+  (** does the lexer return COMMENT tokens? *)
+let return_comments = false
+
 open Printf
 
 open DisambiguateTypes
 
 exception Parse_error of Token.flocation * string
 
+let cic_lexer = CicTextualLexer2.cic_lexer ~comments:return_comments ()
+
 let fresh_num_instance =
   let n = ref 0 in
   if use_fresh_num_instances then
@@ -52,7 +57,7 @@ let choice_of_uri uri =
   let term = CicUtil.term_of_uri uri in
   (uri, (fun _ _ _ -> term))
 
-let grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
+let grammar = Grammar.gcreate cic_lexer
 
 let term = Grammar.Entry.create grammar "term"
 let term0 = Grammar.Entry.create grammar "term0"
@@ -156,27 +161,34 @@ EXTEND
   ];
   let_defs:[
     [ defs = LIST1 [
-        var = typed_name;
+        name = IDENT;
         args = LIST1 [
           PAREN "(" ; names = LIST1 IDENT SEP SYMBOL ","; SYMBOL ":";
           ty = term; PAREN ")" ->
             (names, ty)
         ];
         index_name = OPT [ IDENT "on"; idx = IDENT -> idx ];
+        ty = OPT [ SYMBOL ":" ; t = term -> t ];
         SYMBOL <:unicode<def>> (* ≝ *);
         t1 = term ->
-          let rec list_of_lambda ty final_term = function
+          let rec list_of_binder binder ty final_term = function
             | [] -> final_term
             | name::tl -> 
-                CicAst.Binder (`Lambda, (Cic.Name name, Some ty), 
-                  list_of_lambda ty final_term tl)
+                CicAst.Binder (binder, (Cic.Name name, Some ty), 
+                  list_of_binder binder ty final_term tl)
           in
-          let rec lambda_of_arg_list final_term = function
+          let rec binder_of_arg_list binder final_term = function
             | [] -> final_term
             | (l,ty)::tl ->  
-                list_of_lambda ty (lambda_of_arg_list final_term tl) l
+                list_of_binder binder ty 
+                  (binder_of_arg_list binder final_term tl) l
+          in
+          let t1' = binder_of_arg_list `Lambda t1 args in
+          let ty' = 
+            match ty with 
+            | None -> None
+            | Some ty -> Some (binder_of_arg_list `Pi ty args)
           in
-          let t1' = lambda_of_arg_list t1 args in
           let rec get_position_of name n = function 
             | [] -> (None,n)
             | nam::tl -> 
@@ -198,7 +210,7 @@ EXTEND
              | None -> 0 
              | (Some name) -> find_arg name 0 args)
           in
-          (var, t1', index)
+          ((Cic.Name name,ty'), t1', index)
       ] SEP "and" -> defs
     ]];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
@@ -351,7 +363,7 @@ EXTEND
         let idents = match idents with None -> [] | Some idents -> idents in
         return_tactic loc (TacticAst.Intros (num, idents))
     | [ IDENT "intro" | IDENT "Intro" ] ->
-        return_tactic loc (TacticAst.Intros (Some 1, []))
+        return_tactic loc (TacticAst.Intros (None, []))
     | [ IDENT "left" | IDENT "Left" ] -> return_tactic loc TacticAst.Left
     | [ "let" | "Let" ];
       t = tactic_term; "in"; where = IDENT ->
@@ -393,7 +405,9 @@ EXTEND
       [ cmd = command -> return_tactical loc (TacticAst.Command cmd) ]
     | "sequence" LEFTA
       [ tactics = LIST1 NEXT SEP SYMBOL ";" ->
-          return_tactical loc (TacticAst.Seq tactics)
+          (match tactics with
+          | [tactic] -> tactic
+          | _ -> return_tactical loc (TacticAst.Seq tactics))
       ]
     | "then" NONA
       [ tac = tactical;
@@ -452,6 +466,8 @@ EXTEND
   print_kind: [
     [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
       -> `Env
+    | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
+      -> `Coer
   ] ];
 
   command: [
@@ -504,6 +520,8 @@ EXTEND
         return_command loc (TacticAst.Redo (int_opt steps))
     | [ IDENT "baseuri"   | IDENT "Baseuri" ]; uri = OPT QSTRING ->
         return_command loc (TacticAst.Baseuri uri)
+    | [ IDENT "basedir"   | IDENT "Basedir" ]; uri = OPT QSTRING ->
+        return_command loc (TacticAst.Basedir uri)
     | [ IDENT "check"   | IDENT "Check" ]; t = term ->
         return_command loc (TacticAst.Check t)
 (*
@@ -514,7 +532,7 @@ EXTEND
   ];
   script_entry: [
     [ cmd = tactical0 -> Command cmd
-    | s = COMMENT -> Comment (loc, s)
+(*     | s = COMMENT -> Comment (loc, s) *)
     ]
   ];
   script: [ [ entries = LIST0 script_entry; EOI -> (loc, entries) ] ];
@@ -548,7 +566,7 @@ module EnvironmentP3 =
 
     let empty = ""
 
-    let aliases_grammar = Grammar.gcreate CicTextualLexer2.cic_lexer
+    let aliases_grammar = Grammar.gcreate cic_lexer
     let aliases = Grammar.Entry.create aliases_grammar "aliases"
 
     let to_string env =