X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_omdoc%2Fcic2content.ml;h=61003f930fbca68abc1515a78acf92122659e9d2;hb=d3c72d6856cd185e5b3e9f2e8b928b78c7031ed1;hp=614848706f5110a6398937d9548a5d305038c8cc;hpb=caf8d6cf32c9a9ec8d3fba0aa912d080ff5f7d52;p=helm.git

diff --git a/helm/ocaml/cic_omdoc/cic2content.ml b/helm/ocaml/cic_omdoc/cic2content.ml
index 614848706..61003f930 100644
--- a/helm/ocaml/cic_omdoc/cic2content.ml
+++ b/helm/ocaml/cic_omdoc/cic2content.ml
@@ -28,7 +28,7 @@
 (*                           PROJECT HELM                                 *)
 (*                                                                        *)
 (*                Andrea Asperti <asperti@cs.unibo.it>                    *)
-(*                             16/62003                                   *)
+(*                             16/6/2003                                   *)
 (*                                                                        *)
 (**************************************************************************)
 
@@ -70,7 +70,7 @@ let rec occur uri =
     | C.Var _ -> false
     | C.Meta _ -> false
     | C.Sort _ -> false
-    | C.Implicit -> raise NotImplemented
+    | C.Implicit _ -> assert false
     | C.Prod (_,s,t) -> (occur uri s) or (occur uri t)
     | C.Cast (te,ty) -> (occur uri te)
     | C.Lambda (_,s,t) -> (occur uri s) or (occur uri t) (* or false ?? *)
@@ -537,18 +537,37 @@ and acic2content seed ?name ~ids_to_inner_sorts ~ids_to_inner_types t =
           generate_exact seed t id name ~ids_to_inner_types
         else raise Not_a_proof
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
-        let inductive_types =
+        let inductive_types,noparams =
            (match CicEnvironment.get_obj uri with
                Cic.Constant _ -> assert false
              | Cic.Variable _ -> assert false
              | Cic.CurrentProof _ -> assert false
-             | Cic.InductiveDefinition (l,_,_) -> l 
+             | Cic.InductiveDefinition (l,_,n) -> l,n 
            ) in
-        let (_,_,_,constructors) = List.nth inductive_types typeno in 
+        let (_,_,_,constructors) = List.nth inductive_types typeno in
+        let name_and_arities = 
+          let rec count_prods =
+            function 
+               C.Prod (_,_,t) -> 1 + count_prods t
+             | _ -> 0 in
+          List.map 
+            (function (n,t) -> Some n,((count_prods t) - noparams)) constructors in
+        let pp = 
+          let build_proof p (name,arity) =
+            let rec make_context_and_body c p n =
+              if n = 0 then c,(aux p)
+              else 
+                (match p with
+                   Cic.ALambda(idl,vname,s1,t1) ->
+                     let ce = 
+                       build_decl_item seed idl vname s1 ~ids_to_inner_sorts in
+                     make_context_and_body (ce::c) t1 (n-1)
+                   | _ -> assert false) in
+             let context,body = make_context_and_body [] p arity in
+               K.ArgProof
+                {body with K.proof_name = name; K.proof_context=context} in
+          List.map2 build_proof patterns name_and_arities in
         let teid = get_id te in
-        let pp = List.map2 
-          (fun p (name,_) -> (K.ArgProof (aux ~name p))) 
-           patterns constructors in
         let context,term =
           (match 
              build_subproofs_and_args 
@@ -850,6 +869,42 @@ let map_conjectures
   (id,n,context',ty)
 ;;
 
+(* map_sequent is similar to map_conjectures, but the for the hid
+of the hypothesis, which are preserved instead of generating
+fresh ones. We shall have to adopt a uniform policy, soon or later *)
+
+let map_sequent ((id,n,context,ty):Cic.annconjecture) =
+ let module K = Content in
+ let context' =
+  List.map
+   (function
+       (id,None) -> None
+     | (id,Some (name,Cic.ADecl t)) ->
+         Some
+          (* We should call build_decl_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration      *)
+          (`Declaration
+            { K.dec_name = name_of name;
+              K.dec_id = id; 
+              K.dec_inductive = false;
+              K.dec_aref = get_id t;
+              K.dec_type = t
+            })
+     | (id,Some (name,Cic.ADef t)) ->
+         Some
+          (* We should call build_def_item, but we have not computed *)
+          (* the inner-types ==> we always produce a declaration     *)
+          (`Definition
+             { K.def_name = name_of name;
+               K.def_id = id; 
+               K.def_aref = get_id t;
+               K.def_term = t
+             })
+   ) context
+ in
+  (id,n,context',ty)
+;;
+
 let rec annobj2content ~ids_to_inner_sorts ~ids_to_inner_types = 
   let module C = Cic in
   let module K = Content in