Removed Interface since it's job is now done during the scoping.
Moved printing stuff to Global_printer.
This commit is contained in:
Léonard Gérard
parent
f6fb5861ce
commit
1e5697b29a
7 changed files with 57 additions and 134 deletions
|
|
@ -46,6 +46,11 @@ and print_type ff = function
|
|||
| Tarray (ty, n) ->
|
||||
fprintf ff "@[<hov2>%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 "@[<v 2>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 "@."
|
||||
|
||||
|
|
|
|||
|
|
@ -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 }
|
||||
|
||||
|
|
|
|||
|
|
@ -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 "@[<hov 2>type %s = " name;
|
||||
print_list_r print_name "" " |" "" ff tag_name_list;
|
||||
fprintf ff "@.@]"
|
||||
| Tstruct(f_ty_list) ->
|
||||
fprintf ff "@[<hov 2>type %s = " name;
|
||||
fprintf ff "@[<hov 1>";
|
||||
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 "@[<v 2>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
|
||||
|
|
@ -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) ->
|
||||
|
|
|
|||
|
|
@ -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;
|
||||
|
|
|
|||
|
|
@ -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 "@[<v2>contract@\n%a%a@ assume %a;@ enforce %a@]"
|
||||
|
|
|
|||
|
|
@ -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 =
|
||||
|
|
|
|||
Loading…
Reference in a new issue