(*
    ||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: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)

open Printf

let debug = true
let debug_print s = if debug then prerr_endline (Lazy.force s) else ()

exception Error of string lazy_t
let fail msg = raise (Error msg)

type lowtac_status = {
        pstatus : NCic.obj;
        lstatus : LexiconEngine.status
}

type lowtactic = lowtac_status * int -> lowtac_status * int list * int list

type tac_status = {
        gstatus : Continuationals.Stack.t; 
        istatus : lowtac_status;
} 

type tactic = tac_status -> tac_status

type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input

let pp_tac_status status = 
  prerr_endline (NCicPp.ppobj status.istatus.pstatus)
;;

open Continuationals.Stack

let dot_tac status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | ([], _, [], _) :: _ as stack ->
        (* backward compatibility: do-nothing-dot *)
        stack
    | (g, t, k, tag) :: s ->
        match filter_open g, k with
        | loc :: loc_tl, _ -> 
             (([ loc ], t, loc_tl @+ k, tag) :: s) 
        | [], loc :: k ->
            assert (is_open loc);
            (([ loc ], t, k, tag) :: s)
        | _ -> fail (lazy "can't use \".\" here")
  in
   { status with gstatus = new_gstatus }
;;

let branch_tac status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | (g, t, k, tag) :: s ->
          match init_pos g with (* TODO *)
          | [] | [ _ ] -> fail (lazy "too few goals to branch");
          | loc :: loc_tl ->
               ([ loc ], [], [], `BranchTag) :: (loc_tl, t, k, tag) :: s
  in
   { status with gstatus = new_gstatus }
;;

let shift_tac status =
  let new_gstatus = 
    match status.gstatus with
    | (g, t, k, `BranchTag) :: (g', t', k', tag) :: s ->
          (match g' with
          | [] -> fail (lazy "no more goals to shift")
          | loc :: loc_tl ->
                (([ loc ], t @+ filter_open g @+ k, [],`BranchTag)
                :: (loc_tl, t', k', tag) :: s))
     | _ -> fail (lazy "can't shift goals here")
  in
   { status with gstatus = new_gstatus }
;;

let pos_tac i_s status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | ([ loc ], t, [],`BranchTag) :: (g', t', k', tag) :: s
      when is_fresh loc ->
        let l_js = List.filter (fun (i, _) -> List.mem i i_s) ([loc] @+ g') in
          ((l_js, t , [],`BranchTag)
           :: (([ loc ] @+ g') @- l_js, t', k', tag) :: s)
    | _ -> fail (lazy "can't use relative positioning here")
  in
   { status with gstatus = new_gstatus }
;;

let wildcard_tac status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | ([ loc ] , t, [], `BranchTag) :: (g', t', k', tag) :: s
       when is_fresh loc ->
            (([loc] @+ g', t, [], `BranchTag) :: ([], t', k', tag) :: s)
    | _ -> fail (lazy "can't use wildcard here")
  in
   { status with gstatus = new_gstatus }
;;

let merge_tac status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | (g, t, k,`BranchTag) :: (g', t', k', tag) :: s ->
        ((t @+ filter_open g @+ g' @+ k, t', k', tag) :: s)
    | _ -> fail (lazy "can't merge goals here")
  in
   { status with gstatus = new_gstatus }
;;
      
let focus_tac gs status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | s -> assert(gs <> []);
          let stack_locs =
            let add_l acc _ _ l = if is_open l then l :: acc else acc in
            fold ~env:add_l ~cont:add_l ~todo:add_l [] s
          in
          List.iter
            (fun g ->
              if not (List.exists (fun l -> goal_of_loc l = g) stack_locs) then
                fail (lazy (sprintf "goal %d not found (or closed)" g)))
            gs;
          (zero_pos gs, [], [], `FocusTag) :: deep_close gs s
  in
   { status with gstatus = new_gstatus }
;;

let unfocus_tac status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | ([], [], [], `FocusTag) :: s -> s
    | _ -> fail (lazy "can't unfocus, some goals are still open")
  in
   { status with gstatus = new_gstatus }
;;

let skip_tac status =
  let new_gstatus = 
    match status.gstatus with
    | [] -> assert false
    | (gl, t, k, tag) :: s -> 
        let gl = List.map switch_of_loc gl in
        if List.exists (function Open _ -> true | Closed _ -> false) gl then 
          fail (lazy "cannot skip an open goal")
        else 
          ([],t,k,tag) :: s
  in
   { status with gstatus = new_gstatus }
;;

let fold_tactic tac status =
  match status.gstatus with
  | [] -> assert false
  | (g, t, k, tag) :: s ->
      debug_print (lazy ("context length " ^string_of_int (List.length g)));
      let rec aux s go gc =
        function
        | [] -> s, go, gc
        | loc :: loc_tl ->
            debug_print (lazy "inner eval tactical");
            let s, go, gc =
              if List.exists ((=) (goal_of_loc loc)) gc then
                s, go, gc
              else
                match switch_of_loc loc with
                | Closed _ -> fail (lazy "cannot apply to a Closed goal")
                | Open n -> 
                   let s, go', gc' = tac (s,n) in
                   s, (go @- gc') @+ go', gc @+ gc'
            in
            aux s go gc loc_tl
      in
      let s0, go0, gc0 = status.istatus, [], [] in
      let sn, gon, gcn = aux s0 go0 gc0 g in
      debug_print (lazy ("opened: "
        ^ String.concat " " (List.map string_of_int gon)));
      debug_print (lazy ("closed: "
        ^ String.concat " " (List.map string_of_int gcn)));
      let stack =
        (zero_pos gon, t @~- gcn, k @~- gcn, tag) :: deep_close gcn s
      in
       { gstatus = stack; istatus = sn }
;;


let apply t (status,goal) =
 let _,_,metasenv, subst,_ = status.pstatus in
 let _,context,gty = List.assoc goal metasenv in
 let metasenv, subst, lexicon_status, t = 
   GrafiteDisambiguate.disambiguate_nterm (Some gty) status.lstatus context metasenv subst t 
 in
   prerr_endline ("termine disambiguato: " ^ NCicPp.ppterm ~context ~metasenv ~subst t);
   prerr_endline ("menv:" ^ NCicPp.ppmetasenv ~subst metasenv);
   prerr_endline ("subst:" ^ NCicPp.ppsubst subst ~metasenv);
   prerr_endline "fine napply";
   { status with lstatus = lexicon_status }, [goal], []
;;

let apply_tac t = fold_tactic (apply t) ;;