From 4e8713aa42b93294e13e99578436f2d06dbf4910 Mon Sep 17 00:00:00 2001
From: Hiroyuki Katsura <katsura@kb.is.s.u-tokyo.ac.jp>
Date: Sun, 21 Jul 2024 01:42:35 +0900
Subject: [PATCH] Add preproc "Peephole" that implements beta-reduction

---
 lib/rethfl.ml       |  4 ++++
 lib/syntax/trans.ml | 36 +++++++++++++++++++++++++++++++++++-
 2 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/lib/rethfl.ml b/lib/rethfl.ml
index a8fdba3..d34e7c3 100644
--- a/lib/rethfl.ml
+++ b/lib/rethfl.ml
@@ -56,6 +56,10 @@ let main file =
   Log.app begin fun m -> m ~header:"Simplified" "%a"
     Print.(hflz_hes simple_ty_) psi
   end;
+  let psi = Syntax.Trans.Peephole.hflz_hes psi in
+  Log.app begin fun m -> m ~header:"Peephole" "%a"
+    Print.(hflz_hes simple_ty_) psi
+  end;
   let psi, top = Syntax.Trans.Preprocess.main psi in
   match top with
   | Some(top) -> begin
diff --git a/lib/syntax/trans.ml b/lib/syntax/trans.ml
index 1111a14..3acac7a 100644
--- a/lib/syntax/trans.ml
+++ b/lib/syntax/trans.ml
@@ -577,6 +577,40 @@ module RemoveDisjunction = struct
 
 end
 
+module Peephole = struct
+  let rec translate_body = fun body ->
+    let open Hflz in
+    match body with
+    | Bool _
+    | Arith _
+    | Var _
+    | Pred(_, _) -> body
+    | Or(x, y) ->
+      let x' = translate_body x in
+      let y' = translate_body y in
+      Or(x', y')
+    | And(x, y) ->
+      let x' = translate_body x in
+      let y' = translate_body y in
+      And(x', y')
+    | Forall(x, y) ->
+      let y' = translate_body y in
+      Forall(x, y')
+    | Abs(id, y) ->
+      let y' = translate_body y in
+      Abs(id, y')
+    | App(x, y) ->
+      let x' = translate_body x in
+      let y' = translate_body y in
+      begin match x with
+        | Abs(id, x'') -> Subst.Hflz.hflz (IdMap.of_list [id,y']) x''
+        | _ -> App(x', y')
+      end
+  let hflz_hes_rule : 'a Hflz.hes_rule -> 'a Hflz.hes_rule =
+    fun rule -> { rule with body = translate_body rule.body }
+  let hflz_hes : simple_ty Hflz.hes -> simple_ty Hflz.hes = List.map ~f:hflz_hes_rule
+end
+
 module Preprocess = struct
   (* gets hes_rule list. returns hes_rule list and toplevel name*)
   let translate_top top_rule = 
@@ -593,4 +627,4 @@ module Preprocess = struct
   let main psi = match psi with
     | [] -> [], None
     | top::xs -> translate_top top::xs, Some(top.var)
-end
+end
\ No newline at end of file