(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

(* JCF -- 6 janvier 1998  EXPERIMENTAL *)

(*
 *  L'idée est, en quelque sorte, d'avoir de "vraies" métavariables
 *  dans Coq, c'est-à-dire de donner des preuves incomplètes -- mais
 *  où les trous sont typés -- et que les sous-buts correspondants
 *  soient engendrés pour finir la preuve.
 *
 *  Exemple :
 *    J'ai le but
 *        forall (x:nat), { y:nat | (minus y x) = x }
 *    et je donne la preuve incomplète
 *        fun (x:nat) => exist nat [y:nat]((minus y x)=x) (plus x x) ?
 *    ce qui engendre le but
 *        (minus (plus x x) x) = x
 *)

(*  Pour cela, on procède de la manière suivante :
 *
 *  1. Un terme de preuve incomplet est un terme contenant des variables
 *     existentielles Evar i.e. "_" en syntaxe concrète.
 *     La résolution de ces variables n'est plus nécessairement totale
 *     (ise_resolve called with fail_evar=false) et les variables
 *     existentielles restantes sont remplacées par des méta-variables
 *     castées par leur types (celui est connu : soit donné, soit trouvé
 *     pendant la phase de résolution).
 *
 *  2. On met ensuite le terme "à plat" i.e. on n'autorise des MV qu'au
 *     permier niveau et pour chacune d'elles, si nécessaire, on donne
 *     à son tour un terme de preuve incomplet pour la résoudre.
 *     Exemple: le terme (f a _ (fun (x:nat) => e _)) donne
 *         (f a ?1 ?2) avec:
 *           - ?2 := fun (x:nat) => ?3
 *           - ?3 := e ?4
 *         ?1 et ?4 donneront des buts
 *
 *  3. On écrit ensuite une tactique tcc qui engendre les sous-buts
 *     à partir d'une preuve incomplète.
 *)

open Pp
open Util
open Names
open Term
open Termops
open Namegen
open Tacmach
open Sign
open Environ
open Reduction
open Typing
open Tactics
open Tacticals
open Printer

type term_with_holes = TH of constr * meta_type_map * sg_proofs
and  sg_proofs       = (term_with_holes option) list

(* pour debugger *)

let rec pp_th (TH(c,mm,sg)) =
  (str"TH=[ " ++ hov 0 (pr_lconstr c ++ fnl () ++
			      (* pp_mm mm ++ fnl () ++ *)
			   pp_sg sg) ++ str "]")
and pp_mm l =
  hov 0 (prlist_with_sep (fun _ -> (fnl ()))
	   (fun (n,c) -> (int n ++ str" --> " ++ pr_lconstr c)) l)
and pp_sg sg =
  hov 0 (prlist_with_sep (fun _ -> (fnl ()))
	   (function None -> (str"None") | Some th -> (pp_th th)) sg)

(*  compute_metamap : constr -> 'a evar_map -> term_with_holes
 *  réalise le 2. ci-dessus
 *
 *  Pour cela, on renvoie une meta_map qui indique pour chaque meta-variable
 *  si elle correspond à un but (None) ou si elle réduite à son tour
 *  par un terme de preuve incomplet (Some c).
 *
 *  On a donc l'INVARIANT suivant : le terme c rendu est "de niveau 1"
 *  -- i.e. à plat -- et la meta_map contient autant d'éléments qu'il y
 *  a de meta-variables dans c. On suppose de plus que l'ordre dans la
 *  meta_map correspond à celui des buts qui seront engendrés par le refine.
 *)

let replace_by_meta env sigma = function
  | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
  | (TH (c,mm,_)) as th ->
      let n = Evarutil.new_meta() in
      let m = mkMeta n in
      (* quand on introduit une mv on calcule son type *)
      let ty = match kind_of_term c with
	| Lambda (Name id,c1,c2) when isCast c2 ->
	    let _,_,t = destCast c2 in mkNamedProd id c1 t
	| Lambda (Anonymous,c1,c2) when isCast c2 ->
	    let _,_,t = destCast c2 in mkArrow c1 t
	| _ -> (* (App _ | Case _) -> *)
	    let sigma' =
	      List.fold_right (fun (m,t) sigma -> Evd.meta_declare m t sigma)
		mm sigma in
	    Retyping.get_type_of env sigma' c
	(*
	| Fix ((_,j),(v,_,_)) ->
	    v.(j) (* en pleine confiance ! *)
	| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
        *)
      in
      mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]

exception NoMeta

