diff options
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 |