jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Bonjour je suis le nouveau heptgon ! my cute name is heptc.

Browse source
This commit is contained in:
Léonard Gérard 2010-06-15 14:05:26 +02:00
parent c4a6b83fdc
commit e8a3785474
23 changed files with 523 additions and 656 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

68
global/global.ml
View file

@ -1,68 +0,0 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* global data in the symbol tables *)
(* $Id$ *)
open Names
open Ident
open Linearity
open Heptagon
open Static
(** Warning: Whenever these types are modified,
interface_format_version in misc.ml should be incremented. *)
type arg_dec =
{ a_type : ty;
a_name : name option;
a_linearity : linearity;
a_pass_by_ref: bool; }
type sig_desc =
{ inputs : arg_dec list;
outputs : arg_dec list;
contract : contract option;
node : bool;
safe : bool;
targeting : (int*int) list;
params: name list;
params_constraints : size_constr list; }
and field_desc =
{ arg: base_ty; (* if x:arg then x.m: res *)
res: base_ty;
}
and struct_desc =
{ fields : (name * base_ty) list; }
and typ_desc =
| Tabstract
| Tenum of name list
| Tstruct of (name * base_ty) list
type 'a info = { qualid : qualident; info : 'a }
type ivar =
| IVar of ident
| IField of ident * longname
(** [filter_vars l] returns a list of variables identifiers from
a list of ivar.*)
let rec filter_vars = function
| [] -> []
| (IVar id)::l -> id::(filter_vars l)
| _::l -> filter_vars l
let names l =
List.map (fun ad -> ad.a_name) l
let types l =
List.map (fun ad -> ad.a_type) l
let linearities l =
List.map (fun ad -> ad.a_linearity) l

10
global/ident.ml
View file

@ -1,5 +1,15 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* naming and local environment *)
type ident = {
num : int; (* a unique index *)
source : string; (* the original name in the source *)

40
global/ident.mli
View file

@ -1,35 +1,39 @@
(** This modules manages unique identifiers,
[fresh] generates an identifier from a name
[name] returns a unique name from an identifier. *)
(** The (abstract) type of identifiers*)
type ident
type ident
(** Get the source name from an identifier*)
val sourcename : ident -> string
(** Get the full name of an identifier (it is
guaranteed to be unique)*)
(** Get the full name of an identifier (it is guaranteed to be unique) *)
val name : ident -> string
(** [set_sourcename id v] returns id with its
source name changed to v. *)
(** [set_sourcename id v] returns id with its source name changed to v. *)
val set_sourcename : ident -> string -> ident
(** [fresh n] returns a fresh identifier with source name n *)
val fresh : string -> ident
(** [ident_of_var n] returns an identifier corresponding
to a _source_ variable (do not use it for generated variables). *)
to a _source_ variable (do not use it for generated variables). *)
val ident_of_var : string -> ident
(** Maps taking an identifier as a key. *)
module Env :
sig
include (Map.S with type key = ident)
val append : 'a t -> 'a t -> 'a t
val union : 'a t -> 'a t -> 'a t
val diff : 'a t -> 'b t -> 'a t
val partition : (key -> bool) -> 'a t -> 'a t * 'a t
end
sig
include (Map.S with type key = ident)
val append : 'a t -> 'a t -> 'a t
val union : 'a t -> 'a t -> 'a t
val diff : 'a t -> 'b t -> 'a t
val partition : (key -> bool) -> 'a t -> 'a t * 'a t
end
(** A set of identifiers. *)
module IdentSet :
sig
include (Set.S with type elt = ident)
val fprint_t : Format.formatter -> t -> unit
end
sig
include (Set.S with type elt = ident)
val fprint_t : Format.formatter -> t -> unit
end

9
global/initial.ml
View file

@ -8,12 +8,7 @@
(**************************************************************************)
(* initialization of the typing environment *)
(* $Id$ *)
open Misc
open Names
open Global
open Modules
let tglobal = []
let cglobal = []
@ -27,5 +22,5 @@ let pfloat = Modname({ qual = "Pervasives"; id = "float" })
(* build the initial environment *)
let initialize () =
List.iter (fun (f, ty) -> add_type f ty) tglobal;
List.iter (fun (f, ty) -> add_constr f ty) cglobal
List.iter (fun (f, ty) -> Modules.add_type f ty) tglobal;
List.iter (fun (f, ty) -> Modules.add_constr f ty) cglobal

73
global/modules.ml
View file

@ -8,43 +8,41 @@
(**************************************************************************)
(* global symbol tables *)
(* $Id$ *)
open Misc
open Heptagon
open Global
open Signature
open Names
open Types
exception Already_defined
exception Cannot_find_file of string
(** Warning: Whenever this type is modified,
interface_format_version in misc.ml should be incremented. *)
(** Warning: Whenever this type is modified,
interface_format_version in signature.ml should be incremented. *)
type env =
{ mutable name: string;
mutable values: sig_desc NamesEnv.t;
mutable types: typ_desc NamesEnv.t;
mutable constr: base_ty NamesEnv.t;
mutable field: field_desc NamesEnv.t;
mutable structs : struct_desc NamesEnv.t;
mutable values: node NamesEnv.t;
mutable types: type_def NamesEnv.t;
mutable constr: ty NamesEnv.t;
mutable structs : structure NamesEnv.t;
format_version : string;
}
type modules =
{ current: env; (* associated symbol table *)
mutable opened: env list; (* opened tables *)
mutable modules: env NamesEnv.t; (* tables loaded in memory *)
}
let current =
{ name = ""; values = NamesEnv.empty; types = NamesEnv.empty;
constr = NamesEnv.empty; field = NamesEnv.empty; structs = NamesEnv.empty;
let current =
{ name = ""; values = NamesEnv.empty; types = NamesEnv.empty;
constr = NamesEnv.empty; structs = NamesEnv.empty;
format_version = interface_format_version }
let modules =
let modules =
{ current = current; opened = []; modules = NamesEnv.empty }
let findfile filename =
if Sys.file_exists filename then
filename
@ -58,7 +56,7 @@ let findfile filename =
let b = Filename.concat a filename in
if Sys.file_exists b then b else find rest
in find !load_path
let load_module modname =
let name = String.uncapitalize modname in
try
@ -85,7 +83,7 @@ let load_module modname =
Printf.eprintf "Cannot find the compiled interface file %s.\n"
filename;
raise Error
let find_module modname =
try
NamesEnv.find modname modules.modules
@ -94,7 +92,10 @@ let find_module modname =
let m = load_module modname in
modules.modules <- NamesEnv.add modname m modules.modules;
m
type 'a info = { qualid : qualident; info : 'a }
let find where qualname =
let rec findrec ident = function
| [] -> raise Not_found
@ -102,44 +103,40 @@ let find where qualname =
try { qualid = { qual = m.name; id = ident };
info = where ident m }
with Not_found -> findrec ident l in
match qualname with
| Modname({ qual = m; id = ident } as q) ->
| Modname({ qual = m; id = ident } as q) ->
let current = if current.name = m then current else find_module m in
{ qualid = q; info = where ident current }
| Name(ident) -> findrec ident (current :: modules.opened)
(* exported functions *)
let open_module modname =
let m = find_module modname in
modules.opened <- m :: modules.opened
let initialize modname =
let initialize modname =
current.name <- modname;
List.iter open_module !default_used_modules
let add_value f signature =
let add_value f signature =
if NamesEnv.mem f current.values then raise Already_defined;
current.values <- NamesEnv.add f signature current.values
let add_type f typ_desc =
let add_type f type_def =
if NamesEnv.mem f current.types then raise Already_defined;
current.types <- NamesEnv.add f typ_desc current.types
current.types <- NamesEnv.add f type_def current.types
let add_constr f ty_res =
if NamesEnv.mem f current.constr then raise Already_defined;
current.constr <- NamesEnv.add f ty_res current.constr
let add_field f ty_arg ty_res =
if NamesEnv.mem f current.field then raise Already_defined;
current.field <- NamesEnv.add f { arg = ty_arg; res = ty_res } current.field
let add_struct f fields =
if NamesEnv.mem f current.structs then raise Already_defined;
current.structs <- NamesEnv.add f { fields = fields } current.structs
current.structs <- NamesEnv.add f fields current.structs
let find_value = find (fun ident m -> NamesEnv.find ident m.values)
let find_type = find (fun ident m -> NamesEnv.find ident m.types)
let find_constr = find (fun ident m -> NamesEnv.find ident m.constr)
let find_field = find (fun ident m -> NamesEnv.find ident m.field)
let find_struct = find (fun ident m -> NamesEnv.find ident m.structs)
let replace_value f signature =
current.values <- NamesEnv.remove f current.values;
current.values <- NamesEnv.add f signature current.values
@ -150,6 +147,6 @@ let longname n = Modname({ qual = current.name; id = n })
let currentname longname =
match longname with
| Name(n) -> longname
| Modname{ qual = q; id = id} ->
| Modname{ qual = q; id = id} ->
if current.name = q then Name(id) else longname

