Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

Check that names which need to be inferred actually are

Ignore-this: 2cdd4a5cbe364d3f1d714e0d0d2f1eb5

darcs-hash:20091125135805-228f4-02703f6120dab6edb7079e76a503fba02f624134.gz
  • Loading branch information...
commit 1a585ac876c7632e4d2ccfc628cc3655ab3fac7f 1 parent ac98c40
eb authored
Showing with 17 additions and 2 deletions.
  1. +10 −0 Ivor/Errors.lhs
  2. +1 −0  Ivor/PatternDefs.lhs
  3. +6 −2 Ivor/TT.lhs
View
10 Ivor/Errors.lhs
@@ -10,6 +10,7 @@
> | IMessage String
> | IUnbound (Indexed Name) (Indexed Name) (Indexed Name) (Indexed Name) [Name]
> | INoSuchVar Name
+> | ICantInfer Name (Indexed Name)
> | IContext String IError
> deriving (Show, Eq)
@@ -20,3 +21,12 @@
> type IvorM = Either IError
> ifail = Left
+
+Generic error checking can go here:
+
+Check that all the names are real rather than implicit and inferred
+
+> checkRealNames :: [Name] -> Indexed Name -> IvorM ()
+> checkRealNames [] tm = return ()
+> checkRealNames (nm@(MN ("INFER", n)): ns) tm = ifail (ICantInfer nm tm)
+> checkRealNames (_:ns) tm = checkRealNames ns tm
View
1  Ivor/PatternDefs.lhs
@@ -31,6 +31,7 @@ Also return whether the function is definitely total.
> let clauses = nub (concat clausesIn)
> let clauses' = filter (mostSpecClause clauses) clauses
> (ty@(Ind ty'),_) <- typecheck gam tyin
+> checkRealNames (getNames (Sc ty')) ty
> let arity = length (getExpected ty')
> checkNotExists fn gam
> gam' <- gInsert fn (G Undefined ty defplicit) gam
View
8 Ivor/TT.lhs
@@ -188,6 +188,7 @@
> | Message String
> | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]
> | NoSuchVar Name
+> | CantInfer Name ViewTerm
> | ErrContext String TTError
> instance Show TTError where
@@ -197,6 +198,7 @@
> show (Unbound clause clty rhs rhsty ns)
> = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++
> " = " ++ show rhs
+> show (CantInfer n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm
> show (NoSuchVar n) = "No such name as " ++ show n
> show (ErrContext c err) = c ++ show err
@@ -223,6 +225,7 @@
> (view (Term (rhs, Ind TTCore.Star)))
> (view (Term (rhsty, Ind TTCore.Star)))
> names
+> getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star)))
> getError (INoSuchVar n) = NoSuchVar n
> getError (IContext s e) = ErrContext s (getError e)
@@ -482,8 +485,9 @@ do let olddefs = defs st
> t <- raw tm
> let Gam ctxt = defs st
> case (typecheck (defs st) t) of
-> (Right (t, ty)) ->
-> do tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")
+> (Right (t@(Ind t'), ty)) ->
+> do tt $ checkRealNames (getNames (Sc t')) t
+> tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type")
> -- let newdefs = Gam ((n, (G und (finalise t))):ctxt)
> newdefs <- gInsert n (G und (finalise t) defplicit) (Gam ctxt)
> return $ Ctxt st { defs = newdefs }
Please sign in to comment.
Something went wrong with that request. Please try again.