introduction.ml 3.39 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
4
(*  Copyright 2010-2016   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8
(*                                                                  *)
(*  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.                           *)
9
(*                                                                  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
10
(********************************************************************)
MARCHE Claude's avatar
MARCHE Claude committed
11

12 13
(*
  This module was poorly designed by Claude Marché, with the
14
  enormous help of Jean-Christophe Filliâtre and Andrei Paskevich
15 16 17
  for finding the right function in the Why3 API
*)

MARCHE Claude's avatar
MARCHE Claude committed
18
open Ident
19
open Ty
MARCHE Claude's avatar
MARCHE Claude committed
20 21 22
open Term
open Decl

Sylvain Dailler's avatar
Sylvain Dailler committed
23 24 25
(* This label is used to stop the introduction transformation to introduce
variables past it. It is generated by software that uses why3 as a backend
such as SPARK (for counterexamples) *)
26 27 28 29 30
let stop_intro = Ident.create_label "stop_intro"

let rec intros pr f =
  if Slab.mem stop_intro f.t_label then [create_prop_decl Pgoal pr f] else
  match f.t_node with
31
  | Tbinop (Timplies,{ t_node = Tbinop (Tor,f2,{ t_node = Ttrue }) },_)
32 33
      when Slab.mem Term.asym_label f2.t_label ->
        [create_prop_decl Pgoal pr f]
34
  | Tbinop (Timplies,f1,f2) ->
35
      (* split f1 *)
36
      (* f is going to be removed, preserve its labels and location in f2  *)
37
      let f2 = t_label_copy f f2 in
38
      let l = Split_goal.split_intro_right f1 in
39
      List.fold_right
40 41 42 43 44 45
        (fun f acc ->
           let id = create_prsymbol (id_fresh "H") in
           let d = create_prop_decl Paxiom id f in
           d :: acc)
        l
        (intros pr f2)
46
  | Tquant (Tforall,fq) ->
47
      let vsl,_trl,f_t = t_open_quant fq in
MARCHE Claude's avatar
MARCHE Claude committed
48 49
      let intro_var subst vs =
        let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
50
        Mvs.add vs (fs_app ls [] vs.vs_ty) subst,
51
        create_param_decl ls
MARCHE Claude's avatar
MARCHE Claude committed
52
      in
53
      let subst, dl = Lists.map_fold_left intro_var Mvs.empty vsl in
54 55
      (* preserve labels and location of f  *)
      let f = t_label_copy f (t_subst subst f_t) in
MARCHE Claude's avatar
MARCHE Claude committed
56
      dl @ intros pr f
57 58 59 60 61 62
  | Tlet (t,fb) ->
      let vs,f = t_open_bound fb in
      let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
      let f = t_subst_single vs (fs_app ls [] vs.vs_ty) f in
      let d = create_logic_decl [make_ls_defn ls [] t] in
      d :: intros pr f
MARCHE Claude's avatar
MARCHE Claude committed
63 64
  | _ -> [create_prop_decl Pgoal pr f]

65 66 67 68 69 70 71 72
let intros pr f =
  let tvs = t_ty_freevars Stv.empty f in
  let mk_ts tv () = create_tysymbol (id_clone tv.tv_name) [] None in
  let tvm = Mtv.mapi mk_ts tvs in
  let decls = Mtv.map create_ty_decl tvm in
  let subst = Mtv.map (fun ts -> ty_app ts []) tvm in
  Mtv.values decls @ intros pr (t_ty_subst subst Mvs.empty f)

73 74 75
let introduce_premises = Trans.goal intros

let () = Trans.register_transform "introduce_premises" introduce_premises
76 77
  ~desc:"Introduce@ universal@ quantification@ and@ hypothesis@ in@ the@ \
         goal@ into@ constant@ symbol@ and@ axioms."
Andrei Paskevich's avatar
Andrei Paskevich committed
78

79 80 81 82 83 84
let split_intro =
  Trans.compose_l Split_goal.split_goal_wp (Trans.singleton introduce_premises)

let () = Trans.register_transform_l "split_intro" split_intro
  ~desc:"Same@ as@ split_goal_wp,@ but@ moves@ \
    the@ implication@ antecedents@ to@ premises."