X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualParser.mly;h=41a36acc6ae7e3f624905f50c15c1ceba12936d4;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;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..41a36acc6 100644 --- a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly +++ b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly @@ -136,12 +136,14 @@ 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 ; @@ -156,7 +158,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 +186,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 +203,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 +218,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 +229,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 +240,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 +251,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 +262,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 +273,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 +284,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 +296,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 +422,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 (CicUniv.fresh ())) (* TASSI: ?? *)} + | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in let dom2,mk_expr2 = $4 in @@ -614,12 +564,14 @@ pihead: { 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)) @@ -636,12 +588,14 @@ lambdahead: { 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))