From 1189eab517402d8da48f3abb39b6273e8df6892d Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 25 Sep 2024 16:31:39 +0300 Subject: [PATCH 1/3] [ refactor ] Move arguments dependencies calculation function up & nicen --- src/Deriving/DepTyCheck/Util/Reflection.idr | 24 ++++++++++----------- 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr index 18e6fc7d..e4212aaa 100644 --- a/src/Deriving/DepTyCheck/Util/Reflection.idr +++ b/src/Deriving/DepTyCheck/Util/Reflection.idr @@ -389,6 +389,18 @@ export allVarNames : TTImp -> List Name allVarNames = SortedSet.toList . allVarNames' +public export +0 ArgDeps : Nat -> Type +ArgDeps n = DVect n $ SortedSet . Fin . Fin.finToNat + +export +argDeps : (args : List Arg) -> ArgDeps args.length +argDeps args = do + let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName arg, SortedSet.singleton i) + let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices) + flip upmapI args $ \i, deps => flip concatMap deps $ \candidates => + maybe empty singleton $ last' $ mapMaybe tryToFit $ SortedSet.toList candidates + export record NamesInfoInTypes where constructor Names @@ -612,15 +624,3 @@ genTypeName g = do let (IVar _ genTy, _) = unApp genTy | (genTy, _) => failAt (getFC genTy) "Expected a type name" pure genTy - ----------------------------------------------- ---- Analyzing dependently typed signatures --- ----------------------------------------------- - -export -argDeps : (args : List Arg) -> DVect args.length $ SortedSet . Fin . Fin.finToNat -argDeps args = do - let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName arg, SortedSet.singleton i) - let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices) - flip upmapI args $ \i, argDeps => flip concatMap argDeps $ \candidates => - maybe empty singleton $ last' $ mapMaybe tryToFit $ SortedSet.toList candidates From 6904a9ab1b2f79aab371504cfe3278441a80b4d8 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 25 Sep 2024 17:45:11 +0300 Subject: [PATCH 2/3] [ refactor, derive, perf ] Move `TypeApp` type out --- .../DepTyCheck/Gen/Core/ConsDerive.idr | 74 ++++++++++--------- 1 file changed, 38 insertions(+), 36 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 60914773..b2d1d999 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -13,6 +13,42 @@ import public Deriving.DepTyCheck.Gen.Derive %default total +data TypeApp : Con -> Type where + MkTypeApp : + (type : TypeInfo) -> + (0 _ : AllTyArgsNamed type) => + (argTypes : Vect type.args.length .| Either (Fin con.args.length) TTImp) -> + TypeApp con + +getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length $ TypeApp con +getTypeApps con = do + let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName arg, idx) + + -- Analyse that we can do subgeneration for each constructor argument + -- Fails using `Elaboration` if the given expression is not an application to a type constructor + let analyseTypeApp : TTImp -> m $ TypeApp con + analyseTypeApp expr = do + let (lhs, args) = unAppAny expr + ty <- case lhs of + IVar _ lhsName => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type` + | Just found => pure found + -- we didn't found, failing, there are at least two reasons + failAt (getFC lhs) $ if isNamespaced lhsName + then "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)" + else "Usupported applications to a non-concrete type `\{lhsName}`" + IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t + IType _ => pure typeInfoForTypeOfTypes + lhs@(IPi {}) => failAt (getFC lhs) "Fields with function types are not supported in constructors" + lhs => failAt (getFC lhs) "Unsupported type of a constructor field: \{show lhs}" + let Yes lengthCorrect = decEq ty.args.length args.length + | No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application" + _ <- ensureTyArgsNamed ty + pure $ MkTypeApp ty $ rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of + expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs + expr => Right expr + + for con.args.asVect $ analyseTypeApp . type + ------------------------------------------------- --- Derivation of a generator for constructor --- ------------------------------------------------- @@ -52,37 +88,11 @@ namespace NonObligatoryExts -- Prepare intermediate data and functions using this data -- ------------------------------------------------------------- - -- Get file position of the constructor definition (for better error reporting) - let conFC = getFC con.type - -- Build a map from constructor's argument name to its index let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName arg, idx) - -- Analyse that we can do subgeneration for each constructor argument - -- Fails using `Elaboration` if the given expression is not an application to a type constructor - let analyseTypeApp : TTImp -> m TypeApp - analyseTypeApp expr = do - let (lhs, args) = unAppAny expr - ty <- case lhs of - IVar _ lhsName => do let Nothing = lookupType lhsName -- TODO to support `lhsName` to be a type parameter of type `Type` - | Just found => pure found - -- we didn't found, failing, there are at least two reasons - failAt (getFC lhs) $ if isNamespaced lhsName - then "Data type `\{lhsName}` is unavailable at the site of derivation (forgotten import?)" - else "Usupported applications to a non-concrete type `\{lhsName}`" - IPrimVal _ (PrT t) => pure $ typeInfoForPrimType t - IType _ => pure typeInfoForTypeOfTypes - lhs@(IPi {}) => failAt (getFC lhs) "Fields with function types are not supported in constructors" - lhs => failAt (getFC lhs) "Unsupported type of a constructor field: \{show lhs}" - let Yes lengthCorrect = decEq ty.args.length args.length - | No _ => failAt (getFC lhs) "INTERNAL ERROR: wrong count of unapp when analysing type application" - _ <- ensureTyArgsNamed ty - pure $ MkTypeApp ty $ rewrite lengthCorrect in args.asVect <&> \arg => case getExpr arg of - expr@(IVar _ n) => mirror . maybeToEither expr $ lookup n conArgIdxs - expr => Right expr - -- Compute left-to-right need of generation when there are non-trivial types at the left - argsTypeApps <- for con.args.asVect $ analyseTypeApp . type + argsTypeApps <- getTypeApps con -- Get dependencies of constructor's arguments let rawDeps' = argDeps con.args @@ -107,7 +117,7 @@ namespace NonObligatoryExts genForOrder order = map (foldr apply callCons) $ evalStateT givs $ for order $ \genedArg => do -- Get info for the `genedArg` - let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ TypeApp) argsTypeApps + let MkTypeApp typeOfGened argsOfTypeOfGened = index genedArg $ the (Vect _ $ TypeApp con) argsTypeApps -- Acquire the set of arguments that are already present presentArguments <- get @@ -218,14 +228,6 @@ namespace NonObligatoryExts Foldable f => Interpolation (f $ Fin con.args.length) where interpolate = ("[" ++) . (++ "]") . joinBy ", " . map interpolate . toList - -- TODO make this to be a `record` as soon as #2177 is fixed - data TypeApp : Type where - MkTypeApp : - (type : TypeInfo) -> - (0 _ : AllTyArgsNamed type) => - (argTypes : Vect type.args.length .| Either (Fin con.args.length) TTImp) -> - TypeApp - ||| 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. From 56b6a43c7b7ec030d4ca7425bea2ccb4ddf6a453 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 25 Sep 2024 18:58:44 +0300 Subject: [PATCH 3/3] [ refactor ] Make `TypeApp` to be `record` --- src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index b2d1d999..fc2f8b4d 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -13,12 +13,11 @@ import public Deriving.DepTyCheck.Gen.Derive %default total -data TypeApp : Con -> Type where - MkTypeApp : - (type : TypeInfo) -> - (0 _ : AllTyArgsNamed type) => - (argTypes : Vect type.args.length .| Either (Fin con.args.length) TTImp) -> - TypeApp con +record TypeApp (0 con : Con) where + constructor MkTypeApp + argHeadType : TypeInfo + {auto 0 argHeadTypeGood : AllTyArgsNamed argHeadType} + argApps : Vect argHeadType.args.length .| Either (Fin con.args.length) TTImp getTypeApps : Elaboration m => NamesInfoInTypes => (con : Con) -> m $ Vect con.args.length $ TypeApp con getTypeApps con = do @@ -171,14 +170,14 @@ namespace NonObligatoryExts ------------------------------------------------- -- Determine which arguments need to be generated in a left-to-right manner - let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\((MkTypeApp _ as), _) => any isRight as) $ toListI argsTypeApps + let (leftToRightArgsTypeApp, leftToRightArgs) = unzip $ filter (\(ta, _) => any isRight ta.argApps) $ toListI argsTypeApps -------------------------------------------------------------------------------- -- Preparation of input for the left-to-right phase (1st right-to-left phase) -- -------------------------------------------------------------------------------- -- Acquire those variables that appear in non-trivial type expressions, i.e. those which needs to be generated before the left-to-right phase - let preLTR = leftToRightArgsTypeApp >>= \(MkTypeApp _ as) => rights (toList as) >>= allVarNames + let preLTR = leftToRightArgsTypeApp >>= \ta => rights (toList ta.argApps) >>= allVarNames let preLTR = SortedSet.fromList $ mapMaybe (lookup' conArgIdxs) preLTR -- Find rightmost arguments among `preLTR`