(*
    Copyright (C) 2003-19 Richard Bornat & Bernard Sufrin
     
        richard@bornat.me.uk
        sufrin@comlab.ox.ac.uk

    This file is part of the jape proof engine, which is part of jape.

    Jape 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.

    Jape 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 jape; if not, write to the Free Software
    Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
    (or look at http://www.gnu.org).

*)

open Answer
open Cxtfuns
open Cxtstring
open Cxtexterior
open Cxtprovisos
open Cxttype
open Facts
open Listfuns
open Mappingfuns
open Miscellaneous
open Optionfuns
open Provisotype (* ok. RB *)
open Proviso
open Rewinf
open Sequent
open Sml
open Substmapfuns
open Termfuns
open Termstore
open Termstring
open Termtype

(* in 09/2020, this file hadn't been touched since the camlp4 translation from SML-NJ. 
   It's still hardly been cosmeticised.
 *)
let consolereport = Miscellaneous.consolereport
let idf = fun x -> x
let string_of_rewinf = Rewinf.string_of_rewinf

let rewritedebug = ref false
(* the rewrite functions rewrite a term/sequent/proviso, 
   returning Some .. if it rewrites, None if it doesn't.  
   This allows 'conservative' rewrite, which minimises the size of proof states.

   To speed things up, we have removed the property of rewrites that they 
   return information on variables, etc., present within a rewritten formula.
*)

(* rewinf is a quadruple of vars, uVIDs, badres, psig; 
 * vars is all names; uVIDs all VIDs from unknowns; 
 * badres all ResUnknown/Nonum resource numbers from enclosed collections;
 * psig is Some int -- the context contains an int which is incremented 
 * when the provisos change significantly (i.e., when they are rewritten or 
 * augmented - and perhaps when they are simplified, but we shall come to that).
 * The vars, uVIDs and badres lists are sorted and don't contain duplicates.
 *)

(* rawinf is the same as rewinf, but it doesn't have the same invariants -- 
 * essentially the lists are unsorted and may contain duplicates
 *)

type rawinf = term list * vid list * int list * int option

let nullrawinf = [], [], [], None

let mkrawinf raw = raw

let raw2rew_ (vars, uVIDs, badres, psig) =
  mkrewinf (sortunique earliervar vars, sortunique (<) uVIDs, sortunique (<) badres, psig)

(* these functions designed to be folded *)
let rawinfTerm n (t, stuff) =
  let rec f (t, (vars, uVIDs, badres, psig as z)) =
    match t with
    | Id _                  -> Some (t :: vars, uVIDs, badres, psig)
    | Unknown (_, u, _)     -> Some (t :: vars, u :: uVIDs, badres, psig)
    | Subst (_, r, _P, vts) -> let ff = foldterm f in
                               let rec fp ((v, t), z) = ff (ff z v) t in
                               Some (ff (nj_fold fp vts (vars, uVIDs, badres, Some n)) _P)
    | Collection (_, _, es) ->
        let g = function
                | Segvar (_, ms, t), z -> nj_fold (nj_foldterm f) (t :: ms) z
                | Element (_, ResUnknown i, t), z ->
                    foldterm f (vars, uVIDs, i :: badres, psig) t
                | Element (_, _, t), z -> foldterm f z t
        in
        Some (nj_fold g es z)
    | _                     -> None
  in
  foldterm f stuff t

let rec rawinfresnum (r, (vars, uVIDs, badres, psig as raw)) =
  match r with
  ResUnknown i -> vars, uVIDs, i :: badres, psig
  | _          -> raw

let rawinfSeq n (Seq (st, _Hs, _Gs), stuff) =
  let _RIT = rawinfTerm n in 
  _RIT (_Hs, _RIT (_Gs, stuff))

let rawinfProviso n (p, stuff) =
  let _RIT = rawinfTerm n in
  let _RRE ((r, t), stuff) = rawinfresnum (r, _RIT (t, stuff)) in
  match p with
  | FreshProviso (_, _, _, v)       -> _RIT (v, stuff)
  | NotinProviso (v, p)             -> _RIT (v, _RIT (p, stuff))
  | DistinctProviso vs              -> nj_fold _RIT vs stuff
  | NotoneofProviso (vs, pat, _C)   -> nj_fold _RIT vs (_RIT (_C, stuff))
  | UnifiesProviso (p1, p2)         -> _RIT (p1, _RIT (p2, stuff))
  | DischargeProviso (nt,sing,rts)  -> nj_fold _RRE rts stuff
  
let rawinfElements n (es, stuff) =
  let rec _RE (e, stuff) =
    match e with
    | Segvar (_, ops, v) -> rawinfTerm n (v, nj_fold (rawinfTerm n) ops stuff)
    | Element (_, r, t)  -> rawinfresnum (r, rawinfTerm n (t, stuff))
  in
  nj_fold _RE es stuff

let rew_worthwhile subst cxt ri =
 (subst && (match rewinf_psig ri, getprovisosig cxt with
            | Some si, ci -> si <> ci
            | _           -> false
           ) 
  || List.exists (bool_of_opt <.> (fun uVID -> (varmap cxt <@> uVID))) (rewinf_uVIDs ri)
 ) 
 || List.exists (bool_of_opt <.> (fun i -> (resmap cxt <@> i))) (rewinf_badres ri)

(* this is almost f &~ (_Some <.> yes), but types get in the way ... *)
(* do they? I think it's f x &~~ (_Some <.> yes) RB 14/09/20 *)
let rew_ f x yes =
  match f x with
  | Some x' -> Some (yes x')
  | _       -> None

(* this is _Some <.> anyway f *)
let rew_yes f t =
  match f t with
  | None -> Some t
  | some -> some

let rew_2 f x g y yes =
  (option_rewrite2 f g &~ (_Some <.> yes)) (x, y)

let rew_Pair _R = option_rewrite2 _R _R

(* there must be a better way ... *)
let rec rew_3 f x g y h z yes =
  (option_rewrite3 f g h &~ (_Some <.> yes)) (x, y, z)

let rew_binding outer inner (h, (bs, ss, us), env, pat) =
  rew_3 (option_rewritelist outer) bs 
        (option_rewritelist inner) ss
        (option_rewritelist outer) us
        (fun stuff -> registerBinding (stuff, env, pat))

let rec rew_Term subst cxt t =
  let rec _S t =
    match t with
    | Id (_, v, _)      -> None
    | Unknown (_, v, _) -> (match (varmap cxt <@> v) with
                            | Some t' -> rew_yes _S t'
                            | None -> None
                           )
    | App (h, f, a) -> rew_ (rew_Pair _S) (f, a) registerApp
    | Tup (h, sep, ts) ->
        rew_ (option_rewritelist _S) ts (fun ts' -> registerTup (sep, ts'))
    | Literal _ -> None
    | Fixapp (h, ss, ts) ->
        rew_ (option_rewritelist _S) ts
          (fun ts' -> registerFixapp (ss, ts'))
    | Binding binding -> rew_binding _S _S binding
    | Subst _Pm -> rew_Subst subst cxt _Pm
    | Collection (h, k, es) ->
        rew_ (rew_elements subst cxt) es
          (fun es' -> registerCollection (k, es'))
  in
  let res = _S t in
  if !rewritedebug then
  consolereport
    ["rew_Term "; string_of_bool subst; " cxt "; string_of_termarg t; " => ";
     string_of_option string_of_term res];
  res

