From 16731708a6e7f02c3d4e2ba7b64f1a497ad95fff Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Mon, 16 Sep 2024 17:52:51 +0300 Subject: [PATCH] [ refactor ] Remove useless intermediate function --- .../DepTyCheck/Gen/Core/ConsDerive.idr | 84 +++++++++---------- 1 file changed, 39 insertions(+), 45 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index f39959e2..d9cbac54 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -98,64 +98,58 @@ namespace NonObligatoryExts -- Derive constructor calling expression for given order of generation let genForOrder : List (Fin con.args.length) -> m TTImp - genForOrder order = foldr apply callCons <$> evalStateT givs (for order genForOneArg) where + -- ... state is the set of arguments that are already present (given or generated) + genForOrder order = map (foldr apply callCons) $ evalStateT givs $ for order $ \genedArg => do - -- ... state is the set of arguments that are already present (given or generated) - genForOneArg : forall m. - CanonicGen m => - MonadState (SortedSet $ Fin con.args.length) m => - (gened : Fin con.args.length) -> m $ TTImp -> TTImp - genForOneArg genedArg = do + -- Get info for the `genedArg` + let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ TypeApp) argsTypeApps - -- Get info for the `genedArg` - let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ TypeApp) argsTypeApps + -- Acquire the set of arguments that are already present + presentArguments <- get - -- Acquire the set of arguments that are already present - presentArguments <- get + -- TODO to put the following check as up as possible as soon as it typecheks O_O + -- Check that those argument that we need to generate is not already present + let False = contains genedArg presentArguments + | True => pure id - -- TODO to put the following check as up as possible as soon as it typecheks O_O - -- Check that those argument that we need to generate is not already present - let False = contains genedArg presentArguments - | True => pure id + -- Filter arguments classification according to the set of arguments that are left to be generated; + -- Those which are `Right` are given, those which are `Left` are needs to be generated. + let depArgs : Vect typeOfGened.args.length (Either (Fin con.args.length) TTImp) := argsOfTypeOfGened <&> \case + Right expr => Right expr + Left i => if contains i presentArguments then Right $ var $ argName $ index' con.args i else Left i - -- Filter arguments classification according to the set of arguments that are left to be generated; - -- Those which are `Right` are given, those which are `Left` are needs to be generated. - let depArgs : Vect typeOfGened.args.length (Either (Fin con.args.length) TTImp) := argsOfTypeOfGened <&> \case - Right expr => Right expr - Left i => if contains i presentArguments then Right $ var $ argName $ index' con.args i else Left i + -- Determine which arguments will be on the left of dpair in subgen call, in correct order + let subgeneratedArgs = mapMaybe getLeft $ toList depArgs - -- Determine which arguments will be on the left of dpair in subgen call, in correct order - let subgeneratedArgs = mapMaybe getLeft $ toList depArgs + -- Make sure generated arguments will not be generated again + modify $ insert genedArg . union (fromList subgeneratedArgs) - -- Make sure generated arguments will not be generated again - modify $ insert genedArg . union (fromList subgeneratedArgs) + -- Form a task for subgen + let (subgivensLength ** subgivens) = mapMaybe (\(ie, idx) => (idx,) <$> getRight ie) $ depArgs `zip` Fin.range + let subsig : GenSignature := MkGenSignature typeOfGened $ fromList $ fst <$> toList subgivens + let Yes Refl = decEq subsig.givenParams.size subgivensLength + | No _ => fail "INTERNAL ERROR: error in given params set length computation" - -- Form a task for subgen - let (subgivensLength ** subgivens) = mapMaybe (\(ie, idx) => (idx,) <$> getRight ie) $ depArgs `zip` Fin.range - let subsig : GenSignature := MkGenSignature typeOfGened $ fromList $ fst <$> toList subgivens - let Yes Refl = decEq subsig.givenParams.size subgivensLength - | No _ => fail "INTERNAL ERROR: error in given params set length computation" + -- Check if called subgenerator can call the current one + let mutRec = hasNameInsideDeep sig.targetType.name $ var subsig.targetType.name - -- Check if called subgenerator can call the current one - let mutRec = hasNameInsideDeep sig.targetType.name $ var subsig.targetType.name + -- Decide whether to use local (decreasing) or outmost fuel, depending on whether we are in mutual recursion with subgen + let subfuel = if mutRec then fuel else var outmostFuelArg - -- Decide whether to use local (decreasing) or outmost fuel, depending on whether we are in mutual recursion with subgen - let subfuel = if mutRec then fuel else var outmostFuelArg + -- Form an expression to call the subgen + subgenCall <- callGen subsig subfuel $ snd <$> subgivens - -- Form an expression to call the subgen - subgenCall <- callGen subsig subfuel $ snd <$> subgivens + -- Form an expression of binding the result of subgen + let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . flip Vect.index bindNames + let bindSubgenResult = foldr (\l, r => var `{Builtin.DPair.MkDPair} .$ l .$ r) genedArg subgeneratedArgs - -- Form an expression of binding the result of subgen - let genedArg:::subgeneratedArgs = genedArg:::subgeneratedArgs <&> bindVar . flip Vect.index bindNames - let bindSubgenResult = foldr (\l, r => var `{Builtin.DPair.MkDPair} .$ l .$ r) genedArg subgeneratedArgs + -- Form an expression of the RHS of a bind; simplify lambda if subgeneration result type does not require pattern matching + let bindRHS = \cont => case bindSubgenResult of + IBindVar _ n => lam (MkArg MW ExplicitArg (Just $ UN $ Basic n) implicitFalse) cont + _ => `(\ ~bindSubgenResult => ~cont) - -- Form an expression of the RHS of a bind; simplify lambda if subgeneration result type does not require pattern matching - let bindRHS = \cont => case bindSubgenResult of - IBindVar _ n => lam (MkArg MW ExplicitArg (Just $ UN $ Basic n) implicitFalse) cont - _ => `(\ ~bindSubgenResult => ~cont) - - -- Chain the subgen call with a given continuation - pure $ \cont => `(~subgenCall >>= ~(bindRHS cont)) + -- Chain the subgen call with a given continuation + pure $ \cont => `(~subgenCall >>= ~(bindRHS cont)) -- Get dependencies of constructor's arguments let rawDeps = argDeps con.args