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.

4 files changed, 63 insertions, 17 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index f0b6508b..037fd1a7 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -399,6 +399,13 @@ let mk_effect effs =
 
 let no_effect = mk_effect []
 
+let quant_add qi typq =
+  match qi, typq with
+  | QI_aux (QI_const (NC_aux (NC_true, _)), _), _ -> typq
+  | QI_aux (QI_id _, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qi :: qis), l)
+  | QI_aux (QI_const nc, _), TypQ_aux (TypQ_tq qis, l) -> TypQ_aux (TypQ_tq (qis @ [qi]), l)
+  | _, TypQ_aux (TypQ_no_forall, l) -> TypQ_aux (TypQ_tq [qi], l)
+
 let quant_items : typquant -> quant_item list = function
   | TypQ_aux (TypQ_tq qis, _) -> qis
   | TypQ_aux (TypQ_no_forall, _) -> []
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 2a303475..8f555744 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -175,6 +175,8 @@ val nc_int_set : kid -> int list -> n_constraint
    de-morgans to switch and to or and vice versa. *)
 val nc_negate : n_constraint -> n_constraint
 
+(* Functions for working with type quantifiers *)
+val quant_add : quant_item -> typquant -> typquant
 val quant_items : typquant -> quant_item list
 val quant_kopts : typquant -> kinded_id list
 val quant_split : typquant -> kinded_id list * n_constraint list
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
diff --git a/src/type_check.ml b/src/type_check.ml
index e11505e5..aa2d3473 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -754,17 +754,52 @@ end = struct
     with
     | Not_found -> typ_error (id_loc id) ("No val spec found for " ^ string_of_id id)
 
+  let ex_counter = ref 0
+
+  (* TODO: Currently this is duplicated with destruct_exist outside of Env and deals with val spec arguments only. *)
+  let fresh_existential ?name:(n="") () =
+    let fresh = Kid_aux (Var ("'all" ^ string_of_int !ex_counter ^ "#" ^ n), Parse_ast.Unknown) in
+    incr ex_counter; fresh
+
+  let destruct_exist env typ =
+    match expand_synonyms env typ with
+    | Typ_aux (Typ_exist (kids, nc, typ), _) ->
+       let fresh_kids = List.map (fun kid -> (kid, fresh_existential ~name:(string_of_id (id_of_kid kid)) ())) kids in
+       let nc = List.fold_left (fun nc (kid, fresh) -> nc_subst_nexp kid (Nexp_var fresh) nc) nc fresh_kids in
+       let typ = List.fold_left (fun typ (kid, fresh) -> typ_subst_nexp kid (Nexp_var fresh) typ) typ fresh_kids in
+       Some (List.map snd fresh_kids, nc, typ)
+    | _ -> None
+
   let rec update_val_spec id (typq, typ) env =
-    begin
-      let typ = expand_synonyms env typ in
-      let typq = expand_typquant_synonyms env typq in
-      typ_print (lazy (adding ^ "val spec " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
-      let env = match typ with
-        | Typ_aux (Typ_bidir (typ1, typ2), _) -> add_mapping id (typq, typ1, typ2) env
-        | _ -> env
-      in
-      { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
+    begin match expand_synonyms env typ with
+    | Typ_aux (Typ_fn (arg_typs, ret_typ, effect), l) ->
+       (* We perform some canonicalisation for function types where existentials appear on the left, so
+          ({'n, 'n >= 2, int('n)}, foo) -> bar
+          would become
+          forall 'n, 'n >= 2. (int('n), foo) -> bar
+          this enforces the invariant that all things on the left of functions are 'base types' (i.e. without existentials)
+        *)
+       let typq = expand_typquant_synonyms env typq in
+       let base_args = List.map (destruct_exist env) arg_typs in
+       let existential_arg typq = function
+         | None -> typq
+         | Some (exs, nc, _) ->
+            List.fold_left (fun typq kid -> quant_add (mk_qi_id BK_int kid) typq) (quant_add (mk_qi_nc nc) typq) exs
+       in
+       let typq = List.fold_left existential_arg typq base_args in
+       let arg_typs = List.map2 (fun typ -> function Some (_, _, typ) -> typ | None -> typ) arg_typs base_args in
+       let typ = Typ_aux (Typ_fn (arg_typs, ret_typ, effect), l) in
+       typ_print (lazy (adding ^ "val " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
+       { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
+
+    | Typ_aux (Typ_bidir (typ1, typ2), l) ->
+       let env = add_mapping id (typq, typ1, typ2) env in
+       typ_print (lazy (adding ^ "mapping " ^ string_of_id id ^ " : " ^ string_of_bind (typq, typ)));
+       { env with top_val_specs = Bindings.add id (typq, typ) env.top_val_specs }
+
+    | _ -> typ_error (id_loc id) "val definition must have a mapping or function type"
     end
+
   and add_val_spec id (bind_typq, bind_typ) env =
     if not (Bindings.mem id env.top_val_specs)
     then update_val_spec id (bind_typq, bind_typ) env
@@ -776,6 +811,7 @@ end = struct
         typ_error (id_loc id) ("Identifier " ^ string_of_id id ^ " is already bound as " ^ string_of_bind (existing_typq, existing_typ) ^ ", cannot rebind as " ^ string_of_bind (bind_typq, bind_typ))
       else
         env
+
   and add_mapping id (typq, typ1, typ2) env =
     begin
       typ_print (lazy (adding ^ "mapping " ^ string_of_id id));