From f63571c9a6b532f64b415de27bb0ee6cc358388d Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Thu, 11 Oct 2018 21:31:23 +0100
Subject: Change the function type in the AST

Changes the representation of function types in the ast from

Typ_fn : typ -> typ

to

Typ_fn : typ list -> typ

to more accurately represent their use in the various backends, where we often compile functions to either their curried representations as in Lem and Isabelle, or just
multiple argument functions in C. There's still some oddity because a single pattern in a function clause can bind against multiple arguments, and maybe we want to
forbid this in the future. The syntax also hasn't changed (yet), so in theory this change shouldn't break anything (but it invariably will...).

In the future we would ideally require that a function with N arguments has exactly N patterns in its declaration, one for each argument so

f : (x, y) -> z
f _ = ...

would be disallowed (as _ matches both x and y), forcing

f(_, _) = z

this would simply quite a few things,

Also we could have a different syntax for function argument lists and tuples, because it's rather hard to define a function that actually takes a tuple with the syntax
how it is now.

Some issues I noticed when doing this refactoring:

Line 1926 of Coq translation. untuple_args_pat is maybe no longer needed? However there's still some funnyness where a pattern can be used to bind multiple function
arguments so maybe it still is.

Line 2306 of monomorphisation. I simplified the logic here. I think it's equivalent now, but I could be wrong.

Line 4517 of rewrites. I'm not sure what make_cstr_mappings is doing here, but hopefully the simpler version is the same.
---
 src/pretty_print_sail.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7b843ebe..8f78b7dc 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -134,7 +134,7 @@ let doc_nc =
     | _ -> atomic_nc nc
   in
   nc0
-
+  
 let rec doc_typ (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
@@ -154,11 +154,11 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
   | Typ_exist (kids, nc, typ) ->
      braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
-  | Typ_fn (typ1, typ2, Effect_aux (Effect_set [], _)) ->
-     separate space [doc_typ typ1; string "->"; doc_typ typ2]
-  | Typ_fn (typ1, typ2, Effect_aux (Effect_set effs, _)) ->
+  | Typ_fn (typs, typ, Effect_aux (Effect_set [], _)) ->
+     separate space [doc_arg_typs typs; string "->"; doc_typ typ]
+  | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) ->
      let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in
-     separate space [doc_typ typ1; string "->"; doc_typ typ2; string "effect"; ocaml_eff]
+     separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
   | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
@@ -167,6 +167,9 @@ and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
   | Typ_arg_typ typ -> doc_typ typ
   | Typ_arg_nexp nexp -> doc_nexp nexp
   | Typ_arg_order o -> doc_ord o
+and doc_arg_typs = function
+  | [typ] -> doc_typ typ
+  | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
 
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
-- 
cgit v1.2.3


From c1305bf912ff1cc0920c2bb011fee30623504a34 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 22 Oct 2018 16:03:41 +0100
Subject: Fix lem arguments for functions with tuple arguments

Make lem output understand difference between functions taking a tuple
and functions taking multiple arguments. Previously it assumed that no
functions ever took a tuple as an argument, which is incorrect for
mappings.
---
 src/pretty_print_sail.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 8f78b7dc..08ede660 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -354,6 +354,7 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_throw exp -> string "throw" ^^ parens (doc_exp exp)
   | E_try (exp, pexps) ->
      separate space [string "try"; doc_exp exp; string "catch"; doc_pexps pexps]
+  | E_return (E_aux (E_lit (L_aux (L_unit, _)), _)) -> string "return()"
   | E_return exp -> string "return" ^^ parens (doc_exp exp)
   | E_internal_return exp -> string "internal_return" ^^ parens (doc_exp exp)
   | E_app (id, [exp]) when Id.compare (mk_id "pow2") id == 0 ->
@@ -367,8 +368,8 @@ and doc_infix n (E_aux (e_aux, _) as exp) =
          match Bindings.find op !fixities with
          | (Infix, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]
          | (Infix, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r])
-         | (InfixL, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r]
-         | (InfixL, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix (m + 1) r])
+         | (InfixL, m) when m >= n -> separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r]
+         | (InfixL, m) -> parens (separate space [doc_infix m l; doc_id op; doc_infix (m + 1) r])
          | (InfixR, m) when m >= n -> separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r]
          | (InfixR, m) -> parens (separate space [doc_infix (m + 1) l; doc_id op; doc_infix m r])
        with
-- 
cgit v1.2.3


From 5471af45fd04169eb184371dcd8f791e507eab6f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 24 Oct 2018 17:25:47 +0100
Subject: Add constraint synonyms

Currently not enabled by default, the flag -Xconstraint_synonyms
enables them

For generating constraints in ASL parser, we want to be able to give
names to the constraints that we attach to certain variables. It's
slightly awkward right now when constraints get long complicated
because the entire constraint always has to be typed out in full
whenever it appears, and there's no way to abstract away from that.

This adds constraint synonyms, which work much like type synonyms
except for constraints, e.g.