7
global/names.ml
View file

@ -1,4 +1,6 @@
(* long identifiers *)
(** Define qualified names "Module.name" (longname)
[shortname] longname -> name
[fullname] longname -> Module.name *)
type name = string
@ -23,6 +25,7 @@ end
module S = Set.Make (struct type t = string let compare = compare end)
let shortname = function
| Name s -> s
| Modname { id = id; } -> id
@ -38,4 +41,4 @@ let mk_longname s =
Modname { qual = String.sub s 0 ind; id = id; }
with Not_found -> Name s
let fprint_t ff id = Format.fprintf ff "%s" (fullname id)
let print_longname ff id = Format.fprintf ff "%s" (fullname id)

38
global/signature.ml Normal file
View file

@ -0,0 +1,38 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* global data in the symbol tables *)
open Names
open Types
open Static
(** Warning: Whenever these types are modified,
interface_format_version should be incremented. *)
let interface_format_version = "6"
(** Node argument *)
type arg = { a_type : ty; a_name : name option }
type param = { p_name : name }
(** Node signature *)
type node =
{ node_inputs : arg list;
node_outputs : arg list;
node_params : param list; (** Static parameters *)
node_params_constraints : size_constr list }
type structure = (name * ty) list
type type_def = | Tabstract | Tenum of name list | Tstruct of structure
let names_of_arg_list l = List.map (fun ad -> ad.a_name) l
let types_of_arg_list l = List.map (fun ad -> ad.a_type) l

242
global/static.ml
View file

