heptagon/compiler/global/static.ml

160 lines
5.7 KiB
OCaml
Raw Normal View History

(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(** This module defines static expressions, used in params and for constants.
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 10:49:03 +02:00
open Format
2010-06-30 17:20:56 +02:00
type static_exp =
2010-07-01 19:32:54 +02:00
| Svar of name
2010-06-30 17:20:56 +02:00
| Sint of int
| Sfloat of float
| Sbool of bool
2010-07-01 19:32:54 +02:00
| Sconstructor of
2010-06-30 17:20:56 +02:00
| Sarray_power of static_exp * static_exp (** power : 0^n : [0,0,0,0,0,..] *)
| Sarray of static_exp list (** [ e1, e2, e3 ] *)
2010-07-01 19:32:54 +02:00
| Sop of longname * static_exp list (** defined ops for now in pervasives *)
2010-06-15 10:49:03 +02:00
(** Constraints on size expressions. *)
type size_constraint =
2010-07-01 19:32:54 +02:00
| Cequal of static_exp * static_exp (* e1 = e2*)
| Clequal of static_exp * static_exp (* e1 <= e2 *)
| Cfalse
2010-06-15 10:49:03 +02:00
(* unsatisfiable constraint *)
exception Instanciation_failed
2010-06-15 10:49:03 +02:00
exception Not_static
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-07-02 15:38:11 +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. *)
let rec simplify env =
function
2010-07-06 11:12:14 +02:00
| Sconst n -> Sconst n
| Svar id -> (try simplify env (NamesEnv.find id env) with | _ -> Svar id)
| Sop (op, e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
2010-07-06 11:12:14 +02:00
| (Sconst n1, Sconst n2) ->
let n =
(match op with
2010-07-02 15:38:11 +02:00
| Splus -> n1 + n2
| Sminus -> n1 - n2
| Stimes -> n1 * n2
| Sdiv ->
if n2 = 0 then raise Instanciation_failed else n1 / n2)
2010-07-06 11:12:14 +02:00
in Sconst n
| (_, _) -> Sop (op, e1, e2))
2010-06-30 17:20:56 +02:00
(** [int_of_static_exp env e] returns the value of the expression
2010-06-15 10:49:03 +02:00
[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-07-06 11:12:14 +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 10:49:03 +02:00
and a simplified constraint. *)
let is_true env =
function
| Cequal (e1, e2) when e1 = e2 ->
((Some true), (Cequal (simplify env e1, simplify env e2)))
| Cequal (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
2010-07-06 11:12:14 +02:00
| (Sconst n1, Sconst n2) -> ((Some (n1 = n2)), (Cequal (e1, e2)))
| (_, _) -> (None, (Cequal (e1, e2))))
| Clequal (e1, e2) ->
let e1 = simplify env e1 in
let e2 = simplify env e2
in
(match (e1, e2) with
2010-07-06 11:12:14 +02:00
| (Sconst n1, Sconst n2) -> ((Some (n1 <= n2)), (Clequal (e1, e2)))
| (_, _) -> (None, (Clequal (e1, e2))))
| Cfalse -> (None, Cfalse)
2010-07-02 15:38:11 +02:00
exception Solve_failed of size_constraint
2010-06-15 10:49:03 +02:00
(** [solve env constr_list solves a list of constraints. It
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. ]*)
let rec solve const_env =
function
| [] -> []
| c :: l ->
let l = solve const_env l in
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-30 17:20:56 +02:00
let rec static_exp_subst m =
function
| Svar n -> (try List.assoc n m with | Not_found -> Svar n)
2010-07-01 19:32:54 +02:00
| Sop (op, e1, e2) -> Sop (op, static_exp_subst m e1, static_exp_subst m e2)
| s -> s
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 =
let replace_one m = function
2010-07-01 19:32:54 +02:00
| Cequal (e1, e2) -> Cequal (static_exp_subst m e1, static_exp_subst m e2)
| Clequal (e1, e2) -> Clequal (static_exp_subst m e1, static_exp_subst m e2)
| Cfalse -> Cfalse
in List.map (replace_one m) constr
let op_to_string =
2010-07-02 15:38:11 +02:00
function | Splus -> "+" | Sminus -> "-" | Stimes -> "*" | Sdiv -> "/"
2010-06-30 17:20:56 +02:00
let rec print_static_exp ff =
function
2010-07-01 19:32:54 +02:00
| SConst i -> fprintf ff "%d" i
| Svar id -> fprintf ff "%s" id
| Sop (op, e1, e2) ->
fprintf ff "@[(%a %s %a)@]"
2010-06-30 17:20:56 +02:00
print_static_exp e1 (op_to_string op) print_static_exp e2
2010-07-02 15:38:11 +02:00
let print_size_constraint ff = function
| Cequal (e1, e2) ->
2010-07-01 19:32:54 +02:00
fprintf ff "@[%a = %a@]" print_static_exp e1 print_static_exp e2
| Clequal (e1, e2) ->
2010-07-01 19:32:54 +02:00
fprintf ff "@[%a <= %a@]" print_static_exp e1 print_static_exp e2
| Cfalse -> fprintf ff "Cfalse"
2010-07-02 15:38:11 +02:00
let psize_constraint oc c =
let ff = formatter_of_out_channel oc
2010-07-02 15:38:11 +02:00
in (print_size_constraint ff c; fprintf ff "@?")