(*
    ||M||  This file is part of HELM, an Hypertextual, Electronic        
    ||A||  Library of Mathematics, developed at the Computer Science     
    ||T||  Department, University of Bologna, Italy.                     
    ||I||                                                                
    ||T||  HELM is free software; you can redistribute it and/or         
    ||A||  modify it under the terms of the GNU General Public License   
    \   /  version 2 or (at your option) any later version.      
     \ /   This software is distributed as is, NO WARRANTY.     
      V_______________________________________________________________ *)

(* $Id$ *)

module C = NCic
module Ref = NReference

let map_term_fold_a g k f a = function
 | C.Meta _ -> assert false
 | C.Implicit _
 | C.Sort _
 | C.Const _
 | C.Rel _ as t -> a,t
 | C.Appl [] | C.Appl [_] -> assert false
 | C.Appl l as orig ->
    let a,l1 = 
      (* sharing fold? *)
      List.fold_right 
        (fun t (a,l) -> let a,t = f k a t in a, t :: l) 
        l (a,[])
    in
    a, if l1 == l then orig else (match l1 with
       | C.Appl l :: tl -> C.Appl (l@tl)
       | _ -> C.Appl l1)
 | C.Prod (n,s,t) as orig ->
     let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
     a, if t1 == t && s1 == s then orig else C.Prod (n,s1,t1)
 | C.Lambda (n,s,t) as orig -> 
     let a,s1 = f k a s in let a,t1 = f (g (n,C.Decl s) k) a t in
     a, if t1 == t && s1 == s then orig else C.Lambda (n,s1,t1)
 | C.LetIn (n,ty,t,b) as orig -> 
     let a,ty1 = f k a ty in let a,t1 = f k a t in
     let a,b1 = f (g (n,C.Def (t,ty)) k) a b in
     a, if ty1 == ty && t1 == t && b1 == b then orig else C.LetIn (n,ty1,t1,b1)
 | C.Match (r,oty,t,pl) as orig -> 
     let a,oty1 = f k a oty in let a,t1 = f k a t in 
     let a,pl1 = 
       (* sharing fold? *)
       List.fold_right (fun t (a,l) -> let a,t = f k a t in a,t::l) pl (a,[])
     in
     a, if oty1 == oty && t1 == t && pl1 == pl then orig 
        else C.Match(r,oty1,t1,pl1)
;;

let metas_of_term subst context term =
  let rec aux ctx acc = function
    | NCic.Rel i -> 
         (match HExtlib.list_skip (i-1) ctx with
         | (_,NCic.Def (bo,_)) :: ctx -> aux ctx acc bo
         | _ -> acc)
    | NCic.Meta(i,l) -> 
         (try
           let _,_,bo,_ = NCicUtils.lookup_subst i subst in
           let bo = NCicSubstitution.subst_meta l bo in
           aux ctx acc bo
         with NCicUtils.Subst_not_found _ -> 
            let shift, lc = l in
            let lc = NCicUtils.expand_local_context lc in
            let l = List.map (NCicSubstitution.lift shift) lc in
            List.fold_left (aux ctx) (i::acc) l)
    | t -> NCicUtils.fold (fun e c -> e::c) ctx aux acc t
  in
    HExtlib.list_uniq (List.sort Pervasives.compare (aux context [] term))
;;