constraint Size('n) = 'n in {1, 2, 4, 8} | 128 <= 'n <= 256

these constraints can then be used instead of the full constraint, e.g.

val f : forall 'n, where Size('n). int('n) -> unit

Unfortunatly we need to have a keyword to 'call' the constraint
synonym otherwise the grammer stops being LR(1). This could be
resolved by parsing all constraints into Parse_ast.atyp and then
de-sugaring them into constraints, which is what happens for
n-expressions already, but that would require quite a bit of work on
the parser.

To avoid this forcing changes to any other parts of Sail, the intended
invariant is that all constraints appearing anywhere in a type-checked
AST have no constraint synonyms, so they don't have to worry about
matching on NC_app, or calling Env.expand_typquant_synonyms (which
isn't even exported for this reason).
---
 src/pretty_print_sail.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 08ede660..0b0a8305 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -123,6 +123,7 @@ let doc_nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
+    | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps)
     | _ -> parens (nc0 nc)
   and nc0 (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -134,7 +135,7 @@ let doc_nc =
     | _ -> atomic_nc nc
   in
   nc0
-  
+
 let rec doc_typ (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
@@ -586,6 +587,8 @@ let rec doc_def def = group (match def with
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
+  | DEF_constraint (id, kids, nc) ->
+     separate space [string "constraint"; doc_id id; parens (separate_map (comma ^^ space) doc_kid kids); equals; doc_nc nc]
   | DEF_overload (id, ids) ->
      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
   ) ^^ hardline
-- 
cgit v1.2.3


From 546bd3e14957199cc1efc0810fb4a2c58ba23fde Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Mon, 29 Oct 2018 15:52:20 +0000
Subject: Pretty printer tweaks for ASL parser

No longer remove braces around singleton expressions, as this can
produce unreadably long lines in ASL parser output when assignments
are converted to lets.

Add brackets around as-patterns for type-variables
---
 src/pretty_print_sail.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 0b0a8305..37c48220 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -237,7 +237,7 @@ let rec doc_pat (P_aux (p_aux, _) as pat) =
   (* P_var short form sugar *)
   | P_var (P_aux (P_id id, _), TP_aux (TP_var kid, _)) when Id.compare (id_of_kid kid) id == 0 ->
      doc_kid kid
-  | P_var (pat, tpat) -> separate space [doc_pat pat; string "as"; doc_typ_pat tpat]
+  | P_var (pat, tpat) -> parens (separate space [doc_pat pat; string "as"; doc_typ_pat tpat])
   | P_vector pats -> brackets (separate_map (comma ^^ space) doc_pat pats)
   | P_vector_concat pats -> separate_map (space ^^ string "@" ^^ space) doc_pat pats
   | P_wild -> string "_"
@@ -286,7 +286,6 @@ let fixities =
 let rec doc_exp (E_aux (e_aux, _) as exp) =
   match e_aux with
   | E_block [] -> string "()"
-  | E_block [exp] -> doc_exp exp
   | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace
   | E_nondet exps -> assert false
   (* This is mostly for the -convert option *)
-- 
cgit v1.2.3


From 001e28b487c8a4cb2a25519a3acc8ac8c1aaabf5 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 31 Oct 2018 15:43:56 +0000
Subject: Rename Reporting_basic to Reporting

There is no Reporting_complex, so it's not clear what the basic is
intended to signify anyway.

Add a GitHub issue link to any err_unreachable errors (as they are all
bugs)
---
 src/pretty_print_sail.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 37c48220..7de4dd40 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -162,7 +162,7 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
      separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
-  | Typ_internal_unknown -> raise (Reporting_basic.err_unreachable l __POS__ "escaped Typ_internal_unknown")
+  | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
 and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
   match ta_aux with
   | Typ_arg_typ typ -> doc_typ typ
-- 
cgit v1.2.3


From c54f60b713087e33758c63dc110fe02d3fea29c9 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 1 Nov 2018 17:26:01 +0000
Subject: Changes to enable analysing type errors in ASL parser

Also some pretty printer improvements

Make all the tests use the same colours for green/red/yellow
---
 src/pretty_print_sail.ml | 50 +++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 41 insertions(+), 9 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7de4dd40..d71b32b2 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -52,6 +52,8 @@ open Ast
 open Ast_util
 open PPrint
 
+let opt_use_heuristics = ref false
+
 module Big_int = Nat_big_num
 
 let doc_op symb a b = infix 2 1 symb a b
@@ -124,11 +126,26 @@ let doc_nc =
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
     | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps)
-    | _ -> parens (nc0 nc)
-  and nc0 (NC_aux (nc_aux, _) as nc) =
-    match nc_aux with
-    | NC_or (c1, c2) -> separate space [nc0 c1; string "|"; nc1 c2]
-    | _ -> nc1 nc
+    | _ -> nc0 ~parenthesize:true nc
+  and nc0 ?parenthesize:(parenthesize=false) (NC_aux (nc_aux, _) as nc) =
+    (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if
+       we rewrite a disjunction as a set constraint, then we can
+       always omit the parens. *)
+    let parens' = if parenthesize then parens else (fun x -> x) in
+    let disjs = constraint_disj nc in
+    let collect_constants kid = function
+      | NC_aux (NC_equal (Nexp_aux (Nexp_var kid', _), Nexp_aux (Nexp_constant c, _)), _) when Kid.compare kid kid' = 0 -> Some c
+      | _ -> None
+    in
+    match disjs with
+    | NC_aux (NC_equal (Nexp_aux (Nexp_var kid, _), Nexp_aux (Nexp_constant c, _)), _) :: ncs ->
+       let constants = List.map (collect_constants kid) ncs in
+       begin match Util.option_all (List.map (collect_constants kid) ncs) with
+       | None | Some [] -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs)
+       | Some cs ->
+          separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int (c :: cs))]
+       end
+    | _ -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs)
   and nc1 (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
@@ -146,6 +163,7 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
   | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0->
      string "bits" ^^ parens (doc_typ_arg len)
                *)
+  | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 -> string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
@@ -172,6 +190,12 @@ and doc_arg_typs = function
   | [typ] -> doc_typ typ
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
 
+let doc_kopt = function
+  | KOpt_aux (KOpt_none kid, _) -> doc_kid kid
+  | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
+  | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
+  | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
+
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
@@ -193,14 +217,22 @@ let doc_quants quants =
   | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
   | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
 
-
-
-let doc_binding (TypQ_aux (tq_aux, _), typ) =
+let doc_binding ((TypQ_aux (tq_aux, _) as typq), typ) =
   match tq_aux with
   | TypQ_no_forall -> doc_typ typ
   | TypQ_tq [] -> doc_typ typ
   | TypQ_tq qs ->
-     string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ
+     if !opt_use_heuristics && String.length (string_of_typquant typq) > 60 then
+       let kopts, ncs = quant_split typq in
+       if ncs = [] then
+         string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ dot
+         ^//^ doc_typ typ
+       else
+         string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ comma
+         ^//^ (separate_map (space ^^ string "&" ^^ space) doc_nc ncs ^^ dot
+               ^^ hardline ^^ doc_typ typ)
+     else
+       string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ
 
 let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ)
 
-- 
cgit v1.2.3


From 953bfdd18c71bcd6c486aac74fe145104c3b2a4d Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 7 Nov 2018 18:56:28 +0000
Subject: Improvements to latex generation

The main changes so far are:

* Allow markdown formatting in doc comments. We parse the markdown
  using Omd, which is a OCaml library for parsing markdown. The nice
  thing about this library is it's pure OCaml and has no dependencies
  other the the stdlib. Incidentally it was also developed at OCaml
  labs. Using markdown keeps our doc-comments from becoming latex
  specfic, and having an actual parser is _much_ nicer than trying to
  hackily process latex in doc-comments using OCamls somewhat sub-par
  regex support.

* More sane conversion latex identifiers the main approach is to
  convert Sail identifiers to lowerCamelCase, replacing numbers with
  words, and then add a 'category' code based on the type of
  identifier, so for a function we'd have fnlowerCamelCase and for
  type synonym typelowerCamelCase etc. Because this transformation is
  non-injective we keep track of identifiers we've generated so we end
  up with identifierA, identifierB, identifierC when there are
  collisions.

* Because we parse markdown in doc comments doc comments can use Sail
  identifiers directly in hyperlinks, without having to care about how
  they are name-mangled down into TeX compatible things.

* Allow directives to be passed through the compiler to
  backends. There are various $latex directives that modify the latex
  output. Most usefully there's a

  $latex newcommand name markdown

  directive that uses the markdown parser to generate latex
  commands. An example of why this is useful is bellow. We can also use

  $latex noref id

  To suppress automatically inserting links to an identifier

* Refactor the latex generator to make the overall generation process
  cleaner

