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