Added heptcheck in heptagon/main

When given a .ept file, it just check its validity.
When given a .epi file, it checks it and creates
the .epci compiled file.

heptagon/analysis/interface.ml

@@ -14,6 +14,8 @@ open Heptagon
 open Signature
 open Modules
 open Typing
+open Pp_tools
+open Types
 
 module Type =
   struct
@@ -49,16 +51,16 @@ struct
       | Tabstract -> fprintf ff "@[type %s@.@]" name
       | Tenum(tag_name_list) ->
 	        fprintf ff "@[<hov 2>type %s = " name;
-	        print_list ff print_name " |" tag_name_list;
+	        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 ff 
-	          (fun ff (field, ty) -> print_name ff field;
+	        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) ";" f_ty_list;
-	        fprintf ff "}@]@.@]"
+	             print_type ff ty) "{" ";" "}" ff f_ty_list;
+	        fprintf ff "@]@.@]"
 
   let signature ff name { node_inputs = inputs;
 			  node_outputs = outputs;
@@ -73,24 +75,22 @@ struct
 
     let print_node_params ff = function
       | [] -> ()
-      | l -> 
-	        fprintf ff "<<";
-	        print_list ff print_name "," l;
-	        fprintf ff ">>" in
+      | l -> print_list_r print_name "<<" "," ">>" ff l
+	  in
       
       fprintf ff "@[<v 2>val ";
       print_name ff name;
-      print_node_params ff params;
-      fprintf ff "(@[";
-      print_list ff print ";" inputs;
-      fprintf ff "@]) returns (@[";
-      print_list ff print ";" outputs;
-      fprintf ff "@])";
+      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 ff Static.print_size_constr "," constr;
+	           print_list_r Static.print_size_constr "" "," "" ff constr;
 	           fprintf ff "@]"
       );
       fprintf ff "@.@]"

heptagon/heptagon.ml

@@ -169,10 +169,10 @@ let mk_var_dec ?(last = Var) name ty  =
   { v_name = name; v_type = ty;
     v_last = last; v_loc = Location.get_current_location () }
 
-let mk_block defnames eqs =
+let mk_block ?(statefull = true) defnames eqs =
   { b_local = []; b_equs = eqs; b_defnames = defnames;
-    b_statefull = true; b_loc = no_location }
-  
+    b_statefull = statefull; b_loc = no_location }
+
 let dfalse = mk_exp (Econst (Cconstr Initial.pfalse)) (Tid Initial.pbool)
 let dtrue = mk_exp (Econst (Cconstr Initial.ptrue)) (Tid Initial.pbool)
   
@@ -182,6 +182,11 @@ let mk_ifthenelse e1 e2 e3 =
 let mk_simple_equation pat e =
   mk_equation ~statefull:false (Eeq(pat, e))
 
