split specialisation into an explicit pass module

src/pipeline.ml

@@ -42,29 +42,6 @@ let default_flags =
 let obligation ?(kind = Preserve_relation) pass subject detail =
   { pass; kind; subject; detail }
 
-let rec specialise_term note term =
-  match term with
-  | Source.TyApp (Source.TyLam (x, body), ty) ->
-      note Preserve_relation "type application cloning" ("instantiated type binder " ^ x ^ " at " ^ Types.string_of_typ ty);
-      Source.(substitute_type x ty (specialise_term note body))
-  | Source.Pair (a, b) -> Source.Pair (specialise_term note a, specialise_term note b)
-  | Source.Inl (ty, t) -> Source.Inl (ty, specialise_term note t)
-  | Source.Inr (ty, t) -> Source.Inr (ty, specialise_term note t)
-  | Source.Lam (x, a, b, body) -> Source.Lam (x, a, b, specialise_term note body)
-  | Source.App (f, a) -> Source.App (specialise_term note f, specialise_term note a)
-  | Source.TyLam (x, body) -> Source.TyLam (x, specialise_term note body)
-  | Source.TyApp (t, ty) -> Source.TyApp (specialise_term note t, ty)
-  | Source.Roll (ty, t) -> Source.Roll (ty, specialise_term note t)
-  | Source.Unroll t -> Source.Unroll (specialise_term note t)
-  | Source.Fix (f, ty, body) -> Source.Fix (f, ty, specialise_term note body)
-  | Source.Eq (g, a, b) -> Source.Eq (g, specialise_term note a, specialise_term note b)
-  | Source.If (c, t, e) -> Source.If (specialise_term note c, specialise_term note t, specialise_term note e)
-  | Source.Let (x, a, b) -> Source.Let (x, specialise_term note a, specialise_term note b)
-  | Source.LetPair (x, y, a, b) -> Source.LetPair (x, y, specialise_term note a, specialise_term note b)
-  | Source.Case (s, (x, l), (y, r)) ->
-      Source.Case (specialise_term note s, (x, specialise_term note l), (y, specialise_term note r))
-  | other -> other
-
 let rec inline_cost = function
   | Source.Int _ | Source.Bool _ | Source.Var _ -> 1
   | Source.Lam (_, _, _, body) | Source.TyLam (_, body) -> 1 + inline_cost body
@@ -201,7 +178,10 @@ let compile flags source_type source_program =
     obligations := obligation ~kind pass subject detail :: !obligations
   in
   let specialised =
-    if flags.specialise then specialise_term (note "specialise") source_program
+    if flags.specialise then
+      Specialise.run
+        ~note:(fun ~subject ~detail -> note "specialise" Preserve_relation subject detail)
+        source_program
     else source_program
   in
   let inlined =

src/specialise.ml

@@ -0,0 +1,26 @@
+open Types
+
+let rec run ~note term =
+  match term with
+  | Source.TyApp (Source.TyLam (x, body), ty) ->
+      note
+        ~subject:"type application cloning"
+        ~detail:("instantiated type binder " ^ x ^ " at " ^ string_of_typ ty);
+      Source.(substitute_type x ty (run ~note body))
+  | Source.Pair (a, b) -> Source.Pair (run ~note a, run ~note b)
+  | Source.Inl (ty, t) -> Source.Inl (ty, run ~note t)
+  | Source.Inr (ty, t) -> Source.Inr (ty, run ~note t)
+  | Source.Lam (x, a, b, body) -> Source.Lam (x, a, b, run ~note body)
+  | Source.App (f, a) -> Source.App (run ~note f, run ~note a)
+  | Source.TyLam (x, body) -> Source.TyLam (x, run ~note body)
+  | Source.TyApp (t, ty) -> Source.TyApp (run ~note t, ty)
+  | Source.Roll (ty, t) -> Source.Roll (ty, run ~note t)
+  | Source.Unroll t -> Source.Unroll (run ~note t)
+  | Source.Fix (f, ty, body) -> Source.Fix (f, ty, run ~note body)
+  | Source.Eq (g, a, b) -> Source.Eq (g, run ~note a, run ~note b)
+  | Source.If (c, t, e) -> Source.If (run ~note c, run ~note t, run ~note e)
+  | Source.Let (x, a, b) -> Source.Let (x, run ~note a, run ~note b)
+  | Source.LetPair (x, y, a, b) -> Source.LetPair (x, y, run ~note a, run ~note b)
+  | Source.Case (s, (x, l), (y, r)) ->
+      Source.Case (run ~note s, (x, run ~note l), (y, run ~note r))
+  | other -> other

src/specialise.mli

@@ -0,0 +1 @@
+val run : note:(subject:string -> detail:string -> unit) -> Source.term -> Source.term

src/vanity.ml

@@ -1,6 +1,7 @@
 module Types = Types
 module Source = Source
 module Target = Target
+module Specialise = Specialise
 module Pipeline = Pipeline
 module Relation = Relation
 module Typecheck = Typecheck