From b8c162ce9cb1faeec621b751fff9aff46e022417 Mon Sep 17 00:00:00 2001
From: Tom Smeding <tom@tomsmeding.com>
Date: Thu, 14 Nov 2024 19:27:57 +0100
Subject: Configuration for CHAD

---
 src/CHAD/Top.hs | 13 +++++++------
 1 file changed, 7 insertions(+), 6 deletions(-)

(limited to 'src/CHAD/Top.hs')

diff --git a/src/CHAD/Top.hs b/src/CHAD/Top.hs
index 9df5412..4b2a844 100644
--- a/src/CHAD/Top.hs
+++ b/src/CHAD/Top.hs
@@ -1,5 +1,6 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE ImplicitParams #-}
 {-# LANGUAGE PolyKinds #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
@@ -41,13 +42,13 @@ d1eIdentity :: SList STy env -> D1E env :~: env
 d1eIdentity SNil = Refl
 d1eIdentity (t `SCons` env) | Refl <- d1Identity t, Refl <- d1eIdentity env = Refl
 
-chad :: SList STy env -> Ex env t -> Ex (D2 t : D1E env) (TPair (D1 t) (Tup (D2E env)))
-chad env term
+chad :: CHADConfig -> SList STy env -> Ex env t -> Ex (D2 t : D1E env) (TPair (D1 t) (Tup (D2E env)))
+chad config env term
   | Refl <- mergeEnvNoAccum env
   , Refl <- mergeEnvOnlyMerge env
-  = freezeRet (mergeDescr env) (drev (mergeDescr env) term)
+  = let ?config = config in freezeRet (mergeDescr env) (drev (mergeDescr env) term)
 
-chad' :: SList STy env -> Ex env t -> Ex (D2 t : env) (TPair t (Tup (D2E env)))
-chad' env term
+chad' :: CHADConfig -> SList STy env -> Ex env t -> Ex (D2 t : env) (TPair t (Tup (D2E env)))
+chad' config env term
   | Refl <- d1eIdentity env, Refl <- d1Identity (typeOf term)
-  = chad env term
+  = chad config env term
-- 
cgit v1.2.3-70-g09d2