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

open Continuationals.Stack
open NTacStatus
module Ast = CicNotationPt

let id_tac status = status ;;
let print_tac message status = prerr_endline message; status ;;

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 block_tac l status =
  List.fold_left (fun status tac -> tac status) status l
;;

let compare_statuses ~past ~present =
 let _,_,past,_,_ = past.pstatus in 
 let _,_,present,_,_ = present.pstatus in 
 let closed = 
  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
 in
 let opened = 
   List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present)
 in
 opened, closed
;;



(* Exec and distribute_tac form a retraction pair:
    1) exec (distribute_tac low_tac) (s,i) = low_tac (s,i)
    2) tac [s]::G = G1::...::Gn::G' && G' is G with some goals closed =>
         distribute_tac (exec tac) [s]::G = (G1@...Gn)::G'
    3) tac G = distribute_tac (exec tac) G if  
       tac = distribute_tac lowtac
    4) atomic_tac t === distribute_tac (exec t)

   Note that executing an high tactic on a set of goals may be stronger
   than executing the same tactic on those goals, but once at a time
   (e.g. the tactic could perform a global analysis of the set of goals)
*)

let exec tac low_status g =
  let stack = [ [0,Open g], [], [], `NoTag ] in
  let status = tac { gstatus = stack ; istatus = low_status } in
   status.istatus
;;

let distribute_tac 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
        | [] -> 
            debug_print (lazy "no selected goals");
            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 sn = tac s n in
                   let go', gc' = compare_statuses ~past:s ~present:sn in
                   sn, ((go @+ [n]) @- 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 atomic_tac htac = distribute_tac (exec htac) ;;

let exact t status goal =
 let goalty = get_goalty status goal in
 let status, t = disambiguate status t (Some goalty) (ctx_of goalty) in
 instantiate status goal t
;;

let exact_tac t = distribute_tac (exact t) ;;

let find_in_context name context =
  let rec aux acc = function
    | [] -> raise Not_found
    | (hd,_) :: tl when hd = name -> acc
    | _ :: tl ->  aux (acc + 1) tl
  in
  aux 1 context
;;

let clear names status goal =
 let goalty = get_goalty status goal in
 let js =
   List.map 
     (fun name -> 
        try find_in_context name (ctx_of goalty)
        with Not_found -> 
          fail (lazy ("hypothesis '" ^ name ^ "' not found"))) 
     names
 in
 let n,h,metasenv,subst,o = status.pstatus in
 let metasenv,subst,_ = NCicMetaSubst.restrict metasenv subst goal js in
  { status with pstatus = n,h,metasenv,subst,o }
;;

let force f s = Lazy.force f s;;

let clear_tac names =
 if names = [] then id_tac else distribute_tac (clear names)
;;

let generalize0_tac args =
 if args = [] then id_tac
 else exact_tac ("",0,Ast.Appl (Ast.Implicit :: args))
;;

let select0_tac ~where:(wanted,_,where) ~job  =
 let found, postprocess = 
   match job with
   | `Substexpand argsno -> mk_in_scope, mk_out_scope argsno
   | `Collect l -> (fun s t -> l := t::!l; mk_in_scope s t), mk_out_scope 1
 in
 distribute_tac (fun status goal ->
   let goalty = get_goalty status goal in
   let path = 
     match where with None -> NCic.Implicit `Term | Some where -> where 
   in
   let status, newgoalty = 
     select_term status ~found ~postprocess goalty (wanted,path) 
   in
   let status, instance = 
     mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
   in
   instantiate status goal instance)
;;

