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

(* mk_fresh_name context name typ                      *)
(* returns an identifier which is fresh in the context *)
(* and that resembles [name] as much as possible.      *)
(* [typ] will be the type of the variable              *)
let mk_fresh_name context name ~typ =
 let module C = Cic in
  let basename =
   match name with
      C.Anonymous ->
       (*CSC: great space for improvements here *)
       (try
         (match CicTypeChecker.type_of_aux' [] context typ with
             C.Sort C.Prop -> "H"
	   | C.Sort C.CProp -> "H"
           | C.Sort C.Set -> "x"
           | _ -> "H"
         )
        with CicTypeChecker.TypeCheckerFailure _ -> "H"
       )
    | C.Name name ->
       Str.global_replace (Str.regexp "[0-9]*$") "" name
  in
   let already_used name =
    List.exists (function Some (C.Name n,_) -> n=name | _ -> false) context
   in
    if not (already_used basename) then
     C.Name basename
    else
     let rec try_next n =
      let name' = basename ^ string_of_int n in
       if already_used name' then
        try_next (n+1)
       else
        C.Name name'
     in
      try_next 1
;;

let new_meta_of_proof ~proof:(_, metasenv, _, _) =
  CicMkImplicit.new_meta metasenv

let subst_meta_in_proof proof meta term newmetasenv =
 let uri,metasenv,bo,ty = proof in
  let subst_in = CicMetaSubst.apply_subst [meta,term] in
   let metasenv' =
    newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
   in
    let metasenv'' =
     List.map
      (function i,canonical_context,ty ->
        let canonical_context' =
         List.map
          (function
              Some (n,Cic.Decl s) -> Some (n,Cic.Decl (subst_in s))
            | Some (n,Cic.Def (s,None)) -> Some (n,Cic.Def ((subst_in s),None))
            | None -> None
            | Some (_,Cic.Def (_,Some _)) -> assert false
          ) canonical_context
        in
         i,canonical_context',(subst_in ty)
      ) metasenv'
    in
     let bo' = subst_in bo in
      let newproof = uri,metasenv'',bo',ty in
       (newproof, metasenv'')

(*CSC: commento vecchio *)
(* refine_meta_with_brand_new_metasenv meta term subst_in newmetasenv     *)
(* This (heavy) function must be called when a tactic can instantiate old *)
(* metavariables (i.e. existential variables). It substitues the metasenv *)
(* of the proof with the result of removing [meta] from the domain of     *)
(* [newmetasenv]. Then it replaces Cic.Meta [meta] with [term] everywhere *)
(* in the current proof. Finally it applies [apply_subst_replacing] to    *)
(*  current proof.                                                        *)
(*CSC: A questo punto perche' passare un bo' gia' istantiato, se tanto poi *)
(*CSC: ci ripasso sopra apply_subst!!!                                     *)
(*CSC: Attenzione! Ora questa funzione applica anche [subst_in] a *)
(*CSC: [newmetasenv].                                             *)
let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv =
 let (uri,_,bo,ty) = proof in
  let bo' = subst_in bo in
  let metasenv' =
   List.fold_right
    (fun metasenv_entry i ->
      match metasenv_entry with
         (m,canonical_context,ty) when m <> meta ->
           let canonical_context' =
            List.map
             (function
                 None -> None
               | Some (i,Cic.Decl t) -> Some (i,Cic.Decl (subst_in t))
               | Some (i,Cic.Def (t,None))  ->
                  Some (i,Cic.Def ((subst_in t),None))
               | Some (_,Cic.Def (_,Some _))  -> assert false
             ) canonical_context
           in
            (m,canonical_context',subst_in ty)::i
       | _ -> i
    ) newmetasenv []
  in
   let newproof = uri,metasenv',bo',ty in
    (newproof, metasenv')