@@ -0,0 +1,102 @@
1+{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances, DeriveFunctor #-}
2+
3+module Idris.ElabDecls where
4+
5+import Idris.AbsSyntax
6+
7+import Core.TT
8+import Core.Elaborate
9+import Core.Evaluate
10+import Core.Typecheck
11+
12+elabType :: Name -> PTerm -> Idris ()
13+elabType n ty
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)
19+
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)
29+
30+elabCon :: (Name, PTerm) -> Idris (Name, Type)
31+elabCon (n, t)
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
38+ return (n, cty)
39+
40+elabClauses :: [PClause] -> Idris ()
41+elabClauses _ = return ()
42+
43+elabClause :: PClause -> Idris ()
44+elabClause _ = return ()
45+
46+elabDecl :: PDecl -> Idris ()
47+elabDecl d = idrisCatch (elabDecl' d) (\e -> iputStrLn (show e))
48+
49+elabDecl' (PFix _ _) = return () -- nothing to elaborate
50+elabDecl' (PTy n ty) = do iLOG $ "Elaborating type decl " ++ show n
51+ elabType n ty
52+elabDecl' (PData d) = do iLOG $ "Elaborating " ++ show d
53+ elabData d
54+elabDecl' d@(PClauses ps) = do iLOG $ "Elaborating " ++ show d
55+ elabClauses ps
56+
57+-- Using the elaborator, convert a term in raw syntax to a fully
58+-- elaborated, typechecked term.
59+--
60+-- If building a pattern match, we convert undeclared variables from
61+-- holes to pattern bindings.
62+
63+build :: Bool -> PTerm -> Elab Term
64+build pattern tm = do elab pattern tm
65+ get_term
66+
67+elab :: Bool -> PTerm -> Elab ()
68+elab pattern tm = elab' tm
69+ where
70+ isph (_, Placeholder) = True
71+ isph _ = False
72+
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)
77+ (patvar n)
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")
85+ claim tyn (RSet 0)
86+ forall n (Var tyn)
87+ focus tyn
88+ elab' ty
89+ elab' sc
90+ solve
91+ elab' (PApp (PRef f) imps args)
92+ = do ns <- apply (Var f) (map isph imps ++ map (\x -> False) args)
93+ solve
94+ elabArgs ns (map snd imps ++ args)
95+ elab' x = fail $ "Not implemented " ++ show x
96+
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
100+
101+
102+