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

exception Bad_pattern of string

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
   (* empty context is ok for term since it wont be used by apply_subst *)
   (* hack: since we do not know the context and the type of term, we
      create a substitution with cc =[] and type = Implicit; they will be
      in  any case dropped by apply_subst, but it would be better to rewrite
      the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
  let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] 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
     (* Metavariables can appear also in the *statement* of the theorem
      * since the parser does not reject as statements terms with
      * metavariable therein *)
     let ty' = subst_in ty 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
  (* Metavariables can appear also in the *statement* of the theorem
   * since the parser does not reject as statements terms with
   * metavariable therein *)
  let ty' = subst_in ty 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')

let compare_metasenvs ~oldmetasenv ~newmetasenv =
 List.map (function (i,_,_) -> i)
  (List.filter
   (function (i,_,_) ->
     not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv)
;;

(** finds the _pointers_ to subterms that are alpha-equivalent to wanted in t *)
let find_subterms ~eq ~wanted t =
  let rec find w t =
    if eq w t then 
      [t]
    else
      match t with
      | Cic.Sort _ 
      | Cic.Rel _ -> []
      | Cic.Meta (_, ctx) -> 
          List.fold_left (
            fun acc e -> 
              match e with 
              | None -> acc 
              | Some t -> find w t @ acc
          ) [] ctx
      | Cic.Lambda (_, t1, t2) 
      | Cic.Prod (_, t1, t2) 
      | Cic.LetIn (_, t1, t2) -> 
          find w t1 @ find (CicSubstitution.lift 1 w) t2
      | Cic.Appl l -> 
          List.fold_left (fun acc t -> find w t @ acc) [] l
      | Cic.Cast (t, ty) -> find w t @ find w ty
      | Cic.Implicit _ -> assert false
      | Cic.Const (_, esubst)
      | Cic.Var (_, esubst) 
      | Cic.MutInd (_, _, esubst) 
      | Cic.MutConstruct (_, _, _, esubst) -> 
          List.fold_left (fun acc (_, t) -> find w t @ acc) [] esubst
      | Cic.MutCase (_, _, outty, indterm, patterns) -> 
          find w outty @ find w indterm @ 
            List.fold_left (fun acc p -> find w p @ acc) [] patterns
      | Cic.Fix (_, funl) -> 
          List.fold_left (
            fun acc (_, _, ty, bo) -> find w ty @ find w bo @ acc
          ) [] funl
      | Cic.CoFix (_, funl) ->
          List.fold_left (
            fun acc (_, ty, bo) -> find w ty @ find w bo @ acc
          ) [] funl
  in
  find wanted t
  
let select ~term ~pattern =
  let add_ctx i name entry =
      (Some (name, entry)) :: i
  in
  (* i is the number of binder traversed *) 
  let rec aux i pattern term =
    match (pattern, term) with
    | Cic.Implicit (Some `Hole), t -> [i,t]
    | Cic.Implicit (Some `Type), t -> []
    | Cic.Implicit None,_ -> []
    | Cic.Meta (_, ctxt1), Cic.Meta (_, ctxt2) ->
        List.concat
          (List.map2
            (fun t1 t2 ->
              (match (t1, t2) with Some t1, Some t2 -> aux i t1 t2 | _ -> []))
            ctxt1 ctxt2)
    | Cic.Cast (te1, ty1), Cic.Cast (te2, ty2) -> aux i te1 te2 @ aux i ty1 ty2
    | Cic.Prod (Cic.Anonymous, s1, t1), Cic.Prod (name, s2, t2)
    | Cic.Lambda (Cic.Anonymous, s1, t1), Cic.Lambda (name, s2, t2) ->
        aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
    | Cic.Prod (Cic.Name n1, s1, t1), 
      Cic.Prod ((Cic.Name n2) as name , s2, t2)
    | Cic.Lambda (Cic.Name n1, s1, t1), 
      Cic.Lambda ((Cic.Name n2) as name, s2, t2) when n1 = n2->
        aux i s1 s2 @ aux (add_ctx i name (Cic.Decl s2)) t1 t2
    | Cic.Prod (name1, s1, t1), Cic.Prod (name2, s2, t2)
    | Cic.Lambda (name1, s1, t1), Cic.Lambda (name2, s2, t2) -> []
    | Cic.LetIn (Cic.Anonymous, s1, t1), Cic.LetIn (name, s2, t2) -> 
        aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
    | Cic.LetIn (Cic.Name n1, s1, t1), 
      Cic.LetIn ((Cic.Name n2) as name, s2, t2) when n1 = n2-> 
        aux i s1 s2 @ aux (add_ctx i name (Cic.Def (s2,None))) t1 t2
    | Cic.LetIn (name1, s1, t1), Cic.LetIn (name2, s2, t2) -> []
    | Cic.Appl terms1, Cic.Appl terms2 -> auxs i terms1 terms2
    | Cic.Var (_, subst1), Cic.Var (_, subst2)
    | Cic.Const (_, subst1), Cic.Const (_, subst2)
    | Cic.MutInd (_, _, subst1), Cic.MutInd (_, _, subst2)
    | Cic.MutConstruct (_, _, _, subst1), Cic.MutConstruct (_, _, _, subst2) ->
        auxs i (List.map snd subst1) (List.map snd subst2)
    | Cic.MutCase (_, _, out1, t1, pat1), Cic.MutCase (_ , _, out2, t2, pat2) ->
        aux i out1 out2 @ aux i t1 t2 @ auxs i pat1 pat2
    | Cic.Fix (_, funs1), Cic.Fix (_, funs2) ->
        List.concat
          (List.map2
            (fun (_, _, ty1, bo1) (_, _, ty2, bo2) -> 
              aux i ty1 ty2 @ aux i bo1 bo2)
            funs1 funs2)
    | Cic.CoFix (_, funs1), Cic.CoFix (_, funs2) ->
        List.concat
          (List.map2
            (fun (_, ty1, bo1) (_, ty2, bo2) -> aux i ty1 ty2 @ aux i bo1 bo2)
            funs1 funs2)
    | x,y -> 
        raise (Bad_pattern 
                (Printf.sprintf "Pattern %s versus term %s" 
                  (CicPp.ppterm x)
                  (CicPp.ppterm y)))
  and auxs i terms1 terms2 =  (* as aux for list of terms *)
    List.concat (List.map2 (fun t1 t2 -> aux i t1 t2) terms1 terms2)
  in
  aux [] pattern term

let pattern_of ?(equality=(==)) ~term terms =
  let (===) x y = equality x y in
  let rec aux t =
    match t with
    | t when List.exists (fun t' -> t === t') terms -> Cic.Implicit (Some `Hole)
    | Cic.Var (uri, subst) -> Cic.Var (uri, aux_subst subst)
    | Cic.Meta (i, ctxt) ->
        let ctxt =
          List.map (function None -> None | Some t -> Some (aux t)) ctxt
        in
        Cic.Meta (i, ctxt)
    | Cic.Cast (t, ty) -> Cic.Cast (aux t, aux ty)
    | Cic.Prod (name, s, t) -> Cic.Prod (name, aux s, aux t)
    | Cic.Lambda (name, s, t) -> Cic.Lambda (name, aux s, aux t)
    | Cic.LetIn (name, s, t) -> Cic.LetIn (name, aux s, aux t)
    | Cic.Appl terms -> Cic.Appl (List.map aux terms)
    | Cic.Const (uri, subst) -> Cic.Const (uri, aux_subst subst)
    | Cic.MutInd (uri, tyno, subst) -> Cic.MutInd (uri, tyno, aux_subst subst)
    | Cic.MutConstruct (uri, tyno, consno, subst) ->
        Cic.MutConstruct (uri, tyno, consno, aux_subst subst)
    | Cic.MutCase (uri, tyno, outty, t, pat) ->
        Cic.MutCase (uri, tyno, aux outty, aux t, List.map aux pat)
    | Cic.Fix (funno, funs) ->
        let funs =
          List.map (fun (name, i, ty, bo) -> (name, i, aux ty, aux bo)) funs
        in
        Cic.Fix (funno, funs)
    | Cic.CoFix (funno, funs) ->
        let funs =
          List.map (fun (name, ty, bo) -> (name, aux ty, aux bo)) funs
        in
        Cic.CoFix (funno, funs)
    | Cic.Rel _
    | Cic.Sort _
    | Cic.Implicit _ -> t
  and aux_subst subst =
    List.map (fun (uri, t) -> (uri, aux t)) subst
  in
  aux term