* Work around the fact that some operating systems consider
  case-sensitive file names to be a good thing

* Fix a bug where latex generation wouldn't occur unless the directory
  specified by -o didn't exist

This isn't quite all the requested features for good CHERI
documentation, but new features should be much easier to add now.
---
 src/pretty_print_sail.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d71b32b2..c23b5ecc 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -567,7 +567,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | _ -> string "TYPEDEF"
 
 
-let doc_spec (VS_aux (v, annot)) =
+let doc_spec ?comment:(comment=false) (VS_aux (v, annot)) =
   let doc_extern ext =
     let doc_backend b = Util.option_map (fun id -> string (b ^ ":") ^^ space ^^
       utf8string ("\"" ^ String.escaped id ^  "\"")) (ext b) in
@@ -576,7 +576,7 @@ let doc_spec (VS_aux (v, annot)) =
   in
   match v with
   | VS_val_spec(ts,id,ext,is_cast) ->
-     docstring annot
+     if comment then docstring annot else empty
      ^^ string "val" ^^ space
      ^^ (if is_cast then (string "cast" ^^ space) else empty)
      ^^ doc_id id ^^ space
@@ -615,6 +615,8 @@ let rec doc_def def = group (match def with
      ^^ hardline ^^ string "}"
   | DEF_reg_dec dec -> doc_dec dec
   | DEF_scattered sdef -> doc_scattered sdef
+  | DEF_pragma (pragma, arg, l) ->
+     string ("$" ^ pragma ^ " " ^ arg)
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
-- 
cgit v1.2.3


From 60bcce4648ed029ca3c19c023f5ca525b43eced4 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 13 Nov 2018 18:54:35 +0000
Subject: Make pretty printer stricter with brace placement

Also add a special case for shift-left when we are shifting 8 by a two
bit opcode, or 32 by a one bit opcode.
---
 src/pretty_print_sail.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d71b32b2..93693339 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -119,7 +119,7 @@ let doc_nc =
     match nc_aux with
     | NC_true -> string "true"
     | NC_false -> string "false"
-    | NC_equal (n1, n2) -> nc_op "=" n1 n2
+    | NC_equal (n1, n2) -> nc_op "==" n1 n2
     | NC_not_equal (n1, n2) -> nc_op "!=" n1 n2
     | NC_bounded_ge (n1, n2) -> nc_op ">=" n1 n2
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
@@ -318,7 +318,8 @@ let fixities =
 let rec doc_exp (E_aux (e_aux, _) as exp) =
   match e_aux with
   | E_block [] -> string "()"
-  | E_block exps -> surround 2 0 lbrace (doc_block exps) rbrace
+  | E_block exps ->
+     group (lbrace ^^ nest 4 (hardline ^^ doc_block exps) ^^ hardline ^^ rbrace)
   | E_nondet exps -> assert false
   (* This is mostly for the -convert option *)
   | E_app_infix (x, id, y) when Id.compare (mk_id "quot") id == 0 ->
-- 
cgit v1.2.3


From 81ce65d8213b9dc26e204512408e6a340fe985fa Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Thu, 15 Nov 2018 17:12:37 +0000
Subject: Add simple valspec printing in latex that drops effects and other
 extraneous details (TODO make this optional).

---
 src/pretty_print_sail.ml | 25 ++++++++++++++-----------
 1 file changed, 14 insertions(+), 11 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index c23b5ecc..7608f78b 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -113,7 +113,7 @@ let rec doc_nexp =
   in
   nexp0
 
-let doc_nc =
+let doc_nc nc =
   let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
   let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -151,9 +151,9 @@ let doc_nc =
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
     | _ -> atomic_nc nc
   in
-  nc0
+  nc0 (constraint_simp nc)
 
-let rec doc_typ (Typ_aux (typ_aux, l)) =
+let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
   | Typ_app (id, []) -> doc_id id
@@ -177,7 +177,10 @@ let rec doc_typ (Typ_aux (typ_aux, l)) =
      separate space [doc_arg_typs typs; string "->"; doc_typ typ]
   | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) ->
      let ocaml_eff = braces (separate (comma ^^ space) (List.map (fun be -> string (string_of_base_effect be)) effs)) in
-     separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
+     if simple then
+       separate space [doc_arg_typs typs; string "->"; doc_typ ~simple:simple typ]
+     else
+       separate space [doc_arg_typs typs; string "->"; doc_typ typ; string "effect"; ocaml_eff]
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
@@ -217,24 +220,24 @@ let doc_quants quants =
   | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
   | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
 
-let doc_binding ((TypQ_aux (tq_aux, _) as typq), typ) =
+let doc_binding ?(simple=false) ((TypQ_aux (tq_aux, _) as typq), typ) =
   match tq_aux with
-  | TypQ_no_forall -> doc_typ typ
-  | TypQ_tq [] -> doc_typ typ
+  | TypQ_no_forall -> doc_typ ~simple:simple typ
+  | TypQ_tq [] -> doc_typ ~simple:simple typ
   | TypQ_tq qs ->
      if !opt_use_heuristics && String.length (string_of_typquant typq) > 60 then
        let kopts, ncs = quant_split typq in
        if ncs = [] then
          string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ dot
-         ^//^ doc_typ typ
+         ^//^ doc_typ ~simple:simple typ
        else
          string "forall" ^^ space ^^ separate_map space doc_kopt kopts ^^ comma
          ^//^ (separate_map (space ^^ string "&" ^^ space) doc_nc ncs ^^ dot
-               ^^ hardline ^^ doc_typ typ)
+               ^^ hardline ^^ doc_typ ~simple:simple typ)
      else
-       string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ typ
+       string "forall" ^^ space ^^ doc_quants qs ^^ dot ^//^ doc_typ ~simple:simple typ
 
-let doc_typschm (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding (typq, typ)
+let doc_typschm ?(simple=false) (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_binding ~simple:simple (typq, typ)
 
 let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ
 
-- 
cgit v1.2.3


From 626c68dad5ea79da7776b4628e5ae22ca742669e Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 16 Nov 2018 18:28:17 +0000
Subject: Canonicalise functions types in val specs

This brings Sail closer to MiniSail, and means that

type my_range 'n 'm = {'o, 'n <= 'o <= 'm. int('o)}

will work on the left hand side of a function type in the same way as
a regular built-in range type. This means that in principle neither
range nor int need be built-in types, as both can be implemented in
terms of int('n) (atom internally). It also means we can easily
identify type variables that need to be made into implict arguments,
with the criterion for that being simply any type variable that
doesn't appear in a base type on the LHS of the function, or only
appears on the RHS.
---
 src/pretty_print_sail.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 93693339..31b1ed85 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -68,7 +68,7 @@ let doc_kid kid = string (Ast_util.string_of_kid kid)
 let doc_int n = string (Big_int.to_string n)
 
 let docstring (l, _) = match l with
-  | Parse_ast.Documented (str, _) -> string "/**" ^^ string str ^^ string "*/" ^^ hardline
+  | Parse_ast.Documented (str, _) -> string "/*!" ^^ string str ^^ string "*/" ^^ hardline
   | _ -> empty
 
 let doc_ord (Ord_aux(o,_)) = match o with
@@ -483,13 +483,14 @@ let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) =
 
 let doc_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord]
 
-let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), _)) =
-  match funcls with
-  | [] -> failwith "Empty function list"
-  | _ ->
-     let sep = hardline ^^ string "and" ^^ space in
-     let clauses = separate_map sep doc_funcl funcls in
-     string "function" ^^ space ^^ clauses
+let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), annot)) =
+  docstring annot
+  ^^ match funcls with
+     | [] -> failwith "Empty function list"
+     | _ ->
+        let sep = hardline ^^ string "and" ^^ space in
+        let clauses = separate_map sep doc_funcl funcls in
+        string "function" ^^ space ^^ clauses
 
 let rec doc_mpat (MP_aux (mp_aux, _) as mpat) =
   match mp_aux with
