[ experim ] Nail down every implementation of derivation interfaces

Author: buzden

src/Deriving/DepTyCheck/Gen.idr

@@ -297,7 +297,7 @@ wrapFuel fuelArg = lam $ MkArg MW ExplicitArg (Just fuelArg) `(Data.Fuel.Fuel)
 ------------------------------
 
 export
-deriveGenExpr : DeriveBodyForType => (signature : TTImp) -> Elab TTImp
+deriveGenExpr : (signature : TTImp) -> Elab TTImp
 deriveGenExpr signature = do
   checkResult@(signature ** externals ** _) <- checkTypeIsGen DerivationTask signature
   let externalsSigToName = fromList $ externals.externals <&> \(sig, _) => (sig, nameForGen sig)
@@ -345,7 +345,7 @@ deriveGenExpr signature = do
 |||
 |||
 export %macro
-deriveGen : DeriveBodyForType => Elab a
+deriveGen : Elab a
 deriveGen = do
   Just signature <- goal
      | Nothing => fail "The goal signature is not found. Generators derivation must be used only for fully defined signatures"
@@ -365,7 +365,7 @@ deriveGen = do
 |||   genX = deriveGenFor $ Fuel -> (Fuel -> Gen Y) => (a : A) -> (c : C) -> Gen (b ** X a b c)
 |||   ```
 export %macro
-deriveGenFor : DeriveBodyForType => (0 a : Type) -> Elab a
+deriveGenFor : (0 a : Type) -> Elab a
 deriveGenFor a = do
   sig <- quote a
   tt <- deriveGenExpr sig
@@ -376,7 +376,7 @@ deriveGenFor a = do
 ||| Caution! When `logDerivation` is set to `True`, this function would change the global logging state
 ||| and wouldn't turn it back.
 export
