2 (** {2 Auxiliary functions} *)
4 let uri = UriManager.uri_of_string
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)
11 (** {2 Helm's objects shorthands} *)
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"
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"
25 let refl_eqt = mutconstruct eqt_URI 0 1
26 let sym_eqt = const sym_eqt_URI
31 let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"
32 let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"
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
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"
51 let rplus = const rplus_URI
52 let rmult = const rmult_URI
53 let ropp = const ropp_URI
56 let rtheory = const rtheory_URI
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"
65 let plus = const plus_URI
66 let mult = const mult_URI
67 let pred = const pred_URI
70 (** {2 Helpers for creating common terms}
73 exception NegativeInteger
76 if n < 0 then raise NegativeInteger;
77 let rec aux = function
79 | n -> Cic.Appl [ Datatypes.succ; (aux (n - 1)) ]
84 if n < 0 then raise NegativeInteger;
85 let rec aux = function
87 | 1 -> Reals.r1 (* to avoid trailing "+ 0" *)
88 | n -> Cic.Appl [ Reals.rplus; Reals.r1; (aux (n - 1)) ]