(*
    ||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$ *)

exception MetaSubstFailure of string Lazy.t
exception Uncertain of string Lazy.t

(*
(*** Functions to apply a substitution ***)

let apply_subst_gen ~appl_fun subst term =
 let rec um_aux =
  let module C = Cic in
  let module S = CicSubstitution in 
   function
      C.Rel _ as t -> t
    | C.Var (uri,exp_named_subst) ->
       let exp_named_subst' =
         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
       in
       C.Var (uri, exp_named_subst')
    | C.Meta (i, l) -> 
        (try
          let (_, t,_) = lookup_subst i subst in
          um_aux (S.subst_meta l t)
        with CicUtil.Subst_not_found _ -> 
	  (* unconstrained variable, i.e. free in subst*)
          let l' =
            List.map (function None -> None | Some t -> Some (um_aux t)) l
          in
           C.Meta (i,l'))
    | C.Sort _
    | C.Implicit _ as t -> t
    | C.Cast (te,ty) -> C.Cast (um_aux te, um_aux ty)
    | C.Prod (n,s,t) -> C.Prod (n, um_aux s, um_aux t)
    | C.Lambda (n,s,t) -> C.Lambda (n, um_aux s, um_aux t)
    | C.LetIn (n,s,ty,t) -> C.LetIn (n, um_aux s, um_aux ty, um_aux t)
    | C.Appl (hd :: tl) -> appl_fun um_aux hd tl
    | C.Appl _ -> assert false
    | C.Const (uri,exp_named_subst) ->
       let exp_named_subst' =
         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
       in
       C.Const (uri, exp_named_subst')
    | C.MutInd (uri,typeno,exp_named_subst) ->
       let exp_named_subst' =
         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
       in
       C.MutInd (uri,typeno,exp_named_subst')
    | C.MutConstruct (uri,typeno,consno,exp_named_subst) ->
       let exp_named_subst' =
         List.map (fun (uri, t) -> (uri, um_aux t)) exp_named_subst
       in
       C.MutConstruct (uri,typeno,consno,exp_named_subst')
    | C.MutCase (sp,i,outty,t,pl) ->
       let pl' = List.map um_aux pl in
       C.MutCase (sp, i, um_aux outty, um_aux t, pl')
    | C.Fix (i, fl) ->
       let fl' =
         List.map (fun (name, i, ty, bo) -> (name, i, um_aux ty, um_aux bo)) fl
       in
       C.Fix (i, fl')
    | C.CoFix (i, fl) ->
       let fl' =
         List.map (fun (name, ty, bo) -> (name, um_aux ty, um_aux bo)) fl
       in
       C.CoFix (i, fl')
 in
  um_aux term
;;

let apply_subst =
  let appl_fun um_aux he tl =
    let tl' = List.map um_aux tl in
    let t' =
     match um_aux he with
        Cic.Appl l -> Cic.Appl (l@tl')
      | he' -> Cic.Appl (he'::tl')
    in
     begin
      match he with
         Cic.Meta (m,_) -> CicReduction.head_beta_reduce t'
       | _ -> t'
     end
  in
  fun subst t ->
(*     incr apply_subst_counter; *)
match subst with
   [] -> t
 | _ -> apply_subst_gen ~appl_fun subst t
;;

let profiler = HExtlib.profile "U/CicMetaSubst.apply_subst"
let apply_subst s t = 
  profiler.HExtlib.profile (apply_subst s) t


let apply_subst_context subst context =
 match subst with
    [] -> context
  | _ ->
(*
  incr apply_subst_context_counter;
  context_length := !context_length + List.length context;
*)
  List.fold_right
    (fun item context ->
      match item with
      | Some (n, Cic.Decl t) ->
          let t' = apply_subst subst t in
          Some (n, Cic.Decl t') :: context
      | Some (n, Cic.Def (t, ty)) ->
          let ty' = apply_subst subst ty in
          let t' = apply_subst subst t in
          Some (n, Cic.Def (t', ty')) :: context
      | None -> None :: context)
    context []

let apply_subst_metasenv subst metasenv =
(*
  incr apply_subst_metasenv_counter;
  metasenv_length := !metasenv_length + List.length metasenv;
*)
match subst with
   [] -> metasenv
 | _ ->
  List.map
    (fun (n, context, ty) ->
      (n, apply_subst_context subst context, apply_subst subst ty))
    (List.filter
      (fun (i, _, _) -> not (List.mem_assoc i subst))
      metasenv)

let tempi_type_of_aux_subst = ref 0.0;;
let tempi_subst = ref 0.0;;
let tempi_type_of_aux = ref 0.0;;
*)

let newmeta = 
  let maxmeta = ref 0 in
  fun () -> incr maxmeta; !maxmeta
;;

exception NotInTheList;;

let position n (shift, lc) =
  match lc with
  | NCic.Irl len when n <= shift || n > shift + len -> raise NotInTheList
  | NCic.Irl _ -> n - shift
  | NCic.Ctx tl ->
      let rec aux k = function 
         | [] -> raise NotInTheList
         | (NCic.Rel m)::_ when m + shift = n -> k
         | _::tl -> aux (k+1) tl 
      in
       aux 1 tl
;;

let pack_lc orig = 
  let rec are_contiguous k = function
    | [] -> true
    | (NCic.Rel j) :: tl when j = k+1 -> are_contiguous j tl
    | _ -> false
  in
  match orig with
  | _, NCic.Ctx [] -> 0, NCic.Irl 0
  | shift, NCic.Ctx (NCic.Rel k::tl as l) when are_contiguous k tl ->
      shift+k-1, NCic.Irl (List.length l)
  | _ -> orig
;;

let mk_restricted_irl shift len restrictions =
  let rec aux n =
    if n = 0 then [] else
      if List.mem (n+shift) restrictions then aux (n-1)
      else (NCic.Rel n)::aux (n-1)
  in
    pack_lc (shift, NCic.Ctx (List.rev (aux len)))
;;

exception Occur;;

let rec force_does_not_occur metasenv subst restrictions t =
 let rec aux k ms = function
    | NCic.Rel r when List.mem (r - k) restrictions -> raise Occur
    | NCic.Meta (n, l) as orig ->
       (* we ignore the subst since restrict will take care of already
        * instantiated/restricted metavariabels *)
       let (metasenv,subst as ms), restrictions_for_n, l' =
         match l with
         | shift, NCic.Irl len -> 
             let restrictions = 
               List.filter 
                (fun i -> i > shift && i <= shift + len) restrictions in
             ms, restrictions, mk_restricted_irl shift len restrictions
         | shift, NCic.Ctx l ->
            let ms, _, restrictions_for_n, l =
             List.fold_right
               (fun t (ms, i, restrictions_for_n, l) ->
                 try 
                   let ms, t = aux (k-shift) ms t in
                   ms, i-1, restrictions_for_n, t::l
                 with Occur ->
                   ms, i-1, i::restrictions_for_n, l)
               l (ms, List.length l, [], [])
            in
             ms, restrictions_for_n, pack_lc (shift, NCic.Ctx l)
       in
       if restrictions_for_n = [] then
         ms, if l = l' then orig else NCic.Meta (n, l')
       else
         let metasenv, subst, newmeta = 
           restrict metasenv subst n restrictions_for_n 
         in
           (metasenv, subst), NCic.Meta (newmeta, l')
    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
 in
   aux 0 (metasenv,subst) t 

and force_does_not_occur_in_context metasenv subst restrictions = function
  | name, NCic.Decl t as orig ->
      let (metasenv, subst), t' =
        force_does_not_occur metasenv subst restrictions t in
      metasenv, subst, (if t == t' then orig else (name,NCic.Decl t'))
  | name, NCic.Def (bo, ty) as orig ->
      let (metasenv, subst), bo' =
        force_does_not_occur metasenv subst restrictions bo in
      let (metasenv, subst), ty' =
        force_does_not_occur metasenv subst restrictions ty in
      metasenv, subst, 
       (if bo == bo' && ty == ty' then orig else (name, NCic.Def (bo', ty')))

and erase_in_context metasenv subst pos restrictions = function
  | [] -> metasenv, subst, restrictions, []
  | hd::tl as orig ->
      let metasenv, subst, restricted, tl' = 
        erase_in_context metasenv subst (pos+1) restrictions tl in
      if List.mem pos restricted then
        metasenv, subst, restricted, tl'
      else
        try
          let metasenv, subst, hd' =
            let delifted_restricted = 
              List.map ((+) ~-pos) (List.filter ((<=) pos) restricted) in
            force_does_not_occur_in_context 
              metasenv subst delifted_restricted hd
          in
           metasenv, subst, restricted, 
            (if hd' == hd && tl' == tl then orig else (hd' :: tl'))
        with Occur ->
            metasenv, subst, (pos :: restricted), tl'

and restrict metasenv subst i restrictions =
  assert (restrictions <> []);
  try 
    let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
      try 
        let metasenv, subst, restrictions, newctx = 
          erase_in_context metasenv subst 1 restrictions ctx in
        let (metasenv, subst), newty =  
          force_does_not_occur metasenv subst restrictions ty in
        let (metasenv, subst), newbo =  
          force_does_not_occur metasenv subst restrictions bo in
        let j = newmeta () in
        let subst_entry_j = j, (name, newctx, newty, newbo) in
        let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
        let subst_entry_i = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
        metasenv,
        subst_entry_j :: List.map 
          (fun (n,_) as orig -> if i = n then subst_entry_i else orig) subst,
        j
      with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
            ("Cannot restrict the context of the metavariable ?%d over "^^
            "the hypotheses %s since ?%d is already instantiated "^^
            "with %s and at least one of the hypotheses occurs in "^^
            "the substituted term") i  (String.concat ", " 
            (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)) i
            (NCicPp.ppterm ~metasenv ~subst ~context:ctx bo))))
  with NCicUtils.Subst_not_found _ -> 
    try 
      let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
      try
        let metasenv, subst, restrictions, newctx = 
          erase_in_context metasenv subst 1 restrictions ctx in
        let (metasenv, subst), newty =  
          force_does_not_occur metasenv subst restrictions ty in
        let j = newmeta () in
        let metasenv_entry = j, (name, newctx, newty) in
        let reloc_irl = mk_restricted_irl 0 (List.length ctx) restrictions in
        let subst_entry = i, (name, ctx, NCic.Meta (j, reloc_irl), ty) in
        List.map 
          (fun (n,_) as orig -> if i = n then metasenv_entry else orig) 
          metasenv,
        subst_entry :: subst, j
      with Occur -> raise (MetaSubstFailure (lazy (Printf.sprintf
          ("Cannot restrict the context of the metavariable ?%d "^^
          "over the hypotheses %s since metavariable's type depends "^^
          "on at least one of them") i (String.concat ", " 
          (List.map (fun x -> fst (List.nth ctx (x-1))) restrictions)))))
    with 
    | NCicUtils.Meta_not_found _ -> assert false
;;

(* INVARIANT: we suppose that t is not another occurrence of Meta(n,_), 
   otherwise the occur check does not make sense in case of unification
   of ?n with ?n *)
let delift metasenv subst context n l t =
  let rec aux k (metasenv, subst as ms) = function
    | NCic.Rel n as t when n <= k -> ms, t
    | NCic.Rel n -> 
        (try
          match List.nth context (n-k-1) with
          | _,NCic.Def (bo,_) -> 
                (try ms, NCic.Rel ((position (n-k) l) + k)
                 with NotInTheList ->
                (* CSC: This bit of reduction hurts performances since it is
                 * possible to  have an exponential explosion of the size of the
                 * proof. required for nat/nth_prime.ma *)
                  aux k ms (NCicSubstitution.lift n bo))
          | _,NCic.Decl _ -> ms, NCic.Rel ((position (n-k) l) + k)
        with Failure _ -> assert false) (*Unbound variable found in delift*)
    | NCic.Meta (i,l1) as orig ->
        (try
           let _,_,t,_ = NCicUtils.lookup_subst i subst in
           aux k ms (NCicSubstitution.subst_meta l1 t)
         with NCicUtils.Subst_not_found _ ->
           (* see the top level invariant *)
           if (i = n) then 
            raise (MetaSubstFailure (lazy (Printf.sprintf (
              "Cannot unify the metavariable ?%d with a term that has "^^
              "as subterm %s in which the same metavariable "^^
              "occurs (occur check)") i 
               (NCicPp.ppterm ~context ~metasenv ~subst t))))
           else
              let shift1,lc1 = l1 in
              let shift,lc = l in
              match lc, lc1 with
              | NCic.Irl len, NCic.Irl len1 
                when shift1 < shift || len1 + shift1 > len + shift ->
                  let restrictions = 
                     HExtlib.list_seq 1 (shift - shift1) @
                     HExtlib.list_seq (shift+len+1) (shift1+len1)
                  in
                  let metasenv, subst, newmeta = 
                     restrict metasenv subst i restrictions 
                  in
                  (metasenv, subst), 
                  NCic.Meta(newmeta, mk_restricted_irl shift1 len1 restrictions)
              | NCic.Irl _, NCic.Irl _ when shift = 0 -> ms, orig
              | NCic.Irl _, NCic.Irl _ ->
                   ms, NCic.Meta (i, (shift1 - shift, lc1))
              | _ -> 
                  let lc1 = NCicUtils.expand_local_context lc1 in
                  let rec deliftl tbr j ms = function
                    | [] -> ms, tbr, []
                    | t::tl ->
                        let ms, tbr, tl = deliftl tbr (j+1) ms tl in
                        try 
                          let ms, t = aux (k-shift1) ms t in 
                          ms, tbr, t::tl
                        with
                        | NotInTheList | MetaSubstFailure _ -> ms, j::tbr, tl
                  in
                  let (metasenv, subst), to_be_r, lc1' = deliftl [] 1 ms lc1 in
                  let l1 = pack_lc (shift, NCic.Ctx lc1') in
                  if to_be_r = [] then
                    (metasenv, subst), 
                    (if lc1' = lc1 then orig else NCic.Meta (i,l1))
                  else
                    let metasenv, subst, newmeta = 
                      restrict metasenv subst i to_be_r in
                    (metasenv, subst), NCic.Meta(newmeta,l1))
    | t -> NCicUntrusted.map_term_fold_a (fun _ k -> k+1) k aux ms t
  in
   try aux 0 (metasenv,subst) t
   with NotInTheList ->
      (* This is the case where we fail even first order unification. *)
      (* The reason is that our delift function is weaker than first  *)
      (* order (in the sense of alpha-conversion). See comment above  *)
      (* related to the delift function.                              *)
      let msg = (lazy (Printf.sprintf
        ("Error trying to abstract %s over [%s]: the algorithm only tried to "^^
        "abstract over bound variables") (NCicPp.ppterm ~metasenv ~subst
        ~context t) (String.concat "; " (List.map (NCicPp.ppterm ~metasenv
        ~subst ~context) (let shift, lc = l in List.map (NCicSubstitution.lift
        shift) (NCicUtils.expand_local_context lc))))))
      in
      let shift, lc = l in
      let lc = NCicUtils.expand_local_context lc in
      let l = List.map (NCicSubstitution.lift shift) lc in
       if
         List.exists
          (fun t -> NCicUntrusted.metas_of_term subst context t = [])
            l
       then
        raise (Uncertain msg)
       else
        raise (MetaSubstFailure msg)
;;

(*
(* delifts a term t of n levels strating from k, that is changes (Rel m)
 * to (Rel (m - n)) when m > (k + n). if k <= m < k + n delift fails
 *)
let delift_rels_from subst metasenv k n =
 let rec liftaux subst metasenv k =
  let module C = Cic in
   function
      C.Rel m as t ->
       if m < k then
        t, subst, metasenv
       else if m < k + n then
         raise DeliftingARelWouldCaptureAFreeVariable
       else
        C.Rel (m - n), subst, metasenv
    | C.Var (uri,exp_named_subst) ->
       let exp_named_subst',subst,metasenv = 
        List.fold_right
         (fun (uri,t) (l,subst,metasenv) ->
           let t',subst,metasenv = liftaux subst metasenv k t in
            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
       in
        C.Var (uri,exp_named_subst'),subst,metasenv
    | C.Meta (i,l) ->
        (try
          let (_, t,_) = lookup_subst i subst in
           liftaux subst metasenv k (CicSubstitution.subst_meta l t)
         with CicUtil.Subst_not_found _ -> 
          let l',to_be_restricted,subst,metasenv =
           let rec aux con l subst metasenv =
            match l with
               [] -> [],[],subst,metasenv
             | he::tl ->
                let tl',to_be_restricted,subst,metasenv =
                 aux (con + 1) tl subst metasenv in
                let he',more_to_be_restricted,subst,metasenv =
                 match he with
                    None -> None,[],subst,metasenv
                  | Some t ->
                     try
                      let t',subst,metasenv = liftaux subst metasenv k t in
                       Some t',[],subst,metasenv
                     with
                      DeliftingARelWouldCaptureAFreeVariable ->
                       None,[i,con],subst,metasenv
                in
                 he'::tl',more_to_be_restricted@to_be_restricted,subst,metasenv
           in
            aux 1 l subst metasenv in
          let metasenv,subst = restrict subst to_be_restricted metasenv in
           C.Meta(i,l'),subst,metasenv)
    | C.Sort _ as t -> t,subst,metasenv
    | C.Implicit _ as t -> t,subst,metasenv
    | C.Cast (te,ty) ->
       let te',subst,metasenv = liftaux subst metasenv k te in
       let ty',subst,metasenv = liftaux subst metasenv k ty in
        C.Cast (te',ty'),subst,metasenv
    | C.Prod (n,s,t) ->
       let s',subst,metasenv = liftaux subst metasenv k s in
       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
        C.Prod (n,s',t'),subst,metasenv
    | C.Lambda (n,s,t) ->
       let s',subst,metasenv = liftaux subst metasenv k s in
       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
        C.Lambda (n,s',t'),subst,metasenv
    | C.LetIn (n,s,ty,t) ->
       let s',subst,metasenv = liftaux subst metasenv k s in
       let ty',subst,metasenv = liftaux subst metasenv k ty in
       let t',subst,metasenv = liftaux subst metasenv (k+1) t in
        C.LetIn (n,s',ty',t'),subst,metasenv
    | C.Appl l ->
       let l',subst,metasenv =
        List.fold_right
         (fun t (l,subst,metasenv) ->
           let t',subst,metasenv = liftaux subst metasenv k t in
            t'::l,subst,metasenv) l ([],subst,metasenv) in
       C.Appl l',subst,metasenv
    | C.Const (uri,exp_named_subst) ->
       let exp_named_subst',subst,metasenv = 
        List.fold_right
         (fun (uri,t) (l,subst,metasenv) ->
           let t',subst,metasenv = liftaux subst metasenv k t in
            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
       in
        C.Const (uri,exp_named_subst'),subst,metasenv
    | C.MutInd (uri,tyno,exp_named_subst) ->
       let exp_named_subst',subst,metasenv = 
        List.fold_right
         (fun (uri,t) (l,subst,metasenv) ->
           let t',subst,metasenv = liftaux subst metasenv k t in
            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
       in
        C.MutInd (uri,tyno,exp_named_subst'),subst,metasenv
    | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
       let exp_named_subst',subst,metasenv = 
        List.fold_right
         (fun (uri,t) (l,subst,metasenv) ->
           let t',subst,metasenv = liftaux subst metasenv k t in
            (uri,t')::l,subst,metasenv) exp_named_subst ([],subst,metasenv)
       in
        C.MutConstruct (uri,tyno,consno,exp_named_subst'),subst,metasenv
    | C.MutCase (sp,i,outty,t,pl) ->
       let outty',subst,metasenv = liftaux subst metasenv k outty in
       let t',subst,metasenv = liftaux subst metasenv k t in
       let pl',subst,metasenv =
        List.fold_right
         (fun t (l,subst,metasenv) ->
           let t',subst,metasenv = liftaux subst metasenv k t in
            t'::l,subst,metasenv) pl ([],subst,metasenv)
       in
        C.MutCase (sp,i,outty',t',pl'),subst,metasenv
    | C.Fix (i, fl) ->
       let len = List.length fl in
       let liftedfl,subst,metasenv =
        List.fold_right
         (fun (name, i, ty, bo) (l,subst,metasenv) ->
           let ty',subst,metasenv = liftaux subst metasenv k ty in
           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
            (name,i,ty',bo')::l,subst,metasenv
         ) fl ([],subst,metasenv)
       in
        C.Fix (i, liftedfl),subst,metasenv
    | C.CoFix (i, fl) ->
       let len = List.length fl in
       let liftedfl,subst,metasenv =
        List.fold_right
         (fun (name, ty, bo) (l,subst,metasenv) ->
           let ty',subst,metasenv = liftaux subst metasenv k ty in
           let bo',subst,metasenv = liftaux subst metasenv (k+len) bo in
            (name,ty',bo')::l,subst,metasenv
         ) fl ([],subst,metasenv)
       in
        C.CoFix (i, liftedfl),subst,metasenv
 in
  liftaux subst metasenv k

let delift_rels subst metasenv n t =
  delift_rels_from subst metasenv 1 n t
*)