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;;

(* It returns true iff the proof has been perforated, i.e. if a subterm *)
(* has been changed into a meta.                                        *)
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 metasenv =
     match !P.proof with
        None -> assert false
      | Some (_,metasenv,_,_) -> metasenv
    in
     let ty =
      CicTypeChecker.type_of_aux' metasenv type_checker_env_of_context term
     in
      let (meta,perforated) =
       (* If the selected term is already a meta, we return it. *)
       (* Otherwise, we are trying to refine a non-meta term... *)
       match term with
          Cic.Meta n -> P.goal := Some (n,(context,ty)) ; n,false
        | _ -> P.perforate context term ty,true (* P.perforate also sets the goal *)
      in
       perforated
;;