Merge branch 'sail2' into rmem_interpreter

17 files changed, 224 insertions, 233 deletions

diff --git a/src/ast_util.ml b/src/ast_util.ml
index b9ab21b2..1d0689e4 100644
--- a/src/ast_util.ml
+++ b/src/ast_util.ml
@@ -296,7 +296,7 @@ let bool_typ = mk_id_typ (mk_id "bool")
 let string_typ = mk_id_typ (mk_id "string")
 let list_typ typ = mk_typ (Typ_app (mk_id "list", [mk_typ_arg (Typ_arg_typ typ)]))
 let tuple_typ typs = mk_typ (Typ_tup typs)
-let function_typ typ1 typ2 eff = mk_typ (Typ_fn (typ1, typ2, eff))
+let function_typ arg_typs ret_typ eff = mk_typ (Typ_fn (arg_typs, ret_typ, eff))
 
 let vector_typ n ord typ =
   mk_typ (Typ_app (mk_id "vector",
@@ -613,8 +613,11 @@ and string_of_typ_aux = function
   | Typ_var kid -> string_of_kid kid
   | Typ_tup typs -> "(" ^ string_of_list ", " string_of_typ typs ^ ")"
   | Typ_app (id, args) -> string_of_id id ^ "(" ^ string_of_list ", " string_of_typ_arg args ^ ")"
-  | Typ_fn (typ_arg, typ_ret, eff) ->
-     string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
+  | Typ_fn ([typ_arg], typ_ret, eff) ->
+     string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff     
+  | Typ_fn (typ_args, typ_ret, eff) ->
+     "(" ^ string_of_list ", " string_of_typ typ_args ^ ") -> "
+     ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
   | Typ_bidir (typ1, typ2) -> string_of_typ typ1 ^ " <-> " ^ string_of_typ typ2
   | Typ_exist (kids, nc, typ) ->
      "{" ^ string_of_list " " string_of_kid kids ^ ", " ^ string_of_n_constraint nc ^ ". " ^ string_of_typ typ ^ "}"
@@ -901,8 +904,8 @@ module Typ = struct
     | Typ_internal_unknown, Typ_internal_unknown -> 0
     | Typ_id id1, Typ_id id2 -> Id.compare id1 id2
     | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2
-    | Typ_fn (t1,t2,e1), Typ_fn (t3,t4,e2) ->
-       (match compare t1 t3 with
+    | Typ_fn (ts1,t2,e1), Typ_fn (ts3,t4,e2) ->
+       (match Util.compare_list compare ts1 ts3 with
        | 0 -> (match compare t2 t4 with
          | 0 -> effect_compare e1 e2
          | n -> n)
@@ -1084,7 +1087,7 @@ let rec tyvars_of_typ (Typ_aux (t,_)) =
   | Typ_internal_unknown -> KidSet.empty
   | Typ_id _ -> KidSet.empty
   | Typ_var kid -> KidSet.singleton kid
-  | Typ_fn (t1,t2,_) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
+  | Typ_fn (ts, t, _) -> List.fold_left KidSet.union (tyvars_of_typ t) (List.map tyvars_of_typ ts)
   | Typ_bidir (t1, t2) -> KidSet.union (tyvars_of_typ t1) (tyvars_of_typ t2)
   | Typ_tup ts ->
      List.fold_left (fun s t -> KidSet.union s (tyvars_of_typ t))
@@ -1345,7 +1348,8 @@ let rec locate_typ l (Typ_aux (typ_aux, _)) =
     | Typ_internal_unknown -> Typ_internal_unknown
     | Typ_id id -> Typ_id (locate_id l id)
     | Typ_var kid -> Typ_var (locate_kid l kid)
-    | Typ_fn (arg_typ, ret_typ, effect) -> Typ_fn (locate_typ l arg_typ, locate_typ l ret_typ, locate_effect l effect)
+    | Typ_fn (arg_typs, ret_typ, effect) ->
+       Typ_fn (List.map (locate_typ l) arg_typs, locate_typ l ret_typ, locate_effect l effect)
     | Typ_bidir (typ1, typ2) -> Typ_bidir (locate_typ l typ1, locate_typ l typ2)
     | Typ_tup typs -> Typ_tup (List.map (locate_typ l) typs)
     | Typ_exist (kids, constr, typ) -> Typ_exist (List.map (locate_kid l) kids, locate_nc l constr, locate_typ l typ)
diff --git a/src/ast_util.mli b/src/ast_util.mli
index 9dafbcd8..bbe9463e 100644
--- a/src/ast_util.mli
+++ b/src/ast_util.mli
@@ -132,7 +132,7 @@ val vector_typ : nexp -> order -> typ -> typ
 val list_typ : typ -> typ
 val exc_typ : typ
 val tuple_typ : typ list -> typ
-val function_typ : typ -> typ -> effect -> typ
+val function_typ : typ list -> typ -> effect -> typ
 
 val no_effect : effect
 val mk_effect : base_effect_aux list -> effect
diff --git a/src/c_backend.ml b/src/c_backend.ml
index d58094ca..d825bbae 100644
--- a/src/c_backend.ml
+++ b/src/c_backend.ml
@@ -568,8 +568,7 @@ let cdef_ctyps ctx = function
   | CDEF_fundef (id, _, _, instrs) ->
      let _, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-       | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let arg_ctyps, ret_ctyp = List.map (ctyp_of_typ ctx) arg_typs, ctyp_of_typ ctx ret_typ in
@@ -803,8 +802,7 @@ let compile_funcall l ctx id args typ =
       c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env
   in
   let arg_typs, ret_typ = match fn_typ with
-    | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-    | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+    | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
     | _ -> assert false
   in
   let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in
@@ -1304,7 +1302,6 @@ let compile_type_def ctx (TD_aux (type_def, _)) =
 
   | TD_variant (id, _, _, tus, _) ->
      let compile_tu = function
-       | Tu_aux (Tu_ty_id (Typ_aux (Typ_fn (typ, _, _), _), id), _) -> ctyp_of_typ ctx typ, id
        | Tu_aux (Tu_ty_id (typ, id), _) -> ctyp_of_typ ctx typ, id
      in
      let ctus = List.fold_left (fun ctus (ctyp, id) -> Bindings.add id ctyp ctus) Bindings.empty (List.map compile_tu tus) in
@@ -1540,8 +1537,7 @@ let rec compile_def ctx = function
      c_debug (lazy "Compiling VS");
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-       | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in
@@ -1556,8 +1552,8 @@ let rec compile_def ctx = function
        with Type_error _ ->
          c_debug (lazy ("Falling back to global env for " ^ string_of_id id)); Env.get_val_spec id ctx.tc_env
      in
-     let arg_typ, ret_typ = match fn_typ with
-       | Typ_fn (arg_typ, ret_typ, _) -> arg_typ, ret_typ
+     let arg_typs, ret_typ = match fn_typ with
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
 
@@ -1567,10 +1563,7 @@ let rec compile_def ctx = function
      (* The context must be updated before we call ctyp_of_typ on the argument types. *)
      let ctx = { ctx with local_env = add_typquant (id_loc id) quant ctx.tc_env } in
 
-     let arg_ctyps = match arg_typ with
-       | Typ_aux (Typ_tup arg_typs, _) -> List.map (ctyp_of_typ ctx) arg_typs
-       | _ -> [ctyp_of_typ ctx arg_typ]
-     in
+     let arg_ctyps =  List.map (ctyp_of_typ ctx) arg_typs in
      let ret_ctyp = ctyp_of_typ ctx ret_typ in
 
      (* Optimize and compile the expression to ANF. *)
@@ -2790,8 +2783,7 @@ let codegen_def' ctx = function
      (* Extract type information about the function from the environment. *)
      let quant, Typ_aux (fn_typ, _) = Env.get_val_spec id ctx.tc_env in
      let arg_typs, ret_typ = match fn_typ with
-       | Typ_fn (Typ_aux (Typ_tup arg_typs, _), ret_typ, _) -> arg_typs, ret_typ
-       | Typ_fn (arg_typ, ret_typ, _) -> [arg_typ], ret_typ
+       | Typ_fn (arg_typs, ret_typ, _) -> arg_typs, ret_typ
        | _ -> assert false
      in
      let ctx' = { ctx with local_env = add_typquant (id_loc id) quant ctx.local_env } in
diff --git a/src/gen_lib/sail2_string.lem b/src/gen_lib/sail2_string.lem
index c50db099..de7588dc 100644
--- a/src/gen_lib/sail2_string.lem
+++ b/src/gen_lib/sail2_string.lem
@@ -20,6 +20,10 @@ val string_drop : string -> ii -> string
 let string_drop str n =
   toString (drop (natFromInteger n) (toCharList str))
 
+val string_take : string -> ii -> string
+let string_take str n =
+  toString (take (natFromInteger n) (toCharList str))
+
 val string_length : string -> ii
 let string_length s = integerFromNat (stringLength s)
 
diff --git a/src/initial_check.ml b/src/initial_check.ml
index dcb7a925..4e6e941d 100644
--- a/src/initial_check.ml
+++ b/src/initial_check.ml
@@ -182,9 +182,16 @@ let rec to_ast_typ (k_env : kind Envmap.t) (def_ord : order) (t: Parse_ast.atyp)
                                  | K_infer -> k.k <- K_Typ; Typ_var v
                                  | _ -> typ_error l "Required a variable with kind Type, encountered " None (Some v) (Some k))
                    | None -> typ_error l "Encountered an unbound variable" None (Some v) None)
-               | Parse_ast.ATyp_fn(arg,ret,efct) -> Typ_fn( (to_ast_typ k_env def_ord arg),
-                                                            (to_ast_typ k_env def_ord ret),
-                                                            (to_ast_effects k_env efct))
+               | Parse_ast.ATyp_fn(arg,ret,efct) ->
+                  begin match arg with
+                  | Parse_ast.ATyp_aux (Parse_ast.ATyp_tup args, _) ->
+                     Typ_fn (List.map (to_ast_typ k_env def_ord) args,
+                             (to_ast_typ k_env def_ord ret),
+                             (to_ast_effects k_env efct))
+                  | _ -> Typ_fn ([to_ast_typ k_env def_ord arg],
+                                 (to_ast_typ k_env def_ord ret),
+                                 (to_ast_effects k_env efct))
+                  end
                | Parse_ast.ATyp_bidir (typ1, typ2) -> Typ_bidir ( (to_ast_typ k_env def_ord typ1),
                                                                   (to_ast_typ k_env def_ord typ2))
                | Parse_ast.ATyp_tup(typs) -> Typ_tup( List.map (to_ast_typ k_env def_ord) typs)
@@ -1093,11 +1100,11 @@ let quant_item_arg = function
 let undefined_typschm id typq =
   let qis = quant_items typq in
   if qis = [] then
-    mk_typschm typq (mk_typ (Typ_fn (unit_typ, mk_typ (Typ_id id), mk_effect [BE_undef])))
+    mk_typschm typq (function_typ [unit_typ] (mk_typ (Typ_id id)) (mk_effect [BE_undef]))
   else
-    let arg_typ = mk_typ (Typ_tup (List.concat (List.map quant_item_typ qis))) in
+    let arg_typs = List.concat (List.map quant_item_typ qis) in
     let ret_typ = app_typ id (List.concat (List.map quant_item_arg qis)) in
-    mk_typschm typq (mk_typ (Typ_fn (arg_typ, ret_typ, mk_effect [BE_undef])))
+    mk_typschm typq (function_typ arg_typs ret_typ (mk_effect [BE_undef]))
 
 let have_undefined_builtins = ref false
 
@@ -1132,6 +1139,10 @@ let generate_undefineds vs_ids (Defs defs) =
        mk_exp (E_app (id, List.map (fun _ -> mk_lit_exp L_undef) typs))
     | Tu_aux (Tu_ty_id (typ, id), _) -> mk_exp (E_app (id, [mk_lit_exp L_undef]))
   in
+  let p_tup = function
+    | [pat] -> pat
+    | pats -> mk_pat (P_tup pats)
+  in
   let undefined_td = function
     | TD_enum (id, _, ids, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
        let typschm = typschm_of_string dec_ord ("unit -> " ^ string_of_id id ^ " effect {undef}") in
@@ -1144,13 +1155,13 @@ let generate_undefineds vs_ids (Defs defs) =
                                mk_exp (E_app (mk_id "internal_pick",
                                               [mk_exp (E_list (List.map (fun id -> mk_exp (E_id id)) ids))])))]]
     | TD_record (id, _, typq, fields, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
-       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
+       let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        [mk_val_spec (VS_val_spec (undefined_typschm id typq, prepend_id "undefined_" id, (fun _ -> None), false));
         mk_fundef [mk_funcl (prepend_id "undefined_" id)
                             pat
                             (mk_exp (E_record (mk_fexps (List.map (fun (_, id) -> mk_fexp id (mk_lit_exp L_undef)) fields))))]]
     | TD_variant (id, _, typq, tus, _) when not (IdSet.mem (prepend_id "undefined_" id) vs_ids) ->
-       let pat = mk_pat (P_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id)))) in
+       let pat = p_tup (quant_items typq |> List.map quant_item_param |> List.concat |> List.map (fun id -> mk_pat (P_id id))) in
        let body =
          if !opt_fast_undefined && List.length tus > 0 then
            undefined_tu (List.hd tus)
