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

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

type tactic = tac_status -> tac_status

type tactic_term = CicNotationPt.term Disambiguate.disambiguator_input
type tactic_pattern = GrafiteAst.npattern Disambiguate.disambiguator_input

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

let pp_lowtac_status status = 
  prerr_endline "--------------------------------------------";
  prerr_endline (NCicPp.ppobj status.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 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 
 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i past)) present),
 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
;;



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

   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
        | [] -> 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 @- 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 }
;;

type cic_term = NCic.conjecture
type ast_term = string * int * CicNotationPt.term
type position = [ `Ctx of NCic.context | `Term of cic_term ]


let relocate context (name,ctx,t as term) =
  let is_prefix l1 l2 =
    let rec aux = function
      | [],[] -> true
      | x::xs, y::ys -> x=y && aux (xs,ys)
      | _ -> false
    in
      aux (List.rev l1, List.rev l2)
  in
  if ctx = context then term else 
  if is_prefix ctx context then 
    (name, context, 
      NCicSubstitution.lift (List.length context - List.length ctx) t)
  else
    assert false
;;

let disambiguate (status : lowtac_status) (t : ast_term)  
                 (ty : cic_term option) (where : position) =
 let uri,height,metasenv,subst,obj = status.pstatus in
 let context = match where with `Ctx c -> c | `Term (_,c,_) -> c in
 let expty = 
   match ty with 
   | None -> None | Some ty -> let _,_,x = relocate context ty in Some x 
 in
 let metasenv, subst, lexicon_status, t = 
   GrafiteDisambiguate.disambiguate_nterm expty
    status.lstatus context metasenv subst t 
 in
 let new_pstatus = uri,height,metasenv,subst,obj in
 { lstatus = lexicon_status; pstatus = new_pstatus }, (None, context, t) 
;;

let in_scope_tag = "tag:in_scope" ;;
let out_scope_tag = "tag:out_scope" ;;

let typeof status where t =
  let _,_,metasenv,subst,_ = status.pstatus in
  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
  let _,_,t = relocate ctx t in
  let ty = NCicTypeChecker.typeof ~subst ~metasenv ctx t in
  None, ctx, ty
;;
  
let whd status ?delta where t =
  let _,_,metasenv,subst,_ = status.pstatus in
  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
  let _,_,t = relocate ctx t in
  let t = NCicReduction.whd ~subst ?delta ctx t in
  None, ctx, t
;;
  
let unify status where a b =
  let n,h,metasenv,subst,o = status.pstatus in
  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
  let _,_,a = relocate ctx a in
  let _,_,b = relocate ctx b in
  let metasenv, subst = 
    NCicUnification.unify (NCicUnifHint.db ()) metasenv subst ctx a b
  in
  { status with pstatus = n,h,metasenv,subst,o }
;;

let refine status where term expty =
  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
  let nt,_,term = relocate ctx term in
  let ne, ty = 
    match expty with None -> None, None 
    | Some e -> let n,_, e = relocate ctx e in Some n, Some e
  in
  let name,height,metasenv,subst,obj = status.pstatus in
  let db = NCicUnifHint.db () in (* XXX fixme *)
  let coercion_db = NCicCoercion.db () in
  let look_for_coercion = NCicCoercion.look_for_coercion coercion_db in
  let metasenv, subst, t, ty = 
   NCicRefiner.typeof db ~look_for_coercion metasenv subst ctx term ty
  in
  { status with pstatus = (name,height,metasenv,subst,obj) }, 
  (nt,ctx,t), (ne,ctx,ty)
;;

let get_goal (status : lowtac_status) (g : int) =
 let _,_,metasenv,_,_ = status.pstatus in
 List.assoc g metasenv
;;