+let mk_switch_equation ?(statefull = true) e l = 
+  mk_equation ~statefull:statefull (Eswitch (e, l))
+
+
+
 (*
 let cfalse = Cconstr Initial.pfalse
   

heptagon/main/compiler_utils.ml

@@ -0,0 +1,55 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+open Misc
+open Location
+
+let lexical_error err loc =
+  Printf.eprintf "%aIllegal character.\n" output_location loc;
+  raise Error
+
+let syntax_error loc =
+  Printf.eprintf "%aSyntax error.\n" output_location loc;
+  raise Error
+
+let language_error lang =
+  Printf.eprintf "Unknown language: %s.\n" lang
+
+let parse parsing_fun lexing_fun lexbuf =
+  try
+    parsing_fun lexing_fun lexbuf
+  with
+    | Lexer.Lexical_error(err, pos1, pos2) ->
+        lexical_error err (Loc(pos1, pos2))
+    | Parsing.Parse_error ->
+        let pos1 = Lexing.lexeme_start lexbuf
+        and pos2 = Lexing.lexeme_end lexbuf in
+        let l = Loc(pos1,pos2) in
+        syntax_error l
+
+let comment s = Printf.printf "** %s done **\n" s; flush stdout
+
+let do_pass f d p pp enabled =
+  if enabled
+  then
+    let r = f p in
+    if !verbose
+    then begin
+      comment d;
+      pp r;
+    end;
+    r
+  else p
+
+let do_silent_pass f d p enabled =
+  if enabled
+  then begin
+    let r = f p in
+    if !verbose then comment d; r
+  end
+  else p

heptagon/main/hept_compiler.ml

@@ -0,0 +1,50 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+open Misc
+open Compiler_utils
+
+let compile_impl pp p =
+  (* Typing *)
+  let p = do_pass Typing.program "Typing" p pp true in
+    
+    if !print_types then Interface.Printer.print stdout;
+    
+    (* Causality check *)
+    let p = do_silent_pass Causality.program "Causality check" p true in
+      
+    (* Initialization check *)
+    let p =
+      do_silent_pass Initialization.program "Initialization check" p !init in
+
+    (* Completion of partial definitions *)
+    let p = do_pass Completion.program "Completion" p pp true in
+
+    (* Automata *)
+    let p = do_pass Automata.program "Automata" p pp true in
+
+    (* Present *)
+    let p = do_pass Present.program "Present" p pp true in
+
+    (* Shared variables (last) *)
+    let p = do_pass Last.program "Last" p pp true in
+
+    (* Reset *)
+    let p = do_pass Reset.program "Reset" p pp true in
+
+    (* Every *)
+    let p = do_pass Every.program "Every" p pp true in
+
+      (* Return the transformed AST *)
+      p
+
+
+let compile_interface l =
+  Interface.Type.main l;
+  if !print_types then Interface.Printer.print stdout;
+  l

heptagon/main/heptcheck.ml

@@ -0,0 +1,141 @@
+(**************************************************************************)
+(*                                                                        *)
+(*  Heptagon                                                              *)
+(*                                                                        *)
+(*  Author : Marc Pouzet                                                  *)
+(*  Organization : Demons, LRI, University of Paris-Sud, Orsay            *)
+(*                                                                        *)
+(**************************************************************************)
+
+(* Checks the validity of a Heptagon file (interface or implementation).*)
+
+open Misc
+open Compiler_utils
+open Location
+
+let init_compiler modname source_name ic =
+    Location.initialize source_name ic;
+    Modules.initialize modname;
+    Initial.initialize ()
+
+let pp = Printer.print stdout
+
+let parse_implementation lexbuf =
+  parse Parser.program Lexer.token lexbuf
+
+let parse_interface lexbuf =
+  parse Parser.interface Lexer.token lexbuf
+
+let compile_impl modname filename = 
+  (* input and output files *)
+  let source_name = filename ^ ".ept" in
+
+  let ic = open_in source_name in
+  let close_all_files () =
+    close_in ic 
+  in
+
+    try
+      init_compiler modname source_name ic;
+        
+      (* Parsing of the file *)
+      let lexbuf = Lexing.from_channel ic in
+      let p = parse_implementation lexbuf in
+
+      (* Convert the parse tree to Heptagon AST *)
+      let p = Scoping.translate_program p in
+        if !verbose
+        then begin
+          comment "Parsing";
+          pp p
+        end;
+
+        (* Call the compiler*)
+        Hept_compiler.compile_impl pp p;
+
+        if !verbose
+        then begin
+          comment "Check successfull"
+        end;    
+        close_all_files ()
+
+    with x -> close_all_files (); raise x    
+
+let compile_interface modname filename =
+  (* input and output files *)
+  let source_name = filename ^ ".epi" in
+  let obj_interf_name = filename ^ ".epci" in
+
+  let ic = open_in source_name in
+  let itc = open_out_bin obj_interf_name in
+  let close_all_files () =
+    close_in ic;
+    close_out itc in
+
+  try
+    init_compiler modname source_name ic;
+
+    (* Parsing of the file *)
+    let lexbuf = Lexing.from_channel ic in
+    let l = parse_interface lexbuf in
+
+    (* Convert the parse tree to Heptagon AST *)
+    let l = Scoping.translate_interface l in
+
+      (* Call the compiler*)
+      Hept_compiler.compile_interface l;
+
+      Modules.write itc;
+
+    close_all_files ()
+  with
+    | x -> close_all_files (); raise x
+
+let compile file =
+  if Filename.check_suffix file ".ept"
+  then
+    let filename = Filename.chop_suffix file ".ept" in
+    let modname = String.capitalize(Filename.basename filename) in
+      compile_impl modname filename
+  else if Filename.check_suffix file ".epi"
+  then
+    let filename = Filename.chop_suffix file ".epi" in
+    let modname = String.capitalize(Filename.basename filename) in
+      compile_interface modname filename
+  else
+    raise (Arg.Bad ("Unknow file type: " ^ file))
+
+let doc_verbose = "\t\t\tSet verbose mode"
+and doc_version = "\t\tThe version of the compiler"
+and doc_print_types = "\t\t\tPrint types"
+and doc_include = "<dir>\t\tAdd <dir> to the list of include directories"
+and doc_stdlib = "<dir>\t\tDirectory for the standard library"
+and doc_locate_stdlib = "\t\tLocate standard libray"
+and doc_no_pervasives = "\tDo not load the pervasives module"
+and doc_full_type_info = "\t\t\tPrint full type information"
+and doc_noinit = "\t\tDisable initialization analysis"
+
+let errmsg = "Options are:"
+
+let main () =
+  try
+    Arg.parse
+      [
+        "-v",Arg.Set verbose, doc_verbose;
+        "-version", Arg.Unit show_version, doc_version;
+        "-i", Arg.Set print_types, doc_print_types;
+        "-I", Arg.String add_include, doc_include;
+        "-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
+        "-stdlib", Arg.String set_stdlib, doc_stdlib;
+        "-nopervasives", Arg.Unit set_no_pervasives, doc_no_pervasives;
+	      "-noinit", Arg.Clear init, doc_noinit;
+        "-fti", Arg.Set full_type_info, doc_full_type_info;
+      ]
+      compile
+      errmsg;
+  with
+    | Misc.Error -> exit 2;;
+
+main ()
+
+

heptagon/parsing/lexer.mll

@@ -21,12 +21,10 @@ let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);;
 List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
  "node", NODE;
  "fun", FUN;