@@ -1256,7 +1267,7 @@ let generate_enum_functions vs_ids (Defs defs) =
          else
            [ enum_val_spec name
               [mk_qi_id BK_int kid; mk_qi_nc (range_constraint kid)]
-              (function_typ (atom_typ (nvar kid)) (mk_typ (Typ_id id)) no_effect);
+              (function_typ [atom_typ (nvar kid)] (mk_typ (Typ_id id)) no_effect);
              mk_fundef [funcl] ]
        in
 
@@ -1273,7 +1284,7 @@ let generate_enum_functions vs_ids (Defs defs) =
          in
          if IdSet.mem name vs_ids then []
          else
-           [ enum_val_spec name [] (function_typ (mk_typ (Typ_id id)) to_typ no_effect);
+           [ enum_val_spec name [] (function_typ [mk_typ (Typ_id id)] to_typ no_effect);
              mk_fundef [funcl] ]
        in
        enum :: to_enum @ from_enum @ gen_enums defs
diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index aaf1672a..f7a481e6 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -135,7 +135,7 @@ let subst_src_typ substs t =
     | Typ_id _
     | Typ_var _
       -> ty
-    | Typ_fn (t1,t2,e) -> re (Typ_fn (s_styp substs t1, s_styp substs t2,e))
+    | Typ_fn (t1,t2,e) -> re (Typ_fn (List.map (s_styp substs) t1, s_styp substs t2,e))
     | Typ_bidir (t1, t2) -> re (Typ_bidir (s_styp substs t1, s_styp substs t2))
     | Typ_tup ts -> re (Typ_tup (List.map (s_styp substs) ts))
     | Typ_app (id,tas) -> re (Typ_app (id,List.map (s_starg substs) tas))
@@ -353,7 +353,7 @@ let rec contains_exist (Typ_aux (ty,l)) =
   | Typ_id _
   | Typ_var _
     -> false
-  | Typ_fn (t1,t2,_) -> contains_exist t1 || contains_exist t2
+  | Typ_fn (t1,t2,_) -> List.exists contains_exist t1 || contains_exist t2
   | Typ_bidir (t1, t2) -> contains_exist t1 || contains_exist t2
   | Typ_tup ts -> List.exists contains_exist ts
   | Typ_app (_,args) -> List.exists contains_exist_arg args
@@ -519,7 +519,8 @@ let refine_constructor refinements l env id args =
   | (_,irefinements) -> begin
     let (_,constr_ty) = Env.get_val_spec id env in
     match constr_ty with
-    | Typ_aux (Typ_fn (constr_ty,_,_),_) -> begin
+    (* A constructor should always have a single argument. *)
+    | Typ_aux (Typ_fn ([constr_ty],_,_),_) -> begin
        let arg_ty = typ_of_args args in
        match Type_check.destruct_exist env constr_ty with
        | None -> None
@@ -2302,14 +2303,9 @@ let rewrite_size_parameters env (Defs defs) =
     let pat,guard,exp,pannot = destruct_pexp pexp in
     let env = env_of_annot (l,ann) in
     let _, typ = Env.get_val_spec_orig id env in
-    let typ = match typ with
-      | Typ_aux (Typ_fn (arg_typ,_,_),_) -> arg_typ
-      | _ -> typ (* TODO: error *)
-    in
-    let types =
-      match pat, Env.expand_synonyms env typ with
-      | P_aux (P_tup ps,_), Typ_aux (Typ_tup ts,_) -> ts
-      | _, _ -> [typ]
+    let types = match typ with
+      | Typ_aux (Typ_fn (arg_typs,_,_),_) -> List.map (Env.expand_synonyms env) arg_typs
+      | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function clause does not have a function type")
     in
     let add_parameter (i,nmap) typ =
       let nmap =
@@ -2451,10 +2447,8 @@ in *)
             let typschm = match typschm with
               | TypSchm_aux (TypSchm_ts (tq,typ),l) ->
                  let typ = match typ with
-                   | Typ_aux (Typ_fn (Typ_aux (Typ_tup ts,l),t2,eff),l2) ->
-                      Typ_aux (Typ_fn (Typ_aux (Typ_tup (mapat (replace_type env) to_change ts),l),t2,eff),l2)
-                   | Typ_aux (Typ_fn (typ,t2,eff),l2) ->
-                      Typ_aux (Typ_fn (replace_type env typ,t2,eff),l2)
+                   | Typ_aux (Typ_fn (ts,t2,eff),l2) ->
+                      Typ_aux (Typ_fn (mapat (replace_type env) to_change ts,t2,eff),l2)
                    | _ -> replace_type env typ
                  in TypSchm_aux (TypSchm_ts (tq,typ),l)
             in
@@ -4168,9 +4162,10 @@ let replace_nexp_in_typ env typ orig new_nexp =
     | Typ_var _
         -> false, typ
     | Typ_fn (arg,res,eff) ->
-       let f1, arg = aux arg in
+       let arg' = List.map aux arg in
+       let f1 = List.exists fst arg' in
        let f2, res = aux res in
