New content level representations for LetRec, Inductive and CoInductive.

[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 fddd777f7e13959fac65a76ff202f40ae23f4738..cda76ce0914e44ccaae48e2f716fba326a9b8346 100644 (file)
--- a/helm/software/components/acic_content/termAcicContent.ml
+++ b/helm/software/components/acic_content/termAcicContent.ml
@@ -66,6 +66,7 @@ let constructor_of_inductive_type uri i j =
     fst (List.nth (constructors_of_inductive_type uri i) (j-1))
   with Not_found -> assert false)
 
+
 let ast_of_acic0 term_info acic k =
   let k = k term_info in
   let id_to_uris = term_info.uri in
@@ -117,7 +118,38 @@ let ast_of_acic0 term_info acic k =
     | Cic.ALetIn (id,n,s,t) ->
         idref id (Ast.LetIn ((CicNotationUtil.name_of_cic_name n, None),
           k s, k t))
-    | Cic.AAppl (aid,args) -> idref aid (Ast.Appl (List.map k args))
+    | 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)) ->
+       let last_n n l =
+         let rec aux =
+          function
+             [] -> assert false
+           | [_] as l -> l,1
+           | he::tl ->
+              let (res,len) as res' = aux tl in
+               if len < n then
+                he::res,len + 1
+               else
+                res'
+         in
+          match fst (aux l) with
+             [] -> assert false
+           | [t] -> t
+           | Ast.AttributedTerm (_,(Ast.Appl l))::tl -> 
+               idref aid (Ast.Appl (l@tl))
+           | l -> idref aid (Ast.Appl l)
+       in
+       let deannot_he = Deannotate.deannotate_term he in
+       if CoercGraph.is_a_coercion deannot_he && !Acic2content.hide_coercions
+       then
+         match CoercGraph.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) ->
         register_uri id uri;
         idref id (Ast.Ident (UriManager.name_of_uri uri, aux_substs substs))
@@ -166,28 +198,72 @@ let ast_of_acic0 term_info acic k =
         let defs = 
           List.map
             (fun (_, n, decr_idx, ty, bo) ->
-              ((Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
+              let params,bo =
+               let rec aux =
+                function
+                   Cic.ALambda (_,name,so,ta) ->
+                    let params,rest = aux ta in
+                     (CicNotationUtil.name_of_cic_name name,Some (k so))::
+                      params, rest
+                 | t -> [],t
+               in
+                aux bo
+              in
+              let ty =
+               let rec eat_pis =
+                function
+                   0,ty -> ty
+                 | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+                 | n,ty ->
+                    (* I should do a whd here, but I have no context *)
+                    assert false
+               in
+                eat_pis ((List.length params),ty)
+              in
+               (params,(Ast.Ident (n, None), Some (k ty)), k bo, decr_idx))
             funs
         in
         let name =
           try
             (match List.nth defs no with
-            | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+            | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
             | _ -> assert false)
           with Not_found -> assert false
         in
-        idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
+         idref id (Ast.LetRec (`Inductive, defs, Ast.Ident (name, None)))
     | Cic.ACoFix (id, no, funs) -> 
         let defs = 
           List.map
             (fun (_, n, ty, bo) ->
-              ((Ast.Ident (n, None), Some (k ty)), k bo, 0))
+              let params,bo =
+               let rec aux =
+                function
+                   Cic.ALambda (_,name,so,ta) ->
+                    let params,rest = aux ta in
+                     (CicNotationUtil.name_of_cic_name name,Some (k so))::
+                      params, rest
+                 | t -> [],t
+               in
+                aux bo
+              in
+              let ty =
+               let rec eat_pis =
+                function
+                   0,ty -> ty
+                 | n,Cic.AProd (_,_,_,ta) -> eat_pis (n - 1,ta)
+                 | n,ty ->
+                    (* I should do a whd here, but I have no context *)
+                    assert false
+               in
+                eat_pis ((List.length params),ty)
+              in
+               (params,(Ast.Ident (n, None), Some (k ty)), k bo, 0))
             funs
         in
         let name =
           try
             (match List.nth defs no with
-            | (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
+            | _, (Ast.Ident (n, _), _), _, _ when n <> "_" -> n
             | _ -> assert false)
           with Not_found -> assert false
         in