inlining.mli 2.66 KB
Newer Older
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  *)
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
(*                                                                  *)
10
(********************************************************************)
Francois Bobot's avatar
Francois Bobot committed
11

12
(** Inline non-recursive definitions *)
13 14 15 16

val meta : Theory.meta

(** {2 Generic inlining} *)
Francois Bobot's avatar
Francois Bobot committed
17

Francois Bobot's avatar
Francois Bobot committed
18
val t :
19
  ?use_meta:bool ->
20
  ?in_goal:bool ->
21
  notdeft:(Term.term -> bool) ->
22
  notdeff:(Term.term -> bool) ->
23
  notls  :(Term.lsymbol -> bool) ->
24
  Task.task Trans.trans
25 26 27 28 29 30 31 32 33 34

(** [t ~use_meta ~in_goal ~notdeft ~notdeff ~notls] returns a transformation
    that expands a symbol [ls] in the subsequent declarations unless [ls]
    satisfies one of the following conditions:
    - [ls] is defined via a (mutually) recursive definition;
    - [ls] is an inductive predicate or an algebraic type constructor;
    - [ls] is a function symbol and [notdeft] returns true on its definition;
    - [ls] is a predicate symbol and [notdeff] returns true on its definition;
    - [notls ls] returns [true];
    - [use_meta] is set and [ls] is tagged by "inline : no"
Francois Bobot's avatar
Francois Bobot committed
35

36 37
    Notice that [use_meta], [notdeft], [notdeff], [notls] restrict only which
    symbols are inlined not when.
38 39

    If [in_goal] is set, only the top-most symbols in the goal are expanded.
40
*)
Francois Bobot's avatar
Francois Bobot committed
41

42
(** {2 Registered Transformation} *)
Francois Bobot's avatar
Francois Bobot committed
43

44
val all : Task.task Trans.trans
45
(** [all] corresponds to the transformation "inline_all" *)
Francois Bobot's avatar
Francois Bobot committed
46

47 48
val goal : Task.task Trans.trans
(** [goal] corresponds to the transformation "inline_goal" *)
Francois Bobot's avatar
Francois Bobot committed
49

50 51 52 53 54 55
val trivial : Task.task Trans.trans
(** [trivial] corresponds to the transformation "inline_trivial"
    Inline only the trivial definition :
    logic c : t = a
    logic f(x : t,...., ) : t = g(y : t2,...) *)

56
(*
57
(** Functions to use in other transformations if inlining is needed *)
Francois Bobot's avatar
Francois Bobot committed
58 59 60 61 62

type env

val empty_env : env

63
val addfs : env -> Term.lsymbol -> Term.vsymbol list -> Term.term -> env
64
val addps : env -> Term.lsymbol -> Term.vsymbol list -> Term.term -> env
65 66
(** [addls env ls vs t] trigger the inlining of [ls] by the definition
    [t] with the free variables [vs]. The variables of [vs] must have
67
    the same type as the arguments of [ls] *)
Francois Bobot's avatar
Francois Bobot committed
68

Andrei Paskevich's avatar
Andrei Paskevich committed
69
val replacet : env -> Term.term -> Term.term
70
val replacep : env -> Term.term -> Term.term
71
*)