1 (** {2 Auxiliary functions} *)
3 let uri = UriManager.uri_of_string
5 let const ?(subst = []) uri = Cic.Const (uri, subst)
6 let var ?(subst = []) uri = Cic.Var (uri, subst)
7 let mutconstruct ?(subst = []) uri typeno consno =
8 Cic.MutConstruct (uri, typeno, consno, subst)
9 let mutind ?(subst = []) uri typeno = Cic.MutInd (uri, typeno, subst)
11 let indtyuri_of_uri uri =
12 let index_sharp = String.index uri '#' in
13 let index_num = index_sharp + 3 in
14 (UriManager.uri_of_string (String.sub uri 0 index_sharp),
15 int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1)
17 let indconuri_of_uri uri =
18 let index_sharp = String.index uri '#' in
19 let index_div = String.rindex uri '/' in
20 let index_con = index_div + 1 in
21 (UriManager.uri_of_string (String.sub uri 0 index_sharp),
23 (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
25 (String.sub uri index_con (String.length uri - index_con)))
28 let s = UriManager.string_of_uri uri in
31 (* TODO explicit substitutions? *)
32 let len = String.length s in
33 let sub = String.sub s (len -4) 4 in
36 else if sub = ".var" then
41 let (uri, typeno) = indtyuri_of_uri s in
44 | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
45 (* Constructor of an Inductive Type *)
46 let (uri, typeno, consno) = indconuri_of_uri s in
47 mutconstruct uri typeno consno)
49 | Invalid_argument _ | Not_found -> raise (UriManager.IllFormedUri s)
51 (** {2 Helm's objects shorthands} *)
55 let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind"
56 let true_URI = uri "cic:/Coq/Init/Logic/True.ind"
57 let false_URI = uri "cic:/Coq/Init/Logic/False.ind"
62 let eqt_URI = uri "cic:/Coq/Init/Logic_Type/eqT.ind"
63 let sym_eqt_URI = uri "cic:/Coq/Init/Logic_Type/sym_eqT.con"
65 let refl_eqt = mutconstruct eqt_URI 0 1
66 let sym_eqt = const sym_eqt_URI
71 let bool_URI = uri "cic:/Coq/Init/Datatypes/bool.ind"
72 let nat_URI = uri "cic:/Coq/Init/Datatypes/nat.ind"
74 let trueb = mutconstruct bool_URI 0 1
75 let falseb = mutconstruct bool_URI 0 2
76 let zero = mutconstruct nat_URI 0 1
77 let succ = mutconstruct nat_URI 0 2
82 let r_URI = uri "cic:/Coq/Reals/Rdefinitions/R.con"
83 let rplus_URI = uri "cic:/Coq/Reals/Rdefinitions/Rplus.con"
84 let rmult_URI = uri "cic:/Coq/Reals/Rdefinitions/Rmult.con"
85 let ropp_URI = uri "cic:/Coq/Reals/Rdefinitions/Ropp.con"
86 let r0_URI = uri "cic:/Coq/Reals/Rdefinitions/R0.con"
87 let r1_URI = uri "cic:/Coq/Reals/Rdefinitions/R1.con"
88 let rtheory_URI = uri "cic:/Coq/Reals/Rbase/RTheory.con"
91 let rplus = const rplus_URI
92 let rmult = const rmult_URI
93 let ropp = const ropp_URI
96 let rtheory = const rtheory_URI
101 let plus_URI = uri "cic:/Coq/Init/Peano/plus.con"
102 let mult_URI = uri "cic:/Coq/Init/Peano/mult.con"
103 let pred_URI = uri "cic:/Coq/Init/Peano/pred.con"
105 let plus = const plus_URI
106 let mult = const mult_URI
107 let pred = const pred_URI
110 (** {2 Helpers for creating common terms}
113 exception NegativeInteger
116 if n < 0 then raise NegativeInteger;
117 let rec aux = function
118 | 0 -> Datatypes.zero
119 | n -> Cic.Appl [ Datatypes.succ; (aux (n - 1)) ]
124 if n < 0 then raise NegativeInteger;
125 let rec aux = function
127 | 1 -> Reals.r1 (* to avoid trailing "+ 0" *)
128 | n -> Cic.Appl [ Reals.rplus; Reals.r1; (aux (n - 1)) ]