X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=65216f5d6a1677ce8f943150601fce54184e720d;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=07373374f72d580163b43fb4cc3978b4d7dcb483;hpb=2e6021e158975e808f8cbf653e15a9462409a70a;p=helm.git diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 07373374f..65216f5d6 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -67,78 +67,63 @@ and let symbol_table = Hashtbl.create 503;; (* eq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "eq", - None, Some "cic:/Coq/Init/Logic/eq.ind")) + None, Some HelmLibraryObjects.Logic.eq_SURI)) :: List.map acic2cexpr (List.tl args)));; -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" - (fun aid sid args acic2cexpr -> - Appl - (Some aid, (Symbol (Some sid, "eq", - None, Some "cic:/Coq/Init/Logic_Type/eqT.ind")) - :: List.map acic2cexpr (List.tl args)));; - (* and *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.and_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "and", - None, Some "cic:/Coq/Init/Logic/and.ind")) + None, Some HelmLibraryObjects.Logic.and_SURI)) :: List.map acic2cexpr args));; (* or *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.or_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "or", - None, Some "cic:/Coq/Init/Logic/or.ind")) + None, Some HelmLibraryObjects.Logic.or_SURI)) :: List.map acic2cexpr args));; (* iff *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/iff.con" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.iff_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "iff", - None, Some "cic:/Coq/Init/Logic/iff.con")) + None, Some HelmLibraryObjects.Logic.iff_SURI)) :: List.map acic2cexpr args));; (* not *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/not.con" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.not_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "not", - None, Some "cic:/Coq/Init/Logic/not.con")) + None, Some HelmLibraryObjects.Logic.not_SURI)) :: List.map acic2cexpr args));; (* Rinv *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rinv.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rinv_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "inv", - None, Some "cic:/Coq/Reals/Rdefinitions/Rinv.con")) + None, Some HelmLibraryObjects.Reals.rinv_SURI)) :: List.map acic2cexpr args));; (* Ropp *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Ropp.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.ropp_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "opp", - None, Some "cic:/Coq/Reals/Rdefinitions/Ropp.con")) + None, Some HelmLibraryObjects.Reals.ropp_SURI)) :: List.map acic2cexpr args));; (* exists *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" - (fun aid sid args acic2cexpr -> - match (List.tl args) with - [Cic.ALambda (_,Cic.Name n,s,t)] -> - Binder - (Some aid, "Exists", (n,acic2cexpr s),acic2cexpr t) - | _ -> raise Not_found);; - -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI (fun aid sid args acic2cexpr -> match (List.tl args) with [Cic.ALambda (_,Cic.Name n,s,t)] -> @@ -147,101 +132,97 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" | _ -> raise Not_found);; (* leq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.le_XURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Init/Peano/le.ind")) + None, Some HelmLibraryObjects.Peano.le_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rle.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rle_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "leq", - None, Some "cic:/Coq/Reals/Rdefinitions/Rle.con")) + None, Some HelmLibraryObjects.Reals.rle_SURI)) :: List.map acic2cexpr args));; (* lt *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/lt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.lt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "lt", - None, Some "cic:/Coq/Init/Peano/lt.con")) + None, Some HelmLibraryObjects.Peano.lt_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rlt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rlt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "lt", - None, Some "cic:/Coq/Reals/Rdefinitions/Rlt.con")) + None, Some HelmLibraryObjects.Reals.rlt_SURI)) :: List.map acic2cexpr args));; (* geq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/ge.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.ge_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "geq", - None, Some "cic:/Coq/Init/Peano/ge.con")) + None, Some HelmLibraryObjects.Peano.ge_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rge.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rge_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "geq", - None, Some "cic:/Coq/Reals/Rdefinitions/Rge.con")) + None, Some HelmLibraryObjects.Reals.rge_SURI)) :: List.map acic2cexpr args));; (* gt *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/gt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.gt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "gt", - None, Some "cic:/Coq/Init/Peano/gt.con")) + None, Some HelmLibraryObjects.Peano.gt_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rgt.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rgt_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "gt", - None, Some "cic:/Coq/Reals/Rdefinitions/Rgt.con")) + None, Some HelmLibraryObjects.Reals.rgt_SURI)) :: List.map acic2cexpr args));; (* plus *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/plus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.plus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/Init/Peano/plus.con")) + None, Some HelmLibraryObjects.Peano.plus_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/ZArith/fast_integer/Zplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.BinInt.zplus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/ZArith/fast_integer/Zplus.con")) + None, Some HelmLibraryObjects.BinInt.zplus_SURI)) :: List.map acic2cexpr args));; -let rplus_uri = - UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;; -let r0_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R0.con" ;; -let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;; - -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI (fun aid sid args acic2cexpr -> let appl () = Appl (Some aid, (Symbol (Some sid, "plus", - None, Some "cic:/Coq/Reals/Rdefinitions/Rplus.con")) + None, Some HelmLibraryObjects.Reals.rplus_SURI)) :: List.map acic2cexpr args) in let rec aux acc = function | [ Cic.AConst (nid, uri, []); n] when - UriManager.eq uri r1_uri -> + UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> (match n with - | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri -> + | Cic.AConst (_, uri, []) when + UriManager.eq uri HelmLibraryObjects.Reals.r1_URI -> Num (Some aid, string_of_int (acc + 2)) | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when - UriManager.eq uri rplus_uri -> + UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI -> aux (acc + 1) args | _ -> appl ()) | _ -> appl () @@ -251,48 +232,48 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" (* zero and one *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI (fun aid sid args acic2cexpr -> Num (Some sid, "0")) ;; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI (fun aid sid args acic2cexpr -> Num (Some sid, "1")) ;; (* times *) -Hashtbl.add symbol_table "cic:/Coq/Init/Peano/mult.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.mult_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "times", - None, Some "cic:/Coq/Init/Peano/mult.con")) + None, Some HelmLibraryObjects.Peano.mult_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rmult.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rmult_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "times", - None, Some "cic:/Coq/Reals/Rdefinitions/Rmult.con")) + None, Some HelmLibraryObjects.Reals.rmult_SURI)) :: List.map acic2cexpr args));; (* minus *) -Hashtbl.add symbol_table "cic:/Coq/Arith/Minus/minus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Peano.minus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "minus", - None, Some "cic:/Coq/Arith/Minus/mult.con")) + None, Some HelmLibraryObjects.Peano.minus_SURI)) :: List.map acic2cexpr args));; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rminus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rminus_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "minus", - None, Some "cic:/Coq/Reals/Rdefinitions/Rminus.con")) + None, Some HelmLibraryObjects.Reals.rminus_SURI)) :: List.map acic2cexpr args));; (* div *) -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rdiv_SURI (fun aid sid args acic2cexpr -> Appl (Some aid, (Symbol (Some sid, "div", - None, Some "cic:/Coq/Reals/Rdefinitions/Rdiv.con")) + None, Some HelmLibraryObjects.Reals.rdiv_SURI)) :: List.map acic2cexpr args));; @@ -305,17 +286,18 @@ let string_of_sort = function Cic.Prop -> "Prop" | Cic.Set -> "Set" - | Cic.Type -> "Type" + | Cic.Type _ -> "Type" (* TASSI *) | Cic.CProp -> "Type" ;; let get_constructors uri i = let inductive_types = - (match CicEnvironment.get_obj uri with - Cic.Constant _ -> assert false - | Cic.Variable _ -> assert false - | Cic.CurrentProof _ -> assert false - | Cic.InductiveDefinition (l,_,_) -> l + (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with + Cic.Constant _ -> assert false + | Cic.Variable _ -> assert false + | Cic.CurrentProof _ -> assert false + | Cic.InductiveDefinition (l,_,_) -> l ) in let (_,_,_,constructors) = List.nth inductive_types i in constructors @@ -389,7 +371,8 @@ let acic2cexpr ids_to_inner_sorts t = make_subst subst, Some uri_str)::List.map acic2cexpr tl)) | C.AAppl (aid,C.AMutInd (sid,uri,i,subst)::tl) -> let inductive_types = - (match CicEnvironment.get_obj uri with + (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false @@ -417,7 +400,8 @@ let acic2cexpr ids_to_inner_sorts t = make_subst subst, Some (UriManager.string_of_uri uri))) | C.AMutInd (id,uri,i,subst) -> let inductive_types = - (match CicEnvironment.get_obj uri with + (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in + match o with Cic.Constant _ -> assert false | Cic.Variable _ -> assert false | Cic.CurrentProof _ -> assert false