-- 
cgit v1.2.3


From 4fd0c147e6c53ec64b7e4a8cd0324f6e8e56714f Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 30 Nov 2018 16:30:47 +0000
Subject: Improvements for ASL parser

- Fix pretty printing nested constraints

- Add flow typing for if condition then { throw exn }; ... blocks

- Add optimisations for bitvector concatenation in C
---
 src/pretty_print_sail.ml | 38 ++++++++++++++++----------------------
 1 file changed, 16 insertions(+), 22 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 792c3d23..a2771ae1 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -151,7 +151,7 @@ let doc_nc nc =
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
     | _ -> atomic_nc nc
   in
-  nc0 (constraint_simp nc)
+  nc0 ~parenthesize:true (constraint_simp nc)
 
 let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
@@ -159,16 +159,15 @@ let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   | Typ_app (id, []) -> doc_id id
   | Typ_app (Id_aux (DeIid str, _), [x; y]) ->
      separate space [doc_typ_arg x; doc_typ_arg y]
-              (*
-  | Typ_app (id, [_; len; _; Typ_arg_aux (Typ_arg_typ (Typ_aux (Typ_id tid, _)), _)]) when Id.compare (mk_id "vector") id == 0 && Id.compare (mk_id "bit") tid == 0->
-     string "bits" ^^ parens (doc_typ_arg len)
-               *)
-  | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 -> string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
+  | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
+     string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
   (* Resugar set types like {|1, 2, 3|} *)