and rew_substmap subst cxt vts =
option_rewritelist (rew_Pair (rew_Term subst cxt)) vts

and rew_Subst subst cxt =
fun (h, r, _P, m) ->
let simp = simplifySubst (facts (provisos cxt) cxt) in
match
  rew_2 (rew_Term subst cxt) _P (rew_substmap subst cxt) m
    (fun (_P, m) ->
       if subst then
         match simp m _P with
         | None -> registerSubst (r, _P, m)
         | Some t -> t
       else registerSubst (r, _P, m))
with
| None -> if subst then simp m _P else None
| some -> some

and rew_elements subst cxt es =
let _RT = rew_Term subst cxt in
let def (r, t) = rew_ _RT t (fun t -> [registerElement (r, t)]) in
let rec _RE =
function
| Segvar (_, [], (Unknown _ as v)) ->
    rew_ _RT v
      (function
       | Collection (_, _, es) -> es
       | _ -> raise (Catastrophe_ ["rew_elements 1"]))
| Segvar (_, ps, (Unknown _ as v)) as sv ->
    rew_ _RT v
      (function
       | Collection (_, _, []) -> []
       | Collection (_, _, es) ->
           (* modeifyelement ps <* es *)
           raise
             (Catastrophe_
                ["rew_elements 2 "; string_of_element sv; " ";
                 bracketed_string_of_list string_of_element "," es])
       | _ -> raise (Catastrophe_ ["rew_elements 3"]))