- "safe", SAFE;
  "returns", RETURNS;
  "var", VAR;
  "val", VAL;
  "const", CONST;
- "unsafe", UNSAFE;
  "let", LET;
  "tel", TEL;
  "end", END;

heptagon/parsing/parser.mly

@@ -1,10 +1,9 @@
 %{
 
 open Misc
-open Global
+open Signature
 open Location
 open Names
-open Linearity
 open Parsetree
 
 %}
@@ -118,7 +117,7 @@ const_decs:
 
 const_dec:
   | CONST IDENT COLON ty_ident EQUAL exp
-      { cmake $2 $4 $6 }
+      { mk_const_dec $2 $4 $6 }
 ;
 
 type_decs:
@@ -127,9 +126,9 @@ type_decs:
 ;
 
 type_dec:
-  | TYPE IDENT                      { tmake $2 Type_abs }
-  | TYPE IDENT EQUAL enum_ty_desc   { tmake $2 (Type_enum ($4)) }
-  | TYPE IDENT EQUAL struct_ty_desc { tmake $2 (Type_struct ($4)) }
+  | TYPE IDENT                      { mk_type_dec $2 Type_abs }
+  | TYPE IDENT EQUAL enum_ty_desc   { mk_type_dec $2 (Type_enum ($4)) }
+  | TYPE IDENT EQUAL struct_ty_desc { mk_type_dec $2 (Type_struct ($4)) }
 ;
 
 enum_ty_desc:
@@ -193,7 +192,7 @@ nonmt_params:
 
 param:
   | ident_list COLON ty_ident
-      { List.map (fun id -> vmake id $3 Var) $1 }
+      { List.map (fun id -> mk_var_dec id $3 Var) $1 }
 ;
 
 out_params:
@@ -252,11 +251,11 @@ loc_params:
 
 var_last:
   | ident_list COLON ty_ident
