let get_parent id ids_to_terms ids_to_father_ids =
 match Hashtbl.find ids_to_father_ids id with
    None -> None
  | Some id -> Some (id, Hashtbl.find ids_to_terms id)
;;

let get_context ids_to_terms ids_to_father_ids =
 let module P = ProofEngine in
 let module C = Cic in
  let rec aux id =
   match get_parent id ids_to_terms ids_to_father_ids with
      None -> []
    | Some (parentid,parent) ->
       let term = Hashtbl.find ids_to_terms id in
       let binding =
        match parent with
           C.Rel _
         | C.Var _
         | C.Meta _
         | C.Sort _
         | C.Implicit
         | C.Cast _ -> []
         | C.Prod (n,s,t) when t == term -> [P.Declaration,n,s]
         | C.Prod _ -> []
         | C.Lambda (n,s,t) when t == term -> [P.Declaration,n,s]
         | C.Lambda _ -> []
         | C.LetIn (n,s,t) when t == term -> [P.Definition,n,s]
         | C.LetIn _ -> []
         | C.Appl _
         | C.Const _ -> []
         | C.Abst _ -> assert false
         | C.MutInd _
         | C.MutConstruct _
         | C.MutCase _ -> []
(*CSC: sbagliato: manca il when *)
         | C.Fix (_,ifl) ->
            let counter = ref 0 in
             List.rev_map
              (function (name,_,ty,bo) ->
                let res = (P.Definition, C.Name name, C.Fix (!counter,ifl)) in
                 incr counter ;
                 res
              ) ifl
         | C.CoFix (_,ifl) ->
            let counter = ref 0 in
             List.rev_map
              (function (name,ty,bo) ->
                let res = (P.Definition, C.Name name, C.CoFix (!counter,ifl)) in
                 incr counter ;
                 res
              ) ifl
       in
        binding@(aux parentid)
  in
   aux
;;

exception NotImplemented;;

let to_sequent id ids_to_terms ids_to_father_ids =
 let module P = ProofEngine in
  let term = Hashtbl.find ids_to_terms id in
  let context = get_context ids_to_terms ids_to_father_ids id in
   let type_checker_env_of_context =
    List.map
     (function
         P.Declaration,_,t -> t
       | P.Definition,_,_ -> raise NotImplemented
     ) context
   in
    let ty = CicTypeChecker.type_of_aux' type_checker_env_of_context term in
     ((context,ty) : ProofEngine.sequent)
;;