X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2Fcontent_expressions.ml;h=8c88fd01f1186362a7260c1499c2f56b1eb92fa3;hb=c5d5bf37b1e4c4b9b499ed2cbfe27cf2ec181944;hp=2ff989da184439ef060b5344e4dcbbdbf501a89a;hpb=5f45c292bf9e99bd746f6ec4c7c268022012e925;p=helm.git diff --git a/helm/ocaml/cic_transformations/content_expressions.ml b/helm/ocaml/cic_transformations/content_expressions.ml index 2ff989da1..8c88fd01f 100644 --- a/helm/ocaml/cic_transformations/content_expressions.ml +++ b/helm/ocaml/cic_transformations/content_expressions.ml @@ -36,7 +36,7 @@ (* the type cexpr is inspired by OpenMath. A few primitive constructors have been added, in order to take into account some special features of functional expressions. Most notably: case, let in, let rec, and - explicit substitutons *) + explicit substitutions *) type cexpr = Symbol of string option * string * subst option * string option @@ -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/Rinv.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));; @@ -303,9 +284,10 @@ Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rdiv.con" let string_of_sort = function - Cic.Prop -> "Prop" - | Cic.Set -> "Set" - | Cic.Type -> "Type" + Cic.Prop -> "Prop" + | Cic.Set -> "Set" + | Cic.Type _ -> "Type" (* TASSI *) + | Cic.CProp -> "Type" ;; let get_constructors uri i =