(* Copyright (C) 2002, HELM Team.
 * 
 * This file is part of HELM, an Hypertextual, Electronic
 * Library of Mathematics, developed at the Computer Science
 * Department, University of Bologna, Italy.
 * 
 * HELM is free software; you can redistribute it and/or
 * modify it under the terms of the GNU General Public License
 * as published by the Free Software Foundation; either version 2
 * of the License, or (at your option) any later version.
 * 
 * HELM is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with HELM; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
 * MA  02111-1307, USA.
 * 
 * For details, see the HELM World-Wide-Web page,
 * http://cs.unibo.it/helm/.
 *)

open AutoTypes;;

let debug_print s = ();;(*prerr_endline s;;*)

let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
let ugraph = CicUniv.empty_ugraph;;
let typeof = CicTypeChecker.type_of_aux';;
let ppterm ctx t = 
  let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
  CicPp.pp t names
;;
let is_in_prop context subst metasenv ty =
  let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
  fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
;;
let assert_proof_is_valid proof metasenv context goalty =
  let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
  let b,_ = CicReduction.are_convertible context ty goalty u in
  if not b then
    begin
      prerr_endline (CicPp.ppterm proof);
      prerr_endline (CicPp.ppterm ty);
      prerr_endline (CicPp.ppterm goalty);
    end;
  assert b
;;
let assert_subst_are_disjoint subst subst' =
  assert(List.for_all
    (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst') 
    subst)
;;
let sort_new_elems = 
  List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) 
;;

let split_goals_in_prop metasenv subst gl =
  List.partition 
    (fun g ->
      let _,context,ty = CicUtil.lookup_meta g metasenv in
      try
        let sort,u = typeof ~subst metasenv context ty ugraph in
        fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
      with 
      | CicTypeChecker.AssertFailure s 
      | CicTypeChecker.TypeCheckerFailure s -> 
          debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
          debug_print (Lazy.force s);
          false)
    (* FIXME... they should type! *)
    gl
;;

let split_goals_with_metas metasenv subst gl =
  List.partition 
    (fun g ->
      let _,context,ty = CicUtil.lookup_meta g metasenv in
      let ty = CicMetaSubst.apply_subst subst ty in
      CicUtil.is_meta_closed ty)
    gl
;;

