git.iko.soy/Idris-dev
on master help sign in
Tinker with universe constraints
commitada02de2e4c6fdd2d4792ab00b990f603fc50969 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 25 Nov 2011, 17:20 (15 years ago) parent5b08cc9
4 files changed+14−9
compare with master
unifiedsplit
src/Core/TT.hs+3−1 src/Core/Typecheck.hs+4−4 src/Idris/AbsSyntax.hs+6−4 src/Idris/Delaborate.hs+1
src/Core/TT.hs+3−1
@@ -35,6 +35,7 @@ instance Show FC where
3535data Err = Msg String
3636 | CantUnify Term Term Err
3737 | IncompleteTerm Term
38+ | UniverseError
3839 | At FC Err
3940 deriving Eq
4041
@@ -179,12 +180,13 @@ type RProgram = [(Name, RDef)]
179180
180181data UExp = UVar Int -- universe variable
181182 | UVal Int -- explicit universe level
182− deriving Eq
183+ deriving (Eq, Ord)
183184
184185instance Show UExp where
185186 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]
186187 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
187188 show (UVal x) = show x
189+-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"
188190
189191data UConstraint = ULT UExp UExp
190192 | ULE UExp UExp
src/Core/Typecheck.hs+4−4
@@ -89,7 +89,7 @@ check' holes ctxt env top = chk env top where
8989 (v, cs) <- get
9090 let Set su = normalise ctxt env st
9191 let Set tu = normalise ctxt env tt
92− when (not holes) $ put (v+1, ULT su (UVar v):ULT tu (UVar v):cs)
92+ when (not holes) $ put (v+1, ULE su (UVar v):ULE tu (UVar v):cs)
9393 return (Bind n (Pi sv) (pToV n tv), Set (UVar v))
9494 chk env (RBind n b sc)
9595 = do b' <- checkBinder b
@@ -112,7 +112,7 @@ check' holes ctxt env top = chk env top where
112112 (vv, vt) <- chk env v
113113 let tv' = normalise ctxt env tv
114114 let tt' = normalise ctxt env tt
115− convertsC ctxt env tv vt
115+ convertsC ctxt env vt tv
116116 lift $ isSet ctxt env tt'
117117 return (Let tv vv)
118118 checkBinder (NLet t v)
@@ -120,7 +120,7 @@ check' holes ctxt env top = chk env top where
120120 (vv, vt) <- chk env v
121121 let tv' = normalise ctxt env tv
122122 let tt' = normalise ctxt env tt
123− convertsC ctxt env tv vt
123+ convertsC ctxt env vt tv
124124 lift $ isSet ctxt env tt'
125125 return (NLet tv vv)
126126 checkBinder (Hole t)
@@ -144,7 +144,7 @@ check' holes ctxt env top = chk env top where
144144 (vv, vt) <- chk env v
145145 let tv' = normalise ctxt env tv
146146 let tt' = normalise ctxt env tt
147− convertsC ctxt env tv vt
147+ convertsC ctxt env vt tv
148148 lift $ isSet ctxt env tt'
149149 return (Guess tv vv)
150150 checkBinder (PVar t)
src/Idris/AbsSyntax.hs+6−4
@@ -29,6 +29,7 @@ defaultOpts = IOption 0 False False
2929-- and syntax macros.
3030
3131data IState = IState { tt_ctxt :: Context,
32+ idris_constraints :: [(UConstraint, FC)],
3233 idris_infixes :: [FixDecl],
3334 idris_implicits :: Ctxt [PArg],
3435 idris_statics :: Ctxt [Bool],
@@ -47,7 +48,7 @@ data IState = IState { tt_ctxt :: Context,
4748 errLine :: Maybe Int
4849 }
4950
50−idrisInit = IState initContext [] emptyContext emptyContext emptyContext
51+idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
5152 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing
5253
5354-- The monad for the main REPL - reading and processing files and updating
@@ -111,13 +112,14 @@ setContext ctxt = do i <- get; put (i { tt_ctxt = ctxt } )
111112updateContext :: (Context -> Context) -> Idris ()
112113updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
113114
114−addConstraints :: (Int, [UConstraint]) -> Idris ()
115−addConstraints (v, cs)
115+addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
116+addConstraints fc (v, cs)
116117 = do i <- get
117118 let ctxt = tt_ctxt i
118119 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
119120 next_tvar = v }
120− put (i { tt_ctxt = ctxt' })
121+ let ics = zip cs (repeat fc) ++ idris_constraints i
122+ put (i { tt_ctxt = ctxt', idris_constraints = ics })
121123
122124addDeferred :: [(Name, Type)] -> Idris ()
123125addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
src/Idris/Delaborate.hs+1
@@ -53,5 +53,6 @@ pshow i (CantUnify x y e) = "Can't unify " ++ show (delab i x)
5353 ++ " with " ++ show (delab i y)
5454-- ++ "\n\t(" ++ pshow i e ++ ")"
5555pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
56+pshow i UniverseError = "Universe inconsistency"
5657pshow i (At f e) = show f ++ ":" ++ pshow i e
5758