Cleanup phases?

engine/backends/coq/coq/coq_backend.ml

@@ -723,7 +723,6 @@ module TransformToInputLanguage =
   |> Phases.Reconstruct_question_marks
   |> Side_effect_utils.Hoist
   |> Phases.Local_mutation
-  |> Phases.Remove_mutation
   |> Phases.Reject.Continue
   |> Phases.Cf_into_monads
   |> Phases.Reject.EarlyExit

engine/backends/coq/coq_ast.ml

@@ -264,7 +264,7 @@ functor
               (List.map ~f:(fun t -> pat_to_string t false (depth + 1)) vals)
           ^ ")"
       | AST.AscriptionPat (p, ty) ->
-          "(" ^ pat_to_string p true depth ^ ":" ^ ty_to_string ty
+          "(" ^ pat_to_string p true depth ^ " " ^ ":" ^ " " ^ ty_to_string ty
           ^ ")" (* TODO: Should this be true of false? *)
       | AST.DisjunctivePat pats ->
           let f pat = pat_to_string pat true depth in
@@ -448,7 +448,7 @@ functor
           in
           "Record" ^ " " ^ name
           ^ params_to_string_typed arguments
-          ^ " " ^ ":" ^ " " ^ "Type" ^ " " ^ ":=" ^ "{" ^ variants_str
+          ^ " " ^ ":" ^ " " ^ "Type" ^ " " ^ ":=" ^ " " ^ "{" ^ variants_str
           ^ newline_indent 0 ^ "}."
       | AST.Inductive (name, arguments, variants) ->
           let name_arguments = name ^ params_to_string_typed arguments in
@@ -474,8 +474,8 @@ functor
                 (List.fold_left ~init:"" ~f:(fun a b -> a ^ " {_}") arguments)
                 "."
           in
-          "Inductive" ^ " " ^ name_arguments ^ ":" ^ " " ^ "Type" ^ " " ^ ":="
-          ^ newline_indent 0 ^ variants_str ^ "." ^ args_str
+          "Inductive" ^ " " ^ name_arguments ^ " " ^ ":" ^ " " ^ "Type" ^ " "
+          ^ ":=" ^ newline_indent 0 ^ variants_str ^ "." ^ args_str
       | AST.Class (name, arguments, trait_items) ->
           let field_str =
             List.fold_left ~init:""
@@ -536,9 +536,7 @@ functor
           ^ " " ^ "End" ^ " " ^ name ^ "."
       | AST.Instance (name, arguments, self_ty, ty_list, impl_list) ->
           let ty_list_str =
-            List.fold_left ~init:""
-              ~f:(fun x y -> x ^ ty_to_string y ^ " ")
-              ty_list
+            String.concat ~sep:" " (List.map ~f:ty_to_string ty_list)
           in
           let impl_str =
             List.fold_left ~init:""
@@ -553,14 +551,12 @@ functor
           let ty_str = ty_to_string self_ty in
           "#[global] Instance" ^ " " ^ ty_str ^ "_" ^ name
           ^ params_to_string_typed arguments
-          ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ ":=" ^ " " ^ "{"
+          ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":=" ^ " " ^ "{"
           ^ impl_str ^ newline_indent 0 ^ "}" ^ "."
       | AST.ProgramInstance
           (name, arguments, self_ty, ty_list, InstanceDecls impl_list) ->
           let ty_list_str =
-            List.fold_left ~init:""
-              ~f:(fun x y -> x ^ ty_to_string y ^ " ")
-              ty_list
+            String.concat ~sep:" " (List.map ~f:ty_to_string ty_list)
           in
           let impl_str, impl_str_empty =
             let fl =
@@ -602,23 +598,22 @@ functor
           let ty_str = ty_to_string self_ty in
           "#[global] Program Instance" ^ " " ^ ty_str ^ "_" ^ name
           ^ params_to_string_typed arguments
