0 | ||| Derivation of the outer layer of a constructor-generating function, performing GADT indices check of given arguments.
  1 | module Deriving.DepTyCheck.Gen.ForOneTypeCon.Impl
  2 |
  3 | import public Control.Monad.Error.Either
  4 | import public Control.Monad.State
  5 | import public Control.Monad.State.Tuple
  6 | import public Control.Monad.Writer
  7 |
  8 | import public Deriving.DepTyCheck.Gen.ForOneTypeConRhs.Interface
  9 | import public Deriving.DepTyCheck.Util.DeepConsApp
 10 |
 11 | %default total
 12 |
 13 | -------------------------------------------------
 14 | --- Derivation of a generator for constructor ---
 15 | -------------------------------------------------
 16 |
 17 | isSimpleBindVar : TTImp -> Bool
 18 | isSimpleBindVar $ IBindVar {} = True
 19 | isSimpleBindVar _             = False
 20 |
 21 | export
 22 | canonicConsBody : DeriveBodyRhsForCon => DerivationClosure m => Elaboration m => NamesInfoInTypes => ConsRecs =>
 23 |                   GenSignature -> Name -> Con -> m $ List Clause
 24 | canonicConsBody sig name con = do
 25 |
 26 |   -- Get file position of the constructor definition (for better error reporting)
 27 |   let conFC = getFC con.type
 28 |
 29 |   -- Normalise the types in constructor; expand functions that are used as types, if possible
 30 |   con <- normaliseCon con
 31 |
 32 |   -- Acquire constructor's return type arguments
 33 |   let (conRetTy, conRetTypeArgs) = unAppAny con.type
 34 |   let conRetTypeArgs = conRetTypeArgs <&> getExpr
 35 |
 36 |   -- Match lengths of `conRetTypeArgs` and `sig.targetType.args`
 37 |   let Yes conRetTypeArgsLengthCorrect = conRetTypeArgs.length `decEq` sig.targetType.args.length
 38 |     | No _ => failAt conFC "INTERNAL ERROR: length of the return type does not equal to the type's arguments count"
 39 |
 40 |   let conRetTypeArg : Fin sig.targetType.args.length -> TTImp
 41 |       conRetTypeArg idx = index' conRetTypeArgs $ rewrite conRetTypeArgsLengthCorrect in idx
 42 |
 43 |   -- Determine names of the arguments of the constructor (as a function)
 44 |   let conArgNames = fromList $ argName' <$> con.args
 45 |
 46 |   -- Determine which arguments are already determined by types of givens
 47 |   let depOfGivs = dependeesOfGivens sig
 48 |
 49 |   -- For given arguments, determine whether they are
 50 |   --   - just a free name
 51 |   --   - repeated name of another given parameter (need for `decEq`)
 52 |   --   - (maybe, deeply) constructor call (need to match)
 53 |   --   - a function call to a determined arg (can be calculated, thus need for `decEq`)
 54 |   --   - a function call on a free param (thus, need to use "inverted function" filtering trick; not supported now)
 55 |   --   - something else (cannot manage yet, unless it is fully determined by other given arguments)
 56 |   deepConsApps : Vect _ $ DeepConsAnalysisRes True <- for sig.givenParams.asVect $ \idx => do
 57 |     let argExpr = conRetTypeArg idx
 58 |     let (fns, errs) = runWriter {w=List String} $ analyseDeepConsApp True conArgNames argExpr
 59 |     when (not $ null errs) $ failAt conFC $
 60 |       "Argument #\{show idx} of \{show con.name} with given type arguments [\{showGivens sig}] is not supported, " ++
 61 |       "argument expression: \{show argExpr}, reason(s): \{joinBy "; " errs}"
 62 |     -- Clean up `MustDecEqWith`s if this argument is determined by givens' types
 63 |     pure $ if not $ contains idx depOfGivs then fns else case fns of
 64 |       (lst ** f) => (map determineMustDecEqs <$> lst ** rewrite lengthMap {f=map determineMustDecEqs} lst in f)
 65 |   let allAppliedFreeNames = foldMap (SortedSet.fromList . map fst . fst) deepConsApps
 66 |   let badDecEqExpr : ConsDetermInfo -> Maybe TTImp
 67 |       badDecEqExpr (MustDecEqWith e) = whenT (not $ null $ (allVarNames' e `intersection` conArgNames) `difference` allAppliedFreeNames) e
 68 |       badDecEqExpr _                 = Nothing
 69 |   for_ deepConsApps $ \(vs ** _) => whenJust (foldAlt' vs $ badDecEqExpr . snd) $ \e => failAt conFC $
 70 |     "Unsupported constructor \{show con.name} with given type arguments [\{showGivens sig}] since it contains " ++
 71 |     "an undetermined non-constructor expression `\{show e}` as a given"
 72 |
 73 |   -- Acquire LHS bind expressions for the given parameters
 74 |   -- Determine pairs of names which should be `decEq`'ed
 75 |   let getAndInc : forall m. MonadState Nat m => m Nat
 76 |       getAndInc = get <* modify S
 77 |   let deceqedName : forall m. MonadState Nat m => Name -> m Name
 78 |       -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend
 79 |       deceqedName name = pure $ UN $ Basic $ "to_be_deceqed^^" ++ show name ++ show !getAndInc
 80 |   ((givenConArgs, decEqedNames, _), bindExprs) <-
 81 |     runStateT (empty, [], 0) {stateType=(SortedSet Name, List (Either TTImp Name, Name), Nat)} {m} $
 82 |       for deepConsApps $ \(appliedNames ** bindExprF) => do
 83 |         renamedAppliedNames <- for appliedNames.asVect $ \(name, typeDetermined) =>
 84 |           case typeDetermined of
 85 |             DeterminedByType => pure $ const implicitTrue -- no need to match type-determined parameter by hand
 86 |             NotDeterminedByType => if SortedSet.contains name !get
 87 |               then do
 88 |                 substName <- deceqedName name
 89 |                 modify $ (::) (Right name, substName)
 90 |                 pure $ \alreadyMatchedRenames => bindVar $ if contains substName alreadyMatchedRenames then name else substName
 91 |               else modify (SortedSet.insert name) $> const (bindVar name)
 92 |             MustDecEqWith e => do
 93 |               substName <- deceqedName name
 94 |               modify $ (::) (Left e, substName)
 95 |               pure $ \alreadyMatchedRenames => if contains substName alreadyMatchedRenames then {- e -} implicitTrue else bindVar substName
 96 |         let _ : Vect appliedNames.length $ SortedSet Name -> TTImp = renamedAppliedNames
 97 |         pure $ \alreadyMatchedRenames => bindExprF $ \idx => index idx renamedAppliedNames $ alreadyMatchedRenames
 98 |   let bindExprs = \alreadyMatchedRenames => bindExprs <&> \f => f alreadyMatchedRenames
 99 |
100 |   -- Build a map from constructor's argument name to its index
101 |   let conArgIdxs = SortedMap.fromList $ mapI con.args $ \idx, arg => (argName' arg, idx)
102 |
103 |   -- Determine indices of constructor's arguments that are given
104 |   givenConArgs <- for givenConArgs.asList $ \givenArgName => do
105 |     let Just idx = lookup givenArgName conArgIdxs
106 |       | Nothing => failAt conFC "INTERNAL ERROR: calculated given `\{show givenArgName}` is not found in an arguments list of the constructor"
107 |     pure idx
108 |
109 |   -- Equalise index values which must be propositionally equal to some parameters
110 |   -- NOTE: Here I do all `decEq`s in a row and then match them all against `Yes`.
111 |   --       I could do this step by step and this could be more effective in large series.
112 |   let deceqise : (lhs : Vect sig.givenParams.asList.length TTImp -> TTImp) -> (rhs : TTImp) -> Clause
113 |       deceqise lhs rhs = step lhs empty $ orderLikeInCon decEqedNames where
114 |
115 |         step : (withlhs : Vect sig.givenParams.asList.length TTImp -> TTImp) ->
116 |                (alreadyMatchedRenames : SortedSet Name) ->
117 |                (left : List (Either TTImp Name, Name)) ->
118 |                Clause
119 |         step withlhs matched [] = PatClause EmptyFC .| withlhs (bindExprs matched) .| rhs
120 |         step withlhs matched ((orig, renam)::rest) =
121 |           WithClause EmptyFC (withlhs $ bindExprs matched) MW
122 |             `(Decidable.Equality.decEq ~(var renam) ~(either id var orig))
123 |             Nothing []
124 |             [ -- happy case
125 |               step ((.$ `(Prelude.Yes Builtin.Refl)) . withlhs) (insert renam matched) rest
126 |             , -- empty case
127 |               PatClause EmptyFC .| withlhs (bindExprs matched) .$ `(Prelude.No _) .| `(empty)
128 |             ]
129 |
130 |         -- Order pairs by the first element like they are present in the constructor's signature
131 |         orderLikeInCon : Foldable f => f (Either TTImp Name, Name) -> List (Either TTImp Name, Name)
132 |         orderLikeInCon = do
133 |           let conArgNames = mapMaybe Arg.name con.args
134 |           let conNameToIdx : SortedMap _ $ Fin conArgNames.length := fromList $ mapI conArgNames $ flip (,)
135 |           let [AsInCon] Ord (Either TTImp Name, Name) where
136 |                 compare (Left _, _) (Right _, _) = LT
137 |                 compare (Right _, _) (Left _, _) = GT
138 |                 compare (Right origL, renL) (Right origR, renR) = comparing (lookup' conNameToIdx) origL origR <+> compare renL renR
139 |                 compare (Left _, renL) (Left _, renR) = compare renL renR
140 |           Prelude.toList . foldl SortedSet.insert' (empty @{AsInCon})
141 |
142 |   -- Form the declaration cases of a function generating values of particular constructor
143 |   let fuelArg = "^cons_fuel^" -- I'm using a name containing chars that cannot be present in the code parsed from the Idris frontend
144 |   pure $
145 |     -- Happy case, given arguments conform out constructor's GADT indices
146 |     [ deceqise (callCanonic sig name $ bindVar fuelArg) !(consGenExpr sig con .| fromList givenConArgs .| var fuelArg) ]
147 |     ++ if all isSimpleBindVar $ bindExprs SortedSet.empty then [] {- do not produce dead code if the happy case handles everything already -} else
148 |       -- The rest case, if given arguments do not conform to the current constructor then return empty generator
149 |       [ callCanonic sig name implicitTrue (replicate _ implicitTrue) .= `(empty) ]
150 |