let select_tac ~where ~job move_down_hyps = 
 let (wanted,hyps,where) = GrafiteDisambiguate.disambiguate_npattern where in
 let path = 
  match where with None -> NCic.Implicit `Term | Some where -> where in
 if not move_down_hyps then
  select0_tac ~where:(wanted,hyps,Some path) ~job
 else
  let path = 
   List.fold_left
     (fun path (name,path_name) -> NCic.Prod ("_",path_name,path))
     path (List.rev hyps)
  in
   block_tac [ 
     generalize0_tac (List.map (fun (name,_) -> Ast.Ident (name,None)) hyps);
     select0_tac ~where:(wanted,[],Some path) ~job;
     clear_tac (List.map fst hyps) ]
;;

let generalize_tac ~where = 
 let l = ref [] in
 block_tac [ 
   select_tac ~where ~job:(`Collect l) true; 
   force (lazy (distribute_tac (fun status goal ->
     let goalty = get_goalty status goal in
     (* unift (ctx_of goal) t s *)
     instantiate status goal 
       (mk_cic_term (ctx_of goalty) (NCic.Appl [NCic.Implicit `Term ; 
         term_of_cic_term (List.hd !l) (ctx_of goalty) ]))
   ))) ]
;;


let reopen status =
 let n,h,metasenv,subst,o = status.pstatus in
 let subst, newm = 
   List.partition 
    (function (_,(Some tag,_,_,_)) -> 
            tag <> NCicMetaSubst.in_scope_tag && 
            not (NCicMetaSubst.is_out_scope_tag tag)
    | _ -> true)
    subst 
 in
 let in_m, out_m = 
   List.partition
     (function (_,(Some tag,_,_,_)) -> 
         tag = NCicMetaSubst.in_scope_tag | _ -> assert false)
     newm
 in
 let metasenv = List.map (fun (i,(_,c,_,t)) -> i,(None,c,t)) in_m @ metasenv in
 let in_m = List.map fst in_m in
 let out_m = match out_m with [i] -> i | _ -> assert false in
 { status with pstatus = n,h,metasenv,subst,o }, in_m, out_m 
;;

let change ~where ~with_what status goal =
 let goalty = get_goalty status goal in
 let (wanted,_,where) = GrafiteDisambiguate.disambiguate_npattern where in
 let path = 
   match where with None -> NCic.Implicit `Term | Some where -> where 
 in
 let status, newgoalty = assert false (*
   select_term status 1 goalty (wanted,path)*) in
 let status, in_scope, out_scope = reopen status in
 let status =  List.fold_left (exact with_what) status in_scope in

 let j,(n,cctx,bo,_) = out_scope in
 let _ = typeof status (ctx_of goalty) (Obj.magic (n,cctx,bo))  in

 let n,h,metasenv,subst,o = status.pstatus in
 let subst = out_scope :: subst in
 let status = { status with pstatus = n,h,metasenv,subst,o } in

 let status, instance = 
   mk_meta status (ctx_of newgoalty) (`Decl newgoalty) 
 in
 instantiate status goal instance
;;

let apply t status goal = exact t status goal;;

let apply_tac t = distribute_tac (apply t) ;;
let change_tac ~where ~with_what = distribute_tac (change ~where ~with_what) ;;

type indtyinfo = {
        rightno: int;
        leftno: int;
        consno: int;
        lefts: NCic.term list;
        rights: NCic.term list;
        reference: NReference.reference;
 }
;;

let analyze_indty_tac ~what indtyref = distribute_tac (fun status goal ->
  let goalty = get_goalty status goal in
  let status, what = disambiguate status what None (ctx_of goalty) in
  let ty_what = typeof status (ctx_of what) what in 
  let r,consno,lefts,rights = analyse_indty status ty_what in
  let leftno = List.length rights in
  let rightno = List.length rights in
  indtyref := Some { 
    rightno = rightno; leftno = leftno; consno = consno;
    lefts = lefts; rights = rights; reference = r;
  };
  prerr_endline "FO";
  exec id_tac status goal)
;;

let elim_tac ~what ~where = 
  let indtyinfo = ref None in
  let sort = ref None in
  let compute_goal_sort_tac = distribute_tac (fun status goal ->
    let goalty = get_goalty status goal in
    let goalsort = typeof status (ctx_of goalty) goalty in
    prerr_endline "XXXXXXXX";
    sort := Some goalsort;
    exec id_tac status goal)
  in
  atomic_tac (block_tac [
    analyze_indty_tac ~what indtyinfo;    
    force (lazy (select_tac 
      ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true));
    print_tac "CIAO";
    compute_goal_sort_tac;
    print_tac "CIAO2";
    force (lazy (
     let sort = HExtlib.unopt !sort in
     let ity = HExtlib.unopt !indtyinfo in
     let NReference.Ref (uri, _) = ity.reference in
     let name = NUri.name_of_uri uri ^
      match term_of_cic_term sort (ctx_of sort) with
       | NCic.Sort NCic.Prop -> "_ind"
       | NCic.Sort _ -> "_rect"
       | _ -> assert false 
     in
     let holes = 
       HExtlib.mk_list Ast.Implicit (ity.leftno+1+ ity.consno + ity.rightno) in
     let eliminator = 
       let _,_,w = what in
       Ast.Appl(Ast.Ident(name,None)::holes @ [ w ])
     in
     exact_tac ("",0,eliminator))) ]) 
;;

let rewrite_tac ~dir ~what:(_,_,what) ~where =
 let name =
  match dir with `LeftToRight -> "eq_elim_r" | `RightToLeft -> "eq_ind"
 in
  block_tac
   [ select_tac ~where ~job:(`Substexpand 2) true;
     exact_tac
      ("",0,
       Ast.Appl(Ast.Ident(name,None)::HExtlib.mk_list Ast.Implicit 5 @
        [what]))]
;;

let intro_tac name =
 block_tac
  [ exact_tac
    ("",0,(Ast.Binder (`Lambda,
     (Ast.Ident (name,None),None),Ast.Implicit)));
     if name = "_" then clear_tac [name] else id_tac ]
;;

let cases ~what status goal =
 let gty = get_goalty status goal in
 let status, what = disambiguate status what None (ctx_of gty) in
 let ty = typeof status (ctx_of what) what in
 let ref, consno, _, _ = analyse_indty status ty in
 let t =
  NCic.Match (ref,NCic.Implicit `Term, term_of_cic_term what (ctx_of gty),
    HExtlib.mk_list (NCic.Implicit `Term) consno)
 in
 let ctx = ctx_of gty in
 let status,t,ty = refine status ctx (mk_cic_term ctx t) (Some gty) in
 instantiate status goal t
;;

let cases_tac ~what ~where = 
  let indtyinfo = ref None in
  atomic_tac 
   (block_tac [
      analyze_indty_tac ~what indtyinfo;
      force (lazy (select_tac 
        ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1))true));
      distribute_tac (cases ~what) ])
;;

let case1_tac name =
 let name = if name = "_" then "_clearme" else name in
 block_tac [ intro_tac name; 
             cases_tac 
              ~where:("",0,(None,[],None)) 
              ~what:("",0,Ast.Ident (name,None));
              if name = "_clearme" then clear_tac ["_clearme"] else id_tac ]
;;