SConst -> Sconst

This commit is contained in:
Léonard Gérard 2010-07-06 11:12:14 +02:00
parent 075cab202a
commit 65c12884bd
8 changed files with 20 additions and 20 deletions

View file

@ -20,7 +20,7 @@ open Format
type op = | Splus | Sminus | Stimes | Sdiv
type size_exp =
| SConst of int | Svar of name | Sop of op * size_exp * size_exp
| Sconst of int | Svar of name | Sop of op * size_exp * size_exp
(** Constraints on size expressions. *)
type size_constraint =
@ -48,14 +48,14 @@ let op_from_app_name n =
that can be computed is replaced with the value of the result. *)
let rec simplify env =
function
| SConst n -> SConst n
| 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
| (SConst n1, SConst n2) ->
| (Sconst n1, Sconst n2) ->
let n =
(match op with
| Splus -> n1 + n2
@ -63,14 +63,14 @@ let rec simplify env =
| Stimes -> n1 * n2
| Sdiv ->
if n2 = 0 then raise Instanciation_failed else n1 / n2)
in SConst n
in Sconst n
| (_, _) -> Sop (op, e1, e2))
(** [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 =
match simplify env e with | SConst n -> n | _ -> raise Instanciation_failed
match simplify env e with | Sconst n -> n | _ -> raise Instanciation_failed
(** [is_true env constr] returns whether the constraint is satisfied
in the environment (or None if this can be decided)
@ -85,14 +85,14 @@ let is_true env =
let e2 = simplify env e2
in
(match (e1, e2) with
| (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Cequal (e1, e2)))
| (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
| (SConst n1, SConst n2) -> ((Some (n1 <= n2)), (Clequal (e1, e2)))
| (Sconst n1, Sconst n2) -> ((Some (n1 <= n2)), (Clequal (e1, e2)))
| (_, _) -> (None, (Clequal (e1, e2))))
| Cfalse -> (None, Cfalse)
@ -134,7 +134,7 @@ let op_to_string =
let rec print_size_exp ff =
function
| SConst i -> fprintf ff "%d" i
| Sconst i -> fprintf ff "%d" i
| Svar id -> fprintf ff "%s" id
| Sop (op, e1, e2) ->
fprintf ff "@[(%a %s %a)@]"

View file

@ -14,7 +14,7 @@ type ty =
let invalid_type = Tprod []
let const_array_of ty n = Tarray (ty, SConst n)
let const_array_of ty n = Tarray (ty, Sconst n)
open Pp_tools
open Format

View file

@ -607,7 +607,7 @@ and typing_array_op statefull h op e_list =
let typed_e2 = expect statefull h (Tid Initial.pint) e2 in
let e2 = size_exp_of_exp e2 in
let typed_e1, t1 = typing statefull h e1 in
add_size_constraint (Clequal (SConst 1, e2));
add_size_constraint (Clequal (Sconst 1, e2));
Tarray (t1, e2), op, [typed_e1; typed_e2]
| Eselect idx_list, [e1] ->
let typed_e1, t1 = typing statefull h e1 in
@ -629,8 +629,8 @@ and typing_array_op statefull h op e_list =
let typed_e, t1 = typing statefull h e in
(*Create the expression to compute the size of the array *)
let e1 = Sop (Sminus, size_exp_of_exp idx2, size_exp_of_exp idx1) in
let e2 = Sop (Splus, e1, SConst 1) in
add_size_constraint (Clequal (SConst 1, e2));
let e2 = Sop (Splus, e1, Sconst 1) in
add_size_constraint (Clequal (Sconst 1, e2));
Tarray (element_type t1, e2), op, [typed_e; typed_idx1; typed_idx2]
| Econcat, [e1; e2] ->
let typed_e1, t1 = typing statefull h e1 in
@ -658,7 +658,7 @@ and typing_array_op statefull h op e_list =
let e = size_exp_of_exp e in
let ty, typed_e_list = typing_iterator statefull h it e
expected_ty_list result_ty_list e_list in
add_size_constraint (Clequal (SConst 1, e));
add_size_constraint (Clequal (Sconst 1, e));
List.iter add_size_constraint size_constrs;
ty, Eiterator(it, { op_desc with op_name = f; op_kind = k }, reset),
typed_e::typed_e_list
@ -718,8 +718,8 @@ and typing_array_subscript statefull h idx_list ty =
match ty, idx_list with
| ty, [] -> ty
| Tarray(ty, exp), idx::idx_list ->
add_size_constraint (Clequal (SConst 0, idx));
add_size_constraint (Clequal (idx, Sop(Sminus, exp, SConst 1)));
add_size_constraint (Clequal (Sconst 0, idx));
add_size_constraint (Clequal (idx, Sop(Sminus, exp, Sconst 1)));
typing_array_subscript statefull h idx_list ty
| _, _ -> error (Esubscripted_value_not_an_array ty)

View file

@ -196,7 +196,7 @@ let op_from_app app =
let rec size_exp_of_exp e =
match e.e_desc with
| Econstvar n -> Svar n
| Econst (Cint i) -> SConst i
| Econst (Cint i) -> Sconst i
| Eapp (app, [ e1; e2 ]) ->
let op = op_from_app app
in Sop (op, size_exp_of_exp e1, size_exp_of_exp e2)

View file

@ -120,7 +120,7 @@ let rec translate_size_exp const_env e = match e.e_desc with
Error.message e.e_loc (Error.Econst_var n)
else
Svar n
| Econst (Cint i) -> SConst i
| Econst (Cint i) -> Sconst i
| Eapp(app, [e1;e2]) ->
let op = op_from_app e.e_loc app in
Sop(op, translate_size_exp const_env e1,

View file

@ -20,7 +20,7 @@ let err_message ?(exp=void) ?(loc=exp.e_loc) = function
let rec size_exp_of_exp e =
match e.e_desc with
| Econstvar n -> Svar n
| Econst (Cint i) -> SConst i
| Econst (Cint i) -> Sconst i
| Ecall(op, [e1;e2], _) ->
let sop = op_from_app_name op.op_name in
Sop(sop, size_exp_of_exp e1, size_exp_of_exp e2)

View file

@ -409,7 +409,7 @@ let translate_node_aux const_env
{ cl_id = f; mem = m; objs = j; reset = si; step = step; }
let build_params_list env params_names params_values =
List.fold_left2 (fun env { p_name = n } v -> NamesEnv.add n (SConst v) env)
List.fold_left2 (fun env { p_name = n } v -> NamesEnv.add n (Sconst v) env)
env params_names params_values
let translate_node const_env n =

View file

@ -32,7 +32,7 @@ let rec node_by_name s = function
node_by_name s l
let build env params_names params_values =
List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n (SConst v) m)
List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n (Sconst v) m)
env params_names params_values
let rec collect_exp nodes env e =