- libraryObjects: new default "natural numbers" with the uri of nat.

[helm.git] / helm / software / components / acic_content / termAcicContent.ml

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index c350f38c41ab03c6a735643e676d2e53809e1009..fb890915298b5bb70846c1cc01e1337e56c3ba5f 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -28,6 +28,7 @@
 open Printf
 
 module Ast = CicNotationPt
+module Obj = LibraryObjects
 
 let debug = false
 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
@@ -70,6 +71,21 @@ let constructor_of_inductive_type uri i j =
 let left_params_no_of_inductive_type uri =
    snd (get_types uri)
 
+let destroy_nat annterm =
+  let is_zero = function
+    | Cic.AMutConstruct (_, uri, 0, 1, _) when Obj.is_nat_URI uri -> true
+    | _ -> false
+  in
+  let is_succ = function
+    | Cic.AMutConstruct (_, uri, 0, 2, _) when Obj.is_nat_URI uri -> true
+    | _ -> false
+  in
+  let rec aux acc = function
+    | Cic.AAppl (_, [he ; tl]) when is_succ he -> aux (acc + 1) tl
+    | t when is_zero t -> Some acc
+    | _ -> None in
+  aux 0 annterm
+
 let ast_of_acic0 ~output_type term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
@@ -124,7 +140,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AAppl (aid,(Cic.AConst _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutInd _ as he::tl as args))
     | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t ->
-       (match LibraryObjects.destroy_nat t with
+       (match destroy_nat t with
        | Some n -> idref aid (Ast.Num (string_of_int n, -1))
        | None ->
            let deannot_he = Deannotate.deannotate_term he in