X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=components%2Facic_content%2FtermAcicContent.ml;h=681f3cd541312e8dff3e86e475cfe3e89aa0db7d;hb=249d11773d32add20d665c4f8521b7380e4fec0a;hp=eaa53259021821dc3dc4b053f6eeffbfa160915d;hpb=673e954b37f3a23e73208c67267c7e9d31e3916d;p=helm.git

diff --git a/components/acic_content/termAcicContent.ml b/components/acic_content/termAcicContent.ml
index eaa532590..681f3cd54 100644
--- a/components/acic_content/termAcicContent.ml
+++ b/components/acic_content/termAcicContent.ml
@@ -70,7 +70,7 @@ let constructor_of_inductive_type uri i j =
 let left_params_no_of_inductive_type uri =
    snd (get_types uri)
 
-let ast_of_acic0 term_info acic k =
+let ast_of_acic0 ~output_type term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
   let register_uri id uri = Hashtbl.add id_to_uris id uri in
@@ -123,7 +123,7 @@ let ast_of_acic0 term_info acic k =
           k s, k t))
     | 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)) ->
+    | Cic.AAppl (aid,(Cic.AMutConstruct _ as he::tl as args)) as t ->
        let last_n n l =
          let rec aux =
           function
@@ -143,14 +143,17 @@ let ast_of_acic0 term_info acic k =
                idref aid (Ast.Appl (l@tl))
            | l -> idref aid (Ast.Appl l)
        in
-       let deannot_he = Deannotate.deannotate_term he in
-       if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
-       then
-         match CoercDb.is_a_coercion_to_funclass deannot_he with
-         | None -> idref aid (last_n 1 (List.map k tl))
-         | Some i -> idref aid (last_n (i+1) (List.map k tl))
-       else
-        idref aid (Ast.Appl (List.map k args))
+       (match LibraryObjects.destroy_nat t with
+       | Some n -> idref aid (Ast.Num (string_of_int n, -1))
+       | None ->
+           let deannot_he = Deannotate.deannotate_term he in
+           if CoercDb.is_a_coercion' deannot_he && !Acic2content.hide_coercions
+           then
+             (match CoercDb.is_a_coercion_to_funclass deannot_he with
+             | None -> idref aid (last_n 1 (List.map k tl))
+             | Some i -> idref aid (last_n (i+1) (List.map k tl)))
+           else
+             idref aid (Ast.Appl (List.map k args)))
     | Cic.AAppl (aid,args) ->
         idref aid (Ast.Appl (List.map k args))
     | Cic.AConst (id,uri,substs) ->
@@ -193,12 +196,21 @@ let ast_of_acic0 term_info acic k =
             List.map2
               (fun (name, ty) pat ->
                 incr j;
-                let (capture_variables, rhs) = eat_branch lpsno ty pat in
-                ((name, Some (ctor_puri !j), capture_variables), rhs))
-              constructors patterns
+                let name,(capture_variables,rhs) =
+                 match output_type with
+                    `Term -> name, eat_branch lpsno ty pat
+                  | `Pattern -> "_", ([], k pat)
+                in
+                 Ast.Pattern (name, Some (ctor_puri !j), capture_variables), rhs
+              ) constructors patterns
           with Invalid_argument _ -> assert false
         in
-        idref id (Ast.Case (k te, Some case_indty, Some (k ty), patterns))
+        let indty =
+         match output_type with
+            `Pattern -> None
+          | `Term -> Some case_indty
+        in
+        idref id (Ast.Case (k te, indty, Some (k ty), patterns))
     | Cic.AFix (id, no, funs) -> 
         let defs = 
           List.map
@@ -320,11 +332,12 @@ let instantiate32 term_info idrefs env symbol args =
   if args = [] then head
   else Ast.Appl (head :: List.map instantiate_arg args)
 
-let rec ast_of_acic1 term_info annterm = 
+let rec ast_of_acic1 ~output_type term_info annterm = 
   let id_to_uris = term_info.uri in
   let register_uri id uri = Hashtbl.add id_to_uris id uri in
   match (get_compiled32 ()) annterm with
-  | None -> ast_of_acic0 term_info annterm ast_of_acic1
+  | None ->
+     ast_of_acic0 ~output_type term_info annterm (ast_of_acic1 ~output_type)
   | Some (env, ctors, pid) -> 
       let idrefs =
         List.map
@@ -338,7 +351,8 @@ let rec ast_of_acic1 term_info annterm =
           ctors
       in
       let env' =
-        List.map (fun (name, term) -> (name, ast_of_acic1 term_info term)) env
+       List.map
+        (fun (name, term) -> name, ast_of_acic1 ~output_type term_info term) env
       in
       let _, symbol, args, _ =
         try
@@ -354,11 +368,11 @@ let load_patterns32 t =
   in
   set_compiled32 (lazy (Acic2astMatcher.Matcher32.compiler t))
 
-let ast_of_acic id_to_sort annterm =
+let ast_of_acic ~output_type id_to_sort annterm =
   debug_print (lazy ("ast_of_acic <- "
     ^ CicPp.ppterm (Deannotate.deannotate_term annterm)));
   let term_info = { sort = id_to_sort; uri = Hashtbl.create 211 } in
-  let ast = ast_of_acic1 term_info annterm in
+  let ast = ast_of_acic1 ~output_type term_info annterm in
   debug_print (lazy ("ast_of_acic -> " ^ CicNotationPp.pp_term ast));
   ast, term_info.uri