-  | Typ_exist ([kid1], NC_aux (NC_set (kid2, ints), _), Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
+  | Typ_exist ([kid1],
+               NC_aux (NC_set (kid2, ints), _),
+               Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
          when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
   | Typ_exist (kids, nc, typ) ->
@@ -371,21 +370,16 @@ let rec doc_exp (E_aux (e_aux, _) as exp) =
   | E_assign (lexp, exp) ->
      separate space [doc_lexp lexp; equals; doc_exp exp]
   | E_for (id, exp1, exp2, exp3, order, exp4) ->
-     begin
-       let header =
-         string "foreach" ^^ space ^^
-           group (parens (separate (break 1)
-                                   [ doc_id id;
-                                     string "from " ^^ doc_atomic_exp exp1;
-                                     string "to " ^^ doc_atomic_exp exp2;
-                                     string "by " ^^ doc_atomic_exp exp3;
-                                     string "in " ^^ doc_ord order ]))
-       in
-       match exp4 with
-       | E_aux (E_block [_], _) -> header ^//^ doc_exp exp4
-       | E_aux (E_block _, _) -> header ^^ space ^^ doc_exp exp4
-       | _ -> header ^//^ doc_exp exp4
-     end
+     let header =
+       string "foreach" ^^ space ^^
+         group (parens (separate (break 1)
+                                 [ doc_id id;
+                                   string "from " ^^ doc_atomic_exp exp1;
+                                   string "to " ^^ doc_atomic_exp exp2;
+                                   string "by " ^^ doc_atomic_exp exp3;
+                                   string "in " ^^ doc_ord order ]))
+     in
+     header ^^ space ^^ doc_exp exp4
   (* Resugar an assert with an empty message *)
   | E_throw exp -> string "throw" ^^ parens (doc_exp exp)
   | E_try (exp, pexps) ->
-- 
cgit v1.2.3


From 0363a325ca6c498e086519c4ecaf1f51dbff7f64 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 30 Nov 2018 18:54:42 +0000
Subject: Parser tweaks and fixes

- Completely remove the nexp = nexp syntax in favour of nexp ==
  nexp. All our existing specs have already switched over. As part of
  this fix every test that used the old syntax, and update the
  generated aarch64 specs

- Remove the `type when constraint` syntax. It just makes changing the
  parser in any way really awkward.

- Change the syntax for declaring new types with multiple type
  parameters from:

  type foo('a : Type) ('n : Int), constraint = ...

  to

  type foo('a: Type, 'n: Int), constraint = ...

  This makes type declarations mimic function declarations, and makes
  the syntax for declaring types match the syntax for using types, as
  foo is used as foo(type, nexp). None of our specifications use types
  with multiple type parameters so this change doesn't actually break
  anything, other than some tests. The brackets around the type
  parameters are now mandatory.

- Experiment with splitting Type/Order type parameters from Int type
  parameters in the parser.

  Currently in a type bar(x, y, z) all of x, y, and z could be either
  numeric expressions, orders, or types. This means that in the parser
  we are severely restricted in what we can parse in numeric
  expressions because everything has to be parseable as a type (atyp)
  - it also means we can't introduce boolean type
  variables/expressions or other minisail features (like removing
  ticks from type variables!) because we are heavily constrained by
  what we can parse unambigiously due to how these different type
  parameters can be mixed and interleaved.

  There is now experimental syntax: vector::<'o, 'a>('n) <-->
  vector('n, 'o, 'a) which splits the type argument list into two
  between Type/Order-polymorphic arguments and Int-polymorphic
  arguments. The exact choice of delimiters isn't set in stone - ::<
  and > match generics in Rust. The obvious choices of < and > / [ and
  ] are ambigious in various ways.

  Using this syntax right now triggers a warning.

- Fix undefined behaviour in C compilation when concatenating a
  0-length vector with a 64-length vector.
---
 src/pretty_print_sail.ml | 31 ++++++++++++++++++++++++++-----
 1 file changed, 26 insertions(+), 5 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index a2771ae1..53e77df2 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -151,7 +151,7 @@ let doc_nc nc =
     | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
     | _ -> atomic_nc nc
   in
-  nc0 ~parenthesize:true (constraint_simp nc)
+  atomic_nc (constraint_simp nc)
 
 let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
@@ -219,6 +219,27 @@ let doc_quants quants =
   | [nc] -> kdoc ^^ comma ^^ space ^^ doc_nc nc
   | nc :: ncs -> kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
 
+let doc_param_quants quants =
+  let doc_qi_kopt (QI_aux (qi_aux, _)) =
+    match qi_aux with
+    | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
+    | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
+    | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
+    | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
+    | QI_const nc -> []
+  in
+  let qi_nc (QI_aux (qi_aux, _)) =
+    match qi_aux with
+    | QI_const nc -> [nc]
+    | _ -> []
+  in
+  let kdoc = separate (comma ^^ space) (List.concat (List.map doc_qi_kopt quants)) in
+  let ncs = List.concat (List.map qi_nc quants) in
+  match ncs with
+  | [] -> parens kdoc
+  | [nc] -> parens kdoc ^^ comma ^^ space ^^ doc_nc nc
+  | nc :: ncs -> parens kdoc ^^ comma ^^ space ^^ doc_nc (List.fold_left nc_and nc ncs)
+
 let doc_binding ?(simple=false) ((TypQ_aux (tq_aux, _) as typq), typ) =
   match tq_aux with
   | TypQ_no_forall -> doc_typ ~simple:simple typ
@@ -244,7 +265,7 @@ let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _))
   match tq_aux with
   | TypQ_no_forall -> None
   | TypQ_tq [] -> None
-  | TypQ_tq qs -> Some (doc_quants qs)
+  | TypQ_tq qs -> Some (doc_param_quants qs)
 
 let doc_lit (L_aux(l,_)) =
   utf8string (match l with
@@ -547,7 +568,7 @@ let doc_typdef (TD_aux(td,_)) = match td with
      begin
        match doc_typschm_quants typschm with
        | Some qdoc ->
-          doc_op equals (concat [string "type"; space; doc_id id; space; qdoc]) (doc_typschm_typ typschm)
+          doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typschm_typ typschm)
        | None ->
           doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
      end
@@ -556,12 +577,12 @@ let doc_typdef (TD_aux(td,_)) = match td with
   | TD_record (id, _, TypQ_aux (TypQ_no_forall, _), fields, _) | TD_record (id, _, TypQ_aux (TypQ_tq [], _), fields, _) ->
      separate space [string "struct"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
   | TD_record (id, _, TypQ_aux (TypQ_tq qs, _), fields, _) ->
-     separate space [string "struct"; doc_id id; doc_quants qs; equals;
+     separate space [string "struct"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_field fields) rbrace]
   | TD_variant (id, _, TypQ_aux (TypQ_no_forall, _), unions, _) | TD_variant (id, _, TypQ_aux (TypQ_tq [], _), unions, _) ->
      separate space [string "union"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
   | TD_variant (id, _, TypQ_aux (TypQ_tq qs, _), unions, _) ->
-     separate space [string "union"; doc_id id; doc_quants qs; equals;
+     separate space [string "union"; doc_id id; doc_param_quants qs; equals;
                      surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_union unions) rbrace]
   | _ -> string "TYPEDEF"
 
-- 
cgit v1.2.3


From 666062ce4d97fe48307d1feb5bb4eb32087b177a Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 30 Nov 2018 19:33:50 +0000
Subject: Remove constraint synonyms

They weren't needed for ASL parser like I thought they would be, and
they increase the complexity of dealing with constraints throughout
Sail, so just remove them.

Also fix some compiler warnings
---
 src/pretty_print_sail.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 53e77df2..fe533f00 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -125,7 +125,6 @@ let doc_nc nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
-    | NC_app (id, nexps) -> string "where" ^^ space ^^ doc_id id ^^ parens (separate_map (comma ^^ space) doc_nexp nexps)
     | _ -> nc0 ~parenthesize:true nc
   and nc0 ?parenthesize:(parenthesize=false) (NC_aux (nc_aux, _) as nc) =
     (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if
@@ -640,8 +639,6 @@ let rec doc_def def = group (match def with
   | DEF_fixity (prec, n, id) ->
      fixities := Bindings.add id (prec, Big_int.to_int n) !fixities;
      separate space [doc_prec prec; doc_int n; doc_id id]
-  | DEF_constraint (id, kids, nc) ->
-     separate space [string "constraint"; doc_id id; parens (separate_map (comma ^^ space) doc_kid kids); equals; doc_nc nc]
   | DEF_overload (id, ids) ->
      separate space [string "overload"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
   ) ^^ hardline
-- 
cgit v1.2.3


From df3ea2e6da387ead7cba1e27632768e563696502 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 4 Dec 2018 14:53:23 +0000
Subject: Remove FES_Fexps constructor

This makes dealing with records and field expressions in Sail much
nicer because the constructors are no longer stacked together like
matryoshka dolls with unnecessary layers. Previously to get the fields
of a record it would be either

E_aux (E_record (FES_aux (FES_Fexps (fexps, _), _)), _)

but now it is simply:

E_aux (E_record fexps, _)
---
 src/pretty_print_sail.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index fe533f00..b1efd11d 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -453,7 +453,7 @@ and doc_atomic_exp (E_aux (e_aux, _) as exp) =
      brackets (separate space [doc_exp exp1; string "with"; doc_atomic_exp exp2; string ".."; doc_atomic_exp exp3; equals; doc_exp exp4])
   | E_internal_value v -> string (Value.string_of_value v |> Util.green |> Util.clear)
   | _ -> parens (doc_exp exp)
-and doc_fexps (FES_aux (FES_Fexps (fexps, _), _)) =
+and doc_fexps fexps =
   separate_map (comma ^^ space) doc_fexp fexps
 and doc_fexp (FE_aux (FE_Fexp (id, exp), _)) =
   separate space [doc_id id; equals; doc_exp exp]
-- 
cgit v1.2.3


From 272d9565ef7f48baa0982a291c7fde8497ab0cd9 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 5 Dec 2018 20:49:38 +0000
Subject: Re-factor initial check

Mostly this is to change how we desugar types in order to make us more
flexible with what we can parse as a valid constraint as
type. Previously the structure of the initial check forced some
awkward limitations on what was parseable due to how the parse AST is
set up.

As part of this, I've taken the de-scattering of scattered functions
out of the initial check, and moved it to a re-writing step after
type-checking, where I think it logically belongs. This doesn't change
much right now, but opens up some more possibilities in the future:
Since scattered functions are now typechecked normally, any future
module system for Sail would be able to handle them specially, and the
Latex documentation backend can now document scattered functions
explicitly, rather than relying on hackish 'de-scattering' logic to
present documentation as the functions originally appeared.

This has one slight breaking change which is that union clauses must
appear before their uses in scattered functions, so

union ast = Foo : unit

function clause execute(Foo())

is ok, but

function clause execute(Foo())

union ast = Foo : unit

is not. Previously this worked because the de-scattering moved union
clauses upwards before type-checking, but as this now happens after
type-checking they must appear in the correct order. This doesn't
occur in ARM, RISC-V, MIPS, but did appear in Cheri and I submitted a
pull request to re-order the places where it happens.
---
 src/pretty_print_sail.ml | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index b1efd11d..f9908c71 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -613,13 +613,18 @@ let doc_kind_def (KD_aux (KD_nabbrev (_, id, _, nexp), _)) =
 
 let rec doc_scattered (SD_aux (sd_aux, _)) =
   match sd_aux with
-  | SD_scattered_function (_, _, _, id) ->
+  | SD_function (_, _, _, id) ->
      string "scattered" ^^ space ^^ string "function" ^^ space ^^ doc_id id
-  | SD_scattered_funcl funcl ->
+  | SD_funcl funcl ->
      string "function" ^^ space ^^ string "clause" ^^ space ^^ doc_funcl funcl
-  | SD_scattered_end id ->
+  | SD_end id ->
      string "end" ^^ space ^^ doc_id id
-  | _ -> string "SCATTERED"
+  | SD_variant (id, _, TypQ_aux (TypQ_no_forall, _)) ->
+     string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id
+  | SD_variant (id, _, TypQ_aux (TypQ_tq quants, _)) ->
+     string "scattered" ^^ space ^^ string "union" ^^ space ^^ doc_id id ^^ doc_param_quants quants
+  | SD_unioncl (id, tu) ->
+     separate space [string "union clause"; doc_id id; equals; doc_union tu]
 
 let rec doc_def def = group (match def with
   | DEF_default df -> doc_default df
-- 
cgit v1.2.3


From 25ab845211e3df24386a0573b517a01dab879b03 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Thu, 6 Dec 2018 17:16:06 +0000
Subject: Desugar constraints from atyp rather than n_constraint

Previously the valid constraints had to be carefully restricted to
avoid parser ambiguities between n_constraint and atyp. With the
initial check refactored, we can now parse constraints into atyp using
ATyp_app for the operators, and changing ATyp_constant into a more
general ATyp_lit for true and false. Logically this new structure is
more uniform, as atyp is now the parse representation for all
Bool-kinded things (constraints), Type-kinded things (regular types),
and Int-kinded things (n-expressions), and initial_check.ml now splits
all three into n_constraint, typ, and nexp respectively, rather than
how it was before with initial_check splitting types and nexps, but
constraints already being separate in the parser.
---
 src/pretty_print_sail.ml | 5 ++---
 1 file changed, 2 insertions(+), 3 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f9908c71..5201744b 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -146,9 +146,8 @@ let doc_nc nc =
        end
     | _ -> parens' (separate_map (space ^^ bar ^^ space) nc1 disjs)
   and nc1 (NC_aux (nc_aux, _) as nc) =
-    match nc_aux with
-    | NC_and (c1, c2) -> separate space [nc1 c1; string "&"; atomic_nc c2]
-    | _ -> atomic_nc nc
+    let conjs = constraint_conj nc in
+    separate_map (space ^^ string "&" ^^ space) atomic_nc conjs
   in
   atomic_nc (constraint_simp nc)
 
-- 
cgit v1.2.3


From 2c25110ad2f5e636239ba65a2154aae79ffa253c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Fri, 7 Dec 2018 21:53:29 +0000
Subject: Working on better flow typing for ASL

On a new branch because it's completely broken everything for now
---
 src/pretty_print_sail.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 5201744b..7fb67a06 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -259,7 +259,7 @@ let doc_typschm ?(simple=false) (TypSchm_aux (TypSchm_ts (typq, typ), _)) = doc_
 
 let doc_typschm_typ (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) = doc_typ typ
 
-let doc_typschm_quants (TypSchm_aux (TypSchm_ts (TypQ_aux (tq_aux, _), typ), _)) =
+let doc_typquant (TypQ_aux (tq_aux, _)) =
   match tq_aux with
   | TypQ_no_forall -> None
   | TypQ_tq [] -> None
@@ -562,13 +562,13 @@ let doc_field (typ, id) =
 let doc_union (Tu_aux (Tu_ty_id (typ, id), l)) = separate space [doc_id id; colon; doc_typ typ]
 
 let doc_typdef (TD_aux(td,_)) = match td with
-  | TD_abbrev (id, _, typschm) ->
+  | TD_abbrev (id, typq, typ_arg) ->
      begin
-       match doc_typschm_quants typschm with
+       match doc_typquant typq with
        | Some qdoc ->
-          doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typschm_typ typschm)
+          doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typ_arg typ_arg)
        | None ->
-          doc_op equals (concat [string "type"; space; doc_id id]) (doc_typschm_typ typschm)
+          doc_op equals (concat [string "type"; space; doc_id id]) (doc_typ_arg typ_arg)
      end
   | TD_enum (id, _, ids, _) ->
      separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
-- 
cgit v1.2.3


From d8f0854ca9d80d3af8d6a4aaec778643eda9421c Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Sat, 8 Dec 2018 01:06:28 +0000
Subject: Compiling again

Change Typ_arg_ to A_. We use it a lot more now typ_arg is used instead of
uvar as the result of unify. Plus A_ could either stand for argument, or
Any/A type which is quite appropriate in most use cases.

Restore instantiation info in infer_funapp'. Ideally we would save this
instead of recomputing it ever time we need it. However I checked and
there are over 300 places in the code that would need to be changed to add
an extra argument to E_app. Still some issues causing specialisation to
fail however.

Improve the error message when we swap how we infer/check an l-expression,
as this could previously cause the actual cause of a type-checking failure
to be effectively hidden.
---
 src/pretty_print_sail.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 7fb67a06..bae1b893 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -165,7 +165,7 @@ let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   (* Resugar set types like {|1, 2, 3|} *)
   | Typ_exist ([kid1],
                NC_aux (NC_set (kid2, ints), _),
-               Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
+               Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
          when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
   | Typ_exist (kids, nc, typ) ->
@@ -181,11 +181,11 @@ let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   | Typ_bidir (typ1, typ2) ->
      separate space [doc_typ typ1; string "<->"; doc_typ typ2]
   | Typ_internal_unknown -> raise (Reporting.err_unreachable l __POS__ "escaped Typ_internal_unknown")
-and doc_typ_arg (Typ_arg_aux (ta_aux, _)) =
+and doc_typ_arg (A_aux (ta_aux, _)) =
   match ta_aux with
-  | Typ_arg_typ typ -> doc_typ typ
-  | Typ_arg_nexp nexp -> doc_nexp nexp
-  | Typ_arg_order o -> doc_ord o
+  | A_typ typ -> doc_typ typ
+  | A_nexp nexp -> doc_nexp nexp
+  | A_order o -> doc_ord o
 and doc_arg_typs = function
   | [typ] -> doc_typ typ
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
-- 
cgit v1.2.3


From ab4b9ca4f7cab45b6a2a13d0ef125dcf9c276a06 Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 11 Dec 2018 19:54:14 +0000
Subject: Fix all tests with type checking changes

---
 src/pretty_print_sail.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index bae1b893..94bcd54b 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -279,7 +279,7 @@ let doc_lit (L_aux(l,_)) =
   | L_undef -> "undefined"
   | L_string s -> "\"" ^ String.escaped s ^ "\"")
 
-let rec doc_pat (P_aux (p_aux, _) as pat) =
+let rec doc_pat (P_aux (p_aux, (l, _)) as pat) =
   match p_aux with
   | P_id id -> doc_id id
   | P_or (pat1, pat2) -> parens (doc_pat pat1 ^^ string " | " ^^ doc_pat pat2)
@@ -297,7 +297,11 @@ let rec doc_pat (P_aux (p_aux, _) as pat) =
   | P_as (pat, id) -> parens (separate space [doc_pat pat; string "as"; doc_id id])
   | P_app (id, pats) -> doc_id id ^^ parens (separate_map (comma ^^ space) doc_pat pats)
   | P_list pats -> string "[|" ^^ separate_map (comma ^^ space) doc_pat pats ^^ string "|]"
-  | _ -> string (string_of_pat pat)
+  | P_cons (hd_pat, tl_pat) -> separate space [doc_pat hd_pat; string "::"; doc_pat tl_pat]
+  | P_string_append [] -> string "\"\""
+  | P_string_append pats ->
+     parens (separate_map (string " ^ ") doc_pat pats)
+  | P_record _ -> raise (Reporting.err_unreachable l __POS__ "P_record passed to doc_pat")
 
 (* if_block_x is true if x should be printed like a block, i.e. with
    newlines. Blocks are automatically printed as blocks, so this
-- 
cgit v1.2.3


From c65aecd008d34102f4c95649113ed7f9afcc903b Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Wed, 12 Dec 2018 00:49:32 +0000
Subject: Fix various boolean type-variable related issues

Remove some dead code in Pretty_print_common

Start thinking a bit about Minisail-esque syntactic sugar in initial_check
---
 src/pretty_print_sail.ml | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index 94bcd54b..f756f3d2 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -113,7 +113,7 @@ let rec doc_nexp =
   in
   nexp0
 
-let doc_nc nc =
+let rec doc_nc nc =
   let nc_op op n1 n2 = separate space [doc_nexp n1; string op; doc_nexp n2] in
   let rec atomic_nc (NC_aux (nc_aux, _) as nc) =
     match nc_aux with
@@ -125,7 +125,10 @@ let doc_nc nc =
     | NC_bounded_le (n1, n2) -> nc_op "<=" n1 n2
     | NC_set (kid, ints) ->
        separate space [doc_kid kid; string "in"; braces (separate_map (comma ^^ space) doc_int ints)]
-    | _ -> nc0 ~parenthesize:true nc
+    | NC_app (id, args) ->
+       doc_id id ^^ parens (separate_map (comma ^^ space) doc_typ_arg args)
+    | NC_var kid -> doc_kid kid
+    | NC_or _ | NC_and _ -> nc0 ~parenthesize:true nc
   and nc0 ?parenthesize:(parenthesize=false) (NC_aux (nc_aux, _) as nc) =
     (* Rather than parens (nc0 x) we use nc0 ~parenthesize:true x, because if
        we rewrite a disjunction as a set constraint, then we can
@@ -151,7 +154,7 @@ let doc_nc nc =
   in
   atomic_nc (constraint_simp nc)
 
-let rec doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
+and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   match typ_aux with
   | Typ_id id -> doc_id id
   | Typ_app (id, []) -> doc_id id
@@ -186,6 +189,7 @@ and doc_typ_arg (A_aux (ta_aux, _)) =
   | A_typ typ -> doc_typ typ
   | A_nexp nexp -> doc_nexp nexp
   | A_order o -> doc_ord o
+  | A_bool nc -> doc_nc nc
 and doc_arg_typs = function
   | [typ] -> doc_typ typ
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
-- 
cgit v1.2.3


From cdf287dfb69275e479d79ebc0d305e365dd3ee7b Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Wed, 12 Dec 2018 01:45:20 +0000
Subject: Remove KOpt_none constructor

We should infer type variable kinds better in initial_check.ml, but we really don't want to have to deal
with that everywhere, especially when we can no longer easily cheat and assume KOpt_none implies K_int.
---
 src/pretty_print_sail.ml | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index f756f3d2..d779b3a7 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -195,7 +195,6 @@ and doc_arg_typs = function
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
 
 let doc_kopt = function
-  | KOpt_aux (KOpt_none kid, _) -> doc_kid kid
   | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
   | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
   | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
@@ -203,7 +202,6 @@ let doc_kopt = function
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
     | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
     | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
     | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
@@ -224,7 +222,6 @@ let doc_quants quants =
 let doc_param_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-    | QI_id (KOpt_aux (KOpt_none kid, _)) -> [doc_kid kid]
     | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
     | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
     | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
-- 
cgit v1.2.3


From ed5b58ba3a5a73253565edcb6460d2b48f56f887 Mon Sep 17 00:00:00 2001
From: Alasdair
Date: Wed, 12 Dec 2018 03:42:10 +0000
Subject: Generalise existentials for non-integer type variables

---
 src/pretty_print_sail.ml | 23 ++++++++++++-----------
 1 file changed, 12 insertions(+), 11 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index d779b3a7..e0223105 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -65,6 +65,12 @@ let doc_id (Id_aux (id_aux, _)) =
 
 let doc_kid kid = string (Ast_util.string_of_kid kid)
 
+let doc_kopt = function
+  | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
+  | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
+  | kopt when is_order_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
+  | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])
+                
 let doc_int n = string (Big_int.to_string n)
 
 let docstring (l, _) = match l with
@@ -166,13 +172,13 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
   (* Resugar set types like {|1, 2, 3|} *)
-  | Typ_exist ([kid1],
-               NC_aux (NC_set (kid2, ints), _),
-               Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid3, _)), _)]), _))
-         when Kid.compare kid1 kid2 == 0 && Kid.compare kid2 kid3 == 0 && Id.compare (mk_id "atom") id == 0 ->
+  | Typ_exist ([kopt],
+               NC_aux (NC_set (kid1, ints), _),
+               Typ_aux (Typ_app (id, [A_aux (A_nexp (Nexp_aux (Nexp_var kid2, _)), _)]), _))
+         when Kid.compare (kopt_kid kopt) kid1 == 0 && Kid.compare kid1 kid2 == 0 && Id.compare (mk_id "atom") id == 0 ->
      enclose (string "{|") (string "|}") (separate_map (string ", ") doc_int ints)
