(* 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/.
 *)

open ProofEngineTypes

let clearbody ~hyp ~status:(proof, goal) =
 let module C = Cic in
  match hyp with
     None -> assert false
   | Some (_, C.Def (_, Some _)) -> assert false
   | Some (_, C.Decl _) -> raise (Fail "No Body To Clear")
   | Some (n_to_clear_body, C.Def (term,None)) as hyp_to_clear_body ->
      let curi,metasenv,pbo,pty = proof in
       let metano,_,_ = CicUtil.lookup_meta goal metasenv in
        let string_of_name =
         function
            C.Name n -> n
          | C.Anonymous -> "_"
        in
        let metasenv' =
         List.map
          (function
              (m,canonical_context,ty) when m = metano ->
                let canonical_context' =
                 List.fold_right
                  (fun entry context ->
                    match entry with
                       t when t == hyp_to_clear_body ->
                        let cleared_entry =
                         let ty =
                          CicTypeChecker.type_of_aux' metasenv context term
                         in
                          Some (n_to_clear_body, Cic.Decl ty)
                        in
                         cleared_entry::context
                     | None -> None::context
                     | Some (n,C.Decl t)
                     | Some (n,C.Def (t,None)) ->
                        let _ =
                         try
                          CicTypeChecker.type_of_aux' metasenv context t
                         with
                          _ ->
                            raise
                             (Fail
                               ("The correctness of hypothesis " ^
                                string_of_name n ^
                                " relies on the body of " ^
                                string_of_name n_to_clear_body)
                             )
                        in
                         entry::context
                     | Some (_,Cic.Def (_,Some _)) -> assert false
                  ) canonical_context []
                in
                 let _ =
                  try
                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
                  with
                   _ ->
                    raise
                     (Fail
                      ("The correctness of the goal relies on the body of " ^
                       string_of_name n_to_clear_body))
                 in
                  m,canonical_context',ty
            | t -> t
          ) metasenv
        in
         (curi,metasenv',pbo,pty), [goal]

let clear ~hyp:hyp_to_clear ~status:(proof, goal) =
 let module C = Cic in
  match hyp_to_clear with
     None -> assert false
   | Some (n_to_clear, _) ->
      let curi,metasenv,pbo,pty = proof in
       let metano,context,ty =
        CicUtil.lookup_meta goal metasenv
       in
        let string_of_name =
         function
            C.Name n -> n
          | C.Anonymous -> "_"
        in
        let metasenv' =
         List.map
          (function
              (m,canonical_context,ty) when m = metano ->
                let canonical_context' =
                 List.fold_right
                  (fun entry context ->
                    match entry with
                       t when t == hyp_to_clear -> None::context
                     | None -> None::context
                     | Some (_,Cic.Def (_,Some _)) -> assert false
                     | Some (n,C.Decl t)
                     | Some (n,C.Def (t,None)) ->
                        let _ =
                         try
                          CicTypeChecker.type_of_aux' metasenv context t
                         with
                          _ ->
                            raise
                             (Fail
                               ("Hypothesis " ^
                                string_of_name n ^
                                " uses hypothesis " ^
                                string_of_name n_to_clear)
                             )
                        in
                         entry::context
                  ) canonical_context []
                in
                 let _ =
                  try
                   CicTypeChecker.type_of_aux' metasenv canonical_context' ty
                  with
                   _ ->
                    raise
                     (Fail
                      ("Hypothesis " ^ string_of_name n_to_clear ^
                       " occurs in the goal"))
                 in
                  m,canonical_context',ty
            | t -> t
          ) metasenv
        in
         (curi,metasenv',pbo,pty), [goal]