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 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 -> [Some (n,C.Decl s)]
         | C.Prod _ -> []
         | C.Lambda (n,s,t) when t == term -> [Some (n,C.Decl s)]
         | C.Lambda _ -> []
         | C.LetIn (n,s,t) when t == term -> [Some (n,C.Def 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 = Some (C.Name name, (C.Def (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 = Some (C.Name name,(C.Def (C.CoFix (!counter,ifl)))) in
                 incr counter ;
                 res
              ) ifl
       in
        binding@(aux parentid)
  in
   aux
;;

exception NotImplemented;;

(* A subterm is changed into a fresh 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 context term in
     P.perforate context term ty (* P.perforate also sets the goal *)
;;

exception FocusOnlyOnMeta;;

(* If the current selection is a Meta, that Meta becomes the current goal *)
let focus 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 context term in
     match term with
        Cic.Meta (n,_) -> P.goal := Some n
      | _ -> raise FocusOnlyOnMeta
;;