Universes introduction

[helm.git] / helm / ocaml / tex_cic_textual_parser / texCicTextualParser.mly

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index e26145e2855ba815dd03c1814750642ce40779aa..41a36acc6ae7e3f624905f50c15c1ceba12936d4 100644 (file)
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -136,12 +136,14 @@
 
  let mk_implicit () =
   let newmeta = new_meta () in
+  let newuniv = CicUniv.fresh () in
    let new_canonical_context = [] in
     let irl =
      identity_relocation_list_for_metavariable new_canonical_context
     in
      TexCicTextualParser0.metasenv :=
-      [newmeta, new_canonical_context, Sort Type ;
+      [newmeta, new_canonical_context, Sort (Type newuniv);
+       (* TASSI: ?? *)
        newmeta+1, new_canonical_context, Meta (newmeta,irl);
        newmeta+2, new_canonical_context, Meta (newmeta+1,irl)
       ] @ !TexCicTextualParser0.metasenv ;
@@ -151,18 +153,20 @@
 %token <string> ID
 %token <int> META
 %token <int> NUM
+%token <int> RNUM
 %token <UriManager.uri> CONURI
 %token <UriManager.uri> VARURI
 %token <UriManager.uri * int> INDTYURI
 %token <UriManager.uri * int * int> INDCONURI
-%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CAST IMPLICIT NONE
+%token LPAREN RPAREN PROD LAMBDA COLON DOT SET PROP TYPE CPROP CAST IMPLICIT NONE
 %token LETIN FIX COFIX SEMICOLON LCURLY RCURLY CASE ARROW LBRACKET RBRACKET EOF
 %token DOLLAR
-%token PLUS MINUS TIMES EQ
+%token RPLUS RMINUS RTIMES RDIV
+%token PLUS MINUS TIMES EQT EQ NEQT
 %right ARROW
-%right EQ
-%right PLUS MINUS
-%right TIMES
+%nonassoc EQ EQT NEQT
+%left PLUS MINUS RPLUS RMINUS
+%left TIMES RTIMES RDIV
 %start main
 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
 %%
@@ -178,32 +182,87 @@ main:
                          */
 ;
 expr2:
-   NUM
+ | RNUM
+   { [], function interp ->
+      let rec cic_real_of_real =
+       function
+          0 -> Cic.Const (HelmLibraryObjects.Reals.r0_URI, [])
+        | 1 -> Cic.Const (HelmLibraryObjects.Reals.r1_URI,[])
+        | n ->
+          Cic.Appl
+           [ Cic.Const
+               (HelmLibraryObjects.Reals.rplus_URI,[]) ;
+             Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);
+             cic_real_of_real (n - 1)
+           ]
+      in
+       cic_real_of_real $1
+   }
+ | NUM
    { [], function interp ->
       let rec cic_int_of_int =
        function
           0 ->
-           Cic.MutConstruct
-            (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
-             0,1,[])
+           Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,1,[])
         | n ->
           Cic.Appl
-           [ Cic.MutConstruct
-              (UriManager.uri_of_string "cic:/Coq/Init/Datatypes/nat.ind",
-               0,2,[]) ;
+           [ Cic.MutConstruct (HelmLibraryObjects.Datatypes.nat_URI,0,2,[]) ;
              cic_int_of_int (n - 1)
            ]
       in
        cic_int_of_int $1
    }
