0 | ||| A bridge between a single act of derivation (for a single type) and a user derivation task
  1 | module Deriving.DepTyCheck.Gen.ForAllNeededTypes.Impl
  2 |
  3 | import public Control.Monad.State
  4 |
  5 | import public Data.DPair
  6 | import public Data.List.Ex
  7 | import public Data.List.Map
  8 | import public Data.List.Set
  9 | import public Data.SortedMap
 10 |
 11 | import public Decidable.Equality
 12 |
 13 | import public Deriving.DepTyCheck.Gen.ForOneType.Interface
 14 |
 15 | import public Deriving.DepTyCheck.Util.Specialisation
 16 |
 17 | %default total
 18 |
 19 | --- Particular implementations producing the-core-derivation-function closure ---
 20 |
 21 | ClosuringContext : (Type -> Type) -> Type
 22 | ClosuringContext m =
 23 |   ( ListSet GenSignature                                                 -- gens already asked to be derived
 24 |   , MonadState  (ListSet GenSignature, ListSet GenSignature) m           -- two queues of gens to be derived, one for known types, one the unknown ones
 25 |   )
 26 |
 27 | nameForGen : GenSignature -> Name
 28 | nameForGen sig = let (ty, givs) = characteristics sig in UN $ Basic $ "<\{ty}>\{show givs}"
 29 | -- I'm using `UN` but containing chars that cannot be present in the code parsed from the Idris frontend.
 30 |
 31 | -- Instead of staticaly ensuring that map holds only correct values, we check dynamically, because it's hard to go through `==`-based lookup of maps.
 32 | lookupLengthChecked : (intSig : GenSignature) -> SortedMap GenSignature (ExternalGenSignature, Name) ->
 33 |                       Maybe (Name, Subset ExternalGenSignature $ \extSig => extSig.givenParams.size = intSig.givenParams.size)
 34 | lookupLengthChecked intSig m = lookup intSig m >>= \(extSig, name) => (name,) <$>
 35 |                                  case decEq extSig.givenParams.size intSig.givenParams.size of
 36 |                                     Yes prf => Just $ Element extSig prf
 37 |                                     No _    => Nothing
 38 |
 39 | deriveAll : NamesInfoInTypes => ConsRecs => (cc : ClosuringContext m) => DeriveBodyForType => DerivationClosure m => Elaboration m =>
 40 |             ListSet TypeInfo -> List (Decl, Decl) -> m (ListSet TypeInfo, List (Decl, Decl))
 41 | deriveAll weightFunTys decls {cc=(alreadyDerived, _)}= do
 42 |   (toDeriveKnown, toDeriveUnknown) <- mapHom ((`difference` alreadyDerived) . normalise) <$> get {stateType=(ListSet _, ListSet _)}
 43 |   put (empty, toDeriveUnknown)
 44 |   (weightFunTys, decls) <- bimap (foldl insert' weightFunTys . join) (decls ++) . unzip <$> for (toList toDeriveKnown) deriveOne
 45 |   if not $ null toDeriveKnown
 46 |     then assert_total $ deriveAll {cc=(alreadyDerived `union` toDeriveKnown, %search)} weightFunTys decls
 47 |     else if null toDeriveUnknown
 48 |       then pure (weightFunTys, decls)
 49 |       else do
 50 |         (niit, cr) <- updateNamesAndConsRecs $ targetType <$> toList toDeriveUnknown
 51 |         put (toDeriveUnknown, empty)
 52 |         assert_total $ deriveAll @{niit} @{cr} {cc=(alreadyDerived, %search)} weightFunTys decls
 53 |   where
 54 |     deriveOne : GenSignature -> m (List TypeInfo, Decl, Decl)
 55 |     deriveOne sig = do
 56 |       let name = nameForGen sig
 57 |       -- 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
 58 |       let genFunClaim = export' name $ canonicSig sig
 59 |       (tyWithWeightFuns, genFunBody) <- logBounds Info "deptycheck.derive.type" [sig] $ canonicBody sig name
 60 |       pure (tyWithWeightFuns, genFunClaim, def name genFunBody)
 61 |
 62 | DeriveBodyForType => ClosuringContext m => Elaboration m => SortedMap GenSignature (ExternalGenSignature, Name) => DerivationClosure m where
 63 |
 64 |   callGen sig fuel values = do
 65 |
 66 |     -- look for external gens, and call it if exists
 67 |     let Nothing = lookupLengthChecked sig %search
 68 |       | Just (name, Element extSig lenEq) =>
 69 |           logValue Details "deptycheck.derive.closuring.external" [sig] "is used as an external generator" $
 70 |             (callExternalGen extSig name (var outmostFuelArg) $ rewrite lenEq in values, Just (_ ** extSig.gendOrder))
 71 |
 72 |     -- check if internal generator asked for is for a primitive type
 73 |     when (isTypeInfoPrim sig.targetType) $
 74 |       fail "Cannot derive generator for the primitive type \{show $ extractTargetTyExpr sig.targetType}, use external instead"
 75 |     -- the monadic bind is used due to over-normalisation during elaborator script execution causing bad derivator performance otherwise
 76 |     notfound <- pure $ id $ not $ List.Set.contains sig %search
 77 |
 78 |     --       The braces here ↓ are so that the compiler doesn't confuse this with a with application
 79 |     Nothing : Maybe TTImp <- (if notfound then assert_total specialiseIfNeeded sig fuel values else pure Nothing)
 80 |       | Just me => pure (me, Nothing)
 81 |
 82 |     -- remember the task to derive, if necessary
 83 |     when notfound $ do
 84 |       modify $ if isTypeKnown sig.targetType then mapFst $ normalise . List.Set.insert sig else mapSnd $ normalise . List.Set.insert sig
 85 |
 86 |     -- call the internal gen
 87 |     logValue DetailedDebug "deptycheck.derive.closuring.internal" [sig] "is used as an internal generator"
 88 |       (callCanonic sig (nameForGen sig) fuel values, Nothing)
 89 |
 90 | --- Canonic-dischagring function ---
 91 |
 92 | %hide Data.Vect.Dependent.(<*>)
 93 |
 94 | declName : Decl -> String
 95 | declName $ IClaim $ MkFCVal _ $ MkIClaimData {type = MkTy {ty, _}, _} = show ty
 96 | declName $ IData _ _ _ $ MkData  {n, _} = show n
 97 | declName $ IData _ _ _ $ MkLater {n, _} = show n
 98 | declName $ IDef _ nm _ = show nm
 99 | declName $ IParameters _ _ [] = "P"
100 | declName $ IParameters _ _ (d::_) = declName d
101 | declName $ IRecord _ _ _ _ $ MkRecord {n, _} = show n
102 | declName $ INamespace _ (MkNS ns) _ = joinBy "." $ reverse ns
103 | declName $ ITransform _ nm _ _ = show nm
104 | declName $ IRunElabDecl {} = "Z"
105 | declName $ ILog {} = "Z"
106 | declName $ IBuiltin _ _ nm = show nm
107 |
108 | export
109 | runCanonic : DeriveBodyForType => NamesInfoInTypes => ConsRecs =>
110 |              SortedMap ExternalGenSignature Name -> (forall m. DerivationClosure m => m a) -> Elab (a, List Decl)
111 | runCanonic exts calc = do
112 |   let exts = SortedMap.fromList $ exts.asList <&> \namedSig => (fst $ internalise $ fst namedSig, namedSig)
113 |   (x, weightingFuns, derived) <- evalStateT
114 |                          (empty, empty)
115 |                          [| (calc, deriveAll (empty @{TypeInfoEqByName}) []) |]
116 |                          {stateType=(ListSet GenSignature, ListSet GenSignature)}
117 |                          {m=Elab}
118 |   let derived = sortBy (compare `on` declName . fst) $ derived ++ mapMaybe deriveWeightingFun (Prelude.toList weightingFuns)
119 |   let (defs, bodies) = unzip derived
120 |   pure (x, defs ++ bodies)
121 |