(* NOTATION *)

let symbol_table = Hashtbl.create 503 ;;
let lookup_symbol = Hashtbl.find symbol_table ;;

let idref id t = CicAst.AttributedTerm (`IdRef id, t) ;;

let add_symbol uri mnemonic =
  Hashtbl.add symbol_table uri
    (fun aid sid args ast_of_acic ->
      idref aid (CicAst.Appl
        (idref sid (CicAst.Symbol (mnemonic, 0)) :: List.map ast_of_acic args)))
;;

(* 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)" 
  (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" ;;

(* or *)
add_symbol "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)" "or" ;;

(* iff *)
add_symbol "cic:/Coq/Init/Logic/iff.con" "iff" ;;

(* not *)
add_symbol "cic:/Coq/Init/Logic/not.con" "not" ;;

(* Rinv *)
add_symbol "cic:/Coq/Reals/Rdefinitions/Rinv.con" "inv" ;;

(* Ropp *)
add_symbol "cic:/Coq/Reals/Rdefinitions/Ropp.con" "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)" 
  (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);;

(* leq *) 
add_symbol "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)" "leq" ;;
add_symbol "cic:/Coq/Reals/Rdefinitions/Rle.con" "leq" ;;

(* lt *)
add_symbol "cic:/Coq/Init/Peano/lt.con" "lt" ;;
add_symbol "cic:/Coq/Reals/Rdefinitions/Rlt.con" "lt" ;;

(* geq *)
add_symbol "cic:/Coq/Init/Peano/ge.con" "geq" ;;
add_symbol "cic:/Coq/Reals/Rdefinitions/Rge.con" "geq" ;;

(* gt *)
add_symbol "cic:/Coq/Init/Peano/gt.con" "gt" ;;
add_symbol "cic:/Coq/Reals/Rdefinitions/Rgt.con" "gt" ;;

(* plus *)
add_symbol "cic:/Coq/Init/Peano/plus.con" "plus" ;;
add_symbol "cic:/Coq/ZArith/fast_integer/Zplus.con" "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" ;;

Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/Rplus.con" 
  (fun aid sid args ast_of_acic ->
    let appl () =
      idref aid (CicAst.Appl 
        (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
   in
    let rec aux acc = function
      | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
            (match n with
            | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
                idref aid (CicAst.Num (string_of_int (acc+2), 0))
            | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args)
              when UriManager.eq uri rplus_uri ->
                aux (acc + 1) args
            | _ -> appl ())
      | _ -> appl ()
    in
    aux 0 args)
;;

(* zero and one *)
Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R0.con" 
  (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
Hashtbl.add symbol_table "cic:/Coq/Reals/Rdefinitions/R1.con" 
  (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" ;;

(* minus *)
add_symbol "cic:/Coq/Arith/Minus/minus.con" "minus" ;;
add_symbol "cic:/Coq/Reals/Rdefinitions/Rminus.con" "minus" ;;

(* div *)
add_symbol "cic:/Coq/Reals/Rdefinitions/Rdiv.con" "div" ;;