-       f1 || f2, Typ_aux (Typ_fn (arg, res, eff),l)
+       f1 || f2, Typ_aux (Typ_fn (List.map snd arg', res, eff),l)
     | Typ_bidir (t1, t2) ->
        let f1, t1 = aux t1 in
        let f2, t2 = aux t2 in
@@ -4223,9 +4218,10 @@ let rewrite_toplevel_nexps (Defs defs) =
   let rec rewrite_typ_in_spec env nexp_map (Typ_aux (t,ann) as typ_full) =
     match t with
     | Typ_fn (args,res,eff) ->
-       let nexp_map, args = rewrite_typ_in_spec env nexp_map args in
+       let args' = List.map (rewrite_typ_in_spec env nexp_map) args in
+       let nexp_map = List.concat (List.map fst args') in
        let nexp_map, res = rewrite_typ_in_spec env nexp_map res in
-       nexp_map, Typ_aux (Typ_fn (args,res,eff),ann)
+       nexp_map, Typ_aux (Typ_fn (List.map snd args',res,eff),ann)
     | Typ_tup typs ->
        let nexp_map, typs =
          List.fold_right (fun typ (nexp_map,t) ->
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml
index cdc6a730..4828398f 100644
--- a/src/ocaml_backend.ml
+++ b/src/ocaml_backend.ml
@@ -142,7 +142,7 @@ let rec ocaml_typ ctx (Typ_aux (typ_aux, l)) =
   | Typ_app (id, []) -> ocaml_typ_id ctx id
   | Typ_app (id, typs) -> parens (separate_map (string ", ") (ocaml_typ_arg ctx) typs) ^^ space ^^ ocaml_typ_id ctx id
   | Typ_tup typs -> parens (separate_map (string " * ") (ocaml_typ ctx) typs)
-  | Typ_fn (typ1, typ2, _) -> separate space [ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2]
+  | Typ_fn (typs, typ, _) -> separate space [ocaml_typ ctx (Typ_aux (Typ_tup typs, l)); string "->"; ocaml_typ ctx typ]
   | Typ_bidir (t1, t2) -> raise (Reporting_basic.err_general l "Ocaml doesn't support bidir types")
   | Typ_var kid -> zencode_kid kid
   | Typ_exist _ -> assert false
@@ -458,15 +458,15 @@ let ocaml_funcls ctx =
      if Bindings.mem id ctx.externs
      then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline
      else
-       let typ1, typ2 =
+       let arg_typs, ret_typ =
          match Bindings.find id ctx.val_specs with
-         | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2)
+         | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
          | _ -> failwith "Found val spec which was not a function!"
        in
        (* Any remaining type variables after simple_typ rewrite should
           indicate Type-polymorphism. If we have it, we need to generate
           explicit type signatures with universal quantification. *)
-       let kids = KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2) in
+       let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
        let pat_sym = gensym () in
        let pat, exp =
          match pexp with
@@ -476,7 +476,7 @@ let ocaml_funcls ctx =
        let annot_pat =
          let pat =
            if KidSet.is_empty kids then
-             parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1)
+             parens (ocaml_pat ctx pat ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs)))
            else
              ocaml_pat ctx pat
          in
@@ -485,18 +485,18 @@ let ocaml_funcls ctx =
          else pat
        in
        let call_header = function_header () in
-       let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
+       let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
        let call =
          if KidSet.is_empty kids then
            separate space [call_header; zencode ctx id;
-                           annot_pat; colon; ocaml_typ ctx typ2; equals;
+                           annot_pat; colon; ocaml_typ ctx ret_typ; equals;
                            sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
            ^//^ ocaml_exp ctx exp
            ^^ rparen
          else
            separate space [call_header; zencode ctx id; colon;
                            separate space (List.map zencode_kid (KidSet.elements kids)) ^^ dot;
-                           ocaml_typ ctx typ1; string "->"; ocaml_typ ctx typ2; equals;
+                           ocaml_typ ctx (mk_typ (Typ_tup arg_typs)); string "->"; ocaml_typ ctx ret_typ; equals;
                            string "fun"; annot_pat; string "->";
                            sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
            ^//^ ocaml_exp ctx exp
@@ -508,18 +508,18 @@ let ocaml_funcls ctx =
      if Bindings.mem id ctx.externs
      then string ("(* Omitting externed function " ^ string_of_id id ^ " *)") ^^ hardline
      else
-       let typ1, typ2 =
+       let arg_typs, ret_typ =
          match Bindings.find id ctx.val_specs with
-         | Typ_aux (Typ_fn (typ1, typ2, _), _) -> (typ1, typ2)
+         | Typ_aux (Typ_fn (typs, typ, _), _) -> (typs, typ)
          | _ -> failwith "Found val spec which was not a function!"
        in
-       let kids = KidSet.union (tyvars_of_typ typ1) (tyvars_of_typ typ2) in
+       let kids = List.fold_left KidSet.union (tyvars_of_typ ret_typ) (List.map tyvars_of_typ arg_typs) in
        if not (KidSet.is_empty kids) then failwith "Cannot handle polymorphic multi-clause function in OCaml backend" else ();
        let pat_sym = gensym () in
        let call_header = function_header () in
-       let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info typ1 typ2 in
+       let arg_sym, string_of_arg, ret_sym, string_of_ret = trace_info (mk_typ (Typ_tup arg_typs)) ret_typ in
        let call =
-         separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx typ1); equals;
+         separate space [call_header; zencode ctx id; parens (pat_sym ^^ space ^^ colon ^^ space ^^ ocaml_typ ctx (mk_typ (Typ_tup arg_typs))); equals;
                          sail_call id arg_sym pat_sym ret_sym; string "(fun r ->"]
          ^//^ (separate space [string "match"; pat_sym; string "with"] ^^ hardline ^^ ocaml_funcl_matches ctx funcls)
          ^^ rparen
@@ -812,8 +812,7 @@ let ocaml_pp_generators ctx defs orig_types required =
       in
       let make_variant (Tu_aux (Tu_ty_id (typ,id),_)) =
         let arg_typs = match typ with
-          | Typ_aux (Typ_fn (Typ_aux (Typ_tup typs,_),_,_),_) -> typs
-          | Typ_aux (Typ_fn (typ,_,_),_) -> [typ]
+          | Typ_aux (Typ_fn (typs,_,_),_) -> typs
           | Typ_aux (Typ_tup typs,_) -> typs
           | _ -> [typ]
         in
diff --git a/src/pretty_print_common.ml b/src/pretty_print_common.ml
index 2c6c1381..1fb35158 100644
--- a/src/pretty_print_common.ml
+++ b/src/pretty_print_common.ml
@@ -128,8 +128,8 @@ let doc_typ, doc_atomic_typ, doc_nexp, doc_nexp_constraint =
   (* following the structure of parser for precedence *)
   let rec typ ty = fn_typ ty
   and fn_typ ((Typ_aux (t, _)) as ty) = match t with
-  | Typ_fn(arg,ret,efct) ->
-     separate space [tup_typ arg; arrow; fn_typ ret; string "effect"; doc_effects efct]
+  | Typ_fn(args,ret,efct) ->
+     separate space [parens (separate_map (comma ^^ space) tup_typ args); arrow; fn_typ ret; string "effect"; doc_effects efct]
   | Typ_bidir (t1, t2) ->
      separate space [tup_typ t1; bidir; tup_typ t2]
   | _ -> tup_typ ty
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml
index b4fc4a72..806234d6 100644
--- a/src/pretty_print_coq.ml
+++ b/src/pretty_print_coq.ml
@@ -264,7 +264,7 @@ let rec coq_nvars_of_typ (Typ_aux (t,l)) =
   match t with
   | Typ_id _ -> KidSet.empty
   | Typ_var kid -> tyvars_of_nexp (orig_nexp (nvar kid))
-  | Typ_fn (t1,t2,_) -> KidSet.union (trec t1) (trec t2)
+  | Typ_fn (t1,t2,_) -> List.fold_left KidSet.union (trec t2) (List.map trec t1)
   | Typ_tup ts ->
      List.fold_left (fun s t -> KidSet.union s (trec t))
        KidSet.empty ts
@@ -395,15 +395,12 @@ let doc_typ, doc_atomic_typ =
   let rec typ ty = fn_typ true ty
     and typ' ty = fn_typ false ty
     and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_fn(arg,ret,efct) ->
+      | Typ_fn(args,ret,efct) ->
          let ret_typ =
            if effectful efct
            then separate space [string "M"; fn_typ true ret]
            else separate space [fn_typ false ret] in
-         let arg_typs = match arg with
-           | Typ_aux (Typ_tup typs, _) ->
-              List.map (app_typ false) typs
-           | _ -> [tup_typ false arg] in
+         let arg_typs = List.map (app_typ false) args in
          let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in
          (* once we have proper excetions we need to know what the exceptions type is *)
          if atyp_needed then parens tpp else tpp
@@ -641,7 +638,7 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
   | Typ_id _
   | Typ_var _
     -> NexpSet.empty
-  | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2)
+  | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (typeclass_nexps t2) (List.map typeclass_nexps t1)
   | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
   | Typ_app (Id_aux (Id "vector",_),
              [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
@@ -689,18 +686,12 @@ let rec doc_pat ctxt apat_needed exists_as_pairs (P_aux (p,(l,annot)) as pat, ty
         (* Following the type checker to get the subpattern types, TODO perhaps ought
            to persuade the type checker to output these somehow. *)
        let (typq, ctor_typ) = Env.get_val_spec id env in
-       let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
-         | Typ_tup [Typ_aux (Typ_tup typs,_)] -> typs
-         | Typ_tup typs -> typs
-         | _ -> [typ]
-       in
        let arg_typs =
          match Env.expand_synonyms env ctor_typ with
-         | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
+         | Typ_aux (Typ_fn (arg_typs, ret_typ, _), _) ->
             (* The FIXME comes from the typechecker code, not sure what it's about... *)
             let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
-            let arg_typ' = subst_unifiers unifiers arg_typ in
-            untuple arg_typ'
+            List.map (subst_unifiers unifiers) arg_typs
          | _ -> assert false
        in
        let ppp = doc_unop (doc_id_ctor id)
@@ -1144,10 +1135,7 @@ let doc_exp, doc_let =
             else doc_id f, false, false in
           let (tqs,fn_ty) = Env.get_val_spec_orig f env in
           let arg_typs, ret_typ, eff = match fn_ty with
-            | Typ_aux (Typ_fn (arg_typ,ret_typ,eff),_) ->
-               (match arg_typ with
-               | Typ_aux (Typ_tup typs,_) -> typs, ret_typ, eff
-               | _ -> [arg_typ], ret_typ, eff)
+            | Typ_aux (Typ_fn (arg_typs,ret_typ,eff),_) -> arg_typs, ret_typ, eff
             | _ -> raise (Reporting_basic.err_unreachable l __POS__ "Function not a function type")
           in
           let inst =
@@ -1923,8 +1911,8 @@ let merge_var_patterns map pats =
 let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let env = env_of_annot annot in
   let (tq,typ) = Env.get_val_spec_orig id env in
-  let (arg_typ, ret_typ, eff) = match typ with
-    | Typ_aux (Typ_fn (arg_typ, ret_typ, eff),_) -> arg_typ, ret_typ, eff
+  let (arg_typs, ret_typ, eff) = match typ with
+    | Typ_aux (Typ_fn (arg_typs, ret_typ, eff),_) -> arg_typs, ret_typ, eff
     | _ -> failwith ("Function " ^ string_of_id id ^ " does not have function type")
   in
   let build_ex, ret_typ = replace_atom_return_type ret_typ in
@@ -1935,7 +1923,7 @@ let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) =
   let ids_to_avoid = all_ids pexp in
   let bound_kids = tyvars_of_typquant tq in
   let pat,guard,exp,(l,_) = destruct_pexp pexp in
-  let pats, bind = untuple_args_pat arg_typ pat in
+  let pats, bind = untuple_args_pat (mk_typ (Typ_tup arg_typs)) pat in (* FIXME is this needed any more? *)
   let pats, binds = List.split (Util.list_mapi demote_as_pattern pats) in
   let eliminated_kids, kid_to_arg_rename = merge_kids_atoms pats in
   let kid_to_arg_rename, pats = merge_var_patterns kid_to_arg_rename pats in
@@ -2135,7 +2123,7 @@ let doc_regtype_fields (tname, (n1, n2, fields)) =
 let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
   let typ_env = add_typquant l tqs typ_env in
   match typ with
-  | Typ_aux (Typ_fn (args_ty, ret_ty, eff),l') ->
+  | Typ_aux (Typ_fn (typs, ret_ty, eff),l') ->
      let check_typ (args,used) typ =
        match Type_check.destruct_atom_nexp typ_env typ with
        | Some (Nexp_aux (Nexp_var kid,_)) ->
@@ -2144,7 +2132,6 @@ let doc_axiom_typschm typ_env (TypSchm_aux (TypSchm_ts (tqs,typ),l) as ts) =
        | Some _ -> args, used
        | _ -> args, KidSet.union used (tyvars_of_typ typ)
      in
-     let typs = match args_ty with Typ_aux (Typ_tup typs,_) -> typs | _ -> [args_ty] in
      let args, used = List.fold_left check_typ (KidSet.empty, KidSet.empty) typs in
      let used = if is_number ret_ty then used else KidSet.union used (tyvars_of_typ ret_ty) in
      let tqs = match tqs with
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index d7f403a4..232c3aee 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -219,7 +219,7 @@ let rec lem_nexps_of_typ (Typ_aux (t,l)) =
   match t with
   | Typ_id _ -> NexpSet.empty
   | Typ_var kid -> NexpSet.singleton (orig_nexp (nvar kid))
-  | Typ_fn (t1,t2,_) -> NexpSet.union (trec t1) (trec t2)
+  | Typ_fn (t1,t2,_) -> List.fold_left NexpSet.union (trec t2) (List.map trec t1)
   | Typ_tup ts ->
      List.fold_left (fun s t -> NexpSet.union s (trec t))
        NexpSet.empty ts
@@ -258,15 +258,12 @@ let doc_typ_lem, doc_atomic_typ_lem =
   let rec typ ty = fn_typ true ty
     and typ' ty = fn_typ false ty
     and fn_typ atyp_needed ((Typ_aux (t, _)) as ty) = match t with
-      | Typ_fn(arg,ret,efct) ->
+      | Typ_fn(args,ret,efct) ->
          let ret_typ =
            if effectful efct
            then separate space [string "M"; fn_typ true ret]
            else separate space [fn_typ false ret] in
-         let arg_typs = match arg with
-           | Typ_aux (Typ_tup typs, _) ->
-              List.map (app_typ false) typs
-           | _ -> [tup_typ false arg] in
+         let arg_typs = List.map (app_typ false) args in
          let tpp = separate (space ^^ arrow ^^ space) (arg_typs @ [ret_typ]) in
          (* once we have proper excetions we need to know what the exceptions type is *)
          if atyp_needed then parens tpp else tpp
@@ -443,7 +440,7 @@ let rec typeclass_nexps (Typ_aux(t,l)) =
     | Typ_id _
     | Typ_var _
       -> NexpSet.empty
-    | Typ_fn (t1,t2,_) -> NexpSet.union (typeclass_nexps t1) (typeclass_nexps t2)
+    | Typ_fn (ts,t,_) -> List.fold_left NexpSet.union (typeclass_nexps t) (List.map typeclass_nexps ts)
     | Typ_tup ts -> List.fold_left NexpSet.union NexpSet.empty (List.map typeclass_nexps ts)
     | Typ_app (Id_aux (Id "vector",_),
                [Typ_arg_aux (Typ_arg_nexp size_nexp,_);
@@ -531,7 +528,7 @@ let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with
   | Typ_tup ts -> List.exists typ_needs_printed ts
   | Typ_app (Id_aux (Id "itself",_),_) -> true
   | Typ_app (_, targs) -> is_bitvector_typ typ || List.exists typ_needs_printed_arg targs
-  | Typ_fn (t1,t2,_) -> typ_needs_printed t1 || typ_needs_printed t2
+  | Typ_fn (ts,t,_) -> List.exists typ_needs_printed ts || typ_needs_printed t
   | Typ_exist (kids,_,t) ->
      let visible_kids = KidSet.inter (KidSet.of_list kids) (lem_tyvars_of_typ t) in
      typ_needs_printed t && KidSet.is_empty visible_kids
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, _)) =
diff --git a/src/rewrites.ml b/src/rewrites.ml
index 7a085213..cdb15717 100644
--- a/src/rewrites.ml
+++ b/src/rewrites.ml
@@ -255,8 +255,8 @@ let rec rewrite_nexp_ids env (Nexp_aux (nexp, l) as nexp_aux) = match nexp with
 
 let rewrite_defs_nexp_ids, rewrite_typ_nexp_ids =
   let rec rewrite_typ env (Typ_aux (typ, l) as typ_aux) = match typ with
-    | Typ_fn (arg_t, ret_t, eff) ->
-       Typ_aux (Typ_fn (rewrite_typ env arg_t, rewrite_typ env ret_t, eff), l)
+    | Typ_fn (arg_ts, ret_t, eff) ->
+       Typ_aux (Typ_fn (List.map (rewrite_typ env) arg_ts, rewrite_typ env ret_t, eff), l)
     | Typ_tup ts ->
        Typ_aux (Typ_tup (List.map (rewrite_typ env) ts), l)
     | Typ_exist (kids, c, typ) ->
@@ -658,14 +658,8 @@ let rewrite_sizeof (Defs defs) =
         let kid_typs = List.map (fun kid -> atom_typ (nvar kid))
                                 (KidSet.elements (Bindings.find id params_map)) in
         let typ' = match typ with
-          | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) ->
-             let vtyp_arg' = begin
-                 match vtyp_arg with
-                 | Typ_aux (Typ_tup typs, vl) ->
-                    Typ_aux (Typ_tup (kid_typs @ typs), vl)
-                 | _ -> Typ_aux (Typ_tup (kid_typs @ [vtyp_arg]), vl)
-               end in
-             Typ_aux (Typ_fn (vtyp_arg', vtyp_ret, declared_eff), vl)
+          | Typ_aux (Typ_fn (vtyp_args, vtyp_ret, declared_eff), vl) ->
+             Typ_aux (Typ_fn (kid_typs @ vtyp_args, vtyp_ret, declared_eff), vl)
           | _ ->
             raise (Reporting_basic.err_typ l "val spec with non-function type") in
         TypSchm_aux (TypSchm_ts (tq, typ'), l)
@@ -2139,7 +2133,11 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
              | P_aux (P_app (constr_id, args), pannot) ->
                 let argstup_typ = tuple_typ (List.map pat_typ_of args) in
                 let pannot' = swaptyp argstup_typ pannot in
-                let pat' = P_aux (P_tup args, pannot') in
+                let pat' =
+                  match args with
+                  | [arg] -> arg
+                  | _ -> P_aux (P_tup args, pannot')
+                in
                 let pexp' = construct_pexp (pat', guard, exp, annot) in
                 let aux_fun_id = prepend_id (fun_name ^ "_") constr_id in
                 let aux_funcl = FCL_aux (FCL_Funcl (aux_fun_id, pexp'), pannot') in
@@ -2185,7 +2183,15 @@ let rewrite_split_fun_constr_pats fun_name (Defs defs) =
            union_effects eff (effect_of exp))
         no_effect funcls
       in
-      let fun_typ = function_typ args_typ ret_typ eff in
+      let fun_typ =
+        (* Because we got the argument type from a pattern we need to
+           do this. *)
+        match args_typ with
+        | Typ_aux (Typ_tup (args_typs), _) ->
+           function_typ args_typs ret_typ eff
+        | _ ->
+           function_typ [args_typ] ret_typ eff
+      in
       let quant_new_tyvars qis =
         let quant_tyvars = List.fold_left KidSet.union KidSet.empty (List.map tyvars_of_quant_item qis) in
         let typ_tyvars = tyvars_of_typ fun_typ in
@@ -2283,7 +2289,7 @@ let rewrite_fix_val_specs (Defs defs) =
             type synonyms nested in existentials might cause problems).
             A more robust solution would be to make the (global) environment
             more easily available to the pretty-printer. *)
-         let args_t' = Env.expand_synonyms (env_of exp) args_t in
+         let args_t' = List.map (Env.expand_synonyms (env_of exp)) args_t in
          let ret_t' = Env.expand_synonyms (env_of exp) ret_t in
          (tq, Typ_aux (Typ_fn (args_t', ret_t', eff'), a)), eff'
       | _ -> assert false (* find_vs must return a function type *)
@@ -2457,7 +2463,7 @@ and simple_typ_aux = function
   | Typ_app (id, [_; _]) when Id.compare id (mk_id "range") = 0 ->
      Typ_id (mk_id "int")
   | Typ_app (id, args) -> Typ_app (id, List.concat (List.map simple_typ_arg args))
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (simple_typ typ1, simple_typ typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map simple_typ arg_typs, simple_typ ret_typ, effs)
   | Typ_tup typs -> Typ_tup (List.map simple_typ typs)
   | Typ_exist (_, _, Typ_aux (typ, l)) -> simple_typ_aux typ
   | typ_aux -> typ_aux
@@ -3145,7 +3151,7 @@ let construct_toplevel_string_append_func env f_id pat =
                                                                        | typs -> tuple_typ typs
                                                             ), unk)]
   in
-  let fun_typ = (mk_typ (Typ_fn (string_typ, option_typ, no_effect))) in
+  let fun_typ = (mk_typ (Typ_fn ([string_typ], option_typ, no_effect))) in
   let new_val_spec = VS_aux (VS_val_spec (mk_typschm (TypQ_aux (TypQ_no_forall, unk)) fun_typ, f_id, (fun _ -> None), false), unkt) in
   let new_val_spec, env = Type_check.check_val_spec env new_val_spec in
   let non_rec = (Rec_aux (Rec_nonrec, Parse_ast.Unknown)) in
@@ -3705,8 +3711,6 @@ let rewrite_defs_pat_lits rewrite_lit =
     let counter = ref 0 in
 
     let rewrite_pat = function
-      (* HACK: ignore strings for now *)
-      | P_lit (L_aux (L_string _, _)) as p_aux, p_annot -> P_aux (p_aux, p_annot)
       (* Matching on unit is always the same as matching on wildcard *)
       | P_lit (L_aux (L_unit, _) as lit), p_annot when rewrite_lit lit ->
          P_aux (P_wild, p_annot)
@@ -4028,7 +4032,7 @@ let remove_reference_types exp =
     | Typ_app (Id_aux (Id "reg",_), [Typ_arg_aux (Typ_arg_typ (Typ_aux (t_aux2, _)), _)]) ->
       rewrite_t_aux t_aux2
     | Typ_app (name,t_args) -> Typ_app (name,List.map rewrite_t_arg t_args)
-    | Typ_fn (t1,t2,eff) -> Typ_fn (rewrite_t t1,rewrite_t t2,eff)
+    | Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map rewrite_t arg_typs, rewrite_t ret_typ, eff)
     | Typ_tup ts -> Typ_tup (List.map rewrite_t ts)
     | _ -> t_aux
   and rewrite_t_arg t_arg = match t_arg with
@@ -4336,10 +4340,10 @@ let rewrite_defs_realise_mappings (Defs defs) =
       | Typ_aux (Typ_bidir (typ1, typ2), l) -> typ1, typ2, l
       | _ -> Type_check.typ_error l "non-bidir type of mapping?"
     in
-    let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), l) in
-    let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), l) in
-    let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), l) in
-    let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), l) in
+    let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), l) in
+    let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), l) in
+    let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), l) in
+    let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), l) in
 
     let forwards_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_typ, forwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
     let backwards_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_typ, backwards_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
