Vous avez reçu un message "Your GitLab account has been locked ..." ? Pas d'inquiétude : lisez cet article https://docs.gricad-pages.univ-grenoble-alpes.fr/help/unlock/

formula.ml 5.77 KB
Newer Older
1
(*-----------------------------------------------------------------------
2
** Copyright (C) 2001, 2002 - Verimag.
3
4
5
** This file may only be copied under the terms of the GNU Library General
** Public License 
**-----------------------------------------------------------------------
6
**
7
8
9
10
** File: formula.ml
** Main author: jahier@imag.fr
*)

11
open Value
12

13
14
15
16
17
18
19
20
(****************************************************************************)

type expr = 
  | Sum  of expr * expr 
  | Diff of expr * expr 
  | Prod of expr * expr 
  | Quot of expr * expr 
  | Mod  of expr * expr 
21
22
23

  | Ival of int 
  | Fval of float
24
25
26
27
28
29
  | Ivar of string
  | Fvar of string
      
  | Ite of formula * expr * expr
and
  formula =
30
31
  | And of formula * formula
  | Or  of formula * formula
32
  | IteB of formula * formula * formula 
33
  | Not of formula
34
  | EqB of formula * formula
35

36
37
  | True
  | False
38
  | Bvar of string
39

40
41
42
43
44
  | Eq    of expr * expr (* =  *)
  | Sup   of expr * expr (* >  *)
  | SupEq of expr * expr (* >= *)
  | Inf   of expr * expr (* <  *)
  | InfEq of expr * expr (* <= *)
45
46
47
48
49
50
51
52

type formula_eps = 
  | Eps
  | Form of formula

(****************************************************************************)

type node = int
53
54
55
56
type weight =    
    Wint of int 
  | Wident of string
  | Wident_not_sig of string
57
		
58
type arc = node * node
59
type arc_info = weight * formula_eps * string
60
61

type var_name = string
62
type vn = var_name
63

64
type subst = (var_name * Value.t)
65
type num_subst = (var_name * Value.num)
66

67
type var_type = BoolT | IntT of int * int | FloatT of float * float 
68
type vnt = var_name * var_type
69
70
type vne = var_name * (expr * expr)
type vnf = var_name * (formula * formula)
71

72
type env_in  = (var_name, Value.t) Hashtbl.t
73
74
75
type env_out = subst list
type env_loc = subst list

76

77
    
78
79
(****************************************************************************)

80
81
82
83
84
(* exported *)
let (formula_to_var_value: formula -> Value.t) = function
    True -> B(true)
  | False -> B(false)
  | _ -> assert false
85
    
86

87
88
89
let rec 
  (formula_eps_to_string: formula_eps -> string) =
  fun fe -> match fe with
90
      Eps -> " : eps"
91
    | Form(f) -> (" : " ^ (formula_to_string f))
92
93
94
and
  (formula_to_string: formula -> string) =
  fun f -> match f with
95
96
      And(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " ^ " ^ 
		      (formula_to_string f2) ^ ")")
97
    | Or(f1, f2) -> ("(" ^ (formula_to_string f1) ^ " || " ^  
98
		     (formula_to_string f2) ^ ")")
99
100
101
    | IteB(f1, f2, f3) -> ("(if " ^ (formula_to_string f1) ^ " then " ^ 
		       (formula_to_string f2) ^ " else  " ^ 
		       (formula_to_string f3)  ^ ")")
102
    | Not(f1) -> ("!(" ^ (formula_to_string f1) ^ ")")
103
    | EqB(f1, f2) -> ((formula_to_string f1) ^ " = " ^ (formula_to_string f2))
104
105
    | True -> "true"
    | False ->  "false"
106
    | Bvar(str) -> (Prevar.format str)
107
    | Eq(e1, e2) -> ((expr_to_string e1) ^ " = " ^ (expr_to_string e2))
108
109
110
111
    | SupEq(e1, e2) -> ((expr_to_string e1) ^ " >= " ^ (expr_to_string e2))
    | Sup(e1, e2) ->  ((expr_to_string e1) ^ " > " ^ (expr_to_string e2))
    | InfEq(e1, e2) -> ((expr_to_string e1) ^ " <= " ^ (expr_to_string e2))
    | Inf(e1, e2) ->  ((expr_to_string e1) ^ " < " ^ (expr_to_string e2))
