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