@@ -0,0 +1,102 @@
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
3+module Idris.ElabDecls where
12+elabType :: Name -> PTerm -> Idris ()
14+ = do ctxt <- getContext
15+ (ty', log) <- tclift $ elaborate ctxt n (Set 0) (build False ty)
16+ (cty, _) <- tclift $ recheck ctxt [] ty'
17+ iLOG $ "---> " ++ show cty
18+ updateContext (addConstant n cty)
20+elabData :: PData -> Idris ()
21+elabData (PDatadecl n t dcons)
22+ = do ctxt <- getContext
23+ (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
24+ (cty, _) <- tclift $ recheck ctxt [] t'
25+ iLOG $ "---> " ++ show cty
26+ updateContext (addConstant n cty) -- temporary, to check cons
27+ cons <- mapM elabCon dcons
28+ setContext (addDatatype (Data n cty cons) ctxt)
30+elabCon :: (Name, PTerm) -> Idris (Name, Type)
32+ = do ctxt <- getContext
33+ iLOG $ "Constructor " ++ show n ++ " : " ++ showImp True t
34+ (t', log) <- tclift $ elaborate ctxt n (Set 0) (build False t)
35+-- iLOG $ "Rechecking " ++ show t'
36+ (cty, _) <- tclift $ recheck ctxt [] t'
37+ iLOG $ "---> " ++ show n ++ " : " ++ show cty
40+elabClauses :: [PClause] -> Idris ()
41+elabClauses _ = return ()
43+elabClause :: PClause -> Idris ()
44+elabClause _ = return ()
46+elabDecl :: PDecl -> Idris ()
47+elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (show e))
49+elabDecl' (PFix _ _) = return () -- nothing to elaborate
50+elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n
52+elabDecl' (PData d) = do iLOG $ "Elaborating " ++ show d
54+elabDecl' d@(PClauses ps) = do iLOG $ "Elaborating " ++ show d
57+-- Using the elaborator, convert a term in raw syntax to a fully
58+-- elaborated, typechecked term.
60+-- If building a pattern match, we convert undeclared variables from
61+-- holes to pattern bindings.
63+build :: Bool -> PTerm -> Elab Term
64+build pattern tm = do elab pattern tm
67+elab :: Bool -> PTerm -> Elab ()
68+elab pattern tm = elab' tm
70+ isph (_, Placeholder) = True
73+ elab' PSet = do exact (RSet 0); solve
74+ elab' (PQuote r) = do exact r; solve
75+ elab' (PRef n) | pattern
76+ = try (do apply (Var n) []; solve)
78+ elab' (PRef n) = do apply (Var n) []; solve
79+ elab' (PLam n Placeholder sc)
80+ = do attack; intro n; elab' sc; solve
81+ elab' (PPi _ n Placeholder sc)
82+ = do attack; arg n (MN 0 "ty"); elab' sc; solve
83+ elab' (PPi _ n ty sc)
84+ = do attack; tyn <- unique_hole (MN 0 "ty")
91+ elab' (PApp (PRef f) imps args)
92+ = do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)
94+ elabArgs ns (map snd imps ++ args)
95+ elab' x = fail $ "Not implemented " ++ show x
97+ elabArgs [] _ = return ()
98+ elabArgs (n:ns) (Placeholder : args) = elabArgs ns args
99+ elabArgs (n:ns) (t : args) = do focus n; elab' t; elabArgs ns args