destruct.ml

(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2018   --   Inria - CNRS - Paris-Sud University  *)
(*                                                                  *)
(*  This software is distributed under the terms of the GNU Lesser  *)
(*  General Public License version 2.1, with the special exception  *)
(*  on linking described in file LICENSE.                           *)
(*                                                                  *)
(********************************************************************)

open Term
open Decl
open Args_wrapper
open Generic_arg_trans_utils

(** This file contains transformations with arguments that eliminates logic
    connectors (instantiate, destruct, destruct_alg). *)

(** Explanation *)

(* Explanation for destruct premises *)
let destruct_expl = "destruct premise"

let is_lsymbol t =
  match t.t_node with
  | Tapp (_, []) -> true
  | _ -> false

let create_constant ty =
  let fresh_name = Ident.id_fresh "x" in
  let ls = create_lsymbol fresh_name [] (Some ty) in
  (ls, create_param_decl ls)

let rec return_list list_types type_subst =
  match list_types with
  | [] -> []
  | hd :: tl ->
      create_constant (Ty.ty_inst type_subst hd) :: return_list tl type_subst

let my_ls_app_inst ls ty =
  match ls.ls_value, ty with
    | Some _, None -> raise (PredicateSymbolExpected ls)
    | None, Some _ -> raise (FunctionSymbolExpected ls)
    | Some vty, Some ty -> Ty.ty_match Ty.Mtv.empty vty ty
    | None, None -> Ty.Mtv.empty

let rec build_decls cls x =
  match cls with
  | [] -> []
  | (cs, _) :: tl ->
      let type_subst = my_ls_app_inst cs x.t_ty in
      let l = return_list cs.ls_args type_subst in
      let teqx =
        (t_app cs (List.map (fun x -> t_app_infer (fst x) []) l) x.t_ty) in
      let ht = t_equ x teqx in
      let h = Decl.create_prsymbol (gen_ident "h") in
      let new_hyp = Decl.create_prop_decl Decl.Paxiom h ht in
      ((List.map snd l) @ [new_hyp]) :: build_decls tl x

(* Enumerate all constants of a term *)
let rec compounds_of acc (t: term) =
  match t.t_node with
  | Tapp (ls, _) -> Term.t_fold compounds_of (Term.Sls.add ls acc) t
  | _ -> Term.t_fold compounds_of acc t

(* This tactic acts on a term of algebraic type. It introduces one
   new goal per constructor of the type and introduce corresponding
   variables. It also introduce the equality between the term and
   its destruction in the context.
   When replace is set to true, a susbtitution is done when x is an lsymbol.
 *)
let destruct_alg replace (x: term) : Task.task Trans.tlist =
  let ty = x.t_ty in
  (* We list all the constants used in x so that we know the first place in the
     task where we can introduce hypothesis about the destruction of x. *)
  let ls_of_x = ref (compounds_of Term.Sls.empty x) in
  let defined = ref false in
  let r = ref [] in
  match ty with
  | None -> raise (Cannot_infer_type "destruct")
  | Some ty ->
    begin
      match ty.Ty.ty_node with
      | Ty.Tyvar _       -> raise (Cannot_infer_type "destruct")
      | Ty.Tyapp (ts, _) ->
        let trans = Trans.decl_l (fun d ->
          match d.d_node with
          (* TODO not necessary to check this first: this can be optimized *)
          | _ when (not !defined) && Term.Sls.is_empty !ls_of_x ->
              if !r = [] then
                [[d]]
              else
                begin
                  defined := true;
                  List.map (fun x -> x @ [d]) !r
                end
          | Dlogic dls          ->
              ls_of_x :=
                List.fold_left
                  (fun acc (ls, _) -> Term.Sls.remove ls acc)
                  !ls_of_x dls;
              [[d]]
          | Dparam ls ->
              ls_of_x := Term.Sls.remove ls !ls_of_x;
              [[d]]
          | Dind (_, ils)       ->
              ls_of_x :=
                List.fold_left
                  (fun acc (ls, _) -> Term.Sls.remove ls acc)
                  !ls_of_x ils;
              [[d]]
          | Ddata dls           ->
              (try
                (let cls = List.assoc ts dls in
                r := build_decls cls x;
                [[d]]
                )
              with Not_found -> [[d]])
          | Dprop (Pgoal, _, _) ->
              [[d]]
          | _ -> [[d]]) None
        in
        if replace && is_lsymbol x then
          Trans.compose_l trans (Trans.singleton (Subst.subst [x]))
        else
          trans
    end

(* Destruct the head term of an hypothesis if it is either
   conjunction, disjunction or exists *)
