(* 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 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 HelmLibraryObjects.Logic.and_XURI "and" ;;

(* or *)
add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;;

(* iff *)
add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;;

(* not *)
add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;;

(* Rinv *)
add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;;

(* Ropp *)
add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;;

(* exists *)
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)] ->
       idref aid
        (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
  | _ -> raise Not_found);;

(* leq *) 
add_symbol HelmLibraryObjects.Peano.le_XURI "leq" ;;
add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;;

(* lt *)
add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;;
add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;;

(* geq *)
add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;;
add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;;

(* gt *)
add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;;
add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;;

(* plus *)
add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;;
add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;;

let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;;
let r1_uri = HelmLibraryObjects.Reals.r1_URI;;

Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
  (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 HelmLibraryObjects.Reals.r0_SURI
  (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
  (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;

(* times *) 
add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;;
add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;;

(* minus *)
add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;;
add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;;

(* div *)
add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;;