diff --git a/compiler/global/global_printer.ml b/compiler/global/global_printer.ml index 8e3cf5c..ae0228e 100644 --- a/compiler/global/global_printer.ml +++ b/compiler/global/global_printer.ml @@ -46,6 +46,11 @@ and print_type ff = function | Tarray (ty, n) -> fprintf ff "@[%a^%a@]" print_type ty print_static_exp n +let print_field ff field = + fprintf ff "@[%a: %a@]" print_qualname field.f_name print_type field.f_type + +let print_struct ff field_list = print_record print_field ff field_list + let print_size_constraint ff = function | Cequal (e1, e2) -> fprintf ff "@[%a = %a@]" print_static_exp e1 print_static_exp e2 @@ -56,4 +61,47 @@ let print_size_constraint ff = function let print_param ff p = fprintf ff "%a:%a" Names.print_name p.p_name print_type p.p_type +let print_interface_type ff name tdesc = + match tdesc with + | Tabstract -> fprintf ff "@[type %s@]" name + | Tenum tag_name_list -> + fprintf ff "@[<2>type %s =@ %a@]" + name + (print_list_r print_qualname "" " |" "") tag_name_list; + | Tstruct f_ty_list -> + fprintf ff "@[<2>type %s =@ %a@]" name print_struct f_ty_list + | Talias t -> fprintf ff "@[<2>type %s = %a@]" name print_type t + +let print_interface_const ff name c = + fprintf ff "@[<2>const %a : %a = %a@]@." + print_name name + print_type c.Signature.c_type + print_static_exp c.Signature.c_value + +let print_interface_value ff name node = + let print_arg ff arg = match arg.a_name with + | None -> print_type ff arg.a_type + | Some(name) -> + fprintf ff "@[%a : %a@]" print_name name print_type arg.a_type in + let print_node_params ff p_list = + print_list_r (fun ff p -> print_name ff p.p_name) "<<" "," ">>" ff p_list + in + fprintf ff "@[val %a%a@[%a@] returns @[%a@]@,@[%a@]@]" + print_name name + print_node_params node.node_params + (print_list_r print_arg "(" ";" ")") node.node_inputs + (print_list_r print_arg "(" ";" ")") node.node_outputs + (print_list_r print_size_constraint " with: " "," "") + node.node_params_constraints + + +let print_interface ff i = + let m = Modules.current_module () in + NamesEnv.iter + (fun key typdesc -> print_interface_type ff key typdesc) m.m_types; + NamesEnv.iter + (fun key constdec -> print_interface_const ff key constdec) m.m_consts; + NamesEnv.iter + (fun key sigtype -> print_interface_value ff key sigtype) m.m_values; + Format.fprintf ff "@." diff --git a/compiler/global/modules.ml b/compiler/global/modules.ml index aca524e..392fce8 100644 --- a/compiler/global/modules.ml +++ b/compiler/global/modules.ml @@ -240,8 +240,8 @@ let rec unalias_type t = match t with | 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 = +(** Return the current module as a [module_object] *) +let current_module () = (* Filter and transform a qualified env into the current module object env *) let unqualify env = (* unqualify env keys *) QualEnv.fold @@ -255,13 +255,11 @@ let write_current_module oc = 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_consts = unqualify g_env.consts; 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 + m_format_version = g_env.format_version } diff --git a/compiler/heptagon/analysis/interface.ml b/compiler/heptagon/analysis/interface.ml deleted file mode 100644 index f6a9c54..0000000 --- a/compiler/heptagon/analysis/interface.ml +++ /dev/null @@ -1,117 +0,0 @@ -(**************************************************************************) -(* *) -(* Heptagon *) -(* *) -(* Author : Marc Pouzet *) -(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) -(* *) -(**************************************************************************) -(* Read an interface *) - -open Idents -open Names -open Heptagon -open Signature -open Modules -open Pp_tools -open Types - -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 = - 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; - node_statefull = statefull; - node_params = typed_params; - node_params_constraints = []; } - - let read { interf_desc = desc; interf_loc = loc } = - try - match desc with - | Iopen(n) -> open_module n - | Itypedef(tydesc) -> deftype tydesc - | Iconstdef cd -> ignore (typing_const_dec cd) - | Isignature(s) -> - let name, s = sigtype s in - add_value name s - with - TypingError(error) -> message loc error - - let main l = - List.iter read l -end - -module Printer = -struct - open Format - open Hept_printer - - let deftype ff name tdesc = - match tdesc with - | Tabstract -> fprintf ff "@[type %s@.@]" name - | Tenum(tag_name_list) -> - fprintf ff "@[type %s = " name; - print_list_r print_name "" " |" "" ff tag_name_list; - fprintf ff "@.@]" - | Tstruct(f_ty_list) -> - fprintf ff "@[type %s = " name; - fprintf ff "@["; - print_list_r - (fun ff { f_name = field; f_type = ty } -> print_name ff field; - fprintf ff ": "; - print_type ff ty) "{" ";" "}" ff f_ty_list; - fprintf ff "@]@.@]" - - let constdef ff _ c = - fprintf ff "@[const "; - print_name ff c.c_name; - fprintf ff " : "; - print_type ff c.c_type; - fprintf ff " = "; - print_static_exp ff c.c_value; - fprintf ff "@.@]" - - let signature ff name { node_inputs = inputs; - node_outputs = outputs; - node_params = params; - node_params_constraints = constr } = - let print ff arg = - match arg.a_name with - | None -> print_type ff arg.a_type - | Some(name) -> - print_name ff name; fprintf ff ":"; print_type ff arg.a_type - in - - let print_node_params ff = function - | [] -> () - | l -> print_list_r print_name "<<" "," ">>" ff l - in - - fprintf ff "@[val "; - print_name ff name; - print_node_params ff (List.map (fun p -> p.p_name) params); - fprintf ff "@["; - print_list_r print "(" ";" ")" ff inputs; - fprintf ff "@] returns @["; - print_list_r print "(" ";" ")" ff outputs; - fprintf ff "@]"; - (match constr with - | [] -> () - | constr -> - fprintf ff "@\n with: @["; - print_list_r Static.print_size_constraint "" "," "" ff constr; - fprintf ff "@]" - ); - fprintf ff "@.@]" - - let print oc = - let ff = Format.formatter_of_out_channel oc in - NamesEnv.iter (fun key typdesc -> deftype ff key typdesc) current.types; - NamesEnv.iter (fun key constdec -> constdef ff key constdec) current.consts; - NamesEnv.iter (fun key sigtype -> signature ff key sigtype) current.values; - Format.fprintf ff "@?" -end diff --git a/compiler/heptagon/hept_printer.ml b/compiler/heptagon/hept_printer.ml index e12f80b..c037e46 100644 --- a/compiler/heptagon/hept_printer.ml +++ b/compiler/heptagon/hept_printer.ml @@ -269,7 +269,7 @@ let print_type_def ff { t_name = name; t_desc = tdesc } = | Type_alias ty -> fprintf ff "@[type %a@ = %a@.@]" print_qualname name print_type ty | Type_enum(tag_name_list) -> - fprintf ff "@[type %a = " print_qualname name; + fprintf ff "@[<2>type %a = " print_qualname name; print_list_r print_qualname "" "| " "" ff tag_name_list; fprintf ff "@.@]" | Type_struct(f_ty_list) -> diff --git a/compiler/heptagon/main/hept_compiler.ml b/compiler/heptagon/main/hept_compiler.ml index e7c2915..4a44587 100644 --- a/compiler/heptagon/main/hept_compiler.ml +++ b/compiler/heptagon/main/hept_compiler.ml @@ -39,7 +39,7 @@ let compile_impl pp p = (*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 print_interface Format.std_formatter l; (* Causality check *) let p = silent_pass "Causality check" true Causality.program p in @@ -92,10 +92,7 @@ let compile_interface modname filename = (* Convert the parse tree to Heptagon AST *) 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;*) + if !print_types then print_interface Format.std_formatter l; Modules.write itc; diff --git a/compiler/minils/mls_printer.ml b/compiler/minils/mls_printer.ml index 435fc49..c6ff0e4 100644 --- a/compiler/minils/mls_printer.ml +++ b/compiler/minils/mls_printer.ml @@ -170,10 +170,6 @@ let rec print_type_dec ff { t_name = name; t_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_qualname field.f_name print_type field.f_type - - let print_contract ff { c_local = l; c_eq = eqs; c_assume = e_a; c_enforce = e_g; } = fprintf ff "@[contract@\n%a%a@ assume %a;@ enforce %a@]" diff --git a/compiler/utilities/pp_tools.ml b/compiler/utilities/pp_tools.ml index 903af18..442e2f5 100644 --- a/compiler/utilities/pp_tools.ml +++ b/compiler/utilities/pp_tools.ml @@ -53,7 +53,8 @@ let print_record print_field ff record = let print_type_params ff pl = - print_list_r (fun ff s -> fprintf ff "'%s" s) "("","") " ff pl + fprintf ff "@[%a@]" + (print_list_r (fun ff s -> fprintf ff "'%s" s) "("","") ") pl let print_set iter print_element ff set =