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 ;
%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
%%
*/
;
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)
]
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)
]
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)
]
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)
}
| 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
{ 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))
{ 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))