let destruct pr : Task.task Trans.tlist =
  let new_decl = ref None in
  (* This transformation destructs the hypothesis pr. In case pr is an
     implication H : A -> B, the destruction creates two task (one with H
     removed and one with H : B). It also fills new_decl with A.
     The next transformation replace the first goal with A. *)
  let tr_decl =
    Trans.decl_l (fun d ->
    match d.d_node with
    | Dprop (Paxiom, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
      begin
        match ht.t_node with
        | Tbinop (Tand, t1, t2) ->
          let new_pr1 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl1 = create_prop_decl Paxiom new_pr1 t1 in
          let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
          [[new_decl1;new_decl2]]
        | Tbinop (Tor, t1, t2) ->
          let new_pr1 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl1 = create_prop_decl Paxiom new_pr1 t1 in
          let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
          let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
          [[new_decl1];[new_decl2]]
        | Tbinop (Timplies, t1, t2) ->
          begin
            let new_pr2 = create_prsymbol (Ident.id_clone dpr.pr_name) in
            let new_decl2 = create_prop_decl Paxiom new_pr2 t2 in
            new_decl := Some t1;
            (* Creates a task with hypothesis removes (need to prove t1) and one
               with hypothesis replaced by t2 (needs to prove current goal).
               Example: "false -> false" *)
            [] :: [[new_decl2]]
          end
        | Tquant (Texists, tb) ->
          begin
            let (vsl, tr, te) = Term.t_open_quant tb in
            match vsl with
            | x :: tl ->
                let ls = create_lsymbol (Ident.id_clone x.vs_name) [] (Some x.vs_ty) in
                let tx = fs_app ls [] x.vs_ty in
                let x_decl = create_param_decl ls in
                (try
                  let part_t = t_subst_single x tx te in
                  let new_t = t_quant_close Texists tl tr part_t in
                  let new_pr = create_prsymbol (Ident.id_clone dpr.pr_name) in
                  let new_decl = create_prop_decl Paxiom new_pr new_t in
                  [[d; x_decl; new_decl]]
                with
                | Ty.TypeMismatch (ty1, ty2) ->
                    raise (Arg_trans_type ("destruct_exists", ty1, ty2)))
            | [] -> raise (Arg_trans ("destruct_exists"))
          end
        | _ -> raise (Arg_trans ("destruct"))
      end
    | _ -> [[d]]) None in
  Trans.store (fun task ->
    let goal, task = Task.task_separate_goal task in
    let new_tasks = Trans.apply tr_decl task in
    match !new_decl with
    | None ->
      (* Normal destruct case (not implication): add goal back to tasks *)
      List.map (fun task -> Task.add_tdecl task goal) new_tasks
    | Some new_decl ->
      match new_tasks with
      (* Destruct case for an implication. The first goal should be new_decl,
         the second one is unchanged. *)
      | first_task :: second_task :: [] ->
          let pr = create_prsymbol (gen_ident "G") in
          let new_goal = create_goal ~expl:destruct_expl pr new_decl in
          let first_goal = Task.add_decl first_task new_goal in
          let second_goal = Task.add_tdecl second_task goal in
          first_goal :: second_goal :: []
      | _ -> assert false)

(* from task [delta, name:forall x.A |- G,
     build the task [delta,name:forall x.A,name':A[x -> t]] |- G] *)
let instantiate (pr: Decl.prsymbol) lt =
  let r = ref [] in
  Trans.decl
    (fun d ->
      match d.d_node with
      | Dprop (pk, dpr, ht) when Ident.id_equal dpr.pr_name pr.pr_name ->
          let t_subst = subst_forall_list ht lt in
          let new_pr = create_prsymbol (gen_ident "Hinst") in
          let new_decl = create_prop_decl pk new_pr t_subst in
          r := [new_decl];
          [d]
      | Dprop (Pgoal, _, _) -> !r @ [d]
      | _ -> [d]) None

let () = wrap_and_register
    ~desc:"instantiate <prop> <term list> generates a new hypothesis with quantified variables of prop replaced with terms"
    "instantiate"
    (Tprsymbol (Ttermlist Ttrans)) instantiate

let () = wrap_and_register ~desc:"destruct <name> destructs the head logic constructor of hypothesis name (/\\, \\/, -> or <->).\nTo destruct a literal of algebraic type, use destruct_alg."
    "destruct" (Tprsymbol Ttrans_l) destruct

let () = wrap_and_register ~desc:"destruct <name> destructs as an algebraic type"
    "destruct_alg" (Tterm Ttrans_l) (destruct_alg false)

let () = wrap_and_register ~desc:"destruct <name> destructs as an algebraic type and substitute the definition if an lsymbol was provided"
    "destruct_alg_subst" (Tterm Ttrans_l) (destruct_alg true)