+let _ = (** fill symbol_table *)
+ let add_symbol name uri =
+ Hashtbl.add symbol_table uri
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Appl (Ast.AttributedTerm (`IdRef sid, Ast.Symbol (name, -1)) ::
+ List.map acic2ast args)))
+ in
+ (* eq *)
+ Hashtbl.add symbol_table HelmLibraryObjects.Logic.eq_XURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Appl (
+ Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("eq", -1)) ::
+ List.map acic2ast (List.tl args))));
+ (* exists *)
+ Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
+ (fun aid sid args acic2ast ->
+ match (List.tl args) with
+ [Cic.ALambda (_,Cic.Name n,s,t)] ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Binder (`Exists, (Cic.Name n, Some (acic2ast s)), acic2ast t))
+ | _ -> raise Not_found);
+ add_symbol "and" HelmLibraryObjects.Logic.and_XURI;
+ add_symbol "or" HelmLibraryObjects.Logic.or_XURI;
+ add_symbol "iff" HelmLibraryObjects.Logic.iff_SURI;
+ add_symbol "not" HelmLibraryObjects.Logic.not_SURI;
+ add_symbol "inv" HelmLibraryObjects.Reals.rinv_SURI;
+ add_symbol "opp" HelmLibraryObjects.Reals.ropp_SURI;
+ add_symbol "leq" HelmLibraryObjects.Peano.le_XURI;
+ add_symbol "leq" HelmLibraryObjects.Reals.rle_SURI;
+ add_symbol "lt" HelmLibraryObjects.Peano.lt_SURI;
+ add_symbol "lt" HelmLibraryObjects.Reals.rlt_SURI;
+ add_symbol "geq" HelmLibraryObjects.Peano.ge_SURI;
+ add_symbol "geq" HelmLibraryObjects.Reals.rge_SURI;
+ add_symbol "gt" HelmLibraryObjects.Peano.gt_SURI;
+ add_symbol "gt" HelmLibraryObjects.Reals.rgt_SURI;
+ add_symbol "plus" HelmLibraryObjects.Peano.plus_SURI;
+ add_symbol "plus" HelmLibraryObjects.BinInt.zplus_SURI;
+ add_symbol "times" HelmLibraryObjects.Peano.mult_SURI;
+ add_symbol "times" HelmLibraryObjects.Reals.rmult_SURI;
+ add_symbol "minus" HelmLibraryObjects.Peano.minus_SURI;
+ add_symbol "minus" HelmLibraryObjects.Reals.rminus_SURI;
+ add_symbol "div" HelmLibraryObjects.Reals.rdiv_SURI;
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef sid, Ast.Num ("0", -1)));
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
+ (fun aid sid args acic2ast ->
+ Ast.AttributedTerm (`IdRef sid, Ast.Num ("1", -1)));
+ (* plus *)
+ Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
+ (fun aid sid args acic2ast ->
+ let appl () =
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Appl (
+ Ast.AttributedTerm (`IdRef sid, Ast.Symbol ("plus", -1)) ::
+ List.map acic2ast args))
+ in
+ let rec aux acc = function
+ | [ Cic.AConst (nid, uri, []); n] when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ (match n with
+ | Cic.AConst (_, uri, []) when
+ UriManager.eq uri HelmLibraryObjects.Reals.r1_URI ->
+ Ast.AttributedTerm (`IdRef aid,
+ Ast.Num (string_of_int (acc + 2), -1))
+ | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args) when
+ UriManager.eq uri HelmLibraryObjects.Reals.rplus_URI ->
+ aux (acc + 1) args
+ | _ -> appl ())
+ | _ -> appl ()
+ in
+ aux 0 args)
+