@@ -88,6 +88,60 @@ elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
8888 PTerm -> Name -> PTerm -> Idris ()
8989elabRecord info syn fc tyn ty cn cty
9090 = do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])
91+ cty <- implicit syn cn cty
92+ i <- get
93+ cty <- case lookupTy Nothing cn (tt_ctxt i) of
94+ [t] -> return (delab i t)
95+ _ -> fail "Something went inexplicably wrong"
96+ cimp <- case lookupCtxt Nothing cn (idris_implicits i) of
97+ [imps] -> return imps
98+ let ptys = getProjs [] (renameBs cimp cty)
99+ let recty = getRecTy cty
100+ logLvl 6 $ show (recty, ptys)
101+ let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
102+ [pexp (PRef fc rec)])) ptys
103+ let ptpos = zip ptys [0..]
104+ decls <- mapM (mkProj recty substs cimp) ptpos
105+ mapM_ (elabDecl info) (concat decls)
106+ where
107+
108+ renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
109+ = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
110+ renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
111+ renameBs _ t = t
112+
113+ getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
114+ getProjs acc r = reverse acc
115+
116+ getRecTy (PPi _ n ty s) = getRecTy s
117+ getRecTy t = t
118+
119+ rec = MN 0 "rec"
120+
121+ mkp (UN n) = MN 0 ("p_" ++ n)
122+ mkp (MN 0 n) = MN 0 ("p_" ++ n)
123+ mkp (NS n s) = NS (mkp n) s
124+
125+ mkImp (UN n) = UN ("implicit_" ++ n)
126+ mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
127+ mkImp (NS n s) = NS (mkImp n) s
128+
129+ mkProj recty substs cimp ((pn, pty), pos)
130+ = do let pfnTy = PTy defaultSyntax fc [] pn
131+ (PPi expl rec recty
132+ (substMatches substs pty))
133+ let pls = repeat Placeholder
134+ let before = pos
135+ let after = length substs - (pos + 1)
136+ let args = take before pls ++ PRef fc (mkp pn) : take after pls
137+ let iargs = map implicitise (zip cimp args)
138+ let lhs = PApp fc (PRef fc pn)
139+ [pexp (PApp fc (PRef fc cn) iargs)]
140+ let rhs = PRef fc (mkp pn)
141+ let pclause = PClause pn lhs [] rhs []
142+ return [pfnTy, PClauses fc [] pn [pclause]]
143+
144+ implicitise (pa, t) = pa { getTm = t }
91145
92146elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)
93147elabCon info syn tn (n, t_in, fc)