Permalink
Browse files

Record projection

Given a record, defined as follows, for example:

record Foo : Nat -> Set where
      MkFoo : (name : String) ->
              (things : Vect a n) ->
              Foo n

Functions 'name' and 'things' are generated to extract the record
fields. 'implicit_n' and 'implicit_a' are generated to extract the
implicit parts.
  • Loading branch information...
1 parent 34331d9 commit 3c42704162a97c7fae15db72ba439d5405267362 Edwin Brady committed Jan 27, 2012
Showing with 71 additions and 5 deletions.
  1. +9 −1 CHANGELOG
  2. +54 −0 src/Idris/ElabDecls.hs
  3. +3 −3 src/Idris/ElabTerm.hs
  4. +5 −1 src/Idris/Parser.hs
View
@@ -1,8 +1,16 @@
New in 0.9.1:
+-------------
+
+User visible changes:
* dsl notation
-* faster compilation (only compiling names which are used)
+* record projection
* auto implicits and default argument values {auto n : T}, {default val n : T}
+* Additions to prelude
+
+Internal changes:
+
+* faster compilation (only compiling names which are used)
0.1.x to 0.9.0:
View
@@ -88,6 +88,60 @@ elabRecord :: ElabInfo -> SyntaxInfo -> FC -> Name ->
PTerm -> Name -> PTerm -> Idris ()
elabRecord info syn fc tyn ty cn cty
= do elabData info syn fc (PDatadecl tyn ty [(cn, cty, fc)])
+ cty <- implicit syn cn cty
+ i <- get
+ cty <- case lookupTy Nothing cn (tt_ctxt i) of
+ [t] -> return (delab i t)
+ _ -> fail "Something went inexplicably wrong"
+ cimp <- case lookupCtxt Nothing cn (idris_implicits i) of
+ [imps] -> return imps
+ let ptys = getProjs [] (renameBs cimp cty)
+ let recty = getRecTy cty
+ logLvl 6 $ show (recty, ptys)
+ let substs = map (\ (n, _) -> (n, PApp fc (PRef fc n)
+ [pexp (PRef fc rec)])) ptys
+ let ptpos = zip ptys [0..]
+ decls <- mapM (mkProj recty substs cimp) ptpos
+ mapM_ (elabDecl info) (concat decls)
+ where
+
+ renameBs (PImp _ _ _ _ : ps) (PPi p n ty s)
+ = PPi p (mkImp n) ty (renameBs ps (substMatch n (PRef fc (mkImp n)) s))
+ renameBs (_:ps) (PPi p n ty s) = PPi p n ty (renameBs ps s)
+ renameBs _ t = t
+
+ getProjs acc (PPi _ n ty s) = getProjs ((n, ty) : acc) s
+ getProjs acc r = reverse acc
+
+ getRecTy (PPi _ n ty s) = getRecTy s
+ getRecTy t = t
+
+ rec = MN 0 "rec"
+
+ mkp (UN n) = MN 0 ("p_" ++ n)
+ mkp (MN 0 n) = MN 0 ("p_" ++ n)
+ mkp (NS n s) = NS (mkp n) s
+
+ mkImp (UN n) = UN ("implicit_" ++ n)
+ mkImp (MN 0 n) = MN 0 ("implicit_" ++ n)
+ mkImp (NS n s) = NS (mkImp n) s
+
+ mkProj recty substs cimp ((pn, pty), pos)
+ = do let pfnTy = PTy defaultSyntax fc [] pn
+ (PPi expl rec recty
+ (substMatches substs pty))
+ let pls = repeat Placeholder
+ let before = pos
+ let after = length substs - (pos + 1)
+ let args = take before pls ++ PRef fc (mkp pn) : take after pls
+ let iargs = map implicitise (zip cimp args)
+ let lhs = PApp fc (PRef fc pn)
+ [pexp (PApp fc (PRef fc cn) iargs)]
+ let rhs = PRef fc (mkp pn)
+ let pclause = PClause pn lhs [] rhs []
+ return [pfnTy, PClauses fc [] pn [pclause]]
+
+ implicitise (pa, t) = pa { getTm = t }
elabCon :: ElabInfo -> SyntaxInfo -> Name -> (Name, PTerm, FC) -> Idris (Name, Type)
elabCon info syn tn (n, t_in, fc)
View
@@ -143,6 +143,7 @@ elab ist info pattern tcgen fn tm
[] -> False
_ -> True
-- this is to stop us resolve type classes recursively
+ -- trace (show (n, guarded)) $
if (tcname n && ina) then erun fc $ patvar n
else if (defined && not guarded)
then do apply (Var n) []; solve
@@ -226,9 +227,8 @@ elab ist info pattern tcgen fn tm
(elabArgs (ina || not isinf, guarded)
[] False (reverse ns')
(map (\x -> (lazyarg x, getTm x)) (reverse eargs))))
--- (try (do apply2 (Var f) (map (toElab' (ina || not isinf)) args))
- (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
- solve)
+ (do apply_elab f (map (toElab (ina || not isinf, guarded)) args)
+ solve)
ivs' <- get_instances
when (not pattern || (ina && not tcgen)) $
mapM_ (\n -> do focus n
View
@@ -945,8 +945,12 @@ pRecord syn = try (do acc <- pAccessibility
tyn_in <- pfName; ty <- pTSig syn
let tyn = expandNS syn tyn_in
reserved "where"
+ open_block
+ push_indent
(cn, cty, _) <- pConstructor syn
- pTerminator
+ pKeepTerminator
+ pop_indent
+ close_block
accData acc tyn [cn]
return $ PRecord syn fc tyn ty cn cty)

0 comments on commit 3c42704

Please sign in to comment.