-      { List.map (fun id -> vmake id $3 Var) $1 }
+      { List.map (fun id -> mk_var_dec id $3 Var) $1 }
   | LAST IDENT COLON ty_ident EQUAL const
-      { [ vmake $2 $4 (Last(Some($6))) ] }
+      { [ mk_var_dec $2 $4 (Last(Some($6))) ] }
   | LAST IDENT COLON ty_ident
-      { [ vmake $2 $4 (Last(None)) ] }
+      { [ mk_var_dec $2 $4 (Last(None)) ] }
 ;
 
 ident_list:
@@ -292,26 +291,26 @@ opt_bar:
 ;
 
 equ:
-  | pat EQUAL exp { eqmake (Eeq($1, $3)) }
+  | pat EQUAL exp { mk_equation (Eeq($1, $3)) }
   | AUTOMATON automaton_handlers END
-      { eqmake (Eautomaton(List.rev $2)) }
+      { mk_equation (Eautomaton(List.rev $2)) }
   | SWITCH exp opt_bar switch_handlers END
-      { eqmake (Eswitch($2, List.rev $4)) }
+      { mk_equation (Eswitch($2, List.rev $4)) }
   | PRESENT opt_bar present_handlers END
-      { eqmake (Epresent(List.rev $3, bmake [] [])) }
+      { mk_equation (Epresent(List.rev $3, mk_block [] [])) }
   | PRESENT opt_bar present_handlers DEFAULT loc_vars DO equs END
-      { eqmake (Epresent(List.rev $3, bmake $5 $7)) }
+      { mk_equation (Epresent(List.rev $3, mk_block $5 $7)) }
   | IF exp THEN loc_vars DO equs ELSE loc_vars DO equs END
-      { eqmake (Eswitch($2,
-           [{ w_name = Name("true"); w_block = bmake $4 $6};
-      { w_name = Name("false"); w_block = bmake $8 $10 }])) }
+      { mk_equation (Eswitch($2,
+           [{ w_name = Name("true"); w_block = mk_block $4 $6};
+      { w_name = Name("false"); w_block = mk_block $8 $10 }])) }
   | RESET equs EVERY exp
-      { eqmake (Ereset($2, $4)) }
+      { mk_equation (Ereset($2, $4)) }
 ;
 
 automaton_handler:
   | STATE Constructor loc_vars DO equs opt_until_escapes opt_unless_escapes
