simplify detection of functions when translating types

drivers/rust.drv

@@ -7,8 +7,6 @@ theory BuiltIn
 end
 
 module HighOrd
-  (* used by the printer to safely detect function types *)
-  syntax type (->) "FUNCTION_ARROW"
   (* TODO this does not work when there are multiple @ *)
   syntax val ( @ ) "%1(%2)"
 end

src/mlw/rust_printer.ml

@@ -135,19 +135,20 @@ module MLToRust = struct
 
   (* TODO make sure we don't extract any ghosts *)
 
+  let id_is_func = id_equal ts_func.ts_name
+
   let rec translate_ty info (t:ty) : Rust.ty =
     match t with
     | Tvar tvs -> Rust.Tvar tvs
     | Ttuple tl -> Rust.Ttuple (List.map (translate_ty info) tl)
-    (* specialization of a generic type *)
-    | Tapp (ts, tl) ->
-        let syn = query_syntax info.syntax ts in
-        match syn with
-        | Some "FUNCTION_ARROW" ->
-            (* recursively look for multi-argument functions *)
+    (* function *)
+    | Tapp (ts, tl) when id_is_func ts ->
         let args_and_res = function_sig info t in
         let args, res = Lists.chop_last args_and_res in
         Rust.Tfn(args, res)
+    (* specialization of a generic type *)
+    | Tapp (ts, tl) ->
+      match query_syntax info.syntax ts with
       | Some s -> Rust.Tsyn (s, List.map (translate_ty info) tl)
       | None ->
           let tl = List.map (translate_ty info) tl in
@@ -155,13 +156,10 @@ module MLToRust = struct
 
   and function_sig info (t:ty) : Rust.ty list =
     match t with
-    | Tapp (ts, tl) ->
-        (match query_syntax info.syntax ts with
-        | Some "FUNCTION_ARROW" ->
+    | Tapp (ts, tl) when id_is_func ts ->
         (match tl with
         | [ta; tb] -> translate_ty info ta :: function_sig info tb
         | _ -> assert false)
-        | _ -> [translate_ty info t])
     | _ -> [translate_ty info t]
 
   let translate_var (info:info) ((id, ty, _ghost):var) : Rust.var =
@@ -207,15 +205,6 @@ module MLToRust = struct
 
   exception MissingSyntaxLiteral
 
-  let get_record info rs =
-    match Mid.find_opt rs.rs_name info.mo_known_map with
-    | Some {pd_node = PDtype itdl} ->
-        let eq_rs {itd_constructors} =
-          List.exists (rs_equal rs) itd_constructors in
-        let itd = List.find eq_rs itdl in
-        List.filter (fun e -> not (rs_ghost e)) itd.itd_fields
-    | _ -> []
-
   let box_expr (e:Rust.expr) = Rust.Esyntax ("Box::new(%1)", [e])
 
   let rec translate_expr (info:info) (e:expr) : Rust.expr =