-deriveGenPrinter : {default True printTTImp : _} -> {default True logDerivation : _} -> DeriveBodyForType => Type -> Elab Unit
+deriveGenPrinter : {default True printTTImp : _} -> {default True logDerivation : _} -> Type -> Elab Unit
 deriveGenPrinter ty = do
   ty <- quote ty
   when logDerivation $ declare `[%logging "deptycheck.derive.print" 5; %logging "deptycheck.derive.least-effort" 7]
@@ -391,12 +391,3 @@ deriveGenPrinter ty = do
       putStr $ if ~printTTImp then interpolate ~expr else show ~expr
       putStrLn ""
   ]
-
------------------------
---- Global defaults ---
------------------------
-
-%defaulthint %inline
-public export
-DefaultConstructorDerivator : DeriveBodyRhsForCon
-DefaultConstructorDerivator = LeastEffort

src/Deriving/DepTyCheck/Gen/ForAllNeededTypes/Impl.idr

@@ -50,7 +50,7 @@ considerNewType ty = do
   _ : (NamesInfoInTypes, ConsRecs) <- get
   when .| not (isTypeKnown ty) .| updateNamesAndConsRecs ty >>= put
 
-Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.DerivationClosure m = (DeriveBodyForType, Monad m, Elaboration m, ClosuringContext m)
+Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.DerivationClosure m = (Monad m, Elaboration m, ClosuringContext m)
 
 Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.needWeightFun ty = when (not !(gets $ contains ty.name)) $ do
   modify {stateType=SortedSet Name} $ insert ty.name
@@ -124,7 +124,7 @@ Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface.callGen sig fuel values = do
 --- Canonic-dischagring function ---
 
 export
-runCanonic : DeriveBodyForType => NamesInfoInTypes => ConsRecs =>
+runCanonic : NamesInfoInTypes => ConsRecs =>
              SortedMap ExternalGenSignature Name -> (forall m. DerivationClosure m => m a) -> Elab (a, List Decl)
 runCanonic exts calc = do
   let exts = SortedMap.fromList $ exts.asList <&> \namedSig => (fst $ internalise $ fst namedSig, namedSig)

src/Deriving/DepTyCheck/Gen/ForOneType/Impl.idr

@@ -36,9 +36,7 @@ canonicDefaultRHS = canonicDefaultRHS' id
 --- Derivation functions ---
 ----------------------------
 
-export
-DeriveBodyRhsForCon => DeriveBodyForType where
-  canonicBody sig n = do
+Deriving.DepTyCheck.Gen.ForOneType.Interface.canonicBody sig n = do
 
     -- check that there is at least one constructor
     Prelude.when .| null sig.targetType.cons .| fail "No constructors found for the type `\{show sig.targetType.name}`"
@@ -107,7 +105,3 @@ DeriveBodyRhsForCon => DeriveBodyForType where
 
         callConsGen : (fuel : TTImp) -> Con -> TTImp
         callConsGen fuel con = canonicDefaultRHS' interimNamesWrapper sig .| consGenName con .| fuel
-
-export
-MainCoreDerivator : DeriveBodyRhsForCon => DeriveBodyForType
-MainCoreDerivator = %search

src/Deriving/DepTyCheck/Gen/ForOneType/Interface.idr

@@ -9,6 +9,5 @@ import public Deriving.DepTyCheck.Gen.Signature
 --- Deriving body of a generator for a single type ---
 ------------------------------------------------------
 
-public export
-interface DeriveBodyForType where
-  canonicBody : DerivationClosure m => Elaboration m => NamesInfoInTypes => ConsRecs => GenSignature -> Name -> m $ List Clause
+export
+canonicBody : DerivationClosure m => Elaboration m => NamesInfoInTypes => ConsRecs => GenSignature -> Name -> m $ List Clause

src/Deriving/DepTyCheck/Gen/ForOneTypeCon/Impl.idr

@@ -20,7 +20,7 @@ isSimpleBindVar $ IBindVar {} = True
 isSimpleBindVar _             = False
 
 export
-canonicConsBody : DeriveBodyRhsForCon => DerivationClosure m => Elaboration m => NamesInfoInTypes => GenSignature -> Name -> Con -> m $ List Clause
+canonicConsBody : DerivationClosure m => Elaboration m => NamesInfoInTypes => GenSignature -> Name -> Con -> m $ List Clause
 canonicConsBody sig name con = do
 
   -- Get file position of the constructor definition (for better error reporting)

src/Deriving/DepTyCheck/Gen/ForOneTypeConRhs/Impl.idr

@@ -216,13 +216,11 @@ callCon con = reAppAny (var con.name) . toList . mapI (appArg . index' con.args)
 -- "Non-obligatory" means that some present external generator of some type
 -- may be ignored even if its type is really used in a generated data constructor.
 
-||| Least-effort non-obligatory tactic is one which *does not use externals* during taking a decision on the order.
-||| It uses externals if decided order happens to be given by an external generator, but is not obliged to use any.
-||| It is seemingly most simple to implement, maybe the fastest and
-||| fits well when external generators are provided for non-dependent types.
-export
-[LeastEffort] DeriveBodyRhsForCon where
-  consGenExpr sig con givs fuel = do
+-- Least-effort non-obligatory tactic is one which *does not use externals* during taking a decision on the order.
+-- It uses externals if decided order happens to be given by an external generator, but is not obliged to use any.
+-- It is seemingly most simple to implement, maybe the fastest and
+-- fits well when external generators are provided for non-dependent types.
+Deriving.DepTyCheck.Gen.ForOneTypeConRhs.Interface.consGenExpr sig con givs fuel = do
 
     -------------------------------------------------------------
     -- Prepare intermediate data and functions using this data --
@@ -355,54 +353,3 @@ export
         let df = believe_me $ deriveFirst @{impl} (rewrite tyLen in Prelude.toList sig.givenParams) (rewrite conLen in Prelude.toList givs)
         let userImposed = filter (not . contains' givs) $ nub $ conArgIdx <$> df
         logValue FineDetails "deptycheck.derive.least-effort" [sig, con] "- user-imposed: \{userImposed}" userImposed
-
---||| Best effort non-obligatory tactic tries to use as much external generators as possible
---||| but discards some there is a conflict between them.
---||| All possible non-conflicting layouts may be produced in the generated values list.
---|||
---||| E.g. when we have external generators ``(a : _) -> (b : T ** C a b)`` and ``(b : T ** D b)`` and
---||| a constructor of form ``C a b -> D b -> ...``, we can use values from both pairs
---||| ``(a : _) -> (b : T ** C a b)`` with ``(b : T) -> D b`` and
---||| ``(a : _) -> (b : T) -> C a b`` with ``(b : T ** D b)``,
---||| i.e. to use both of external generators to form the generated values list
---||| but not obligatorily all the external generators at the same time.
---export
---[BestEffort] DeriveBodyRhsForCon where
---  consGenExpr sig con givs fuel = do
---    ?cons_body_besteff_nonoblig_rhs
-
---------------------------
---- Obligatory tactics ---
---------------------------
-
--- "Obligatory" means that is some external generator is present and a constructor has
--- an argument of a type which is generated by this external generator, it must be used
--- in the constructor's generator.
---
--- Dependent types are important here, i.e. generator ``(a : _) -> (b ** C a b)``
--- is considered to be a generator for the type ``C``.
--- The problem with obligatory generators is that some external generators may be incompatible.
---
---   E.g. once we have ``(a : _) -> (b ** C a b)`` and ``(a ** b ** C a b)`` at the same time,
---   once ``C`` is used in the same constructor, we cannot guarantee that we will use both external generators.
---
---   The same problem is present once we have external generators for ``(a : _) -> (b : T ** C a b)`` and ``(b : T ** D b)`` at the same time,
---   and both ``C`` and ``D`` are used in the same constructor with the same parameter of type ``T``,
---   i.e. when constructor have something like ``C a b -> D b -> ...``.
---
---   Notice, that this problem does not arise in constructors of type ``C a b1 -> D b2 -> ...``
---
--- In this case, we cannot decide in general which value of type ``T`` to be used for generation is we have to use both generators.
--- We can either fail to generate a value for such constructor (``FailFast`` tactic),
--- or alternatively we can try to match all the generated values of type ``T`` from both generators
--- using ``DecEq`` and leave only intersection (``DecEqConflicts`` tactic).
-
---export
---[FailFast] DeriveBodyRhsForCon where
---  consGenExpr sig con givs fuel = do
---    ?cons_body_obl_ff_rhs
-
---export
---[DecEqConflicts] DeriveBodyRhsForCon where
---  consGenExpr sig con givs fuel = do
---    ?cons_body_obl_deceq_rhs

src/Deriving/DepTyCheck/Gen/ForOneTypeConRhs/Interface.idr

@@ -10,7 +10,6 @@ import public Deriving.DepTyCheck.Gen.ForAllNeededTypes.Interface
 
 --- Interface ---
 
-public export
-interface DeriveBodyRhsForCon where
-  consGenExpr : DerivationClosure m => Elaboration m => NamesInfoInTypes =>
-                GenSignature -> (con : Con) -> (given : SortedSet $ Fin con.args.length) -> (fuel : TTImp) -> m TTImp
+export
+consGenExpr : DerivationClosure m => Elaboration m => NamesInfoInTypes =>
+              GenSignature -> (con : Con) -> (given : SortedSet $ Fin con.args.length) -> (fuel : TTImp) -> m TTImp