From 71284ef6c56c909e7205543f3fe8b916517f79b0 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Thu, 4 Sep 2003 16:44:04 +0000
Subject: [PATCH] - added dot notation for real numbers and basic operations on
 them - added support for \eqt

---
 .../texCicTextualLexer.mll                    |  10 ++
 .../texCicTextualParser.mly                   | 101 +++++++++++++++++-
 2 files changed, 106 insertions(+), 5 deletions(-)

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 01ddd0cf3..06bbab076 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -90,6 +90,11 @@ rule token =
                    (indtyuri_of_uri ("cic:" ^ (unquote (L.lexeme lexbuf)))) }
   | indconuri   { INDCONURI
                    (indconuri_of_uri("cic:" ^ (unquote (L.lexeme lexbuf)))) }
+  | num '.'     {
+                  let lexeme = L.lexeme lexbuf in
+                  RNUM (int_of_string
+                    (String.sub lexeme 0 (String.length lexeme - 1)))
+                }
   | num         { NUM (int_of_string (L.lexeme lexbuf)) }
   | '?' num     { let lexeme = L.lexeme lexbuf in
                    META
@@ -108,6 +113,7 @@ rule token =
   | "\\lambda"  { LAMBDA }
   | "\\pi"      { PROD }
   | "\\forall"  { PROD }
+  | "\\eqt"     { EQT }
   | ':'         { COLON }
   | '.'         { DOT }
   | "\\to"      { ARROW }
@@ -115,6 +121,10 @@ rule token =
   | dollar      { DOLLAR }
   | eof         { EOF }
   (* Arithmetical operators *)
+  | "+."        { RPLUS }
+  | "-."        { RMINUS }
+  | "*."        { RTIMES }
+  | "/."        { RDIV }
   | '+'         { PLUS }
   | '-'         { MINUS }
   | '*'         { TIMES }
diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index e26145e28..f5aa71417 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -151,6 +151,7 @@
 %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
@@ -158,11 +159,12 @@
 %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
 %token DOLLAR
-%token PLUS MINUS TIMES EQ
+%token RPLUS RMINUS RTIMES RDIV
+%token PLUS MINUS TIMES EQT EQ
 %right ARROW
-%right EQ
-%right PLUS MINUS
-%right TIMES
+%right EQ EQT
+%right PLUS MINUS RPLUS RMINUS
+%right TIMES RTIMES RDIV
 %start main
 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
 %%
@@ -178,7 +180,30 @@ main:
 			  */
 ;
 expr2:
-   NUM
+ | RNUM
+   { [], function interp ->
+      let rec cic_real_of_real =
+       function
+          0 ->
+           Cic.Const
+            (UriManager.uri_of_string
+              "cic:/Coq/Reals/Rdefinitions/R0.con",[])
+        | 1 ->
+           Cic.Const
+            (UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con",[])
+        | n ->
+          Cic.Appl
+           [ Cic.Const
+               (UriManager.uri_of_string
+                  "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
+             Cic.Const (UriManager.uri_of_string
+              "cic:/Coq/Reals/Rdefinitions/R1.con",[]);
+             cic_real_of_real (n - 1)
+           ]
+      in
+       cic_real_of_real $1
+   }
+ | NUM
    { [], function interp ->
       let rec cic_int_of_int =
        function
@@ -196,6 +221,58 @@ expr2:
       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
+           (UriManager.uri_of_string
+              "cic:/Coq/Reals/Rdefinitions/Rplus.con",[]) ;
+          (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
+           (UriManager.uri_of_string
+              "cic:/Coq/Reals/Rdefinitions/Rminus.con",[]) ;
+          (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
+           (UriManager.uri_of_string
+              "cic:/Coq/Reals/Rdefinitions/Rmult.con",[]) ;
+          (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
+           (UriManager.uri_of_string
+              "cic:/Coq/Reals/Rdefinitions/Rdiv.con",[]) ;
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
  | expr2 PLUS expr2
    { let dom1,mk_expr1 = $1 in
      let dom2,mk_expr2 = $3 in
@@ -232,6 +309,20 @@ expr2:
           (mk_expr2 interp)
          ]
    }
+ | expr2 EQT expr2
+   { let dom1,mk_expr1 = $1 in
+     let dom2,mk_expr2 = $3 in
+     let dom3,mk_expr3 = mk_implicit () in
+      let dom = union dom1 (union dom2 dom3) in
+       dom, function interp ->
+        Cic.Appl
+         [Cic.MutInd
+           (UriManager.uri_of_string "cic:/Coq/Init/Logic_Type/eqT.ind",0,[]) ;
+          (mk_expr3 interp) ;
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
  | expr2 EQ expr2
    { let dom1,mk_expr1 = $1 in
      let dom2,mk_expr2 = $3 in
-- 
2.39.2