@@ -0,0 +1,274 @@
1+module Pruviloj.Derive.Eliminators
2+
3+import Language.Reflection.Utils
4+import Data.Vect
5+
6+import Pruviloj.Core
7+import Pruviloj.Internals.TyConInfo
8+import Pruviloj.Internals
9+import Pruviloj.Renamers
10+
11+
12+%access private
13+
14+bindParams : TyConInfo -> Elab ()
15+bindParams info = traverse_ (uncurry forall) (getParams info)
16+
17+||| Bind indices at new names and return a renamer that's used to
18+||| rewrite an application of something to their designated global
19+||| names
20+bindIndices : TyConInfo -> Elab Renamer
21+bindIndices info = bind' (getIndices info) (const Nothing)
22+ where bind' : List (TTName, Raw) -> Renamer -> Elab Renamer
23+ bind' [] ren = return ren
24+ bind' ((n, t) :: ixs) ren = do n' <- nameFrom n
25+ forall n' (alphaRaw ren t)
26+ bind' ixs (extend ren n n')
27+
28+||| Return the renaming required to use the result type for this
29+||| binding of the indices
30+bindTarget : TyConInfo -> Elab (TTName, Renamer)
31+bindTarget info = do ren <- bindIndices info
32+ tn <- gensym "target"
33+ forall tn (alphaRaw ren $ result info)
34+ return (tn, ren)
35+
36+elabMotive : TyConInfo -> Elab ()
37+elabMotive info = do attack
38+ ren <- bindIndices info
39+ x <- gensym "scrutinee"
40+ forall x (alphaRaw ren $ result info)
41+ fill `(Type)
42+ solve -- the attack
43+ solve -- the motive type hole
44+
45+
46+
47+
48+headsMatch : Raw -> Raw -> Bool
49+headsMatch x y =
50+ case (headName x, headName y) of
51+ (Just n1, Just n2) => n1 == n2
52+ _ => False
53+
54+||| Make an induction hypothesis if one is called for
55+mkIh : TyConInfo -> (motiveName : TTName) -> (recArg : TTName) -> (argty, fam : Raw) -> Elab ()
56+mkIh info motiveName recArg argty fam =
57+ case !(stealBindings argty (const Nothing)) of
58+ (argArgs, argRes) =>
59+ if headsMatch argRes fam
60+ then do ih <- gensym "ih"
61+ ihT <- newHole "ihT" `(Type)
62+ forall ih (Var ihT)
63+ focus ihT
64+ attack
65+ for_ {b=()} argArgs $ \(n, b) =>
66+ forall n (getBinderTy b)
67+ let argTm : Raw = mkApp (Var recArg) (map (Var . fst) argArgs)
68+ argTmTy <- forgetTypes (snd !(check argTm))
69+ argHoles <- apply (Var motiveName)
70+ (replicate (length (getIndices info))
71+ (True, 0) ++
72+ [(False,1)])
73+ argH <- snd <$> last argHoles
74+ focus argH
75+ fill argTm; solve
76+ solve -- attack
77+ solve -- ihT
78+ else return ()
79+
80+elabMethodTy : TyConInfo -> TTName -> List CtorArg -> Raw -> Raw -> Elab ()
81+elabMethodTy info motiveName [] res ctorApp =
82+ do argHoles <- apply (Var motiveName)
83+ (replicate (length (getIndices info)) (True, 0) ++
84+ [(False, 1)])
85+ argH <- snd <$> last argHoles
86+ focus argH; fill ctorApp; solve
87+ solve
88+elabMethodTy info motiveName (CtorParameter arg :: args) res ctorApp =
89+ elabMethodTy info motiveName args res (RApp ctorApp (Var (argName arg)))
90+elabMethodTy info motiveName (CtorField arg :: args) res ctorApp =
91+ do let n = argName arg
92+ let t = argTy arg
93+ attack; forall n t
94+ mkIh info motiveName n t (result info)
95+ elabMethodTy info motiveName args res (RApp ctorApp (Var n))
96+ solve
97+
98+
99+
100+elabMethod : TyConInfo -> (motiveName, ctorN : TTName) -> List CtorArg -> Raw -> Elab ()
101+elabMethod info motiveName ctorN ctorArgs resTy =
102+ do elabMethodTy info motiveName ctorArgs resTy (Var ctorN)
103+
104+
105+||| Bind a method for a constructor
106+bindMethod : TyConInfo -> (motiveName, cn : TTName) -> List CtorArg -> Raw -> Elab ()
107+bindMethod info motiveName cn cargs cty =
108+ do n <- nameFrom cn
109+ h <- newHole "methTy" `(Type)
110+ forall n (Var h)
111+ focus h; elabMethod info motiveName cn cargs cty
112+
113+getElimTy : TyConInfo -> List (TTName, List CtorArg, Raw) -> Elab Raw
114+getElimTy info ctors =
115+ do ty <- runElab `(Type) $
116+ do bindParams info
117+ (scrut, iren) <- bindTarget info
118+ motiveN <- gensym "P"
119+ motiveH <- newHole "motive" `(Type)
120+ forall motiveN (Var motiveH)
121+ focus motiveH
122+ elabMotive info
123+
124+ for_ {b=()} ctors $ \(cn, cargs, cresty) =>
125+ bindMethod info motiveN cn cargs cresty
126+ let ret = mkApp (Var motiveN)
127+ (map (Var . fst)
128+ (getIndices info) ++
129+ [Var scrut])
130+ apply (alphaRaw iren ret) []
131+ solve
132+ forgetTypes (fst ty)
133+
134+
135+
136+data ElimArg = IHArgument TTName | NormalArgument TTName
137+
138+instance Show ElimArg where
139+ show (IHArgument x) = "IHArgument " ++ show x
140+ show (NormalArgument x) = "NormalArgument " ++ show x
141+
142+getElimClause : TyConInfo -> (elimn : TTName) -> (methCount : Nat) ->
143+ (TTName, List CtorArg, Raw) -> Nat -> Elab FunClause
144+getElimClause info elimn methCount (cn, args, resTy) whichCon =
145+ elabPatternClause
146+ (do -- Establish a hole for each parameter
147+ for (getParams info) {b=()} $ \(n, ty) =>
148+ do claim n ty
149+ unfocus n
150+
151+
152+ -- Establish a hole for each argument to the constructor
153+ for {b=()} args $ \arg =>
154+ case arg of
155+ CtorParameter _ => return ()
156+ CtorField arg => do claim (argName arg) (argTy arg)
157+ unfocus (argName arg)
158+
159+ -- Establish a hole for the scrutinee (infer type)
160+ scrutinee <- newHole "scrutinee" resTy
161+
162+
163+ -- Apply the eliminator to the proper holes
164+ let paramApp : Raw = mkApp (Var elimn) $
165+ map (Var . fst) (getParams info)
166+
167+ -- We leave the RHS with a function type: motive -> method* -> res
168+ -- to make it easier to map methods to constructors
169+ holes <- apply paramApp (replicate (length (getIndices info))
170+ (True, 0) ++
171+ [(False, 1)])
172+ scr <- snd <$> last holes
173+ focus scr; fill (Var scrutinee); solve
174+ solve
175+
176+ -- Fill the scrutinee with the concrete constructor pattern
177+ focus scrutinee
178+ apply (mkApp (Var cn) $
179+ map (\x => case x of
180+ CtorParameter param => Var (argName param)
181+ CtorField arg => Var (argName arg))
182+ args)
183+ []
184+ solve)
185+ (do motiveN <- gensym "motive"
186+ intro motiveN
187+ prevMethods <- doTimes whichCon intro1
188+ methN <- gensym "useThisMethod"
189+ intro methN
190+ nextMethods <- intros
191+
192+ argSpec <- Foldable.concat <$>
193+ for args
194+ (\x =>
195+ case x of
196+ CtorParameter _ => return List.Nil
197+ CtorField arg =>
198+ do let n = argName arg
199+ let t = argTy arg
200+ (argArgs, argRes) <- stealBindings t (const Nothing)
201+ if headsMatch argRes (result info) --recursive
202+ then return [ NormalArgument n
203+ , IHArgument n
204+ ]
205+ else return [NormalArgument n])
206+
207+ argHs <- apply (Var methN) (replicate (List.length argSpec) (True, 0))
208+ solve
209+
210+ -- Now build the recursive calls for the induction hypotheses
211+ for_ {a=(ElimArg, TTName)} {b=()}
212+ !(zipH argSpec (map snd argHs))
213+ (\(spec, nh) =>
214+ case spec of
215+ NormalArgument n => do focus nh
216+ apply (Var n) []
217+ solve
218+ IHArgument n =>
219+ do focus nh
220+ attack
221+ local <- intros
222+ ihHs <- apply (Var elimn) $
223+ replicate (length (TyConInfo.args info)) (True, 0) ++
224+ [(False, 1)] ++
225+ replicate (S methCount) (True, 0)
226+ solve -- application
227+
228+ let (arg::motive::methods) = map snd $ drop (length (TyConInfo.args info)) ihHs
229+ focus arg
230+
231+ apply (mkApp (Var n) (map Var local)) []; solve
232+ solve -- attack
233+
234+
235+ focus motive; fill (Var motiveN); solve
236+ let methodArgs : List TTName = toList prevMethods ++ [methN] ++ nextMethods
237+ remaining <- zipH methods methodArgs
238+
239+ for_ {b=()} remaining $ \todo =>
240+ do focus (fst todo)
241+ fill (Var (snd todo))
242+ solve))
243+
244+
245+
246+ where bindLam : List (TTName, Binder Raw) -> Raw -> Raw
247+ bindLam [] x = x
248+ bindLam ((n, b)::rest) x = RBind n (Lam (getBinderTy b)) $ bindLam rest x
249+
250+getElimClauses : TyConInfo -> (elimn : TTName) ->
251+ List (TTName, List CtorArg, Raw) -> Elab (List FunClause)
252+getElimClauses info elimn ctors =
253+ let methodCount = length ctors
254+ in traverse (\(i, con) => getElimClause info elimn methodCount con i)
255+ (enumerate ctors)
256+
257+instance Show FunClause where
258+ show (MkFunClause x y) = "(MkFunClause " ++ show x ++ " " ++ show y ++ ")"
259+
260+abstract
261+deriveElim : (tyn, elimn : TTName) -> Elab ()
262+deriveElim tyn elimn =
263+ do -- Begin with some basic sanity checking: the type name uniquely
264+ -- determines a datatype
265+ (MkDatatype tyn tyconArgs tyconRes ctors') <- lookupDatatypeExact tyn
266+
267+ info <- getTyConInfo tyconArgs (Var tyn)
268+ ctors <- traverse (processCtorArgs info) ctors'
269+ declareType $ Declare elimn [] !(getElimTy info ctors)
270+ clauses <- getElimClauses info elimn ctors
271+
272+ defineFunction $ DefineFun elimn clauses
273+ return ()
274+