4 let symbol_table = Hashtbl.create 503 ;;
5 let lookup_symbol = Hashtbl.find symbol_table ;;
7 let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;;
9 let add_symbol uri mnemonic =
10 Hashtbl.add symbol_table uri
11 (fun aid sid args ast_of_acic ->
12 idref aid (CicAst.Appl
13 (idref sid (CicAst.Symbol (mnemonic, 0)) :: List.map ast_of_acic args)))
17 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)"
18 (fun aid sid args ast_of_acic ->
19 idref aid (CicAst.Appl
20 (idref sid (CicAst.Symbol ("eq", 0)) ::
21 List.map ast_of_acic (List.tl args)))) ;;
22 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/eqT.ind#xpointer(1/1)"
23 (fun aid sid args ast_of_acic ->
24 idref aid (CicAst.Appl
25 (idref sid (CicAst.Symbol ("eq", 0)) ::
26 List.map ast_of_acic (List.tl args)))) ;;
29 add_symbol "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" "and" ;;
32 add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;;
35 add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;;
38 add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;;
41 add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;;
44 add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "opp" ;;
47 Hashtbl.add symbol_table "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)"
48 (fun aid sid args ast_of_acic ->
49 match (List.tl args) with
50 [Cic.ALambda (_,n,s,t)] ->
52 (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
53 | _ -> raise Not_found);;
54 Hashtbl.add symbol_table "cic:/Coq/Init/Logic_Type/exT.ind#xpointer(1/1)"
55 (fun aid sid args ast_of_acic ->
56 match (List.tl args) with
57 [Cic.ALambda (_,n,s,t)] ->
59 (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
60 | _ -> raise Not_found);;
63 add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;;
64 add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;;
67 add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;;
68 add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;;
71 add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;;
72 add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;;
75 add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;;
76 add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;;
79 add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;;
80 add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "plus" ;;
83 UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/Rplus.con" ;;
84 let r1_uri = UriManager.uri_of_string "cic:/Coq/Reals/Rdefinitions/R1.con" ;;
86 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
87 (fun aid sid args ast_of_acic ->
89 idref aid (CicAst.Appl
90 (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
92 let rec aux acc = function
93 | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
95 | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
96 idref aid (CicAst.Num (string_of_int (acc+2), 0))
97 | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args)
98 when UriManager.eq uri rplus_uri ->
107 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con"
108 (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
109 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con"
110 (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
113 add_symbol "cic:/Coq/Init/Peano/mult.con" "times" ;;
114 add_symbol "cic:/Coq/Reals/Rdefinitions/Rmult.con" "times" ;;
117 add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;;
118 add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;;
121 add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;;