inlining.mli 3.32 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18
(**************************************************************************)
(*                                                                        *)
(*  Copyright (C) 2010-                                                   *)
(*    Francois Bobot                                                      *)
(*    Jean-Christophe Filliatre                                           *)
(*    Johannes Kanig                                                      *)
(*    Andrei Paskevich                                                    *)
(*                                                                        *)
(*  This software is free software; you can redistribute it and/or        *)
(*  modify it under the terms of the GNU Library General Public           *)
(*  License version 2.1, with the special exception on linking            *)
(*  described in file LICENSE.                                            *)
(*                                                                        *)
(*  This software 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.                  *)
(*                                                                        *)
(**************************************************************************)
Francois Bobot's avatar
Francois Bobot committed
19

20
(** Inline non-recursive definitions *)
21 22 23 24

val meta : Theory.meta

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

Francois Bobot's avatar
Francois Bobot committed
26
val t :
27
  ?use_meta:bool ->
28
  ?in_goal:bool ->
29 30 31
  notdeft:(Term.term -> bool) ->
  notdeff:(Term.fmla -> bool) ->
  notls  :(Term.lsymbol -> bool) ->
32
  Task.task Trans.trans
33 34 35 36 37 38 39 40 41 42

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

44 45
    Notice that [use_meta], [notdeft], [notdeff], [notls] restrict only which
    symbols are inlined not when.
46 47

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

50
(** {2 Registered Transformation} *)
Francois Bobot's avatar
Francois Bobot committed
51

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

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

58 59 60 61 62 63
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,...) *)

64
(*
65
(** Functions to use in other transformations if inlining is needed *)
Francois Bobot's avatar
Francois Bobot committed
66 67 68 69 70

type env

val empty_env : env

71 72 73 74
val addfs : env -> Term.lsymbol -> Term.vsymbol list -> Term.term -> env
val addps : env -> Term.lsymbol -> Term.vsymbol list -> Term.fmla -> env
(** [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
75
    the same type as the arguments of [ls] *)
Francois Bobot's avatar
Francois Bobot committed
76

Andrei Paskevich's avatar
Andrei Paskevich committed
77
val replacet : env -> Term.term -> Term.term
Francois Bobot's avatar
Francois Bobot committed
78
val replacep : env -> Term.fmla -> Term.fmla
79
*)