-      { { s_state = $2; s_block = bmake $3 $5;
+      { { s_state = $2; s_block = mk_block $3 $5;
     s_until = $6; s_unless = $7 } }
 ;
 
@@ -350,7 +349,7 @@ escapes:
 
 switch_handler:
   | constructor loc_vars DO equs
-      { { w_name = $1; w_block = bmake $2 $4 } }
+      { { w_name = $1; w_block = mk_block $2 $4 } }
 ;
 
 switch_handlers:
@@ -362,7 +361,7 @@ switch_handlers:
 
 present_handler:
   | exp loc_vars DO equs
-      { { p_cond = $1; p_block = bmake $2 $4 } }
+      { { p_cond = $1; p_block = mk_block $2 $4 } }
 ;
 
 present_handlers:
@@ -444,7 +443,7 @@ exp:
   | SUBTRACTIVE exp %prec prec_uminus
       { mk_exp (mk_op_call ("~"^$1) [] [$2]) }
   | IF exp THEN exp ELSE exp
-      { mk_exp (Eapp(mk_app Eifthenelse [$2; $4; $6])) }
+      { mk_exp (Eapp(mk_app Eifthenelse, [$2; $4; $6])) }
   | simple_exp ARROW exp
       { mk_exp (Eapp(mk_app Earrow, [$1; $3])) }
   | LAST IDENT
@@ -457,7 +456,7 @@ exp:
   | exp indexes 
       { mk_exp (mk_array_op_call (Eselect $2) [$1]) }
   | exp DOT indexes DEFAULT exp 
-      { mk_exp (mk_array_op_call Eselect_dyn [$1; $5]@$3) }
+      { mk_exp (mk_array_op_call Eselect_dyn ([$1; $5]@$3)) }
   | exp WITH indexes EQUAL exp
       { mk_exp (mk_array_op_call (Eupdate $3) [$1; $5]) }
   | exp LBRACKET exp DOUBLE_DOT exp RBRACKET
@@ -562,7 +561,8 @@ interface_decl:
   | OPEN Constructor { mk_interface_decl (Iopen $2) }
   | VAL node_or_fun ident node_params LPAREN params_signature RPAREN
     RETURNS LPAREN params_signature RPAREN
-    { mk_interface_decl (Isignature({ sig_name = $4; sig_inputs = $6;
+    { mk_interface_decl (Isignature({ sig_name = $3; 
+                                      sig_inputs = $6;
                                       sig_outputs = $10;
                                       sig_params = $4; })) }
 ;
@@ -578,8 +578,8 @@ nonmt_params_signature:
 ;
 
 param_signature:
-  | IDENT COLON ty_ident { Signature.mk_arg (Some $1) $3) }
-  | ty_ident { Signature.mk_arg None $1 }
+  | IDENT COLON ty_ident { mk_arg (Some $1) $3 }
+  | ty_ident { mk_arg None $1 }
 ;
 
 %%

heptagon/parsing/parsetree.ml

@@ -150,6 +150,8 @@ type program =
       p_nodes  : node_dec list;
       p_consts : const_dec list; }
 
+type arg = { a_type : ty; a_name : name option }
+
 type signature =
     { sig_name    : name;
       sig_inputs  : arg list;
@@ -210,3 +212,6 @@ let mk_const_dec id ty e =
   { c_name = id; c_type = ty; c_value = e;
     c_loc = Location.get_current_location (); }
 
+let mk_arg name ty =
+  { a_type = ty; a_name = name }
+

heptagon/parsing/scoping.ml

@@ -293,7 +293,7 @@ let translate_typedec const_env ty =
     | Type_enum(tag_list) -> Heptagon.Type_enum(tag_list)
     | Type_struct(field_ty_list) ->
 	      let translate_field_type (f,ty) = 
-	        f, translate_type const_env ty
+	        Signature.mk_field f (translate_type const_env ty)
 	      in
 	        Heptagon.Type_struct (List.map translate_field_type field_ty_list)
   in
@@ -315,10 +315,15 @@ let translate_program p =
     Heptagon.p_nodes = List.map (translate_node const_env Rename.empty) p.p_nodes;
     Heptagon.p_consts = List.map (translate_const_dec const_env) p.p_consts; }
 
+let translate_arg const_env a =
+  { Signature.a_name = a.a_name;
+    Signature.a_type = translate_type const_env a.a_type }
+
 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 = s.sig_inputs;
-    Heptagon.sig_outputs = s.sig_outputs;
+    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_params = List.map Signature.mk_param s.sig_params; }
 
 let translate_interface_desc const_env = function 

heptagon/transformations/present.ml

@@ -13,15 +13,8 @@
 open Misc
 open Location
 open Heptagon
-open Global
 open Initial
 
-let block defnames statefull eqs =
-  { b_local = []; b_equs = eqs; b_defnames = defnames;
-    b_statefull = statefull; b_loc = no_location }
-let switch statefull e l =
-  { eq_desc = Eswitch(e, l); eq_statefull = statefull; eq_loc = no_location }
-
 let rec translate_eq v eq =
   match eq.eq_desc with
     | Eswitch(e, switch_handlers) ->
@@ -54,8 +47,8 @@ and translate_switch_handlers handlers =
 and translate_present_handlers handlers cont =
   let translate_present_handler { p_cond = e; p_block = b } cont =
     let statefull = b.b_statefull or cont.b_statefull in
-    block b.b_defnames statefull
-      [switch statefull e [{ w_name = ptrue; w_block = b };
+    mk_block ~statefull:statefull b.b_defnames 
+      [mk_switch_equation ~statefull:statefull e [{ w_name = ptrue; w_block = b };
                            { w_name = pfalse; w_block = cont }]] in
   let b = List.fold_right translate_present_handler handlers cont in
   List.hd (b.b_equs)