(* Copyright (C) 2000, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

(**************************************************************************)
(*                                                                        *)
(*                           PROJECT HELM                                 *)
(*                                                                        *)
(*                Andrea Asperti <asperti@cs.unibo.it>                    *)
(*                             16/62003                                   *)
(*                                                                        *)
(**************************************************************************)

(* e se mettessi la conversione di BY nell'apply_context ? *)
(* sarebbe carino avere l'invariante che la proof2pres
generasse sempre prove con contesto vuoto *)
 
let gen_id seed =
 let res = "p" ^ string_of_int !seed in
  incr seed ;
  res
;;

let name_of = function
    Cic.Anonymous -> None
  | Cic.Name b -> Some b;;
 
exception Not_a_proof;;
exception NotImplemented;;
exception NotApplicable;;
   
(* we do not care for positivity, here, that in any case is enforced by
   well typing. Just a brutal search *)

let rec occur uri = 
  let module C = Cic in
  function
      C.Rel _ -> false
    | C.Var _ -> false
    | C.Meta _ -> false
    | C.Sort _ -> false
    | C.Implicit -> raise NotImplemented
    | 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 ?? *)
    | C.LetIn (_,s,t) -> (occur uri s) or (occur uri t)
    | C.Appl l -> 
        List.fold_left 
          (fun b a -> 
             if b then b  
             else (occur uri a)) false l
    | C.Const (_,_) -> false
    | C.MutInd (uri1,_,_) -> if uri = uri1 then true else false
    | C.MutConstruct (_,_,_,_) -> false
    | C.MutCase _ -> false (* presuming too much?? *)
    | C.Fix _ -> false (* presuming too much?? *)
    | C.CoFix (_,_) -> false (* presuming too much?? *)
;;

let get_id = 
  let module C = Cic in
  function
      C.ARel (id,_,_,_) -> id
    | C.AVar (id,_,_) -> id
    | C.AMeta (id,_,_) -> id
    | C.ASort (id,_) -> id
    | C.AImplicit _ -> raise NotImplemented
    | C.AProd (id,_,_,_) -> id
    | C.ACast (id,_,_) -> id
    | C.ALambda (id,_,_,_) -> id
    | C.ALetIn (id,_,_,_) -> id
    | C.AAppl (id,_) -> id
    | C.AConst (id,_,_) -> id
    | C.AMutInd (id,_,_,_) -> id
    | C.AMutConstruct (id,_,_,_,_) -> id
    | C.AMutCase (id,_,_,_,_,_) -> id
    | C.AFix (id,_,_) -> id
    | C.ACoFix (id,_,_) -> id
;;

let test_for_lifting ~ids_to_inner_types = 
  let module C = Cic in
  let module C2A = Cic2acic in
  (* atomic terms are never lifted, according to my policy *)
  function
      C.ARel (id,_,_,_) -> false
    | C.AVar (id,_,_) -> false
    | C.AMeta (id,_,_) -> false
    | C.ASort (id,_) -> false
    | C.AImplicit _ -> raise NotImplemented
    | C.AProd (id,_,_,_) -> false
    | C.ACast (id,_,_) -> 
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
    | C.ALambda (id,_,_,_) -> 
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
    | C.ALetIn (id,_,_,_) -> 
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
    | C.AAppl (id,_) ->
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false) 
    | C.AConst (id,_,_) -> 
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false) 
    | C.AMutInd (id,_,_,_) -> false
    | C.AMutConstruct (id,_,_,_,_) -> 
       (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
        (* oppure: false *)
    | C.AMutCase (id,_,_,_,_,_) ->
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
    | C.AFix (id,_,_) ->
          (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
    | C.ACoFix (id,_,_) ->
         (try 
            ignore (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized;
            true;
          with notfound -> false)
;;

let build_args seed l subproofs ~ids_to_inner_types ~ids_to_inner_sorts =
  let module C = Cic in
  let module K = Content in
  let rec aux l subrpoofs =
    match l with
      [] -> []
    | t::l1 -> 
        if (test_for_lifting t ~ids_to_inner_types) then
          (match subproofs with
             [] -> assert false
           | p::tl -> 
              let new_arg = 
                K.Premise
                  { K.premise_id = gen_id seed;
                    K.premise_xref = p.K.proof_id;
                    K.premise_binder = p.K.proof_name;
                    K.premise_n = None
                  }
                in new_arg::(aux l1 tl))
        else 
          let hd = 
            (match t with 
               C.ARel (idr,idref,n,b) ->
                 let sort = 
                   (try Hashtbl.find ids_to_inner_sorts idr 
                    with notfound -> "Type") in 
                 if sort ="Prop" then 
                    K.Premise 
                      { K.premise_id = gen_id seed;
                        K.premise_xref = idr;
                        K.premise_binder = Some b;
                        K.premise_n = Some n
                      }
                 else (K.Term t)
             | _ -> (K.Term t)) in 
          hd::(aux l1 subproofs)
  in aux l subproofs
;;

(* transform a proof p into a proof list, concatenating the last 
conclude element to the apply_context list, in case context is
empty. Otherwise, it just returns [p] *)

let flat seed p = 
 let module K = Content in
  if (p.K.proof_context = []) then
    if p.K.proof_apply_context = [] then [p]
    else 
      let p1 =
        { p with
          K.proof_id = gen_id seed;
          K.proof_context = []; 
          K.proof_apply_context = []
        } in
      p.K.proof_apply_context@[p1]
  else 
    [p]
;;

let rec serialize seed = 
  function 
      [] -> []
    | p::tl -> (flat seed p)@(serialize seed tl);;

(* top_down = true if the term is a LAMBDA or a decl *)
let generate_conversion seed top_down id inner_proof ~ids_to_inner_types =
 let module C2A = Cic2acic in
 let module K = Content in
 let exp = (try ((Hashtbl.find ids_to_inner_types id).C2A.annexpected)
            with Not_found -> None)
 in
 match exp with
     None -> inner_proof
   | Some expty ->
       if inner_proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
         { K.proof_name = None ;
            K.proof_id   = gen_id seed;
            K.proof_context = [] ;
            K.proof_apply_context = [];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "TD_Conversion";
                K.conclude_args = [K.ArgProof inner_proof];
                K.conclude_conclusion = Some expty
              };
          }
        else
          { K.proof_name = None ;
            K.proof_id   = gen_id seed;
            K.proof_context = [] ;
            K.proof_apply_context = [inner_proof];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "BU_Conversion";
                K.conclude_args =  
                 [K.Premise 
                  { K.premise_id = gen_id seed;
                    K.premise_xref = inner_proof.K.proof_id; 
                    K.premise_binder = None;
                    K.premise_n = None
                  } 
                 ]; 
                K.conclude_conclusion = Some expty
              };
          }
;;

let generate_exact seed t id name ~ids_to_inner_types =
  let module C2A = Cic2acic in
  let module K = Content in
    { K.proof_name = name;
      K.proof_id   = id ;
      K.proof_context = [] ;
      K.proof_apply_context = [];
      K.proof_conclude = 
        { K.conclude_id = gen_id seed; 
          K.conclude_aref = id;
          K.conclude_method = "Exact";
          K.conclude_args = [K.Term t];
          K.conclude_conclusion = 
              try Some (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
              with notfound -> None
        };
    }
;;

let generate_intros_let_tac seed id n s is_intro inner_proof name ~ids_to_inner_types =
  let module C2A = Cic2acic in
  let module C = Cic in
  let module K = Content in
    { K.proof_name = name;
      K.proof_id   = id ;
      K.proof_context = [] ;
      K.proof_apply_context = [];
      K.proof_conclude = 
        { K.conclude_id = gen_id seed; 
          K.conclude_aref = id;
          K.conclude_method = "Intros+LetTac";
          K.conclude_args = [K.ArgProof inner_proof];
          K.conclude_conclusion = 
            try Some 
             (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
            with notfound -> 
              (match inner_proof.K.proof_conclude.K.conclude_conclusion with
                 None -> None
              | Some t -> 
                  if is_intro then Some (C.AProd ("gen"^id,n,s,t))
                  else Some (C.ALetIn ("gen"^id,n,s,t)))
        };
    }
;;

let build_decl_item seed id n s ~ids_to_inner_sorts =
 let module K = Content in
  let sort = Hashtbl.find ids_to_inner_sorts (Cic2acic.source_id_of_id id) in
  if sort = "Prop" then
     `Hypothesis
       { K.dec_name = name_of n;
         K.dec_id = gen_id seed; 
         K.dec_inductive = false;
         K.dec_aref = id;
         K.dec_type = s
       }
  else 
     `Declaration
       { K.dec_name = name_of n;
         K.dec_id = gen_id seed; 
         K.dec_inductive = false;
         K.dec_aref = id;
         K.dec_type = s
       }
;;

let rec build_def_item seed id n t ~ids_to_inner_sorts ~ids_to_inner_types =
 let module K = Content in
  let sort = Hashtbl.find ids_to_inner_sorts id in
  if sort = "Prop" then
     `Proof (acic2content seed ~name:(name_of n) ~ids_to_inner_sorts  ~ids_to_inner_types t)
  else 
     `Definition
       { K.def_name = name_of n;
         K.def_id = gen_id seed; 
         K.def_aref = id;
         K.def_term = t
       }

(* the following function must be called with an object of sort
Prop. For debugging purposes this is tested again, possibly raising an 
Not_a_proof exception *)

and acic2content seed ?(name = None) ~ids_to_inner_sorts ~ids_to_inner_types t =
  let rec aux ?(name = None) t =
  let module C = Cic in
  let module K = Content in
  let module C2A = Cic2acic in
  let t1 =
    match t with 
      C.ARel (id,idref,n,b) as t ->
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then
          generate_exact seed t id name ~ids_to_inner_types 
        else raise Not_a_proof
    | C.AVar (id,uri,exp_named_subst) as t ->
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then
          generate_exact seed t id name ~ids_to_inner_types 
        else raise Not_a_proof
    | C.AMeta (id,n,l) as t ->
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then
          generate_exact seed t id name ~ids_to_inner_types 
        else raise Not_a_proof
    | C.ASort (id,s) -> raise Not_a_proof
    | C.AImplicit _ -> raise NotImplemented
    | C.AProd (_,_,_,_) -> raise Not_a_proof
    | C.ACast (id,v,t) -> aux v
    | C.ALambda (id,n,s,t) -> 
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then 
          let proof = aux t ~name:None in
          let proof' = 
            if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
               match proof.K.proof_conclude.K.conclude_args with
                 [K.ArgProof p] -> p
               | _ -> assert false                  
            else proof in
          let proof'' =
            { proof' with
              K.proof_name = None;
              K.proof_context = 
                (build_decl_item seed id n s ids_to_inner_sorts)::
                  proof'.K.proof_context
            }
          in
          generate_intros_let_tac seed id n s true proof'' name ~ids_to_inner_types
        else raise Not_a_proof 
    | C.ALetIn (id,n,s,t) ->
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then 
          let proof = aux t in
          let proof' = 
            if proof.K.proof_conclude.K.conclude_method = "Intros+LetTac" then
               match proof.K.proof_conclude.K.conclude_args with
                 [K.ArgProof p] -> p
               | _ -> assert false                  
            else proof in
          let proof'' =
            { proof' with
               K.proof_name = name;
               K.proof_context = 
                 ((build_def_item seed id n s ids_to_inner_sorts 
                   ids_to_inner_types):> Cic.annterm K.in_proof_context_element)
                 ::proof'.K.proof_context;
            }
          in
          generate_intros_let_tac seed id n s false proof'' name ~ids_to_inner_types
        else raise Not_a_proof 
    | C.AAppl (id,li) ->
        (try rewrite 
           seed name id li ids_to_inner_types ids_to_inner_sorts
         with NotApplicable ->
         try inductive 
          seed name id li ids_to_inner_types ids_to_inner_sorts
         with NotApplicable ->
          let args_to_lift = 
            List.filter (test_for_lifting ~ids_to_inner_types) li in
          let subproofs = 
            match args_to_lift with
                [_] -> List.map aux args_to_lift 
            | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
          let args = build_args seed li subproofs 
                 ~ids_to_inner_types ~ids_to_inner_sorts in
            { K.proof_name = name;
              K.proof_id   = gen_id seed;
              K.proof_context = [];
              K.proof_apply_context = serialize seed subproofs;
              K.proof_conclude = 
                { K.conclude_id = gen_id seed;
                  K.conclude_aref = id;
                  K.conclude_method = "Apply";
                  K.conclude_args = args;
                  K.conclude_conclusion = 
                     try Some 
                       (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                     with notfound -> None
                 };
            })
    | C.AConst (id,uri,exp_named_subst) as t ->
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then
          generate_exact seed t id name ~ids_to_inner_types
        else raise Not_a_proof
    | C.AMutInd (id,uri,i,exp_named_subst) -> raise Not_a_proof
    | C.AMutConstruct (id,uri,i,j,exp_named_subst) as t ->
        let sort = Hashtbl.find ids_to_inner_sorts id in
        if sort = "Prop" then 
          generate_exact seed t id name ~ids_to_inner_types
        else raise Not_a_proof
    | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
        let teid = get_id te in
        let pp = List.map (function p -> (K.ArgProof (aux p))) patterns in
        (match 
          (try Some (Hashtbl.find ids_to_inner_types teid).C2A.annsynthesized
           with notfound -> None)
         with
             Some tety -> (* we must lift up the argument *)
               let p = (aux te) in
               { K.proof_name = Some "name";
                 K.proof_id   = gen_id seed;
                 K.proof_context = []; 
                 K.proof_apply_context = flat seed p;
                 K.proof_conclude = 
                   { K.conclude_id = gen_id seed; 
                     K.conclude_aref = id;
                     K.conclude_method = "Case";
                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
                     K.conclude_conclusion = 
                       try Some 
                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                       with notfound -> None  
                   }
               }
           | None ->
               { K.proof_name = name;
                 K.proof_id   = gen_id seed;
                 K.proof_context = []; 
                 K.proof_apply_context = [];
                 K.proof_conclude = 
                   { K.conclude_id = gen_id seed; 
                     K.conclude_aref = id;
                     K.conclude_method = "Case";
                     K.conclude_args = (K.Term ty)::(K.Term te)::pp;
                     K.conclude_conclusion = 
                       try Some 
                        (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                       with notfound -> None 
                   }
               }
         )  
    | C.AFix (id, no, [(id1,n,_,ty,bo)]) -> 
        let proof = (aux bo) in (* must be recursive !! *)
          { K.proof_name = name;
            K.proof_id   = gen_id seed;
            K.proof_context = [`Proof proof]; 
            K.proof_apply_context = [];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "Exact";
                K.conclude_args =
                [ K.Premise
                  { K.premise_id = gen_id seed; 
                    K.premise_xref = proof.K.proof_id;
                    K.premise_binder = proof.K.proof_name;
                    K.premise_n = Some 1;
                  }
                ];
                K.conclude_conclusion =
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                   with notfound -> None
              }
        }
    | C.AFix (id, no, funs) -> 
        let proofs = 
          List.map (function (id1,n,_,ty,bo) -> (`Proof (aux bo))) funs in
        let jo = 
          { K.joint_id = gen_id seed;
            K.joint_kind = `Recursive;
            K.joint_defs = proofs
          } 
        in
          { K.proof_name = name;
            K.proof_id   = gen_id seed;
            K.proof_context = [`Joint jo]; 
            K.proof_apply_context = [];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "Exact";
                K.conclude_args =
                [ K.Premise
                  { K.premise_id = gen_id seed; 
                    K.premise_xref = jo.K.joint_id;
                    K.premise_binder = Some "tiralo fuori";
                    K.premise_n = Some no;
                  }
                ];
                K.conclude_conclusion =
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                   with notfound -> None
              }
        } 
    | C.ACoFix (id,no,[(id1,n,ty,bo)]) -> 
        let proof = (aux bo) in (* must be recursive !! *)
          { K.proof_name = name;
            K.proof_id   = gen_id seed;
            K.proof_context = [`Proof proof]; 
            K.proof_apply_context = [];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "Exact";
                K.conclude_args =
                [ K.Premise
                  { K.premise_id = gen_id seed; 
                    K.premise_xref = proof.K.proof_id;
                    K.premise_binder = proof.K.proof_name;
                    K.premise_n = Some 1;
                  }
                ];
                K.conclude_conclusion =
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                   with notfound -> None
              }
        } 
    | C.ACoFix (id,no,funs) -> 
        let proofs = 
          List.map (function (id1,n,ty,bo) -> (`Proof (aux bo))) funs in
        let jo = 
          { K.joint_id = gen_id seed;
            K.joint_kind = `Recursive;
            K.joint_defs = proofs
          } 
        in
          { K.proof_name = name;
            K.proof_id   = gen_id seed;
            K.proof_context = [`Joint jo]; 
            K.proof_apply_context = [];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "Exact";
                K.conclude_args =
                [ K.Premise
                  { K.premise_id = gen_id seed; 
                    K.premise_xref = jo.K.joint_id;
                    K.premise_binder = Some "tiralo fuori";
                    K.premise_n = Some no;
                  }
                ];
                K.conclude_conclusion =
                  try Some 
                    (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                  with notfound -> None
              };
        } 
     in 
     let id = get_id t in
     generate_conversion seed false id t1 ~ids_to_inner_types
in aux ~name:name t

and inductive seed name id li ids_to_inner_types ids_to_inner_sorts =
  let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
  let module C2A = Cic2acic in
  let module K = Content in
  let module C = Cic in
  match li with 
    C.AConst (idc,uri,exp_named_subst)::args ->
      let uri_str = UriManager.string_of_uri uri in
      let suffix = Str.regexp_string "_ind.con" in
      let len = String.length uri_str in 
      let n = (try (Str.search_backward suffix uri_str len)
               with Not_found -> -1) in
      if n<0 then raise NotApplicable
      else 
        let prefix = String.sub uri_str 0 n in
        let ind_str = (prefix ^ ".ind") in 
        let ind_uri = UriManager.uri_of_string ind_str in
        let inductive_types,noparams =
           (match CicEnvironment.get_obj ind_uri with
               Cic.Constant _ -> assert false
             | Cic.Variable _ -> assert false
             | Cic.CurrentProof _ -> assert false
             | Cic.InductiveDefinition (l,_,n) -> (l,n) 
           ) in
        let rec split n l =
          if n = 0 then ([],l) else
          let p,a = split (n-1) (List.tl l) in
          ((List.hd l::p),a) in
        let params_and_IP,tail_args = split (noparams+1) args in 
        let constructors = 
            (match inductive_types with
              [(_,_,_,l)] -> l
            | _ -> raise NotApplicable) (* don't care for mutual ind *) in
        let constructors1 = 
          let rec clean_up n t =
             if n = 0 then t else
             (match t with
                (label,Cic.Prod (_,_,t)) -> clean_up (n-1) (label,t)
              | _ -> assert false) in
          List.map (clean_up noparams) constructors in
        let no_constructors= List.length constructors in
        let args_for_cases, other_args = 
          split no_constructors tail_args in
        let args_to_lift = 
          List.filter (test_for_lifting ~ids_to_inner_types) other_args in
        let subproofs = 
          match args_to_lift with
            [_] -> List.map aux args_to_lift 
          | _ -> List.map (aux ~name:(Some "H")) args_to_lift in
        prerr_endline "****** end subproofs *******"; flush stderr;
        let other_method_args = 
          build_args seed other_args subproofs 
             ~ids_to_inner_types ~ids_to_inner_sorts in
(*
        let rparams,inductive_arg =
          let rec aux =
            function 
              [] -> assert false            
            | [ia] -> [],ia
            | a::tl -> let (p,ia) = aux tl in (a::p,ia) in
          aux other_method_args in 
*)
        prerr_endline "****** end other *******"; flush stderr;
        let method_args=
          let rec build_method_args =
            function
                [],_-> [] (* extra args are ignored ???? *)
              | (name,ty)::tlc,arg::tla ->
                  let idarg = get_id arg in
                  let sortarg = 
                    (try (Hashtbl.find ids_to_inner_sorts idarg)
                     with Not_found -> "Type") in
                  let hdarg = 
                    if sortarg = "Prop" then
                      let (co,bo) = 
                        let rec bc = 
                          function 
                            Cic.Prod (_,s,t),Cic.ALambda(idl,n,s1,t1) ->
                              let ce = 
                                build_decl_item 
                                  seed idl n s1 ~ids_to_inner_sorts in
                              if (occur ind_uri s) then
                                (  prerr_endline ("inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; 
                                   match t1 with
                                   Cic.ALambda(id2,n2,s2,t2) ->
                                     let inductive_hyp =
                                       `Hypothesis
                                         { K.dec_name = name_of n2;
                                           K.dec_id = gen_id seed; 
                                           K.dec_inductive = true;
                                           K.dec_aref = id2;
                                           K.dec_type = s2
                                         } in
                                     let (context,body) = bc (t,t2) in
                                     (ce::inductive_hyp::context,body)
                                 | _ -> assert false)
                              else 
                                (  prerr_endline ("no inductive:" ^ (UriManager.string_of_uri ind_uri) ^ (CicPp.ppterm s)); flush stderr; 
                                let (context,body) = bc (t,t1) in
                                (ce::context,body))
                            | _ , t -> ([],aux t ~name:None) in
                        bc (ty,arg) in
                      K.ArgProof
                       { bo with
                         K.proof_name = Some name;
                         K.proof_context = co; 
                       };
                    else (K.Term arg) in
                  hdarg::(build_method_args (tlc,tla))
              | _ -> assert false in
          build_method_args (constructors1,args_for_cases) in
          { K.proof_name = None;
            K.proof_id   = gen_id seed;
            K.proof_context = []; 
            K.proof_apply_context = subproofs;
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "ByInduction";
                K.conclude_args =
                  K.Aux no_constructors 
                  ::K.Term (C.AAppl id ((C.AConst(idc,uri,exp_named_subst))::params_and_IP))
                  ::method_args@other_method_args;
                K.conclude_conclusion = 
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                   with notfound -> None  
              }
          } 
  | _ -> raise NotApplicable

and rewrite seed name id li ids_to_inner_types ids_to_inner_sorts =
  let aux ?(name = None) = acic2content seed ~name:None ~ids_to_inner_types ~ids_to_inner_sorts in
  let module C2A = Cic2acic in
  let module K = Content in
  let module C = Cic in
  match li with 
    C.AConst (sid,uri,exp_named_subst)::args ->
      let uri_str = UriManager.string_of_uri uri in
      if uri_str = "cic:/Coq/Init/Logic/eq_ind.con" or
         uri_str = "cic:/Coq/Init/Logic/eq_ind_r.con" then 
        let subproof = aux (List.nth args 3) in
        let method_args =
          let rec ma_aux n = function
              [] -> []
            | a::tl -> 
                let hd = 
                  if n = 0 then
                    K.Premise
                     { K.premise_id = gen_id seed;
                       K.premise_xref = subproof.K.proof_id;
                       K.premise_binder = None;
                       K.premise_n = None
                     }
                  else 
                    let aid = get_id a in
                    let asort = (try (Hashtbl.find ids_to_inner_sorts aid)
                      with Not_found -> "Type") in
                    if asort = "Prop" then
                      K.ArgProof (aux a)
                    else K.Term a in
                hd::(ma_aux (n-1) tl) in
          (ma_aux 3 args) in 
          { K.proof_name = None;
            K.proof_id   = gen_id seed;
            K.proof_context = []; 
            K.proof_apply_context = [subproof];
            K.proof_conclude = 
              { K.conclude_id = gen_id seed; 
                K.conclude_aref = id;
                K.conclude_method = "Rewrite";
                K.conclude_args = 
                  K.Term (C.AConst (sid,uri,exp_named_subst))::method_args;
                K.conclude_conclusion = 
                   try Some 
                     (Hashtbl.find ids_to_inner_types id).C2A.annsynthesized
                   with notfound -> None
              }
          } 
      else raise NotApplicable
  | _ -> raise NotApplicable
;; 

let map_conjectures
 seed ~ids_to_inner_sorts ~ids_to_inner_types (id,n,context,ty)
=
 let context' =
  List.map
   (function
       (id,None) as item -> item
     | (id,Some (name,Cic.ADecl t)) ->
         id,
          Some
           (build_decl_item seed (get_id t) name t
            ~ids_to_inner_sorts)
     | (id,Some (name,Cic.ADef t)) ->
         id,
          Some
           (build_def_item seed (get_id t) name t
            ~ids_to_inner_sorts ~ids_to_inner_types)
   ) 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
  let module C2A = Cic2acic in
  let seed = ref 0 in
  function
      C.ACurrentProof (_,_,n,conjectures,bo,ty,params) ->
        (gen_id seed, params,
          Some
           (List.map
             (map_conjectures seed ~ids_to_inner_sorts ~ids_to_inner_types)
             conjectures),
          `Def (K.Const,ty,
            build_def_item seed (get_id bo) (C.Name n) bo 
             ~ids_to_inner_sorts ~ids_to_inner_types))
    | C.AConstant (_,_,n,Some bo,ty,params) ->
         (gen_id seed, params, None,
           `Def (K.Const,ty,
             build_def_item seed (get_id bo) (C.Name n) bo 
               ~ids_to_inner_sorts ~ids_to_inner_types))
    | C.AConstant (id,_,n,None,ty,params) ->
         (gen_id seed, params, None,
           `Decl (K.Const,
             build_decl_item seed id (C.Name n) ty 
               ~ids_to_inner_sorts))
    | C.AVariable (_,n,Some bo,ty,params) ->
         (gen_id seed, params, None,
           `Def (K.Var,ty,
             build_def_item seed (get_id bo) (C.Name n) bo
               ~ids_to_inner_sorts ~ids_to_inner_types))
    | C.AVariable (id,n,None,ty,params) ->
         (gen_id seed, params, None,
           `Decl (K.Var,
             build_decl_item seed id (C.Name n) ty
              ~ids_to_inner_sorts))
    | C.AInductiveDefinition (id,l,params,nparams) ->
         (gen_id seed, params, None,
            `Joint
              { K.joint_id = gen_id seed;
                K.joint_kind = `Inductive nparams;
                K.joint_defs = List.map (build_inductive seed) l
              }) 

and
    build_inductive seed = 
     let module K = Content in
      fun (_,n,b,ty,l) ->
        `Inductive
          { K.inductive_id = gen_id seed;
            K.inductive_kind = b;
            K.inductive_type = ty;
            K.inductive_constructors = build_constructors seed l
           }

and 
    build_constructors seed l =
     let module K = Content in
      List.map 
       (fun (n,t) ->
           { K.dec_name = Some n;
             K.dec_id = gen_id seed;
             K.dec_inductive = false;
             K.dec_aref = "";
             K.dec_type = t
           }) l
;;
   
(* 
and 'term cinductiveType = 
 id * string * bool * 'term *                (* typename, inductive, arity *)
   'term cconstructor list                   (*  constructors        *)

and 'term cconstructor =
 string * 'term    
*)