Multiple Prod branches did not have their inner-sorts computed properly.

[helm.git] / helm / gTopLevel / cic2acic.ml

diff --git a/helm/gTopLevel/cic2acic.ml b/helm/gTopLevel/cic2acic.ml
index 8d849634dd0726fba35c6f0aaca9c3b7e1b92e89..c18e7d6a684f7ba143a08cbebe12cd67fc59edbb 100644 (file)
--- a/helm/gTopLevel/cic2acic.ml
+++ b/helm/gTopLevel/cic2acic.ml
@@ -23,8 +23,6 @@
  * http://cs.unibo.it/helm/.
  *)
 
-exception NotImplemented;;
-
 type anntypes =
  {annsynthesized : Cic.annterm ; annexpected : Cic.annterm option}
 ;;
@@ -43,6 +41,8 @@ let fresh_id seed ids_to_terms ids_to_father_ids =
    res
 ;;
 
+let source_id_of_id id = "#source#" ^ id;;
+
 exception NotEnoughElements;;
 exception NameExpected;;
 
@@ -169,27 +169,33 @@ let acic_of_cic_context' seed ids_to_terms ids_to_father_ids ids_to_inner_sorts
           | C.Prod (n,s,t) ->
               Hashtbl.add ids_to_inner_sorts fresh_id''
                (string_of_sort innertype) ;
-              C.AProd
-               (fresh_id'', n, aux' context idrefs s,
-                aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
+                   let sourcetype = T.type_of_aux' metasenv context s in
+                    Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+                     (string_of_sort sourcetype) ;
+               C.AProd
+                (fresh_id'', n, aux' context idrefs s,
+                 aux' ((Some (n, C.Decl s))::context) (fresh_id''::idrefs) t)
           | C.Lambda (n,s,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
-             if innersort = "Prop" then
-              begin
-               let father_is_lambda =
-                match father with
-                   None -> false
-                 | Some father' ->
-                    match Hashtbl.find ids_to_terms father' with
-                       C.Lambda _ -> true
-                     | _ -> false
-               in
-                if (not father_is_lambda) || expected_available then
-                 add_inner_type fresh_id''
-              end ;
-             C.ALambda
-              (fresh_id'',n, aux' context idrefs s,
-               aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
+                  let sourcetype = T.type_of_aux' metasenv context s in
+                   Hashtbl.add ids_to_inner_sorts (source_id_of_id fresh_id'')
+                    (string_of_sort sourcetype) ;
+              if innersort = "Prop" then
+               begin
+                let father_is_lambda =
+                 match father with
+                    None -> false
+                  | Some father' ->
+                     match Hashtbl.find ids_to_terms father' with
+                        C.Lambda _ -> true
+                      | _ -> false
+                in
+                 if (not father_is_lambda) || expected_available then
+                  add_inner_type fresh_id''
+               end ;
+              C.ALambda
+               (fresh_id'',n, aux' context idrefs s,
+                aux' ((Some (n, C.Decl s)::context)) (fresh_id''::idrefs) t)
           | C.LetIn (n,s,t) ->
              Hashtbl.add ids_to_inner_sorts fresh_id'' innersort ;
              if innersort = "Prop" then
@@ -303,8 +309,19 @@ let acic_object_of_cic_object obj =
        let aty = acic_term_of_cic_term' ty None in
         C.AConstant
          ("mettereaposto",Some "mettereaposto2",id,Some abo,aty, params)
-    | C.Constant (id,None,ty,params) -> raise NotImplemented
-    | C.Variable (id,bo,ty,params) -> raise NotImplemented
+    | C.Constant (id,None,ty,params) ->
+       let aty = acic_term_of_cic_term' ty None in
+        C.AConstant
+         ("mettereaposto",None,id,None,aty, params)
+    | C.Variable (id,bo,ty,params) ->
+       let abo =
+        match bo with
+           None -> None
+         | Some bo -> Some (acic_term_of_cic_term' bo (Some ty))
+       in
+       let aty = acic_term_of_cic_term' ty None in
+        C.AVariable
+         ("mettereaposto",id,abo,aty, params)
     | C.CurrentProof (id,conjectures,bo,ty,params) ->
        let aconjectures =
         List.map
@@ -357,7 +374,25 @@ let acic_object_of_cic_object obj =
        let aty = acic_term_of_cic_term_context' conjectures [] [] ty None in
         C.ACurrentProof
          ("mettereaposto","mettereaposto2",id,aconjectures,abo,aty,params)
-    | C.InductiveDefinition (tys,params,paramsno) -> raise NotImplemented
+    | C.InductiveDefinition (tys,params,paramsno) ->
+       let context =
+        List.map
+         (fun (name,_,arity,_) -> Some (C.Name name, C.Decl arity)) tys in
+       let idrefs = List.map (function _ -> gen_id seed) tys in
+       let atys =
+        List.map2
+         (fun id (name,inductive,ty,cons) ->
+           let acons =
+            List.map
+             (function (name,ty) ->
+               (name,
+                 acic_term_of_cic_term_context' [] context idrefs ty None)
+             ) cons
+           in
+            (id,name,inductive,acic_term_of_cic_term' ty None,acons)
+         ) (List.rev idrefs) tys
+       in
+        C.AInductiveDefinition ("mettereaposto",atys,params,paramsno)
    in
     aobj,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts,ids_to_inner_types,
      ids_to_conjectures,ids_to_hypotheses