| Element (_, (ResUnknown i as r), t) ->
    (* This code, and the type of resmap, are designed to fix a space leak.
     * Provided that it is invariant that resource numbers map uniquely
     * to formulae in the tree (modulo rewriting), then it is safe to 
     * take a canonical version of any element.  
     * Without this, some replayed proofs generate enormous amounts of
     * space
     *)
    (match (resmap cxt <@> i) with
     | Some (r, t) -> rew_yes (rew_elements subst cxt) [registerElement (r, t)]
     | None        -> def (r, t)
    )
| Element (_, r, t) -> def (r, t)
| _                 -> None
in
match es with
[] -> None
| e :: es ->
  match _RE e, rew_elements subst cxt es with
  | Some es1, Some es2 -> Some (es1 @ es2)
  | None, Some es -> Some (e :: es)
  | Some es1, None -> Some (es1 @ es)
  | None, None -> None

and rew_resnum cxt r =
  match r with
  | ResUnknown i ->
      (match (resmap cxt <@> i) with
       | Some (r, _) -> rew_yes (rew_resnum cxt) r
       | None        -> None
      )
    | _              -> None

and rew_resnum_and_term subst cxt (r, t) = 
  let def () = rew_ (rew_Term subst cxt) t (fun t -> (r,t)) in
  match r with
  | ResUnknown i -> (match (resmap cxt <@> i) with
                    | Some (r, t) -> rew_resnum_and_term subst cxt (r, t)
                    | None        -> def ()
                   )
  | _            -> def ()
  
let rec rew_Seq subst cxt =
  fun (Seq (st, _H, _G)) ->
  rew_2 (rew_Term subst cxt) _H (rew_Term subst cxt) _G
    (fun (_H', _G') -> Seq (st, _H', _G'))

let rec rew_Proviso subst cxt p =
  let _RT = rew_Term subst cxt in
  match p with
  | FreshProviso (h, g, r, v)       -> rew_ _RT v (fun v -> FreshProviso (h, g, r, v))
  | NotinProviso vp                 -> rew_ (rew_Pair _RT) vp _NotinProviso
  | DistinctProviso vs              -> rew_ (option_rewritelist _RT) vs _DistinctProviso
  | NotoneofProviso (vs, pat, _C)   -> rew_3 (option_rewritelist _RT) vs _RT pat _RT _C _NotoneofProviso
  | UnifiesProviso pp               -> rew_ (rew_Pair _RT) pp _UnifiesProviso
  | DischargeProviso (nt,sing,rts)  -> rew_ (option_rewritelist (rew_resnum_and_term subst cxt)) rts (_DischargeProviso nt sing)
  
let rec rew_update a1 a2 a3 a4 =
  match a1, a2, a3, a4 with
| f, g, Some ri, cxt ->
    begin match rewinf_psig ri with
    | Some n ->
        let n' = getprovisosig cxt in
        if n = n' then None else Some (f (rewinf_setpsig ri (Some n')))
    | None -> None
    end
  | f, g, None, cxt -> g ()

