git.iko.soy/Idris-dev
on master help sign in
Tinker with universe constraints
ada02deEdwin Brady
src/Core/TT.hs+3−1
compare with master
unifiedsplit
@@ -35,6 +35,7 @@ instance Show FC where
35data Err = Msg String
35data Err = Msg String
36 | CantUnify Term Term Err
36 | CantUnify Term Term Err
37 | IncompleteTerm Term
37 | IncompleteTerm Term
38+ | UniverseError
38 | At FC Err
39 | At FC Err
39 deriving Eq
40 deriving Eq
40
41
@@ -179,12 +180,13 @@ type RProgram = [(Name, RDef)]
179
180
180data UExp = UVar Int -- universe variable
181data UExp = UVar Int -- universe variable
181 | UVal Int -- explicit universe level
182 | UVal Int -- explicit universe level
182− deriving Eq
183+ deriving (Eq, Ord)
183
184
184instance Show UExp where
185instance Show UExp where
185 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]
186 show (UVar x) | x < 26 = [toEnum (x + fromEnum 'a')]
186 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
187 | otherwise = toEnum ((x `mod` 26) + fromEnum 'a') : show (x `div` 26)
187 show (UVal x) = show x
188 show (UVal x) = show x
189+-- show (UMax l r) = "max(" ++ show l ++ ", " ++ show r ++")"
188
190
189data UConstraint = ULT UExp UExp
191data UConstraint = ULT UExp UExp
190 | ULE UExp UExp
192 | ULE UExp UExp
src/Core/Typecheck.hs+4−4
@@ -89,7 +89,7 @@ check' holes ctxt env top = chk env top where
89 (v, cs) <- get
89 (v, cs) <- get
90 let Set su = normalise ctxt env st
90 let Set su = normalise ctxt env st
91 let Set tu = normalise ctxt env tt
91 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)
93 return (Bind n (Pi sv) (pToV n tv), Set (UVar v))
93 return (Bind n (Pi sv) (pToV n tv), Set (UVar v))
94 chk env (RBind n b sc)
94 chk env (RBind n b sc)
95 = do b' <- checkBinder b
95 = do b' <- checkBinder b
@@ -112,7 +112,7 @@ check' holes ctxt env top = chk env top where
112 (vv, vt) <- chk env v
112 (vv, vt) <- chk env v
113 let tv' = normalise ctxt env tv
113 let tv' = normalise ctxt env tv
114 let tt' = normalise ctxt env tt
114 let tt' = normalise ctxt env tt
115− convertsC ctxt env tv vt
115+ convertsC ctxt env vt tv
116 lift $ isSet ctxt env tt'
116 lift $ isSet ctxt env tt'
117 return (Let tv vv)
117 return (Let tv vv)
118 checkBinder (NLet t v)
118 checkBinder (NLet t v)
@@ -120,7 +120,7 @@ check' holes ctxt env top = chk env top where
120 (vv, vt) <- chk env v
120 (vv, vt) <- chk env v
121 let tv' = normalise ctxt env tv
121 let tv' = normalise ctxt env tv
122 let tt' = normalise ctxt env tt
122 let tt' = normalise ctxt env tt
123− convertsC ctxt env tv vt
123+ convertsC ctxt env vt tv
124 lift $ isSet ctxt env tt'
124 lift $ isSet ctxt env tt'
125 return (NLet tv vv)
125 return (NLet tv vv)
126 checkBinder (Hole t)
126 checkBinder (Hole t)
@@ -144,7 +144,7 @@ check' holes ctxt env top = chk env top where
144 (vv, vt) <- chk env v
144 (vv, vt) <- chk env v
145 let tv' = normalise ctxt env tv
145 let tv' = normalise ctxt env tv
146 let tt' = normalise ctxt env tt
146 let tt' = normalise ctxt env tt
147− convertsC ctxt env tv vt
147+ convertsC ctxt env vt tv
148 lift $ isSet ctxt env tt'
148 lift $ isSet ctxt env tt'
149 return (Guess tv vv)
149 return (Guess tv vv)
150 checkBinder (PVar t)
150 checkBinder (PVar t)
src/Idris/AbsSyntax.hs+6−4
@@ -29,6 +29,7 @@ defaultOpts = IOption 0 False False
29-- and syntax macros.
29-- and syntax macros.
30
30
31data IState = IState { tt_ctxt :: Context,
31data IState = IState { tt_ctxt :: Context,
32+ idris_constraints :: [(UConstraint, FC)],
32 idris_infixes :: [FixDecl],
33 idris_infixes :: [FixDecl],
33 idris_implicits :: Ctxt [PArg],
34 idris_implicits :: Ctxt [PArg],
34 idris_statics :: Ctxt [Bool],
35 idris_statics :: Ctxt [Bool],
@@ -47,7 +48,7 @@ data IState = IState { tt_ctxt :: Context,
47 errLine :: Maybe Int
48 errLine :: Maybe Int
48 }
49 }
49
50
50−idrisInit = IState initContext [] emptyContext emptyContext emptyContext
51+idrisInit = IState initContext [] [] emptyContext emptyContext emptyContext
51 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing
52 "" defaultOpts 6 [] [] [] [] [] [] [] [] Nothing
52
53
53-- The monad for the main REPL - reading and processing files and updating
54-- 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 } )
111updateContext :: (Context -> Context) -> Idris ()
112updateContext :: (Context -> Context) -> Idris ()
112updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
113updateContext f = do i <- get; put (i { tt_ctxt = f (tt_ctxt i) } )
113
114
114−addConstraints :: (Int, [UConstraint]) -> Idris ()
115+addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()
115−addConstraints (v, cs)
116+addConstraints fc (v, cs)
116 = do i <- get
117 = do i <- get
117 let ctxt = tt_ctxt i
118 let ctxt = tt_ctxt i
118 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
119 let ctxt' = ctxt { uconstraints = cs ++ uconstraints ctxt,
119 next_tvar = v }
120 next_tvar = v }
121+ let ics = zip cs (repeat fc) ++ idris_constraints i
120− put (i { tt_ctxt = ctxt' })
122+ put (i { tt_ctxt = ctxt', idris_constraints = ics })
121
123
122addDeferred :: [(Name, Type)] -> Idris ()
124addDeferred :: [(Name, Type)] -> Idris ()
123addDeferred ns = do mapM_ (\(n, t) -> updateContext (addTyDecl n (tidyNames [] t))) ns
125addDeferred 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)
53 ++ " with " ++ show (delab i y)
53 ++ " with " ++ show (delab i y)
54-- ++ "\n\t(" ++ pshow i e ++ ")"
54-- ++ "\n\t(" ++ pshow i e ++ ")"
55pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
55pshow i (IncompleteTerm t) = "Incomplete term " ++ show t
56+pshow i UniverseError = "Universe inconsistency"
56pshow i (At f e) = show f ++ ":" ++ pshow i e
57pshow i (At f e) = show f ++ ":" ++ pshow i e
57
58