-          ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ ":=" ^ newline_indent 1
-          ^ impl_str
+          ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":="
+          ^ newline_indent 1 ^ impl_str
           ^ (if impl_str_empty then "" else newline_indent 1)
           ^ (match impl_list with
             | [] -> "_"
             | _ -> "{|" (* ^ name ^ " " ^ ty_list_str *) ^ " " ^ arg_str ^ "|}")
           ^ "." ^ fail_next_obligation
       | AST.ProgramInstance (name, arguments, self_ty, ty_list, TermDef term) ->
           let ty_list_str =
-            List.fold_left ~init:""
-              ~f:(fun x y -> x ^ ty_to_string y ^ " ")
-              ty_list
+            String.concat ~sep:" " (List.map ~f:ty_to_string ty_list)
           in
           let ty_str = ty_to_string self_ty in
           "#[global] Program Instance" ^ " " ^ ty_str ^ "_" ^ name
           ^ params_to_string_typed arguments
-          ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ ":=" ^ newline_indent 1
+          ^ " " ^ ":" ^ " " ^ name ^ " " ^ ty_list_str ^ " " ^ ":="
+          ^ newline_indent 1
           ^ term_to_string_without_paren term 1
           ^ "." ^ fail_next_obligation
       | AST.Require (_, [], rename) -> ""

engine/backends/coq/ssprove/ssprove_backend.ml

@@ -615,7 +615,7 @@ module TransformToInputLanguage (* : PHASE *) =
     |> Phases.Trivialize_assign_lhs
     |> Phases.Reconstruct_question_marks
     |> Side_effect_utils.Hoist
-    |> Phases.Local_mutation
+    (* |> Phases.Local_mutation *)
     (* |> Phases.State_passing_loop *)
     |> Phases.Reject.Continue
     |> Phases.Cf_into_monads

engine/backends/fstar/fstar_backend.ml

@@ -1266,7 +1266,6 @@ module TransformToInputLanguage =
   |> Phases.Reconstruct_question_marks
   |> Side_effect_utils.Hoist
   |> Phases.Local_mutation
-  |> Phases.Remove_mutation
   |> Phases.Reject.Continue
   |> Phases.Cf_into_monads
   |> Phases.Reject.EarlyExit

engine/backends/proverif/proverif_backend.ml

@@ -587,7 +587,6 @@ module TransformToInputLanguage =
   |> Phases.Trivialize_assign_lhs
   |> Side_effect_utils.Hoist
   |> Phases.Local_mutation
-  |> Phases.Remove_mutation
   |> Phases.Reject.Continue
   |> Phases.Reconstruct_question_marks
   |> SubtypeToInputLanguage

engine/lib/diagnostics.ml

@@ -34,7 +34,6 @@ module Phase = struct
     | ResugarQuestionMarks
     | HoistSideEffects
     | LocalMutation
-    | RemoveMutation
     | TrivializeAssignLhs
     | CfIntoMonads
     | FunctionalizeLoops

engine/lib/phases.ml

@@ -9,4 +9,3 @@ module Cf_into_monads = Phase_cf_into_monads.Make
 module Functionalize_loops = Phase_functionalize_loops.Make
 module Reject = Phase_reject
 module Local_mutation = Phase_local_mutation.Make
-module Remove_mutation = Phase_remove_mutation.Make

engine/lib/phases/phase_local_mutation.ml

@@ -18,8 +18,7 @@ struct
 
   module FB = struct
     include F
-
-    (* include Features.Off.Mutable_variable *)
+    include Features.Off.Mutable_variable
     include Features.On.State_passing_loop
   end
 
@@ -62,10 +61,10 @@ struct
     let rec dpat' (span : span) (p : A.pat') : B.pat' =
       match p with
       | [%inline_arms "dpat'.*" - PBinding - PDeref] -> auto
-      | PBinding { var : Local_ident.t; typ; mut; subpat; _ } ->
+      | PBinding { var : Local_ident.t; typ; subpat; _ } ->
           PBinding
             {
-              mut;
+              mut = Immutable;
               mode = ByValue;
               var;
               typ = dty span typ;

engine/lib/phases/phase_local_mutation.mli

@@ -15,8 +15,7 @@ module Make
 
     module FB = struct
       include F
-
-      (* include Features.Off.Mutable_variable *)
+      include Features.Off.Mutable_variable
       include Features.On.State_passing_loop
     end