Conditions.ml

(**************************************************************************)
(*                                                                        *)
(*  This file is part of WP plug-in of Frama-C.                           *)
(*                                                                        *)
(*  Copyright (C) 2007-2019                                               *)
(*    CEA (Commissariat a l'energie atomique et aux energies              *)
(*         alternatives)                                                  *)
(*                                                                        *)
(*  you can redistribute it and/or modify it under the terms of the GNU   *)
(*  Lesser General Public License as published by the Free Software       *)
(*  Foundation, version 2.1.                                              *)
(*                                                                        *)
(*  It 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 Lesser General Public License for more details.                   *)
(*                                                                        *)
(*  See the GNU Lesser General Public License version 2.1                 *)
(*  for more details (enclosed in the file licenses/LGPLv2.1).            *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Weakest Pre Accumulator                                            --- *)
(* -------------------------------------------------------------------------- *)

open Qed.Logic
open Cil_types
open Lang
open Lang.F

let dkey_pruning = Wp_parameters.register_category "pruning"

(* -------------------------------------------------------------------------- *)
(* --- Category                                                           --- *)
(* -------------------------------------------------------------------------- *)

type category =
  | EMPTY  (** Empty Sequence, equivalent to True, but with State. *)
  | TRUE   (** Logically equivalent to True *)
  | FALSE  (** Logically equivalent to False *)
  | MAYBE  (** Any Hypothesis *)

let c_and c1 c2 =
  match c1 , c2 with
  | FALSE , _ | _ , FALSE -> FALSE
  | MAYBE , _ | _ , MAYBE -> MAYBE
  | TRUE , _  | _ , TRUE -> TRUE
  | EMPTY , EMPTY -> EMPTY

let c_or c1 c2 =
  match c1 , c2 with
  | FALSE , FALSE -> FALSE
  | EMPTY , EMPTY -> EMPTY
  | TRUE , TRUE -> TRUE
  | _ -> MAYBE

let rec cfold_and a f = function
  | [] -> a | e::es -> cfold_and (c_and a (f e)) f es

let rec cfold_or a f = function
  | [] -> a | e::es -> cfold_or (c_or a (f e)) f es

let c_conj f es = cfold_and EMPTY f es
let c_disj f = function [] -> FALSE | e::es -> cfold_or (f e) f es

(* -------------------------------------------------------------------------- *)
(* --- Datatypes                                                          --- *)
(* -------------------------------------------------------------------------- *)

type step = {
  mutable id : int ; (* step identifier *)
  size : int ; (* number of conditions *)
  vars : Vars.t ;
  stmt : stmt option ;
  descr : string option ;
  deps : Property.t list ;
  warn : Warning.Set.t ;
  condition : condition ;
}
and sequence = {
  seq_size : int ;
  seq_vars : Vars.t ;
  seq_core : Pset.t ;
  seq_catg : category ;
  seq_list : step list ;
}
and condition =
  | Type of pred
  | Have of pred
  | When of pred
  | Core of pred
  | Init of pred
  | Branch of pred * sequence * sequence
  | Either of sequence list
  | State of Mstate.state

(* -------------------------------------------------------------------------- *)
(* --- Variable Utilities                                                 --- *)
(* -------------------------------------------------------------------------- *)

let vars_seqs w = List.fold_left (fun xs s -> Vars.union xs s.seq_vars) Vars.empty w
let vars_list s = List.fold_left (fun xs s -> Vars.union xs s.vars) Vars.empty s
let size_list s = List.fold_left (fun n s -> n + s.size) 0 s
let vars_cond = function
  | Type q | When q | Have q | Core q | Init q -> F.varsp q
  | Branch(p,sa,sb) -> Vars.union (F.varsp p) (Vars.union sa.seq_vars sb.seq_vars)
  | Either cases -> vars_seqs cases
  | State _ -> Vars.empty
let size_cond = function
  | Type _ | When _ | Have _ | Core _ | Init _ | State _ -> 1
  | Branch(_,sa,sb) -> 1 + sa.seq_size + sb.seq_size
  | Either cases -> List.fold_left (fun n s -> n + s.seq_size) 1 cases
let vars_hyp hs = hs.seq_vars
let vars_seq (hs,g) = Vars.union (F.varsp g) hs.seq_vars

(* -------------------------------------------------------------------------- *)
(* --- Core Utilities                                                     --- *)
(* -------------------------------------------------------------------------- *)

let is_core p = match F.e_expr p with
  (*  | Qed.Logic.Eq (a,b) -> is_def a && is_def b *)
  | Qed.Logic.Eq _ -> true
  | _ -> false

let rec add_core s p = match F.p_expr p with
  | Qed.Logic.And ps -> List.fold_left add_core Pset.empty ps
  | _ -> if is_core p then Pset.add p s else s

let core_cond = function
  | Type _ | State _ -> Pset.empty
  | Have p | When p | Core p | Init p -> add_core Pset.empty p
  | Branch(_,sa,sb) -> Pset.inter sa.seq_core sb.seq_core
  | Either [] -> Pset.empty
  | Either (c::cs) ->
      List.fold_left (fun w s -> Pset.inter w s.seq_core) c.seq_core cs

let add_core_step ps s = Pset.union ps (core_cond s.condition)

let core_list s = List.fold_left add_core_step Pset.empty s

(* -------------------------------------------------------------------------- *)
(* --- Category                                                           --- *)
(* -------------------------------------------------------------------------- *)

let catg_seq s = s.seq_catg
let catg_cond = function
  | State _ -> TRUE
  | Have p | Type p | When p | Core p | Init p ->
      begin
        match F.is_ptrue p with
        | No -> FALSE
        | Maybe -> MAYBE
        | Yes -> EMPTY
      end
  | Either cs -> c_disj catg_seq cs
  | Branch(_,a,b) -> c_or a.seq_catg b.seq_catg
let catg_step s = catg_cond s.condition
let catg_list l = c_conj catg_step l

(* -------------------------------------------------------------------------- *)
(* --- Sequence Constructor                                               --- *)
(* -------------------------------------------------------------------------- *)

let sequence l = {
  seq_size = size_list l ;
  seq_vars = vars_list l ;
  seq_core = core_list l ;
  seq_catg = catg_list l ;
  seq_list = l ;
}

(* -------------------------------------------------------------------------- *)
(* --- Sequence Comparator                                                --- *)
(* -------------------------------------------------------------------------- *)

let rec equal_cond ca cb =
  match ca,cb with
  | State _ , State _ -> true
  | Type p , Type q
  | Have p , Have q
  | When p , When q
  | Core p , Core q
  | Init p , Init q
    -> p == q
  | Branch(p,a,b) , Branch(q,a',b') ->
      p == q && equal_seq a a' && equal_seq b b'
  | Either u, Either v ->
      Qed.Hcons.equal_list equal_seq u v
  | State _ , _ | _ , State _
  | Type _ , _ | _ , Type _
  | Have _ , _ | _ , Have _
  | When _ , _ | _ , When _
  | Core _ , _ | _ , Core _
  | Init _ , _ | _ , Init _
  | Branch _ , _ | _ , Branch _
    -> false

and equal_step a b =
  equal_cond a.condition b.condition

and equal_list sa sb =
  Qed.Hcons.equal_list equal_step sa sb

and equal_seq sa sb =
  equal_list sa.seq_list sb.seq_list

(* -------------------------------------------------------------------------- *)
(* --- Core Inference                                                     --- *)
(* -------------------------------------------------------------------------- *)

module Core =
struct

  let rec fpred core p = match F.p_expr p with
    | Qed.Logic.And ps -> F.p_conj (List.map (fpred core) ps)
    | _ -> if Pset.mem p core then p_true else p

  let fcond core = function
    | Core p -> Core (fpred core p)
    | Have p -> Have (fpred core p)
    | When p -> When (fpred core p)
    | Init p -> Init (fpred core p)
    | (Type _ | Branch _ | Either _ | State _) as cond -> cond

  let fstep core step =
    let condition = fcond core step.condition in
    let vars = vars_cond condition in
    { step with condition ; vars }

  let factorize a b =
    if Wp_parameters.Core.get () then
      let core = Pset.inter a.seq_core b.seq_core in
      if Pset.is_empty core then None else
        let ca = List.map (fstep core) a.seq_list in
        let cb = List.map (fstep core) b.seq_list in
        Some (F.p_conj (Pset.elements core) , sequence ca , sequence cb)
    else None

end

(* -------------------------------------------------------------------------- *)
(* --- Bundle (non-simplified conditions)                                 --- *)
(* -------------------------------------------------------------------------- *)

module Bundle :
sig
  type t
  val empty : t
  val vars : t -> Vars.t
  val is_empty : t -> bool
  val category : t -> category
  val add : step -> t -> t
  val factorize : t -> t -> t * t * t
  val big_inter : t list -> t
  val diff : t -> t -> t
  val head : t -> Mstate.state option
  val freeze: ?join:step -> t -> sequence
  val map : (condition -> 'a) -> t -> 'a list
end =
struct
  module SEQ = Qed.Listset.Make
      (struct
        type t = int * step
        let equal (k1,_) (k2,_) = k1 = k2
        let compare (k1,s1) (k2,s2) =
          let rank = function
            | Type _ -> 0
            | When _ -> 1
            | _ -> 2
          in
          let r = rank s1.condition - rank s2.condition in
          if r = 0 then Transitioning.Stdlib.compare k2 k1 else r
      end)

  type t = Vars.t * SEQ.t

  let vars = fst
  let cid = ref 0
  let fresh () = incr cid ; assert (!cid > 0) ; !cid

  let add s (xs,t) = Vars.union xs s.vars , SEQ.add (fresh (),s) t

  let empty = Vars.empty , []
  let is_empty = function (_,[]) -> true | _ -> false

  let head = function _,(_,{ condition = State s }) :: _ -> Some s | _ -> None

  let build seq =
    let xs = List.fold_left
        (fun xs (_,s) -> Vars.union xs s.vars) Vars.empty seq in
    xs , seq

  let factorize (_,a) (_,b) =
    let l,m,r = SEQ.factorize a b in
    build l , build m , build r

  let big_inter cs = build (SEQ.big_inter (List.map snd cs))
  let diff (_,a) (_,b) = build (SEQ.diff a b)
  let freeze ?join (seq_vars,bundle) =
    let seq = List.map snd bundle in
    let seq_list = match join with None -> seq | Some s -> seq @ [s] in
    let seq_size = size_list seq in
    let seq_catg = catg_list seq in
    { seq_size ; seq_vars ; seq_core = Pset.empty ; seq_catg ; seq_list }
  let map f b = List.map (fun (_,s) -> f s.condition) (snd b)
  let category (_,bundle) = c_conj (fun (_,s) -> catg_step s) bundle
end

(* -------------------------------------------------------------------------- *)
(* --- Hypotheses                                                         --- *)
(* -------------------------------------------------------------------------- *)

type bundle = Bundle.t
type sequent = sequence * F.pred

let pretty = ref (fun _fmt _seq -> ())

let is_true = function { seq_catg = TRUE | EMPTY } -> true | _ -> false
let is_empty = function { seq_catg = EMPTY } -> true | _ -> false

let is_absurd_h h = match h.condition with
  | (Core p | When p | Have p) -> p == F.p_false
  | _ -> false

let is_trivial_h h = match h.condition with
  | State _ -> false
  | (Type p | Core p | When p | Have p | Init p) -> p == F.p_true
  | Branch(_,a,b) -> is_true a && is_true b
  | Either w -> List.for_all is_true w

let is_trivial_hs_p hs p = p == F.p_true || List.exists is_absurd_h hs
let is_trivial_hsp (hs,p) = is_trivial_hs_p hs p
let is_trivial (s:sequent) = is_trivial_hs_p (fst s).seq_list (snd s)

(* -------------------------------------------------------------------------- *)
(* --- Extraction                                                         --- *)
(* -------------------------------------------------------------------------- *)

let rec pred_cond = function
  | State _ -> F.p_true
  | When p | Type p | Have p | Core p | Init p -> p
  | Branch(p,a,b) -> F.p_if p (pred_seq a) (pred_seq b)
  | Either cases -> F.p_any pred_seq cases
and pred_seq seq = F.p_all (fun s -> pred_cond s.condition) seq.seq_list
let extract bundle = Bundle.map pred_cond bundle
let bundle = Bundle.freeze ?join:None

let intersect p bundle = Vars.intersect (F.varsp p) (Bundle.vars bundle)
let occurs x bundle = Vars.mem x (Bundle.vars bundle)

(* -------------------------------------------------------------------------- *)
(* --- Constructors                                                       --- *)
(* -------------------------------------------------------------------------- *)

let nil = Bundle.empty
let noid = (-1)

let step ?descr ?stmt ?(deps=[]) ?(warn=Warning.Set.empty) cond =
  {
    id = noid ;
    size = size_cond cond ;
    vars = vars_cond cond ;
    stmt = stmt ;
    descr = descr ;
    warn = warn ;
    deps = deps ;
    condition = cond ;
  }

let update_cond ?descr ?(deps=[]) ?(warn=Warning.Set.empty) h c =
  let descr = match h.descr, descr  with
    | None, _ -> descr ;
    | Some _, None -> h.descr ;
    | Some decr1, Some descr2 -> Some (decr1 ^ "-" ^ descr2)
  in {
    id = noid ;
    condition = c ;
    stmt = h.stmt ;
    size = size_cond c ;
    vars = vars_cond c ;
    descr = descr ;
    deps = deps@h.deps ;
    warn = Warning.Set.union h.warn warn ;
  }

type 'a disjunction = D_TRUE | D_FALSE | D_EITHER of 'a list

let disjunction phi es =
  let positives = ref false in (* TRUE or EMPTY items *)
  let remains = List.filter
      (fun e ->
         match phi e with
         | TRUE | EMPTY -> positives := true ; false
         | MAYBE -> true
         | FALSE -> false
      ) es in
  match remains with
  | [] -> if !positives then D_TRUE else D_FALSE
  | cs -> D_EITHER cs

(* -------------------------------------------------------------------------- *)
(* --- Prenex-Form Introduction                                           --- *)
(* -------------------------------------------------------------------------- *)

let prenex_intro p =
  try
    let open Qed.Logic in
    (* invariant: xs <> []; result <-> forall xs, hs -> p *)
    let rec walk hs xs p =
      match F.p_expr p with
      | Imply(h,p) -> walk (h::hs) xs p
      | Bind(Forall,_,_) -> bind hs xs p
      | _ ->
          if hs = [] then raise Exit ;
          F.p_forall (List.rev xs) (F.p_hyps (List.concat hs) p)
    (* invariant: result <-> forall hs xs (\tau.bind) *)
    and bind hs xs p =
      let pool = Lang.get_pool () in
      let ctx,t = e_open ~pool ~forall:true
          ~exists:false ~lambda:false (e_prop p) in
      let xs = List.fold_left (fun xs (_,x) -> x::xs) xs (List.rev ctx) in
      walk hs xs (F.p_bool t)
    (* invariant: result <-> p *)
    and crawl p =
      match F.p_expr p with
      | Imply(h,p) -> F.p_hyps h (crawl p)
      | Bind(Forall,_,_) -> bind [] [] p
      | _ -> raise Exit
    in crawl p
  with Exit -> p

(* -------------------------------------------------------------------------- *)
(* --- Existential Introduction                                           --- *)
(* -------------------------------------------------------------------------- *)

let rec exist_intro p =
  let open Qed.Logic in
  match F.p_expr p with
  | And ps -> F.p_all exist_intro ps
  | Bind(Exists,_,_) ->
      let pool = Lang.get_pool () in
      let _,t = e_open ~pool ~exists:true
          ~forall:false ~lambda:false (e_prop p) in
      exist_intro (F.p_bool t)
  | _ ->
      if Wp_parameters.Prenex.get ()
      then prenex_intro p
      else p

let rec exist_intros = function
  | [] -> []
  | p::hs -> begin
      let open Qed.Logic in
      match F.p_expr p with
      | And ps -> exist_intros (ps@hs)
      | Bind(Exists,_,_) ->
          let pool = Lang.get_pool () in
          let _,t = F.QED.e_open ~pool ~exists:true
              ~forall:false ~lambda:false (e_prop p) in
          exist_intros ((F.p_bool t)::hs)
      | _ -> p::(exist_intros hs)
    end

(* -------------------------------------------------------------------------- *)
(* --- Universal Introduction                                            --- *)
(* -------------------------------------------------------------------------- *)

let rec forall_intro p =
  let open Qed.Logic in
  match F.p_expr p with
  | Bind(Forall,_,_) ->
      let pool = Lang.get_pool () in
      let _,t = F.QED.e_open ~pool ~forall:true
          ~exists:false ~lambda:false (e_prop p) in
      forall_intro (F.p_bool t)
  | Imply(hs,p) ->
      let hs = exist_intros hs in
      let hp,p = forall_intro p in
      hs @ hp , p
  | Or qs -> (* analogy with Imply *)
      let hps,ps = List.fold_left (fun (hs,ps) q ->
          let hp,p = forall_intro q in (* q <==> (hp ==> p) *)
          (hp @ hs), (p::ps)) ([],[]) qs
      in (* ORs qs  <==> ORs (hps ==> ps)
                    <==> ((ANDs hps) ==> ORs ps) *)
      hps, (p_disj ps)
  | _ -> [] , p

(* -------------------------------------------------------------------------- *)
(* --- Constructors                                                       --- *)
(* -------------------------------------------------------------------------- *)

type 'a attributed =
  ( ?descr:string ->
    ?stmt:stmt ->
    ?deps:Property.t list ->
    ?warn:Warning.Set.t ->
    'a )

let domain ps hs =
  if ps = [] then hs else
    Bundle.add (step (Type (p_conj ps))) hs

let intros ps hs =
  if ps = [] then hs else
    let p = F.p_all exist_intro ps in
    Bundle.add (step ~descr:"Goal" (When p)) hs

let state ?descr ?stmt state hs =
  let cond = State state in
  let s = step ?descr ?stmt cond in
  Bundle.add s hs

let assume ?descr ?stmt ?deps ?warn ?(init=false) p hs =
  match F.is_ptrue p with
  | Yes -> hs
  | No ->
      let cond = if init then Init p else Have p in
      let s = step ?descr ?stmt ?deps ?warn cond in
      Bundle.add s Bundle.empty
  | Maybe ->
      begin
        match Bundle.category hs with
        | MAYBE | TRUE | EMPTY ->
            let p = exist_intro p in
            let cond = if init then Init p else Have p in
            let s = step ?descr ?stmt ?deps ?warn cond in
            Bundle.add s hs
        | FALSE -> hs
      end

let join = function None -> None | Some s -> Some (step (State s))

let branch ?descr ?stmt ?deps ?warn p ha hb =
  match F.is_ptrue p with
  | Yes -> ha
  | No -> hb
  | Maybe ->
      match Bundle.category ha , Bundle.category hb with
      | TRUE , TRUE -> Bundle.empty
      | _ , FALSE -> assume ?descr ?stmt ?deps ?warn p ha
      | FALSE , _ -> assume ?descr ?stmt ?deps ?warn (p_not p) hb
      | _ ->
          let ha,hs,hb = Bundle.factorize ha hb in
          if Bundle.is_empty ha && Bundle.is_empty hb then hs else
            let join = join (Bundle.head hs) in
            let a = Bundle.freeze ?join ha in
            let b = Bundle.freeze ?join hb in
            let s = step ?descr ?stmt ?deps ?warn (Branch(p,a,b)) in
            Bundle.add s hs

let either ?descr ?stmt ?deps ?warn cases =
  match disjunction Bundle.category cases with
  | D_TRUE -> Bundle.empty
  | D_FALSE ->
      let s = step ?descr ?stmt ?deps ?warn (Have p_false) in
      Bundle.add s Bundle.empty
  | D_EITHER cases ->
      let trunk = Bundle.big_inter cases in
      let cases = List.map (fun case -> Bundle.diff case trunk) cases in
      match disjunction Bundle.category cases with
      | D_TRUE -> trunk
      | D_FALSE ->
          let s = step ?descr ?stmt ?deps ?warn (Have p_false) in
          Bundle.add s Bundle.empty
      | D_EITHER cases ->
          let cases = List.map Bundle.freeze cases in
          let s = step ?descr ?stmt ?deps ?warn (Either cases) in
          Bundle.add s trunk

let merge cases = either ~descr:"Merge" cases

(* -------------------------------------------------------------------------- *)
(* --- Flattening                                                         --- *)
(* -------------------------------------------------------------------------- *)

let rec flat_catg = function
  | [] -> EMPTY
  | s::cs ->
      match catg_step s with
      | EMPTY -> flat_catg cs
      | r -> r

let flat_cons step tail =
  match flat_catg tail with
  | FALSE -> tail
  | _ -> step :: tail

let flat_concat head tail =
  match flat_catg head with
  | EMPTY -> tail
  | FALSE -> head
  | MAYBE|TRUE ->
      match flat_catg tail with
      | EMPTY -> head
      | FALSE -> tail
      | MAYBE|TRUE -> head @ tail

let core_residual step core = {
  id = noid ;
  size = 1 ;
  vars = F.varsp core ;
  condition = Core core ;
  descr = None ;
  warn = Warning.Set.empty ;
  deps = [] ;
  stmt = step.stmt ;
}

let core_branch step p a b =
  let condition =
    match a.seq_catg , b.seq_catg with
    | (TRUE | EMPTY) , (TRUE|EMPTY) -> Have p_true
    | _ -> Branch(p,a,b)
  in update_cond step condition

let rec flatten_sequence m = function
  | [] -> []
  | step :: seq ->
      match step.condition with
      | State _ -> flat_cons step (flatten_sequence m seq)
      | Have p | Type p | When p | Core p | Init p ->
          begin
            match F.is_ptrue p with
            | Yes -> m := true ; flatten_sequence m seq
            | No -> (* FALSE context *) if seq <> [] then m := true ; [step]
            | Maybe -> flat_cons step (flatten_sequence m seq)
          end
      | Branch(p,a,b) ->
          begin
            match F.is_ptrue p with
            | Yes -> m := true ; flat_concat a.seq_list (flatten_sequence m seq)
            | No -> m := true ; flat_concat b.seq_list (flatten_sequence m seq)
            | Maybe ->
                let sa = a.seq_list in
                let sb = b.seq_list in
                match a.seq_catg , b.seq_catg with
                | (TRUE|EMPTY) , (TRUE|EMPTY) ->
                    m := true ; flatten_sequence m seq
                | _ , FALSE ->
                    m := true ;
                    let step = update_cond step (Have p) in
                    step :: sa @ flatten_sequence m seq
                | FALSE , _ ->
                    m := true ;
                    let step = update_cond step (Have (p_not p)) in
                    step :: sb @ flatten_sequence m seq
                | _ ->
                    begin
                      match Core.factorize a b with
                      | None -> step :: flatten_sequence m seq
                      | Some( core , a , b ) ->
                          m := true ;
                          let score = core_residual step core in
                          let scond = core_branch step p a b in
                          score :: scond :: flatten_sequence m seq
                    end
          end
      | Either [] -> (* FALSE context *) if seq <> [] then m := true ; [step]
      | Either cases ->
          match disjunction catg_seq cases with
          | D_TRUE -> m := true ; flatten_sequence m seq
          | D_FALSE -> m := true ; [ update_cond step (Have p_false) ]
          | D_EITHER [hc] ->
              m := true ; flat_concat hc.seq_list (flatten_sequence m seq)
          | D_EITHER cs ->
              let step = update_cond step (Either cs) in
              flat_cons step (flatten_sequence m seq)

(* -------------------------------------------------------------------------- *)
(* --- Mapping                                                            --- *)
(* -------------------------------------------------------------------------- *)

let lift f e = F.e_prop (f (F.p_bool e))

let rec map_condition f = function
  | State s -> State (Mstate.apply (lift f) s)
  | Have p -> Have (f p)
  | Type p -> Type (f p)
  | When p -> When (f p)
  | Core p -> Core (f p)
  | Init p -> Init (f p)
  | Branch(p,a,b) -> Branch(f p,map_sequence f a,map_sequence f b)
  | Either cs -> Either (List.map (map_sequence f) cs)

and map_step f h = update_cond h (map_condition f h.condition)

and map_steplist f = function
  | [] -> []
  | h::hs ->
      let h = map_step f h in
      let hs = map_steplist f hs in
      if is_trivial_h h then hs else h :: hs

and map_sequence f s =
  sequence (map_steplist f s.seq_list)

and map_sequent f (hs,g) = map_sequence f hs , f g

(* -------------------------------------------------------------------------- *)
(* --- Ground Simplifier                                                  --- *)
(* -------------------------------------------------------------------------- *)

module Ground = Letify.Ground

let rec ground_flow ~fwd env h =
  match h.condition with
  | State s ->
      let s = Mstate.apply (Ground.e_apply env) s in
      update_cond h (State s)
  | Type _ | Have _ | When _ | Core _ | Init _ ->
      let phi = if fwd then Ground.forward else Ground.backward in
      let cond = map_condition (phi env) h.condition in
      update_cond h cond
  | Branch(p,a,b) ->
      let p,wa,wb = Ground.branch env p in
      let a = ground_flowseq ~fwd wa a in
      let b = ground_flowseq ~fwd wb b in
      update_cond h (Branch(p,a,b))
  | Either ws ->
      let ws = List.map
          (fun w -> ground_flowseq ~fwd (Ground.copy env) w) ws in
      update_cond h (Either ws)

and ground_flowseq ~fwd env hs =
  sequence (ground_flowlist ~fwd env hs.seq_list)

and ground_flowlist ~fwd env hs =
  if fwd
  then ground_flowdir ~fwd env hs
  else List.rev (ground_flowdir ~fwd env (List.rev hs))

and ground_flowdir ~fwd env = function
  | [] -> []
  | h::hs ->
      let h = ground_flow ~fwd env h in
      let hs = ground_flowdir ~fwd env hs in
      if is_trivial_h h then hs else h :: hs

let ground (hs,g) =
  let hs = ground_flowlist ~fwd:true (Ground.top ()) hs in
  let hs = ground_flowlist ~fwd:false (Ground.top ()) hs in
  let env = Ground.top () in
  let hs = ground_flowlist ~fwd:true env hs in
  hs , Ground.p_apply env g

(* -------------------------------------------------------------------------- *)
(* --- Letify                                                             --- *)
(* -------------------------------------------------------------------------- *)

module Sigma = Letify.Sigma
module Defs = Letify.Defs

let used_of_dseq ds =
  Array.fold_left (fun ys (_,step) -> Vars.union ys step.vars) Vars.empty ds

let bind_dseq target (di,_) sigma =
  Letify.bind (Letify.bind sigma di target) di (Defs.domain di)

let locals sigma ~target ~required ?(step=Vars.empty) k dseq =
  (* returns ( target , export ) *)
  let t = ref target in
  let e = ref (Vars.union required step) in
  Array.iteri
    (fun i (_,step) ->
       if i > k then t := Vars.union !t step.vars ;
       if i <> k then e := Vars.union !e step.vars ;
    ) dseq ;
  Vars.diff !t (Sigma.domain sigma) , !e

let dseq_of_step sigma step =
  let defs =
    match step.condition with
    | Init p | Have p | When p | Core p -> Defs.extract (Sigma.p_apply sigma p)
    | Type _ | Branch _ | Either _ | State _ -> Defs.empty
  in defs , step

let letify_assume sref (_,step) =
  let current = !sref in
  begin
    match step.condition with
    | Type _ | Branch _ | Either _ | State _ -> ()
    | Init p | Have p | When p | Core p ->
        if Wp_parameters.Simpl.get () then
          sref := Sigma.assume current p
  end ; current

[@@@ warning "-32"]
let rec letify_type sigma used p = match F.p_expr p with
  | And ps -> p_all (letify_type sigma used) ps
  | _ ->
      let p = Sigma.p_apply sigma p in
      if Vars.intersect used (F.varsp p) then p else F.p_true
[@@@ warning "+32"]

let rec letify_seq sigma0 ~target ~export (seq : step list) =
  let dseq = Array.map (dseq_of_step sigma0) (Array.of_list seq) in
  let sigma1 = Array.fold_right (bind_dseq target) dseq sigma0 in
  let sref = ref sigma1 in (* with definitions *)
  let dsigma = Array.map (letify_assume sref) dseq in
  let sigma2 = !sref in (* with assumptions *)
  let outside = Vars.union export target in
  let inside = used_of_dseq dseq in
  let used = Vars.diff (Vars.union outside inside) (Sigma.domain sigma2) in
  let required = Vars.union outside (Sigma.codomain sigma2) in
  let sequence =
    Array.mapi (letify_step dseq dsigma ~used ~required ~target) dseq in
  let modified = ref (not (Sigma.equal sigma0 sigma1)) in
(*
  let sequence =
    if Wp_parameters.Ground.get () then fst (ground_hrp sequence)
    else sequence in
*)
  let sequence = flatten_sequence modified (Array.to_list sequence) in
  !modified , sigma1 , sigma2 , sequence

and letify_step dseq dsigma ~required ~target ~used i (d,s) =
  let sigma = dsigma.(i) in
  let cond = match s.condition with
    | State s -> State (Mstate.apply (Sigma.e_apply sigma) s)
    | Init p ->
        let p = Sigma.p_apply sigma p in
        let ps = Letify.add_definitions sigma d required [p] in
        Init (p_conj ps)
    | Have p ->
        let p = Sigma.p_apply sigma p in
        let ps = Letify.add_definitions sigma d required [p] in
        Have (p_conj ps)
    | Core p ->
        let p = Sigma.p_apply sigma p in
        let ps = Letify.add_definitions sigma d required [p] in
        Core (p_conj ps)
    | When p ->
        let p = Sigma.p_apply sigma p in
        let ps = Letify.add_definitions sigma d required [p] in
        When (p_conj ps)
    | Type p ->
        Type (letify_type sigma used p)
    | Branch(p,a,b) ->
        let p = Sigma.p_apply sigma p in
        let step = F.varsp p in
        let (target,export) = locals sigma ~target ~required ~step i dseq in
        let sa = Sigma.assume sigma p in
        let sb = Sigma.assume sigma (p_not p) in
        let a = letify_case sa ~target ~export a in
        let b = letify_case sb ~target ~export b in
        Branch(p,a,b)
    | Either cases ->
        let (target,export) = locals sigma ~target ~required i dseq in
        Either (List.map (letify_case sigma ~target ~export) cases)
  in update_cond s cond

and letify_case sigma ~target ~export seq =
  let (_,_,_,s) = letify_seq sigma ~target ~export seq.seq_list
  in sequence s

(* -------------------------------------------------------------------------- *)
(* --- External Simplifier                                                --- *)
(* -------------------------------------------------------------------------- *)

let simplify_exp solvers e =
  List.fold_left (fun e s -> s#simplify_exp e) e solvers
let simplify_goal solvers p =
  List.fold_left (fun p s -> s#simplify_goal p) p solvers
let simplify_hyp solvers p =
  List.fold_left (fun p s -> s#simplify_hyp p) p solvers
let simplify_branch solvers p =
  List.fold_left (fun p s -> s#simplify_branch p) p solvers

let apply_hyp modified solvers h =
  let simple p =
    let p' = simplify_hyp solvers p in
    if not (Lang.F.eqp p p') then modified := true;
    List.iter (fun s -> s#assume p') solvers; p'
  in
  match h.condition with
  | State s -> update_cond h (State (Mstate.apply (simplify_exp solvers) s))
  | Init p -> update_cond h (Init (simple p))
  | Type p -> update_cond h (Type (simple p))
  | Have p -> update_cond h (Have (simple p))
  | When p -> update_cond h (When (simple p))
  | Core p -> update_cond h (Core (simple p))
  | Branch(p,_,_) -> List.iter (fun s -> s#target p) solvers; h
  | Either _ -> h

let decide_branch modified solvers h =
  match h.condition with
  | Branch(p,a,b) ->
      let q = simplify_branch solvers p in
      if q != p then
        ( modified := true ; update_cond h (Branch(q,a,b)) )
      else h
  | _ -> h

let add_infer modified s hs =
  let p = p_conj s#infer in
  if p != p_true then
    ( modified := true ; step ~descr:s#name (Have p) :: hs )
  else
    hs

type outcome =
  | NoSimplification
  | Simplified of hsp
  | Trivial

and hsp = step list * pred

let apply_simplifiers (solvers : simplifier list) (hs,g) =
  if solvers = [] then NoSimplification
  else
    try
      let modified = ref false in
      let solvers = List.map (fun s -> s#copy) solvers in
      let hs = List.map (apply_hyp modified solvers) hs in
      List.iter (fun s -> s#target g) solvers ;
      List.iter (fun s -> s#fixpoint) solvers ;
      let hs = List.map (decide_branch modified solvers) hs in
      let hs = List.fold_right (add_infer modified) solvers hs in
      let p = simplify_goal solvers g in
      if p != g || !modified then
        Simplified (hs,p)
      else
        NoSimplification
    with Contradiction ->
      Trivial

(* -------------------------------------------------------------------------- *)
(* --- Sequence Builder                                                   --- *)
(* -------------------------------------------------------------------------- *)

let empty = {
  seq_size = 0 ;
  seq_vars = Vars.empty ;
  seq_core = Pset.empty ;
  seq_catg = EMPTY ;
  seq_list = [] ;
}

let trivial = empty , F.p_true

let append sa sb =
  if sa.seq_size = 0 then sb else
  if sb.seq_size = 0 then sa else
    let seq_size = sa.seq_size + sb.seq_size in
    let seq_vars = Vars.union sa.seq_vars sb.seq_vars in
    let seq_core = Pset.union sa.seq_core sb.seq_core in
    let seq_list = sa.seq_list @ sb.seq_list in
    let seq_catg = c_and sa.seq_catg sb.seq_catg in
    { seq_size ; seq_vars ; seq_core ; seq_catg ; seq_list }

let concat slist =
  if slist = [] then empty else
    let seq_size = List.fold_left (fun n s -> n + s.seq_size) 0 slist in
    let seq_list = List.concat (List.map (fun s -> s.seq_list) slist) in
    let seq_vars = List.fold_left (fun w s -> Vars.union w s.seq_vars)
        Vars.empty slist in
    let seq_core = List.fold_left (fun w s -> Pset.union w s.seq_core)
        Pset.empty slist in
    let seq_catg = c_conj catg_seq slist in
    { seq_size ; seq_vars ; seq_core ; seq_catg ; seq_list }

let seq_branch ?stmt p sa sb =
  sequence [step ?stmt (Branch(p,sa,sb))]

(* -------------------------------------------------------------------------- *)
(* --- Introduction Utilities                                             --- *)
(* -------------------------------------------------------------------------- *)

let lemma g =
  let cc g =
    let hs,p = forall_intro g in
    let hs = List.map (fun p -> step (Have p)) hs in
    sequence hs , p
  in Lang.local ~vars:(F.varsp g) cc g

let introduction (hs,g) =
  let flag = ref false in
  let intro p = let q = exist_intro p in if q != p then flag := true ; q in
  let hj = List.map (map_step intro) hs.seq_list in
  let hi,p = forall_intro g in
  let hi = List.map (fun p -> step (Have p)) hi in
  if not !flag && hi == [] then
    if p == g then None else Some (hs , p)
  else
    Some (sequence (hi @ hj) , p)

let introduction_eq s = match introduction s with
  | Some s' -> s'
  | None -> s

(* -------------------------------------------------------------------------- *)
(* --- Constant Folder                                                    --- *)
(* -------------------------------------------------------------------------- *)

module ConstantFolder =
struct

  open Qed