+ | expr2 RPLUS expr2
+   { let dom1,mk_expr1 = $1 in
+     let dom2,mk_expr2 = $3 in
+      let dom = union dom1 dom2 in
+       dom, function interp ->
+        Cic.Appl
+         [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ;
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
+ | expr2 RMINUS expr2
+   { let dom1,mk_expr1 = $1 in
+     let dom2,mk_expr2 = $3 in
+      let dom = union dom1 dom2 in
+       dom, function interp ->
+        Cic.Appl
+         [Cic.Const (HelmLibraryObjects.Reals.rminus_URI,[]);
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
+ | expr2 RTIMES expr2
+   { let dom1,mk_expr1 = $1 in
+     let dom2,mk_expr2 = $3 in
+      let dom = union dom1 dom2 in
+       dom, function interp ->
+        Cic.Appl
+         [Cic.Const (HelmLibraryObjects.Reals.rmult_URI,[]) ;
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
+ | expr2 RDIV expr2
+   { let dom1,mk_expr1 = $1 in
+     let dom2,mk_expr2 = $3 in
+      let dom = union dom1 dom2 in
+       dom, function interp ->
+        Cic.Appl
+         [Cic.Const (HelmLibraryObjects.Reals.rdiv_URI,[]) ;
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
  | expr2 PLUS expr2
    { let dom1,mk_expr1 = $1 in
      let dom2,mk_expr2 = $3 in
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string "cic:/Coq/Init/Peano/plus.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Reals.rplus_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -214,8 +273,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string "cic:/Coq/Arith/Minus/minus.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Peano.minus_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -226,8 +284,7 @@ expr2:
       let dom = union dom1 dom2 in
        dom, function interp ->
         Cic.Appl
-         [Cic.Const
-           (UriManager.uri_of_string "cic:/Coq/Init/Peano/mult.con",[]) ;
+         [Cic.Const (HelmLibraryObjects.Peano.mult_URI,[]) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
          ]
@@ -239,8 +296,7 @@ expr2:
       let dom = union dom1 (union dom2 dom3) in
        dom, function interp ->
         Cic.Appl
-         [Cic.MutInd
-           (UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind",0,[]) ;
+         [Cic.MutInd (HelmLibraryObjects.Logic.eq_URI,0,[]) ;
           (mk_expr3 interp) ;
           (mk_expr1 interp) ;
           (mk_expr2 interp)
@@ -366,9 +422,10 @@ expr2:
     }
  | IMPLICIT
     { mk_implicit () }
- | SET  { [], function _ -> Sort Set }
- | PROP { [], function _ -> Sort Prop }
- | TYPE { [], function _ -> Sort Type }
+ | SET   { [], function _ -> Sort Set }
+ | PROP  { [], function _ -> Sort Prop }
+ | TYPE  { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)}
+ | CPROP { [], function _ -> Sort CProp }
  | LPAREN expr CAST expr RPAREN
     { let dom1,mk_expr1 = $2 in
       let dom2,mk_expr2 = $4 in
@@ -507,12 +564,14 @@ pihead:
     { TexCicTextualParser0.binders :=
        (Some (Name $2))::!TexCicTextualParser0.binders;
       let newmeta = new_meta () in
+      let newuniv = CicUniv.fresh () in
        let new_canonical_context = [] in
         let irl =
          identity_relocation_list_for_metavariable new_canonical_context
         in
          TexCicTextualParser0.metasenv :=
-          [newmeta, new_canonical_context, Sort Type ;
+          [newmeta, new_canonical_context, Sort (Type newuniv);
+          (* TASSI: ?? *)
            newmeta+1, new_canonical_context, Meta (newmeta,irl)
           ] @ !TexCicTextualParser0.metasenv ;
          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))
@@ -529,12 +588,14 @@ lambdahead:
     { TexCicTextualParser0.binders :=
        (Some (Name $2))::!TexCicTextualParser0.binders;
       let newmeta = new_meta () in
+      let newuniv = CicUniv.fresh () in
        let new_canonical_context = [] in
         let irl =
          identity_relocation_list_for_metavariable new_canonical_context
         in
          TexCicTextualParser0.metasenv :=
-          [newmeta, new_canonical_context, Sort Type ;
+          [newmeta, new_canonical_context, Sort (Type newuniv) ;
+          (* TASSI: ?? *)
            newmeta+1, new_canonical_context, Meta (newmeta,irl)
           ] @ !TexCicTextualParser0.metasenv ;
          Cic.Name $2, ([], function _ -> Meta (newmeta+1,irl))