@ -1,176 +1,164 @@
(** 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],...
(** 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],...
*)
open Names
open Format
type op = SPlus | SMinus | STimes | SDiv
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_constr =
| Equal of size_exp * size_exp (* e1 = e2*)
| LEqual of size_exp * size_exp (* e1 <= e2 *)
| False (* unsatisfiable constraint *)
| False
exception Instanciation_failed
(* unsatisfiable constraint *)
exception Instanciation_failed
exception Not_static
(** Returns the op from an operator full name. *)
let op_from_app_name n =
match n with
| 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
| 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
(** [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
let rec simplify env =
function
| SConst n -> SConst n
| SVar id ->
(try
simplify env (NamesEnv.find id env)
with
_ -> SVar id
)
| SOp(op, e1, e2) ->
| 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 ->
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)
)
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))
(** [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)
and a simplified constraint. *)
let is_true env = function
| Equal (e1,e2) when e1 = e2 ->
Some true, Equal (simplify env e1, simplify env e2)
let is_true env =
function
| Equal (e1, e2) when e1 = e2 ->
((Some true), (Equal (simplify env e1, simplify env e2)))
| Equal (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), Equal (e1,e2)
| _, _ -> None, Equal (e1,e2)
)
let e2 = simplify env e2
in
(match (e1, e2) with
| (SConst n1, SConst n2) -> ((Some (n1 = n2)), (Equal (e1, e2)))
| (_, _) -> (None, (Equal (e1, e2))))
| LEqual (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), LEqual (e1,e2)
| _, _ -> None, LEqual (e1,e2)
)
| False -> None, False
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)
exception Solve_failed of size_constr
(** [solve env constr_list solves a list of constraints. It
removes equations that can be decided and simplify others.
removes equations that can be decided and simplify others.
If one equation cannot be satisfied, it raises Solve_failed. ]*)
let rec solve const_env = function
let rec solve const_env =
function
| [] -> []
| c::l ->
| 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
)
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)
(** Substitutes variables in the size exp with their value
in the map (mapping vars to size exps). *)
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)
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)
| s -> s
(** 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
| 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)
in
List.map (replace_one m) constr
let op_to_string = function
| SPlus -> "+"
| SMinus -> "-"
| STimes -> "*"
| SDiv -> "/"
let rec print_size_exp ff = function
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
| SConst i -> fprintf ff "%d" i
| SVar id -> fprintf ff "%s" id
| SOp (op, e1, e2) ->
fprintf ff "@[(";
print_size_exp ff e1;
fprintf ff " %s " (op_to_string op);
print_size_exp ff e2;
fprintf ff ")@]"
(fprintf ff "@[(";
print_size_exp ff e1;
fprintf ff " %s " (op_to_string op);
print_size_exp ff e2;
fprintf ff ")@]")
let rec print_list ff print sep l =
match l with
| [] -> ()
| [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"
| [] -> ()
| [ 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"
let psize_constr oc c =
let ff = formatter_of_out_channel oc in
print_size_constr ff c; fprintf ff "@?"
let ff = formatter_of_out_channel oc
in (print_size_constr ff c; fprintf ff "@?")

17
global/types.ml Normal file
View file

@ -0,0 +1,17 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
open Static
open Names
type ty =
| Tprod of ty list | Tid of longname | Tarray of ty * size_exp
let const_array_of ty n = Tarray (ty, SConst n)

2
heptagon/analysis/interface.ml
View file

@ -83,7 +83,7 @@ struct
print_list ff
(fun ff (field, ty) -> print_name ff field;
fprintf ff ": ";
print_base_type ff ty) ";" f_ty_list;
print_type ff ty) ";" f_ty_list;
fprintf ff "}@]@.@]"
let signature ff name { inputs = inputs;

34
heptagon/analysis/typing.ml
View file

@ -139,8 +139,8 @@ let message loc kind =
let add_value f signature =
try add_value f signature with Already_defined -> error (Ealready_defined f)
let add_type f typ_desc =
try add_type f typ_desc with Already_defined -> error (Ealready_defined f)
let add_type f type_def =
try add_type f type_def with Already_defined -> error (Ealready_defined f)
let add_constr f ty_res =
try add_constr f ty_res with Already_defined -> error (Ealready_defined f)
let add_field f ty_arg ty_res =
@ -223,17 +223,17 @@ let prod = function
| ty_list -> Tprod(ty_list)
let rec typing_const c =
let typed_c, base_ty = match c with
let typed_c, ty = match c with
| Cint _ -> c, Tid(pint)
| Cfloat _ -> c, Tid(pfloat)
| Cconstr(c) ->
let { qualid = q; info = base_ty } = find_constr c in
Cconstr(Modname(q)), base_ty
| Cconst_array(n, c) ->
let { qualid = q; info = ty } = find_constr c in
Cconstr(Modname(q)), ty
| Carray(n, c) ->
let c, ty = typing_const c in
Cconst_array(n,c), Tarray(base_type ty, n)
Carray(n,c), Tarray(type ty, n)
in
typed_c, Tbase(base_ty)
typed_c, Tbase(ty)
let typ_of_name h x =
try
@ -294,12 +294,12 @@ let simplify_type loc const_env ty =
with
Instanciation_failed -> message loc (Etype_should_be_static (Tbase ty))
let rec subst_base_type_vars m = function
| Tarray(ty, e) -> Tarray(subst_base_type_vars m ty, size_exp_subst m e)
let rec subst_type_vars m = function
| Tarray(ty, e) -> Tarray(subst_type_vars m ty, size_exp_subst m e)
| t -> t
let rec subst_type_vars m = function
| Tbase ty -> Tbase (subst_base_type_vars m ty)
| Tbase ty -> Tbase (subst_type_vars m ty)
| Tprod l -> Tprod (List.map (subst_type_vars m) l)
let equal expected_tag_list actual_tag_list =
@ -492,8 +492,8 @@ and typing_app statefull h op e_list =
ty, op, typed_e1::typed_defe::typed_idx_list
| Eupdate idx_list, [e1;e2] ->
let typed_e1, t1 = typing statefull h e1 in
let base_ty = typing_array_subscript statefull h idx_list t1 in
let typed_e2 = expect statefull h base_ty e2 in
let ty = typing_array_subscript statefull h idx_list t1 in
let typed_e2 = expect statefull h ty e2 in
t1, op, [typed_e1; typed_e2]
| Eselect_slice, [e; idx1; idx2] ->
let typed_idx1 = expect statefull h (Tbase(Tint)) idx1 in
@ -612,10 +612,10 @@ and typing_iterator statefull h it n args_ty_list result_ty_list e_list =
and typing_array_subscript statefull h idx_list ty =
match ty, idx_list with
| ty, [] -> ty
| Tbase(Tarray(base_ty, exp)), idx::idx_list ->
| Tbase(Tarray(ty, exp)), idx::idx_list ->
add_size_constr (LEqual (SConst 0, idx));
add_size_constr (LEqual (idx, SOp(SMinus, exp, SConst 1)));
typing_array_subscript statefull h idx_list (Tbase base_ty)
typing_array_subscript statefull h idx_list (Tbase ty)
| _, _ -> error (Esubscripted_value_not_an_array ty)
(* This function checks that the array dimensions matches
@ -623,10 +623,10 @@ and typing_array_subscript statefull h idx_list ty =
and typing_array_subscript_dyn statefull h idx_list ty =
match ty, idx_list with
| ty, [] -> ty, []
| Tbase(Tarray(base_ty, exp)), idx::idx_list ->
| Tbase(Tarray(ty, exp)), idx::idx_list ->
let typed_idx = expect statefull h (Tbase(Tint)) idx in
let ty, typed_idx_list =
typing_array_subscript_dyn statefull h idx_list (Tbase base_ty) in
typing_array_subscript_dyn statefull h idx_list (Tbase ty) in
ty, typed_idx::typed_idx_list
| _, _ -> error (Esubscripted_value_not_an_array ty)

461
heptagon/heptagon.ml
View file

@ -7,37 +7,23 @@
(* *)
(**************************************************************************)
(* the internal representation *)
(* $Id$ *)
open Location
open Misc
open Names
open Linearity
open Ident
open Interference_graph
open Ident
open Static
open Signature
type inlining_policy =
| Ino
| Ione
| Irec
type ty =
| Tbase of base_ty
| Tprod of ty list
type iterator_name =
| Imap
| Ifold
| Imapfold
and base_ty =
| Tint | Tfloat | Tbool
| Tid of longname
| Tarray of base_ty * size_exp
type exp =
{ e_desc : desc; e_ty : ty; e_loc : location }
and exp =
{ e_desc: desc;
mutable e_ty: ty;
mutable e_linearity : linearity;
e_loc: location }
and desc =
and desc =
| Econst of const
| Evar of ident
| Econstvar of name
@ -47,324 +33,225 @@ and desc =
| Efield of exp * longname
| Estruct of (longname * exp) list
| Earray of exp list
| Ereset_mem of ident * exp * ident
and app =
{ mutable a_op : op; (* hange of global name after typing *)
a_inlined : inlining_policy; (* node to inline or not *)
}
and app =
{ a_op : op; }
and op =
and op =
| Epre of const option
| Efby | Earrow | Eifthenelse | Enode of longname * size_exp list
| Eevery of longname * size_exp list | Eop of longname * size_exp list
| Erepeat | Eselect of size_exp list | Eselect_dyn
| Efby
| Earrow
| Eifthenelse
| Earray_op of array_op
| Ecall of op_desc * exp option (** [op_desc] is the function called
[exp option] is the optional reset condition *)
and array_op =
| Erepeat
| Eselect of size_exp list
| Eselect_dyn
| Eupdate of size_exp list
| Eselect_slice
| Econcat | Ecopy
| Eiterator of iterator_name * longname * size_exp list * exp option
| Efield_update of longname
| Eflatten of longname | Emake of longname
| Econcat
| Eiterator of iterator_name * op_desc * exp option
and op_desc = longname * size_exp list * op_kind
and op_kind = | Eop | Enode
and const =
and const =
| Cint of int
| Cfloat of float
| Cconstr of longname
| Cconst_array of size_exp * const
| Carray of size_exp * const
and pat =
| Etuplepat of pat list
| Evarpat of ident
and pat =
| Etuplepat of pat list | Evarpat of ident
type eq =
{ eq_desc : eqdesc;
mutable eq_statefull : bool;
eq_loc : location }
{ eq_desc : eqdesc; eq_statefull : bool; eq_loc : location }
and eqdesc =
and eqdesc =
| Eautomaton of state_handler list
| Eswitch of exp * switch_handler list
| Epresent of present_handler list * block
| Ereset of eq list * exp
| Eeq of pat * exp
and block =
{ b_local: var_dec list;
b_equs: eq list;
mutable b_defnames: ty Env.t;
mutable b_statefull: bool;
b_loc: location; }
and block =
{ b_local : var_dec list; b_equs : eq list; mutable b_defnames : ty Env.t;
mutable b_statefull : bool; b_loc : location
}
and state_handler =
{ s_state : name;
s_block : block;
s_until : escape list;
s_unless : escape list; }
and state_handler =
{ s_state : name; s_block : block; s_until : escape list;
s_unless : escape list
}
and escape =
{ e_cond : exp;
e_reset : bool;
e_next_state : name; }
and escape =
{ e_cond : exp; e_reset : bool; e_next_state : name
}
and switch_handler =
{ w_name : longname;
w_block : block; }
and switch_handler =
{ w_name : longname; w_block : block
}
and present_handler =
{ p_cond : exp;
p_block : block; }
and present_handler =
{ p_cond : exp; p_block : block
}
and var_dec =
{ v_name : ident;
mutable v_type : base_ty;
mutable v_linearity : linearity;
v_last : last;
v_loc : location; }
and var_dec =
{ v_name : ident; mutable v_type : ty; v_last : last; v_loc : location }
and last = Var | Last of const option
and last =
| Var | Last of const option
type type_dec =
{ t_name : name;
t_desc : type_desc;
t_loc : location }
{ t_name : name; t_desc : type_desc; t_loc : location }
and type_desc =
| Type_abs
| Type_enum of name list
| Type_struct of (name * base_ty) list
and type_desc =
| Type_abs | Type_enum of name list | Type_struct of structure
type contract =
{ c_assume : exp;
c_enforce : exp;
c_controllables : var_dec list;
c_local : var_dec list;
c_eq : eq list;
}
{ c_assume : exp; c_enforce : exp; c_controllables : var_dec list;
c_local : var_dec list; c_eq : eq list
}
type node_dec =
{ n_name : name;
n_statefull : bool;
n_input : var_dec list;
n_output : var_dec list;
n_local : var_dec list;
n_contract : contract option;
n_equs : eq list;
n_loc : location;
n_states_graph : (name,name) interf_graph;
n_params : name list;
n_params_constraints : size_constr list;
}
{ n_name : name; n_statefull : bool; n_input : var_dec list;
n_output : var_dec list; n_local : var_dec list;
n_contract : contract option; n_equs : eq list; n_loc : location;
n_params : name list;
n_params_constraints : size_constr list
}
type const_dec =
{ c_name : name;
c_type : base_ty;
c_value : size_exp;
c_loc : location; }
{ c_name : name; c_type : ty; c_value : size_exp; c_loc : location }
type program =
{ p_pragmas: (name * string) list;
p_opened : name list;
p_types : type_dec list;
p_nodes : node_dec list;
p_consts : const_dec list; }
{ p_pragmas : (name * string) list; p_opened : name list;
p_types : type_dec list; p_nodes : node_dec list;
p_consts : const_dec list
}
type signature =
{ sig_name : name;
sig_inputs : (name option * base_ty * linearity) list;
sig_outputs : (name option * base_ty * linearity) list;
sig_node : bool;
sig_safe : bool;
sig_params : name list; }
{ sig_name : name; sig_inputs : arg list;
sig_outputs : arg list; sig_params : param list
}
type interface = interface_decl list
type interface =
interface_decl list
and interface_decl =
{ interf_desc : interface_desc;
interf_loc : location }
and interface_desc =
| Iopen of name
| Itypedef of type_dec
| Isignature of signature
let tbool = Tbool
and interface_decl =
{ interf_desc : interface_desc; interf_loc : location
}
and interface_desc =
| Iopen of name | Itypedef of type_dec | Isignature of signature
let edesc e = e.e_desc
let eqdesc eq = eq.eq_desc
(* Helper functions to create AST. *) (*TODO refactor en mk_*)
(* Helper functions to create AST. *)
let pbool = Modname({ qual = "Pervasives"; id = "bool" })
let ptrue = Modname({ qual = "Pervasives"; id = "true" })
let pfalse = Modname({ qual = "Pervasives"; id = "false" })
let por = Modname({ qual = "Pervasives"; id = "or" })
let pint = Modname({ qual = "Pervasives"; id = "int" })
let pfloat = Modname({ qual = "Pervasives"; id = "float" })
let emake desc ty = { e_desc = desc; e_ty = ty;
e_linearity = NotLinear; e_loc = no_location }
let eop op = { a_op = op; a_inlined = Ino }
let tmake name desc = { t_name = name; t_desc = desc; t_loc = no_location }
let eqmake desc = { eq_desc = desc; eq_statefull = true; eq_loc = no_location }
let tybool = Tbase(tbool)
let cfalse = Cconstr(pfalse)
let ctrue = Cconstr(ptrue)
let emake desc ty =
{ e_desc = desc; e_ty = ty; e_linearity = NotLinear; e_loc = no_location; }
let eop op = { a_op = op; a_inlined = Ino; }
let tmake name desc = { t_name = name; t_desc = desc; t_loc = no_location; }
let eqmake desc =
{ eq_desc = desc; eq_statefull = true; eq_loc = no_location; }
let tybool = Tbase tbool
let cfalse = Cconstr pfalse
let ctrue = Cconstr ptrue
let make_bool desc = emake desc tybool
let bool_var n = make_bool (Evar(n))
let bool_var n = make_bool (Evar n)
let bool_param n =
{ v_name = n; v_type = tbool; v_last = Var;
v_loc = no_location; v_linearity = NotLinear }
let dfalse = make_bool (Econst(Cconstr(pfalse)))
let dtrue = make_bool (Econst(Cconstr(ptrue)))
let var n ty = emake (Evar(n)) ty
{
v_name = n;
v_type = tbool;
v_last = Var;
v_loc = no_location;
v_linearity = NotLinear;
}
let dfalse = make_bool (Econst (Cconstr pfalse))
let dtrue = make_bool (Econst (Cconstr ptrue))
let var n ty = emake (Evar n) ty
let param n ty =
{ v_name = n; v_type = ty; v_linearity = NotLinear;
v_last = Var; v_loc = no_location }
{
v_name = n;
v_type = ty;
v_linearity = NotLinear;
v_last = Var;
v_loc = no_location;
}
let fby_state initial e =
{ e with e_desc = Eapp(eop (Epre(Some(Cconstr initial))), [e]) }
let fby_false e = emake (Eapp(eop (Epre(Some(cfalse))), [e])) tybool
let last_false x = emake (Elast(x)) tybool
let ifthenelse e1 e2 e3 = emake (Eapp(eop Eifthenelse, [e1;e2;e3])) e2.e_ty
let rec or_op e1 e2 = { e1 with e_desc = Eapp(eop (Eop(por, [])), [e1; e2]) }
let pair e1 e2 = emake (Etuple([e1;e2])) (Tprod [e1.e_ty;e2.e_ty])
{ (e) with e_desc = Eapp (eop (Epre (Some (Cconstr initial))), [ e ]); }
let fby_false e = emake (Eapp (eop (Epre (Some cfalse)), [ e ])) tybool
let last_false x = emake (Elast x) tybool
let ifthenelse e1 e2 e3 =
emake (Eapp (eop Eifthenelse, [ e1; e2; e3 ])) e2.e_ty
let rec or_op e1 e2 =
{ (e1) with e_desc = Eapp (eop (Eop (por, [])), [ e1; e2 ]); }
let pair e1 e2 = emake (Etuple [ e1; e2 ]) (Tprod [ e1.e_ty; e2.e_ty ])
let block defnames eqs =
{ b_local = []; b_equs = eqs; b_defnames = defnames;
b_statefull = true; b_loc = no_location }
let eq pat e = eqmake (Eeq(pat, e))
let reset eq_list e = eqmake (Ereset(eq_list, e))
let switch e l = eqmake (Eswitch(e, l))
let varpat n = Evarpat(n)
(* Helper functions to work with type*)
let base_type ty =
match ty with
| Tbase ty -> ty
| _ -> assert false
let is_scalar_type ty =
let pint = Modname({ qual = "Pervasives"; id = "int" }) in
let pfloat = Modname({ qual = "Pervasives"; id = "float" }) in
let pbool = Modname({ qual = "Pervasives"; id = "bool" }) in
match ty with
| Tbase(Tint) | Tbase(Tfloat) | Tbase(Tbool) -> true
| Tbase(Tid name_int) when name_int = pint -> true
| Tbase(Tid name_float) when name_float = pfloat -> true
| Tbase(Tid name_bool) when name_bool = pbool -> true
| _ -> false
let array_of ty exp =
Tbase(Tarray (base_type ty, exp))
let const_array_of ty n =
array_of ty (SConst n)
{
b_local = [];
b_equs = eqs;
b_defnames = defnames;
b_statefull = true;
b_loc = no_location;
}
let eq pat e = eqmake (Eeq (pat, e))
let reset eq_list e = eqmake (Ereset (eq_list, e))
let switch e l = eqmake (Eswitch (e, l))
let varpat n = Evarpat n
let op_from_app app =
match app.a_op with
| Eop (n,_) -> op_from_app_name n
| _ -> raise Not_static
| Eop (n, _) -> op_from_app_name n
| _ -> raise Not_static
let rec size_exp_of_exp e =
match e.e_desc with
match e.e_desc with
| Econstvar n -> SVar n
| 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)
| Eapp (app, ([ e1; e2 ])) ->
let op = op_from_app app
in SOp (op, size_exp_of_exp e1, size_exp_of_exp e2)
| _ -> raise Not_static
module Vars =
struct
let rec vars_pat locals acc = function
| Evarpat(x) ->
if (IdentSet.mem x locals) or (IdentSet.mem x acc) then
acc
else
IdentSet.add x acc
| Etuplepat(pat_list) -> List.fold_left (vars_pat locals) acc pat_list
(** @return the set of variables defined in [pat]. *)
let vars_pat pat =
let rec _vars_pat locals acc = function
| Evarpat x ->
if (IdentSet.mem x locals) or (IdentSet.mem x acc)
then acc
else IdentSet.add x acc
| Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
in _vars_pat IdentSet.empty IdentSet.empty pat
let rec left locals acc e =
match e.e_desc with
| Eapp({a_op = Epre _},[e]) -> acc
| Eapp({a_op = Efby}, [e1;e2]) -> left locals acc e1
| Etuple(e_list) | Eapp({a_op = _}, e_list) | Earray(e_list)->
List.fold_left (left locals) acc e_list
| Evar(n) | Ereset_mem (_, _, n) ->
if (IdentSet.mem n acc) or (IdentSet.mem n locals) then
acc
else
IdentSet.add n acc
| Efield(e, _) -> left locals acc e
| Estruct(f_e_list) ->
List.fold_left (fun acc (_, e) -> left locals acc e) acc f_e_list
| Elast _ | Econst _ | Econstvar _ -> acc
let rec read locals acc eq =
match eq.eq_desc with
| Eeq(pat, e) -> left locals acc e
| Ereset(eq_list, e) ->
List.fold_left (read locals) (left locals acc e) eq_list
| Eautomaton(state_handlers) ->
let escapes locals acc e_list =
List.fold_left
(fun acc { e_cond = e } -> left locals acc e) acc e_list in
List.fold_left
(fun acc {s_block = b; s_until = e_list1; s_unless = e_list2} ->
let new_locals, acc = read_and_locals_block locals acc b in
let acc = escapes new_locals acc e_list1 in
escapes locals acc e_list2)
acc state_handlers
| Eswitch(e, switch_handlers) ->
List.fold_left
(fun acc { w_block = b } -> read_block locals acc b)
(left locals acc e) switch_handlers
| Epresent(present_handlers, b) ->
List.fold_left
(fun acc { p_cond = e; p_block = b } ->
read_block locals (left locals acc e) b)
(read_block locals acc b) present_handlers
and read_and_locals_block locals acc { b_local = l; b_equs = eq_list } =
let locals =
List.fold_left
(fun acc { v_name = n } -> if IdentSet.mem n acc then acc else IdentSet.add n acc)
locals l in
locals, List.fold_left (read locals) acc eq_list
and read_block locals acc b =
let _, acc = read_and_locals_block locals acc b in acc
let rec def locals acc eq =
match eq.eq_desc with
| Eeq(pat, _) -> vars_pat locals acc pat
| Eautomaton(state_handler) ->
List.fold_left
(fun acc { s_block = b } ->
def_block locals acc b) acc state_handler
| Eswitch(_, switch_handler) ->
List.fold_left
(fun acc { w_block = b } ->
def_block locals acc b) acc switch_handler
| Epresent(present_handler, b) ->
List.fold_left
(fun acc { p_block = b } -> def_block locals acc b)
(def_block locals acc b) present_handler
| Ereset(eq_list, _) -> def_list locals acc eq_list
and def_block locals acc ({ b_local = l; b_equs = eq_list }) =
let locals =
List.fold_left
(fun acc { v_name = n } -> if IdentSet.mem n acc then acc else IdentSet.add n acc)
locals l in
def_list locals acc eq_list
and def_list locals acc def_list = List.fold_left (def locals) acc def_list
let read eq = IdentSet.elements (read IdentSet.empty IdentSet.empty eq)
let def eq = IdentSet.elements (def IdentSet.empty IdentSet.empty eq)
let antidep eq = false
let vars_list pat = IdentSet.elements (vars_pat IdentSet.empty IdentSet.empty pat)
end

12
heptagon/parsing/scoping.ml
View file

@ -128,7 +128,7 @@ let rec translate_type const_env = function
Heptagon.Tprod(List.map (translate_type const_env) ty_list)
| Tid ln -> Heptagon.Tbase (Heptagon.Tid ln)
| Tarray (ty, e) ->
let ty = Heptagon.base_type (translate_type const_env ty) in
let ty = Heptagon.type (translate_type const_env ty) in
Heptagon.Tbase (Heptagon.Tarray (ty, translate_size_exp const_env e))
and translate_exp const_env env e =
@ -178,7 +178,7 @@ and translate_desc loc const_env env = function
let e_list = List.map (translate_exp const_env env) e_list in
(match e_list with
| [{ Heptagon.e_desc = Heptagon.Econst c }; e1 ] ->
Heptagon.Econst (Heptagon.Cconst_array (Heptagon.size_exp_of_exp e1, c))
Heptagon.Econst (Heptagon.Carray (Heptagon.size_exp_of_exp e1, c))
| _ -> Heptagon.Eapp (translate_app const_env env app, e_list)
)
| Eapp (app, e_list) ->
@ -244,7 +244,7 @@ and translate_switch_handler loc const_env env sh =
and translate_var_dec const_env env vd =
{ Heptagon.v_name = Rename.name vd.v_loc env vd.v_name;
Heptagon.v_type = Heptagon.base_type (translate_type const_env vd.v_type);
Heptagon.v_type = Heptagon.type (translate_type const_env vd.v_type);
Heptagon.v_linearity = vd.v_linearity;
Heptagon.v_last = translate_last env vd.v_last;
Heptagon.v_loc = vd.v_loc }
@ -285,7 +285,7 @@ let translate_typedec const_env ty =
| Type_enum(tag_list) -> Heptagon.Type_enum(tag_list)
| Type_struct(field_ty_list) ->
let translate_field_type (f,ty) =
f, Heptagon.base_type (translate_type const_env ty)
f, Heptagon.type (translate_type const_env ty)
in
Heptagon.Type_struct (List.map translate_field_type field_ty_list)
in
@ -295,7 +295,7 @@ let translate_typedec const_env ty =
let translate_const_dec const_env cd =
{ Heptagon.c_name = cd.c_name;
Heptagon.c_type = Heptagon.base_type (translate_type const_env cd.c_type);
Heptagon.c_type = Heptagon.type (translate_type const_env cd.c_type);
Heptagon.c_value = translate_size_exp const_env cd.c_value;
Heptagon.c_loc = cd.c_loc; }
@ -309,7 +309,7 @@ let translate_program p =
let translate_signature const_env s =
let translate_field_type (f,(ty,lin)) =
f, Heptagon.base_type (translate_type const_env ty), lin
f, Heptagon.type (translate_type const_env ty), lin
in
let const_env = build_id_list no_location const_env s.sig_params in

23
heptagon/printer.ml
View file

@ -19,6 +19,15 @@ open Modules
open Static
open Format
let iterator_to_string i =
match i with
| Imap -> "map"
| Ifold -> "fold"
| Imapfold -> "mapfold"
let rec print_list ff print sep l =
match l with
| [] -> ()
@ -69,18 +78,18 @@ let rec print_pat ff = function
print_list ff print_pat "," pat_list;
fprintf ff ")@]"
let rec print_base_type ff = function
let rec print_type ff = function
| Tint -> fprintf ff "int"
| Tbool -> fprintf ff "bool"
| Tfloat -> fprintf ff "float"
| Tid(id) -> print_longname ff id
| Tarray(ty, e) ->
print_base_type ff ty;
print_type ff ty;
fprintf ff "^";
print_size_exp ff e;
and print_type ff = function
| Tbase(base_ty) -> print_base_type ff base_ty
| Tbase(ty) -> print_type ff ty
| Tprod(ty_list) ->
fprintf ff "@[(";
print_list ff print_type " *" ty_list;
@ -90,7 +99,7 @@ and print_c ff = function
| Cint i -> fprintf ff "%d" i
| Cfloat f -> fprintf ff "%f" f
| Cconstr(tag) -> print_longname ff tag
| Cconst_array (n, c) ->
| Carray (n, c) ->
print_c ff c;
fprintf ff "^";
print_size_exp ff n
@ -100,7 +109,7 @@ and print_vd ff { v_name = n; v_type = ty; v_last = last } =
begin match last with Last _ -> fprintf ff "last " | _ -> () end;
print_ident ff n;
fprintf ff ": ";
print_base_type ff ty;
print_type ff ty;
begin
match last with Last(Some(v)) -> fprintf ff "= ";print_c ff v
| _ -> ()
@ -378,14 +387,14 @@ let print_type_def ff { t_name = name; t_desc = tdesc } =
(fun ff (field, ty) ->
print_name ff field;
fprintf ff ": ";
print_base_type ff ty) ";" f_ty_list;
print_type ff ty) ";" f_ty_list;
fprintf ff "}@]@.@]"
let print_const_dec ff c =
fprintf ff "@[const ";
print_name ff c.c_name;
fprintf ff " : ";
print_base_type ff c.c_type;
print_type ff c.c_type;
fprintf ff " = ";
print_size_exp ff c.c_value;
fprintf ff "@.@]"

16
main/hept2mls.ml
View file

@ -75,7 +75,7 @@ let equation locals l_eqs e =
let n = Ident.fresh "ck" in
n,
{ v_name = n; v_copy_of = None;
v_type = exp_base_type e; v_linearity = NotLinear; v_clock = Cbase } :: locals,
v_type = exp_type e; v_linearity = NotLinear; v_clock = Cbase } :: locals,
{ p_lhs = Evarpat(n); p_rhs = e } :: l_eqs
(* inserts the definition [x,e] into the set of shared equations *)
@ -190,7 +190,7 @@ let rec const = function
| Heptagon.Cint i -> Cint i
| Heptagon.Cfloat f -> Cfloat f
| Heptagon.Cconstr t -> Cconstr t
| Heptagon.Cconst_array(n, c) -> Cconst_array(n, const c)
| Heptagon.Carray(n, c) -> Carray(n, const c)
open Format
@ -221,7 +221,7 @@ let application env { Heptagon.a_op = op; Heptagon.a_inlined = inlined } e_list
store the bounds (which will be used at code generation time, where the types
are harder to find). *)
| Heptagon.Eselect_dyn, e::defe::idx_list ->
let bounds = bounds_list (exp_base_type e) in
let bounds = bounds_list (exp_type e) in
Eselect_dyn (idx_list, bounds,
e, defe)
| Heptagon.Eupdate idx_list, [e1;e2] ->
@ -304,14 +304,14 @@ let rec translate_pat = function
| Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
let rec rename_pat ni locals s_eqs = function
| Heptagon.Evarpat(n), Heptagon.Tbase(base_ty) ->
| Heptagon.Evarpat(n), Heptagon.Tbase(ty) ->
if IdentSet.mem n ni then
let n_copy = Ident.fresh (sourcename n) in
let base_ty = translate_btype base_ty in
let ty = translate_btype ty in
Evarpat(n_copy),
{ v_name = n_copy; v_copy_of = None;
v_type = base_ty; v_linearity = NotLinear; v_clock = Cbase } :: locals,
add n (make_exp (Evar n_copy) (Tbase(base_ty)) NotLinear Cbase no_location)
v_type = ty; v_linearity = NotLinear; v_clock = Cbase } :: locals,
add n (make_exp (Evar n_copy) (Tbase(ty)) NotLinear Cbase no_location)
s_eqs
else Evarpat n, locals, s_eqs
| Heptagon.Etuplepat(l), Heptagon.Tprod(l_ty) ->
@ -325,7 +325,7 @@ let rec rename_pat ni locals s_eqs = function
| _ -> assert false
let all_locals ni p =
IdentSet.is_empty (IdentSet.inter (Heptagon.Vars.vars_pat IdentSet.empty IdentSet.empty p) ni)
IdentSet.is_empty (IdentSet.inter (Heptagon.vars_pat p) ni)
let rec translate_eq env ni (locals, l_eqs, s_eqs) eq =
match Heptagon.eqdesc eq with