112
113
114
115
116
117
118
119
120
121
122
123
124
and
  (expr_to_string: expr -> string) =
  fun e -> match e with 
      Sum(e1, e2) ->  ("(" ^ (expr_to_string e1) ^ " + " ^ 
		       (expr_to_string e2)  ^ ")")
    | Diff(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " - " ^ 
		       (expr_to_string e2)  ^ ")")
    | Prod(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " * " ^ 
		       (expr_to_string e2)  ^ ")")
    | Quot(e1, e2) -> ("(" ^ (expr_to_string e1) ^ " / " ^ 
		       (expr_to_string e2)  ^ ")")
    | Mod(e1, e2) ->  ("(" ^ (expr_to_string e1) ^ " mod " ^ 
		       (expr_to_string e2)  ^ ")")
125
126
    | Ivar(str) -> (Prevar.format str)
    | Fvar(str) -> (Prevar.format str)
127
    | Ival(i) -> string_of_int i
128
    | Fval(f) -> Util.my_string_of_float f 
129
130
131
132
    | Ite(f,e1,e2) -> ("(if " ^ (formula_to_string f) ^ " then " ^ 
		       (expr_to_string e1) ^ " else  " ^ 
		       (expr_to_string e2)  ^ ")")

133

134
135
136
137
138
139
140
141
let rec (support : formula -> vn list) =
  fun f -> 
    match f with 
	And(Bvar(vn), ff) -> (vn::(support ff))
      | True ->  []
      | _ -> assert false

let (weight_to_string : weight -> string) = 
142
143
  fun w ->  
    match w with 
144
145
	Wint(w) -> string_of_int w 
      | Wident(label) -> label
146
      | Wident_not_sig(label) -> ("! " ^ label)
147

148

149
let (arc_info_to_string : arc_info -> string) =
150
151
152
153
154
155
156
157
158
159
160
  fun (weight, formula_eps, post_cond_label) -> 
    let pc_str = 
      if 
	post_cond_label = "identity" 
      then 
	"" 
      else 
	(" : " ^ post_cond_label) 
    in
    ( (weight_to_string weight) ^ " "  ^ 
      (formula_eps_to_string formula_eps) ^  pc_str)
161

162

163
164
165
let (var_type_to_string : var_type -> string) =
  fun vt -> 
    match vt with
166
	BoolT  -> "bool"
167
168
      | IntT(i1, i2) -> "int"
      | FloatT(f1, f2) -> "float"
169

170
171
172
173
174
175
176
let (var_type_to_string2 : var_type -> string) =
  fun vt -> 
    match vt with
	BoolT  -> "bool"
      | IntT(i1, i2) -> "int"
      | FloatT(f1, f2) -> "real"

177
178
179
180
181
182
183



let (print_subst_list : subst list -> out_channel -> unit) =
  fun sl oc -> 
    List.iter 
    (fun (vn, e) -> 
184
       output_string oc (Prevar.format vn);
185
       output_string oc " = ";
186
       Value.print oc e; 
187
       output_string oc "\n\t"
188
189
    ) 
    (Util.sort_list_string_pair sl)
190
191
192
193
194

let (print_env_in : env_in -> out_channel -> unit) =
  fun tbl oc -> 
    Hashtbl.iter 
    (fun vn e -> 
195
       output_string oc (Prevar.format vn) ;
196
       output_string oc " = ";
197
       Value.print oc e; 
198
       output_string oc "\n\t"
199
200
201
    ) 
    tbl
  
202
203
204
(****************************************************************************)

(* exported *)
205
let (expr_to_var_value: expr -> Value.t) = function
206
207
208
209
210
211
    Ival(i) -> N(I(i))
  | Fval(f) -> N(F(f))
  | _ -> assert false


(* exported *)
212
let (formula_to_var_value: formula -> Value.t) = function
213
214
215
    True -> B(true)
  | False -> B(false)
  | _ -> assert false