inlining.mli 2.59 KB
Newer Older
Andrei Paskevich's avatar
Andrei Paskevich committed
1 2 3
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
4
(*  Copyright 2010-2015   --   INRIA - CNRS - Paris-Sud University  *)
Andrei Paskevich's avatar
Andrei Paskevich committed
5 6 7 8 9
(*                                                                  *)
(*  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.                           *)
(********************************************************************)
Francois Bobot's avatar
Francois Bobot committed
10

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

val meta : Theory.meta

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

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

(** [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
34

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

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

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

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

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

49 50 51 52 53 54
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,...) *)

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

type env

val empty_env : env

62
val addfs : env -> Term.lsymbol -> Term.vsymbol list -> Term.term -> env
63
val addps : env -> Term.lsymbol -> Term.vsymbol list -> Term.term -> env
64 65
(** [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
66
    the same type as the arguments of [ls] *)
Francois Bobot's avatar
Francois Bobot committed
67

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