From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 31 Jan 2005 17:17:32 +0000 (+0000)
Subject: added basedir and improved let{rec} syntax
X-Git-Tag: V_0_1_0~84
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=422735774bab813a8a9a4efb185a4cac268cb723;p=helm.git

added basedir and improved let{rec} syntax
---

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index 452593005..d062ed109 100644
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -156,27 +156,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 +205,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) ] ];
@@ -504,6 +511,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)
 (*