diff options
| author | Tom Smeding <tom@tomsmeding.com> | 2024-11-14 19:27:57 +0100 |
|---|---|---|
| committer | Tom Smeding <tom@tomsmeding.com> | 2024-11-14 19:27:57 +0100 |
| commit | b8c162ce9cb1faeec621b751fff9aff46e022417 (patch) | |
| tree | 9c31700f34f9a1f1a67e0a73c880938130e87ee6 /src/CHAD/Top.hs | |
| parent | bb84f6930702a02ba982795e2bb95a64d61f672b (diff) | |
Configuration for CHAD
Diffstat (limited to 'src/CHAD/Top.hs')
| -rw-r--r-- | src/CHAD/Top.hs | 13 |
1 files changed, 7 insertions, 6 deletions
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 |