Big change: parenthesis can now be put in any place to disambiguate the

[helm.git] / helm / ocaml / cic_textual_parser / cicTextualParser.mly

diff --git a/helm/ocaml/cic_textual_parser/cicTextualParser.mly b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
index 1d4bd933d151f9a7b8ad7ba8a79dc45eca3a8275..5afd56ed9d75e29110c85f12a496b8148e4e8fae 100644 (file)
--- a/helm/ocaml/cic_textual_parser/cicTextualParser.mly
+++ b/helm/ocaml/cic_textual_parser/cicTextualParser.mly
@@ -119,17 +119,33 @@
  ;;
 
  let var_uri_of_id id interp =
-  match interp id with
-     None -> raise (UnknownIdentifier id)
-   | Some (CicTextualParser0.VarUri uri) -> uri
-   | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
+  let module CTP0 = CicTextualParser0 in
+   match interp id with
+      None -> raise (UnknownIdentifier id)
+    | Some (CTP0.Uri (CTP0.VarUri uri)) -> uri
+    | Some _ -> raise TheLeftHandSideOfAnExplicitNamedSubstitutionMustBeAVariable
  ;;
 
  let indty_uri_of_id id interp =
-  match interp id with
-     None -> raise (UnknownIdentifier id)
-   | Some (CicTextualParser0.IndTyUri (uri,tyno)) -> (uri,tyno)
-   | Some _ -> raise InductiveTypeURIExpected
+  let module CTP0 = CicTextualParser0 in
+   match interp id with
+      None -> raise (UnknownIdentifier id)
+    | Some (CTP0.Uri (CTP0.IndTyUri (uri,tyno))) -> (uri,tyno)
+    | Some _ -> raise InductiveTypeURIExpected
+ ;;
+
+ let mk_implicit () =
+  let newmeta = new_meta () in
+   let new_canonical_context = [] in
+    let irl =
+     identity_relocation_list_for_metavariable new_canonical_context
+    in
+     CicTextualParser0.metasenv :=
+      [newmeta, new_canonical_context, Sort Type ;
+       newmeta+1, new_canonical_context, Meta (newmeta,irl);
+       newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
+      ] @ !CicTextualParser0.metasenv ;
+     [], function _ -> Meta (newmeta+2,irl)
  ;;
 %}
 %token <string> ID
@@ -139,15 +155,18 @@
 %token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
-%token ALIAS
 %token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %right ARROW
 %start main
-%type <string list * ((string -> CicTextualParser0.uri option) -> Cic.term)> main
+%type <string list * ((string -> CicTextualParser0.interp_codomain option) -> Cic.term)> main
 %%
 main:
- expr EOF { $1 }
+ | EOF { raise CicTextualParser0.Eof } /* FG: was never raised */
+ | expr EOF { $1 }
+ | expr SEMICOLON { $1 } /*  FG: to read several terms in a row
+                          *  Do we need to clear some static variables? 
+                         */
 ;
 expr2:
    CONURI exp_named_subst
@@ -183,7 +202,11 @@ expr2:
           function interp ->
            match interp $1 with
              None  -> raise (UnknownIdentifier $1)
-           | Some uri -> term_of_uri uri (mk_exp_named_subst interp)
+           | Some (CicTextualParser0.Uri uri) ->
+               term_of_uri uri (mk_exp_named_subst interp)
+            | Some CicTextualParser0.Implicit ->
+               (*CSC: not very clean; to maximize code reusage *)
+               snd (mk_implicit ()) ""
    }
  | CASE LPAREN expr COLON INDTYURI SEMICOLON expr RPAREN LCURLY branches RCURLY
     { let dom1,mk_expr1 = $3 in
@@ -260,18 +283,7 @@ expr2:
              CoFix (idx,fixfuns)
     }
  | IMPLICIT
-    { let newmeta = new_meta () in
-       let new_canonical_context = [] in
-        let irl =
-         identity_relocation_list_for_metavariable new_canonical_context
-        in
-         CicTextualParser0.metasenv :=
-          [newmeta, new_canonical_context, Sort Type ;
-           newmeta+1, new_canonical_context, Meta (newmeta,irl);
-           newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
-          ] @ !CicTextualParser0.metasenv ;
-         [], function _ -> Meta (newmeta+2,irl)
-    }
+    { mk_implicit () }
  | SET  { [], function _ -> Sort Set }
  | PROP { [], function _ -> Sort Prop }
  | TYPE { [], function _ -> Sort Type }
@@ -285,14 +297,16 @@ expr2:
     { let dom,mk_substitutionlist = $3 in
        dom, function interp -> Meta ($1, mk_substitutionlist interp)
     } 
- | LPAREN expr expr exprlist RPAREN
-    { let dom1,mk_expr1 = $2 in
-      let dom2,mk_expr2 = $3 in
-      let dom3,mk_exprlist = $4 in
-       let dom = union dom1 (union dom2 dom3) in
-        dom,
-         function interp ->
-          Appl ([mk_expr1 interp ; mk_expr2 interp]@(mk_exprlist interp))
+ | LPAREN expr exprlist RPAREN
+    { let length,dom2,mk_exprlist = $3 in
+       match length with
+          0 -> $2
+        | _ ->
+          let dom1,mk_expr1 = $2 in
+           let dom = union dom1 dom2 in
+            dom,
+             function interp ->
+              Appl ((mk_expr1 interp)::(mk_exprlist interp))
     }
 ;
 exp_named_subst :
@@ -405,11 +419,6 @@ pihead:
      let dom,mk_expr = $1 in
       Anonymous, (dom, function interp -> mk_expr interp)
    }
- | LPAREN expr RPAREN ARROW
-   { CicTextualParser0.binders := (Some Anonymous)::!CicTextualParser0.binders ;
-     let dom,mk_expr = $2 in
-      Anonymous, (dom, function interp -> mk_expr interp)
-   }
  | PROD ID DOT
     { CicTextualParser0.binders := (Some (Name $2))::!CicTextualParser0.binders;
       let newmeta = new_meta () in
@@ -466,12 +475,12 @@ branches:
 ;
 exprlist:
     
-    { [], function _ -> [] }
+    { 0, [], function _ -> [] }
  | expr exprlist
     { let dom1,mk_expr = $1 in
-      let dom2,mk_exprlist = $2 in
+      let length,dom2,mk_exprlist = $2 in
        let dom = union dom1 dom2 in
-        dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
+        length+1, dom, function interp -> (mk_expr interp)::(mk_exprlist interp)
     }
 ;
 exprseplist: