From b12e0836b066d3da70ca3a842d39377c2c9e9d90 Mon Sep 17 00:00:00 2001 From: Lasse Letager Hansen Date: Wed, 31 Jan 2024 17:55:26 +0100 Subject: [PATCH] Cleanup phases? --- engine/backends/coq/coq/coq_backend.ml | 1 - engine/backends/coq/coq_ast.ml | 29 ++++---- .../backends/coq/ssprove/ssprove_backend.ml | 2 +- engine/backends/fstar/fstar_backend.ml | 1 - engine/backends/proverif/proverif_backend.ml | 1 - engine/lib/diagnostics.ml | 1 - engine/lib/phases.ml | 1 - engine/lib/phases/phase_local_mutation.ml | 7 +- engine/lib/phases/phase_local_mutation.mli | 3 +- engine/lib/phases/phase_remove_mutation.ml | 66 ------------------- engine/lib/phases/phase_remove_mutation.mli | 28 -------- 11 files changed, 17 insertions(+), 123 deletions(-) delete mode 100644 engine/lib/phases/phase_remove_mutation.ml delete mode 100644 engine/lib/phases/phase_remove_mutation.mli diff --git a/engine/backends/coq/coq/coq_backend.ml b/engine/backends/coq/coq/coq_backend.ml index 2116782be..9f3b22779 100644 --- a/engine/backends/coq/coq/coq_backend.ml +++ b/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 diff --git a/engine/backends/coq/coq_ast.ml b/engine/backends/coq/coq_ast.ml index 09230b05d..610294aef 100644 --- a/engine/backends/coq/coq_ast.ml +++ b/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,8 +598,8 @@ 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 | [] -> "_" @@ -611,14 +607,13 @@ functor ^ "." ^ 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) -> "" diff --git a/engine/backends/coq/ssprove/ssprove_backend.ml b/engine/backends/coq/ssprove/ssprove_backend.ml index 3fc254873..6e110b57a 100644 --- a/engine/backends/coq/ssprove/ssprove_backend.ml +++ b/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 diff --git a/engine/backends/fstar/fstar_backend.ml b/engine/backends/fstar/fstar_backend.ml index f5d66ef43..0e5523088 100644 --- a/engine/backends/fstar/fstar_backend.ml +++ b/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 diff --git a/engine/backends/proverif/proverif_backend.ml b/engine/backends/proverif/proverif_backend.ml index ef2605be2..d0ffdfb6e 100644 --- a/engine/backends/proverif/proverif_backend.ml +++ b/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 diff --git a/engine/lib/diagnostics.ml b/engine/lib/diagnostics.ml index 048e3e50d..f6470cb77 100644 --- a/engine/lib/diagnostics.ml +++ b/engine/lib/diagnostics.ml @@ -34,7 +34,6 @@ module Phase = struct | ResugarQuestionMarks | HoistSideEffects | LocalMutation - | RemoveMutation | TrivializeAssignLhs | CfIntoMonads | FunctionalizeLoops diff --git a/engine/lib/phases.ml b/engine/lib/phases.ml index b7c3bb1b2..07a971f21 100644 --- a/engine/lib/phases.ml +++ b/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 diff --git a/engine/lib/phases/phase_local_mutation.ml b/engine/lib/phases/phase_local_mutation.ml index 3457fd63a..06dc1ff9c 100644 --- a/engine/lib/phases/phase_local_mutation.ml +++ b/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; diff --git a/engine/lib/phases/phase_local_mutation.mli b/engine/lib/phases/phase_local_mutation.mli index a45350fa9..6dec94af3 100644 --- a/engine/lib/phases/phase_local_mutation.mli +++ b/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 diff --git a/engine/lib/phases/phase_remove_mutation.ml b/engine/lib/phases/phase_remove_mutation.ml deleted file mode 100644 index cf5050025..000000000 --- a/engine/lib/phases/phase_remove_mutation.ml +++ /dev/null @@ -1,66 +0,0 @@ -(* TODO: handle Exn report *) -open! Prelude -open Side_effect_utils - -module%inlined_contents Make - (F : Features.T - with type mutable_reference = Features.Off.mutable_reference - and type mutable_pointer = Features.Off.mutable_pointer - and type raw_pointer = Features.Off.raw_pointer - and type arbitrary_lhs = Features.Off.arbitrary_lhs - and type nontrivial_lhs = Features.Off.nontrivial_lhs - and type monadic_action = Features.Off.monadic_action - and type monadic_binding = Features.Off.monadic_binding - and type for_index_loop = Features.Off.for_index_loop - and type state_passing_loop = Features.On.state_passing_loop) = -struct - open Ast - module FA = F - - module FB = struct - include F - include Features.Off.Mutable_variable - end - - include - Phase_utils.MakeBase (F) (FB) - (struct - let phase_id = Diagnostics.Phase.RemoveMutation - end) - - module Implem : ImplemT.T = struct - let metadata = metadata - - module UA = Ast_utils.Make (F) - module UB = Ast_utils.Make (FB) - - module S = struct - include Features.SUBTYPE.Id - end - - module SI = MakeSI (FB) - - [%%inline_defs dmutability] - - 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; subpat; _ } -> - PBinding - { - mut = Immutable; - mode = ByValue; - var; - typ = dty span typ; - subpat = Option.map ~f:(dpat *** Fn.id) subpat; - } - | PDeref { subpat; _ } -> (dpat subpat).p - - and dexpr_unwrapped e = dexpr e [@@inline_ands bindings_of dexpr - dexpr'] - - [%%inline_defs "Item.*"] - end - - include Implem -end -[@@add "subtype.ml"] diff --git a/engine/lib/phases/phase_remove_mutation.mli b/engine/lib/phases/phase_remove_mutation.mli deleted file mode 100644 index e8d1e02a8..000000000 --- a/engine/lib/phases/phase_remove_mutation.mli +++ /dev/null @@ -1,28 +0,0 @@ -open! Prelude - -module Make - (F : Features.T - with type mutable_reference = Features.Off.mutable_reference - and type mutable_pointer = Features.Off.mutable_pointer - and type raw_pointer = Features.Off.raw_pointer - and type arbitrary_lhs = Features.Off.arbitrary_lhs - and type nontrivial_lhs = Features.Off.nontrivial_lhs - and type monadic_action = Features.Off.monadic_action - and type monadic_binding = Features.Off.monadic_binding - and type for_index_loop = Features.Off.for_index_loop - and type state_passing_loop = Features.On.state_passing_loop) : sig - include module type of struct - module FA = F - - module FB = struct - include F - include Features.Off.Mutable_variable - end - - module A = Ast.Make (F) - module B = Ast.Make (FB) - module ImplemT = Phase_utils.MakePhaseImplemT (A) (B) - end - - include ImplemT.T -end