From 3bec2787ed93cd8132d25233ebfb3de275c20a47 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Mon, 19 Jan 2004 11:38:41 +0000 Subject: [PATCH] added Peano module and functions to create natural/real terms --- helm/ocaml/cic/helmLibraryObjects.ml | 37 ++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml index 2d4938181..1d7e9285e 100644 --- a/helm/ocaml/cic/helmLibraryObjects.ml +++ b/helm/ocaml/cic/helmLibraryObjects.ml @@ -1,4 +1,6 @@ +(** {2 Auxiliary functions} *) + let uri = UriManager.uri_of_string let const ?(subst = []) uri = Cic.Const (uri, subst) @@ -6,6 +8,8 @@ let var ?(subst = []) uri = Cic.Var (uri, subst) let mutconstruct ?(subst = []) uri typeno consno = Cic.MutConstruct (uri, typeno, consno, subst) +(** {2 Helm's objects shorthands} *) + module Logic = struct let eq_URI = uri "cic:/Coq/Init/Logic/eq.ind" @@ -52,3 +56,36 @@ module Reals = let rtheory = const rtheory_URI end +module Peano = + struct + let plus_URI = uri "cic:/Coq/Init/Peano/plus.con" + let mult_URI = uri "cic:/Coq/Init/Peano/mult.con" + let pred_URI = uri "cic:/Coq/Init/Peano/pred.con" + + let plus = const plus_URI + let mult = const mult_URI + let pred = const pred_URI + end + +(** {2 Helpers for creating common terms} + * (e.g. numbers)} *) + +exception NegativeInteger + +let build_nat n = + if n < 0 then raise NegativeInteger; + let rec aux = function + | 0 -> Datatypes.zero + | n -> Cic.Appl [ Datatypes.succ; (aux (n - 1)) ] + in + aux n + +let build_real n = + if n < 0 then raise NegativeInteger; + let rec aux = function + | 0 -> Reals.r0 + | 1 -> Reals.r1 (* to avoid trailing "+ 0" *) + | n -> Cic.Appl [ Reals.rplus; Reals.r1; (aux (n - 1)) ] + in + aux n + -- 2.39.2