model_parser.mli 2.85 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 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
(** Counter-example model values *)
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;
}

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

val array_add_element : 
  array : model_array -> 
  index : model_value -> 
  value : model_value -> 
  model_array
(** Adds an element to the array. 
    @param array : the array to that the element will be added
    
    @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

(** Counter-example model elements. Each element represents
    a counter-example for a single source-code element.*)
49 50
type model_element = { 
  me_name     : string;
51 52 53 54 55
    (** 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. *)
56 57
  me_term     : Term.term option;
    (** Why term corresponding to the element.  *)
58 59
}

60 61 62
val create_model_element : 
  name     : string -> 
  value    : model_value -> 
63 64 65
  ?location : Loc.position -> 
  ?term     : Term.term ->
  unit ->
66 67 68 69 70 71
  model_element
(** Creates a counter-example model element. 
    @param name : the name of the source-code element

    @param value  : counter-example value for the element

72 73 74
    @param location : source-code location of the element 
    
    @param term : why term corresponding to the element *)
75 76 77 78 79

val print_model : Format.formatter -> model_element list -> unit

val model_to_string : model_element list -> string

80
type model_parser = string ->  Printer.printer_mapping -> model_element list
81 82 83 84 85 86

val register_model_parser : desc:Pp.formatted -> string -> model_parser -> unit

val lookup_model_parser : string -> model_parser

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