type binder_type =
   Declaration
 | Definition
;;

type metas_context = (int * Cic.term) list;;

type context = (binder_type * Cic.name * Cic.term) list;;

type sequent = context * Cic.term;;

let proof = ref (None : (metas_context * Cic.term * Cic.term) option);;
(*CSC: Quando facciamo Clear di una ipotesi, cosa succede? *)
(* Note: the sequent is redundant: it can be computed from the type of the   *)
(* metavariable and its context in the proof. We keep it just for efficiency *)
(* because computing the context of a term may be quite expensive.           *)
let goal = ref (None : (int * sequent) option);;

exception NotImplemented

(*CSC: Funzione che deve sparire!!! *)
let cic_context_of_context =
 List.map
  (function
      Declaration,_,t -> t
    | Definition,_,_ -> raise NotImplemented
  )
;;

let refine_meta meta term newmetasenv =
 let (metasenv,bo,ty) =
  match !proof with
     None -> assert false
   | Some (metasenv,bo,ty) -> metasenv,bo,ty
 in
  let metasenv' = newmetasenv @ (List.remove_assoc meta metasenv) in
  let bo' =
   let rec aux =
    let module C = Cic in
     function
        C.Rel _ as t -> t
      | C.Var _ as t  -> t
      | C.Meta meta' when meta=meta' -> term
      | C.Meta _ as t -> t
      | C.Sort _ as t -> t
      | C.Implicit as t -> t
      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
      | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
      | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
      | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
      | C.Appl l -> C.Appl (List.map aux l)
      | C.Const _ as t -> t
      | C.Abst _ as t -> t
      | C.MutInd _ as t -> t
      | C.MutConstruct _ as t -> t
      | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
         C.MutCase (sp,cookingsno,i,aux outt, aux t,
          List.map aux pl)
      | C.Fix (i,fl) ->
         let substitutedfl =
          List.map
           (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
            fl
         in
          C.Fix (i, substitutedfl)
      | C.CoFix (i,fl) ->
         let substitutedfl =
          List.map
           (fun (name,ty,bo) -> (name, aux ty, aux bo))
            fl
         in
          C.CoFix (i, substitutedfl)
   in
    aux bo
  in
   proof := Some (metasenv',bo',ty)
;;

let new_meta () =
 let metasenv =
  match !proof with
     None -> assert false
   | Some (metasenv,_,_) -> metasenv
 in
  let rec aux =
   function
      None,[] -> 1
    | Some n,[] -> n
    | None,(n,_)::tl -> aux (Some n,tl)
    | Some m,(n,_)::tl -> if n > m then aux (Some n,tl) else aux (Some m,tl)
  in
   1 + aux (None,metasenv)
;;

(* metas_in_term term                                                *)
(* Returns the ordered list of the metas that occur in [term].       *)
(* Duplicates are removed. The implementation is not very efficient. *)
let metas_in_term term =
 let module C = Cic in
  let rec aux =
   function
      C.Rel _
    | C.Var _ -> []
    | C.Meta n -> [n]
    | C.Sort _
    | C.Implicit -> []
    | C.Cast (te,ty) -> (aux te) @ (aux ty)
    | C.Prod (_,s,t) -> (aux s) @ (aux t)
    | C.Lambda (_,s,t) -> (aux s) @ (aux t)
    | C.LetIn (_,s,t) -> (aux s) @ (aux t)
    | C.Appl l -> List.fold_left (fun i t -> i @ (aux t)) [] l
    | C.Const _
    | C.Abst _
    | C.MutInd _
    | C.MutConstruct _ -> []
    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
       (aux outt) @ (aux t) @
        (List.fold_left (fun i t -> i @ (aux t)) [] pl)
    | C.Fix (i,fl) ->
        List.fold_left (fun i (_,_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
    | C.CoFix (i,fl) ->
        List.fold_left (fun i (_,ty,bo) -> i @ (aux bo) @ (aux ty)) [] fl
  in
   let metas = aux term in
    let rec elim_duplicates =
     function
        [] -> []
      | he::tl ->
         he::(elim_duplicates (List.filter (function el -> he <> el) tl))
    in
     elim_duplicates metas
;;

(* perforate context term ty                                                 *)
(* replaces the term [term] in the proof with a new metavariable whose type  *)
(* is [ty]. [context] must be the context of [term] in the whole proof. This *)
(* could be easily computed; so the only reasons to have it as an argument   *)
(* are efficiency reasons.                                                   *)
let perforate context term ty =
 let module C = Cic in
  let newmeta = new_meta () in
   match !proof with
      None -> assert false
    | Some (metasenv,bo,gty) ->
       (* We push the new meta at the end of the list for pretty-printing *)
       (* purposes: in this way metas are ordered.                        *)
       let metasenv' = metasenv@[newmeta,ty] in
       let rec aux =
        function
           (* Is == strong enough? *)
           t when t == term -> C.Meta newmeta
         | C.Rel _ as t -> t
         | C.Var _ as t  -> t
         | C.Meta _ as t -> t
         | C.Sort _ as t -> t
         | C.Implicit as t -> t
         | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
         | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
         | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
         | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
         | C.Appl l -> C.Appl (List.map aux l)
         | C.Const _ as t -> t
         | C.Abst _ as t -> t
         | C.MutInd _ as t -> t
         | C.MutConstruct _ as t -> t
         | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
            C.MutCase (sp,cookingsno,i,aux outt, aux t,
             List.map aux pl)
         | C.Fix (i,fl) ->
            let substitutedfl =
             List.map
              (fun (name,i,ty,bo) -> (name, i, aux ty, aux bo))
               fl
            in
             C.Fix (i, substitutedfl)
         | C.CoFix (i,fl) ->
            let substitutedfl =
             List.map
              (fun (name,ty,bo) -> (name, aux ty, aux bo))
               fl
            in
             C.CoFix (i, substitutedfl)
       in
        let bo' = aux bo in
        (* It may be possible that some metavariables occurred only in *)
        (* the term we are perforating and they now occurs no more. We *)
        (* get rid of them, collecting the really useful metavariables *)
        (* in metasenv''.                                              *)
         let newmetas = metas_in_term bo' in
          let metasenv'' =
           List.filter (function (n,_) -> List.mem n newmetas) metasenv'
          in
           proof := Some (metasenv'',bo',gty) ;
           goal := Some (newmeta,(context,ty)) ;
           newmeta
;;

(************************************************************)
(*                  Some easy tactics.                      *)
(************************************************************)

exception Fail of string;;

let intros () =
 let module C = Cic in
 let module R = CicReduction in
  let metasenv =
   match !proof with
      None -> assert false
    | Some (metasenv,_,_) -> metasenv
  in
  let (metano,context,ty) =
   match !goal with
      None -> assert false
    | Some (metano,(context,ty)) -> metano,context,ty
  in
   let newmeta = new_meta () in
    let rec collect_context =
     function
        C.Cast (te,_)   -> collect_context te
      | C.Prod (n,s,t)  ->
         let (ctx,ty,bo) = collect_context t in
          ((Declaration,n,s)::ctx,ty,C.Lambda(n,s,bo))
      | C.LetIn (n,s,t) ->
         let (ctx,ty,bo) = collect_context t in
          ((Definition,n,s)::ctx,ty,C.LetIn(n,s,bo))
      | _ as t -> [], t, (C.Meta newmeta)
    in
     let revcontext',ty',bo' = collect_context ty in
      let context'' = (List.rev revcontext') @ context in
       refine_meta metano bo' [newmeta,ty'] ;
       goal := Some (newmeta,(context'',ty'))
;;

(* The term bo must be closed in the current context *)
let exact bo =
 let module T = CicTypeChecker in
 let module R = CicReduction in
  let metasenv =
   match !proof with
      None -> assert false
    | Some (metasenv,_,_) -> metasenv
  in
  let (metano,context,ty) =
   match !goal with
      None -> assert false
    | Some (metano,(context,ty)) ->
       assert (ty = List.assoc metano metasenv) ;
       (* Invariant: context is the actual context of the meta in the proof *)
       metano,context,ty
  in
   (*CSC: deve sparire! *)
   let context = cic_context_of_context context in
    if R.are_convertible (T.type_of_aux' metasenv context bo) ty then
     refine_meta metano bo []
    else
     raise (Fail "The type of the provided term is not the one expected.")
;;