let rec rew_cxt cxt =
  (* there is no point rewriting the substitutions inside the provisos
  * until we have replaced the unknowns.  
  * That fact is the whole reason for the 'subst' argument in the rew_
  * functions.
  *)
  let rec needsit subst cxt =
    function Some inf -> rew_worthwhile subst cxt inf
    |        None     -> true
  in
  let rec doprovisos subst cxt =
    let (ps, pinf) = getprovisos cxt in
    if needsit subst cxt pinf then
      let rec newrewinf n ps =
        Some (raw2rew_ (nj_fold (rawinfProviso n) ((provisoactual <* ps)) nullrawinf))
      in
      let rec yes nextcxt ps =
        Some (setprovisos nextcxt (ps, newrewinf (getprovisosig cxt) ps))
      in
      let rec updatesig () =
        let rec f pinf' = setprovisos cxt (ps, Some pinf') in
        let rec g () = yes cxt ps in (* doesn't change ps, so doesn't cause incprovisosig *)
         rew_update f g pinf cxt
      in
      let rec rew_visproviso subst cxt vp =
        rew_ (rew_Proviso subst cxt <.> provisoactual) vp
          (provisoresetactual vp)
      in
      match option_rewritelist (rew_visproviso subst cxt) ps with
      | Some ps -> yes (incprovisosig cxt) ps
      | None -> updatesig ()
    else None
  in
  (* end doprovisos *)
         
  let rec doexterior subst cxt =
    match getexterior cxt with
    | Exterior ((ss, s), inf, fvinf) ->
        if needsit subst cxt inf then
          let rec yes (ss, s) =
            let raw =
              nj_fold (rawinfSeq (getprovisosig cxt)) (s :: ss) nullrawinf
            in
            let inf = raw2rew_ raw in
            let fvinf =
              match rewinf_vars inf, rewinf_uVIDs inf with
              | avs, [] ->
                  let (Seq (_, hs, cs)) = s in
                  let hbindings = varbindings hs in
                  let cbindings = varbindings cs in
                  let rec sv1 (s, stuff) =
                    bmerge (seqvars varbindings bmerge s) stuff
                  in
                  let stuff = nj_fold sv1 ss (bmerge hbindings cbindings) in
                  let ps = optionfilter
                             ((function NotinProviso p -> Some p
                               | _                     -> None) <.> provisoactual)
                             (provisos cxt)
                  in
                  let (fvs, m)   = freevarsfrombindings stuff ps in
                  let (bhfvs, _) = freevarsfrombindings hbindings ps in
                  let (bcfvs, _) = freevarsfrombindings cbindings ps in
                  Some {avs=avs; fvs=fvs; vmap=mkmap m; bhfvs=bhfvs; bcfvs=bcfvs}
              | _ -> None
            in
            Some (setexterior (incprovisosig cxt) (Exterior ((ss, s), Some inf, fvinf)))
          in
          let rec updatesig () =
            let rec f inf' =
              setexterior cxt (Exterior ((ss, s), Some inf', fvinf))
            in
            let rec g _ = yes (ss, s) in rew_update f g inf cxt
          in
          match
            rew_2 (option_rewritelist (rew_Seq subst cxt)) ss
              (rew_Seq subst cxt) s idf
          with
          | Some r -> yes r
          | None -> updatesig ()
        else None
    | _ -> None
  in
  (* end doexterior *)
     
  let rec doit subst cxt =
    let rec doit2 cxt =
      match doexterior subst cxt with
      | Some cxt -> rew_yes (doit true) cxt
      | None -> if subst then None else doit true cxt
    in
    match doprovisos subst cxt with
    | Some cxt -> rew_yes (if subst then doit true else doit2) cxt
    | None -> doit2 cxt
  in
  let r = doit false cxt in
  if !rewritedebug then
    consolereport ["rew_cxt "; string_of_cxt cxt; " => "; string_of_option string_of_cxt r];
  r
  (*end rew_cxt*)
  
let rawinfTerm cxt = rawinfTerm (getprovisosig cxt)

let rawinfSeq cxt = rawinfSeq (getprovisosig cxt)

let rawinfProviso cxt = rawinfProviso (getprovisosig cxt)

let rawinfElements cxt = rawinfElements (getprovisosig cxt)

let rec rewinfCxt cxt =
match getprovisos cxt, getexterior cxt with
(_, Some pinf), Exterior (_, Some binf, _) ->
  rewinf_merge (pinf, binf)
| (_, Some pinf), _ -> pinf
| _, Exterior (_, Some binf, _) -> binf
| _ -> nullrewinf
