0 | module Deriving.DepTyCheck.Gen.Signature
  1 |
  2 | import public Data.DPair
  3 | import public Data.Fin
  4 | import public Data.List.Ex
  5 | import public Data.SortedMap
  6 | import public Data.SortedMap.Dependent
  7 | import public Data.SortedMap.Extra
  8 | import public Data.SortedSet
  9 |
 10 | import public Deriving.DepTyCheck.Util.ArgsPerm
 11 | import public Deriving.DepTyCheck.Util.Primitives
 12 |
 13 | import public Language.Reflection.Compat
 14 | import public Language.Reflection.Expr
 15 | import public Language.Reflection.Logging
 16 |
 17 | %default total
 18 |
 19 | ------------------------------------------------------------
 20 | --- Simplest `Gen` signature, user for internal requests ---
 21 | ------------------------------------------------------------
 22 |
 23 | public export
 24 | record GenSignature where
 25 |   constructor MkGenSignature
 26 |   targetType : TypeInfo
 27 |   {auto 0 targetTypeCorrect : AllTyArgsNamed targetType}
 28 |   givenParams : SortedSet $ Fin targetType.args.length
 29 |
 30 | namespace GenSignature
 31 |
 32 |   export
 33 |   characteristics : GenSignature -> (String, List Nat)
 34 |   characteristics $ MkGenSignature ty giv = (show ty.name, toNatList giv)
 35 |
 36 |   export
 37 |   showGivens : GenSignature -> String
 38 |   showGivens sig = joinBy ", " $ do
 39 |     let uName : Arg -> Maybe UserName
 40 |         uName $ MkArg {name=Just $ UN un, _} = Just un
 41 |         uName _ = Nothing
 42 |     sig.givenParams.asList <&> \idx => maybe (show idx) (\n => "\{show idx}(\{show n})") $ uName $ index' sig.targetType.args idx
 43 |
 44 | public export %inline
 45 | (.generatedParams) : (sig : GenSignature) -> SortedSet $ Fin sig.targetType.args.length
 46 | sig.generatedParams = fromList (allFins sig.targetType.args.length) `difference` sig.givenParams
 47 |
 48 | export
 49 | LogPosition GenSignature where logPosition sig = "\{show $ extractTargetTyExpr sig.targetType}[\{showGivens sig}]"
 50 |
 51 | public export
 52 | Eq GenSignature where (==) = (==) `on` characteristics
 53 |
 54 | public export
 55 | Ord GenSignature where compare = comparing characteristics
 56 |
 57 | ||| Set of type arguments for which there exists a given argument depending on it
 58 | -- This is very similar to `dependees` function from libs, but is takes into account the difference between given and non-given arguments.
 59 | -- Maybe, that function should be generalised and this one to be reimplemented through the generalised one.
 60 | export
 61 | dependeesOfGivens : (sig : GenSignature) -> FinSet sig.targetType.args.length
 62 | dependeesOfGivens sig = do
 63 |   let nameToIndex = SortedMap.fromList $ mapI sig.targetType.args $ \i, arg => (argName' arg, i)
 64 |   let varsInGivens = concatMap (\idx => allVarNames' $ type $ index' sig.targetType.args idx) sig.givenParams
 65 |   fromList $ mapMaybe (lookup' nameToIndex) $ Prelude.toList varsInGivens
 66 |
 67 | appFuel : (topmost : Name) -> (fuel : TTImp) -> TTImp
 68 | appFuel = app . var
 69 |
 70 | export
 71 | canonicSig : GenSignature -> TTImp
 72 | canonicSig sig = piAll returnTy $ MkArg MW ExplicitArg Nothing `(Data.Fuel.Fuel) :: (arg <$> Prelude.toList sig.givenParams) where
 73 |   -- TODO Check that the resulting `TTImp` reifies to a `Type`? During this check, however, all types must be present in the caller's context.
 74 |
 75 |   arg : Fin sig.targetType.args.length -> Arg
 76 |   arg idx = let MkArg {name, type, _} = index' sig.targetType.args idx in MkArg MW ExplicitArg name type
 77 |
 78 |   returnTy : TTImp
 79 |   returnTy = `(Test.DepTyCheck.Gen.Gen Test.DepTyCheck.Gen.Emptiness.MaybeEmpty ~(buildDPair targetTypeApplied generatedArgs)) where
 80 |
 81 |     targetTypeApplied : TTImp
 82 |     targetTypeApplied = foldr apply (extractTargetTyExpr sig.targetType) $ reverse $ sig.targetType.args <&> \(MkArg {name, piInfo, _}) => do
 83 |                           let name = stname name
 84 |                           case piInfo of
 85 |                             ExplicitArg   => (.$ var name)
 86 |                             ImplicitArg   => \f => namedApp f name $ var name
 87 |                             DefImplicit _ => \f => namedApp f name $ var name
 88 |                             AutoImplicit  => (`autoApp` var name)
 89 |
 90 |     generatedArgs : List (Name, TTImp)
 91 |     generatedArgs = mapMaybeI sig.targetType.args $ \idx, (MkArg {name, type, _}) =>
 92 |                       ifThenElse .| contains idx sig.givenParams .| Nothing .| Just (stname name, type)
 93 |
 94 | -- Complementary to `canonicSig`
 95 | export
 96 | callCanonic : (0 sig : GenSignature) -> (topmost : Name) -> (fuel : TTImp) -> Vect sig.givenParams.size TTImp -> TTImp
 97 | callCanonic _ = foldl app .: appFuel
 98 |
 99 | -----------------------------------------------------
100 | --- Data types for the safe signature formulation ---
101 | -----------------------------------------------------
102 |
103 | public export
104 | data ArgExplicitness = ExplicitArg | ImplicitArg
105 |
106 | public export
107 | Eq ArgExplicitness where
108 |   ExplicitArg == ExplicitArg = True
109 |   ImplicitArg == ImplicitArg = True
110 |   _ == _ = False
111 |
112 | namespace ArgExplicitness
113 |
114 |   public export
115 |   (.toTT) : ArgExplicitness -> PiInfo a
116 |   (.toTT) ExplicitArg = ExplicitArg
117 |   (.toTT) ImplicitArg = ImplicitArg
118 |
119 | ------------------------------------------------------------------
120 | --- Datatypes to describe signatures after checking user input ---
121 | ------------------------------------------------------------------
122 |
123 | --- `Gen` signature containing info about params explicitness and their names ---
124 |
125 | public export
126 | record ExternalGenSignature where
127 |   constructor MkExternalGenSignature
128 |   targetType : TypeInfo
129 |   {auto 0 targetTypeCorrect : AllTyArgsNamed targetType}
130 |   givenParams : SortedMap (Fin targetType.args.length) (ArgExplicitness, Name)
131 |   givensOrder : Vect givenParams.size $ Fin givenParams.size -- must be a permutation
132 |   {gendParamsCnt : _}
133 |   gendOrder   : Vect gendParamsCnt $ Fin gendParamsCnt -- must be a permutation
134 |
135 | namespace ExternalGenSignature
136 |
137 |   -- characterises external generator signatures ignoring particular order of given/generated arguments
138 |   export
139 |   characteristics : ExternalGenSignature -> (String, List Nat)
140 |   characteristics $ MkExternalGenSignature ty giv _ _ = (show ty.name, toNatList $ keys giv)
141 |
142 | -- Compares external generator signatures ignoring particular order of given/generated arguments
143 | public export
144 | Eq ExternalGenSignature where (==) = (==) `on` characteristics
145 |
146 | -- Compares external generator signatures ignoring particular order of given/generated arguments
147 | public export
148 | Ord ExternalGenSignature where compare = comparing characteristics
149 |
150 | export
151 | callExternalGen : (sig : ExternalGenSignature) -> (topmost : Name) -> (fuel : TTImp) -> Vect sig.givenParams.size TTImp -> TTImp
152 | callExternalGen sig topmost fuel values =
153 |   foldl (flip apply) (appFuel topmost fuel) $ reorder sig.givensOrder (sig.givenParams.asVect `zip` values) <&> \case
154 |     ((_, ExplicitArg, _   ), value) => (.$ value)
155 |     ((_, ImplicitArg, name), value) => \f => namedApp f name value
156 |
157 | export
158 | internalise : (extSig : ExternalGenSignature) -> Subset GenSignature $ \sig => sig.givenParams.size = extSig.givenParams.size
159 | internalise $ MkExternalGenSignature ty giv _ _ = Element (MkGenSignature ty $ keySet giv) $ keySetSize giv
160 |