Make union types consistent in the AST

Previously union types could have no-argument constructors, for
example the option type was previously:

union option ('a : Type) = {
  Some : 'a,
  None
}

Now every union constructor must have a type, so option becomes:

union option ('a : Type) = {
  Some : 'a,
  None : unit
}

The reason for this is because previously these two different types of
constructors where very different in the AST, constructors with
arguments were used the E_app AST node, and no-argument constructors
used the E_id node. This was particularly awkward, because it meant
that E_id nodes could have polymorphic types, i.e. every E_id node
that was also a union constructor had to be annotated with a type
quantifier, in constrast with all other identifiers that have
unquantified types. This became an issue when monomorphising types,
because the machinery for figuring out function instantiations can't
be applied to identifier nodes. The same story occurs in patterns,
where previously unions were split across P_id and P_app nodes - now
the P_app node alone is used solely for unions.

This is a breaking change because it changes the syntax for union
constructors - where as previously option was matched as:

function is_none opt = match opt {
  Some(_) => false,
  None    => true
}

it is now matched as

function is_none opt = match opt {
  Some(_) => false,
  None()  => true
}

note that constructor() is syntactic sugar for constructor(()), i.e. a
one argument constructor with unit as it's value. This is exactly the
same as for functions where a unit-function can be called as f() and
not as f(()). (This commit also makes exit() work consistently in the
same way) An attempt to pattern match a variable with the same name as
a union-constructor now gives an error as a way to guard against
mistakes made because of this change.

There is probably an argument for supporting the old syntax via some
syntactic sugar, as it is slightly prettier that way, but for now I
have chosen to keep the implementation as simple as possible.

The RISCV spec, ARM spec, and tests have been updated to account for
this change. Furthermore the option type can now be included from
$SAIL_DIR/lib/ using

$include <option.sail>

1 files changed, 23 insertions, 42 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index a0390a94..f2136f07 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -445,24 +445,22 @@ let doc_typschm_lem quants (TypSchm_aux(TypSchm_ts(tq,t),_)) =
   else pt
 
 let is_ctor env id = match Env.lookup_id id env with
-| Enum _ | Union _ -> true
+| Enum _ -> true
 | _ -> false
 
 (*Note: vector concatenation, literal vectors, indexed vectors, and record should
   be removed prior to pp. The latter two have never yet been seen
 *)
 let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with
+  | P_app(id, _) when string_of_id id = "None" -> string "Nothing"
   | P_app(id, ((_ :: _) as pats)) ->
     let ppp = doc_unop (doc_id_lem_ctor id)
                        (parens (separate_map comma (doc_pat_lem ctxt true) pats)) in
     if apat_needed then parens ppp else ppp
-  | P_app(id,[]) -> doc_id_lem_ctor id
+  | P_app(id, []) -> doc_id_lem_ctor id
   | P_lit lit  -> doc_lit_lem lit
   | P_wild -> underscore
-  | P_id id ->
-     begin match id with
-     | Id_aux (Id "None",_) -> string "Nothing" (* workaround temporary issue *)
-     | _ -> doc_id_lem id end
+  | P_id id -> doc_id_lem id
   | P_var(p,_) -> doc_pat_lem ctxt true p
   | P_as(p,id) -> parens (separate space [doc_pat_lem ctxt true p; string "as"; doc_id_lem id])
   | P_typ(Typ_aux (Typ_tup typs, _), P_aux (P_tup pats, _)) ->
@@ -614,6 +612,7 @@ let doc_exp_lem, doc_let_lem =
     | E_app(f,args) ->
        begin match f with
        (* temporary hack to make the loop body a function of the temporary variables *)
+       | Id_aux (Id "None", _) as none -> doc_id_lem_ctor none
        | Id_aux (Id "foreach", _) ->
           begin
             match args with
@@ -681,7 +680,7 @@ let doc_exp_lem, doc_let_lem =
           end
        | _ ->
           begin match annot with
-          | Some (env, _, _) when (is_ctor env f) ->
+          | Some (env, _, _) when Env.is_union_constructor f env ->
              let epp =
                match args with
                | [] -> doc_id_lem_ctor f
@@ -899,10 +898,9 @@ let doc_exp_lem, doc_let_lem =
   in top_exp, let_exp
 
 (*TODO Upcase and downcase type and constructors as needed*)
-let doc_type_union_lem (Tu_aux(typ_u,_)) = match typ_u with
-  | Tu_ty_id(typ,id) -> separate space [pipe; doc_id_lem_ctor id; string "of";
-                                        parens (doc_typ_lem typ)]
-  | Tu_id id -> separate space [pipe; doc_id_lem_ctor id]
+let doc_type_union_lem (Tu_aux(Tu_ty_id(typ,id),_)) =
+  separate space [pipe; doc_id_lem_ctor id; string "of";
+                  parens (doc_typ_lem typ)]
 
 let rec doc_range_lem (BF_aux(r,_)) = match r with
   | BF_single i -> parens (doc_op comma (doc_int i) (doc_int i))
@@ -995,19 +993,12 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
              (separate space [string "let rec";fromInterpValueF;string "v";equals;string "match v with"])
              (
                ((separate_map (break 1))
-                  (fun (Tu_aux (tu,_)) ->
-                    match tu with
-                    | Tu_ty_id (ty,cid) ->
-                       (separate space)
-                         [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
-                          arrow;
-                          doc_id_lem_ctor cid;
-                          parens (string "fromInterpValue v")]
-                    | Tu_id cid ->
-                       (separate space)
-                         [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
-                          arrow;
-                          doc_id_lem_ctor cid])
+                  (fun (Tu_aux (Tu_ty_id (ty,cid),_)) ->
+                    (separate space)
+                      [pipe;string "SI.V_ctor";parens (make_id true cid);underscore;underscore;string "v";
+                       arrow;
+                       doc_id_lem_ctor cid;
+                       parens (string "fromInterpValue v")])
                   ar) ^/^
 
                   ((separate space) [pipe;string "SI.V_tuple [v]";arrow;fromInterpValueF;string "v"]) ^/^
@@ -1024,24 +1015,14 @@ let doc_typdef_lem (TD_aux(td, (l, annot))) = match td with
              (separate space [string "let";toInterpValueF;equals;string "function"])
              (
                ((separate_map (break 1))
-                  (fun (Tu_aux (tu,_)) ->
-                    match tu with
-                    | Tu_ty_id (ty,cid) ->
-                       (separate space)
-                         [pipe;doc_id_lem_ctor cid;string "v";arrow;
-                          string "SI.V_ctor";
-                          parens (make_id false cid);
-                          parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                          string "SI.C_Union";
-                          parens (string "toInterpValue v")]
-                    | Tu_id cid ->
-                       (separate space)
-                         [pipe;doc_id_lem_ctor cid;arrow;
-                          string "SI.V_ctor";
-                          parens (make_id false cid);
-                          parens (string "SIA.T_id " ^^ string_lit (doc_id id));
-                          string "SI.C_Union";
-                          parens (string "toInterpValue ()")])
+                  (fun (Tu_aux (Tu_ty_id (ty,cid),_)) ->
+                    (separate space)
+                      [pipe;doc_id_lem_ctor cid;string "v";arrow;
+                       string "SI.V_ctor";
+                       parens (make_id false cid);
+                       parens (string "SIA.T_id " ^^ string_lit (doc_id id));
+                       string "SI.C_Union";
+                       parens (string "toInterpValue v")])
                   ar) ^/^
                  string "end") in
          let fromToInterpValuePP =