From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 29 May 2003 16:26:56 +0000 (+0000)
Subject: 1. minus binary operator added
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=194de297e16afcd857f36aba9c06fa6919654d94;p=helm.git

1. minus binary operator added
2. identifiers can no longer start with a non-letter character
---

diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
index 7f70b8e88..320162c75 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualLexer.mll
@@ -63,8 +63,9 @@
 }
 let dollar = '$'
 let num = ['1'-'9']['0'-'9']* | '0'
-let alfa = ['A'-'Z' 'a'-'z' '_' ''' '-'] | "\\_"
-let ident = alfa (alfa | num)*
+let letter = ['A'-'Z' 'a'-'z']
+let alfa = letter | ['_' ''' '-'] | "\\_"
+let ident = letter (alfa | num)*
 let baseuri = '/'(ident '/')* ident '.'
 let conuri = baseuri "con"
 let varuri = baseuri "var"
@@ -115,6 +116,7 @@ rule token =
   | eof         { EOF }
   (* Arithmetical operators *)
   | '+'         { PLUS }
+  | '-'         { MINUS }
   | '*'         { TIMES }
   | '='         { EQ }
 {}
diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
index 245485922..e26145e28 100644
--- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
+++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly
@@ -158,10 +158,10 @@
 %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 TIMES EQ
+%token PLUS MINUS TIMES EQ
 %right ARROW
 %right EQ
-%right PLUS
+%right PLUS MINUS
 %right TIMES
 %start main
 %type <CicTextualParser0.interpretation_domain_item list * (CicTextualParser0.interpretation -> Cic.term)> main
@@ -208,6 +208,18 @@ expr2:
           (mk_expr2 interp)
          ]
    }
+ | expr2 MINUS 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/Arith/Minus/minus.con",[]) ;
+          (mk_expr1 interp) ;
+          (mk_expr2 interp)
+         ]
+   }
  | expr2 TIMES expr2
    { let dom1,mk_expr1 = $1 in
      let dom2,mk_expr2 = $3 in