model_parser.mli 3.93 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 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50
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

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 60
type model_element = { 
  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
val create_model_element : 
  name     : string -> 
  value    : model_value -> 
73 74 75
  ?location : Loc.position -> 
  ?term     : Term.term ->
  unit ->
76 77 78 79 80 81
  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

82 83 84
    @param location : source-code location of the element 
    
    @param term : why term corresponding to the element *)
85

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

val empty_model : model

(*
*************************************************************** 
**  Quering the model
***************************************************************
*)
100

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

val model_to_string : model -> string

105
val interleave_with_source : model -> string -> string -> string
106 107 108 109 110 111 112 113 114 115 116

(*
*************************************************************** 
** Registering model parser
***************************************************************
*)
type model_parser =  string -> Printer.printer_mapping -> model
(** Parses the input string into model elements, estabilishes 
    a mapping between these elements and mapping from printer 
    and builds model data structure.
*)
117

118 119
type raw_model_parser =  string -> model_element list
(** Parses the input string into model elements. *)
120

121
val register_model_parser : desc:Pp.formatted -> string -> raw_model_parser -> unit
122 123 124 125

val lookup_model_parser : string -> model_parser

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