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.

1 files changed, 4 insertions, 3 deletions

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) ->