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 <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 RPLUS RMINUS RTIMES RDIV
-%token PLUS MINUS TIMES EQT EQ
+%token PLUS MINUS TIMES EQT EQ NEQT
%right ARROW
-%nonassoc EQ EQT
+%nonassoc EQ EQT NEQT
%left PLUS MINUS RPLUS RMINUS
%left TIMES RTIMES RDIV
%start main
{ [], 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",[])
+ 0 -> Cic.Const (HelmLibraryObjects.Reals.r0_URI, [])
+ | 1 -> Cic.Const (HelmLibraryObjects.Reals.r1_URI,[])
| 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",[]);
+ (HelmLibraryObjects.Reals.rplus_URI,[]) ;
+ Cic.Const (HelmLibraryObjects.Reals.r1_URI,[]);
cic_real_of_real (n - 1)
]
in
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
let dom = union dom1 dom2 in
dom, function interp ->
Cic.Appl
- [Cic.Const
- (UriManager.uri_of_string
- "cic:/Coq/Reals/Rdefinitions/Rplus.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/Reals/Rdefinitions/Rminus.con",[]) ;
+ [Cic.Const (HelmLibraryObjects.Reals.rminus_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/Reals/Rdefinitions/Rmult.con",[]) ;
+ [Cic.Const (HelmLibraryObjects.Reals.rmult_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/Reals/Rdefinitions/Rdiv.con",[]) ;
+ [Cic.Const (HelmLibraryObjects.Reals.rdiv_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/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",[]) ;
- (mk_expr1 interp) ;
- (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) ;
+ [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))