- hExtlib: added debugging information for split_nth

[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 470ab6b3f413d710ef4f502e3f4232c258da2587..ee7ed08d0eb37ac23b8cf204cc7823b0949aaf69 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
@@ -109,7 +125,7 @@ let ast_of_acic0 ~output_type term_info acic k =
     | Cic.AProd (id,n,s,t) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type _ -> `Pi
+          | `Set | `Type _ | `NType _ -> `Pi
           | `Prop | `CProp _ -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
@@ -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 =
@@ -470,7 +489,9 @@ let remove_interpretation id =
 
 let _ = load_patterns32 []
 
-let instantiate_appl_pattern env appl_pattern =
+let instantiate_appl_pattern 
+  ~mk_appl ~mk_implicit ~term_of_uri env appl_pattern 
+=
   let lookup name =
     try List.assoc name env
     with Not_found ->
@@ -478,10 +499,10 @@ let instantiate_appl_pattern env appl_pattern =
       assert false
   in
   let rec aux = function
-    | Ast.UriPattern uri -> CicUtil.term_of_uri uri
-    | Ast.ImplicitPattern -> Cic.Implicit None
+    | Ast.UriPattern uri -> term_of_uri uri
+    | Ast.ImplicitPattern -> mk_implicit false
     | Ast.VarPattern name -> lookup name
-    | Ast.ApplPattern terms -> Cic.Appl (List.map aux terms)
+    | Ast.ApplPattern terms -> mk_appl (List.map aux terms)
   in
   aux appl_pattern