-  | Typ_exist (kids, nc, typ) ->
-     braces (separate_map space doc_kid kids ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
+  | Typ_exist (kopts, nc, typ) ->
+     braces (separate_map space doc_kopt kopts ^^ comma ^^ space ^^ doc_nc nc ^^ dot ^^ space ^^ doc_typ typ)
   | Typ_fn (typs, typ, Effect_aux (Effect_set [], _)) ->
      separate space [doc_arg_typs typs; string "->"; doc_typ typ]
   | Typ_fn (typs, typ, Effect_aux (Effect_set effs, _)) ->
@@ -194,11 +200,6 @@ and doc_arg_typs = function
   | [typ] -> doc_typ typ
   | typs -> parens (separate_map (comma ^^ space) doc_typ typs)
 
-let doc_kopt = function
-  | kopt when is_nat_kopt kopt -> doc_kid (kopt_kid kopt)
-  | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
-  | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
-
 let doc_quants quants =
   let doc_qi_kopt (QI_aux (qi_aux, _)) =
     match qi_aux with
-- 
cgit v1.2.3


From 56fb5bf999d7cc900d6535da4168e220862d3d9c Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Wed, 12 Dec 2018 17:37:13 +0000
Subject: Add a test case for various simple boolean properties

test/typecheck/pass/tautology.sail constaints tests of various boolean
properties, e.g.

  // de Morgan
  _prove(constraint(not('p | 'q) <--> not('p) & not('q)));
  _prove(constraint(not('p & 'q) <--> not('p) | not('q)));

introduce a new _not_prove case which allows us to assert in tests
that a constraint is not provable. This test essentially tests that
constraints map to sensible problems in the SMT solver, without
testing flow typing or any other features.

Add a script test/typecheck/update_errors.sh, which regenerates the
expected error messages. Testing that type-checking failures is
important, but can be brittle when the error messages change for
inconsequential reasons. This script automates fixing this.

Also ensure that this test case works correctly in Lem
---
 src/pretty_print_sail.ml | 17 ++++++++++++++---
 1 file changed, 14 insertions(+), 3 deletions(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index e0223105..c4b9bdd3 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -70,7 +70,7 @@ let doc_kopt = function
   | kopt when is_typ_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])
   | kopt when is_order_kopt kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])
   | kopt -> parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])
