X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FcicTextualParser2.ml;h=e35101862cb0c6137fa0b6f69b3b12a1be8019ff;hb=c66e9d17eda5e5defcb363e42d891d2b407cf7c3;hp=478e97d390531fe2df2e77f29570a0e0c17455cb;hpb=10be6b9fb25a5bcd8721f707beba4b8a125591b5;p=helm.git

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 478e97d39..e35101862 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -75,6 +75,10 @@ let name_of_string = function
   | "_" -> Cic.Anonymous
   | s -> Cic.Name s
 
+let string_of_name = function
+  | Cic.Anonymous -> "_"
+  | Cic.Name s -> s
+  
 let int_opt = function
   | None -> None
   | Some lexeme -> Some (int_of_string lexeme)
@@ -120,8 +124,8 @@ EXTEND
   ];
   typed_name: [
     [ PAREN "("; i = IDENT; SYMBOL ":"; typ = term; PAREN ")" ->
-        (name_of_string i, Some typ)
-    | i = IDENT -> (name_of_string i, None)
+        (Cic.Name i, Some typ)
+    | i = IDENT -> (Cic.Name i, None)
     ]
   ];
   subst: [
@@ -150,25 +154,70 @@ EXTEND
         (head, vars)
     ]
   ];
+  let_defs:[
+    [ defs = LIST1 [
+        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_binder binder ty final_term = function
+            | [] -> final_term
+            | name::tl -> 
+                CicAst.Binder (binder, (Cic.Name name, Some ty), 
+                  list_of_binder binder ty final_term tl)
+          in
+          let rec binder_of_arg_list binder final_term = function
+            | [] -> final_term
+            | (l,ty)::tl ->  
+                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 rec get_position_of name n = function 
+            | [] -> (None,n)
+            | nam::tl -> 
+                if nam = name then 
+                  (Some n,n) 
+                else 
+                  (get_position_of name (n+1) tl)
+          in
+          let rec find_arg name n = function 
+            | [] -> (fail loc (sprintf "Argument %s not found" name))
+            | (l,_)::tl -> 
+                let (got,len) = get_position_of name 0 l in
+                (match got with 
+                | None -> (find_arg name (n+len) tl)
+                | Some where -> n + where)
+          in
+          let index = 
+            (match index_name with 
+             | None -> 0 
+             | (Some name) -> find_arg name 0 args)
+          in
+          ((Cic.Name name,ty'), t1', index)
+      ] SEP "and" -> defs
+    ]];
   constructor: [ [ name = IDENT; SYMBOL ":"; typ = term -> (name, typ) ] ];
   term0: [ [ t = term; EOI -> return_term loc t ] ];
   term:
     [ "letin" NONA
       [ "let"; var = typed_name;
-        SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
+        SYMBOL <:unicode<def>> (* ≝ *);
         t1 = term; "in"; t2 = term ->
           return_term loc (CicAst.LetIn (var, t1, t2))
       | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
-          defs = LIST1 [
-            var = typed_name;
-            index = OPT [ PAREN "("; index = NUM; PAREN ")" ->
-              int_of_string index
-            ];
-            SYMBOL "="; (* SYMBOL <:unicode<def>> (* ≝ *); *)
-            t1 = term ->
-              (var, t1, (match index with None -> 0 | Some i -> i))
-          ] SEP "and";
-          "in"; body = term ->
+        defs = let_defs; "in"; body = term ->
             return_term loc (CicAst.LetRec (ind_kind, defs, body))
       ]
     | "binder" RIGHTA
@@ -235,7 +284,8 @@ EXTEND
         "with";
         PAREN "[";
         patterns = LIST0 [
-          lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term ->
+          lhs = pattern; SYMBOL <:unicode<Rightarrow>> (* ⇒ *); rhs = term
+          ->
             ((lhs: CicAst.case_pattern), rhs)
         ] SEP SYMBOL "|";
         PAREN "]" ->
@@ -406,17 +456,40 @@ EXTEND
       let ind_types = fst_ind_type :: tl_ind_types in
       (params, ind_types)
   ] ];
+  print_kind: [
+    [ [ IDENT "Env" | IDENT "env" | IDENT "Environment" | IDENT "environment" ]
+      -> `Env
+    | [ IDENT "Coer" | IDENT "coer" | IDENT "Coercions" | IDENT "coercions" ]
+      -> `Coer
+  ] ];
+
   command: [
     [ [ IDENT "abort" | IDENT "Abort" ] -> return_command loc TacticAst.Abort
     | [ IDENT "proof" | IDENT "Proof" ] -> return_command loc TacticAst.Proof
     | [ IDENT "quit"  | IDENT "Quit"  ] -> return_command loc TacticAst.Quit
     | [ IDENT "qed"   | IDENT "Qed"   ] ->
         return_command loc (TacticAst.Qed None)
+    | [ IDENT "print"   | IDENT "Print" ];
+      print_kind = print_kind ->
+            return_command loc (TacticAst.Print print_kind)
     | [ IDENT "save"  | IDENT "Save"  ]; name = IDENT ->
         return_command loc (TacticAst.Qed (Some name))
     | flavour = theorem_flavour; name = OPT IDENT; SYMBOL ":"; typ = term;
       body = OPT [ SYMBOL <:unicode<def>> (* ≝ *); body = term -> body ] ->
         return_command loc (TacticAst.Theorem (flavour, name, typ, body))
+    | "let"; ind_kind = [ "corec" -> `CoInductive | "rec"-> `Inductive ];
+        defs = let_defs -> 
+          let name,ty = 
+            match defs with
+            | ((Cic.Name name,Some ty),_,_) :: _ -> name,ty
+            | ((Cic.Name name,None),_,_) :: _ -> 
+                fail loc ("No type given for " ^ name)
+            | _ -> assert false 
+          in
+          let body = CicAst.Ident (name,None) in
+          TacticAst.Theorem(`Definition, Some name, ty,
+            Some (CicAst.LetRec (ind_kind, defs, body)))
+          
     | [ IDENT "inductive" | IDENT "Inductive" ]; spec = inductive_spec ->
         let (params, ind_types) = spec in
         return_command loc (TacticAst.Inductive (params, ind_types))
@@ -440,6 +513,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)
 (*