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 HelmLibraryObjects.Logic.eq_XURI
  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
  23 (* and *)
  24 add_symbol HelmLibraryObjects.Logic.and_XURI "and" ;;
  25
  26 (* or *)
  27 add_symbol HelmLibraryObjects.Logic.or_XURI "or" ;;
  28
  29 (* iff *)
  30 add_symbol HelmLibraryObjects.Logic.iff_SURI "iff" ;;
  31
  32 (* not *)
  33 add_symbol HelmLibraryObjects.Logic.not_SURI "not" ;;
  34
  35 (* Rinv *)
  36 add_symbol HelmLibraryObjects.Reals.rinv_SURI "inv" ;;
  37
  38 (* Ropp *)
  39 add_symbol HelmLibraryObjects.Reals.ropp_SURI "opp" ;;
  40
  41 (* exists *)
  42 Hashtbl.add symbol_table HelmLibraryObjects.Logic.ex_XURI
  43   (fun aid sid args ast_of_acic ->
  44    match (List.tl args) with
  45      [Cic.ALambda (_,n,s,t)] ->
  46        idref aid
  47         (CicAst.Binder (`Exists, (n, Some (ast_of_acic s)), ast_of_acic t))
  48   | _ -> raise Not_found);;
  49
  50 (* leq *)
  51 add_symbol HelmLibraryObjects.Peano.le_XURI "leq" ;;
  52 add_symbol HelmLibraryObjects.Reals.rle_SURI "leq" ;;
  53
  54 (* lt *)
  55 add_symbol HelmLibraryObjects.Peano.lt_SURI "lt" ;;
  56 add_symbol HelmLibraryObjects.Reals.rlt_SURI "lt" ;;
  57
  58 (* geq *)
  59 add_symbol HelmLibraryObjects.Peano.ge_SURI "geq" ;;
  60 add_symbol HelmLibraryObjects.Reals.rge_SURI "geq" ;;
  61
  62 (* gt *)
  63 add_symbol HelmLibraryObjects.Peano.gt_SURI "gt" ;;
  64 add_symbol HelmLibraryObjects.Reals.rgt_SURI "gt" ;;
  65
  66 (* plus *)
  67 add_symbol HelmLibraryObjects.Peano.plus_SURI "plus" ;;
  68 add_symbol HelmLibraryObjects.BinInt.zplus_SURI "plus" ;;
  69
  70 let rplus_uri = HelmLibraryObjects.Reals.rplus_URI;;
  71 let r1_uri = HelmLibraryObjects.Reals.r1_URI;;
  72
  73 Hashtbl.add symbol_table HelmLibraryObjects.Reals.rplus_SURI
  74   (fun aid sid args ast_of_acic ->
  75     let appl () =
  76       idref aid (CicAst.Appl
  77         (idref sid (CicAst.Symbol ("plus", 0)) :: List.map ast_of_acic args))
  78    in
  79     let rec aux acc = function
  80       | [ Cic.AConst (nid, uri, []); n] when UriManager.eq uri r1_uri ->
  81             (match n with
  82             | Cic.AConst (_, uri, []) when UriManager.eq uri r1_uri ->
  83                 idref aid (CicAst.Num (string_of_int (acc+2), 0))
  84             | Cic.AAppl (_, Cic.AConst (_, uri, []) :: args)
  85               when UriManager.eq uri rplus_uri ->
  86                 aux (acc + 1) args
  87             | _ -> appl ())
  88       | _ -> appl ()
  89     in
  90     aux 0 args)
  91 ;;
  92
  93 (* zero and one *)
  94 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r0_SURI
  95   (fun _ sid _ _ -> idref sid (CicAst.Num ("0", 0))) ;;
  96 Hashtbl.add symbol_table HelmLibraryObjects.Reals.r1_SURI
  97   (fun _ sid _ _ -> idref sid (CicAst.Num ("1", 0))) ;;
  98
  99 (* times *)
 100 add_symbol HelmLibraryObjects.Peano.mult_SURI "times" ;;
 101 add_symbol HelmLibraryObjects.Reals.rmult_SURI "times" ;;
 102
 103 (* minus *)
 104 add_symbol HelmLibraryObjects.Peano.minus_SURI "minus" ;;
 105 add_symbol HelmLibraryObjects.Reals.rminus_SURI "minus" ;;
 106
 107 (* div *)
 108 add_symbol HelmLibraryObjects.Reals.rdiv_SURI "div" ;;
 109