-                
+
 let doc_int n = string (Big_int.to_string n)
 
 let docstring (l, _) = match l with
@@ -168,6 +168,8 @@ and doc_typ ?(simple=false) (Typ_aux (typ_aux, l)) =
      separate space [doc_typ_arg x; doc_typ_arg y]
   | Typ_app (id, typs) when Id.compare id (mk_id "atom") = 0 ->
      string "int" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
+  | Typ_app (id, typs) when Id.compare id (mk_id "atom_bool") = 0 ->
+     string "bool" ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_app (id, typs) -> doc_id id ^^ parens (separate_map (string ", ") doc_typ_arg typs)
   | Typ_tup typs -> parens (separate_map (string ", ") doc_typ typs)
   | Typ_var kid -> doc_kid kid
@@ -205,6 +207,7 @@ let doc_quants quants =
     match qi_aux with
     | QI_id kopt when is_nat_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Int"])]
     | QI_id kopt when is_typ_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Type"])]
+    | QI_id kopt when is_bool_kopt kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Bool"])]
     | QI_id kopt -> [parens (separate space [doc_kid (kopt_kid kopt); colon; string "Order"])]
     | QI_const nc -> []
   in
@@ -225,6 +228,7 @@ let doc_param_quants quants =
     match qi_aux with
     | QI_id kopt when is_nat_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Int"]
     | QI_id kopt when is_typ_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Type"]
