11||| A bridge between a single act of derivation (for a single type) and a user derivation task
22module Deriving.DepTyCheck.Gen.ForAllNeededTypes.Impl
33
4- import public Control . Monad . Either
5- import public Control . Monad . Reader
64import public Control . Monad . State
7- import public Control . Monad . State . Tuple
8- import public Control . Monad . Writer
9- import public Control . Monad . RWS
105
116import public Data . DPair
12- import public Data . List . Map
7+ import public Data . List . Set
138import public Data . SortedMap
14- import public Data . SortedMap . Extra
15- import public Data . SortedSet
169
1710import public Decidable . Equality
1811
@@ -24,9 +17,8 @@ import public Deriving.DepTyCheck.Gen.ForOneType.Interface
2417
2518ClosuringContext : (Type -> Type ) -> Type
2619ClosuringContext m =
27- ( MonadState (ListMap GenSignature Name ) m -- gens already asked to be derived
28- , MonadState (List (GenSignature , Name ), List (GenSignature , Name )) m -- two queues of gens to be derived, one for known types, one the unknown ones
29- , MonadState (SortedSet TypeInfo ) m -- type names that were asked for deriving their weighting function
20+ ( ListSet GenSignature -- gens already asked to be derived
21+ , MonadState (ListSet GenSignature , ListSet GenSignature ) m -- two queues of gens to be derived, one for known types, one the unknown ones
3022 )
3123
3224nameForGen : GenSignature -> Name
@@ -41,32 +33,31 @@ lookupLengthChecked intSig m = lookup intSig m >>= \(extSig, name) => (name,) <$
4133 Yes prf => Just $ Element extSig prf
4234 No _ => Nothing
4335
44- deriveAll : NamesInfoInTypes => ConsRecs => DeriveBodyForType => DerivationClosure m => ClosuringContext m => Elaboration m =>
45- List (Decl, Decl) -> m $ List (Decl, Decl)
46- deriveAll acc = do
47- (toDeriveKnown, toDeriveUnknown) <- get {stateType= (List _ , List _ )}
48- put ([] , toDeriveUnknown)
49- derived <- ( ++ acc) <$> for toDeriveKnown deriveOne
36+ deriveAll : NamesInfoInTypes => ConsRecs => (cc : ClosuringContext m ) => DeriveBodyForType => DerivationClosure m => Elaboration m =>
37+ ListSet TypeInfo -> List (Decl, Decl) -> m (ListSet TypeInfo, List (Decl, Decl) )
38+ deriveAll weightFunTys decls {cc = (alreadyDerived, _ )} = do
39+ (toDeriveKnown, toDeriveUnknown) <- mapHom (( `difference` alreadyDerived) . normalise) <$> get {stateType= (ListSet _ , ListSet _ )}
40+ put (empty , toDeriveUnknown)
41+ (weightFunTys, decls) <- bimap ( foldl insert' weightFunTys . join) (decls ++ ) . unzip <$> for (toList toDeriveKnown) deriveOne
5042 if not $ null toDeriveKnown
51- then assert_total deriveAll derived
43+ then assert_total $ deriveAll {cc = (alreadyDerived `union` toDeriveKnown, % search)} weightFunTys decls
5244 else if null toDeriveUnknown
53- then pure derived
45+ then pure (weightFunTys, decls)
5446 else do
55- (niit, cr) <- updateNamesAndConsRecs $ targetType . fst <$> toDeriveUnknown
56- put (toDeriveUnknown, [] )
57- assert_total $ deriveAll @{niit} @{cr} derived
47+ (niit, cr) <- updateNamesAndConsRecs $ targetType <$> toList toDeriveUnknown
48+ put (toDeriveUnknown, empty )
49+ assert_total $ deriveAll @{niit} @{cr} {cc = (alreadyDerived `union` toDeriveUnknown, % search)} weightFunTys decls
5850 where
59- deriveOne : (GenSignature, Name) -> m (Decl, Decl)
60- deriveOne (sig, name) = do
51+ deriveOne : GenSignature -> m (List TypeInfo, Decl, Decl)
52+ deriveOne sig = do
53+ let name = nameForGen sig
6154 -- derive declaration and body for the asked signature. It's important to call it AFTER update of the map in the state to not to cycle
6255 let genFunClaim = export' name $ canonicSig sig
63- genFunBody <- logBounds Info " deptycheck.derive.type" $ def name <$> canonicBody sig name
64- pure (genFunClaim, genFunBody)
56+ (tyWithWeightFuns, genFunBody) <- logBounds Info " deptycheck.derive.type" $ canonicBody sig name
57+ pure (tyWithWeightFuns, genFunClaim, def name genFunBody)
6558
6659DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignature (ExternalGenSignature , Name ) => DerivationClosure m where
6760
68- needWeightFun = modify . SortedSet . insert
69-
7061 callGen sig fuel values = do
7162
7263 -- look for external gens, and call it if exists
@@ -75,28 +66,15 @@ DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignatu
7566 logValue Details " deptycheck.derive.closuring.external" " is used as an external generator" $
7667 (callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values, Just (_ ** extSig. gendOrder))
7768
78- -- get the expression of calling the internal gen, derive if necessary
79- internalGenCall <- do
80-
81- -- look for existing (already derived) internals, use it if exists
82- let Nothing = List . Map . lookup sig ! get
83- | Just name => pure $ callCanonic sig name fuel values
84-
85- -- nothing found, then derive! acquire the name
86- let name = nameForGen sig
87-
88- -- remember that we're responsible for this signature derivation
89- modify $ List . Map . insert sig name
69+ -- put to derivation queue if necessary
70+ when (not $ List . Set . contains sig % search) $ do
9071
9172 -- remember the task to derive
92- modify {stateType= (List _ , List _ )} $ if isTypeKnown sig. targetType then mapFst $ (:: ) (sig, name) else mapSnd $ (:: ) (sig, name)
93-
94- -- return the name of the newly derived generator
95- pure $ callCanonic sig name fuel values
73+ modify $ if isTypeKnown sig. targetType then mapFst $ normalise . List . Set . insert sig else mapSnd $ normalise . List . Set . insert sig
9674
9775 -- call the internal gen
9876 logValue DetailedDebug " deptycheck.derive.closuring.internal" " is used as an internal generator"
99- (internalGenCall , Nothing )
77+ (callCanonic sig (nameForGen sig) fuel values , Nothing )
10078
10179-- - Canonic-dischagring function ---
10280
@@ -106,7 +84,7 @@ declName : Decl -> String
10684declName $ IClaim $ MkFCVal _ $ MkIClaimData {type = MkTy {ty, _ }, _ } = show ty
10785declName $ IData _ _ _ $ MkData {n, _ } = show n
10886declName $ IData _ _ _ $ MkLater {n, _ } = show n
109- declName $ IDef fc nm cls = ? declName_rhs_2
87+ declName $ IDef _ nm _ = show nm
11088declName $ IParameters _ _ [] = " P"
11189declName $ IParameters _ _ (d:: _ ) = declName d
11290declName $ IRecord _ _ _ _ $ MkRecord {n, _ } = show n
@@ -121,10 +99,10 @@ runCanonic : DeriveBodyForType => NamesInfoInTypes => ConsRecs =>
12199 SortedMap ExternalGenSignature Name -> (forall m. DerivationClosure m => m a) -> Elab (a, List Decl)
122100runCanonic exts calc = do
123101 let exts = SortedMap . fromList $ exts. asList <&> \ namedSig => (fst $ internalise $ fst namedSig, namedSig)
124- (( _ , _ , weightingFuns), (x, derived)) <- runStateT
125- (empty, ( empty, empty), empty @{ TypeInfoOrdByName } )
126- [| (calc, deriveAll []) | ]
127- {stateType= (ListMap GenSignature Name , ( List ( GenSignature , Name ), List ( GenSignature , Name )), SortedSet TypeInfo )}
102+ (x, weightingFuns, derived) <- evalStateT
103+ (empty, empty)
104+ [| (calc, deriveAll (empty @{ TypeInfoEqByName }) []) | ]
105+ {stateType= (ListSet GenSignature , ListSet GenSignature )}
128106 {m= Elab }
129107 let derived = sortBy (compare `on` declName . fst ) $ derived ++ mapMaybe deriveWeightingFun (Prelude . toList weightingFuns)
130108 let (defs, bodies) = unzip derived
0 commit comments