let instantiate status i t =
 let (goalname, context, _ as ety) = get_goal status i in
 let status, (_,_,t), (_,_,ty) = refine status (`Term ety) t (Some ety) in

 let name,height,metasenv,subst,obj = status.pstatus in
 let metasenv = List.filter (fun j,_ -> j <> i) metasenv in
 let subst = (i, (goalname, context, t, ty)) :: subst in
 { status with pstatus = (name,height,metasenv,subst,obj) }
;;

let mk_meta status ?name where bo_or_ty =
  let n,h,metasenv,subst,o = status.pstatus in
  let ctx = match where with `Ctx c -> c | `Term (_,c,_) -> c in
  match bo_or_ty with
  | `Decl ty ->
      let _,_,ty = relocate ctx ty in
      let metasenv, _, instance, _ = 
        NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
      in
      let status = { status with pstatus = n,h,metasenv,subst,o } in
      status, (None,ctx,instance)
  | `Def bo ->
      let _,_,ty = typeof status (`Ctx ctx) bo in
      let metasenv, metano, instance, _ = 
        NCicMetaSubst.mk_meta ?name metasenv ctx (`WithType ty)
      in
      let status = { status with pstatus = n,h,metasenv,subst,o } in
      let status = instantiate status metano bo in
      status, (None,ctx,instance)
;;

let select_term low_status (name,context,term) (wanted,path) =
  let found status ctx t wanted =
    (* we could lift wanted step-by-step *)
    try true, unify status (`Ctx ctx) (None,ctx,t) wanted
    with 
    | NCicUnification.UnificationFailure _ 
    | NCicUnification.Uncertain _ -> false, status
  in
  let match_term status ctx (wanted : cic_term) t =
    let rec aux ctx status t =
      let b, status = found status ctx t wanted in
      if b then 
        let status, (_,_,t) = 
          mk_meta status ~name:in_scope_tag (`Ctx ctx) (`Def (None,ctx,t))
        in    
        status, t
      else NCicUntrusted.map_term_fold_a (fun e c -> e::c) ctx aux status t
     in 
       aux ctx status t
  in 
  let rec select status ctx pat cic = 
    match pat, cic with
    | NCic.LetIn (_,t1,s1,b1), NCic.LetIn (n,t2,s2,b2) ->
        let status, t = select status ctx t1 t2 in
        let status, s = select status ctx s1 s2 in
        let ctx = (n, NCic.Def (s2,t2)) :: ctx in
        let status, b = select status ctx b1 b2 in
        status, NCic.LetIn (n,t,s,b)
    | NCic.Lambda (_,s1,t1), NCic.Lambda (n,s2,t2) ->
        let status, s = select status ctx s1 s2 in
        let ctx = (n, NCic.Decl s2) :: ctx in
        let status, t = select status ctx t1 t2 in
        status, NCic.Lambda (n,s,t)
    | NCic.Prod (_,s1,t1), NCic.Prod (n,s2,t2) ->
        let status, s = select status ctx s1 s2 in
        let ctx = (n, NCic.Decl s2) :: ctx in
        let status, t = select status ctx t1 t2 in
        status, NCic.Prod (n,s,t)
    | NCic.Appl l1, NCic.Appl l2 ->
        let status, l = 
           List.fold_left2
             (fun (status,l) x y -> 
              let status, x = select status ctx x y in
              status, x::l)
             (status,[]) l1 l2
        in
        status, NCic.Appl (List.rev l)
    | NCic.Match (_,ot1,t1,pl1), NCic.Match (u,ot2,t2,pl2) ->
        let status, t = select status ctx t1 t2 in
        let status, ot = select status ctx ot1 ot2 in
        let status, pl = 
           List.fold_left2
             (fun (status,l) x y -> 
              let status, x = select status ctx x y in
              status, x::l)
             (status,[]) pl1 pl2
        in
        status, NCic.Match (u,ot,t,List.rev pl)
    | NCic.Implicit `Hole, t -> 
        (match wanted with
        | Some wanted -> 
             let status, wanted = disambiguate status wanted None (`Ctx ctx) in
             match_term status ctx wanted t
        | None -> match_term status ctx (None,ctx,t) t)
    | NCic.Implicit _, t -> status, t
    | _,t -> 
        fail (lazy ("malformed pattern: " ^ NCicPp.ppterm ~metasenv:[]
          ~context:[] ~subst:[] pat))
  in
  let status, term = select low_status context path term in
  let term = (name, context, term) in
  mk_meta status ~name:out_scope_tag (`Ctx context) (`Def term)
;;

let select ~where status goal = 
 let name, _, _ as goalty = get_goal 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 = select_term status goalty (wanted,path) in
 let status, instance = 
   mk_meta status ?name (`Term newgoalty) (`Decl newgoalty) 
 in
 instantiate status goal instance
;;

let select_tac ~where = distribute_tac (select ~where) ;;

let exact t status goal =
 let goalty = get_goal status goal in
 let status, t = disambiguate status t (Some goalty) (`Term goalty) in
 instantiate status goal t
;;

let exact_tac t = distribute_tac (exact t) ;;

let reopen status =
 let n,h,metasenv,subst,o = status.pstatus in
 let subst, newm = 
   List.partition 
    (function (_,(Some tag,_,_,_)) -> tag <> in_scope_tag && tag <> out_scope_tag
    | _ -> true)
    subst 
 in
 let in_m, out_m = 
   List.partition
     (function (_,(Some tag,_,_,_)) -> tag = 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 (name,_,_ as goalty) = get_goal 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 = select_term status 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 (`Term goalty) (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 ?name (`Term 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) ;;

let elim_tac ~what ~where status =
 block_tac
   [ select_tac ~where;
     distribute_tac (fun status goal ->
       let goalty = get_goal status goal in
       let status, (_,_,w as what) = 
         disambiguate status what None (`Term goalty) in
       let _ty_what = typeof status (`Term what) what in 
       (* check inductive... find eliminator *)
       let w = (*astify what *) CicNotationPt.Ident ("m",None) in
       let holes = [ 
         CicNotationPt.Implicit;CicNotationPt.Implicit;CicNotationPt.Implicit]
       in
       let eliminator = 
         CicNotationPt.Appl(CicNotationPt.Ident("nat_ind",None)::holes @ [ w ])
       in
       exec (apply_tac ("",0,eliminator)) status goal) ] 
   status
;;

let intro_tac name =
 exact_tac
  ("",0,(CicNotationPt.Binder (`Lambda,
   (CicNotationPt.Ident (name,None),None),CicNotationPt.Implicit)))
;;

let analyse_indty status ty = 
 let ref, args =
  match whd status (`Term ty) ty with
   | _,_,NCic.Const ref -> ref, []
   | _,_,NCic.Appl (NCic.Const ref :: args) -> ref, args
   | _,_,_ -> fail (lazy ("not an inductive type")) in
 let _,lno,tl,_,i = NCicEnvironment.get_checked_indtys ref in
 let _,_,_,cl = List.nth tl i in
 let consno = List.length cl in
 let left, right = HExtlib.split_nth lno args in
 ref, consno, left, right
;;

let case status goal =
 let _,ctx,_ = get_goal status goal in
 let ty = typeof status (`Ctx ctx) ("",ctx,NCic.Rel 1) in
 let ref, consno, left, right = analyse_indty status ty in
 let t =
  NCic.Match (ref,NCic.Implicit `Term,NCic.Rel 1,
    HExtlib.mk_list (NCic.Implicit `Term) consno)
 in
 let status,t,ty = refine status (`Ctx ctx) ("",ctx,t) None in
 instantiate status goal t
;;

let case_tac = distribute_tac case;;

let case1_tac name =
 block_tac [ intro_tac name; case_tac ]
;;