@@ -4377,7 +4381,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
     let prefix_wildcard = mk_pexp (Pat_exp (mk_pat P_wild, mk_exp (E_app (mk_id "None", [mk_exp (E_lit (mk_lit L_unit))])))) in
     let string_defs =
       begin if subtype_check env typ1 string_typ && subtype_check env string_typ typ1 then
-              let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               let forwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq forwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
               let forwards_prefix_spec, env = Type_check.check_val_spec env forwards_prefix_spec in
               let forwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl true prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
@@ -4387,7 +4391,7 @@ let rewrite_defs_realise_mappings (Defs defs) =
               forwards_prefix_spec @ forwards_prefix_fun
             else
               if subtype_check env typ2 string_typ && subtype_check env string_typ typ2 then
-                let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+                let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
                 let backwards_prefix_spec = VS_aux (VS_val_spec (mk_typschm typq backwards_prefix_typ, prefix_id, (fun _ -> None), false), (Parse_ast.Unknown,())) in
                 let backwards_prefix_spec, env = Type_check.check_val_spec env backwards_prefix_spec in
                 let backwards_prefix_match = mk_exp (E_case (arg_exp, ((List.map (fun mapcl -> strip_mapcl mapcl |> realise_prefix_mapcl false prefix_id) mapcls) |> List.flatten) @ [prefix_wildcard])) in