+    | QI_id kopt when is_bool_kopt kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Bool"]
     | QI_id kopt -> [doc_kid (kopt_kid kopt) ^^ colon ^^ space ^^ string "Order"]
     | QI_const nc -> []
   in
@@ -567,14 +571,21 @@ let doc_field (typ, id) =
 
 let doc_union (Tu_aux (Tu_ty_id (typ, id), l)) = separate space [doc_id id; colon; doc_typ typ]
 
+let doc_typ_arg_kind (A_aux (aux, _)) =
+  match aux with
+  | A_nexp _ -> space ^^ string "->" ^^ space ^^string "Int"
+  | A_bool _ -> space ^^ string "->" ^^ space ^^ string "Bool"
+  | A_order  _ -> space ^^ string "->" ^^ space ^^ string "Order"
+  | A_typ _ -> empty
+
 let doc_typdef (TD_aux(td,_)) = match td with
   | TD_abbrev (id, typq, typ_arg) ->
      begin
        match doc_typquant typq with
        | Some qdoc ->
-          doc_op equals (concat [string "type"; space; doc_id id; qdoc]) (doc_typ_arg typ_arg)
+          doc_op equals (concat [string "type"; space; doc_id id; qdoc; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
        | None ->
-          doc_op equals (concat [string "type"; space; doc_id id]) (doc_typ_arg typ_arg)
+          doc_op equals (concat [string "type"; space; doc_id id; doc_typ_arg_kind typ_arg]) (doc_typ_arg typ_arg)
      end
   | TD_enum (id, _, ids, _) ->
      separate space [string "enum"; doc_id id; equals; surround 2 0 lbrace (separate_map (comma ^^ break 1) doc_id ids) rbrace]
-- 
cgit v1.2.3


From e5d108332cf700f73ea7b7527d0ae6006b0944c5 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Mon, 17 Dec 2018 12:23:30 +0000
Subject: Adapt Coq and termination measure support to typechecker changes Also
 output termination measures in Sail printer

---
 src/pretty_print_sail.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/pretty_print_sail.ml')

diff --git a/src/pretty_print_sail.ml b/src/pretty_print_sail.ml
index c4b9bdd3..345312f7 100644
--- a/src/pretty_print_sail.ml
+++ b/src/pretty_print_sail.ml
@@ -509,14 +509,21 @@ let doc_funcl (FCL_aux (FCL_Funcl (id, Pat_aux (pexp,_)), _)) =
 
 let doc_default (DT_aux (DT_order ord, _)) = separate space [string "default"; string "Order"; doc_ord ord]
 
+let doc_rec (Rec_aux (r,_)) =
+  match r with
+  | Rec_nonrec
+  | Rec_rec -> empty
+  | Rec_measure (pat,exp) -> braces (doc_pat pat ^^ string " => " ^^ doc_exp exp) ^^ space
+
 let doc_fundef (FD_aux (FD_function (r, typa, efa, funcls), annot)) =
   docstring annot
   ^^ match funcls with
      | [] -> failwith "Empty function list"
      | _ ->
+        let rec_pp = doc_rec r in
         let sep = hardline ^^ string "and" ^^ space in
         let clauses = separate_map sep doc_funcl funcls in
-        string "function" ^^ space ^^ clauses
+        string "function" ^^ space ^^ rec_pp ^^ clauses
 
 let rec doc_mpat (MP_aux (mp_aux, _) as mpat) =
   match mp_aux with
-- 
cgit v1.2.3