X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftex_cic_textual_parser%2FtexCicTextualParser.mly;h=41a36acc6ae7e3f624905f50c15c1ceba12936d4;hb=3bb4ce11fb9d4c6375483a80344beb94c4517dd7;hp=f6f557947a0598509c1ce9c45f66fc0f79b99009;hpb=296b163c8a2b09a6f87cbab15c2016de92fc8e70;p=helm.git diff --git a/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly b/helm/ocaml/tex_cic_textual_parser/texCicTextualParser.mly index f6f557947..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 ; @@ -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) @@ -475,7 +424,7 @@ expr2: { mk_implicit () } | SET { [], function _ -> Sort Set } | PROP { [], function _ -> Sort Prop } - | TYPE { [], function _ -> Sort Type } + | TYPE { [], function _ -> Sort (Type (CicUniv.fresh ())) (* TASSI: ?? *)} | CPROP { [], function _ -> Sort CProp } | LPAREN expr CAST expr RPAREN { let dom1,mk_expr1 = $2 in @@ -615,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)) @@ -637,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))