@@ -4512,9 +4516,7 @@ let make_cstr_mappings env ids m =
     (fun id ->
       let _,ty = Env.get_val_spec id env in
       let args = match ty with
-        | Typ_aux (Typ_fn (Typ_aux (Typ_tup [Typ_aux (Typ_tup tys,_)],_),_,_),_)
-        | Typ_aux (Typ_fn (Typ_aux (Typ_tup tys,_),_,_),_)
-          -> List.map (fun _ -> RP_any) tys
+        | Typ_aux (Typ_fn (tys,_,_),_) -> List.map (fun _ -> RP_any) tys
         | _ -> [RP_any]
       in RP_app (id,args)) ids in
   let rec aux ids acc l =
@@ -4972,7 +4974,7 @@ let rewrite_defs_c = [
   ("mapping_builtins", rewrite_defs_mapping_patterns);
   ("rewrite_undefined", rewrite_undefined_if_gen false);
   ("rewrite_defs_vector_string_pats_to_bit_list", rewrite_defs_vector_string_pats_to_bit_list);
-  ("pat_lits", rewrite_defs_pat_lits rewrite_no_strings);
+  ("pat_lits", rewrite_defs_pat_lits (fun _ -> true));
   ("vector_concat_assignments", rewrite_vector_concat_assignments);
   ("tuple_assignments", rewrite_tuple_assignments);
   ("simple_assignments", rewrite_simple_assignments);
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 28015945..a718e6d5 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -530,6 +530,13 @@ let string_startswith (str1, str2) = String.length str1 >= String.length str2 &&
 
 let string_drop (str, n) = if (Big_int.less_equal (Big_int.of_int (String.length str)) n) then "" else let n = Big_int.to_int n in String.sub str n (String.length str - n)
 
+let string_take (str, n) =
+  let n = Big_int.to_int n in
+  if String.length str <= n then
+    str
+  else
+    String.sub str 0 n
+
 let string_length str = Big_int.of_int (String.length str)
 
 let string_append (s1, s2) = s1 ^ s2
@@ -704,28 +711,6 @@ let speculate_conditional_success () = true
 (* Return nanoseconds since epoch. Truncates to ocaml int but will be OK for next 100 years or so... *)
 let get_time_ns () = Big_int.of_int (int_of_float (1e9 *. Unix.gettimeofday ()))
 
-let rec n_leading_spaces s =
-  match String.length s with
-  | 0 -> 0
-  | 1 -> begin match s with
-         | " " -> 1
-         | _ -> 0
-         end
-  | len -> begin match String.get s 0 with
-           | ' ' -> 1 + (n_leading_spaces (String.sub s 1 (len - 1)))
-           | _ -> 0
-           end
-
-
-let opt_spc_matches_prefix s =
-  ZSome ((), n_leading_spaces s |> Big_int.of_int)
-
-let spc_matches_prefix s =
-  let n = n_leading_spaces s in
-  match n with
-  | 0 -> ZNone ()
-  | n -> ZSome ((), Big_int.of_int n)
-
 (* Python:
 f = """let hex_bits_{0}_matches_prefix s =
   match maybe_int_of_prefix s with
@@ -1124,7 +1109,7 @@ let cycle_count () = ()
 
 (* TODO range, atom, register(?), int, nat, bool, real(!), list, string, itself(?) *)
 let rand_zvector (g : 'generators) (size : int) (order : bool) (elem_gen : 'generators -> 'a) : 'a list =
-  List.init size (fun _ -> elem_gen g)
+  Util.list_init size (fun _ -> elem_gen g)
 
 let rand_zbit (g : 'generators) : bit =
   if Random.bool() then B0 else B1
diff --git a/src/spec_analysis.ml b/src/spec_analysis.ml
index 44440ecf..56c488ff 100644
--- a/src/spec_analysis.ml
+++ b/src/spec_analysis.ml
@@ -88,8 +88,8 @@ let nameset_bigunion = List.fold_left Nameset.union mt
 let rec free_type_names_t consider_var (Typ_aux (t, l)) = match t with
   | Typ_var name -> if consider_var then Nameset.add (string_of_kid name) mt else mt
   | Typ_id name -> Nameset.add (string_of_id name) mt
-  | Typ_fn (t1,t2,_) -> Nameset.union (free_type_names_t consider_var t1)
-                          (free_type_names_t consider_var t2)
+  | Typ_fn (arg_typs,ret_typ,_) ->
+     List.fold_left Nameset.union (free_type_names_t consider_var ret_typ) (List.map (free_type_names_t consider_var) arg_typs)
   | Typ_bidir (t1, t2) -> Nameset.union (free_type_names_t consider_var t1)
                                         (free_type_names_t consider_var t2)
   | Typ_tup ts -> free_type_names_ts consider_var ts
@@ -120,7 +120,8 @@ let rec fv_of_typ consider_var bound used (Typ_aux (t,l)) : Nameset.t =
     then conditional_add_typ bound used (Ast.Id_aux (Ast.Id v,l))
     else used
   | Typ_id id -> conditional_add_typ bound used id
-  | Typ_fn(arg,ret,_) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used arg) ret
+  | Typ_fn(arg,ret,_) ->
+     fv_of_typ consider_var bound (List.fold_left Nameset.union Nameset.empty (List.map (fv_of_typ consider_var bound used) arg)) ret
   | Typ_bidir(t1, t2) -> fv_of_typ consider_var bound (fv_of_typ consider_var bound used t1) t2 (* TODO FIXME? *)
   | Typ_tup ts -> List.fold_right (fun t n -> fv_of_typ consider_var bound n t) ts used
   | Typ_app(id,targs) ->
diff --git a/src/specialize.ml b/src/specialize.ml
index 81c8b0b0..4d7a997f 100644
--- a/src/specialize.ml
+++ b/src/specialize.ml
@@ -65,7 +65,8 @@ let rec nexp_simp_typ (Typ_aux (typ_aux, l)) =
     | Typ_tup typs -> Typ_tup (List.map nexp_simp_typ typs)
     | Typ_app (f, args) -> Typ_app (f, List.map nexp_simp_typ_arg args)
     | Typ_exist (kids, nc, typ) -> Typ_exist (kids, nc, nexp_simp_typ typ)
-    | Typ_fn (typ1, typ2, effect) -> Typ_fn (nexp_simp_typ typ1, nexp_simp_typ typ2, effect)
+    | Typ_fn (arg_typs, ret_typ, effect) ->
+       Typ_fn (List.map nexp_simp_typ arg_typs, nexp_simp_typ ret_typ, effect)
     | Typ_bidir (t1, t2) -> Typ_bidir (nexp_simp_typ t1, nexp_simp_typ t2)
     | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
   in
@@ -137,8 +138,8 @@ let string_of_instantiation instantiation =
     | Typ_var kid -> kid_name kid
     | Typ_tup typs -> "(" ^ Util.string_of_list ", " string_of_typ typs ^ ")"
     | Typ_app (id, args) -> string_of_id id ^ "(" ^ Util.string_of_list ", " string_of_typ_arg args ^ ")"
-    | Typ_fn (typ_arg, typ_ret, eff) ->
-       string_of_typ typ_arg ^ " -> " ^ string_of_typ typ_ret ^ " effect " ^ string_of_effect eff
+    | Typ_fn (arg_typs, ret_typ, eff) ->
+       "(" ^ Util.string_of_list ", " string_of_typ arg_typs ^ ") -> " ^ string_of_typ ret_typ ^ " effect " ^ string_of_effect eff
     | Typ_bidir (t1, t2) ->
        string_of_typ t1 ^ " <-> " ^ string_of_typ t2
     | Typ_exist (kids, nc, typ) ->
@@ -257,7 +258,8 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
-  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
   | Typ_bidir (t1, t2) -> KidSet.union (typ_frees ~exs:exs t1) (typ_frees ~exs:exs t2)
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
@@ -273,7 +275,8 @@ let rec typ_int_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_int_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_int_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_int_frees ~exs:(KidSet.of_list kids) typ
-  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_int_frees ~exs:exs typ1) (typ_int_frees ~exs:exs typ2)
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.fold_left KidSet.union (typ_int_frees ~exs:exs ret_typ) (List.map (typ_int_frees ~exs:exs) arg_typs)
   | Typ_bidir (t1, t2) -> KidSet.union (typ_int_frees ~exs:exs t1) (typ_int_frees ~exs:exs t2)
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
 and typ_arg_int_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
diff --git a/src/type_check.ml b/src/type_check.ml
index 565d1eed..e1232046 100644
--- a/src/type_check.ml
+++ b/src/type_check.ml
@@ -183,7 +183,7 @@ and strip_typ_aux : typ_aux -> typ_aux = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id id -> Typ_id (strip_id id)
   | Typ_var kid -> Typ_var (strip_kid kid)
-  | Typ_fn (typ1, typ2, effect) -> Typ_fn (strip_typ typ1, strip_typ typ2, strip_effect effect)
+  | Typ_fn (arg_typs, ret_typ, effect) -> Typ_fn (List.map strip_typ arg_typs, strip_typ ret_typ, strip_effect effect)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (strip_typ typ1, strip_typ typ2)
   | Typ_tup typs -> Typ_tup (List.map strip_typ typs)
   | Typ_exist (kids, constr, typ) -> Typ_exist ((List.map strip_kid kids), strip_n_constraint constr, strip_typ typ)
@@ -253,7 +253,7 @@ and typ_subst_nexp_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_nexp sv subst) arg_typs, typ_subst_nexp sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_nexp sv subst typ1, typ_subst_nexp sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_nexp sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_nexp sv subst) args)
@@ -270,7 +270,7 @@ and typ_subst_typ_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> if Kid.compare kid sv = 0 then subst else Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_typ sv subst) arg_typs, typ_subst_typ sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_typ sv subst typ1, typ_subst_typ sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_typ sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_typ sv subst) args)
@@ -293,7 +293,7 @@ and typ_subst_order_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_order sv subst) arg_typs, typ_subst_order sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_order sv subst typ1, typ_subst_order sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_order sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_order sv subst) args)
@@ -309,7 +309,7 @@ and typ_subst_kid_aux sv subst = function
   | Typ_internal_unknown -> Typ_internal_unknown
   | Typ_id v -> Typ_id v
   | Typ_var kid -> if Kid.compare kid sv = 0 then Typ_var subst else Typ_var kid
-  | Typ_fn (typ1, typ2, effs) -> Typ_fn (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2, effs)
+  | Typ_fn (arg_typs, ret_typ, effs) -> Typ_fn (List.map (typ_subst_kid sv subst) arg_typs, typ_subst_kid sv subst ret_typ, effs)
   | Typ_bidir (typ1, typ2) -> Typ_bidir (typ_subst_kid sv subst typ1, typ_subst_kid sv subst typ2)
   | Typ_tup typs -> Typ_tup (List.map (typ_subst_kid sv subst) typs)
   | Typ_app (f, args) -> Typ_app (f, List.map (typ_subst_arg_kid sv subst) args)
@@ -602,7 +602,7 @@ end = struct
     match typ with
     | Typ_internal_unknown -> Typ_aux (Typ_internal_unknown, l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (expand_synonyms env) typs), l)
-    | Typ_fn (typ1, typ2, effs) -> Typ_aux (Typ_fn (expand_synonyms env typ1, expand_synonyms env typ2, effs), l)
+    | Typ_fn (arg_typs, ret_typ, effs) -> Typ_aux (Typ_fn (List.map (expand_synonyms env) arg_typs, expand_synonyms env ret_typ, effs), l)
     | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (expand_synonyms env typ1, expand_synonyms env typ2), l)
     | Typ_app (id, args) ->
        begin
@@ -658,7 +658,7 @@ end = struct
     match typ_aux with
     | Typ_internal_unknown
     | Typ_id _ | Typ_var _ -> typ
-    | Typ_fn (arg_typ, ret_typ, effect) -> Typ_aux (Typ_fn (map_nexps f arg_typ, map_nexps f ret_typ, effect), l)
+    | Typ_fn (arg_typs, ret_typ, effect) -> Typ_aux (Typ_fn (List.map (map_nexps f) arg_typs, map_nexps f ret_typ, effect), l)
     | Typ_bidir (typ1, typ2) -> Typ_aux (Typ_bidir (map_nexps f typ1, map_nexps f typ2), l)
     | Typ_tup typs -> Typ_aux (Typ_tup (List.map (map_nexps f) typs), l)
     | Typ_exist (kids, nc, typ) -> Typ_aux (Typ_exist (kids, nc, map_nexps f typ), l)
@@ -699,8 +699,8 @@ end = struct
 
   let rec canonicalize env typ =
     match typ with
-    | Typ_aux (Typ_fn (arg_typ, ret_typ, effects), l) when is_canonical env arg_typ ->
-       Typ_aux (Typ_fn (arg_typ, canonicalize env ret_typ, effects), l)
+    | Typ_aux (Typ_fn (arg_typs, ret_typ, effects), l) when List.for_all (is_canonical env) arg_typs ->
+       Typ_aux (Typ_fn (arg_typs, canonicalize env ret_typ, effects), l)
     | Typ_aux (Typ_fn _, l) -> typ_error l ("Function type " ^ string_of_typ typ ^ " is not canonical")
     | _ ->
        let existentials, constrs, (Typ_aux (typ_aux, l) as typ) = canonical env typ in
@@ -735,7 +735,7 @@ end = struct
       | exception Not_found ->
          typ_error l ("Unbound kind identifier " ^ string_of_kid kid ^ " in type " ^ string_of_typ typ)
     end
-    | Typ_fn (typ_arg, typ_ret, effs) -> wf_typ ~exs:exs env typ_arg; wf_typ ~exs:exs env typ_ret
+    | Typ_fn (arg_typs, ret_typ, effs) -> List.iter (wf_typ ~exs:exs env) arg_typs; wf_typ ~exs:exs env ret_typ
     | Typ_bidir (typ1, typ2) when strip_typ typ1 = strip_typ typ2 ->
        typ_error l "Bidirectional types cannot be the same on both sides"
     | Typ_bidir (typ1, typ2) -> wf_typ ~exs:exs env typ1; wf_typ ~exs:exs env typ2
@@ -859,10 +859,10 @@ end = struct
       let forwards_matches_id = mk_id (string_of_id id ^ "_forwards_matches") in
       let backwards_id = mk_id (string_of_id id ^ "_backwards") in
       let backwards_matches_id = mk_id (string_of_id id ^ "_backwards_matches") in
-      let forwards_typ = Typ_aux (Typ_fn (typ1, typ2, no_effect), Parse_ast.Unknown) in
-      let forwards_matches_typ = Typ_aux (Typ_fn (typ1, bool_typ, no_effect), Parse_ast.Unknown) in
-      let backwards_typ = Typ_aux (Typ_fn (typ2, typ1, no_effect), Parse_ast.Unknown) in
-      let backwards_matches_typ = Typ_aux (Typ_fn (typ2, bool_typ, no_effect), Parse_ast.Unknown) in
+      let forwards_typ = Typ_aux (Typ_fn ([typ1], typ2, no_effect), Parse_ast.Unknown) in
+      let forwards_matches_typ = Typ_aux (Typ_fn ([typ1], bool_typ, no_effect), Parse_ast.Unknown) in
+      let backwards_typ = Typ_aux (Typ_fn ([typ2], typ1, no_effect), Parse_ast.Unknown) in
+      let backwards_matches_typ = Typ_aux (Typ_fn ([typ2], bool_typ, no_effect), Parse_ast.Unknown) in
       let env =
         { env with mappings = Bindings.add id (typq, typ1, typ2) env.mappings }
         |> add_val_spec forwards_id (typq, forwards_typ)
@@ -872,10 +872,10 @@ end = struct
       in
       let prefix_id = mk_id (string_of_id id ^ "_matches_prefix") in
       begin if strip_typ typ1 = string_typ then
-              let forwards_prefix_typ = Typ_aux (Typ_fn (typ1, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let forwards_prefix_typ = Typ_aux (Typ_fn ([typ1], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ2; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               add_val_spec prefix_id (typq, forwards_prefix_typ) env
             else if strip_typ typ2 = string_typ then
-              let backwards_prefix_typ = Typ_aux (Typ_fn (typ2, app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
+              let backwards_prefix_typ = Typ_aux (Typ_fn ([typ2], app_typ (mk_id "option") [Typ_arg_aux (Typ_arg_typ (tuple_typ [typ1; nat_typ]), Parse_ast.Unknown)], no_effect), Parse_ast.Unknown) in
               add_val_spec prefix_id (typq, backwards_prefix_typ) env
             else
               env
@@ -946,7 +946,7 @@ end = struct
           | args -> mk_typ (Typ_app (id, args))
         in
         let fold_accessors accs (typ, fid) =
-          let acc_typ = mk_typ (Typ_fn (rectyp, typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          let acc_typ = mk_typ (Typ_fn ([rectyp], typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
           typ_print (lazy (indent 1 ^ "Adding accessor " ^ string_of_id id ^ "." ^ string_of_id fid ^ " :: " ^ string_of_bind (typq, acc_typ)));
           Bindings.add (field_name id fid) (typq, acc_typ) accs
         in
@@ -962,7 +962,8 @@ end = struct
 
   let get_accessor rec_id id env =
     match get_accessor_fn rec_id id env with
-    | (typq, Typ_aux (Typ_fn (rec_typ, field_typ, effect), _)) ->
+    (* All accessors should have a single argument (the record itself) *)
+    | (typq, Typ_aux (Typ_fn ([rec_typ], field_typ, effect), _)) ->
        (typq, rec_typ, field_typ, effect)
     | _ -> typ_error (id_loc id) ("Accessor with non-function type found for " ^ string_of_id (field_name rec_id id))
 
@@ -1144,8 +1145,8 @@ end = struct
     let rec aux (Typ_aux (t,a)) =
       let rewrap t = Typ_aux (t,a) in
       match t with
-      | Typ_fn (t1, t2, eff) ->
-        rewrap (Typ_fn (aux t1, aux t2, eff))
+      | Typ_fn (arg_typs, ret_typ, eff) ->
+        rewrap (Typ_fn (List.map aux arg_typs, aux ret_typ, eff))
       | Typ_tup ts ->
         rewrap (Typ_tup (List.map aux ts))
       | Typ_app (r, [Typ_arg_aux (Typ_arg_typ rtyp,_)]) when string_of_id r = "register" ->
@@ -1288,7 +1289,7 @@ let rec is_typ_monomorphic (Typ_aux (typ, l)) =
   | Typ_id _ -> true
   | Typ_tup typs -> List.for_all is_typ_monomorphic typs
   | Typ_app (id, args) -> List.for_all is_typ_arg_monomorphic args
-  | Typ_fn (typ1, typ2, _) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
+  | Typ_fn (arg_typs, ret_typ, _) -> List.for_all is_typ_monomorphic arg_typs && is_typ_monomorphic ret_typ
   | Typ_bidir (typ1, typ2) -> is_typ_monomorphic typ1 && is_typ_monomorphic typ2
   | Typ_exist _ | Typ_var _ -> false
   | Typ_internal_unknown -> unreachable l __POS__ "escaped Typ_internal_unknown"
@@ -1450,8 +1451,8 @@ let rec typ_nexps (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.concat (List.map typ_nexps typs)
   | Typ_app (f, args) -> List.concat (List.map typ_arg_nexps args)
   | Typ_exist (kids, nc, typ) -> typ_nexps typ
-  | Typ_fn (typ1, typ2, _) ->
-     typ_nexps typ1 @ typ_nexps typ2
+  | Typ_fn (arg_typs, ret_typ, _) ->
+     List.concat (List.map typ_nexps arg_typs) @ typ_nexps ret_typ
   | Typ_bidir (typ1, typ2) ->
      typ_nexps typ1 @ typ_nexps typ2
 and typ_arg_nexps (Typ_arg_aux (typ_arg_aux, l)) =
@@ -1469,7 +1470,7 @@ let rec typ_frees ?exs:(exs=KidSet.empty) (Typ_aux (typ_aux, l)) =
   | Typ_tup typs -> List.fold_left KidSet.union KidSet.empty (List.map (typ_frees ~exs:exs) typs)
   | Typ_app (f, args) -> List.fold_left KidSet.union KidSet.empty (List.map (typ_arg_frees ~exs:exs) args)
   | Typ_exist (kids, nc, typ) -> typ_frees ~exs:(KidSet.of_list kids) typ
-  | Typ_fn (typ1, typ2, _) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
+  | Typ_fn (arg_typs, ret_typ, _) -> List.fold_left KidSet.union (typ_frees ~exs:exs ret_typ) (List.map (typ_frees ~exs:exs) arg_typs)
   | Typ_bidir (typ1, typ2) -> KidSet.union (typ_frees ~exs:exs typ1) (typ_frees ~exs:exs typ2)
 and typ_arg_frees ?exs:(exs=KidSet.empty) (Typ_arg_aux (typ_arg_aux, l)) =
   match typ_arg_aux with
@@ -1517,8 +1518,9 @@ let typ_identical env typ1 typ2 =
     match typ1, typ2 with
     | Typ_id v1, Typ_id v2 -> Id.compare v1 v2 = 0
     | Typ_var kid1, Typ_var kid2 -> Kid.compare kid1 kid2 = 0
-    | Typ_fn (arg_typ1, ret_typ1, eff1), Typ_fn (arg_typ2, ret_typ2, eff2) ->
-       typ_identical' arg_typ1 arg_typ2
+    | Typ_fn (arg_typs1, ret_typ1, eff1), Typ_fn (arg_typs2, ret_typ2, eff2)
+         when List.length arg_typs1 = List.length arg_typs2 ->
+       List.for_all2 typ_identical' arg_typs1 arg_typs2
        && typ_identical' ret_typ1 ret_typ2
        && strip_effect eff1 = strip_effect eff2
     | Typ_bidir (typ1, typ2), Typ_bidir (typ3, typ4) ->
@@ -1850,7 +1852,7 @@ let rec alpha_equivalent env typ1 typ2 =
       match aux with
       | Typ_internal_unknown -> Typ_internal_unknown
       | Typ_id _ | Typ_var _ -> aux
-      | Typ_fn (typ1, typ2, eff) -> Typ_fn (relabel typ1, relabel typ2, eff)
+      | Typ_fn (arg_typs, ret_typ, eff) -> Typ_fn (List.map relabel arg_typs, relabel ret_typ, eff)
       | Typ_bidir (typ1, typ2) -> Typ_bidir (relabel typ1, relabel typ2)
       | Typ_tup typs -> Typ_tup (List.map relabel typs)
       | Typ_exist (kids, nc, typ) ->
@@ -2236,7 +2238,8 @@ let rec filter_casts env from_typ to_typ casts =
      begin
        let (quant, cast_typ) = Env.get_val_spec cast env in
        match cast_typ with
-       | Typ_aux (Typ_fn (cast_from_typ, cast_to_typ, _), _)
+       (* A cast should be a function A -> B and have only a single argument type. *)
+       | Typ_aux (Typ_fn ([cast_from_typ], cast_to_typ, _), _)
             when match_typ env from_typ cast_from_typ && match_typ env to_typ cast_to_typ ->
           typ_print (lazy ("Considering cast " ^ string_of_typ cast_typ ^ " for " ^ string_of_typ from_typ ^ " to " ^ string_of_typ to_typ));
           cast :: filter_casts env from_typ to_typ casts
@@ -2400,11 +2403,11 @@ let rec check_exp env (E_aux (exp_aux, (l, ())) as exp : unit exp) (Typ_aux (typ
         print_endline ("Solved " ^ string_of_nexp nexp ^ " = " ^ Big_int.to_string n);
         annot_exp (E_lit (L_aux (L_unit, Parse_ast.Unknown))) unit_typ
      end
-  (* All constructors are treated as having one argument so Ctor(x, y)
-     is checked as Ctor((x, y)) *)
-  | E_app (ctor, x :: y :: zs), _ when Env.is_union_constructor ctor env ->
-     typ_print (lazy ("Checking multiple argument constructor: " ^ string_of_id ctor));
-     crule check_exp env (mk_exp ~loc:l (E_app (ctor, [mk_exp ~loc:l (E_tuple (x :: y :: zs))]))) typ
+  (* All constructors and mappings are treated as having one argument
+     so Ctor(x, y) is checked as Ctor((x, y)) *)
+  | E_app (f, x :: y :: zs), _ when Env.is_union_constructor f env || Env.is_mapping f env ->
+     typ_print (lazy ("Checking multiple argument constructor or mapping: " ^ string_of_id f));
+     crule check_exp env (mk_exp ~loc:l (E_app (f, [mk_exp ~loc:l (E_tuple (x :: y :: zs))]))) typ
   | E_app (mapping, xs), _ when Env.is_mapping mapping env ->
      let forwards_id = mk_id (string_of_id mapping ^ "_forwards") in
      let backwards_id = mk_id (string_of_id mapping ^ "_backwards") in
@@ -2725,7 +2728,9 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
             | Invalid_argument _ -> typ_error l "Tuple pattern and tuple type have different length"
           in
           annot_pat (P_tup (List.rev tpats)) typ, env, guards
-       | _ -> typ_error l "Cannot bind tuple pattern against non tuple type"
+       | _ ->
+          typ_error l (Printf.sprintf "Cannot bind tuple pattern %s against non tuple type %s"
+                         (string_of_pat pat) (string_of_typ typ))
      end
   | P_app (f, pats) when Env.is_union_constructor f env ->
      begin
@@ -2734,14 +2739,10 @@ and bind_pat env (P_aux (pat_aux, (l, ())) as pat) (Typ_aux (typ_aux, _) as typ)
        let untuple (Typ_aux (typ_aux, _) as typ) = match typ_aux with
          | Typ_tup typs -> typs
          | _ -> [typ]
-       in
+       in       
        match Env.expand_synonyms env ctor_typ with
-       | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
+       | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
           begin
-            let arg_typ = match arg_typ with
-              | Typ_aux (Typ_tup [arg_typ], _) -> arg_typ
-              | _ -> arg_typ
-            in
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for pattern " ^ string_of_typ typ));
               let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
@@ -3473,10 +3474,7 @@ and infer_funapp' l env f (typq, f_typ) xs ret_ctx_typ =
   in
   let quants, typ_args, typ_ret, eff =
     match Env.expand_synonyms env f_typ with
-    | Typ_aux (Typ_fn (Typ_aux (Typ_tup typ_args, _), typ_ret, eff), _) ->
-       quant_items typq, typ_args, typ_ret, eff
-    | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
-       quant_items typq, [typ_arg], typ_ret, eff
+    | Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) -> quant_items typq, typ_args, typ_ret, eff
     | _ -> typ_error l (string_of_typ f_typ ^ " is not a function type")
   in
   let unifiers = instantiate_simple_equations quants in
@@ -3610,12 +3608,8 @@ and bind_mpat allow_unknown other_env env (MP_aux (mpat_aux, (l, ())) as mpat) (
          | _ -> [typ]
        in
        match Env.expand_synonyms env ctor_typ with
-       | Typ_aux (Typ_fn (arg_typ, ret_typ, _), _) ->
+       | Typ_aux (Typ_fn ([arg_typ], ret_typ, _), _) ->
           begin
-            let arg_typ = match arg_typ with
-              | Typ_aux (Typ_tup [arg_typ], _) -> arg_typ
-              | _ -> arg_typ
-            in
             try
               typ_debug (lazy ("Unifying " ^ string_of_bind (typq, ctor_typ) ^ " for mapping-pattern " ^ string_of_typ typ));
               let unifiers, _, _ (* FIXME! *) = unify l env ret_typ typ in
@@ -4185,7 +4179,7 @@ let check_letdef orig_env (LB_aux (letbind, (l, _))) =
 
 let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
   match typ with
-  | Typ_aux (Typ_fn (typ_arg, typ_ret, eff), _) ->
+  | Typ_aux (Typ_fn (typ_args, typ_ret, eff), _) ->
      begin
        let env = Env.add_ret_typ typ_ret env in
        (* We want to forbid polymorphic undefined values in all cases,
@@ -4199,7 +4193,16 @@ let check_funcl env (FCL_aux (FCL_Funcl (id, pexp), (l, _))) typ =
          then Env.allow_polymorphic_undefineds env
          else env
        in
-       let typed_pexp, prop_eff = propagate_pexp_effect (check_case env typ_arg (strip_pexp pexp) typ_ret) in
+       (* This is one of the cases where we are allowed to treat
+          function arguments as like a tuple, and maybe we
+          shouldn't. *)
+       let typed_pexp, prop_eff =
+         match typ_args with
+         | [typ_arg] ->
+            propagate_pexp_effect (check_case env typ_arg (strip_pexp pexp) typ_ret)
+         | _ ->
+            propagate_pexp_effect (check_case env (Typ_aux (Typ_tup typ_args, l)) (strip_pexp pexp) typ_ret)
+       in
        FCL_aux (FCL_Funcl (id, typed_pexp), (l, Some ((env, typ, prop_eff), Some typ)))
      end
   | _ -> typ_error l ("Function clause must have function type: " ^ string_of_typ typ ^ " is not a function type")
@@ -4251,7 +4254,6 @@ let mapcl_effect (MCL_aux (_, (l, annot))) =
   | Some ((_, _, eff), _) -> eff
   | None -> no_effect (* Maybe could be assert false. This should never happen *)
 
-
 let infer_funtyp l env tannotopt funcls =
   match tannotopt with
   | Typ_annot_opt_aux (Typ_annot_opt_some (quant, ret_typ), _) ->
@@ -4266,8 +4268,15 @@ let infer_funtyp l env tannotopt funcls =
        match funcls with
        | [FCL_aux (FCL_Funcl (_, Pat_aux (pexp,_)), _)] ->
           let pat = match pexp with Pat_exp (pat,_) | Pat_when (pat,_,_) -> pat in
-          let arg_typ = typ_from_pat pat in
-          let fn_typ = mk_typ (Typ_fn (arg_typ, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
+          (* The function syntax lets us bind multiple function
+             arguments with a single pattern, hence why we need to do
+             this. But perhaps we don't want to allow this? *)
+          let arg_typs =
+            match typ_from_pat pat with
+            | Typ_aux (Typ_tup arg_typs, _) -> arg_typs
+            | arg_typ -> [arg_typ]
+          in
+          let fn_typ = mk_typ (Typ_fn (arg_typs, ret_typ, Effect_aux (Effect_set [], Parse_ast.Unknown))) in
           (quant, fn_typ)
        | _ -> typ_error l "Cannot infer function type for function with multiple clauses"
      end
@@ -4308,8 +4317,8 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
        let (quant, typ) = infer_funtyp l env tannotopt funcls in
        false, (quant, typ), env
   in
-  let vtyp_arg, vtyp_ret, declared_eff, vl = match typ with
-    | Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, declared_eff), vl) -> vtyp_arg, vtyp_ret, declared_eff, vl
+  let vtyp_args, vtyp_ret, declared_eff, vl = match typ with
+    | Typ_aux (Typ_fn (vtyp_args, vtyp_ret, declared_eff), vl) -> vtyp_args, vtyp_ret, declared_eff, vl
     | _ -> typ_error l "Function val spec was not a function type"
   in
   check_tannotopt env quant vtyp_ret tannotopt;
@@ -4320,7 +4329,7 @@ let check_fundef env (FD_aux (FD_function (recopt, tannotopt, effectopt, funcls)
   let vs_def, env, declared_eff =
     if not have_val_spec
     then
-      let typ = Typ_aux (Typ_fn (vtyp_arg, vtyp_ret, eff), vl) in
+      let typ = Typ_aux (Typ_fn (vtyp_args, vtyp_ret, eff), vl) in
       [mk_val_spec env quant typ id], Env.add_val_spec id (quant, typ) env, eff
     else [], env, declared_eff
   in
@@ -4429,15 +4438,8 @@ let check_type_union env variant typq (Tu_aux (tu, l)) =
      env
      |> Env.add_union_id v (typq, typ)
      |> Env.add_val_spec v (typq, typ)
-  | Tu_ty_id (typ, v) ->
-     (* If a constructor type is a tuple we need to wrap it again in a
-        dummy tuple constructor so that it actually gets treated as a
-        tuple and not a multiple argument function! *)
-     let tuple = match typ with
-       | Typ_aux (Typ_tup _, _) -> mk_typ (Typ_tup [typ])
-       | _ -> typ
-     in
-     let typ' = mk_typ (Typ_fn (tuple, ret_typ, no_effect)) in
+  | Tu_ty_id (arg_typ, v) ->
+     let typ' = mk_typ (Typ_fn ([arg_typ], ret_typ, no_effect)) in
      env
      |> Env.add_union_id v (typq, typ')
      |> Env.add_val_spec v (typq, typ')
@@ -4564,11 +4566,11 @@ let initial_env =
   |> Env.add_val_spec (mk_id "size_itself_int")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
-       function_typ (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))])
+       function_typ [app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]]
          (atom_typ (nvar (mk_kid "n"))) no_effect)
   |> Env.add_extern (mk_id "make_the_value") (fun _ -> Some "make_the_value")
   |> Env.add_val_spec (mk_id "make_the_value")
       (TypQ_aux (TypQ_tq [QI_aux (QI_id (KOpt_aux (KOpt_none (mk_kid "n"),Parse_ast.Unknown)),
                                   Parse_ast.Unknown)],Parse_ast.Unknown),
-       function_typ (atom_typ (nvar (mk_kid "n")))
+       function_typ [atom_typ (nvar (mk_kid "n"))]
          (app_typ (mk_id "itself") [mk_typ_arg (Typ_arg_nexp (nvar (mk_kid "n")))]) no_effect)
diff --git a/src/value.ml b/src/value.ml
index 6c9990a1..157c16fc 100644
--- a/src/value.ml
+++ b/src/value.ml
@@ -219,6 +219,10 @@ let value_string_drop = function
   | [v1; v2] -> V_string (Sail_lib.string_drop (coerce_string v1, coerce_int v2))
   | _ -> failwith "value string_drop"
 
+let value_string_take = function
+  | [v1; v2] -> V_string (Sail_lib.string_take (coerce_string v1, coerce_int v2))
+  | _ -> failwith "value string_take"
+
 let value_string_length = function
   | [v] -> V_int (coerce_string v |> Sail_lib.string_length)
   | _ -> failwith "value string_length"
@@ -549,6 +553,7 @@ let primops =
       ("eq_string", value_eq_string);
       ("string_startswith", value_string_startswith);
       ("string_drop", value_string_drop);
+      ("string_take", value_string_take);
       ("string_length", value_string_length);
       ("eq_bit", value_eq_bit);
       ("eq_anything", value_eq_anything);