(*
    ||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.Itl len -> n - shift
  | NCic.Ctx tl ->
      let rec aux k = function 
         | [] -> raise NotInTheList
         | (Cic.Rel m)::_ when m + shift = n -> k
         | _::tl -> aux (k+1) tl 
      in
       aux 1 tl
;;

exception Occur;;

let rec force_does_not_occur metasenv subst restrictions t =
 let rec aux k = function
    | C.Rel r when List.mem (r - k) restrictions -> raise Occur
    | C.Meta (n, l) as t ->
       (* we ignore the subst since restrict will take care of already
        * instantiated/restricted metavariabels *)
       let more_to_be_restricted = ref [] in
       let l' =
         let i = ref 0 in
         HExtlib.map_option 
           (fun t ->
             incr i ;
             try 
               let (*subst, metasenv,*) t = aux k t in Some t
             with Occur ->
               more_to_be_restricted := !i :: !more_to_be_restricted; None)
           l
       in
       if !more_to_be_restricted = [] then
         if l = l' then t else NCic.Meta (n, l')
       else
         let metasenv, subst, newmeta = 
           restrict metasenv subst n !more_to_be_restricted 
         in
           (*metasenv, subst,*) NCic.Meta (newmeta, l')
    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 in
   aux 0 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 (i+1) restrictions tl in
      if List.mem i restricted then
        metasenv, subst, restricted, tl'
      else
        try
          let metasenv, subst, hd' =
            let delifted_restricted = List.map ((+) ~-i) restricted in
             force_does_not_occur_in_context 
              metasenv susbst delifted_restricted hd
          in
           metasenv, subst, restricted, 
            (if hd' == hd && tl' == tl then orig else (hd' :: tl'))
        with Occur ->
            metasenv, subst, (i :: restricted), tl'

and restrict metasenv subst i restrictions =
  assert (restrictions <> []);
  try 
    let name, ctx, bo, ty = NCicUtils.lookup_subst i subst in
      try 
        let name, ctx, ty = NCicUtils.lookup_meta i metasenv in
        let metasenv, subst, restrictions, newctx = 
          erase_in_context metasenv subst 1 restrictions in
        let metasenv, subst, _ =  
          force_does_not_occur metasenv subst restrictions ty in
        let metasenv, subst, _ =  
          force_does_not_occur metasenv subst restrictions bo in
        (* we don't care newly generated bo/tys since up to subst they are
         * convertible (only metas are substituted for metas *)
        metasenv, subst, ?
      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
      let metasenv, subst, restrictions, newctx = 
        erase_in_context metasenv subst 1 restrictions 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 subst_entry = i,(name,ctx, NCic.Meta (j, irl - restrictions), ty) in
      List.map 
        (fun (n,x) as orig -> if i = n then metasenv_entry else orig) metasenv,
      subst_entry :: subst, j
    with 
    | NCicUtils.Meta_not_found _ -> assert false
    | 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))))))

(* 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 to_be_restricted = ref [] in
  let rec aux k = function
    | NCic.Rel n as t when n <= k -> t
    | NCic.Rel n -> 
        (try
          match List.nth context (n-k-1) with
          | _,NCic.Def (bo,_) -> 
                (try C.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 (NCicSubstitution.lift n bo))
          | _,NCic.Decl _ -> 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,_ = NCicUtil.lookup_subst i subst in
           aux k (NCicSubstitution.subst_meta l1 t)
         with NCicUtil.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 subst, metasenv, newmeta = 
                     restrict metasenv subst i restrictions 
                  in
                  (* return that meta *)
                  assert false
              | NCic.Irl len, NCic.Irl len1 when shift = 0 -> orig
              | NCic.Irl len, NCic.Irl len1 ->
                   NCic.Meta (i, (shift1 - shift, lc1))
              | _ -> 
                  let lc1 = NCicUtils.expand_local_context lc1 in
                  let rec deliftl j = function
                    | [] -> []
                    | t::tl ->
                        let tl = deliftl (j+1) tl in
                        try (aux (k+shift1) t)::tl
                        with
                        | NotInTheList | MetaSubstFailure _ ->
                            to_be_restricted := (i,j)::!to_be_restricted; 
                            tl
                  in
                  let l1 = deliftl 1 l1 in
                  C.Meta(i,l1)) (* or another ?k and possibly compress l1 *)
    | t -> NCicUtils.map (fun _ k -> k+1) k aux t
  in
  let t = aux 0 t in
  let metasenv, subst = restrict subst !to_be_restricted metasenv in
  metasenv, subst, t
;;

(*
  in
   let res =
    try
     deliftaux 0 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.                              *)
(* debug_print (lazy "First Order UnificationFailure during delift") ;
debug_print(lazy (sprintf
        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
        (ppterm subst t)
        (String.concat "; "
          (List.map
            (function Some t -> ppterm subst t | None -> "_") l
          )))); *)
      let msg = (lazy (sprintf
        "Error trying to abstract %s over [%s]: the algorithm only tried to abstract over bound variables"
        (ppterm ~metasenv subst t)
        (String.concat "; "
          (List.map
            (function Some t -> ppterm ~metasenv subst t | None -> "_")
            l))))
      in
       if
         List.exists
          (function
              Some t -> CicUtil.is_meta_closed (apply_subst subst t)
            | None -> true) l
       then
        raise (Uncertain msg)
       else
        raise (MetaSubstFailure msg)
   in
   let (metasenv, subst) = restrict subst !to_be_restricted metasenv in
    res, metasenv, subst
;;
*)

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