helm/ocaml/cic_transformations/contentTable.ml

   1
   2 (* NOTATION *)
   3
   4 let symbol_table = Hashtbl.create 503 ;;
   5 let lookup_symbol = Hashtbl.find symbol_table ;;
   6
   7 let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;;
   8
   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)))
  14 ;;
  15
  16 (* eq *)
  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)))) ;;
  27
  28 (* and *)
  29 add_symbol "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)" "and" ;;
  30
  31 (* or *)
  32 add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;;
  33
  34 (* iff *)
  35 add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;;
  36
  37 (* not *)
  38 add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;;
  39
  40 (* Rinv *)
  41 add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;;
  42
  43 (* Ropp *)
  44 add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "opp" ;;
  45
  46 (* exists *)
  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)] ->
  51        idref aid
  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)] ->
  58        idref aid
  59         (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
  60   | _ -> raise Not_found);;
  61
  62 (* leq *)
  63 add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;;
  64 add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;;
  65
  66 (* lt *)
  67 add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;;
  68 add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;;
  69
  70 (* geq *)
  71 add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;;
  72 add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;;
  73
  74 (* gt *)
  75 add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;;
  76 add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;;
  77
  78 (* plus *)
  79 add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;;
  80 add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "plus" ;;
  81
  82 let rplus_uri =
  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" ;;
  85
  86 Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con"
  87   (fun aid sid args ast_of_acic ->
  88     let appl () =
  89       idref aid (CicAst.Appl
  90         (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
  91    in
  92     let rec aux acc = function
  93       | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
  94             (match n with
  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 ->
  99                 aux (acc + 1) args
 100             | _ -> appl ())
 101       | _ -> appl ()
 102     in
 103     aux 0 args)
 104 ;;
 105
 106 (* zero and one *)
 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))) ;;
 111
 112 (* times *)
 113 add_symbol "cic:/Coq/Init/Peano/mult.con" "times" ;;
 114 add_symbol "cic:/Coq/Reals/Rdefinitions/Rmult.con" "times" ;;
 115
 116 (* minus *)
 117 add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;;
 118 add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;;
 119
 120 (* div *)
 121 add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;;
 122