X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FtermAcicContent.ml;h=ee7ed08d0eb37ac23b8cf204cc7823b0949aaf69;hb=2b837ca9e298eb44eee95d9ca0e331c577785dcb;hp=508411d2847b1b84083141efa5bbe14aed16a8fa;hpb=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git

diff --git a/helm/software/components/acic_content/termAcicContent.ml b/helm/software/components/acic_content/termAcicContent.ml
index 508411d28..ee7ed08d0 100644
--- 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
@@ -135,7 +151,7 @@ let ast_of_acic0 ~output_type term_info acic k =
              | Some (_,_,_,sats,cpos) -> 
                  if cpos < List.length tl then
                    let _,rest = 
-                     try HExtlib.split_nth (cpos+sats+1) tl with Failure _ -> [],[] 
+                     try HExtlib.split_nth "TAC 1" (cpos+sats+1) tl with Failure _ -> [],[] 
                    in
                    if rest = [] then
                      idref aid (List.nth (List.map k tl) cpos)
@@ -442,19 +458,22 @@ let set_active_interpretations ids =
 
 exception Interpretation_not_found
 
-let lookup_interpretations symbol =
+let lookup_interpretations ?(sorted=true) symbol =
   try
-   HExtlib.list_uniq
-    (List.sort Pervasives.compare
-     (List.map
-      (fun id ->
-        let (dsc, _, args, appl_pattern) =
-          try
-            Hashtbl.find !level2_patterns32 id
-          with Not_found -> assert false 
-        in
-        dsc, args, appl_pattern)
-      !(Hashtbl.find !interpretations symbol)))
+    let raw = 
+      List.map (
+        fun id ->
+          let (dsc, _, args, appl_pattern) =
+            try
+              Hashtbl.find !level2_patterns32 id
+            with Not_found -> assert false 
+          in
+          dsc, args, appl_pattern
+      )
+      !(Hashtbl.find !interpretations symbol)
+    in
+    if sorted then HExtlib.list_uniq (List.sort Pervasives.compare raw)
+              else raw
   with Not_found -> raise Interpretation_not_found
 
 let remove_interpretation id =