From a210419fd60c00d011f70fb1b968031621e4c01a Mon Sep 17 00:00:00 2001
From: Arnaud Bailly <arnaud@pankzsoft.com>
Date: Tue, 28 Oct 2025 18:34:16 +0100
Subject: Provide function to go back from a deBruijn term to an AST

---
 .../haskell/src/Minilang/Lambda/DeBruijn.hs        | 43 +++++++++++++++-------
 1 file changed, 29 insertions(+), 14 deletions(-)

(limited to 'lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs')

diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
index 6b5b7a2..290839e 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/DeBruijn.hs
@@ -1,42 +1,57 @@
+{-# LANGUAGE LambdaCase #-}
 module Minilang.Lambda.DeBruijn where
 
 import Data.List (elemIndex)
-import Data.Text (Text)
+import Data.Text (Text, unpack, pack)
 import Minilang.Lambda.Eval (Term)
 import qualified Minilang.Lambda.Eval as Eval
 
-data DeBruijn
+data DeBruijn ann
   = FV Text
-  | Var Int
-  | Lam DeBruijn
-  | App DeBruijn DeBruijn
+  | Var ann Int
+  | Lam ann (DeBruijn ann)
+  | App (DeBruijn ann) (DeBruijn ann)
   deriving (Show, Read, Eq)
 
+fromDeBruijn :: DeBruijn Text -> Term
+fromDeBruijn = \case
+  FV x -> Eval.Var x
+  Var s _ -> Eval.Var s
+  Lam s body -> Eval.Lam s (fromDeBruijn body)
+  App f a -> Eval.App (fromDeBruijn f) (fromDeBruijn a)
+
 -- Convert a term with named variables to De Bruijn indices
-toDeBruijn :: Term -> DeBruijn
+toDeBruijn :: Term -> DeBruijn Text
 toDeBruijn term = go term []
   where
     go (Eval.Var x) env =
       case elemIndex x env of
-        Just idx -> Var idx
+        Just idx -> Var x idx
         Nothing -> FV x
     go (Eval.Lam x body) env =
-      Lam (go body (x : env))
+      Lam x (go body (x : env))
     go (Eval.App f a) env =
       App (go f env) (go a env)
 
-eval :: DeBruijn -> DeBruijn
+eval :: DeBruijn ann -> DeBruijn ann
 eval (App f a) =
   case eval f of
-    Lam body -> eval (substitute 0 a body)
+    Lam _ body -> eval (substitute 0 a body)
     f' -> App f' a
 eval term = term
 
-substitute :: Int -> DeBruijn -> DeBruijn -> DeBruijn
+substitute :: Int -> DeBruijn ann -> DeBruijn ann -> DeBruijn ann
 substitute n arg term = case term of
   FV x -> FV x
-  Var x
+  Var t x
     | x == n -> arg
-    | otherwise -> Var x
-  Lam body -> Lam (substitute (n + 1) arg body)
+    | otherwise -> Var t x
+  Lam x body -> Lam x (substitute (n + 1) arg body)
   App f a -> App (substitute n arg f) (substitute n arg a)
+
+pretty :: DeBruijn Text -> Text
+pretty = \case
+  FV x -> x
+  Var s _ -> s
+  Lam s body -> "(lam (" <> s <> ") " <> pretty body <> ")"
+  App f a -> "(" <> pretty f <> " " <> pretty a <> ")"
-- 
cgit v1.3.1