let order_new_goals metasenv subst open_goals ppterm =
  let prop,rest = split_goals_in_prop metasenv subst open_goals in
  let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
  let open_goals =
    (List.map (fun x -> x,P) (closed_prop @ open_prop)) 
    @ 
    (List.map (fun x -> x,T) rest)
  in
  let tys = 
    List.map 
      (fun (i,_) -> 
        let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals 
  in
  debug_print ("   OPEN: "^
    String.concat " " 
      (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
  open_goals
;;

let try_candidate subst fake_proof goalno depth context cand =
  let ppterm = ppterm context in
  try 
    debug_print ("   PROVO: " ^ ppterm cand);
    let subst', ((_,metasenv,_,_), open_goals) =
      PrimitiveTactics.apply_with_subst ~term:cand ~subst (fake_proof,goalno) 
    in
    debug_print ("   OK: " ^ ppterm cand);
    (*FIXME:sicuro che posso @?*)
    assert_subst_are_disjoint subst subst';
    let subst = subst@subst' in
    let open_goals = order_new_goals metasenv subst open_goals ppterm in
    let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
    Some (metasenv,subst,open_goals) 
  with ProofEngineTypes.Fail s -> (*debug_print("   KO: "^Lazy.force s);*)None
;;

(* Works if there is no dependency over proofs *)
let is_a_green_cut goalty =
  CicUtil.is_meta_closed goalty
;;
let prop = function (_,_,P) -> true | _ -> false;;

let auto_main context flags elems cache universe =
  let timeout = 
    if flags.timeout = 0. then 
      infinity 
    else 
      Unix.gettimeofday () +. flags.timeout 
  in
  let ppterm = ppterm context in
  let irl = mk_irl context in
  let rec aux cache = function (* elems in OR *)
    | [] -> Fail "no more steps can be done", cache (* COMPLETE FAILURE *)
    | (metasenv,subst,[])::tl -> 
        Success (metasenv,subst,tl), cache (* solution::cont *)
    | (metasenv,subst,goals)::tl when 
      List.length (List.filter prop goals) > flags.maxwidth -> 
        debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
        aux cache tl (* FAILURE (width) *)
    | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl -> 
        if Unix.gettimeofday() > timeout then Fail "timeout",cache 
        else
        try
          let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
          debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
          if sort = T then
            (debug_print (" FAILURE(not in prop)");
            aux cache tl (* FAILURE (not in prop) *))
          else
          match aux_single cache metasenv subst elem goalty cc with
          | Fail _, cache -> 
              debug_print (" FAIL: " ^string_of_int goalno^ ":"^ppterm goalty);
              let cache = cache_add_failure cache goalty depth in
              aux cache tl
          | Success (metasenv,subst,others), cache ->
              (* others are alternatives in OR *)
              try
                let goal = Cic.Meta(goalno,irl) in
                let proof = CicMetaSubst.apply_subst subst goal in
                debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
                if is_a_green_cut goalty then
                  (assert_proof_is_valid proof metasenv context goalty;
                  let cache = cache_add_success cache goalty proof in
                  aux cache ((metasenv,subst,gl)::tl))
                else
                  (let goalty = CicMetaSubst.apply_subst subst goalty in
                  assert_proof_is_valid proof metasenv context goalty;
                  let cache = 
                    if is_a_green_cut goalty then
                      cache_add_success cache goalty proof
                    else
                      cache
                  in
                  let others = 
                    List.map 
                      (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl)) 
                    others
                  in 
                  aux cache ((metasenv,subst,gl)::others@tl))
              with CicUtil.Meta_not_found i when i = goalno ->
                assert false
        with CicUtil.Meta_not_found i when i = goalno -> 
          (* goalno was closed by sideeffect *)
          aux cache ((metasenv,subst,gl)::tl)
  and aux_single cache metasenv subst (goalno, depth, _) goalty cc =
    let goalty = CicMetaSubst.apply_subst subst goalty in
(*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
      (* FAILURE (euristic cut) *)
    match cache_examine cache goalty with
    | Failed_in d when d >= depth -> Fail "depth",cache(*FAILURE(depth)*)
    | Succeded t -> 
        assert(List.for_all (fun (i,_) -> i <> goalno) subst);
        let entry = goalno, (cc, t,goalty) in
        assert_subst_are_disjoint subst [entry];
        let subst = entry :: subst in
        let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
        debug_print ("  CACHE HIT!");
        Success (metasenv, subst, []),cache
    | UnderInspection -> Fail "looping",cache
    | Notfound 
    | Failed_in _ when depth > 0 -> (* we have more depth now *)
        let cache = cache_add_underinspection cache goalty depth in
        let candidates = get_candidates universe goalty in
        let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
        let elems = 
          HExtlib.filter_map
            (try_candidate subst fake_proof goalno depth context)
            candidates
        in
        let elems = sort_new_elems elems in
        aux cache elems
    | _ -> Fail "??",cache 
  in
    aux cache elems
;;
    
let auto universe cache context metasenv gl flags =
  let goals = order_new_goals metasenv [] gl CicPp.ppterm in
  let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
  let elems = [metasenv,[],goals] in
  match auto_main context flags elems cache universe with
  | Fail s,cache -> prerr_endline s;None,cache
  | Success (metasenv,subst,_), cache -> Some (subst,metasenv), cache
;;

let auto_all_solutions universe cache context metasenv gl flags =
  let goals = order_new_goals metasenv [] gl CicPp.ppterm in
  let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
  let elems = [metasenv,[],goals] in
  let bigbang = Unix.gettimeofday () in
  let rec aux solutions cache elems flags =
    match auto_main context flags elems cache universe with
    | Fail s,cache ->prerr_endline s; solutions,cache
    | Success (metasenv,subst,others), cache -> 
        let elapsed = Unix.gettimeofday () -. bigbang in
        if elapsed > flags.timeout then
          ((subst,metasenv)::solutions), cache
        else
          aux ((subst,metasenv)::solutions) cache others 
            {flags with timeout = flags.timeout -. elapsed}
  in
  aux [] cache elems flags
;;