(* Copyright (C) 2002, 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/.
 *)

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,None))]
         | C.LetIn _ -> []
         | C.Appl _
         | C.Const _ -> []
         | 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)), Some ty)))
                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)), Some ty)))
                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.get_proof () with
       None -> assert false
     | Some (_,metasenv,_,_) -> metasenv
   in
    let ty,_ = (* TASSI: FIXME ehhmmmm *)
      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph 
    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.get_proof () with
       None -> assert false
     | Some (_,metasenv,_,_) -> metasenv
   in
    let ty,_ = 
      CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph 
    in
      match term with
          Cic.Meta (n,_) -> P.goal := Some n
	| _ -> raise FocusOnlyOnMeta
;;