From 619e54333d7ba0aa934820bd03d7e0ee2e19b3ac Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 24 Feb 2004 15:39:22 +0000 Subject: [PATCH] More uris ported to V8.0. --- .../ocaml/cic_transformations/contentTable.ml | 69 ++++++++----------- 1 file changed, 28 insertions(+), 41 deletions(-) diff --git a/helm/ocaml/cic_transformations/contentTable.ml b/helm/ocaml/cic_transformations/contentTable.ml index 7950ce284..c41a8386a 100644 --- a/helm/ocaml/cic_transformations/contentTable.ml +++ b/helm/ocaml/cic_transformations/contentTable.ml @@ -14,44 +14,32 @@ let add_symbol uri mnemonic = ;; (* eq *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)" - (fun aid sid args ast_of_acic -> - idref aid (CicAst.Appl - (idref sid (CicAst.Symbol ("eq", 0)) :: - List.map ast_of_acic (List.tl args)))) ;; -Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)" +Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI (fun aid sid args ast_of_acic -> idref aid (CicAst.Appl (idref sid (CicAst.Symbol ("eq", 0)) :: List.map ast_of_acic (List.tl args)))) ;; (* and *) -add_symbol "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" "and" ;; +add_symbol HelmLibraryObjects.Logic.and_XURI "and" ;; (* or *) -add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;; +add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;; (* iff *) -add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;; +add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;; (* not *) -add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;; +add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;; (* Rinv *) -add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;; +add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;; (* Ropp *) -add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "opp" ;; +add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;; (* exists *) -Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)" - (fun aid sid args ast_of_acic -> - match (List.tl args) with - [Cic.ALambda (_,n,s,t)] -> - idref aid - (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic 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 ast_of_acic -> match (List.tl args) with [Cic.ALambda (_,n,s,t)] -> @@ -60,30 +48,29 @@ Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)" | _ -> raise Not_found);; (* leq *) -add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;; -add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;; +add_symbol HelmLibraryObjects.Peano.le_XURI "leq" ;; +add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;; (* lt *) -add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;; -add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;; +add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;; +add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;; (* geq *) -add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;; -add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;; +add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;; +add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;; (* gt *) -add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;; -add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;; +add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;; +add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;; (* plus *) -add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;; -add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "plus" ;; +add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;; +add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;; -let rplus_uri = - UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;; -let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;; +let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;; +let r1_uri = HelmLibraryObjects.Reals.r1_URI;; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI (fun aid sid args ast_of_acic -> let appl () = idref aid (CicAst.Appl @@ -104,19 +91,19 @@ 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 _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;; -Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" +Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;; (* times *) -add_symbol "cic:/Coq/Init/Peano/mult.con" "times" ;; -add_symbol "cic:/Coq/Reals/Rdefinitions/Rmult.con" "times" ;; +add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;; +add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;; (* minus *) -add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;; -add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;; +add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;; +add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;; (* div *) -add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;; +add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;; -- 2.39.2