model_parser.mli 4.77 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11
(********************************************************************)
(*                                                                  *)
(*  The Why3 Verification Platform   /   The Why3 Development Team  *)
(*  Copyright 2010-2015   --   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.                           *)
(*                                                                  *)
(********************************************************************)

12
(*
13
***************************************************************
14 15 16
**  Counter-example model values
****************************************************************
*)
17 18 19 20 21 22 23 24 25 26 27 28 29
type model_value =
 | Integer of string
 | Array of model_array
 | Other of string
and  arr_index = {
  arr_index_key : int;
  arr_index_value : model_value;
}
and model_array = {
  arr_others  : model_value;
  arr_indices : arr_index list;
}

30 31
val array_create_constant :
  value : model_value ->
32 33 34
  model_array
(** Creates constant array with all indices equal to the parameter value. *)

35 36 37 38
val array_add_element :
  array : model_array ->
  index : model_value ->
  value : model_value ->
39
  model_array
40
(** Adds an element to the array.
41
    @param array : the array to that the element will be added
42

43 44 45 46 47 48 49 50
    @param index : the index on which the element will be added.
    Note that the index must be of value model_value.Integer

    @param value : the value of the element to be added
*)

val print_model_value : Format.formatter -> model_value -> unit

51 52

(*
53
***************************************************************
54 55 56
**  Model elements
***************************************************************
*)
57 58
(** Counter-example model elements. Each element represents
    a counter-example for a single source-code element.*)
59
type model_element = {
60
  me_name     : string;
61 62 63 64 65
    (** The name of the source-code element.  *)
  me_value    : model_value;
    (** Counter-example value for the element. *)
  me_location : Loc.position option;
    (** Source-code location of the element. *)
66 67
  me_term     : Term.term option;
    (** Why term corresponding to the element.  *)
68 69
}

70 71 72 73
val create_model_element :
  name     : string ->
  value    : model_value ->
  ?location : Loc.position ->
74 75
  ?term     : Term.term ->
  unit ->
76
  model_element
77
(** Creates a counter-example model element.
78 79 80 81
    @param name : the name of the source-code element

    @param value  : counter-example value for the element

82 83
    @param location : source-code location of the element

84
    @param term : why term corresponding to the element *)
85

86
(*
87
***************************************************************
88 89
**  Model definitions
***************************************************************
90 91
*)
type model
92 93 94 95

val empty_model : model

(*
96
***************************************************************
97 98 99
**  Quering the model
***************************************************************
*)
100

101 102 103 104
val print_model : Format.formatter -> model -> unit

val model_to_string : model -> string

105 106 107 108
val print_model_json : Format.formatter -> model -> unit

val model_to_string_json : model -> string

109
val interleave_with_source :
110 111
  ?start_comment:string ->
  ?end_comment:string ->
112 113 114
  model ->
  string ->
  string ->
115
  string
116 117

(*
118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137
***************************************************************
**  Filtering the model
***************************************************************
*)
val model_for_positions_and_decls : model ->
  positions: Loc.position list -> model
(** Given a model and a list of source-code positions returns model
    that contains only elements from the input model that are on these
    positions plus for every file in the model, elements that are
    in the positions of function declarations. Elements with other
    positions are filtered out.

    Assumes that for each file the element on the first line of the model
    has position of function declaration.

    Only filename and line number is used to identify positions.
*)

(*
***************************************************************
138 139 140 141
** Registering model parser
***************************************************************
*)
type model_parser =  string -> Printer.printer_mapping -> model
142 143
(** Parses the input string into model elements, estabilishes
    a mapping between these elements and mapping from printer
144 145
    and builds model data structure.
*)
146

147 148
type raw_model_parser =  string -> model_element list
(** Parses the input string into model elements. *)
149

150
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
151 152 153 154

val lookup_model_parser : string -> model_parser

val list_model_parsers : unit -> (string * Pp.formatted) list