(*
    ||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 fire_beta, upto = 
      match l with C.Meta _ :: _ -> true, List.length l - 1 | _ -> false, 0 
    in
    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 
       let t =
        match l1 with
         | C.Appl l :: tl -> C.Appl (l@tl)
         | _ -> C.Appl l1
       in
        if fire_beta then NCicReduction.head_beta_reduce ~upto t
        else t
 | 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))
;;

module NCicHash =
 Hashtbl.Make
  (struct
    type t = C.term
    let equal = (==)
    let hash = Hashtbl.hash_param 100 1000 
   end)
;;

let mk_appl he args = 
  if args = [] then he else
  match he with
  | NCic.Appl l -> NCic.Appl (l@args)
  | _ -> NCic.Appl (he::args)
;;

let map_obj_kind ?(skip_body=false) f =
 let do_bo f x = if skip_body then x else f x in
 function
    NCic.Constant (relev,name,bo,ty,attrs) ->
     NCic.Constant (relev,name,do_bo (HExtlib.map_option f) bo, f ty,attrs)
  | NCic.Fixpoint (ind,fl,attrs) ->
     let fl =
      List.map
       (function (relevance,name,recno,ty,bo) -> 
          relevance,name,recno,f ty,do_bo f bo)
       fl
     in
      NCic.Fixpoint (ind,fl,attrs)
  | NCic.Inductive (is_ind,lno,itl,attrs) ->
      let itl = 
        List.map
         (fun (relevance,name,ty,cl) ->
           let cl = 
             List.map (fun (relevance, name, ty) ->
                relevance, name, f ty)
             cl
           in
           relevance, name, f ty, cl)
         itl
      in
      NCic.Inductive (is_ind,lno,itl,attrs)
;;

exception Occurr;;

let clean_or_fix_dependent_abstrations ctx t =
  let occurrs_1 t =
    let rec aux n _ = function
      | NCic.Meta _ -> ()
      | NCic.Rel i when i = n + 1 -> raise Occurr
      | t -> NCicUtils.fold (fun _ k -> k + 1) n aux () t
    in
    try aux 0 () t; false
    with Occurr -> true
  in
  let fresh ctx name = 
    if not (List.mem name ctx) then name 
    else
     let rec aux i =
       let attempt = name ^ string_of_int i in
       if List.mem attempt ctx then aux (i+1) 
       else attempt
     in 
      aux 0
  in
  let rec aux ctx = function
  | NCic.Meta _ as t -> t
  | NCic.Prod (name,s,t) when name.[0] = '#' && occurrs_1 t ->
      let name = fresh ctx (String.sub name 1 (String.length name-1)) in
      NCic.Prod (name,aux ctx s, aux (name::ctx) t)
  | NCic.Prod (name,s,t) when name.[0] = '#' && not (occurrs_1 t) ->
      NCic.Prod ("_",aux ctx s,aux ("_"::ctx) t)
  | NCic.Prod ("_",s,t) -> NCic.Prod("_",aux ctx s,aux ("_"::ctx) t)
  | NCic.Prod (name,s,t) when name.[0] <> '_' && not (occurrs_1 t) ->
      let name = fresh ctx ("_"^name) in
      NCic.Prod (name, aux ctx s, aux (name::ctx) t)
  | NCic.Prod (name,s,t) when List.mem name ctx ->
      let name = fresh ctx name in
      NCic.Prod (name, aux ctx s, aux (name::ctx) t)
  | NCic.Lambda (name,s,t) when List.mem name ctx ->
      let name = fresh ctx name in
      NCic.Lambda (name, aux ctx s, aux (name::ctx) t)
  | t -> NCicUtils.map (fun (e,_) ctx -> e::ctx) ctx aux t
  in
    aux (List.map fst ctx) t
;;

let apply_subst subst context t = 
 let rec apply_subst subst () =
 function
    NCic.Meta (i,lc) ->
     (try
       let _,_,t,_ = NCicUtils.lookup_subst i subst in
       let t = NCicSubstitution.subst_meta lc t in
        apply_subst subst () t
      with
       Not_found ->
        match lc with
           _,NCic.Irl _ -> NCic.Meta (i,lc)
         | n,NCic.Ctx l ->
            NCic.Meta
             (i,(0,NCic.Ctx
                 (List.map (fun t ->
                   apply_subst subst () (NCicSubstitution.lift n t)) l))))
  | t -> NCicUtils.map (fun _ () -> ()) () (apply_subst subst) t
 in
  clean_or_fix_dependent_abstrations context (apply_subst subst () t)
;;

let apply_subst_context subst context =
  let rec aux c = function 
    | [] -> []
    | (name,NCic.Decl t as e) :: tl -> 
        (name, NCic.Decl (apply_subst subst c t)) :: aux (e::c) tl
    | (name,NCic.Def (t1,t2) as e) :: tl -> 
        (name, NCic.Def (apply_subst subst c t1,apply_subst subst c t2)) :: 
          aux (e::c) tl
  in
    List.rev (aux [] (List.rev context))
;;

let rec apply_subst_metasenv subst = function
  | [] -> []
  | (i,_) :: _ when List.mem_assoc i subst -> assert false
  | (i,(name,ctx,ty)) :: tl ->
      (i,(name,apply_subst_context subst ctx,apply_subst subst ctx ty)) ::
         apply_subst_metasenv subst tl
;;

let height_of_term tl =
 let h = ref 0 in
 let get_height (NReference.Ref (uri,_)) =
  let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
   height in
 let rec aux =
  function
     NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
   | NCic.Meta _ -> ()
   | NCic.Rel _
   | NCic.Sort _ -> ()
   | NCic.Implicit _ -> assert false
   | NCic.Const nref -> h := max !h (get_height nref)
   | NCic.Prod (_,t1,t2)
   | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
   | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
   | NCic.Appl l -> List.iter aux l
   | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
 in
  List.iter aux tl;
  1 + !h
;;

let height_of_obj_kind uri =
 function
    NCic.Inductive _
  | NCic.Constant (_,_,None,_,_)
  | NCic.Fixpoint (false,_,_) -> 0
  | NCic.Fixpoint (true,ifl,_) ->
     let iflno = List.length ifl in
      height_of_term
       (List.fold_left
        (fun l (_,_,_,ty,bo) ->
          let bo = NCicTypeChecker.debruijn uri iflno [] bo in
           ty::bo::l
       ) [] ifl)
  | NCic.Constant (_,_,Some bo,ty,_) -> height_of_term [bo;ty]
;;