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 metasenv =
    match !P.proof with
       None -> assert false
     | Some (_,metasenv,_,_) -> metasenv
   in
    let ty =
     CicTypeChecker.type_of_aux' metasenv
      (P.cic_context_of_named_context 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
;;