@@ -29,134 +29,145 @@ isSet ctxt env tm = isSet' (normalise ctxt env tm)
2929 isSet' tm = fail (showEnv env tm ++ " is not a Set")
3030
3131recheck :: Context -> Env -> Term -> TC (Term, Type)
32−recheck ctxt env tm = check ctxt env (forget tm)
32+recheck ctxt env tm
33+ = case check' False ctxt env (forget tm) of -- holes banned
34+ Error (IncompleteTerm _) -> Error $ IncompleteTerm tm
35+ x -> x
3336
3437check :: Context -> Env -> Raw -> TC (Term, Type)
35−check ctxt env (Var n)
36− | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
37− | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
38− | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)
39−check ctxt env (RApp f a)
40− = do (fv, fty) <- check ctxt env f
41− (av, aty) <- check ctxt env a
42− let fty' = renameBinders 0 $ normalise ctxt env fty
43− case fty' of
44− Bind x (Pi s) t ->
45− do converts ctxt env s aty
46− let apty = normalise emptyContext env (Bind x (Let aty av) t)
47− return (App fv av, apty)
48− t -> fail "Can't apply a non-function type"
49− -- This rather unpleasant hack is needed because during incomplete
50− -- proofs, variables are locally bound with an explicit name. If we just
51− -- make sure bound names in function types are locally unique, machine
52− -- generated names, we'll be fine.
53− where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)
54− (renameBinders (i+1) t)
55− renameBinders i sc = sc
56−check ctxt env (RSet i) = return (Set i, Set i) -- LATER: (i+1))
57−check ctxt env (RConstant c) = return (Constant c, constType c)
58− where constType (I _) = Constant IType
59− constType (BI _) = Constant BIType
60− constType (Fl _) = Constant FlType
61− constType (Ch _) = Constant ChType
62− constType (Str _) = Constant StrType
63− constType _ = Set 0
64−check ctxt env (RBind n b sc)
65− = do b' <- checkBinder b
66− (scv, sct) <- check ctxt ((n, b'):env) sc
67− discharge n b' (pToV n scv) (pToV n sct)
68− where checkBinder (Lam t)
69− = do (tv, tt) <- check ctxt env t
70− let tv' = normalise ctxt env tv
71− let tt' = normalise ctxt env tt
72− isSet ctxt env tt'
73− return (Lam tv)
74− checkBinder (Pi t)
75− = do (tv, tt) <- check ctxt env t
76− let tv' = normalise ctxt env tv
77− let tt' = normalise ctxt env tt
78− isSet ctxt env tt'
79− return (Pi tv)
80− checkBinder (Let t v)
81− = do (tv, tt) <- check ctxt env t
82− (vv, vt) <- check ctxt env v
83− let tv' = normalise ctxt env tv
84− let tt' = normalise ctxt env tt
85− converts ctxt env tv vt
86− isSet ctxt env tt'
87− return (Let tv vv)
88− checkBinder (NLet t v)
89− = do (tv, tt) <- check ctxt env t
90− (vv, vt) <- check ctxt env v
91− let tv' = normalise ctxt env tv
92− let tt' = normalise ctxt env tt
93− converts ctxt env tv vt
94− isSet ctxt env tt'
95− return (NLet tv vv)
96− checkBinder (Hole t)
97− = do (tv, tt) <- check ctxt env t
98− let tv' = normalise ctxt env tv
99− let tt' = normalise ctxt env tt
100− isSet ctxt env tt'
101− return (Hole tv)
102− checkBinder (GHole t)
103− = do (tv, tt) <- check ctxt env t
104− let tv' = normalise ctxt env tv
105− let tt' = normalise ctxt env tt
106− isSet ctxt env tt'
107− return (GHole tv)
108− checkBinder (Guess t v)
109− = do (tv, tt) <- check ctxt env t
110− (vv, vt) <- check ctxt env v
111− let tv' = normalise ctxt env tv
112− let tt' = normalise ctxt env tt
113− converts ctxt env tv vt
114− isSet ctxt env tt'
115− return (Guess tv vv)
116− checkBinder (PVar t)
117− = do (tv, tt) <- check ctxt env t
118− let tv' = normalise ctxt env tv
119− let tt' = normalise ctxt env tt
120− isSet ctxt env tt'
121− return (PVar tv)
122− checkBinder (PVTy t)
123− = do (tv, tt) <- check ctxt env t
124− let tv' = normalise ctxt env tv
125− let tt' = normalise ctxt env tt
126− isSet ctxt env tt'
127− return (PVTy tv)
38+check = check' True -- Holes allowed
12839
129− discharge n (Lam t) scv sct
130− = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
131− discharge n (Pi t) scv sct
132− = return (Bind n (Pi t) scv, sct)
133− discharge n (Let t v) scv sct
134− = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
135− discharge n (NLet t v) scv sct
136− = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
137− discharge n (Hole t) scv sct
138− = do -- A hole can't appear in the type of its scope
139− checkNotHoley 0 sct
140− return (Bind n (Hole t) scv, sct)
141− discharge n (GHole t) scv sct
142− = do -- A hole can't appear in the type of its scope
143− checkNotHoley 0 sct
144− return (Bind n (GHole t) scv, sct)
145− discharge n (Guess t v) scv sct
146− = do -- A hole can't appear in the type of its scope
147− checkNotHoley 0 sct
148− return (Bind n (Guess t v) scv, sct)
149− discharge n (PVar t) scv sct
150− = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)
151− discharge n (PVTy t) scv sct
152− = return (Bind n (PVTy t) scv, sct)
153−
154− checkNotHoley i (V v)
155− | v == i = fail "You can't put a hole where a hole don't belong"
156− checkNotHoley i (App f a) = do checkNotHoley i f
157− checkNotHoley i a
158− checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
159− checkNotHoley _ _ = return ()
40+check' :: Bool -> Context -> Env -> Raw -> TC (Term, Type)
41+check' holes ctxt env top = chk env top where
42+ chk env (Var n)
43+ | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)
44+ | Just (P nt n' ty) <- lookupP n ctxt = return (P nt n' ty, ty)
45+ | otherwise = do fail $ "No such variable " ++ show n ++ " in " ++ show (map fst env)
46+ chk env (RApp f a)
47+ = do (fv, fty) <- chk env f
48+ (av, aty) <- chk env a
49+ let fty' = renameBinders 0 $ normalise ctxt env fty
50+ case fty' of
51+ Bind x (Pi s) t ->
52+ do converts ctxt env s aty
53+ let apty = normalise emptyContext env (Bind x (Let aty av) t)
54+ return (App fv av, apty)
55+ t -> fail "Can't apply a non-function type"
56+ -- This rather unpleasant hack is needed because during incomplete
57+ -- proofs, variables are locally bound with an explicit name. If we just
58+ -- make sure bound names in function types are locally unique, machine
59+ -- generated names, we'll be fine.
60+ where renameBinders i (Bind x (Pi s) t) = Bind (MN i "binder") (Pi s)
61+ (renameBinders (i+1) t)
62+ renameBinders i sc = sc
63+ chk env (RSet i) = return (Set i, Set i) -- LATER: (i+1))
64+ chk env (RConstant c) = return (Constant c, constType c)
65+ where constType (I _) = Constant IType
66+ constType (BI _) = Constant BIType
67+ constType (Fl _) = Constant FlType
68+ constType (Ch _) = Constant ChType
69+ constType (Str _) = Constant StrType
70+ constType _ = Set 0
71+ chk env (RBind n b sc)
72+ = do b' <- checkBinder b
73+ (scv, sct) <- chk ((n, b'):env) sc
74+ discharge n b' (pToV n scv) (pToV n sct)
75+ where checkBinder (Lam t)
76+ = do (tv, tt) <- chk env t
77+ let tv' = normalise ctxt env tv
78+ let tt' = normalise ctxt env tt
79+ isSet ctxt env tt'
80+ return (Lam tv)
81+ checkBinder (Pi t)
82+ = do (tv, tt) <- chk env t
83+ let tv' = normalise ctxt env tv
84+ let tt' = normalise ctxt env tt
85+ isSet ctxt env tt'
86+ return (Pi tv)
87+ checkBinder (Let t v)
88+ = do (tv, tt) <- chk env t
89+ (vv, vt) <- chk env v
90+ let tv' = normalise ctxt env tv
91+ let tt' = normalise ctxt env tt
92+ converts ctxt env tv vt
93+ isSet ctxt env tt'
94+ return (Let tv vv)
95+ checkBinder (NLet t v)
96+ = do (tv, tt) <- chk env t
97+ (vv, vt) <- chk env v
98+ let tv' = normalise ctxt env tv
99+ let tt' = normalise ctxt env tt
100+ converts ctxt env tv vt
101+ isSet ctxt env tt'
102+ return (NLet tv vv)
103+ checkBinder (Hole t)
104+ | not holes = tfail (IncompleteTerm undefined)
105+ | otherwise
106+ = do (tv, tt) <- chk env t
107+ let tv' = normalise ctxt env tv
108+ let tt' = normalise ctxt env tt
109+ isSet ctxt env tt'
110+ return (Hole tv)
111+ checkBinder (GHole t)
112+ = do (tv, tt) <- chk env t
113+ let tv' = normalise ctxt env tv
114+ let tt' = normalise ctxt env tt
115+ isSet ctxt env tt'
116+ return (GHole tv)
117+ checkBinder (Guess t v)
118+ | not holes = tfail (IncompleteTerm undefined)
119+ | otherwise
120+ = do (tv, tt) <- chk env t
121+ (vv, vt) <- chk env v
122+ let tv' = normalise ctxt env tv
123+ let tt' = normalise ctxt env tt
124+ converts ctxt env tv vt
125+ isSet ctxt env tt'
126+ return (Guess tv vv)
127+ checkBinder (PVar t)
128+ = do (tv, tt) <- chk env t
129+ let tv' = normalise ctxt env tv
130+ let tt' = normalise ctxt env tt
131+ isSet ctxt env tt'
132+ return (PVar tv)
133+ checkBinder (PVTy t)
134+ = do (tv, tt) <- chk env t
135+ let tv' = normalise ctxt env tv
136+ let tt' = normalise ctxt env tt
137+ isSet ctxt env tt'
138+ return (PVTy tv)
139+
140+ discharge n (Lam t) scv sct
141+ = return (Bind n (Lam t) scv, Bind n (Pi t) sct)
142+ discharge n (Pi t) scv sct
143+ = return (Bind n (Pi t) scv, sct)
144+ discharge n (Let t v) scv sct
145+ = return (Bind n (Let t v) scv, Bind n (Let t v) sct)
146+ discharge n (NLet t v) scv sct
147+ = return (Bind n (NLet t v) scv, Bind n (Let t v) sct)
148+ discharge n (Hole t) scv sct
149+ = do -- A hole can't appear in the type of its scope
150+ checkNotHoley 0 sct
151+ return (Bind n (Hole t) scv, sct)
152+ discharge n (GHole t) scv sct
153+ = do -- A hole can't appear in the type of its scope
154+ checkNotHoley 0 sct
155+ return (Bind n (GHole t) scv, sct)
156+ discharge n (Guess t v) scv sct
157+ = do -- A hole can't appear in the type of its scope
158+ checkNotHoley 0 sct
159+ return (Bind n (Guess t v) scv, sct)
160+ discharge n (PVar t) scv sct
161+ = return (Bind n (PVar t) scv, Bind n (PVTy t) sct)
162+ discharge n (PVTy t) scv sct
163+ = return (Bind n (PVTy t) scv, sct)
164+
165+ checkNotHoley i (V v)
166+ | v == i = fail "You can't put a hole where a hole don't belong"
167+ checkNotHoley i (App f a) = do checkNotHoley i f
168+ checkNotHoley i a
169+ checkNotHoley i (Bind n b sc) = checkNotHoley (i+1) sc
170+ checkNotHoley _ _ = return ()
160171
161172
162173checkProgram :: Context -> RProgram -> TC Context