helm/ocaml/cic/helmLibraryObjects.ml

   1
   2 (** {2 Auxiliary functions} *)
   3
   4 let uri = UriManager.uri_of_string
   5
   6 let const ?(subst = []) uri = Cic.Const (uri, subst)
   7 let var ?(subst = []) uri = Cic.Var (uri, subst)
   8 let mutconstruct ?(subst = []) uri typeno consno =
   9   Cic.MutConstruct (uri, typeno, consno, subst)
  10
  11 (** {2 Helm's objects shorthands} *)
  12
  13 module Logic =
  14   struct
  15     let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
  16     let true_URI = uri "cic:/Coq/Init/Logic/True.ind"
  17     let false_URI = uri "cic:/Coq/Init/Logic/False.ind"
  18   end
  19
  20 module Logic_Type =
  21   struct
  22     let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
  23     let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
  24
  25     let refl_eqt = mutconstruct eqt_URI 0 1
  26     let sym_eqt = const sym_eqt_URI
  27   end
  28
  29 module Datatypes =
  30   struct
  31     let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"
  32     let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"
  33
  34     let trueb = mutconstruct bool_URI 0 1
  35     let falseb = mutconstruct bool_URI 0 2
  36     let zero = mutconstruct nat_URI 0 1
  37     let succ = mutconstruct nat_URI 0 2
  38   end
  39
  40 module Reals =
  41   struct
  42     let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
  43     let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con"
  44     let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
  45     let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con"
  46     let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
  47     let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
  48     let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
  49
  50     let r = const r_URI
  51     let rplus = const rplus_URI
  52     let rmult = const rmult_URI
  53     let ropp = const ropp_URI
  54     let r0 = const r0_URI
  55     let r1 = const r1_URI
  56     let rtheory = const rtheory_URI
  57   end
  58
  59 module Peano =
  60   struct
  61     let plus_URI = uri "cic:/Coq/Init/Peano/plus.con"
  62     let mult_URI = uri "cic:/Coq/Init/Peano/mult.con"
  63     let pred_URI = uri "cic:/Coq/Init/Peano/pred.con"
  64
  65     let plus = const plus_URI
  66     let mult = const mult_URI
  67     let pred = const pred_URI
  68   end
  69
  70 (** {2 Helpers for creating common terms}
  71  *  (e.g. numbers)} *)
  72
  73 exception NegativeInteger
  74
  75 let build_nat n =
  76   if n < 0 then raise NegativeInteger;
  77   let rec aux = function
  78     | 0 -> Datatypes.zero
  79     | n -> Cic.Appl [ Datatypes.succ; (aux (n - 1)) ]
  80   in
  81   aux n
  82
  83 let build_real n =
  84   if n < 0 then raise NegativeInteger;
  85   let rec aux = function
  86     | 0 -> Reals.r0
  87     | 1 -> Reals.r1 (* to avoid trailing "+ 0" *)
  88     | n -> Cic.Appl [ Reals.rplus; Reals.r1; (aux (n - 1)) ]
  89   in
  90   aux n
  91