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

Add error for non-stateful decls. in pervasives

Browse source 
Attempts to compile a pervasives.epi containing functions with multiple
outputs or nodes now fail with an informative error message.

* The following files demonstrate the problem:

  pervasives.epi:
    type bool = true | false
    external val node test(bool;bool) returns bool

  broken.ept:
    node broken() returns (y : bool)
    let
      y = test(false, false);
    tel

  Running:
    heptc -nopervasives pervasives.epi
    heptc -stdlib . -target c broken.ept

  Fails with:

    ---------
    Internal compiler error
    Passe : Static evaluation failed of the pervasive operator test
    ----------
    Fatal error: exception Misc.Assert_false

* A different error occurs for nodes that return multiple outputs:

  pervasives.epi:
    type bool = true | false
    external val node test(bool;bool) returns (bool;bool)

  broken.ept:
    node broken() returns (y : bool)
    var l1 : bool;
    let
      (y,l1) = test(false, false);
    tel

  Running:
    heptc -nopervasives pervasives.epi
    heptc -stdlib . broken.ept

  Gives:
    Inconsistent clock annotation for exp test(false, false).
    File "broken.ept", line 4, characters 11-29:
    >  (y,l1) = test(false, false);
    >           ^^^^^^^^^^^^^^^^^^
    Clock Clash: this expression has clock 'a3,
    but is expected to have clock ('a4 * 'a5).

  The name "test" is parsed as an Eextvalue (rather than an Eapp), and there
  is an implicit assumption in compiler/minils/analysis/clocking.ml that such
  values have a simple clock.
This commit is contained in:
Timothy Bourke 2016-04-26 10:07:21 +02:00
parent 755b570a96
commit 0b7eba8458
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
compiler/heptagon/analysis/typing.ml
View file

@ -57,6 +57,7 @@ type error =
| Enon_exaustive
| Epartial_switch of name
| Etoo_many_outputs
| Ebad_pervasives
| Esome_fields_are_missing
| Esubscripted_value_not_an_array of ty
| Earray_subscript_should_be_const
@ -149,7 +150,10 @@ let message loc kind =
print_location loc
s
| Etoo_many_outputs ->
eprintf "%aA function may only returns a basic value.@."
eprintf "%aA function may only return a basic value.@."
print_location loc
| Ebad_pervasives ->
eprintf "%aNo nodes or multiple return values allowed in Pervasives.@."
print_location loc
| Esome_fields_are_missing ->
eprintf "%aSome fields are missing.@."
@ -1287,6 +1291,9 @@ let typing_typedec td =
let typing_signature s =
let typed_params, cenv = build_node_params QualEnv.empty s.sig_params in
if Modules.current () = Pervasives
&& (s.sig_stateful || List.length s.sig_outputs > 1)
then message s.sig_loc Ebad_pervasives;
{ s with sig_params = typed_params;
sig_inputs = List.map (typing_arg cenv) s.sig_inputs;
sig_outputs = List.map (typing_arg cenv) s.sig_outputs; }