X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualParser.mly;h=3ca69d5c6d59ba9f0fd3701942f6c58a8f8ba97f;hb=78cf601fd8b8dbb386b0db315dcbfdbe8256c15f;hp=500565823d20a328166fd06dda7e2222d4860777;hpb=a335fa89b0340ba3fb5d60566075ca83b5bda5d1;p=helm.git diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly index 500565823..3ca69d5c6 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly @@ -156,7 +156,7 @@ %token VARURI %token INDTYURI %token 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 @@ -184,20 +184,13 @@ expr2: { [], 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 @@ -208,14 +201,10 @@ expr2: 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 @@ -227,9 +216,7 @@ expr2: 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) ] @@ -240,9 +227,7 @@ expr2: 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) ] @@ -253,9 +238,7 @@ expr2: 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) ] @@ -266,9 +249,7 @@ expr2: 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) ] @@ -279,8 +260,7 @@ expr2: 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) ] @@ -291,8 +271,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) ] @@ -303,42 +282,11 @@ expr2: 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) ] } - | expr2 NEQT 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.Const (UriManager.uri_of_string "cic:/Coq/Init/Logic/not.con",[]); - 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 @@ -346,8 +294,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) @@ -473,9 +420,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 } + | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in let dom2,mk_expr2 = $4 in