From a54e570d0fb1702eafbc1229be249ebf33132c70 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Le=CC=81onard=20Ge=CC=81rard?= Date: Thu, 9 Sep 2010 00:35:06 +0200 Subject: [PATCH] Hept Scoping should be ok and documented, Hept Parsing too, all the reset to review carefully, Typing to cut from all the scoping. --- compiler/global/clocks.ml | 4 - compiler/global/global_printer.ml | 59 ++ compiler/global/initial.ml | 16 +- compiler/global/location.ml | 4 +- compiler/global/modules.ml | 385 ++++++++----- compiler/global/names.ml | 79 +-- compiler/global/signature.ml | 44 +- compiler/global/static.ml | 48 +- compiler/global/types.ml | 40 +- compiler/heptagon/analysis/interface.ml | 4 +- compiler/heptagon/analysis/statefull.ml | 2 +- compiler/heptagon/analysis/typing.ml | 113 ++-- compiler/heptagon/hept_printer.ml | 29 +- compiler/heptagon/heptagon.ml | 118 ++-- compiler/heptagon/main/hept_compiler.ml | 41 +- compiler/heptagon/main/heptcheck.ml | 10 +- compiler/heptagon/parsing/hept_parser.mly | 63 ++- compiler/heptagon/parsing/hept_parsetree.ml | 58 +- compiler/heptagon/parsing/hept_scoping.ml | 534 +++++++++++------- compiler/heptagon/transformations/automata.ml | 2 +- compiler/main/hept2mls.ml | 3 +- compiler/main/heptc.ml | 28 +- compiler/main/mls2obc.ml | 36 +- compiler/minils/main/mls_compiler.ml | 18 +- compiler/minils/main/mlsc.ml | 7 +- compiler/minils/minils.ml | 13 +- compiler/minils/mls_printer.ml | 29 +- compiler/minils/mls_utils.ml | 9 +- compiler/minils/parsing/mls_lexer.mll | 2 +- compiler/minils/parsing/mls_parser.mly | 99 ++-- compiler/minils/parsing/mls_parsetree.ml | 78 +-- compiler/minils/transformations/callgraph.ml | 96 ++-- compiler/minils/transformations/itfusion.ml | 8 +- compiler/minils/transformations/normalize.ml | 15 +- compiler/minils/transformations/schedule.ml | 1 - compiler/obc/c/cgen.ml | 62 +- compiler/obc/c/cmain.ml | 4 +- compiler/obc/obc.ml | 4 +- compiler/obc/obc_printer.ml | 12 +- compiler/obc/obc_utils.ml | 5 +- compiler/utilities/global/compiler_utils.ml | 33 +- compiler/utilities/misc.ml | 19 +- compiler/utilities/misc.mli | 5 +- compiler/utilities/pp_tools.ml | 8 +- heptc | 2 +- 45 files changed, 1221 insertions(+), 1028 deletions(-) create mode 100644 compiler/global/global_printer.ml diff --git a/compiler/global/clocks.ml b/compiler/global/clocks.ml index 0b183e5..4519834 100644 --- a/compiler/global/clocks.ml +++ b/compiler/global/clocks.ml @@ -95,10 +95,6 @@ let rec skeleton ck = function | Tprod ty_list -> Cprod (List.map (skeleton ck) ty_list) | Tarray _ | Tid _ -> Ck ck -let rec const_skeleton ck se = match se.se_desc with - | Stuple se_list -> Cprod (List.map (const_skeleton ck) se_list) - | _ -> Ck ck - let ckofct = function | Ck ck -> ck_repr ck | Cprod ct_list -> Cbase diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml new file mode 100644 index 0000000..8e3cf5c --- /dev/null +++ b/compiler/global/global_printer.ml @@ -0,0 +1,59 @@ +open Names +open Signature +open Types +open Clocks +open Modules +open Format +open Pp_tools + +let print_qualname ff qn = match qn with + | { qual = "Pervasives"; name = n } -> print_name ff n + | { qual = m; name = n } when m = g_env.current_mod -> print_name ff n + | { qual = m; name = n } -> fprintf ff "%s.%a" m print_name n + + +let rec print_static_exp ff se = match se.se_desc with + | Sint i -> fprintf ff "%d" i + | Sbool b -> fprintf ff "%b" b + | Sfloat f -> fprintf ff "%f" f + | Sconstructor ln -> print_qualname ff ln + | Svar id -> fprintf ff "%a" print_qualname id + | Sop (op, se_list) -> + if is_infix (shortname op) + then + let op_s = opname op ^ " " in + fprintf ff "@[%a@]" + (print_list_l print_static_exp "(" op_s ")") se_list + else + fprintf ff "@[<2>%a@,%a@]" + print_qualname op print_static_exp_tuple se_list + | Sarray_power (se, n) -> + fprintf ff "%a^%a" print_static_exp se print_static_exp n + | Sarray se_list -> + fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["";""]") se_list + | Stuple se_list -> print_static_exp_tuple ff se_list + | Srecord f_se_list -> + print_record (print_couple print_qualname + print_static_exp """ = """) ff f_se_list + +and print_static_exp_tuple ff l = + fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l + +and print_type ff = function + | Tprod ty_list -> + fprintf ff "@[%a@]" (print_list_r print_type "(" " *" ")") ty_list + | Tid id -> print_qualname ff id + | Tarray (ty, n) -> + fprintf ff "@[%a^%a@]" print_type ty print_static_exp n + +let print_size_constraint ff = function + | Cequal (e1, e2) -> + fprintf ff "@[%a = %a@]" print_static_exp e1 print_static_exp e2 + | Clequal (e1, e2) -> + fprintf ff "@[%a <= %a@]" print_static_exp e1 print_static_exp e2 + | Cfalse -> fprintf ff "Cfalse" + +let print_param ff p = + fprintf ff "%a:%a" Names.print_name p.p_name print_type p.p_type + + diff --git a/compiler/global/initial.ml b/compiler/global/initial.ml index bc4756b..4f8a0eb 100644 --- a/compiler/global/initial.ml +++ b/compiler/global/initial.ml @@ -14,14 +14,14 @@ open Types let tglobal = [] let cglobal = [] -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 pbool = { qual = "Pervasives"; name = "bool" } +let ptrue = { qual = "Pervasives"; name = "true" } +let pfalse = { qual = "Pervasives"; name = "false" } +let por = { qual = "Pervasives"; name = "or" } +let pint = { qual = "Pervasives"; name = "int" } +let pfloat = { qual = "Pervasives"; name = "float" } -let mk_pervasives s = Modname({ qual = "Pervasives"; id = s }) +let mk_pervasives s = { qual = "Pervasives"; name = s } let mk_static_int_op op args = mk_static_exp ~ty:(Tid pint) (Sop (op,args)) @@ -37,4 +37,4 @@ let mk_static_bool b = (* build the initial environment *) let initialize () = List.iter (fun (f, ty) -> Modules.add_type f ty) tglobal; - List.iter (fun (f, ty) -> Modules.add_constr f ty) cglobal + List.iter (fun (f, ty) -> Modules.add_constrs f ty) cglobal diff --git a/compiler/global/location.ml b/compiler/global/location.ml index fe1ab18..37a6c00 100644 --- a/compiler/global/location.ml +++ b/compiler/global/location.ml @@ -89,10 +89,10 @@ let print_location ff (Loc(p1,p2)) = if f1 != f2 then (* Strange case *) fprintf ff - "File \"%s\" line %d, character %d, to file \"%s\" line %d, character %d@\n" + "File \"%s\" line %d, character %d, to file \"%s\" line %d, character %d@." f1 l1 n1 f2 l2 n2 - else begin + else begin (* Same file *) if l2 > l1 then fprintf ff "File \"%s\", line %d-%d, characters %d-%d:@\n" f1 l1 l2 n1 n2 diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index cbdcc29..9386bac 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -6,181 +6,254 @@ (* Organization : Demons, LRI, University of Paris-Sud, Orsay *) (* *) (**************************************************************************) -(* global symbol tables *) + +(* Module objects and global environnement management *) open Misc open Signature -open Names open Types +open Names exception Already_defined -exception Cannot_find_file of string (** Warning: Whenever this type is modified, interface_format_version in signature.ml should be incremented. *) -type env = - { mutable name: string; - mutable values: node NamesEnv.t; - mutable types: type_def NamesEnv.t; - mutable constr: ty NamesEnv.t; - mutable structs: structure NamesEnv.t; - mutable fields: name NamesEnv.t; - mutable consts: const_def 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; structs = NamesEnv.empty; fields = NamesEnv.empty; - consts = NamesEnv.empty; format_version = interface_format_version } - -let modules = - { current = current; opened = []; modules = NamesEnv.empty } - -let findfile filename = - if Sys.file_exists filename then - filename - else if not(Filename.is_implicit filename) then - raise(Cannot_find_file filename) +(** Object serialized in compiled interfaces. *) +type module_object = + { m_name : string; + m_values : node NamesEnv.t; + m_types : type_def NamesEnv.t; + m_consts : const_def NamesEnv.t; + m_constrs : name NamesEnv.t; + m_fields : name NamesEnv.t; + m_format_version : string; } + +type env = { + (** Current module name *) + mutable current_mod : module_name; + (** Modules opened and loaded into the env *) + mutable opened_mod : module_name list; + (** Modules loaded into the env *) + mutable loaded_mod : module_name list; + (** Node definitions *) + mutable values : node QualEnv.t; + (** Type definitions *) + mutable types : type_def QualEnv.t; + (** Constants definitions *) + mutable consts : const_def QualEnv.t; + (** Constructors mapped to their corresponding type *) + mutable constrs : qualname QualEnv.t; + (** Fields mapped to their corresponding type *) + mutable fields : qualname QualEnv.t; + (** Accepted compiled interface version *) + format_version : string } + +(** The global environnement *) +let g_env = + { current_mod = ""; + opened_mod = []; + loaded_mod = []; + values = QualEnv.empty; + types = QualEnv.empty; + constrs = QualEnv.empty; + fields = QualEnv.empty; + consts = QualEnv.empty; + format_version = interface_format_version } + + +let is_loaded m = List.mem m g_env.loaded_mod +let is_opened m = List.mem m g_env.opened_mod + + +(** Append a module to the global environnment *) +let _append_module mo = + (* Transforms a module object NamesEnv into its qualified version *) + let qualify mo_env = (* qualify env keys *) + NamesEnv.fold + (fun x v env -> QualEnv.add { qual = mo.m_name; name = x } v env) + mo_env QualEnv.empty in + let qualify_all mo_env = (* qualify env keys and values *) + NamesEnv.fold + (fun x v env -> + QualEnv.add {qual= mo.m_name; name= x} {qual= mo.m_name; name= v} env) + mo_env QualEnv.empty in + g_env.values <- QualEnv.append (qualify mo.m_values) g_env.values; + g_env.types <- QualEnv.append (qualify mo.m_types) g_env.types; + g_env.constrs <- QualEnv.append (qualify_all mo.m_constrs) g_env.constrs; + g_env.fields <- QualEnv.append (qualify_all mo.m_fields) g_env.fields; + g_env.consts <- QualEnv.append (qualify mo.m_consts) g_env.consts + +(** Load a module into the global environnement unless already loaded *) +let _load_module modname = + if is_loaded modname then () else - let rec find = function - [] -> - raise(Cannot_find_file filename) - | a::rest -> - 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 - let filename = findfile (name ^ ".epci") in - let ic = open_in_bin filename in - try - let m:env = input_value ic in - if m.format_version <> interface_format_version then ( - Format.eprintf "The file %s was compiled with \ - an older version of the compiler.@\n \ - Please recompile %s.ept first.@." filename name; - raise Error - ); - close_in ic; - m - with - | End_of_file | Failure _ -> - close_in ic; - Format.eprintf "Corrupted compiled interface file %s.@\n\ - Please recompile %s.ept first.@." filename name; - raise Error - with - | Cannot_find_file(filename) -> - Format.eprintf "Cannot find the compiled interface file %s.@." - filename; - raise Error - -let find_module modname = - try - NamesEnv.find modname modules.modules - with - Not_found -> - 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 - | m :: l -> - 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) -> - 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 name = String.uncapitalize modname in + let filename = Misc.findfile (name ^ ".epci") in + let ic = + try + open_in_bin filename + with + | Misc.Cannot_find_file(f) -> + Format.eprintf "Cannot find the compiled interface file %s.@." f; + raise Error in + let mo:module_object = + try + input_value ic + with + | End_of_file | Failure _ -> + close_in ic; + Format.eprintf "Corrupted compiled interface file %s.@\n\ + Please recompile %s.ept first.@." filename name; + raise Error in + if mo.m_format_version <> interface_format_version + then ( + Format.eprintf "The file %s was compiled with an older version \ + of the compiler.@\nPlease recompile %s.ept first.@." + filename name; + raise Error ); + _append_module mo + + + +(** Opens a module unless already opened + by loading it into the global environnement and seting it as opened *) let open_module modname = - let m = find_module modname in - modules.opened <- m :: modules.opened + if is_opened modname then () + else + _load_module modname; + g_env.opened_mod <- modname::g_env.opened_mod + +(** Initialize the global environnement : + set current module and open default modules *) let initialize modname = - current.name <- modname; + g_env.current_mod <- modname; + g_env.opened_mod <- []; + g_env.loaded_mod <- [modname]; List.iter open_module !default_used_modules -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 type_def = - if NamesEnv.mem f current.types then raise Already_defined; - 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_struct f fields = - if NamesEnv.mem f current.structs then raise Already_defined; - current.structs <- NamesEnv.add f fields current.structs -let add_field f n = - if NamesEnv.mem f current.fields then raise Already_defined; - current.fields <- NamesEnv.add f n current.fields -let add_const f n = - if NamesEnv.mem f current.consts then raise Already_defined; - current.consts <- NamesEnv.add f n current.consts - -let add_value_by_longname ln signature = - match ln with - | Modname { qual = modname; id = f } -> - let m = - if modname = current.name then - current - else - NamesEnv.find modname modules.modules in - if not (NamesEnv.mem f m.values) then - m.values <- NamesEnv.add f signature m.values - | Name _ -> raise Not_found - -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_struct = find (fun ident m -> NamesEnv.find ident m.structs) -let find_field = find (fun ident m -> NamesEnv.find ident m.fields) -let find_const = find (fun ident m -> NamesEnv.find ident m.consts) - -let replace_value f signature = - current.values <- NamesEnv.remove f current.values; - current.values <- NamesEnv.add f signature current.values - -let write oc = output_value oc current - -let longname n = Modname({ qual = current.name; id = n }) -let currentname longname = - match longname with - | Name(n) -> longname - | Modname{ qual = q; id = id} -> - if current.name = q then Name(id) else longname - -exception Undefined_type of longname -(** @return the unaliased version of a type. *) -let rec unalias_type = function + +(** { 3 Add functions prevent redefinitions } *) + +let _check_not_defined env f = + if QualEnv.mem f env then raise Already_defined + +let add_value f v = + _check_not_defined g_env.values f; + g_env.values <- QualEnv.add f v g_env.values +let add_type f v = + _check_not_defined g_env.types f; + g_env.types <- QualEnv.add f v g_env.types +let add_constrs f v = + _check_not_defined g_env.constrs f; + g_env.constrs <- QualEnv.add f v g_env.constrs +let add_field f v = + _check_not_defined g_env.fields f; + g_env.fields <- QualEnv.add f v g_env.fields +let add_const f v = + _check_not_defined g_env.consts f; + g_env.consts <- QualEnv.add f v g_env.consts + + +(** { 3 Find functions look in the global environnement, nothing more } *) + +let _check_loaded_module m = + if not (List.mem m g_env.loaded_mod) + then ( + Format.eprintf "The module %s was not loaded." m; + raise Error ) + +let _find env x = + try QualEnv.find x env + with Not_found -> + _check_loaded_module x.qual; (* should never arrive, sanity check *) + raise Not_found + +let find_value = _find g_env.values +let find_type = _find g_env.types +let find_constrs = _find g_env.constrs +let find_field = _find g_env.fields +let find_const = _find g_env.consts + + +(** { 3 Load_check functions } + Try to load the needed module and then to find it, + return true if in the table, return false if it can't find it. *) + +let _check env q = + _load_module q.qual; + try let _ = QualEnv.find q env in true + with Not_found -> false + +let check_value = _check g_env.values +let check_type = _check g_env.types +let check_constrs = _check g_env.constrs +let check_field = _check g_env.fields +let check_const = _check g_env.consts + + + +(** { 3 Qualify functions [qualify_* name] return the qualified name + matching [name] in the global env scope (current module :: opened modules). + @raise [Not_found] if not in scope } *) + +let _qualify env name = + let tries m = + try + let _ = QualEnv.find { qual = m; name = name } env in + true + with Not_found -> false in + let m = List.find tries (g_env.current_mod::g_env.opened_mod) in + { qual = m; name = name } + +let qualify_value = _qualify g_env.values +let qualify_type = _qualify g_env.types +let qualify_constrs = _qualify g_env.constrs +let qualify_field = _qualify g_env.fields +let qualify_const = _qualify g_env.consts + +(** @return the name as qualified with the current module *) +let current_qual n = { qual = g_env.current_mod; name = n } + + +exception Undefined_type of qualname + +(** @return the unaliased version of a type. @raise Undefined_type *) +let rec unalias_type t = match t with | Tid ty_name -> (try - let { qualid = q; info = ty_desc } = find_type ty_name in - match ty_desc with - | Talias ty -> unalias_type ty - | _ -> Tid (Modname q) + match find_type ty_name with + | Talias ty -> unalias_type ty + | _ -> t with Not_found -> raise (Undefined_type ty_name)) | Tarray (ty, n) -> Tarray(unalias_type ty, n) | Tprod ty_list -> Tprod (List.map unalias_type ty_list) + + +(** Write the current module as a [module_object] to oc *) +let write_current_module oc = + (* Filter and transform a qualified env into the current module object env *) + let unqualify env = (* unqualify env keys *) + QualEnv.fold + (fun x v current -> + if x.qual = g_env.current_mod + then NamesEnv.add x.name v current + else current) env NamesEnv.empty in + let unqualify_all env = (* unqualify env keys and values *) + QualEnv.fold + (fun x v current -> + if x.qual = g_env.current_mod + then NamesEnv.add x.name v.name current + else current) env NamesEnv.empty in + let current = + { m_name = g_env.current_mod; + m_values = unqualify g_env.values; + m_types = unqualify g_env.types; + m_constrs = unqualify_all g_env.constrs; + m_fields = unqualify_all g_env.fields; + m_consts = unqualify g_env.consts; + m_format_version = g_env.format_version } in + output_value oc current + diff --git a/compiler/global/names.ml b/compiler/global/names.ml index 4e36a2d..ea0dac7 100644 --- a/compiler/global/names.ml +++ b/compiler/global/names.ml @@ -4,60 +4,46 @@ type name = string -type longname = - | Name of name - | Modname of qualident +and qualname = { qual: string; name: string } -and qualident = { qual: string; id: string } +type type_name = qualname +type fun_name = qualname +type field_name = qualname +type constructor_name = qualname +type constant_name = qualname +type module_name = name -type type_name = longname -type fun_name = longname +let local_qualname = "$$%local_current_illegal_module_name%$$" +let local_qn name = { qual = local_qualname; name = name } -type field_name = longname - -type constructor_name = longname - -type constant_name = longname - - -module NamesM = struct - type t = name - let compare = compare +module NamesEnv = struct + include (Map.Make(struct type t = name let compare = compare end)) + let append env0 env = fold (fun key v env -> add key v env) env0 env end -module NamesEnv = -struct - include (Map.Make(NamesM)) +module QualEnv = struct + include (Map.Make(struct type t = qualname let compare = compare end)) - let append env0 env = - fold (fun key v env -> add key v env) env0 env + (** [append env' env] appends env' to env *) + let append env' env = fold (fun key v env -> add key v env) env' env end -module LongNameEnv = Map.Make (struct - type t = longname - let compare = compare - end) - module S = Set.Make (struct type t = string let compare = compare end) -let shortname = function - | Name s -> s - | Modname { id = id; } -> id +let shortname { name = n; } = n -let fullname = function - | Name s -> s - | Modname { qual = qual; id = id; } -> qual ^ "." ^ id +let fullname { qual = qual; name = n; } = qual ^ "." ^ n -let mk_longname s = +let qualname_of_string s = try let ind = String.index s '.' in if ind = 0 || ind = String.length s - 1 then invalid_arg "mk_longname: ill-formed identifier"; - let id = String.sub s (ind + 1) (String.length s - ind - 1) in - Modname { qual = String.sub s 0 ind; id = id; } - with Not_found -> Name s + let n = String.sub s (ind + 1) (String.length s - ind - 1) in + { qual = String.sub s 0 ind; name = n; } + with Not_found -> { qual = ""; name = s } (** Are infix [or], [quo], [mod], [land], [lor], [lxor], [lsl], [lsr], [asr] @@ -73,22 +59,15 @@ let is_infix s = | 'a' .. 'z' | 'A' .. 'Z' | '_' | '`' -> false | _ -> true) +open Format + let print_name ff n = let n = if is_infix n then "( " ^ (n ^ " )") (* do not remove the space around n, since for example "(*" would create bugs *) else n - in Format.fprintf ff "%s" n - -let print_longname ff n = - match n with - | Name m -> print_name ff m - | Modname { qual = "Pervasives"; id = m } -> print_name ff m - | Modname { qual = m1; id = m2 } -> - Format.fprintf ff "%s." m1; - print_name ff m2 - -let opname ln = match ln with - | Name n -> n - | Modname { qual = "Pervasives"; id = m; } -> m - | Modname { qual = qual; id = id; } -> qual ^ "." ^ id + in fprintf ff "%s" n + +let opname qn = match qn with + | { qual = "Pervasives"; name = m; } -> m + | { qual = qual; name = n; } -> qual ^ "." ^ n diff --git a/compiler/global/signature.ml b/compiler/global/signature.ml index e2c87d2..7adedc9 100644 --- a/compiler/global/signature.ml +++ b/compiler/global/signature.ml @@ -12,7 +12,7 @@ open Types (** Warning: Whenever these types are modified, interface_format_version should be incremented. *) -let interface_format_version = "10" +let interface_format_version = "20" (** Node argument *) type arg = { a_name : name option; a_type : ty } @@ -20,30 +20,30 @@ type arg = { a_name : name option; a_type : ty } (** Node static parameters *) type param = { p_name : name; p_type : ty } -(** Constraints on size expressions. *) +(** Constraints on size expressions *) type size_constraint = - | Cequal of static_exp * static_exp (* e1 = e2*) + | Cequal of static_exp * static_exp (* e1 = e2 *) | Clequal of static_exp * static_exp (* e1 <= e2 *) | Cfalse (** Node signature *) -type node = - { node_inputs : arg list; - node_outputs : arg list; - node_statefull : bool; - node_params : param list; (** Static parameters *) - node_params_constraints : size_constraint list } - -type field = { f_name : name; f_type : ty } +type node = { + node_inputs : arg list; + node_outputs : arg list; + node_statefull : bool; + node_params : param list; + node_params_constraints : size_constraint list } + +type field = { f_name : field_name; f_type : ty } type structure = field list type type_def = | Tabstract | Talias of ty - | Tenum of name list + | Tenum of constructor_name list | Tstruct of structure -type const_def = { c_name : name; c_type : ty; c_value : static_exp } +type const_def = { c_type : ty; c_value : static_exp } let names_of_arg_list l = List.map (fun ad -> ad.a_name) l @@ -55,18 +55,20 @@ let mk_param name ty = { p_name = name; p_type = ty } let mk_field n ty = { f_name = n; f_type = ty } -let mk_const_def name ty value = - { c_name = name; c_type = ty; c_value = value } +let mk_const_def ty value = + { c_type = ty; c_value = value } + +let mk_node ?(constraints = []) ins outs statefull params = + { node_inputs = ins; + node_outputs = outs; + node_statefull = statefull; + node_params = params; + node_params_constraints = constraints } let rec field_assoc f = function | [] -> raise Not_found | { f_name = n; f_type = ty }::l -> - if shortname f = n then ty + if f = n then ty else field_assoc f l -open Format - -let print_param ff p = - fprintf ff "%a:%a" Names.print_name p.p_name print_type p.p_type - diff --git a/compiler/global/static.ml b/compiler/global/static.ml index a3f39c5..024900d 100644 --- a/compiler/global/static.ml +++ b/compiler/global/static.ml @@ -10,8 +10,7 @@ (** 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],... -*) + x[n - 1], x[1 + 3],... *) open Names open Format @@ -25,34 +24,26 @@ exception Partial_instanciation of static_exp exception Not_static -(** Returns the op from an operator full name. *) -let op_from_app_name ln = - match ln with - | Modname { qual = "Pervasives" } -> ln - | _ -> raise Not_static - - - let partial_apply_op op se_list = match se_list with | [{ se_desc = Sint n1 }; { se_desc = Sint n2 }] -> (match op with - | Modname { qual = "Pervasives"; id = "+" } -> + | { qual = "Pervasives"; name = "+" } -> Sint (n1 + n2) - | Modname { qual = "Pervasives"; id = "-" } -> + | { qual = "Pervasives"; name = "-" } -> Sint (n1 - n2) - | Modname { qual = "Pervasives"; id = "*" } -> + | { qual = "Pervasives"; name = "*" } -> Sint (n1 * n2) - | Modname { qual = "Pervasives"; id = "/" } -> + | { qual = "Pervasives"; name = "/" } -> let n = if n2 = 0 then raise Instanciation_failed else n1 / n2 in Sint n - | Modname { qual = "Pervasives"; id = "=" } -> + | { qual = "Pervasives"; name = "=" } -> Sbool (n1 = n2) | _ -> assert false (*TODO: add missing operators*) ) | [{ se_desc = Sint n }] -> (match op with - | Modname { qual = "Pervasives"; id = "~-" } -> Sint (-n) + | { qual = "Pervasives"; name = "~-" } -> Sint (-n) | _ -> assert false (*TODO: add missing operators*) ) | _ -> Sop(op, se_list) @@ -67,12 +58,10 @@ let eval_core eval apply_op env se = match se.se_desc with | Sint _ | Sfloat _ | Sbool _ | Sconstructor _ -> se | Svar ln -> ( try (* first try to find in global const env *) - let { info = cd } = find_const ln in + let cd = find_const ln in eval env cd.c_value - with Not_found -> ( - match ln with (* then try to find in local env *) - | Name n -> eval env (NamesEnv.find n env) - | Modname _ -> raise Not_found ) ) + with Not_found -> (* then try to find in local env *) + eval env (QualEnv.find ln env)) | Sop (op, se_list) -> let se_list = List.map (eval env) se_list in { se with se_desc = apply_op op se_list } @@ -109,7 +98,8 @@ let int_of_static_exp env se = | Sint i -> i | _ -> (Format.eprintf "Internal compiler error, \ - [eval_int] received the static_exp %a.@." Types.print_static_exp se; + [eval_int] received the static_exp %a.@." + Global_printer.print_static_exp se; assert false) (** [is_true env constr] returns whether the constraint is satisfied @@ -152,10 +142,7 @@ let rec solve const_env = in the map (mapping vars to size exps). *) let rec static_exp_subst m se = match se.se_desc with - | Svar ln -> - (match ln with - | Name n -> (try NamesEnv.find n m with | Not_found -> se) - | Modname _ -> se) + | Svar qn -> (try QualEnv.find qn m with | Not_found -> se) | Sop (op, se_list) -> { se with se_desc = Sop (op, List.map (static_exp_subst m) se_list) } | Sarray_power (se, n) -> @@ -181,12 +168,3 @@ let instanciate_constr m constr = List.map (replace_one m) constr -open Format - -let print_size_constraint ff = function - | Cequal (e1, e2) -> - fprintf ff "@[%a = %a@]" print_static_exp e1 print_static_exp e2 - | Clequal (e1, e2) -> - fprintf ff "@[%a <= %a@]" print_static_exp e1 print_static_exp e2 - | Cfalse -> fprintf ff "Cfalse" - diff --git a/compiler/global/types.ml b/compiler/global/types.ml index 4b87f38..9bf3318 100644 --- a/compiler/global/types.ml +++ b/compiler/global/types.ml @@ -34,47 +34,9 @@ let prod = function | [ty] -> ty | ty_list -> Tprod ty_list + (** DO NOT use this after the typing, since it could give invalid_type *) let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc = { se_desc = desc; se_ty = ty; se_loc = loc } -open Pp_tools -open Format - -let rec print_static_exp ff se = match se.se_desc with - | Sint i -> fprintf ff "%d" i - | Sbool b -> fprintf ff "%b" b - | Sfloat f -> fprintf ff "%f" f - | Sconstructor ln -> print_longname ff ln - | Svar id -> fprintf ff "%a" print_longname id - (* | Sop (op, [e_l; e_r]) -> *) - (* fprintf ff "(@[<2>%a@ %a %a@])" *) - (* print_static_exp e_l print_longname op print_static_exp r *) - | Sop (op, se_list) -> - if is_infix (shortname op) - then - let op_s = opname op ^ " " in - fprintf ff "@[%a@]" - (print_list_l print_static_exp "(" op_s ")") se_list - else - fprintf ff "@[<2>%a@,%a@]" - print_longname op print_static_exp_tuple se_list - | Sarray_power (se, n) -> - fprintf ff "%a^%a" print_static_exp se print_static_exp n - | Sarray se_list -> - fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "["";""]") se_list - | Stuple se_list -> print_static_exp_tuple ff se_list - | Srecord f_se_list -> - print_record (print_couple print_longname - print_static_exp """ = """) ff f_se_list - -and print_static_exp_tuple ff l = - fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "("","")") l - -and print_type ff = function - | Tprod ty_list -> - fprintf ff "@[%a@]" (print_list_r print_type "(" " *" ")") ty_list - | Tid id -> print_longname ff id - | Tarray (ty, n) -> - fprintf ff "@[%a^%a@]" print_type ty print_static_exp n diff --git a/compiler/heptagon/analysis/interface.ml b/compiler/heptagon/analysis/interface.ml index 07cbf28..f6a9c54 100644 --- a/compiler/heptagon/analysis/interface.ml +++ b/compiler/heptagon/analysis/interface.ml @@ -13,7 +13,6 @@ open Names open Heptagon open Signature open Modules -open Typing open Pp_tools open Types @@ -21,7 +20,8 @@ module Type = struct let sigtype { sig_name = name; sig_inputs = i_list; sig_statefull = statefull; sig_outputs = o_list; sig_params = params } = - let typed_params, const_env = build_node_params NamesEnv.empty params in + let typed_params, const_env = + Typing.build_node_params NamesEnv.empty params in let check_arg a = { a with a_type = check_type const_env a.a_type } in name, { node_inputs = List.map check_arg i_list; node_outputs = List.map check_arg o_list; diff --git a/compiler/heptagon/analysis/statefull.ml b/compiler/heptagon/analysis/statefull.ml index adc2f3a..d719d7c 100644 --- a/compiler/heptagon/analysis/statefull.ml +++ b/compiler/heptagon/analysis/statefull.ml @@ -40,7 +40,7 @@ let edesc funs statefull ed = | Efby _ | Epre _ -> ed, true | Eapp({ a_op = Earrow }, _, _) -> ed, true | Eapp({ a_op = (Enode f | Efun f) } as app, e_list, r) -> - let { qualid = q; info = ty_desc } = find_value f in + let ty_desc = find_value f in let op = if ty_desc.node_statefull then Enode f else Efun f in Eapp({ app with a_op = op }, e_list, r), ty_desc.node_statefull or statefull diff --git a/compiler/heptagon/analysis/typing.ml b/compiler/heptagon/analysis/typing.ml index 31b9da9..7541e75 100644 --- a/compiler/heptagon/analysis/typing.ml +++ b/compiler/heptagon/analysis/typing.ml @@ -17,6 +17,7 @@ open Modules open Initial open Static open Types +open Global_printer open Heptagon open Hept_mapfold @@ -38,11 +39,11 @@ type error = | Esome_fields_are_missing | Esubscripted_value_not_an_array of ty | Earray_subscript_should_be_const - | Eundefined_const of longname + | Eundefined_const of qualname | Econstraint_solve_failed of size_constraint | Etype_should_be_static of ty | Erecord_type_expected of ty - | Eno_such_field of ty * longname + | Eno_such_field of ty * qualname | Eempty_record | Eempty_array | Efoldi_bad_args of ty @@ -78,8 +79,8 @@ let message loc kind = Format.eprintf "%aType Clash: this expression has type %a, @\n\ but is expected to have type %a.@." print_location loc - Types.print_type actual_ty - Types.print_type expected_ty + print_type actual_ty + print_type expected_ty | Earity_clash(actual_arit, expected_arit) -> Format.eprintf "%aType Clash: this expression expects %d arguments,@\n\ but is expected to have %d.@." @@ -116,7 +117,7 @@ let message loc kind = Format.eprintf "%aSubscript used on a non array type : %a.@." print_location loc - Types.print_type ty + Global_printer.print_type ty | Earray_subscript_should_be_const -> Format.eprintf "%aSubscript has to be a static value.@." @@ -135,17 +136,17 @@ let message loc kind = Format.eprintf "%aThis type should be static : %a.@." print_location loc - Types.print_type ty + print_type ty | Erecord_type_expected ty -> Format.eprintf "%aA record was expected (found %a).@." print_location loc - Types.print_type ty + print_type ty | Eno_such_field (ty, f) -> Format.eprintf "%aThe record type '%a' does not have a '%s' field.@." print_location loc - Types.print_type ty + print_type ty (shortname f) | Eempty_record -> Format.eprintf @@ -160,7 +161,7 @@ let message loc kind = "%aThe function given to foldi should expect an integer \ as the last but one argument (found: %a).@." print_location loc - Types.print_type ty + print_type ty end; raise Error @@ -296,11 +297,10 @@ let simplify_type loc ty = Instanciation_failed -> message loc (Etype_should_be_static ty) let build_subst names values = - if List.length names <> List.length values then - error (Estatic_arity_clash (List.length values, List.length names)); - - List.fold_left2 (fun m { p_name = n } v -> NamesEnv.add n v m) - NamesEnv.empty names values + if List.length names <> List.length values + then error (Estatic_arity_clash (List.length values, List.length names)); + List.fold_left2 (fun m n v -> QualEnv.add n v m) + QualEnv.empty names values let rec subst_type_vars m = function | Tarray(ty, e) -> Tarray(subst_type_vars m ty, static_exp_subst m e) @@ -407,7 +407,7 @@ let check_static_field_unicity l = [loc] is the location used for error reporting.*) let struct_info_from_name n = try - let { qualid = q; + let { qualname = q; info = fields } = find_struct n in q, fields with @@ -426,18 +426,19 @@ let struct_info ty = match ty with [loc] is the location used for error reporting.*) let struct_info_from_field f = try - let { qualid = q; info = n } = find_field f in - struct_info_from_name (Modname { qual = q.qual; id = n }) + let { qualname = q; info = n } = find_field f in + struct_info_from_name { qual = q.qual; name = n } with Not_found -> error (Eundefined (fullname f)) (** [check_type t] checks that t exists *) +(*TODO should be already done in scoping *) let rec check_type const_env = function | Tarray(ty, e) -> let typed_e = expect_static_exp const_env (Tid Initial.pint) e in Tarray(check_type const_env ty, typed_e) | Tid ty_name -> - (try Tid(Modname((find_type ty_name).qualid)) + (try Tid((find_type ty_name).qualname) with Not_found -> error (Eundefined(fullname ty_name))) | Tprod l -> Tprod (List.map (check_type const_env) l) @@ -450,23 +451,20 @@ and typing_static_exp const_env se = | Sfloat v -> Sfloat v, Tid Initial.pfloat | Svar ln -> (try (* this can be a global const*) - let { qualid = q; info = cd } = Modules.find_const ln in - Svar (Modname q), cd.Signature.c_type + let { qualname = q; info = cd } = Modules.find_const ln in + Svar q, cd.Signature.c_type +(* TODO verifier... *) with Not_found -> (* or a static parameter *) - (match ln with - | Name n -> - (try Svar ln, NamesEnv.find n const_env - with Not_found -> error (Eundefined_const ln)) - | Modname _ -> error (Eundefined_const ln)) - ) + (try Svar ln, QualEnv.find ln const_env + with Not_found -> error (Eundefined_const ln) ) ) | Sconstructor c -> - let { qualid = q; info = ty } = find_constr c in - Sconstructor(Modname q), ty + let { qualname = q; info = ty } = find_constr c in + Sconstructor q, ty | Sop (op, se_list) -> - let { qualid = q; info = ty_desc } = find_value op in + let { qualname = q; info = ty_desc } = find_value op in let typed_se_list = typing_static_args const_env (types_of_arg_list ty_desc.node_inputs) se_list in - Sop (Modname q, typed_se_list), + Sop (q, typed_se_list), prod (types_of_arg_list ty_desc.node_outputs) | Sarray_power (se, n) -> let typed_n = expect_static_exp const_env (Tid Initial.pint) n in @@ -496,8 +494,8 @@ and typing_static_exp const_env se = check_static_field_unicity f_se_list; let f_se_list = List.map (typing_static_field const_env fields - (Tid (Modname q)) q.qual) f_se_list in - Srecord f_se_list, Tid (Modname q) + (Tid q) q.qual) f_se_list in + Srecord f_se_list, Tid q in { se with se_ty = ty; se_desc = desc }, ty @@ -508,7 +506,7 @@ and typing_static_field const_env fields t1 modname (f,se) = try let ty = check_type const_env (field_assoc f fields) in let typed_se = expect_static_exp const_env ty se in - Modname { qual = modname; id = shortname f }, typed_se + { qual = modname; name = shortname f }, typed_se with Not_found -> message se.se_loc (Eno_such_field (t1, f)) @@ -563,8 +561,8 @@ let rec typing const_env h e = check_field_unicity l; let l = List.map (typing_field - const_env h fields (Tid (Modname q)) q.qual) l in - Estruct l, Tid (Modname q) + const_env h fields (Tid q) q.qual) l in + Estruct l, Tid q | Epre (None, e) -> let typed_e,ty = typing const_env h e in @@ -583,9 +581,12 @@ let rec typing const_env h e = | Eiterator (it, ({ a_op = (Enode f | Efun f); a_params = params } as app), n, e_list, reset) -> - let { qualid = q; info = ty_desc } = find_value f in - let op, expected_ty_list, result_ty_list = kind (Modname q) ty_desc in - let m = build_subst ty_desc.node_params params in + let { qualname = q; info = ty_desc } = find_value f in + let op, expected_ty_list, result_ty_list = kind q ty_desc in +(*TODO verifier....*) + let node_params = + List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in + let m = build_subst node_params params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in let result_ty_list = List.map (subst_type_vars m) result_ty_list in @@ -611,7 +612,7 @@ and typing_field const_env h fields t1 modname (f, e) = try let ty = check_type const_env (field_assoc f fields) in let typed_e = expect const_env h ty e in - Modname { qual = modname; id = shortname f }, typed_e + { qual = modname; name = shortname f }, typed_e with Not_found -> message e.e_loc (Eno_such_field (t1, f)) @@ -642,9 +643,12 @@ and typing_app const_env h op e_list = t1, op, [typed_e1; typed_e2; typed_e3] | { a_op = (Efun f | Enode f); a_params = params } as app, e_list -> - let { qualid = q; info = ty_desc } = find_value f in - let op, expected_ty_list, result_ty_list = kind (Modname q) ty_desc in - let m = build_subst ty_desc.node_params params in + let { qualname = q; info = ty_desc } = find_value f in + let op, expected_ty_list, result_ty_list = kind q ty_desc in +(*TODO verifier....*) + let node_params = + List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in + let m = build_subst node_params params in let expected_ty_list = List.map (subst_type_vars m) expected_ty_list in let typed_e_list = typing_args const_env h expected_ty_list e_list in @@ -678,7 +682,7 @@ and typing_app const_env h op e_list = let typed_e, t1 = typing const_env h e in let q, fields = struct_info t1 in let t2 = field_type const_env fn fields t1 e.e_loc in - let fn = Modname { qual = q.qual; id = shortname fn } in + let fn = { qual = q.qual; name = shortname fn } in let f = { f with se_desc = Sconstructor fn } in t2, { op with a_params = [f] }, [typed_e] @@ -690,7 +694,7 @@ and typing_app const_env h op e_list = | Sconstructor fn -> fn | _ -> assert false) in let f = { f with se_desc = - Sconstructor (Modname { qual = q.qual; id = shortname fn }) } in + Sconstructor { qual = q.qual; name = shortname fn } } in let t2 = field_type const_env fn fields t1 e1.e_loc in let typed_e2 = expect const_env h t2 e2 in t1, { op with a_params = [f] } , [typed_e1; typed_e2] @@ -945,7 +949,7 @@ and typing_switch_handlers const_env h acc ty switch_handlers = let typed_b, defined_names, _ = typing_block const_env h b in { w_block = typed_b; (* Replace handler name with fully qualified name *) - w_name = Modname((find_constr name).qualid)}, + w_name = (find_constr name).qualname}, defined_names in let typed_switch_handlers, defined_names_list = @@ -1050,7 +1054,9 @@ let solve loc cl = let build_node_params const_env l = let check_param env p = let ty = check_type const_env p.p_type in - { p with p_type = ty }, NamesEnv.add p.p_name ty env + let p = { p with p_type = ty } in + let n = Names.local_qn p.p_name in + p, QualEnv.add n ty env in mapfold check_param const_env l @@ -1061,7 +1067,7 @@ let node ({ n_name = f; n_statefull = statefull; n_params = node_params; } as n) = try let typed_params, const_env = - build_node_params NamesEnv.empty node_params in + build_node_params QualEnv.empty node_params in let typed_i_list, (input_names, h) = build const_env Env.empty i_list in let typed_o_list, (output_names, h) = build const_env h o_list in @@ -1075,9 +1081,6 @@ let node ({ n_name = f; n_statefull = statefull; included_env defined_names output_names; included_env output_names defined_names; - (* if not (statefull) & (List.length o_list <> 1) - then error (Etoo_many_outputs);*) - let cl = get_size_constraint () in let cl = solve loc cl in add_value f (signature statefull typed_i_list typed_o_list typed_params cl); @@ -1098,13 +1101,13 @@ let deftype { t_name = n; t_desc = tdesc; t_loc = loc } = | Type_alias ln -> add_type n (Talias ln) | Type_enum(tag_name_list) -> add_type n (Tenum tag_name_list); - List.iter (fun tag -> add_constr tag (Tid (longname n))) tag_name_list + List.iter (fun tag -> add_constr tag (Tid (qualname n))) tag_name_list | Type_struct(field_ty_list) -> let field_ty_list = List.map (fun f -> mk_field f.f_name (simplify_type loc - (check_type NamesEnv.empty f.f_type))) + (check_type QualEnv.empty f.f_type))) field_ty_list in add_type n (Tstruct field_ty_list); add_struct n field_ty_list; @@ -1114,10 +1117,10 @@ let deftype { t_name = n; t_desc = tdesc; t_loc = loc } = TypingError(error) -> message loc error let typing_const_dec cd = - let ty = check_type NamesEnv.empty cd.c_type in - let se = expect_static_exp NamesEnv.empty ty cd.c_value in + let ty = check_type QualEnv.empty cd.c_type in + let se = expect_static_exp QualEnv.empty ty cd.c_value in let cd = { cd with c_value = se; c_type = ty } in - add_const cd.c_name (mk_const_def cd.c_name cd.c_type cd.c_value); + add_const cd.c_name (mk_const_def cd.c_type cd.c_value); cd let program diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index 27fbe31..e12f80b 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -15,6 +15,7 @@ open Idents open Modules open Static open Format +open Global_printer open Pp_tools open Types open Signature @@ -68,7 +69,7 @@ and print_exp ff e = ) | Estruct(f_e_list) -> print_list_r - (fun ff (field, e) -> print_longname ff field;fprintf ff " = "; + (fun ff (field, e) -> print_qualname ff field;fprintf ff " = "; print_exp ff e) "{" ";" "}" ff f_e_list; fprintf ff "}@]" @@ -78,10 +79,10 @@ and print_exp ff e = print_iterator ff it; fprintf ff " "; (match params with - | [] -> print_longname ff ln + | [] -> print_qualname ff ln | l -> fprintf ff "("; - print_longname ff ln; + print_qualname ff ln; print_call_params ff params; fprintf ff ")" ); @@ -114,7 +115,7 @@ and print_op ff op params e_list = | Earray, _, e_list -> print_list_r print_exp "[" "," "]" ff e_list | (Efun f|Enode f), params, e_list -> - print_longname ff f; + print_qualname ff f; print_call_params ff params; print_exps ff e_list | Efield, [field], [e] -> @@ -210,7 +211,7 @@ and print_eq_list ff = function and print_state_handler ff { s_state = s; s_block = b; s_until = until; s_unless = unless } = fprintf ff " @[state "; - fprintf ff "%s@," s; + fprintf ff "%a@," print_name s; print_block ff b; if until <> [] then begin @@ -228,7 +229,7 @@ and print_state_handler ff and print_switch_handler ff { w_name = tag; w_block = b } = fprintf ff " @[| "; - print_longname ff tag; + print_qualname ff tag; fprintf ff "@,"; print_block ff b; fprintf ff "@]" @@ -264,25 +265,25 @@ and print_block ff { b_local = v_list; b_equs = eqs; b_defnames = defnames } = let print_type_def ff { t_name = name; t_desc = tdesc } = match tdesc with - | Type_abs -> fprintf ff "@[type %s@.@]" name + | Type_abs -> fprintf ff "@[type %a@.@]" print_qualname name | Type_alias ty -> - fprintf ff "@[type %s@ = %a@.@]" name print_type ty + fprintf ff "@[type %a@ = %a@.@]" print_qualname name print_type ty | Type_enum(tag_name_list) -> - fprintf ff "@[type %s = " name; - print_list_r print_name "" "| " "" ff tag_name_list; + fprintf ff "@[type %a = " print_qualname name; + print_list_r print_qualname "" "| " "" ff tag_name_list; fprintf ff "@.@]" | Type_struct(f_ty_list) -> - fprintf ff "@[type %s = " name; + fprintf ff "@[type %a = " print_qualname name; print_list_r (fun ff { f_name = field; f_type = ty } -> - print_name ff field; + print_qualname ff field; fprintf ff ": "; print_type ff ty) "{" ";" "}" ff f_ty_list; fprintf ff "@.@]" let print_const_dec ff c = fprintf ff "@[const "; - print_name ff c.c_name; + print_qualname ff c.c_name; fprintf ff " : "; print_type ff c.c_type; fprintf ff " = "; @@ -317,7 +318,7 @@ let print_node ff n_block = nb; n_output = no; n_contract = contract; n_params = params; } = fprintf ff "@[node "; - print_name ff n; + print_qualname ff n; fprintf ff "@[%a@]" print_node_params params; fprintf ff "@[%a@]" (print_list_r print_vd "(" ";" ")") ni; fprintf ff " returns "; diff --git a/compiler/heptagon/heptagon.ml b/compiler/heptagon/heptagon.ml index d9af65a..0521e19 100644 --- a/compiler/heptagon/heptagon.ml +++ b/compiler/heptagon/heptagon.ml @@ -24,7 +24,10 @@ type iterator_type = | Ifoldi | Imapfold -type exp = { e_desc : desc; e_ty : ty; e_loc : location } +type exp = { + e_desc : desc; + e_ty : ty; + e_loc : location } and desc = | Econst of static_exp @@ -36,7 +39,10 @@ and desc = | Eapp of app * exp list * exp option | Eiterator of iterator_type * app * static_exp * exp list * exp option -and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } +and app = { + a_op : op; + a_params : static_exp list; + a_unsafe : bool } and op = | Eequal @@ -59,7 +65,10 @@ and pat = | Etuplepat of pat list | Evarpat of var_ident -type eq = { eq_desc : eqdesc; eq_statefull : bool; eq_loc : location } +type eq = { + eq_desc : eqdesc; + eq_statefull : bool; + eq_loc : location } and eqdesc = | Eautomaton of state_handler list @@ -69,82 +78,92 @@ and eqdesc = | Eeq of pat * exp and block = { - b_local : var_dec list; - b_equs : eq list; - b_defnames : ty Env.t; + b_local : var_dec list; + b_equs : eq list; + b_defnames : ty Env.t; b_statefull : bool; - b_loc : location } + b_loc : location } and state_handler = { - s_state : state_name; - s_block : block; - s_until : escape list; + s_state : state_name; + s_block : block; + s_until : escape list; s_unless : escape list } and escape = { - e_cond : exp; - e_reset : bool; + e_cond : exp; + e_reset : bool; e_next_state : state_name } -and switch_handler = { w_name : constructor_name; w_block : block } +and switch_handler = { + w_name : constructor_name; + 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_ident : var_ident; - v_type : ty; - v_last : last; - v_loc : location } + v_type : ty; + v_last : last; + v_loc : location } and last = Var | Last of static_exp option -type type_dec = { t_name : name; t_desc : type_dec_desc; t_loc : location } +type type_dec = { + t_name : qualname; + t_desc : type_dec_desc; + t_loc : location } and type_dec_desc = | Type_abs | Type_alias of ty - | Type_enum of name list + | Type_enum of constructor_name list | Type_struct of structure type contract = { - c_assume : exp; + c_assume : exp; c_enforce : exp; - c_block : block } + c_block : block } type node_dec = { - n_name : name; + n_name : qualname; n_statefull : bool; - n_input : var_dec list; - n_output : var_dec list; - n_contract : contract option; - n_block : block; - n_loc : location; - n_params : param list; + n_input : var_dec list; + n_output : var_dec list; + n_contract : contract option; + n_block : block; + n_loc : location; + n_params : param list; n_params_constraints : size_constraint list } type const_dec = { - c_name : name; - c_type : ty; + c_name : qualname; + c_type : ty; c_value : static_exp; - c_loc : location } + c_loc : location } type program = { p_modname : name; - p_opened : name list; - p_types : type_dec list; - p_nodes : node_dec list; - p_consts : const_dec 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 : arg list; + sig_name : qualname; + sig_inputs : arg list; sig_statefull : bool; - sig_outputs : arg list; - sig_params : param list } + sig_outputs : arg list; + sig_params : param list; + sig_loc : location } type interface = interface_decl list -and interface_decl = { interf_desc : interface_desc; interf_loc : location } +and interface_decl = { + interf_desc : interface_desc; + interf_loc : location } and interface_desc = | Iopen of name @@ -188,17 +207,14 @@ let mk_simple_equation pat e = let mk_switch_equation ?(statefull = true) e l = mk_equation ~statefull:statefull (Eswitch (e, l)) -(** @return a size exp operator from a Heptagon operator. *) -let op_from_app app = - match app.a_op with - | Efun op -> op_from_app_name op - | _ -> raise Not_static - -(** Translates a Heptagon exp into a static size exp. *) -(*let rec static_exp_of_exp e = - match e.e_desc with - | Econst se -> se - | _ -> raise Not_static *) +let mk_signature name ins outs statefull params loc = + { sig_name = name; + sig_inputs = ins; + sig_statefull = statefull; + sig_outputs = outs; + sig_params = params; + sig_loc = loc } + (** @return the set of variables defined in [pat]. *) let vars_pat pat = diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index 4e45bb9..e7c2915 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -26,8 +26,9 @@ let parse parsing_fun lexing_fun lexbuf = let l = Loc(pos1,pos2) in syntax_error l -let parse_implementation lexbuf = - parse Hept_parser.program Hept_lexer.token lexbuf +let parse_implementation modname lexbuf = + let p = parse Hept_parser.program Hept_lexer.token lexbuf in + { p with Hept_parsetree.p_modname = modname } let parse_interface lexbuf = parse Hept_parser.interface Hept_lexer.token lexbuf @@ -35,39 +36,39 @@ let parse_interface lexbuf = let compile_impl pp p = (* Typing *) - let p = do_pass Typing.program "Typing" p pp true in - let p = do_pass Statefull.program "Statefullness check" p pp true in + (*let p = pass "Typing" true Typing.program p pp in*) + let p = silent_pass "Statefullness check" true Statefull.program p in - if !print_types then Interface.Printer.print stdout; + (*if !print_types then Interface.Printer.print stdout;*) (* Causality check *) - let p = do_silent_pass Causality.program "Causality check" p true in + let p = silent_pass "Causality check" true Causality.program p in - (* Initialization check *) - let p = - do_silent_pass Initialization.program "Initialization check" p !init in + (* Initialization check *)(* + let p = silent_pass "Initialization check" !init Initialization.program p in*) (* Completion of partial definitions *) - let p = do_pass Completion.program "Completion" p pp true in + let p = pass "Completion" true Completion.program p pp in + (* Inlining *)(* let p = let call_inline_pass = (List.length !inline > 0) || !Misc.flatten in - do_pass Inline.program "Inlining" p pp call_inline_pass in + pass "Inlining" call_inline_pass Inline.program p pp in *) (* Automata *) - let p = do_pass Automata.program "Automata" p pp true in + (*let p = pass "Automata" true Automata.program p pp in*) (* Present *) - let p = do_pass Present.program "Present" p pp true in + let p = pass "Present" true Present.program p pp in (* Shared variables (last) *) - let p = do_pass Last.program "Last" p pp true in + let p = pass "Last" true Last.program p pp in (* Reset *) - let p = do_pass Reset.program "Reset" p pp true in + let p = pass "Reset" true Reset.program p pp in (* Every *) - let p = do_pass Every.program "Every" p pp true in + let p = pass "Every" true Every.program p pp in (* Return the transformed AST *) p @@ -87,14 +88,14 @@ let compile_interface modname filename = init_compiler modname; (* Parsing of the file *) - let l = parse_interface lexbuf in + let l = do_silent_pass "Parsing" parse_interface lexbuf in (* Convert the parse tree to Heptagon AST *) - let l = Hept_scoping.translate_interface l in + let l = do_silent_pass "Scoping" Hept_scoping.translate_interface l in (* Compile*) - Interface.Type.main l; - if !print_types then Interface.Printer.print stdout; + (*Interface.Type.main l; + if !print_types then Interface.Printer.print stdout;*) Modules.write itc; diff --git a/compiler/heptagon/main/heptcheck.ml b/compiler/heptagon/main/heptcheck.ml index 7ce3a51..977566b 100644 --- a/compiler/heptagon/main/heptcheck.ml +++ b/compiler/heptagon/main/heptcheck.ml @@ -28,17 +28,13 @@ let check_implementation modname filename = init_compiler modname; (* Parsing of the file *) - let p = parse_implementation lexbuf in - comment "Parsing"; + let p = do_silent_pass parse_implementation "Parsing" lexbuf true in (* Convert the parse tree to Heptagon AST *) - let p = Hept_scoping.translate_program p in - comment "Scoping"; - pp p; + let p = do_pass Hept_scoping.translate_program "Scoping" p pp true in (* Call the compiler*) - let p = Hept_compiler.compile_impl pp p in - comment "Checking"; + let p = do_silent_pass Hept_compiler.compile_impl "Checking" p true in close_all_files () diff --git a/compiler/heptagon/parsing/hept_parser.mly b/compiler/heptagon/parsing/hept_parser.mly index 5ccecf1..1e2bf6e 100644 --- a/compiler/heptagon/parsing/hept_parser.mly +++ b/compiler/heptagon/parsing/hept_parser.mly @@ -146,7 +146,7 @@ label_ty_list: ; label_ty: - IDENT COLON ty_ident { ($1, $3) } + IDENT COLON ty_ident { $1, $3 } ; node_decs: @@ -158,14 +158,14 @@ node_dec: | node_or_fun ident node_params LPAREN in_params RPAREN RETURNS LPAREN out_params RPAREN contract b=block(LET) TEL - {{ n_name = $2; - n_statefull = $1; - n_input = $5; - n_output = $9; - n_contract = $11; - n_block = b; - n_params = $3; - n_loc = (Loc($startpos,$endpos)) }} + {{ n_name = $2; + n_statefull = $1; + n_input = $5; + n_output = $9; + n_contract = $11; + n_block = b; + n_params = $3; + n_loc = (Loc($startpos,$endpos)) }} ; node_or_fun: @@ -216,7 +216,7 @@ contract: ; opt_assume: - | /* empty */ { mk_constructor_exp Initial.ptrue (Loc($startpos,$endpos)) } + | /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) } | ASSUME exp { $2 } ; @@ -250,7 +250,7 @@ ident_list: ; ty_ident: - | longname + | qualname { Tid $1 } | ty_ident POWER simple_exp { Tarray ($1, $3) } @@ -293,8 +293,8 @@ _equ: { Epresent(List.rev $3, b) } | IF exp THEN tb=block(DO) ELSE fb=block(DO) END { Eswitch($2, - [{ w_name = Name("true"); w_block = tb }; - { w_name = Name("false"); w_block = fb }]) } + [{ w_name = ptrue; w_block = tb }; + { w_name = pfalse; w_block = fb }]) } | RESET equs EVERY exp { Ereset(mk_block [] $2 (Loc($startpos,$endpos)), $4) } ; @@ -343,7 +343,7 @@ switch_handler: ; constructor_or_bool: - | BOOL { Name(if $1 then "true" else "false") } + | BOOL { if $1 then Q Initial.ptrue else Q Initial.pfalse } | constructor { $1 } switch_handlers: @@ -394,13 +394,13 @@ _simple_exp: | LBRACE field_exp_list RBRACE { Estruct $2 } | LBRACKET array_exp_list RBRACKET { mk_call Earray $2 } | LPAREN tuple_exp RPAREN { mk_call Etuple $2 } - | simple_exp DOT c=longname + | simple_exp DOT c=qualname { mk_call ~params:[mk_constructor_exp c (Loc($startpos(c),$endpos(c)))] Efield [$1] } ; node_name: - | longname call_params { mk_app (Enode $1) $2 } + | qualname call_params { mk_app (Enode $1) $2 } exp: @@ -462,13 +462,13 @@ _exp: | exp AROBASE exp { mk_call Econcat [$1; $3] } /*Iterators*/ - | iterator longname DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN + | iterator qualname DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN { mk_iterator_call $1 $2 [] $4 $7 } - | iterator LPAREN longname DOUBLE_LESS array_exp_list DOUBLE_GREATER + | iterator LPAREN qualname DOUBLE_LESS array_exp_list DOUBLE_GREATER RPAREN DOUBLE_LESS simple_exp DOUBLE_GREATER LPAREN exps RPAREN { mk_iterator_call $1 $3 $5 $9 $12 } /*Records operators */ - | LBRACE simple_exp WITH DOT c=longname EQUAL exp RBRACE + | LBRACE simple_exp WITH DOT c=qualname EQUAL exp RBRACE { mk_call ~params:[mk_constructor_exp c (Loc($startpos(c),$endpos(c)))] Efield_update [$2; $7] } ; @@ -491,24 +491,24 @@ indexes: ; constructor: - | Constructor { Name($1) } %prec prec_ident - | Constructor DOT Constructor { Modname({qual = $1; id = $3}) } + | Constructor { ToQ $1 } %prec prec_ident + | Constructor DOT Constructor { Q {qual = $1; name = $3} } ; -longname: - | ident { Name($1) } - | Constructor DOT ident { Modname({qual = $1; id = $3}) } +qualname: + | ident { ToQ $1 } + | Constructor DOT ident { Q {qual = $1; name = $3} } ; -const: c=_const { mk_static_exp c ~loc:(Loc($startpos,$endpos)) } +const: c=_const { mk_static_exp c (Loc($startpos,$endpos)) } _const: | INT { Sint $1 } | FLOAT { Sfloat $1 } | BOOL { Sbool $1 } | constructor { Sconstructor $1 } | Constructor DOT ident - { Svar (Modname({qual = $1; id = $3})) } + { Svar (Q {qual = $1; name = $3}) } ; tuple_exp: @@ -527,7 +527,7 @@ array_exp_list: ; field_exp: - | longname EQUAL exp { ($1, $3) } + | qualname EQUAL exp { ($1, $3) } ; /* identifiers */ @@ -569,10 +569,11 @@ _interface_decl: | VAL node_or_fun ident node_params LPAREN params_signature RPAREN RETURNS LPAREN params_signature RPAREN { Isignature({ sig_name = $3; - sig_inputs = $6; - sig_statefull = $2; - sig_outputs = $10; - sig_params = $4; }) } + sig_inputs = $6; + sig_statefull = $2; + sig_outputs = $10; + sig_params = $4; + sig_loc = (Loc($startpos,$endpos)) }) } ; params_signature: diff --git a/compiler/heptagon/parsing/hept_parsetree.ml b/compiler/heptagon/parsing/hept_parsetree.ml index 8a8da46..ddec0bd 100644 --- a/compiler/heptagon/parsing/hept_parsetree.ml +++ b/compiler/heptagon/parsing/hept_parsetree.ml @@ -13,6 +13,31 @@ open Location open Signature open Types +type qualname = + | Q of Names.qualname (* already qualified name *) + | ToQ of name (* name to qualify in the scoping process *) + +type type_name = qualname +type fun_name = qualname +type field_name = qualname +type constructor_name = qualname +type constant_name = qualname +type module_name = name + +type static_exp = { se_desc: static_exp_desc; se_ty: ty; se_loc: location } + +and static_exp_desc = + | Svar of constant_name + | Sint of int + | Sfloat of float + | Sbool of bool + | Sconstructor of constructor_name + | Stuple of static_exp list + | Sarray_power of static_exp * static_exp (** power : 0^n : [0,0,0,0,0,..] *) + | Sarray of static_exp list (** [ e1, e2, e3 ] *) + | Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *) + | Sop of fun_name * static_exp list (** defined ops for now in pervasives *) + type iterator_type = | Imap | Ifold @@ -21,7 +46,7 @@ type iterator_type = type ty = | Tprod of ty list - | Tid of longname + | Tid of qualname | Tarray of ty * exp and exp = @@ -34,7 +59,7 @@ and desc = | Elast of name | Epre of exp option * exp | Efby of exp * exp - | Estruct of (longname * exp) list + | Estruct of (qualname * exp) list | Eapp of app * exp list | Eiterator of iterator_type * app * exp * exp list @@ -43,8 +68,8 @@ and app = { a_op: op; a_params: exp list; } and op = | Eequal | Etuple - | Enode of longname - | Efun of longname + | Enode of qualname + | Efun of qualname | Eifthenelse | Earrow | Efield @@ -89,7 +114,7 @@ and escape = e_next_state : name; } and switch_handler = - { w_name : longname; + { w_name : constructor_name; w_block : block; } and present_handler = @@ -148,11 +173,12 @@ type program = type arg = { a_type : ty; a_name : name option } type signature = - { sig_name : name; - sig_inputs : arg list; + { sig_name : name; + sig_inputs : arg list; sig_statefull : bool; - sig_outputs : arg list; - sig_params : var_dec list; } + sig_outputs : arg list; + sig_params : var_dec list; + sig_loc : location } type interface = interface_decl list @@ -178,13 +204,16 @@ let mk_call ?(params=[]) op exps = let mk_op_call ?(params=[]) s exps = mk_call ~params:params - (Efun (Modname { qual = "Pervasives"; id = s })) exps + (Efun (Q { qual = "Pervasives"; name = s })) exps let mk_iterator_call it ln params n exps = Eiterator (it, mk_app (Enode ln) params, n, exps) +let mk_static_exp ?(ty = invalid_type) desc loc = + { se_desc = desc; se_ty = ty; se_loc = loc } + let mk_constructor_exp f loc = - mk_exp (Econst (mk_static_exp (Sconstructor f))) loc + mk_exp (Econst (mk_static_exp (Sconstructor f) loc)) loc let mk_type_dec name desc loc = { t_name = name; t_desc = desc; t_loc = loc } @@ -204,9 +233,12 @@ let mk_block locals eqs loc = b_loc = loc } let mk_const_dec id ty e loc = - { c_name = id; c_type = ty; c_value = e; - c_loc = loc } + { c_name = id; c_type = ty; c_value = e; c_loc = loc } let mk_arg name ty = { a_type = ty; a_name = name } + + +let ptrue = Q Initial.ptrue +let pfalse = Q Initial.pfalse diff --git a/compiler/heptagon/parsing/hept_scoping.ml b/compiler/heptagon/parsing/hept_scoping.ml index f3ca5dd..8b6b785 100644 --- a/compiler/heptagon/parsing/hept_scoping.ml +++ b/compiler/heptagon/parsing/hept_scoping.ml @@ -1,6 +1,28 @@ (** Scoping. Introduces unique indexes for local names and replace global names by qualified names *) + +(* [local_const] is the environnement with local constant variables, + that is for now only the statics node parameters. + It is built with [build_const]. + When qualifying a constant var, + it is first check in the local_const env, so qualified with [local_qn] + if not found we try to qualify with the global env. *) + +(* The global environement is initialized by the scoping pass. + This allow at the same time + to qualify types, constants, constructors, fields and node calls, + according to the current module definitions and opened modules. *) + +(* [env] of type Rename.t is the renaming environnement + used to map a var name to a var ident. + It is initialized at node declaration level with the inputs and outputs, + and then appended with the local var declarations at each block level + with the [build] function. *) + +(* convention : static params are set as the first static args, + op (a3) == op (a2,a3) == op (a1,a2,a3) *) + open Location open Types open Hept_parsetree @@ -8,27 +30,38 @@ open Names open Idents open Format open Static +open Global_printer open Modules module Error = struct type error = - | Evar of string - | Econst_var of string - | Evariable_already_defined of string - | Econst_variable_already_defined of string + | EvarUnbound of name + | EqualUnbound of qualname + | Econst_var of name + | Enotlast of name + | Evariable_already_defined of name + | Econst_variable_already_defined of name | Estatic_exp_expected let message loc kind = begin match kind with - | Evar name -> + | EvarUnbound name -> eprintf "%aThe value identifier %s is unbound.@." print_location loc name + |EqualUnbound q -> + eprintf "%aThe qualified name %a can't be found.@." + print_location loc + print_qualname q | Econst_var name -> eprintf "%aThe const identifier %s is unbound.@." print_location loc name + | Enotlast name -> + eprintf "%aThe variable identifier %s should be declared as a last.@." + print_location loc + name | Evariable_already_defined name -> eprintf "%aThe variable %s is already defined.@." print_location loc @@ -42,140 +75,199 @@ struct print_location loc end; raise Misc.Error + + exception ScopingError of error + + let error kind = raise (ScopingError(kind)) end +open Error + + +(** { 3 qualify when ToQ and check when Q according to the global env } *) + +let _qualify_with_error qfun cqfun q = match q with + | ToQ name -> + (*TODO good error*) + (try qfun name with Not_found -> error (EvarUnbound name)) + | Q q -> + if cqfun q then q else error (EqualUnbound q) + +let qualify_value = _qualify_with_error qualify_value check_value +let qualify_type = _qualify_with_error qualify_type check_type +let qualify_constrs = _qualify_with_error qualify_constrs check_constrs +let qualify_field = _qualify_with_error qualify_field check_field + +(** Qualify with [Names.local_qualname] when in local_const, + otherwise qualify according to the global env *) +let qualify_const local_const c = match c with + | ToQ c -> + if S.mem c local_const + then local_qn c + else (try qualify_const c with Not_found -> raise Not_static) + | Q q -> + if check_const q then q else raise Not_static + + module Rename = struct + open Error include (Map.Make (struct type t = string let compare = String.compare end)) - let append env0 env = - fold (fun key v env -> add key v env) env0 env - - let name loc env n = + (** Rename a var *) + let var loc env n = + try fst (find n env) + with Not_found -> message loc (EvarUnbound n) + (** Rename a last *) + let last loc env n = try - find n env - with - Not_found -> Error.message loc (Error.Evar(n)) + let id, last = find n env in + if not last then message loc (Enotlast n) else id + with Not_found -> message loc (EvarUnbound n) + (** Add a var *) + let add_var loc env n = + if mem n env then message loc (Evariable_already_defined n) + else (* create a new id for this var and add it to the env *) + add n (ident_of_name n, false) env + (** Add a last *) + let add_last loc env n = + if mem n env then message loc (Evariable_already_defined n) + else (* create a new id for this var and add it to the env *) + add n (ident_of_name n, true) env + (** Add a var dec *) + let add env vd = + let add = match vd.v_last with + | Var -> add_var + | Last _ -> add_last in + add vd.v_loc env vd.v_name + (** Append a list of var dec *) + let append env vd_list = List.fold_left add env vd_list end -(*Functions to build the renaming map*) -let add_var loc x env = - if Rename.mem x env then - Error.message loc (Error.Evariable_already_defined x) - else (* create a new id for this var and add it to the env *) - Rename.add x (ident_of_name x) env - -let add_const_var loc x env = - if NamesEnv.mem x env then - Error.message loc (Error.Econst_variable_already_defined x) - else (* create a new id for this var and add it to the env *) - NamesEnv.add x x env - -let build_vd_list env l = - let build_vd env vd = - add_var vd.v_loc vd.v_name env - in - List.fold_left build_vd env l - -let build_cd env cd = - add_const_var cd.c_loc cd.c_name env - -let build_id_list loc env l = - let build_id env vd = - add_const_var loc vd.v_name env - in - List.fold_left build_id env l - -(* Translate the AST into Heptagon. *) + +(** Function to build the defined static parameters set *) +let build_const loc vd_list = + let _add_const_var loc c local_const = + if S.mem c local_const + then Error.message loc (Error.Econst_variable_already_defined c) + else S.add c local_const in + let build local_const vd = + _add_const_var loc vd.v_name local_const in + List.fold_left build S.empty vd_list + + +(** { 3 Translate the AST into Heptagon. } *) let translate_iterator_type = function | Imap -> Heptagon.Imap | Ifold -> Heptagon.Ifold | Ifoldi -> Heptagon.Ifoldi | Imapfold -> Heptagon.Imapfold -let op_from_app loc app = +(** convention : static params are set as the first static args, + op (a3) == op (a2,a3) == op (a1,a2,a3) *) +let static_app_from_app app args= match app.a_op with - | Efun op | Enode op -> op_from_app_name op + | Efun (Q ({ qual = "pervasives" } as q)) + | Enode (Q ({ qual = "pervasives" } as q)) -> + q, (app.a_params @ args) | _ -> raise Not_static -let rec static_exp_of_exp const_env e = - let desc = match e.e_desc with - | Evar n -> - if NamesEnv.mem n const_env then - Svar (Name n) - else - (try - let { qualid = q } = find_const (Name n) in - Svar (Modname q) - with Not_found -> raise Not_static) - | Econst se -> se.se_desc - | Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) -> - Sarray_power (static_exp_of_exp const_env e, - static_exp_of_exp const_env n) - | Eapp({ a_op = Earray }, e_list) -> - Sarray (List.map (static_exp_of_exp const_env) e_list) - | Eapp({ a_op = Etuple }, e_list) -> - Stuple (List.map (static_exp_of_exp const_env) e_list) - | Eapp(app, e_list) -> - let op = op_from_app e.e_loc app in - Sop(op, List.map (static_exp_of_exp const_env) e_list) - | Estruct e_list -> - Srecord (List.map (fun (f,e) -> f, - static_exp_of_exp const_env e) e_list) - | _ -> raise Not_static - in - mk_static_exp ~loc:e.e_loc desc +let rec translate_static_exp local_const se = + try + let se_d = translate_static_exp_desc local_const se.se_desc in + Types.mk_static_exp ~loc:se.se_loc se_d + with + | ScopingError err -> message se.se_loc err + +and translate_static_exp_desc local_const ed = + let t = translate_static_exp local_const in + match ed with + | Svar q -> Types.Svar (qualify_const local_const q) + | Sint i -> Types.Sint i + | Sfloat f -> Types.Sfloat f + | Sbool b -> Types.Sbool b + | Sconstructor c -> Types.Sconstructor (qualify_constrs c) + | Stuple se_list -> Types.Stuple (List.map t se_list) + | Sarray_power (se,sn) -> Types.Sarray_power (t se, t sn) + | Sarray se_list -> Types.Sarray (List.map t se_list) + | Srecord se_f_list -> + let qualf (f, se) = (qualify_field f, t se) in + Types.Srecord (List.map qualf se_f_list) + | Sop (fn, se_list) -> Types.Sop (qualify_value fn, List.map t se_list) + +let rec static_exp_of_exp local_const e = + try + let t = static_exp_of_exp local_const in + let desc = match e.e_desc with + | Evar n -> Types.Svar (qualify_const local_const (ToQ n)) + | Econst se -> translate_static_exp_desc local_const se.se_desc + | Eapp({ a_op = Earray_fill; a_params = [n] }, [e]) -> + Types.Sarray_power (t e, t n) + | Eapp({ a_op = Earray }, e_list) -> + Types.Sarray (List.map t e_list) + | Eapp({ a_op = Etuple }, e_list) -> + Types.Stuple (List.map t e_list) + | Eapp(app, e_list) -> + let op, args = static_app_from_app app e_list in + Types.Sop (op, List.map t args) + | Estruct e_list -> + Types.Srecord (List.map (fun (f,e) -> qualify_field f, t e) e_list) + | _ -> raise Not_static in + Types.mk_static_exp ~loc:e.e_loc desc + with + | ScopingError err -> message e.e_loc err + +let expect_static_exp local_const e = + try static_exp_of_exp local_const e + with Not_static -> message e.e_loc Estatic_exp_expected -let expect_static_exp const_env e = +let rec translate_type loc local_const ty = try - static_exp_of_exp const_env e + (match ty with + | Tprod ty_list -> + Types.Tprod(List.map (translate_type loc local_const) ty_list) + | Tid ln -> Types.Tid (qualify_type ln) + | Tarray (ty, e) -> + let ty = translate_type loc local_const ty in + Types.Tarray (ty, expect_static_exp local_const e)) with - Not_static -> Error.message e.e_loc Error.Estatic_exp_expected + | ScopingError err -> message loc err -let rec translate_type const_env = function - | Tprod ty_list -> Types.Tprod(List.map (translate_type const_env) ty_list) - | Tid ln -> Types.Tid ln - | Tarray (ty, e) -> - let ty = translate_type const_env ty in - Types.Tarray (ty, expect_static_exp const_env e) -and translate_exp const_env env e = +and translate_exp local_const env e = let desc = try (* try to see if the exp is a constant *) - Heptagon.Econst (static_exp_of_exp const_env e) + Heptagon.Econst (static_exp_of_exp local_const e) with - Not_static -> translate_desc e.e_loc const_env env e.e_desc in + Not_static -> translate_desc e.e_loc local_const env e.e_desc in { Heptagon.e_desc = desc; Heptagon.e_ty = Types.invalid_type; Heptagon.e_loc = e.e_loc } -and translate_desc loc const_env env = function - | Econst c -> Heptagon.Econst c - | Evar x -> - if Rename.mem x env then (* defined var *) - Heptagon.Evar (Rename.name loc env x) - else (* undefined var *) - Error.message loc (Error.Evar x) - | Elast x -> Heptagon.Elast (Rename.name loc env x) - | Epre (None, e) -> Heptagon.Epre (None, translate_exp const_env env e) +and translate_desc loc local_const env = function + | Econst c -> Heptagon.Econst (translate_static_exp local_const c) + | Evar x -> Heptagon.Evar (Rename.var loc env x) + | Elast x -> Heptagon.Elast (Rename.last loc env x) + | Epre (None, e) -> Heptagon.Epre (None, translate_exp local_const env e) | Epre (Some c, e) -> - Heptagon.Epre (Some (expect_static_exp const_env c), - translate_exp const_env env e) - | Efby (e1, e2) -> Heptagon.Efby (translate_exp const_env env e1, - translate_exp const_env env e2) + Heptagon.Epre (Some (expect_static_exp local_const c), + translate_exp local_const env e) + | Efby (e1, e2) -> Heptagon.Efby (translate_exp local_const env e1, + translate_exp local_const env e2) | Estruct f_e_list -> let f_e_list = - List.map (fun (f,e) -> f, translate_exp const_env env e) f_e_list in + List.map (fun (f,e) -> qualify_field f, translate_exp local_const env e) + f_e_list in Heptagon.Estruct f_e_list | Eapp ({ a_op = op; a_params = params }, e_list) -> - let e_list = List.map (translate_exp const_env env) e_list in - let params = List.map (expect_static_exp const_env) params in + let e_list = List.map (translate_exp local_const env) e_list in + let params = List.map (expect_static_exp local_const) params in let app = Heptagon.mk_op ~params:params (translate_op op) in Heptagon.Eapp (app, e_list, None) | Eiterator (it, { a_op = op; a_params = params }, n, e_list) -> - let e_list = List.map (translate_exp const_env env) e_list in - let n = expect_static_exp const_env n in - let params = List.map (expect_static_exp const_env) params in + let e_list = List.map (translate_exp local_const env) e_list in + let n = expect_static_exp local_const n in + let params = List.map (expect_static_exp local_const) params in let app = Heptagon.mk_op ~params:params (translate_op op) in Heptagon.Eiterator (translate_iterator_type it, app, n, e_list, None) @@ -194,161 +286,183 @@ and translate_op = function | Eselect_slice -> Heptagon.Eselect_slice | Econcat -> Heptagon.Econcat | Eselect_dyn -> Heptagon.Eselect_dyn - | Efun ln -> Heptagon.Efun ln - | Enode ln -> Heptagon.Enode ln + | Efun ln -> Heptagon.Efun (qualify_value ln) + | Enode ln -> Heptagon.Enode (qualify_value ln) and translate_pat loc env = function - | Evarpat x -> Heptagon.Evarpat (Rename.name loc env x) + | Evarpat x -> Heptagon.Evarpat (Rename.var loc env x) | Etuplepat l -> Heptagon.Etuplepat (List.map (translate_pat loc env) l) -let rec translate_eq const_env env eq = - { Heptagon.eq_desc = translate_eq_desc eq.eq_loc const_env env eq.eq_desc ; +let rec translate_eq local_const env eq = + { Heptagon.eq_desc = translate_eq_desc eq.eq_loc local_const env eq.eq_desc ; Heptagon.eq_statefull = false; Heptagon.eq_loc = eq.eq_loc } -and translate_eq_desc loc const_env env = function +and translate_eq_desc loc local_const env = function | Eswitch(e, switch_handlers) -> let sh = List.map - (translate_switch_handler loc const_env env) + (translate_switch_handler loc local_const env) switch_handlers in - Heptagon.Eswitch (translate_exp const_env env e, sh) + Heptagon.Eswitch (translate_exp local_const env e, sh) | Eeq(p, e) -> - Heptagon.Eeq (translate_pat loc env p, translate_exp const_env env e) + Heptagon.Eeq (translate_pat loc env p, translate_exp local_const env e) | Epresent (present_handlers, b) -> Heptagon.Epresent - (List.map (translate_present_handler const_env env) present_handlers - , fst (translate_block const_env env b)) + (List.map (translate_present_handler local_const env) present_handlers + , fst (translate_block local_const env b)) | Eautomaton state_handlers -> - Heptagon.Eautomaton (List.map (translate_state_handler const_env env) + Heptagon.Eautomaton (List.map (translate_state_handler local_const env) state_handlers) | Ereset (b, e) -> - let b, _ = translate_block const_env env b in - Heptagon.Ereset (b, translate_exp const_env env e) - -and translate_block const_env env b = - let env = build_vd_list env b.b_local in - { Heptagon.b_local = translate_vd_list const_env env b.b_local; - Heptagon.b_equs = List.map (translate_eq const_env env) b.b_equs; - Heptagon.b_defnames = Env.empty ; + let b, _ = translate_block local_const env b in + Heptagon.Ereset (b, translate_exp local_const env e) + +and translate_block local_const env b = + let env = Rename.append env b.b_local in + { Heptagon.b_local = translate_vd_list local_const env b.b_local; + Heptagon.b_equs = List.map (translate_eq local_const env) b.b_equs; + Heptagon.b_defnames = Env.empty; Heptagon.b_statefull = false; Heptagon.b_loc = b.b_loc }, env -and translate_state_handler const_env env sh = - let b, env = translate_block const_env env sh.s_block in +and translate_state_handler local_const env sh = + let b, env = translate_block local_const env sh.s_block in { Heptagon.s_state = sh.s_state; Heptagon.s_block = b; - Heptagon.s_until = List.map (translate_escape const_env env) sh.s_until; - Heptagon.s_unless = List.map (translate_escape const_env env) sh.s_unless; } + Heptagon.s_until = List.map (translate_escape local_const env) sh.s_until; + Heptagon.s_unless = + List.map (translate_escape local_const env) sh.s_unless; } -and translate_escape const_env env esc = - { Heptagon.e_cond = translate_exp const_env env esc.e_cond; +and translate_escape local_const env esc = + { Heptagon.e_cond = translate_exp local_const env esc.e_cond; Heptagon.e_reset = esc.e_reset; Heptagon.e_next_state = esc.e_next_state } -and translate_present_handler const_env env ph = - { Heptagon.p_cond = translate_exp const_env env ph.p_cond; - Heptagon.p_block = fst (translate_block const_env env ph.p_block) } +and translate_present_handler local_const env ph = + { Heptagon.p_cond = translate_exp local_const env ph.p_cond; + Heptagon.p_block = fst (translate_block local_const env ph.p_block) } -and translate_switch_handler loc const_env env sh = - { Heptagon.w_name = sh.w_name; - Heptagon.w_block = fst (translate_block const_env env sh.w_block) } +and translate_switch_handler loc local_const env sh = + try + { Heptagon.w_name = qualify_constrs sh.w_name; + Heptagon.w_block = fst (translate_block local_const env sh.w_block) } + with + | ScopingError err -> message loc err -and translate_var_dec const_env env vd = - { Heptagon.v_ident = Rename.name vd.v_loc env vd.v_name; - Heptagon.v_type = translate_type const_env vd.v_type; - Heptagon.v_last = translate_last const_env env vd.v_last; - Heptagon.v_loc = vd.v_loc } +and translate_var_dec local_const env vd = + (* env is initialized with the declared vars before their translation *) + { Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name; + Heptagon.v_type = translate_type vd.v_loc local_const vd.v_type; + Heptagon.v_last = translate_last local_const vd.v_last; + Heptagon.v_loc = vd.v_loc } -and translate_vd_list const_env env = - List.map (translate_var_dec const_env env) +and translate_vd_list local_const env = + List.map (translate_var_dec local_const env) -and translate_last const_env env = function +and translate_last local_const = function | Var -> Heptagon.Var | Last (None) -> Heptagon.Last None - | Last (Some e) -> Heptagon.Last (Some (expect_static_exp const_env e)) + | Last (Some e) -> Heptagon.Last (Some (expect_static_exp local_const e)) -let translate_contract const_env env ct = - let b, _ = translate_block const_env env ct.c_block in - { Heptagon.c_assume = translate_exp const_env env ct.c_assume; - Heptagon.c_enforce = translate_exp const_env env ct.c_enforce; +let translate_contract local_const env ct = + let b, _ = translate_block local_const env ct.c_block in + { Heptagon.c_assume = translate_exp local_const env ct.c_assume; + Heptagon.c_enforce = translate_exp local_const env ct.c_enforce; Heptagon.c_block = b } -let param_of_var_dec const_env vd = - Signature.mk_param vd.v_name (translate_type const_env vd.v_type) - -let translate_node const_env env node = - let const_env = build_id_list node.n_loc const_env node.n_params in - let env = build_vd_list env (node.n_input @ node.n_output) in - let b, env = translate_block const_env env node.n_block in - { Heptagon.n_name = node.n_name; +let params_of_var_decs local_const = + List.map (fun vd -> Signature.mk_param + vd.v_name + (translate_type vd.v_loc local_const vd.v_type)) + +let translate_node node = + (* Node's params go to local_const env *) + let local_const = build_const node.n_loc node.n_params in + (* Inputs and outputs define the initial local env *) + let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in + let b, env = translate_block local_const env0 node.n_block in + (* the env of the block is used in the contract translation *) + let n = current_qual node.n_name in + { Heptagon.n_name = n; Heptagon.n_statefull = node.n_statefull; - Heptagon.n_input = translate_vd_list const_env env node.n_input; - Heptagon.n_output = translate_vd_list const_env env node.n_output; - Heptagon.n_contract = Misc.optional - (translate_contract const_env env) node.n_contract; + Heptagon.n_input = translate_vd_list local_const env0 node.n_input; + Heptagon.n_output = translate_vd_list local_const env0 node.n_output; + Heptagon.n_contract = + Misc.optional (translate_contract local_const env) node.n_contract; Heptagon.n_block = b; Heptagon.n_loc = node.n_loc; - Heptagon.n_params = List.map (param_of_var_dec const_env) node.n_params; + Heptagon.n_params = params_of_var_decs local_const node.n_params; Heptagon.n_params_constraints = []; } -let translate_typedec const_env ty = - let onetype = function - | Type_abs -> Heptagon.Type_abs - | Type_alias ty -> Heptagon.Type_alias (translate_type const_env ty) - | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list) - | Type_struct(field_ty_list) -> - let translate_field_type (f,ty) = - Signature.mk_field f (translate_type const_env ty) in - Heptagon.Type_struct (List.map translate_field_type field_ty_list) - in - { Heptagon.t_name = ty.t_name; - Heptagon.t_desc = onetype ty.t_desc; - Heptagon.t_loc = ty.t_loc } - -let translate_const_dec const_env cd = - { Heptagon.c_name = cd.c_name; - Heptagon.c_type = translate_type const_env cd.c_type; - Heptagon.c_value = expect_static_exp const_env cd.c_value; - Heptagon.c_loc = cd.c_loc; }, build_cd const_env cd +let translate_typedec ty = + let n = current_qual ty.t_name in + let tydesc = match ty.t_desc with + | Type_abs -> + add_type n Signature.Tabstract; + Heptagon.Type_abs + | Type_alias t -> + let t = translate_type ty.t_loc S.empty t in + add_type n (Signature.Talias t); + Heptagon.Type_alias t + | Type_enum(tag_list) -> + let tag_list = List.map current_qual tag_list in + List.iter (fun tag -> add_constrs tag n) tag_list; + add_type n (Signature.Tenum tag_list); + Heptagon.Type_enum tag_list + | Type_struct(field_ty_list) -> + let translate_field_type (f,t) = + let f = current_qual f in + let t = translate_type ty.t_loc S.empty t in + add_field f n; + Signature.mk_field f t in + let field_list = List.map translate_field_type field_ty_list in + add_type n (Signature.Tstruct field_list); + Heptagon.Type_struct field_list in + { Heptagon.t_name = n; + Heptagon.t_desc = tydesc; + Heptagon.t_loc = ty.t_loc } + + +let translate_const_dec cd = + let c_name = current_qual cd.c_name in + let c_type = translate_type cd.c_loc S.empty cd.c_type in + let c_value = expect_static_exp S.empty cd.c_value in + add_const c_name (Signature.mk_const_def c_type c_value); + { Heptagon.c_name = c_name; + Heptagon.c_type = c_type; + Heptagon.c_value = c_value; + Heptagon.c_loc = cd.c_loc; } let translate_program p = List.iter open_module p.p_opened; - let p_consts, const_env = - Misc.mapfold translate_const_dec NamesEnv.empty p.p_consts in { Heptagon.p_modname = p.p_modname; Heptagon.p_opened = p.p_opened; - Heptagon.p_types = List.map (translate_typedec const_env) p.p_types; - Heptagon.p_nodes = - List.map (translate_node const_env Rename.empty) p.p_nodes; - Heptagon.p_consts = p_consts; } - -let translate_arg const_env a = - Signature.mk_arg a.a_name (translate_type const_env a.a_type) + Heptagon.p_types = List.map translate_typedec p.p_types; + Heptagon.p_nodes = List.map translate_node p.p_nodes; + Heptagon.p_consts = List.map translate_const_dec p.p_consts; } let translate_signature s = - let const_env = build_id_list no_location NamesEnv.empty s.sig_params in - { Heptagon.sig_name = s.sig_name; - Heptagon.sig_inputs = List.map (translate_arg const_env) s.sig_inputs; - Heptagon.sig_outputs = List.map (translate_arg const_env) s.sig_outputs; - Heptagon.sig_statefull = s.sig_statefull; - Heptagon.sig_params = List.map (param_of_var_dec const_env) s.sig_params; } - -let translate_interface_desc const_env = function - | Iopen n -> Heptagon.Iopen n, const_env - | Itypedef tydec -> - Heptagon.Itypedef (translate_typedec const_env tydec), const_env - | Iconstdef const_dec -> - let const_dec, const_env = translate_const_dec const_env const_dec in - Heptagon.Iconstdef const_dec, const_env - | Isignature s -> Heptagon.Isignature (translate_signature s) , const_env - -let translate_interface_decl const_env idecl = - let desc, const_env = - translate_interface_desc const_env idecl.interf_desc in + let local_const = build_const s.sig_loc s.sig_params in + let translate_arg a = + Signature.mk_arg a.a_name (translate_type s.sig_loc local_const a.a_type) in + let n = current_qual s.sig_name in + let i = List.map translate_arg s.sig_inputs in + let o = List.map translate_arg s.sig_outputs in + let p = params_of_var_decs local_const s.sig_params in + add_value n (Signature.mk_node i o s.sig_statefull p); + Heptagon.mk_signature n i o s.sig_statefull p s.sig_loc + + +let translate_interface_desc = function + | Iopen n -> open_module n; Heptagon.Iopen n + | Itypedef tydec -> Heptagon.Itypedef (translate_typedec tydec) + | Iconstdef const_dec -> Heptagon.Iconstdef (translate_const_dec const_dec) + | Isignature s -> Heptagon.Isignature (translate_signature s) + +let translate_interface_decl idecl = + let desc = translate_interface_desc idecl.interf_desc in { Heptagon.interf_desc = desc; - Heptagon.interf_loc = idecl.interf_loc }, const_env + Heptagon.interf_loc = idecl.interf_loc } -let translate_interface i = - let i, _ = Misc.mapfold translate_interface_decl NamesEnv.empty i in - i +let translate_interface i = List.map translate_interface_decl i diff --git a/compiler/heptagon/transformations/automata.ml b/compiler/heptagon/transformations/automata.ml index 45fa2d7..d352993 100644 --- a/compiler/heptagon/transformations/automata.ml +++ b/compiler/heptagon/transformations/automata.ml @@ -48,7 +48,7 @@ let intro_type states = let state_type = "st" ^ n in state_type_dec_list := (mk_type_dec state_type (Type_enum (list states))) :: !state_type_dec_list; - Name(state_type) + current_qual state_type (** Allows to classify an automaton : Moore automatons doesn't have strong transitions, diff --git a/compiler/main/hept2mls.ml b/compiler/main/hept2mls.ml index 42a231f..792a9ad 100644 --- a/compiler/main/hept2mls.ml +++ b/compiler/main/hept2mls.ml @@ -389,8 +389,7 @@ let typedec | Heptagon.Type_abs -> Type_abs | Heptagon.Type_alias ln -> Type_alias ln | Heptagon.Type_enum tag_list -> Type_enum tag_list - | Heptagon.Type_struct field_ty_list -> - Type_struct field_ty_list + | Heptagon.Type_struct field_ty_list -> Type_struct field_ty_list in { t_name = n; t_desc = onetype tdesc; t_loc = loc } diff --git a/compiler/main/heptc.ml b/compiler/main/heptc.ml index 19fd07a..200cf68 100644 --- a/compiler/main/heptc.ml +++ b/compiler/main/heptc.ml @@ -9,9 +9,10 @@ open Misc +open Modules open Location open Compiler_utils - +open Hept_compiler @@ -35,31 +36,22 @@ let compile_impl modname filename = init_compiler modname; add_include (Filename.dirname filename); - (* Set pretty printer to the Heptagon one *) - let pp = Hept_compiler.pp in - (* Parsing of the file *) - let p = Hept_compiler.parse_implementation lexbuf in - let p = { p with Hept_parsetree.p_modname = modname } in - comment "Parsing"; + let p = do_silent_pass "Parsing" (parse_implementation modname) lexbuf in (* Convert the parse tree to Heptagon AST *) - let p = Hept_scoping.translate_program p in - comment "Scoping"; - pp p; + let p = do_pass "Scoping" Hept_scoping.translate_program p pp in (* Process the Heptagon AST *) - let p = Hept_compiler.compile_impl pp p in - Modules.write itc; + let p = compile_impl pp p in + Modules.write_current_module itc; (* Set pretty printer to the Minils one *) let pp = Mls_compiler.pp in (* Compile Heptagon to MiniLS *) - let p = Hept2mls.program p in + let p = do_pass "Translation into MiniLs" Hept2mls.program p pp in Mls_printer.print mlsc p; - comment "Translation into MiniLs"; - pp p; (* Process the MiniLS AST *) let p = Mls_compiler.compile pp p in @@ -69,9 +61,7 @@ let compile_impl modname filename = close_all_files () - with - | x -> close_all_files (); raise x - + with x -> close_all_files (); raise x let main () = @@ -95,7 +85,7 @@ let main () = "-noinit", Arg.Clear init, doc_noinit; "-fti", Arg.Set full_type_info, doc_full_type_info; ] - (Hept_compiler.compile compile_impl) + (compile compile_impl) errmsg; with | Misc.Error -> exit 2;; diff --git a/compiler/main/mls2obc.ml b/compiler/main/mls2obc.ml index d5e1d82..85a41d9 100644 --- a/compiler/main/mls2obc.ml +++ b/compiler/main/mls2obc.ml @@ -26,7 +26,7 @@ let static_exp_of_int i = let gen_obj_name n = (shortname n) ^ "_mem" ^ (gen_symbol ()) -let op_from_string op = Modname { qual = "Pervasives"; id = op; } +let op_from_string op = { qual = "Pervasives"; name = op; } let rec lhs_of_idx_list e = function | [] -> e | idx :: l -> mk_lhs (Larray (lhs_of_idx_list e l, idx)) @@ -206,8 +206,8 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } let vf = translate_var_dec map vf in let vt = translate_var_dec map vt in let action = - Acase (cond, [Name "true", mk_block ~locals:vt true_act; - Name "false", mk_block ~locals:vf false_act]) in + Acase (cond, [ptrue, mk_block ~locals:vt true_act; + pfalse, mk_block ~locals:vf false_act]) in v, si, j, (control map ck action) :: s | Minils.Evarpat x, @@ -251,8 +251,8 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } Aassgn (x, mk_exp (Elhs (lhs_of_idx_list (lhs_of_exp e1) idx))) in let false_act = Aassgn (x, translate map (si, j, s) e2) in let cond = bound_check_expr idx bounds in - let action = Acase (cond, [ Name "true", mk_block [true_act]; - Name "false", mk_block [false_act] ]) in + let action = Acase (cond, [ ptrue, mk_block [true_act]; + pfalse, mk_block [false_act] ]) in v, si, j, (control map ck action) :: s | Minils.Evarpat x, @@ -264,7 +264,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e } let action = Aassgn (lhs_of_idx_list x idx, translate map (si, j, s) e2) in let cond = bound_check_expr idx bounds in - let action = Acase (cond, [ Name "true", mk_block [action] ]) in + let action = Acase (cond, [ ptrue, mk_block [action] ]) in let copy = Aassgn (x, translate map (si, j, s) e1) in v, si, j, (control map ck copy) :: (control map ck action) :: s @@ -327,7 +327,7 @@ and mk_node_call map call_context app loc name_list args = let e = mk_exp (Eop(f, args)) in [], [], [], [Aassgn(List.hd name_list, e) ] - | Minils.Enode f when Itfusion.is_anon_node f -> + | Minils.Enode f when Itfusion.is_anon_node f -> let add_input env vd = Env.add vd.Minils.v_ident (mk_lhs (Lvar vd.Minils.v_ident)) env in let build env vd a = @@ -346,7 +346,7 @@ and mk_node_call map call_context app loc name_list args = act_list in - let nd = Itfusion.find_anon_node f in + let nd = Itfusion.find_anon_node f in let map = List.fold_left add_input map nd.Minils.n_input in let map = List.fold_left2 build map nd.Minils.n_output name_list in let map = List.fold_left add_input map nd.Minils.n_local in @@ -480,24 +480,24 @@ let translate_node let resetm = { m_name = Mreset; m_inputs = []; m_outputs = []; m_body = mk_block si } in - { cd_name = f; cd_mems = m; cd_params = params; + { cd_name = shortname f; cd_mems = m; cd_params = params; cd_objs = j; cd_methods = [stepm; resetm]; cd_loc = loc } let translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc; Minils.t_loc = loc } = - let tdesc = - match tdesc with - | Minils.Type_abs -> Type_abs - | Minils.Type_alias ln -> Type_alias ln - | Minils.Type_enum tag_name_list -> Type_enum tag_name_list - | Minils.Type_struct field_ty_list -> - Type_struct field_ty_list - in { t_name = name; t_desc = tdesc; t_loc = loc } + let tdesc = match tdesc with + | Minils.Type_abs -> Type_abs + | Minils.Type_alias ln -> Type_alias ln + | Minils.Type_enum tag_name_list -> + Type_enum (List.map shortname tag_name_list) + | Minils.Type_struct field_ty_list -> + Type_struct field_ty_list in + { t_name = shortname name; t_desc = tdesc; t_loc = loc } let translate_const_def { Minils.c_name = name; Minils.c_value = se; Minils.c_type = ty; Minils.c_loc = loc } = - { c_name = name; + { c_name = shortname name; c_value = se; c_type = ty; c_loc = loc } diff --git a/compiler/minils/main/mls_compiler.ml b/compiler/minils/main/mls_compiler.ml index 1522d96..60ae7eb 100644 --- a/compiler/minils/main/mls_compiler.ml +++ b/compiler/minils/main/mls_compiler.ml @@ -12,10 +12,9 @@ open Compiler_utils let pp p = if !verbose then Mls_printer.print stdout p -let parse prog_name parsing_fun lexing_fun lexbuf = +let parse parsing_fun lexing_fun lexbuf = try - let p = parsing_fun lexing_fun lexbuf in - { p with p_modname = prog_name } + parsing_fun lexing_fun lexbuf with | Mls_lexer.Lexical_error(err, loc) -> lexical_error err loc @@ -26,22 +25,23 @@ let parse prog_name parsing_fun lexing_fun lexbuf = syntax_error l let parse_implementation prog_name lexbuf = - parse prog_name Mls_parser.program Mls_lexer.token lexbuf + let p = parse Mls_parser.program Mls_lexer.token lexbuf in + { p with Mls_parsetree.p_modname = prog_name } let compile pp p = (* Clocking *) - let p = do_pass Clocking.program "Clocking" p pp true in + let p = pass "Clocking" true Clocking.program p pp in (* Check that the dataflow code is well initialized *) - (*let p = do_silent_pass Init.program "Initialization check" p !init in *) + (*let p = silent_pass "Initialization check" !init Init.program p in *) (* Iterator fusion *) - let p = do_pass Itfusion.program "Iterator fusion" p pp true in + (*let p = pass "Iterator fusion" false Itfusion.program p pp in*) (* Normalization to maximize opportunities *) - let p = do_pass Normalize.program "Normalization" p pp true in + let p = pass "Normalization" true Normalize.program p pp in (* Scheduling *) - let p = do_pass Schedule.program "Scheduling" p pp true in + let p = pass "Scheduling" true Schedule.program p pp in p diff --git a/compiler/minils/main/mlsc.ml b/compiler/minils/main/mlsc.ml index cd1159f..98700a7 100644 --- a/compiler/minils/main/mlsc.ml +++ b/compiler/minils/main/mlsc.ml @@ -36,12 +36,11 @@ let compile_impl modname filename = let pp = Mls_compiler.pp in (* Parsing of the file *) - let p = - do_silent_pass Mls_compiler.parse_implementation "Parsing" lexbuf true in - let p = { p with Minils.p_modname = modname } in + let p = do_silent_pass "Parsing" (Mls_compiler.parse_implementation modname) + lexbuf in (* Convert Parse tree to Minils AST *) - let p = Mls_scoping.translate_program "Scoping" p pp true in + let p = do_pass "Scoping" Mls_scoping.translate_program p pp in (* Process the MiniLS AST *) let p = Mls_compiler.compile pp p in diff --git a/compiler/minils/minils.ml b/compiler/minils/minils.ml index dbc2697..2e9931e 100644 --- a/compiler/minils/minils.ml +++ b/compiler/minils/minils.ml @@ -28,14 +28,14 @@ type iterator_type = | Imapfold type type_dec = { - t_name: name; + t_name: qualname; t_desc: tdesc; t_loc: location } and tdesc = | Type_abs | Type_alias of ty - | Type_enum of name list + | Type_enum of constructor_name list | Type_struct of structure and exp = { @@ -58,7 +58,7 @@ and edesc = | Estruct of (field_name * exp) list (** { field=exp; ... } *) | Eiterator of iterator_type * app * static_exp * exp list * var_ident option - (** map f <> (exp,exp...) reset ident *) + (** map f <> (exp, exp...) reset ident *) and app = { a_op: op; a_params: static_exp list; a_unsafe: bool } (** Unsafe applications could have side effects @@ -79,8 +79,7 @@ and op = | Eselect_dyn (** arg1.[arg3...] default arg2 *) | Eupdate (** [ arg1 with arg3..arg_n = arg2 ] *) | Econcat (** arg1@@arg2 *) -(* -*) + type pat = | Etuplepat of pat list @@ -104,7 +103,7 @@ type contract = { c_eq : eq list } type node_dec = { - n_name : name; + n_name : qualname; n_input : var_dec list; n_output : var_dec list; n_contract : contract option; @@ -115,7 +114,7 @@ type node_dec = { n_params_constraints : size_constraint list } type const_dec = { - c_name : name; + c_name : qualname; c_type : ty; c_value : static_exp; c_loc : location } diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 5e4129d..435fc49 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -6,6 +6,7 @@ open Clocks open Static open Format open Signature +open Global_printer open Pp_tools open Minils @@ -29,7 +30,7 @@ let rec print_pat ff = function let rec print_ck ff = function | Cbase -> fprintf ff "base" | Con (ck, c, n) -> - fprintf ff "%a on %a(%a)" print_ck ck print_longname c print_ident n + fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n | Cvar { contents = Cindex n } -> fprintf ff "base" | Cvar { contents = Clink ck } -> print_ck ff ck @@ -50,10 +51,10 @@ let print_local_vars ff = function let print_const_dec ff c = if !Misc.full_type_info then fprintf ff "const %a : %a = %a" - print_name c.c_name print_type c.c_type print_static_exp c.c_value + print_qualname c.c_name print_type c.c_type print_static_exp c.c_value else fprintf ff "const %a = %a" - print_name c.c_name print_static_exp c.c_value; + print_qualname c.c_name print_static_exp c.c_value; fprintf ff "@." @@ -95,12 +96,12 @@ and print_exp_desc ff = function print_app (app, args) print_every reset | Ewhen (e, c, n) -> fprintf ff "@[<2>(%a@ when %a(%a))@]" - print_exp e print_longname c print_ident n + print_exp e print_qualname c print_ident n | Emerge (x, tag_e_list) -> fprintf ff "@[<2>merge %a@ %a@]" print_ident x print_tag_e_list tag_e_list | Estruct f_e_list -> - print_record (print_couple print_longname print_exp """ = """) ff f_e_list + print_record (print_couple print_qualname print_exp """ = """) ff f_e_list | Eiterator (it, f, param, args, reset) -> fprintf ff "@[<2>(%s (%a)<<%a>>)@,%a@]%a" (iterator_to_string it) @@ -115,7 +116,7 @@ and print_app ff (app, args) = match app.a_op, app.a_params, args with | Etuple, _, a -> print_exp_tuple ff a | (Efun(f)|Enode(f)), p, a -> fprintf ff "@[%a@,%a@,%a@]" - print_longname f print_params p print_exp_tuple a + print_qualname f print_params p print_exp_tuple a | Eifthenelse, _, [e1; e2; e3] -> fprintf ff "@[if %a@ then %a@ else %a@]" print_exp e1 print_exp e2 print_exp e3 @@ -139,7 +140,7 @@ and print_app ff (app, args) = match app.a_op, app.a_params, args with fprintf ff "@[<2>%a@ @@ %a@]" print_exp e1 print_exp e2 and print_handler ff c = - fprintf ff "@[<2>%a@]" (print_couple print_longname print_exp "("" -> "")") c + fprintf ff "@[<2>%a@]" (print_couple print_qualname print_exp "("" -> "")") c and print_tag_e_list ff tag_e_list = fprintf ff "@[%a@]" (print_list print_handler """""") tag_e_list @@ -163,14 +164,14 @@ let rec print_type_dec ff { t_name = name; t_desc = tdesc } = | Type_abs -> () | Type_alias ty -> fprintf ff " =@ %a" print_type ty | Type_enum tag_name_list -> - fprintf ff " =@ %a" (print_list print_name """|""") tag_name_list + fprintf ff " =@ %a" (print_list print_qualname """|""") tag_name_list | Type_struct f_ty_list -> fprintf ff " =@ %a" (print_record print_field) f_ty_list in - fprintf ff "@[<2>type %s%a@]@." name print_type_desc tdesc + fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc and print_field ff field = - fprintf ff "@[%a: %a@]" print_name field.f_name print_type field.f_type + fprintf ff "@[%a: %a@]" print_qualname field.f_name print_type field.f_type let print_contract ff { c_local = l; c_eq = eqs; @@ -185,8 +186,8 @@ let print_contract ff { c_local = l; c_eq = eqs; let print_node ff { n_name = n; n_input = ni; n_output = no; n_contract = contract; n_local = nl; n_equs = ne; n_params = params } = - fprintf ff "@[node %s%a%a@ returns %a@]@\n%a%a%a@]@\n@." - n + fprintf ff "@[node %a%a%a@ returns %a@]@\n%a%a%a@]@\n@." + print_qualname n print_node_params params print_vd_tuple ni print_vd_tuple no @@ -196,9 +197,9 @@ let print_node ff { n_name = n; n_input = ni; n_output = no; let print oc { p_opened = pm; p_types = pt; p_nodes = pn; p_consts = pc } = - let ff = formatter_of_out_channel oc in ( + let ff = formatter_of_out_channel oc in List.iter (print_open_module ff) pm; List.iter (print_const_dec ff) pc; List.iter (print_type_dec ff) pt; List.iter (print_node ff) pn; - fprintf ff "@?" ) + fprintf ff "@?" diff --git a/compiler/minils/mls_utils.ml b/compiler/minils/mls_utils.ml index 38dfd77..faa7685 100644 --- a/compiler/minils/mls_utils.ml +++ b/compiler/minils/mls_utils.ml @@ -46,14 +46,13 @@ let rec vd_mem n = function (** @return whether [ty] corresponds to a record type. *) let is_record_type ty = match ty with | Tid n -> - (try - ignore (Modules.find_struct n); true - with - Not_found -> false) + (match Modules.find_type n with + | Tenum _ -> true + | _ -> false) | _ -> false let is_op = function - | Modname { qual = "Pervasives"; id = _ } -> true | _ -> false + | { qual = "Pervasives"; name = _ } -> true | _ -> false let exp_list_of_static_exp_list se_list = diff --git a/compiler/minils/parsing/mls_lexer.mll b/compiler/minils/parsing/mls_lexer.mll index 5be00a5..ce772e5 100644 --- a/compiler/minils/parsing/mls_lexer.mll +++ b/compiler/minils/parsing/mls_lexer.mll @@ -113,7 +113,7 @@ rule token = parse | newline { new_line lexbuf; token lexbuf } | [' ' '\t'] + { token lexbuf } | "." { DOT } - | ".." { DOTDOt } + | ".." { DOTDOT } | "(" { LPAREN } | ")" { RPAREN } | "*" { STAR } diff --git a/compiler/minils/parsing/mls_parser.mly b/compiler/minils/parsing/mls_parser.mly index 036cb0b..9831568 100644 --- a/compiler/minils/parsing/mls_parser.mly +++ b/compiler/minils/parsing/mls_parser.mly @@ -77,8 +77,8 @@ open Mls_utils | P v=x { Some(v) } qualified(x) : - | n=x { Name(n) } - | m=CONSTRUCTOR DOT n=x { Modname({ qual = m; id = n }) } + | n=x { Modules.qualname n } + | m=CONSTRUCTOR DOT n=x { { qual = m; name = n } } structure(field): LBRACE s=snlist(SEMICOL,field) RBRACE {s} @@ -94,31 +94,30 @@ opens: OPEN c=CONSTRUCTOR {c} const_decs: c=list(const_dec) {c} const_dec: - | CONST n=NAME COLON t=type_ident EQUAL e=const + | CONST n=qualname COLON t=type_ident EQUAL e=const { mk_const_dec n t e (Loc($startpos,$endpos)) } -name: n=NAME | LPAREN n=infix_ RPAREN | LPAREN n=prefix_ RPAREN { n } -ident: n=name { ident_of_name n } +name: n=NAME | LPAREN n=infix RPAREN | LPAREN n=prefix RPAREN { n } +qualname: n=name { Modules.qualname n } -field_type : n=NAME COLON t=type_ident { mk_field n t } +field_type : n=qualname COLON t=type_ident { mk_field n t } -type_ident: NAME { Tid(Name($1)) } +type_ident: qualname { Tid($1) } type_decs: t=list(type_dec) {t} type_dec: - | TYPE n=NAME + | TYPE n=qualname { mk_type_dec Type_abs n (Loc ($startpos,$endpos)) } - | TYPE n=NAME EQUAL e=snlist(BAR,NAME) + | TYPE n=qualname EQUAL e=snlist(BAR,constructor) { mk_type_dec (Type_enum e) n (Loc ($startpos,$endpos)) } - | TYPE n=NAME EQUAL s=structure(field_type) + | TYPE n=qualname EQUAL s=structure(field_type) { mk_type_dec (Type_struct s) n (Loc ($startpos,$endpos)) } node_decs: ns=list(node_dec) {ns} node_dec: - NODE n=name p=params(n_param) LPAREN args=args RPAREN + NODE n=qualname p=params(n_param) LPAREN args=args RPAREN RETURNS LPAREN out=args RPAREN vars=loc_vars eqs=equs - { mk_node ~input:args ~output:out ~local:vars - ~eq:eqs ~loc:(Loc ($startpos,$endpos)) n } + { mk_node p args out vars eqs ~loc:(Loc ($startpos,$endpos)) n } args_t: SEMICOL p=args {p} @@ -140,10 +139,6 @@ ck: | ck_base { Cbase } | ck=ck ON c=constructor LPAREN x=NAME RPAREN { Con (ck, c, x) } -ct: - | LPAREN ctl=snlist(STAR,ct) RPAREN { Cprod ctl } - | c=ck { Ck c } - clock_annot: | /*empty*/ { Cbase } | COLONCOLON c=ck { c } @@ -159,68 +154,75 @@ pat: | n=NAME {Evarpat n} | LPAREN p=snlist(COMMA, pat) RPAREN {Etuplepat p} -longname: l=qualified(name) {l} /* qualified var (not a constructor) */ +longname: l=qualified(name) {l} constructor: /* of type longname */ - | ln=qualified(CONSTRUCTOR) { ln } - | b=BOOL { Name(if b then "true" else "false") } + | ln=qualified(CONSTRUCTOR) { ln } + | b=BOOL { if b then Initial.ptrue else Initial.pfalse } field: - | ln=longname { mk_static_exp ~loc:(Loc($startpos,$endpos)) (Sconstructor ln)} + | c=constructor { mk_constructor_exp c (Loc($startpos,$endpos))} -const : c=_const { mk_static_exp ~loc:(Loc ($startpos,$endpos)) c } +const: c=_const { mk_static_exp ~loc:(Loc ($startpos,$endpos)) c } _const: | i=INT { Sint i } | f=FLOAT { Sfloat f } | c=constructor { Sconstructor c } - | t=tuple(const) { Stuple t } exps: LPAREN e=slist(COMMA, exp) RPAREN {e} field_exp: longname EQUAL exp { ($1, $3) } + simple_exp: | e=_simple_exp {mk_exp e (Loc ($startpos,$endpos)) } _simple_exp: - | n=NAME { Evar (ident_of_name n) } + | n=NAME { Evar n } | s=structure(field_exp) { Estruct s } - | t=tuple(exp) { Eapp(mk_app Etuple, t, None) } - | LBRACKET es=slist(COMMA, exp) RBRACKET { Eapp(mk_app Earray, es, None) } + | t=tuple(exp_woc) { mk_call [] Etuple t None } + | t=tuple(const) + {Econst (mk_static_exp ~loc:(Loc ($startpos,$endpos)) (Stuple t))} + | LBRACKET es=slist(COMMA, exp) RBRACKET { mk_call [] Earray es None } | LPAREN e=_exp RPAREN { e } - exp: | e=simple_exp { e } | e=_exp { mk_exp e (Loc ($startpos,$endpos)) } +exp_woc: + | e=simple_exp { e } + | e=_exp_woc { mk_exp e (Loc ($startpos,$endpos)) } + _exp: + | e=_exp_woc {e} | c=const { Econst c } - | v=const FBY e=exp { Efby(Some(v), e) } +_exp_woc: + | v=exp FBY e=exp { Efby(Some(v), e) } | PRE exp { Efby(None,$2) } - | op=funapp a=exps r=reset { Eapp(op, a, r) } + | app=funapp a=exps r=reset { Eapp(app, a, r) } | e1=exp i_op=infix e2=exp - { Eapp(mk_app (Efun i_op), [e1; e2], None) } + { mk_op_call i_op [e1; e2] } | p_op=prefix e=exp %prec prefixs - { Eapp(mk_app (Efun p_op), [e], None) } + { mk_op_call p_op [e] } | IF e1=exp THEN e2=exp ELSE e3=exp - { Eapp( mk_app Eifthenelse, [e1; e2; e3], None) } + { mk_call [] Eifthenelse [e1; e2; e3] None } | e=simple_exp DOT f=field - { Eapp( mk_app ~params:[f] Efield, [e], None) } - | e=exp WHEN c=constructor LPAREN n=ident RPAREN { Ewhen(e, c, n) } - | MERGE n=ident h=handlers { Emerge(n, h) } + { mk_call [f] Efield [e] None } + | e=exp WHEN c=constructor LPAREN n=name RPAREN { Ewhen(e, c, n) } + | MERGE n=name h=handlers { Emerge(n, h) } | LPAREN r=exp WITH DOT f=field EQUAL nv=exp - { Eapp(mk_app ~params:[f] Efield_update, [r; nv], None) } + { mk_call [f] Efield_update [r; nv] None } | e=exp POWER p=e_param - { Eapp(mk_app ~params:[p] Earray_fill, [e], None) } + { mk_call [p] Earray_fill [e] None } | e=simple_exp i=indexes(exp) /* not e_params to solve conflicts */ - { Eapp(mk_app ~params:i Eselect, [e], None) } + { mk_call i Eselect [e] None } | e=simple_exp i=indexes(exp) DEFAULT d=exp - { Eapp(mk_app Eselect_dyn, [e; d]@i, None) } + { mk_call [] Eselect_dyn ([e; d]@i) None } | LPAREN e=exp WITH i=indexes(e_param) EQUAL nv=exp - { Eapp(mk_app ~params:i Eupdate, [e; nv], None) } + { mk_call i Eupdate [e; nv] None } | e=simple_exp LBRACKET i1=e_param DOTDOT i2=e_param RBRACKET - { Eapp(mk_app ~params:[i1; i2] Eselect_slice, [e], None) } - | e1=exp AROBASE e2=exp { Eapp(mk_app Econcat, [e1;e2], None) } + { mk_call [i1; i2] Eselect_slice [e] None } + | e1=exp AROBASE e2=exp { mk_call [] Econcat [e1;e2] None } | LPAREN f=iterator LPAREN op=funapp RPAREN DOUBLE_LESS p=e_param DOUBLE_GREATER RPAREN a=exps r=reset { Eiterator(f,op,p,a,r) } @@ -232,7 +234,7 @@ index(param): LBRACKET p=param RBRACKET { p } -/* Merge handlers ( B -> e)( C -> ec)... */ +/* Merge handlers ( B -> e ) ( C -> ec )... */ handlers: hs=nonempty_list(handler) { hs } handler: LPAREN c=constructor ARROW e=exp RPAREN { c,e } @@ -242,22 +244,20 @@ iterator: | FOLD { Ifold } | MAPFOLD { Imapfold } -reset: r=option(RESET,ident) { r } +reset: r=option(RESET,name) { r } -/* TODO : Scoping to deal with node and fun ! */ funapp: ln=longname p=params(e_param) { mk_app p (Enode ln) } /* inline so that precendance of POWER is respected in exp */ %inline e_param: e=exp { e } -n_param: n=NAME { mk_param n } +n_param: n=NAME COLON ty=type_ident { mk_param n ty } params(param): | /*empty*/ { [] } | DOUBLE_LESS p=slist(COMMA, param) DOUBLE_GREATER { p } /*Inlining is compulsory in order to preserve priorities*/ -%inline infix: op=infix_ { Name(op) } -%inline infix_: +%inline infix: | op=INFIX0 | op=INFIX1 | op=INFIX2 | op=INFIX3 | op=INFIX4 { op } | STAR { "*" } | EQUAL { "=" } @@ -265,8 +265,7 @@ params(param): | AMPERSAND { "&" } | AMPERAMPER { "&&" } | OR { "or" } | BARBAR { "||" } -%inline prefix: op=prefix_ { Name(op) } -%inline prefix_: +%inline prefix: | op = PREFIX { op } | NOT { "not" } | op = SUBTRACTIVE { "~" ^ op } /*TODO test 3 * -2 and co */ diff --git a/compiler/minils/parsing/mls_parsetree.ml b/compiler/minils/parsing/mls_parsetree.ml index ffaad1f..eeac21d 100644 --- a/compiler/minils/parsing/mls_parsetree.ml +++ b/compiler/minils/parsing/mls_parsetree.ml @@ -14,6 +14,11 @@ open Static open Types open Clocks +type var_name = name + +type ck = + | Cbase + | Con of ck * constructor_name * var_name type exp = { e_desc: edesc; @@ -23,18 +28,18 @@ and app = { a_op: Minils.op; a_params: exp list } and edesc = | Econst of static_exp - | Evar of name + | Evar of var_name | Efby of exp option * exp - | Eapp of Minils.app * exp list * name option - | Ewhen of exp * constructor_name * name - | Emerge of name * (constructor_name * exp) list + | Eapp of app * exp list * var_name option + | Ewhen of exp * constructor_name * var_name + | Emerge of var_name * (constructor_name * exp) list | Estruct of (field_name * exp) list | Eiterator of - Minils.iterator_type * app * exp * exp list * name option + Minils.iterator_type * app * exp * exp list * var_name option and pat = | Etuplepat of pat list - | Evarpat of name + | Evarpat of var_name and eq = { eq_lhs : pat; @@ -42,61 +47,62 @@ and eq = { eq_loc : location } and var_dec = { - v_ident : name; - v_type : ty; + v_name : var_name; + v_type : ty; v_clock : ck; - v_loc : location } + v_loc : location } type node_dec = { - n_name : name; - n_input : var_dec list; - n_output : var_dec list; + n_name : qualname; + n_input : var_dec list; + n_output : var_dec list; n_contract : Minils.contract option; - n_local : var_dec list; - n_equs : eq list; - n_loc : location; - n_params : param list } + n_local : var_dec list; + n_equs : eq list; + n_loc : location; + n_params : param list } type program = { - p_modname : name; + p_modname : name; p_format_version : string; - p_opened : name list; - p_types : Minils.type_dec list; - p_nodes : node_dec list; - p_consts : Minils.const_dec list } + p_opened : name list; + p_types : Minils.type_dec list; + p_nodes : node_dec list; + p_consts : Minils.const_dec list } (** {Helper functions to build the Parsetree *) -let mk_node - ?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = []) - ?(loc = no_location) ?(param = []) ?(constraints = []) ?(pinst = []) name = +let mk_node params input output locals eqs ?(loc = no_location) + ?(contract = None) ?(constraints = []) name = { n_name = name; n_input = input; n_output = output; n_contract = contract; - n_local = local; - n_equs = eq; + n_local = locals; + n_equs = eqs; n_loc = loc; - n_params = param } + n_params = params } -(** The modname field has to be set when known, TODO LG : format_version *) let mk_program o n t c = - { p_modname = ""; p_format_version = ""; - p_opened = o; p_nodes = n; p_types = t; p_consts = c } + { p_modname = Modules.current.Modules.modname; + p_format_version = ""; + p_opened = o; + p_nodes = n; + p_types = t; + p_consts = c } let mk_exp desc loc = { e_desc = desc; e_loc = loc } let mk_app params op = { a_op = op; a_params = params } -let void = mk_exp (Eapp (Minils.mk_app Minils.Etuple, [], None)) +let void = mk_exp (Eapp (mk_app [] Minils.Etuple, [], None)) -let mk_call ?(unsafe=false) ?(params=[]) reset op exps = - Eapp (Minils.mk_app ~unsafe:unsafe op ~params:params, exps, reset) +let mk_call params op exps reset = + Eapp (mk_app params op, exps, reset) let mk_op_call ?(params=[]) s exps = - mk_call ~params:params None - (Minils.Efun (Modname { qual = "Pervasives"; id = s })) exps + mk_call params (Minils.Efun { qual = "Pervasives"; name = s }) exps None let mk_iterator_call it ln params reset n exps = Eiterator (it, mk_app params (Minils.Enode ln), n, exps, reset) @@ -108,6 +114,6 @@ let mk_equation lhs rhs loc = { eq_lhs = lhs; eq_rhs = rhs; eq_loc = loc } let mk_var_dec name ty clock loc = - { v_ident = name; v_type = ty; v_clock = clock; v_loc = loc } + { v_name = name; v_type = ty; v_clock = clock; v_loc = loc } diff --git a/compiler/minils/transformations/callgraph.ml b/compiler/minils/transformations/callgraph.ml index b7f0413..f39755b 100644 --- a/compiler/minils/transformations/callgraph.ml +++ b/compiler/minils/transformations/callgraph.ml @@ -12,7 +12,7 @@ open Minils module Error = struct type error = - | Enode_unbound of longname + | Enode_unbound of qualname | Epartial_instanciation of static_exp let message loc kind = @@ -34,8 +34,8 @@ sig type key = private static_exp (** Fully instantiated param *) type env = key NamesEnv.t val instantiate: env -> static_exp list -> key list - val get_node_instances : LongNameEnv.key -> key list list - val add_node_instance : LongNameEnv.key -> key list -> unit + val get_node_instances : QualEnv.key -> key list list + val add_node_instance : QualEnv.key -> key list -> unit val build : env -> param list -> key list -> env module Instantiate : sig @@ -63,7 +63,7 @@ struct module M = (** Map instance to its instantiated node *) Map.Make( struct - type t = longname * instance + type t = qualname * instance let compare (l1,i1) (l2,i2) = let cl = compare l1 l2 in if cl = 0 then compare_instances i1 i2 else cl @@ -73,7 +73,7 @@ struct let nodes_names = ref M.empty (** Maps a node to its list of instances *) - let nodes_instances = ref LongNameEnv.empty + let nodes_instances = ref QualEnv.empty (** create a params instance *) let instantiate m se = @@ -91,32 +91,30 @@ struct [ln] with the static parameters [params] and stores it. *) let generate_new_name ln params = match params with | [] -> nodes_names := M.add (ln, params) ln !nodes_names - | _ -> (match ln with - | Modname { qual = q; id = id } -> - let new_ln = Modname { qual = q; + | _ -> let { qual = q; name = n } = ln in + let new_ln = { qual = q; (* TODO ??? c'est quoi ce nom ??? *) (* l'utilite de fresh n'est vrai que si toute les fonctions sont touchees.. ce qui n'est pas vrai cf main_nodes *) (* TODO mettre les valeurs des params dans le nom *) - id = id^(Idents.name (Idents.fresh "")) } in - nodes_names := M.add (ln, params) new_ln !nodes_names - | _ -> assert false) + name = n^(Idents.name (Idents.fresh "")) } in + nodes_names := M.add (ln, params) new_ln !nodes_names (** Adds an instance of a node. *) let add_node_instance ln params = (* get the already defined instances *) - let instances = try LongNameEnv.find ln !nodes_instances + let instances = try QualEnv.find ln !nodes_instances with Not_found -> S.empty in if S.mem params instances then () (* nothing to do *) else ( (* it's a new instance *) let instances = S.add params instances in - nodes_instances := LongNameEnv.add ln instances !nodes_instances; + nodes_instances := QualEnv.add ln instances !nodes_instances; generate_new_name ln params ) (** @return the list of instances of a node. *) let get_node_instances ln = let instances_set = - try LongNameEnv.find ln !nodes_instances + try QualEnv.find ln !nodes_instances with Not_found -> S.empty in S.elements instances_set @@ -135,13 +133,14 @@ struct let static_exp funs m se = let se, _ = Global_mapfold.static_exp funs m se in let se = match se.se_desc with - | Svar ln -> - (match ln with - | Name n -> - (try NamesEnv.find n m - with Not_found -> (* It should then be in the global env *) - se) - | Modname _ -> se) + | Svar { qual = q; name = n } -> + if q = local_qualname + then (* This var is a static parameter, it has to be instanciated *) + (try NamesEnv.find n m + with Not_found -> + Format.eprintf "local param not local"; + assert false;) + else se | _ -> se in se, m @@ -176,19 +175,17 @@ struct let n, _ = Mls_mapfold.node_dec_it funs m n in (* Add to the global environment the signature of the new instance *) - let ln = Modname { qual = modname; id = n.n_name } in - let { info = node_sig } = find_value ln in + let { info = node_sig } = find_value n.n_name in let node_sig, _ = Global_mapfold.node_it global_funs m node_sig in let node_sig = { node_sig with node_params = []; node_params_constraints = [] } in (* Find the name that was associated to this instance *) - let ln = node_for_params_call ln params in + let ln = node_for_params_call n.n_name params in Modules.add_value_by_longname ln node_sig; - { n with n_name = shortname ln; n_params = []; n_params_constraints = [];} + { n with n_name = ln; n_params = []; n_params_constraints = []; } let node_dec modname n = - let ln = Modname { qual = modname; id = n.n_name } in - List.map (node_dec_instance modname n) (get_node_instances ln) + List.map (node_dec_instance modname n) (get_node_instances n.n_name) let program p = { p @@ -201,13 +198,13 @@ open Param_instances type info = { mutable opened : program NamesEnv.t; - mutable called_nodes : ((longname * static_exp list) list) LongNameEnv.t; } + mutable called_nodes : ((qualname * static_exp list) list) QualEnv.t; } let info = { (** opened programs*) opened = NamesEnv.empty; (** Maps a node to the list of (node name, params) it calls *) - called_nodes = LongNameEnv.empty } + called_nodes = QualEnv.empty } (** Loads the modname.epo file. *) let load_object_file modname = @@ -240,17 +237,14 @@ let load_object_file modname = (** @return the node with name [ln], loading the corresponding object file if necessary. *) -let node_by_longname ln = - match ln with - | Modname { qual = q; id = id } -> - if not (NamesEnv.mem q info.opened) then - load_object_file q; - (try - let p = NamesEnv.find q info.opened in - List.find (fun n -> n.n_name = id) p.p_nodes - with - Not_found -> Error.message no_location (Error.Enode_unbound ln)) - | _ -> assert false +let node_by_longname ({ qual = q; name = n } as node) = + if not (NamesEnv.mem q info.opened) + then load_object_file q; + try + let p = NamesEnv.find q info.opened in + List.find (fun n -> n.n_name = node) p.p_nodes + with + Not_found -> Error.message no_location (Error.Enode_unbound node) (** @return the list of nodes called by the node named [ln], with the corresponding params (static parameters appear as free variables). *) @@ -260,7 +254,7 @@ let collect_node_calls ln = | [] -> acc | _ -> (match ln with - | Modname { qual = "Pervasives" } -> acc + | { qual = "Pervasives" } -> acc | _ -> (ln, params)::acc) in let edesc funs acc ed = match ed with @@ -279,24 +273,12 @@ let collect_node_calls ln = (** @return the list of nodes called by the node named [ln]. This list is computed lazily the first time it is needed. *) let called_nodes ln = - if not (LongNameEnv.mem ln info.called_nodes) then ( + if not (QualEnv.mem ln info.called_nodes) then ( let called = collect_node_calls ln in - info.called_nodes <- LongNameEnv.add ln called info.called_nodes; + info.called_nodes <- QualEnv.add ln called info.called_nodes; called ) else - LongNameEnv.find ln info.called_nodes - -(* -(** Checks that a static expression does not contain any static parameter. *) -let check_no_static_var se = - let static_exp_desc funs acc sed = match sed with - | Svar (Name n) -> Error.message se.se_loc (Error.Evar_unbound n) - | _ -> raise Misc.Fallback - in - let funs = { Global_mapfold.defaults with - static_exp_desc = static_exp_desc } in - ignore (Global_mapfold.static_exp_it funs false se) -*) + QualEnv.find ln info.called_nodes (** Generates the list of instances of nodes needed to call [ln] with static parameters [params]. *) @@ -316,7 +298,7 @@ let rec call_node (ln, params) = let program p = (* Find the nodes without static parameters *) let main_nodes = List.filter (fun n -> is_empty n.n_params) p.p_nodes in - let main_nodes = List.map (fun n -> (longname n.n_name, [])) main_nodes in + let main_nodes = List.map (fun n -> n.n_name, []) main_nodes in info.opened <- NamesEnv.add p.p_modname p NamesEnv.empty; (* Creates the list of instances starting from these nodes *) List.iter call_node main_nodes; diff --git a/compiler/minils/transformations/itfusion.ml b/compiler/minils/transformations/itfusion.ml index 76e1a4e..ba35770 100644 --- a/compiler/minils/transformations/itfusion.ml +++ b/compiler/minils/transformations/itfusion.ml @@ -22,7 +22,7 @@ let add_anon_node inputs outputs locals eqs = let replace_anon_node n nd = anon_nodes := LongNameEnv.add n nd !anon_nodes -let find_anon_node n = +let find_anon_node n = LongNameEnv.find n !anon_nodes let is_anon_node n = @@ -51,9 +51,9 @@ let vd_of_arg ad = an app object. *) let get_node_inp_outp app = match app.a_op with | (Enode f | Efun f) when is_anon_node f -> - (* first check if it is an anonymous node *) + (* first check if it is an anonymous node *) let nd = find_anon_node f in - nd.n_input, nd.n_output + nd.n_input, nd.n_output | Enode f | Efun f -> (* it is a regular node*) let { info = ty_desc } = find_value f in @@ -113,7 +113,7 @@ let edesc funs acc ed = let _, outp = get_node_inp_outp f in let eq = mk_equation (pat_of_vd_list outp) call in (* create the lambda *) - let anon = mk_app (Enode (add_anon_node inp outp [] (eq::acc_eq_list))) in + let anon = mk_app (Enode (add_anon_node inp outp [] (eq::acc_eq_list))) in Eiterator(Imap, anon, n, args, r), acc ) else ed, acc diff --git a/compiler/minils/transformations/normalize.ml b/compiler/minils/transformations/normalize.ml index 77ef12e..25f90b8 100644 --- a/compiler/minils/transformations/normalize.ml +++ b/compiler/minils/transformations/normalize.ml @@ -7,6 +7,7 @@ (* *) (**************************************************************************) open Misc +open Initial open Names open Idents open Signature @@ -15,8 +16,6 @@ open Mls_utils open Types open Clocks -let ctrue = Name "true" -and cfalse = Name "false" let equation (d_list, eq_list) e = let add_one_var ty d_list = @@ -112,9 +111,9 @@ let rec merge e x ci_a_list = let ifthenelse context e1 e2 e3 = let context, n = intro context e1 in let n = (match n with Evar n -> n | _ -> assert false) in - let context, e2 = whenc context e2 ctrue n in - let context, e3 = whenc context e3 cfalse n in - context, merge e1 n [ctrue, e2; cfalse, e3] + let context, e2 = whenc context e2 ptrue n in + let context, e3 = whenc context e3 pfalse n in + context, merge e1 n [ptrue, e2; pfalse, e3] let const e c = let rec const = function @@ -194,10 +193,10 @@ let rec translate kind context e = (* normalize anonymous nodes *) (match app.a_op with | Enode f when Itfusion.is_anon_node f -> - let nd = Itfusion.find_anon_node f in + let nd = Itfusion.find_anon_node f in let d_list, eq_list = translate_eq_list nd.n_local nd.n_equs in - let nd = { nd with n_equs = eq_list; n_local = d_list } in - Itfusion.replace_anon_node f nd + let nd = { nd with n_equs = eq_list; n_local = d_list } in + Itfusion.replace_anon_node f nd | _ -> () ); (* Add an intermediate equation for each array lit argument. *) diff --git a/compiler/minils/transformations/schedule.ml b/compiler/minils/transformations/schedule.ml index 4d29093..4088967 100644 --- a/compiler/minils/transformations/schedule.ml +++ b/compiler/minils/transformations/schedule.ml @@ -77,7 +77,6 @@ let eqs funs () eq_list = let eqs, () = Mls_mapfold.eqs funs () eq_list in schedule eqs, () -let edesc funs () = function | Eiterator(it, ({ a_op = Enode f } as app), n, e_list, r) when Itfusion.is_anon_node f -> let nd = Itfusion.find_anon_node f in diff --git a/compiler/obc/c/cgen.ml b/compiler/obc/c/cgen.ml index 2d03a68..e844d9b 100644 --- a/compiler/obc/c/cgen.ml +++ b/compiler/obc/c/cgen.ml @@ -59,27 +59,20 @@ let int_of_static_exp se = Static.int_of_static_exp NamesEnv.empty se (** Returns the information concerning a node given by name. *) -let node_info classln = - match classln with - | Modname {qual = modname; id = modname_name } -> - begin try - modname, find_value (Modname({qual = modname; - id = modname_name })) - with Not_found -> - (* name might be of the form Module.name, remove the module name*) - (*let ind_name = (String.length modname) + 1 in - let name = String.sub modname_name ind_name - ((String.length modname_name)-ind_name) in - begin try - modname, find_value (Modname({qual = modname; - id = name })) - with Not_found ->*) - Error.message no_location (Error.Enode modname) - (*end *) - end - | Name n -> - assert false; - Error.message no_location (Error.Enode n) +let node_info {qual = modname; name = modname_name } = + try + modname, find_value {qual = modname; name = modname_name } + with Not_found -> + (* name might be of the form Module.name, remove the module name*) + (*let ind_name = (String.length modname) + 1 in + let name = String.sub modname_name ind_name + ((String.length modname_name)-ind_name) in + begin try + modname, find_value (Modname({qual = modname; + id = name })) + with Not_found ->*) + Error.message no_location (Error.Enode modname) + (*end *) let output_names_list sig_info = let remove_option ad = match ad.a_name with @@ -176,7 +169,7 @@ let rec assoc_type n var_env = let rec unalias_ctype = function | Cty_id ty_name -> (try - let { qualid = q; info = ty_desc } = find_type (longname ty_name) in + let { qualname = q; info = ty_desc } = find_type (qualname ty_name) in match ty_desc with | Talias ty -> unalias_ctype (ctype_of_otype ty) | _ -> Cty_id ty_name @@ -202,8 +195,8 @@ let rec assoc_type_lhs lhs var_env = | Cfield(x, f) -> let ty = assoc_type_lhs x var_env in let n = struct_name ty in - let { info = fields } = find_struct (longname n) in - ctype_of_otype (field_assoc (Name f) fields) + let { info = fields } = find_struct (qualname n) in + ctype_of_otype (field_assoc (qualname f) fields) (** Creates the statement a = [e_1, e_2, ..], which gives a list a[i] = e_i.*) @@ -287,9 +280,8 @@ let rec cexpr_of_exp var_env exp = and cexprs_of_exps var_env exps = List.map (cexpr_of_exp var_env) exps -and cop_of_op_aux var_env op_name cexps = - match op_name with - | Modname { qual = "Pervasives"; id = op } -> +and cop_of_op_aux var_env op_name cexps = match op_name with + | { qual = "Pervasives"; name = op } -> begin match op,cexps with | "~-", [e] -> Cuop ("-", e) | "not", [e] -> Cuop ("!", e) @@ -302,9 +294,7 @@ and cop_of_op_aux var_env op_name cexps = Cbop (copname op, el, er) | _ -> Cfun_call(op, cexps) end - | Modname {qual = m; id = op} -> - Cfun_call(op,cexps) - | Name(op) -> + | {qual = m; name = op} -> Cfun_call(op,cexps) and cop_of_op var_env op_name exps = @@ -350,7 +340,7 @@ let assoc_cn instance obj_env = (assoc_obj (obj_call_name instance) obj_env).o_class let is_op = function - | Modname { qual = "Pervasives"; id = _ } -> true + | { qual = "Pervasives"; name = _ } -> true | _ -> false let out_var_name_of_objn o = @@ -431,8 +421,8 @@ let rec create_affect_const var_env dest c = let rec cstm_of_act var_env obj_env act = match act with (** Case on boolean values are converted to if instead of switch! *) - | Acase (c, [(Name "true", te); (Name "false", fe)]) - | Acase (c, [(Name "false", fe); (Name "true", te)]) -> + | Acase (c, [({name = "true"}, te); ({ name = "false" }, fe)]) + | Acase (c, [({name = "false"}, fe); ({ name = "true"}, te)]) -> let cc = cexpr_of_exp var_env c in let cte = cstm_of_act_list var_env obj_env te in let cfe = cstm_of_act_list var_env obj_env fe in @@ -511,7 +501,7 @@ let global_name = ref "";; (** {2 step() and reset() functions generation *) let mk_current_longname n = - Modname { qual = !global_name; id = n } + { qual = !global_name; name = n } (** Builds the argument list of step function*) let step_fun_args n md = @@ -654,7 +644,7 @@ let decls_of_type_decl otd = Cty_ptr Cty_char, [("x", Cty_id name); ("buf", Cty_ptr Cty_char)])] | Type_struct fl -> - let decls = List.map (fun f -> f.Signature.f_name, + let decls = List.map (fun f -> shortname f.Signature.f_name, ctype_of_otype f.Signature.f_type) fl in [Cdecl_struct (otd.t_name, decls)];; @@ -698,7 +688,7 @@ let cdefs_and_cdecls_of_type_decl otd = [Cdecl_enum (otd.t_name, nl); cdecl_of_cfundef of_string_fun; cdecl_of_cfundef to_string_fun]) | Type_struct fl -> - let decls = List.map (fun f -> f.Signature.f_name, + let decls = List.map (fun f -> shortname f.Signature.f_name, ctype_of_otype f.Signature.f_type) fl in let decl = Cdecl_struct (otd.t_name, decls) in ([], [decl]) diff --git a/compiler/obc/c/cmain.ml b/compiler/obc/c/cmain.ml index db2a5eb..a1d4931 100644 --- a/compiler/obc/c/cmain.ml +++ b/compiler/obc/c/cmain.ml @@ -87,7 +87,7 @@ let main_def_of_class_def cd = | Types.Tid id when id = Initial.pfloat -> "%f" | Types.Tid id when id = Initial.pint -> "%d" | Types.Tid id when id = Initial.pbool -> "%d" - | Tid ((Name sid) | Modname { id = sid }) -> "%s" in + | Tid _ -> "%s" in (** Does reading type [ty] need a buffer? When it is the case, [need_buf_for_ty] also returns the type's name. *) @@ -96,7 +96,7 @@ let main_def_of_class_def cd = | Types.Tid id when id = Initial.pfloat -> None | Types.Tid id when id = Initial.pint -> None | Types.Tid id when id = Initial.pbool -> None - | Tid (Name sid | Modname { id = sid; }) -> Some sid in + | Tid { name = n } -> Some n in let cprint_string s = Csexpr (Cfun_call ("printf", [Cconst (Cstrlit s)])) in diff --git a/compiler/obc/obc.ml b/compiler/obc/obc.ml index 2ff509a..a661732 100644 --- a/compiler/obc/obc.ml +++ b/compiler/obc/obc.ml @@ -16,9 +16,9 @@ open Signature open Location type class_name = name -type instance_name = longname +type instance_name = qualname type obj_name = name -type op_name = longname +type op_name = qualname type type_dec = { t_name : name; diff --git a/compiler/obc/obc_printer.ml b/compiler/obc/obc_printer.ml index fc60e39..fb56ca9 100644 --- a/compiler/obc/obc_printer.ml +++ b/compiler/obc/obc_printer.ml @@ -14,7 +14,7 @@ let print_vd ff vd = let print_obj ff o = fprintf ff "@["; print_name ff o.o_name; - fprintf ff " : "; print_longname ff o.o_class; + fprintf ff " : "; print_qualname ff o.o_class; fprintf ff "@[<2>%a@]" (print_list_r print_static_exp "<<"","">>") o.o_params; (match o.o_size with | Some se -> fprintf ff "[%a]" print_static_exp se @@ -42,7 +42,7 @@ and print_exp ff e = | Estruct(_,f_e_list) -> fprintf ff "@["; print_list_r - (fun ff (field, e) -> print_longname ff field;fprintf ff " = "; + (fun ff (field, e) -> print_qualname ff field;fprintf ff " = "; print_exp ff e) "{" ";" "}" ff f_e_list; fprintf ff "@]" @@ -53,9 +53,9 @@ and print_exp ff e = and print_op ff op e_list = match e_list with | [l; r] -> - fprintf ff "(@[%a@ %a %a@])" print_longname op print_exp l print_exp r + fprintf ff "(@[%a@ %a %a@])" print_qualname op print_exp l print_exp r | _ -> - print_longname ff op; + print_qualname ff op; print_list_l print_exp "(" "," ")" ff e_list let print_asgn ff pref x e = @@ -117,7 +117,7 @@ and print_tag_act_list ff tag_act_list = print_list (fun ff (tag, a) -> fprintf ff "@[case %a:@ %a@]" - print_longname tag + print_qualname tag print_block a) "" "" "" ff tag_act_list @@ -167,7 +167,7 @@ let print_type_def ff { t_name = name; t_desc = tdesc } = fprintf ff "@["; print_list (fun ff { Signature.f_name = field; Signature.f_type = ty } -> - print_name ff field; + print_qualname ff field; fprintf ff ": "; print_type ff ty) "{" ";" "}" ff f_ty_list; fprintf ff "@]@.@]" diff --git a/compiler/obc/obc_utils.ml b/compiler/obc/obc_utils.ml index 84199ce..836f0da 100644 --- a/compiler/obc/obc_utils.ml +++ b/compiler/obc/obc_utils.ml @@ -16,9 +16,8 @@ open Global_mapfold module Deps = struct - let deps_longname deps ln = match ln with - | Modname { qual = modn; } -> S.add modn deps - | _ -> deps + + let deps_longname deps { qual = modn; } = S.add modn deps let deps_static_exp_desc funs deps sedesc = let (sedesc, deps) = Global_mapfold.static_exp_desc funs deps sedesc in diff --git a/compiler/utilities/global/compiler_utils.ml b/compiler/utilities/global/compiler_utils.ml index d5251e8..944d5ae 100644 --- a/compiler/utilities/global/compiler_utils.ml +++ b/compiler/utilities/global/compiler_utils.ml @@ -21,28 +21,29 @@ let syntax_error loc = let language_error lang = Format.eprintf "Unknown language: '%s'.@." lang -let comment s = - if !verbose then Format.printf "** %s done **@." s +let separateur = "\n*********************************************\ + *********************************\n*** " +let comment ?(sep=separateur) s = + if !verbose then Format.printf "%s%s@." sep s -let do_pass f d p pp enabled = +let do_pass d f p pp = + comment (d^" ...\n"); + let r = f p in + pp r; + comment ~sep:"*** " (d^" done."); + r + +let do_silent_pass d f p = do_pass d f p (fun x -> ()) + +let pass d enabled f p pp = if enabled - then - let r = f p in - if !verbose - then begin - comment d; - pp r; - end; - r + then do_pass d f p pp else p -let do_silent_pass f d p enabled = +let silent_pass d enabled f p = if enabled - then begin - let r = f p in - if !verbose then comment d; r - end + then do_silent_pass d f p else p let build_path suf = diff --git a/compiler/utilities/misc.ml b/compiler/utilities/misc.ml index e635ee5..1434800 100644 --- a/compiler/utilities/misc.ml +++ b/compiler/utilities/misc.ml @@ -83,7 +83,7 @@ let tomato = ref false let inline = ref [] -let add_inlined_node s = inline := Names.mk_longname s :: !inline +let add_inlined_node s = inline := s :: !inline let flatten = ref false @@ -216,7 +216,7 @@ let rec assocd value = function assocd value l -(** Compiler iterators *) +(** { 3 Compiler iterators } *) exception Fallback (** Mapfold *) @@ -258,3 +258,18 @@ let mapi3 f l1 l2 l3 = (f i v1 v2 v3)::(aux (i+1) l1 l2 l3) in aux 0 l1 l2 l3 + +exception Cannot_find_file of string + +let findfile filename = + if Sys.file_exists filename then + filename + else if not(Filename.is_implicit filename) then + raise(Cannot_find_file filename) + else + let rec find = function + | [] -> raise(Cannot_find_file filename) + | a::rest -> + let b = Filename.concat a filename in + if Sys.file_exists b then b else find rest in + find !load_path \ No newline at end of file diff --git a/compiler/utilities/misc.mli b/compiler/utilities/misc.mli index 496c404..6c3da07 100644 --- a/compiler/utilities/misc.mli +++ b/compiler/utilities/misc.mli @@ -84,7 +84,7 @@ val cse : bool ref val tomato : bool ref (* List of nodes to inline *) -val inline : Names.longname list ref +val inline : string list ref (* Add a new node name to the list of nodes to inline. *) val add_inlined_node : string -> unit (* Inline every node. *) @@ -187,3 +187,6 @@ val mapi: (int -> 'a -> 'b) -> 'a list -> 'b list val mapi2: (int -> 'a -> 'b -> 'c) -> 'a list -> 'b list -> 'c list val mapi3: (int -> 'a -> 'b -> 'c -> 'd) -> 'a list -> 'b list -> 'c list -> 'd list + +exception Cannot_find_file of string +val findfile : string -> string diff --git a/compiler/utilities/pp_tools.ml b/compiler/utilities/pp_tools.ml index f4d7293..903af18 100644 --- a/compiler/utilities/pp_tools.ml +++ b/compiler/utilities/pp_tools.ml @@ -56,12 +56,12 @@ let print_type_params ff pl = print_list_r (fun ff s -> fprintf ff "'%s" s) "("","") " ff pl -let print_set print_element ff set = +let print_set iter print_element ff set = fprintf ff "@[{@ "; iter (fun e -> fprintf ff "%a@ " print_element e) set; fprintf ff "}@]" -let print_map print_key print_element ff map = - pfrintf ff "@[[@ "; - iter (fun k x -> fprintf ff "| %a -> %a@ " print_key k print_element x map; +let print_map iter print_key print_element ff map = + fprintf ff "@[[@ "; + iter (fun k x -> fprintf ff "| %a -> %a@ " print_key k print_element x) map; fprintf ff "]@]" diff --git a/heptc b/heptc index 3172544..be85d5b 100755 --- a/heptc +++ b/heptc @@ -4,7 +4,7 @@ SCRIPT_DIR=`dirname $0` COMPILER_DIR=compiler #relative to the script_dir -COMPILER=heptc.native +COMPILER=heptc.d.byte HEPTC=$COMPILER_DIR/$COMPILER RUN_DIR=`pwd`