let replace_in_array keep_length env sigma a =
  if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
    raise NoMeta;
  let a' = Array.map (function
			| (TH (c,mm,[])) when not keep_length -> c,mm,[]
			| th -> replace_by_meta env sigma th) a
  in
  let v' = Array.map pi1 a' in
  let mm = Array.fold_left (@) [] (Array.map pi2 a') in
  let sgp = Array.fold_left (@) [] (Array.map pi3 a') in
  v',mm,sgp

let fresh env n =
  let id = match n with Name x -> x | _ -> id_of_string "_H" in
  next_ident_away_in_goal id (ids_of_named_context (named_context env))

let rec compute_metamap env sigma c = match kind_of_term c with
  (* le terme est directement une preuve *)
  | (Const _ | Evar _ | Ind _ | Construct _ |
    Sort _ | Var _ | Rel _) ->
      TH (c,[],[])

  (* le terme est une mv => un but *)
  | Meta n ->
      TH (c,[],[None])

  | Cast (m,_, ty) when isMeta m ->
      TH (c,[destMeta m,ty],[None])


  (* abstraction => il faut décomposer si le terme dessous n'est pas pur
   *    attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
   *    où x est une variable FRAICHE *)
  | Lambda (name,c1,c2) ->
      let v = fresh env name in
      let env' = push_named (v,None,c1) env in
      begin match compute_metamap env' sigma (subst1 (mkVar v) c2) with
	(* terme de preuve complet *)
	| TH (_,_,[]) -> TH (c,[],[])
	(* terme de preuve incomplet *)
	| th ->
	    let m,mm,sgp = replace_by_meta env' sigma th in
	    TH (mkLambda (Name v,c1,m), mm, sgp)
      end

  | LetIn (name, c1, t1, c2) ->
      let v = fresh env name in
      let th1 = compute_metamap env sigma c1 in
      let env' = push_named (v,Some c1,t1) env in
      let th2 = compute_metamap env' sigma (subst1 (mkVar v) c2) in
      begin match th1,th2 with
	(* terme de preuve complet *)
	| TH (_,_,[]), TH (_,_,[]) -> TH (c,[],[])
	(* terme de preuve incomplet *)
	| TH (c1,mm1,sgp1), TH (c2,mm2,sgp2) ->
	    let m1,mm1,sgp1 =
              if sgp1=[] then (c1,mm1,[])
              else replace_by_meta env sigma th1 in
	    let m2,mm2,sgp2 =
              if sgp2=[] then (c2,mm2,[])
              else replace_by_meta env' sigma th2 in
	    TH (mkNamedLetIn v m1 t1 m2, mm1@mm2, sgp1@sgp2)
      end

  (* 4. Application *)
  | App (f,v) ->
      let a = Array.map (compute_metamap env sigma) (Array.append [|f|] v) in
      begin
	try
	  let v',mm,sgp = replace_in_array false env sigma a in
          let v'' = Array.sub v' 1 (Array.length v) in
          TH (mkApp(v'.(0), v''),mm,sgp)
	with NoMeta ->
	  TH (c,[],[])
      end

  | Case (ci,p,cc,v) ->
      (* bof... *)
      let nbr = Array.length v in
      let v = Array.append [|p;cc|] v in
      let a = Array.map (compute_metamap env sigma) v in
      begin
	try
	  let v',mm,sgp = replace_in_array false env sigma a in
	  let v'' = Array.sub v' 2 nbr in
	  TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
	with NoMeta ->
	  TH (c,[],[])
      end

  (* 5. Fix. *)
  | Fix ((ni,i),(fi,ai,v)) ->
      (* TODO: use a fold *)
      let vi = Array.map (fresh env) fi in
      let fi' = Array.map (fun id -> Name id) vi in
      let env' = push_named_rec_types (fi',ai,v) env in
      let a = Array.map
		(compute_metamap env' sigma)
		(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
      in
      begin
	try
	  let v',mm,sgp = replace_in_array true env' sigma a in
	  let fix = mkFix ((ni,i),(fi',ai,v')) in
	  TH (fix,mm,sgp)
	with NoMeta ->
	  TH (c,[],[])
      end

  (* Cast. Est-ce bien exact ? *)
  | Cast (c,_,t) -> compute_metamap env sigma c
      (*let TH (c',mm,sgp) = compute_metamap sign c in
	TH (mkCast (c',t),mm,sgp) *)

  (* Produit. Est-ce bien exact ? *)
  | Prod (_,_,_) ->
      if occur_meta c then
	error "refine: proof term contains metas in a product."
      else
      	TH (c,[],[])

  (* Cofix. *)
  | CoFix (i,(fi,ai,v)) ->
      let vi = Array.map (fresh env) fi in
      let fi' = Array.map (fun id -> Name id) vi in
      let env' = push_named_rec_types (fi',ai,v) env in
      let a = Array.map
		(compute_metamap env' sigma)
		(Array.map (substl (List.map mkVar (Array.to_list vi))) v)
      in
      begin
	try
	  let v',mm,sgp = replace_in_array true env' sigma a in
	  let cofix = mkCoFix (i,(fi',ai,v')) in
	  TH (cofix,mm,sgp)
	with NoMeta ->
	  TH (c,[],[])
      end


(*  tcc_aux : term_with_holes -> tactic
 *
 *  Réalise le 3. ci-dessus
 *)

let ensure_products n =
  let p = ref 0 in
  let rec aux n gl =
    if n = 0 then tclFAIL 0 (mt()) gl
    else
      tclTHEN
        (tclORELSE intro (fun gl -> incr p; introf gl))
        (aux (n-1)) gl in
  tclORELSE
    (aux n)
    (* Now we know how many red are needed *)
    (fun gl -> tclDO !p red_in_concl gl)

let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
  let c = substl subst c in
  match (kind_of_term c,sgp) with
    (* mv => sous-but : on ne fait rien *)
    | Meta _ , _ ->
	tclIDTAC gl

    | Cast (c,_,_), _ when isMeta c ->
	tclIDTAC gl

    (* terme pur => refine *)
    | _,[] ->
	refine c gl

    (* abstraction => intro *)
    | Lambda (Name id,_,m), _ ->
	assert (isMeta (strip_outer_cast m));
	begin match sgp with
	  | [None] -> intro_mustbe_force id gl
	  | [Some th] ->
              tclTHEN (introduction id)
                (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)) gl
	  | _ -> assert false
	end

    | Lambda (Anonymous,_,m), _ -> (* if anon vars are allowed in evars *)
        assert (isMeta (strip_outer_cast m));
	begin match sgp with
	  | [None] -> tclTHEN intro (onLastHypId (fun id -> clear [id])) gl
	  | [Some th] ->
              tclTHEN
                intro
                (onLastHypId (fun id ->
                  tclTHEN
                    (clear [id])
                    (tcc_aux (mkVar (*dummy*) id::subst) th))) gl
	  | _ -> assert false
	end

    (* let in without holes in the body => possibly dependent intro *)
    | LetIn (Name id,c1,t1,c2), _ when not (isMeta (strip_outer_cast c1)) ->
	let c = pf_concl gl in
	let newc = mkNamedLetIn id c1 t1 c in
	tclTHEN
	  (change_in_concl None newc)
	  (match sgp with
	     | [None] -> introduction id
	     | [Some th] ->
                 tclTHEN (introduction id)
                   (onLastHypId (fun id -> tcc_aux (mkVar id::subst) th))
	     | _ -> assert false)
	  gl

    (* let in with holes in the body => unable to handle dependency
       because of evars limitation, use non dependent assert instead *)
    | LetIn (Name id,c1,t1,c2), _ ->
	tclTHENS
          (assert_tac (Name id) t1)
	  [(match List.hd sgp with
	     | None -> tclIDTAC
	     | Some th -> onLastHypId (fun id -> tcc_aux (mkVar id::subst) th));
           (match List.tl sgp with
	     | [] -> refine (subst1 (mkVar id) c2)  (* a complete proof *)
	     | [None] -> tclIDTAC                   (* a meta *)
	     | [Some th] ->                         (* a partial proof *)
                 onLastHypId (fun id -> tcc_aux (mkVar id::subst) th)
             | _ -> assert false)]
          gl

    (* fix => tactique Fix *)
    | Fix ((ni,j),(fi,ai,_)) , _ ->
	let out_name = function
	  | Name id -> id
          | _ -> error "Recursive functions must have names."
	in
	let fixes = array_map3 (fun f n c -> (out_name f,succ n,c)) fi ni ai in
	let firsts,lasts = list_chop j (Array.to_list fixes) in
	tclTHENS
	  (tclTHEN
            (ensure_products (succ ni.(j)))
            (mutual_fix (out_name fi.(j)) (succ ni.(j)) (firsts@List.tl lasts) j))
	  (List.map (function
		       | None -> tclIDTAC
		       | Some th -> tcc_aux subst th) sgp)
	  gl

    (* cofix => tactique CoFix *)
    | CoFix (j,(fi,ai,_)) , _ ->
	let out_name = function
	  | Name id -> id
          | _ -> error "Recursive functions must have names."
	in
	let cofixes = array_map2 (fun f c -> (out_name f,c)) fi ai in
	let firsts,lasts = list_chop j (Array.to_list cofixes) in
	tclTHENS
	  (mutual_cofix (out_name fi.(j)) (firsts@List.tl lasts) j)
	  (List.map (function
		       | None -> tclIDTAC
		       | Some th -> tcc_aux subst th) sgp)
	  gl

    (* sinon on fait refine du terme puis appels rec. sur les sous-buts.
     * c'est le cas pour App et MutCase. *)
    | _ ->
	tclTHENS
	  (refine c)
	  (List.map
            (function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp)
	  gl

(* Et finalement la tactique refine elle-même : *)

let refine (evd,c) gl =
  let sigma = project gl in
  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals (pf_env gl) evd in
  let c = Evarutil.nf_evar evd c in
  let (evd,c) = Evarutil.evars_to_metas sigma (evd,c) in
  (* Relies on Cast's put on Meta's by evars_to_metas, because it is otherwise
     complicated to update meta types when passing through a binder *)
  let th = compute_metamap (pf_env gl) evd c in
  tclTHEN (Refiner.tclEVARS evd) (tcc_aux [] th) gl