2010-06-15 14:05:26 +02:00
|
|
|
(** This module defines static expressions, used in arrays definition
|
|
|
|
|
|
|
|
and anywhere a static value is expected. For instance:
|
|
|
|
const n: int = 3;
|
|
|
|
var x : int^n; var y : int^(n + 2);
|
|
|
|
x[n - 1], x[1 + 3],...
|
2010-06-15 10:49:03 +02:00
|
|
|
*)
|
|
|
|
open Names
|
2010-06-15 14:05:26 +02:00
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
open Format
|
2010-06-15 14:05:26 +02:00
|
|
|
|
|
|
|
type op = | SPlus | SMinus | STimes | SDiv
|
2010-06-15 10:49:03 +02:00
|
|
|
|
|
|
|
type size_exp =
|
2010-06-15 14:05:26 +02:00
|
|
|
| SConst of int | SVar of name | SOp of op * size_exp * size_exp
|
2010-06-15 10:49:03 +02:00
|
|
|
|
|
|
|
(** Constraints on size expressions. *)
|
|
|
|
type size_constr =
|
|
|
|
| Equal of size_exp * size_exp (* e1 = e2*)
|
|
|
|
| LEqual of size_exp * size_exp (* e1 <= e2 *)
|
2010-06-15 14:05:26 +02:00
|
|
|
| False
|
2010-06-15 10:49:03 +02:00
|
|
|
|
2010-06-15 14:05:26 +02:00
|
|
|
(* unsatisfiable constraint *)
|
|
|
|
exception Instanciation_failed
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
exception Not_static
|
2010-06-15 14:05:26 +02:00
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** Returns the op from an operator full name. *)
|
|
|
|
let op_from_app_name n =
|
|
|
|
match n with
|
2010-06-15 14:05:26 +02:00
|
|
|
| Modname { qual = "Pervasives"; id = "+" } | Name "+" -> SPlus
|
|
|
|
| Modname { qual = "Pervasives"; id = "-" } | Name "-" -> SMinus
|
|
|
|
| Modname { qual = "Pervasives"; id = "*" } | Name "*" -> STimes
|
|
|
|
| Modname { qual = "Pervasives"; id = "/" } | Name "/" -> SDiv
|
|
|
|
| _ -> raise Not_static
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** [simplify env e] returns e simplified with the
|
|
|
|
variables values taken from env (mapping vars to integers).
|
|
|
|
Variables are replaced with their values and every operator
|
|
|
|
that can be computed is replaced with the value of the result. *)
|
2010-06-15 14:05:26 +02:00
|
|
|
let rec simplify env =
|
|
|
|
function
|
2010-06-15 10:49:03 +02:00
|
|
|
| SConst n -> SConst n
|
2010-06-15 14:05:26 +02:00
|
|
|
| SVar id -> (try simplify env (NamesEnv.find id env) with | _ -> SVar id)
|
|
|
|
| SOp (op, e1, e2) ->
|
2010-06-15 10:49:03 +02:00
|
|
|
let e1 = simplify env e1 in
|
2010-06-15 14:05:26 +02:00
|
|
|
let e2 = simplify env e2
|
|
|
|
in
|
|
|
|
(match (e1, e2) with
|
|
|
|
| (SConst n1, SConst n2) ->
|
|
|
|
let n =
|
|
|
|
(match op with
|
|
|
|
| SPlus -> n1 + n2
|
|
|
|
| SMinus -> n1 - n2
|
|
|
|
| STimes -> n1 * n2
|
|
|
|
| SDiv ->
|
|
|
|
if n2 = 0 then raise Instanciation_failed else n1 / n2)
|
|
|
|
in SConst n
|
|
|
|
| (_, _) -> SOp (op, e1, e2))
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** [int_of_size_exp env e] returns the value of the expression
|
|
|
|
[e] in the environment [env], mapping vars to integers. Raises
|
|
|
|
Instanciation_failed if it cannot be computed (if a var has no value).*)
|
|
|
|
let int_of_size_exp env e =
|
2010-06-15 14:05:26 +02:00
|
|
|
match simplify env e with | SConst n -> n | _ -> raise Instanciation_failed
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** [is_true env constr] returns whether the constraint is satisfied
|
|
|
|
in the environment (or None if this can be decided)
|
2010-06-15 14:05:26 +02:00
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
and a simplified constraint. *)
|
2010-06-15 14:05:26 +02:00
|
|
|
let is_true env =
|
|
|
|
function
|
|
|
|
| Equal (e1, e2) when e1 = e2 ->
|
|
|
|
((Some true), (Equal (simplify env e1, simplify env e2)))
|
2010-06-15 10:49:03 +02:00
|
|
|
| Equal (e1, e2) ->
|
|
|
|
let e1 = simplify env e1 in
|
2010-06-15 14:05:26 +02:00
|
|
|
let e2 = simplify env e2
|
|
|
|
in
|
|
|
|
(match (e1, e2) with
|
|
|
|
| (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Equal (e1, e2)))
|
|
|
|
| (_, _) -> (None, (Equal (e1, e2))))
|
2010-06-15 10:49:03 +02:00
|
|
|
| LEqual (e1, e2) ->
|
|
|
|
let e1 = simplify env e1 in
|
2010-06-15 14:05:26 +02:00
|
|
|
let e2 = simplify env e2
|
|
|
|
in
|
|
|
|
(match (e1, e2) with
|
|
|
|
| (SConst n1, SConst n2) -> ((Some (n1 <= n2)), (LEqual (e1, e2)))
|
|
|
|
| (_, _) -> (None, (LEqual (e1, e2))))
|
|
|
|
| False -> (None, False)
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
exception Solve_failed of size_constr
|
2010-06-15 14:05:26 +02:00
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** [solve env constr_list solves a list of constraints. It
|
2010-06-15 14:05:26 +02:00
|
|
|
removes equations that can be decided and simplify others.
|
2010-06-15 10:49:03 +02:00
|
|
|
If one equation cannot be satisfied, it raises Solve_failed. ]*)
|
2010-06-15 14:05:26 +02:00
|
|
|
let rec solve const_env =
|
|
|
|
function
|
2010-06-15 10:49:03 +02:00
|
|
|
| [] -> []
|
2010-06-15 14:05:26 +02:00
|
|
|
| c :: l ->
|
2010-06-15 10:49:03 +02:00
|
|
|
let l = solve const_env l in
|
2010-06-15 14:05:26 +02:00
|
|
|
let (res, c) = is_true const_env c
|
|
|
|
in
|
|
|
|
(match res with
|
|
|
|
| None -> c :: l
|
|
|
|
| Some v -> if not v then raise (Solve_failed c) else l)
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** Substitutes variables in the size exp with their value
|
|
|
|
in the map (mapping vars to size exps). *)
|
2010-06-15 14:05:26 +02:00
|
|
|
let rec size_exp_subst m =
|
|
|
|
function
|
|
|
|
| SVar n -> (try List.assoc n m with | Not_found -> SVar n)
|
|
|
|
| SOp (op, e1, e2) -> SOp (op, size_exp_subst m e1, size_exp_subst m e2)
|
2010-06-15 10:49:03 +02:00
|
|
|
| s -> s
|
2010-06-15 14:05:26 +02:00
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
(** Substitutes variables in the constraint list with their value
|
|
|
|
in the map (mapping vars to size exps). *)
|
|
|
|
let instanciate_constr m constr =
|
2010-06-15 14:05:26 +02:00
|
|
|
let replace_one m =
|
|
|
|
function
|
|
|
|
| Equal (e1, e2) -> Equal (size_exp_subst m e1, size_exp_subst m e2)
|
|
|
|
| LEqual (e1, e2) -> LEqual (size_exp_subst m e1, size_exp_subst m e2)
|
|
|
|
| False -> False
|
|
|
|
in List.map (replace_one m) constr
|
|
|
|
|
|
|
|
let op_to_string =
|
|
|
|
function | SPlus -> "+" | SMinus -> "-" | STimes -> "*" | SDiv -> "/"
|
|
|
|
|
|
|
|
let rec print_size_exp ff =
|
|
|
|
function
|
2010-06-15 10:49:03 +02:00
|
|
|
| SConst i -> fprintf ff "%d" i
|
|
|
|
| SVar id -> fprintf ff "%s" id
|
|
|
|
| SOp (op, e1, e2) ->
|
2010-06-15 14:05:26 +02:00
|
|
|
(fprintf ff "@[(";
|
|
|
|
print_size_exp ff e1;
|
|
|
|
fprintf ff " %s " (op_to_string op);
|
|
|
|
print_size_exp ff e2;
|
|
|
|
fprintf ff ")@]")
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
let rec print_list ff print sep l =
|
|
|
|
match l with
|
2010-06-15 14:05:26 +02:00
|
|
|
| [] -> ()
|
|
|
|
| [ x ] -> print ff x
|
|
|
|
| x :: l -> (print ff x; fprintf ff "%s@ " sep; print_list ff print sep l)
|
|
|
|
|
|
|
|
let print_size_constr ff =
|
|
|
|
function
|
|
|
|
| Equal (e1, e2) ->
|
|
|
|
(fprintf ff "@[";
|
|
|
|
print_size_exp ff e1;
|
|
|
|
fprintf ff " = ";
|
|
|
|
print_size_exp ff e2;
|
|
|
|
fprintf ff "@]")
|
|
|
|
| LEqual (e1, e2) ->
|
|
|
|
(fprintf ff "@[";
|
|
|
|
print_size_exp ff e1;
|
|
|
|
fprintf ff " <= ";
|
|
|
|
print_size_exp ff e2;
|
|
|
|
fprintf ff "@]")
|
|
|
|
| False -> fprintf ff "False"
|
|
|
|
|
2010-06-15 10:49:03 +02:00
|
|
|
let psize_constr oc c =
|
2010-06-15 14:05:26 +02:00
|
|
|
let ff = formatter_of_out_channel oc
|
|
|
|
in (print_size_constr ff c; fprintf ff "@?")
|
|
|
|
|