53
minils/minils.ml
View file

@ -21,11 +21,10 @@ open Interference_graph
open Global
open Static
(** Inlining policies, to be held in app records. *)
type inlining_policy =
| Ino (** Do not inline. *)
| Ione (** Just inline on one step. *)
| Irec (** Recursively inline all sub-calls. *)
type iterator_name =
| Imap
| Ifold
| Imapfold
type type_dec =
{ t_name: name;
@ -35,7 +34,7 @@ type type_dec =
and tdesc =
| Type_abs
| Type_enum of name list
| Type_struct of (name * base_ty) list
| Type_struct of (name * ty) list
and exp =
{ e_desc: desc; (* its descriptor *)
@ -49,7 +48,6 @@ and desc =
| Evar of ident
| Econstvar of name
| Efby of const option * exp
| Ereset_mem of ident * const * ident
| Etuple of exp list
| Eop of longname * size_exp list * exp list
| Eapp of app * size_exp list * exp list
@ -89,19 +87,19 @@ and link =
| Clink of ck
and ty =
| Tbase of base_ty
| Tbase of ty
| Tprod of ty list
and base_ty =
and ty =
| Tint | Tfloat
| Tid of longname
| Tarray of base_ty * size_exp
| Tarray of ty * size_exp
and const =
| Cint of int
| Cfloat of float
| Cconstr of longname
| Cconst_array of size_exp * const
| Carray of size_exp * const
and pat =
| Etuplepat of pat list
@ -114,7 +112,7 @@ type eq =
type var_dec =
{ v_name : ident;
v_copy_of : ident option;
v_type : base_ty;
v_type : ty;
v_linearity : linearity;
v_clock : ck }
@ -135,7 +133,7 @@ type node_dec =
n_equs : eq list;
n_loc : location;
n_targeting : (int*int) list;
n_mem_alloc : (base_ty * ivar list) list;
n_mem_alloc : (ty * ivar list) list;
n_states_graph : (name,name) interf_graph;
n_params : name list;
n_params_constraints : size_constr list;
@ -162,13 +160,24 @@ let make_dummy_exp desc ty =
e_ck = Cbase; e_loc = no_location }
(* Helper functions to work with types *)
let base_type = function
let type = function
| Tbase(bty) -> bty
| Tprod _ -> assert false
(*TODO Cedric *)
type ivar = | IVar of ident | IField of ident * longname
(** [filter_vars l] returns a list of variables identifiers from
a list of ivar.*)
let rec filter_vars =
function
| [] -> []
| IVar id :: l -> id :: (filter_vars l)
| _ :: l -> filter_vars l
(* get the type of an expression ; assuming that this type is a base type *)
let exp_base_type e =
base_type e.e_ty
let exp_type e =
type e.e_ty
let rec size_exp_of_exp e =
match e.e_desc with
@ -423,17 +432,17 @@ struct
print_list ff print_pat "," pat_list;
fprintf ff ")@]"
let rec print_base_type ff = function
let rec print_type ff = function
| Tint -> fprintf ff "int"
| Tfloat -> fprintf ff "float"
| Tid(id) -> print_longname ff id
| Tarray(ty, n) ->
print_base_type ff ty;
print_type ff ty;
fprintf ff "^";
print_size_exp ff n
let rec print_type ff = function
| Tbase(base_ty) -> print_base_type ff base_ty
| Tbase(ty) -> print_type ff ty
| Tprod(ty_list) ->
fprintf ff "@[(";
print_list ff print_type " *" ty_list;
@ -459,7 +468,7 @@ struct
fprintf ff "@[<v>";
print_ident ff n;
fprintf ff ":";
print_base_type ff ty;
print_type ff ty;
fprintf ff " at ";
print_ck ff ck;
fprintf ff "@]"
@ -468,7 +477,7 @@ struct
| Cint i -> fprintf ff "%d" i
| Cfloat f -> fprintf ff "%f" f
| Cconstr(tag) -> print_longname ff tag
| Cconst_array (n, c) ->
| Carray (n, c) ->
print_c ff c;
fprintf ff "^";
print_size_exp ff n
@ -675,7 +684,7 @@ struct
print_list ff
(fun ff (field, ty) -> print_name ff field;
fprintf ff ": ";
print_base_type ff ty) ";" f_ty_list;
print_type ff ty) ";" f_ty_list;
fprintf ff "}@]@\n@]"
let print_contract ff {c_local = l;

4
minils/sequential/c.ml
View file

@ -167,8 +167,8 @@ let rec pp_array_decl cty =
syntax! *)
let rec pp_vardecl fmt (s, cty) = match cty with
| Cty_arr (n, cty') ->
let base_ty, indices = pp_array_decl cty in
fprintf fmt "%a %s%s" pp_cty base_ty s indices
let ty, indices = pp_array_decl cty in
fprintf fmt "%a %s%s" pp_cty ty s indices
| _ -> fprintf fmt "%a %s" pp_cty cty s
and pp_paramdecl fmt (s, cty) = match cty with
| Cty_arr (n, cty') -> fprintf fmt "%a* %s" pp_cty cty' s

8
minils/sequential/cgen.ml
View file

@ -107,7 +107,7 @@ let node_info classln =
let output_names_list sig_info =
let remove_option ad = match ad.a_name with
| Some n -> n
| None -> Error.message no_location Error.Eno_unnamed_output
| None -> Error.message no_location Error.Eno_unnamed_output (*TODO fresh*)
in
List.map remove_option sig_info.info.outputs
@ -142,7 +142,7 @@ let rec ctype_of_otype oty =
let ctype_of_heptty ty =
let ty = Merge.translate_btype ty in
let ty = Translate.translate_base_type NamesEnv.empty ty in
let ty = Translate.translate_type NamesEnv.empty ty in
ctype_of_otype ty
let cvarlist_of_ovarlist vl =
@ -266,7 +266,7 @@ let rec cexpr_of_exp var_env exp =
| Cint i -> Cconst (Ccint i)
| Cfloat f -> Cconst (Ccfloat f)
| Cconstr c -> Cconst (Ctag (shortname c))
| Cconst_array(n,c) ->
| Carray(n,c) ->
let cc = cexpr_of_exp var_env (Const c) in
Carraylit (repeat_list cc n)
end
@ -415,7 +415,7 @@ let generate_function_call var_env obj_env outvl objn args mem =
(** Create the statement dest = c where c = v^n^m... *)
let rec create_affect_const var_env dest c =
match c with
| Cconst_array(n,c) ->
| Carray(n,c) ->
let x = gen_symbol () in
[ Cfor(x, 0, n,
create_affect_const var_env (Carray (dest, Clhs (Cvar x))) c) ]

14
minils/sequential/mls2obc.ml
View file

@ -54,22 +54,22 @@ let is_op = function
| _ -> false
let rec translate_type const_env = function
| Minils.Tbase(btyp) -> translate_base_type const_env btyp
| Minils.Tbase(btyp) -> translate_type const_env btyp
| Minils.Tprod _ -> assert false
and translate_base_type const_env = function
and translate_type const_env = function
| Minils.Tint -> Tint
| Minils.Tfloat -> Tfloat
| Minils.Tid(id) -> Tid(id)
| Minils.Tarray(ty, n) -> Tarray (translate_base_type const_env ty,
| Minils.Tarray(ty, n) -> Tarray (translate_type const_env ty,
int_of_size_exp const_env n)
let rec translate_const const_env = function
| Minils.Cint(v) -> Cint(v)
| Minils.Cfloat(v) -> Cfloat(v)
| Minils.Cconstr(c) -> Cconstr(c)
| Minils.Cconst_array(n,c) ->
Cconst_array(int_of_size_exp const_env n, translate_const const_env c)
| Minils.Carray(n,c) ->
Carray(int_of_size_exp const_env n, translate_const const_env c)
let rec translate_pat map = function
| Minils.Evarpat(x) -> [var_from_name map x]
@ -259,7 +259,7 @@ let obj_decl l = List.map (fun (x, t, i) -> { obj = x; cls = t; n = i }) l
let translate_var_dec const_env map l =
let one_var { Minils.v_name = x; Minils.v_type = t } =
{ v_name = x; v_type = translate_base_type const_env t; v_pass_by_ref = false }
{ v_name = x; v_type = translate_type const_env t; v_pass_by_ref = false }
in
(* remove unused vars *)
let l = List.filter (fun { Minils.v_name = x } ->
@ -395,7 +395,7 @@ let translate_ty_def const_env { Minils.t_name = name; Minils.t_desc = tdesc } =
| Minils.Type_enum(tag_name_list) -> Type_enum(tag_name_list)
| Minils.Type_struct(field_ty_list) ->
Type_struct
(List.map (fun (f, ty) -> (f, translate_base_type const_env ty)) field_ty_list)
(List.map (fun (f, ty) -> (f, translate_type const_env ty)) field_ty_list)
in
{ t_name = name; t_desc = tdesc }

31
minils/sequential/obc.ml
View file

@ -23,6 +23,12 @@ type obj_name = name
type op_name = longname
type field_name = longname
type iterator_name =
| Imap
| Ifold
| Imapfold
type ty =
| Tint
| Tfloat
@ -42,7 +48,7 @@ type const =
| Cint of int
| Cfloat of float
| Cconstr of longname
| Cconst_array of int * const
| Carray of int * const
type lhs =
| Var of var_name
@ -108,24 +114,11 @@ type program =
(** [is_scalar_type vd] returns whether the type corresponding
to this variable declaration is scalar (ie a type that can
be returned by a C function). *)
let is_scalar_type vd =
let pint = Modname({ qual = "Pervasives"; id = "int" }) in
let pfloat = Modname({ qual = "Pervasives"; id = "float" }) in
let pbool = Modname({ qual = "Pervasives"; id = "bool" }) in
match vd.v_type with
| Tint | Tfloat -> true
| Tid name_int when name_int = pint -> true
| Tid name_float when name_float = pfloat -> true
| Tid name_bool when name_bool = pbool -> true
| _ -> false
let actual_type ty =
let is_scalar_type ty =
match ty with
| Tid(Name("float"))
| Tid(Modname { qual = "Pervasives"; id = "float" }) -> Tfloat
| Tid(Name("int"))
| Tid(Modname { qual = "Pervasives"; id = "int" }) -> Tint
| _ -> ty
| Tid x ->
(x = Initial.pint) or (x = Initial.pfloat) or (x = Initial.pbool)
| _ -> false
let rec var_name x =
match x with
@ -220,7 +213,7 @@ struct
| Cint i -> fprintf ff "%d" i
| Cfloat f -> fprintf ff "%f" f
| Cconstr(tag) -> print_longname ff tag
| Cconst_array(n,c) ->
| Carray(n,c) ->
print_c ff c;
fprintf ff "^%d" n

2
minils/transformations/normalize.ml
View file

@ -20,7 +20,7 @@ and cfalse = Name("false")
let equation (d_list, eq_list) ({ e_ty = te; e_linearity = l; e_ck = ck } as e) =
let n = Ident.fresh "_v" in
let d_list = { v_name = n; v_copy_of = None;
v_type = base_type te; v_linearity = l; v_clock = ck } :: d_list
v_type = type te; v_linearity = l; v_clock = ck } :: d_list
and eq_list = { p_lhs = Evarpat(n); p_rhs = e } :: eq_list in
(d_list, eq_list), n

13
utilities/misc.ml
View file

@ -7,11 +7,9 @@
(* *)
(**************************************************************************)
(* useful stuff *)
(* $Id$ *)
(* version of the compiler *)
let version = "0.4"
let interface_format_version = "5"
let date = "DATE"
(* standard module *)
@ -142,17 +140,6 @@ let unique l =
List.iter (fun i -> Hashtbl.replace tbl i ()) l;
Hashtbl.fold (fun key data accu -> key :: accu) tbl []
type iterator_name =
Imap
| Ifold
| Imapfold
let iterator_to_string i =
match i with
| Imap -> "map"
| Ifold -> "fold"
| Imapfold -> "mapfold"
let rec incomplete_map f l =
match l with
| [] -> []

2
utilities/misc.mli
View file

@ -7,11 +7,9 @@
(* *)
(**************************************************************************)
(* $Id$ *)
(* Version and date of compilation *)
val version : string
val interface_format_version: string
val date : string
(* List of modules initially opened *)