a854972 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Small reduction in constraint generation

a854972Edwin Brady10 years ago

libs/effects/Effects.idr+4−4

compare with master

unifiedsplit

@@ -448,19 +448,19 @@ runEnv env prog = eff env prog (\r, env => pure (r ** env))

448

449-- ----------------------------------------------- [ some higher order things ]

450

451−mapE : (a -> {xs} EffM m b) -> List a -> {xs} EffM m (List b)

451+mapE : (a -> EffM m b xs (\_ => xs)) -> List a -> EffM m (List b) xs (\_ => xs)

452mapE f [] = pure []

453mapE f (x :: xs) = [| f x :: mapE f xs |]

454

455

456−mapVE : (a -> {xs} EffM m b) ->

456+mapVE : (a -> EffM m b xs (\_ => xs)) ->

457 Vect n a ->

458− {xs} EffM m (Vect n b)

458+ EffM m (Vect n b) xs (\_ => xs)

459mapVE f [] = pure []

460mapVE f (x :: xs) = [| f x :: mapVE f xs |]

461

462

463−when : Bool -> Lazy ({xs} EffM m ()) -> {xs} EffM m ()

463+when : Bool -> Lazy (EffM m () xs (\_ => xs)) -> EffM m () xs (\_ => xs)

464when True e = Force e

465when False e = pure ()

466

libs/effects/effects.ipkg+1−1

@@ -1,6 +1,6 @@

1package effects

3−opts = "--nobasepkgs -i ../prelude -i ../base"

3+opts = "--nobasepkgs --typeintype -i ../prelude -i ../base"

5modules = Effects

6 , Effect.Default

src/Idris/AbsSyntax.hs+7−5

@@ -693,11 +693,13 @@ updateContext f = do i <- getIState; putIState $ (i { tt_ctxt = f (tt_ctxt i) }

693

694addConstraints :: FC -> (Int, [UConstraint]) -> Idris ()

695addConstraints fc (v, cs)

696+ = do tit <- typeInType

697+ when (not tit) $ do

696− = do i <- getIState

698+ i <- getIState

697− let ctxt = tt_ctxt i

699+ let ctxt = tt_ctxt i

698− let ctxt' = ctxt { next_tvar = v }

700+ let ctxt' = ctxt { next_tvar = v }

699− let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)

701+ let ics = insertAll (zip cs (repeat fc)) (idris_constraints i)

700− putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

702+ putIState $ i { tt_ctxt = ctxt', idris_constraints = ics }

701 where

703 where

702 insertAll [] c = c

704 insertAll [] c = c

703 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics

705 insertAll ((ULE (UVal 0) _, fc) : cs) ics = insertAll cs ics

src/Idris/Core/Constraints.hs+31−1

@@ -15,16 +15,46 @@ import Control.Monad.State.Strict

15import Data.List ( partition )

16import qualified Data.Map.Strict as M

17import qualified Data.Set as S

18+import Debug.Trace

19-- | Check that a list of universe constraints can be satisfied.

20-- | Check that a list of universe constraints can be satisfied.

20ucheck :: S.Set ConstraintFC -> TC ()

21ucheck :: S.Set ConstraintFC -> TC ()

21−ucheck = void . solve 10 . S.filter (not . ignore)

22+ucheck = void . solve 10 . S.filter (not . ignore) . dropUnused

22 where

23 where

23 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

24 -- TODO: remove the first ignore clause once Idris.Core.Binary:598 is dealt with

24 ignore (ConstraintFC c _) | any (== Var [] (-1)) (varsIn c) = True

25 ignore (ConstraintFC c _) | any (== Var [] (-1)) (varsIn c) = True

25 ignore (ConstraintFC (ULE a b) _) = a == b

26 ignore (ConstraintFC (ULE a b) _) = a == b

26 ignore _ = False

27 ignore _ = False

29+dropUnused :: S.Set ConstraintFC -> S.Set ConstraintFC

30+dropUnused xs = let cs = S.toList xs

31+ onlhs = countLHS M.empty cs in

32+ addIfUsed S.empty onlhs cs

33+ where

34+ -- Count the number of times a variable occurs on the LHS of a constraint

35+ countLHS ms [] = ms

36+ countLHS ms (c : cs) = let lhvar = getLHS (uconstraint c)

37+ num = case M.lookup lhvar ms of

38+ Nothing -> 1

39+ Just v -> v + 1 in

40+ countLHS (M.insert lhvar num ms) cs

41+

42+ -- Only keep a constraint if the variable on the RHS is used elsewhere

43+ -- on the LHS of a constraint

44+ addIfUsed cs' lhs [] = cs'

45+ addIfUsed cs' lhs (c : cs)

46+ = let rhvar = getRHS (uconstraint c) in

47+ case M.lookup rhvar lhs of

48+ Nothing -> addIfUsed cs' lhs cs

49+ Just v -> addIfUsed (S.insert c cs') lhs cs

50+

51+ getLHS (ULT x _) = x

52+ getLHS (ULE x _) = x

53+

54+ getRHS (ULT _ x) = x

55+ getRHS (ULE _ x) = x

56+

57+

28data Var = Var String Int

58data Var = Var String Int

29 deriving (Eq, Ord, Show)

59 deriving (Eq, Ord, Show)

src/Idris/Core/Typecheck.hs+33−30

@@ -86,7 +86,7 @@ check ctxt env tm

86 = evalStateT (check' True [] ctxt env tm) (0, [])

88check' :: Bool -> String -> Context -> Env -> Raw -> StateT UCs TC (Term, Type)

89−check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

89+check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top where

91 smaller (UType NullType) _ = UType NullType

92 smaller _ (UType NullType) = UType NullType

@@ -98,8 +98,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

98 | otherwise = Complete

100 chk :: Type -> -- uniqueness level

101+ Maybe UExp -> -- universe for kind

101 Env -> Raw -> StateT UCs TC (Term, Type)

102 Env -> Raw -> StateT UCs TC (Term, Type)

102− chk u env (Var n)

103+ chk u lvl env (Var n)

103 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

104 | Just (i, ty) <- lookupTyEnv n env = return (P Bound n ty, ty)

104 -- If we're elaborating, we don't want the private names; if we're

105 -- If we're elaborating, we don't want the private names; if we're

105 -- checking an already elaborated term, we do

106 -- checking an already elaborated term, we do

@@ -109,9 +110,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

109 | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

110 | [P nt n' ty] <- lookupP_all (not holes) True n ctxt

110 = return (P nt n' ty, ty)

111 = return (P nt n' ty, ty)

111 | otherwise = do lift $ tfail $ NoSuchVariable n

112 | otherwise = do lift $ tfail $ NoSuchVariable n

112− chk u env ap@(RApp f RType) | not holes

113+ chk u lvl env ap@(RApp f RType) | not holes

113 -- special case to reduce constraintss

114 -- special case to reduce constraintss

114− = do (fv, fty) <- chk u env f

115+ = do (fv, fty) <- chk u Nothing env f

115 let fty' = case uniqueBinders (map fst env) (finalise fty) of

116 let fty' = case uniqueBinders (map fst env) (finalise fty) of

116 ty@(Bind x (Pi i s k) t) -> ty

117 ty@(Bind x (Pi i s k) t) -> ty

117 _ -> uniqueBinders (map fst env)

118 _ -> uniqueBinders (map fst env)

@@ -126,21 +127,21 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

126 (Bind x (Let (TType v') (TType (UVar tcns v))) t)

127 (Bind x (Let (TType v') (TType (UVar tcns v))) t)

127 return (App Complete fv (TType (UVar tcns v)), apty)

128 return (App Complete fv (TType (UVar tcns v)), apty)

128 Bind x (Pi i s k) t ->

129 Bind x (Pi i s k) t ->

129− do (av, aty) <- chk u env RType

130+ do (av, aty) <- chk u Nothing env RType

130 convertsC ctxt env aty s

131 convertsC ctxt env aty s

131 let apty = simplify initContext env

132 let apty = simplify initContext env

132 (Bind x (Let aty av) t)

133 (Bind x (Let aty av) t)

133 return (App astate fv av, apty)

134 return (App astate fv av, apty)

134 t -> lift $ tfail $ NonFunctionType fv fty

135 t -> lift $ tfail $ NonFunctionType fv fty

135− chk u env ap@(RApp f a)

136+ chk u lvl env ap@(RApp f a)

136− = do (fv, fty) <- chk u env f

137+ = do (fv, fty) <- chk u Nothing env f

137 let fty' = case uniqueBinders (map fst env) (finalise fty) of

138 let fty' = case uniqueBinders (map fst env) (finalise fty) of

138 ty@(Bind x (Pi i s k) t) -> ty

139 ty@(Bind x (Pi i s k) t) -> ty

139 _ -> uniqueBinders (map fst env)

140 _ -> uniqueBinders (map fst env)

140 $ case hnf ctxt env fty of

141 $ case hnf ctxt env fty of

141 ty@(Bind x (Pi i s k) t) -> ty

142 ty@(Bind x (Pi i s k) t) -> ty

142 _ -> normalise ctxt env fty

143 _ -> normalise ctxt env fty

143− (av, aty) <- chk u env a

144+ (av, aty) <- chk u Nothing env a

144 case fty' of

145 case fty' of

145 Bind x (Pi i s k) t ->

146 Bind x (Pi i s k) t ->

146 do convertsC ctxt env aty s

147 do convertsC ctxt env aty s

@@ -148,13 +149,13 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

148 (Bind x (Let aty av) t)

149 (Bind x (Let aty av) t)

149 return (App astate fv av, apty)

150 return (App astate fv av, apty)

150 t -> lift $ tfail $ NonFunctionType fv fty

151 t -> lift $ tfail $ NonFunctionType fv fty

151− chk u env RType

152+ chk u lvl env RType

152 | holes = return (TType (UVal 0), TType (UVal 0))

153 | holes = return (TType (UVal 0), TType (UVal 0))

153 | otherwise = do (v, cs) <- get

154 | otherwise = do (v, cs) <- get

154 let c = ULT (UVar tcns v) (UVar tcns (v+1))

155 let c = ULT (UVar tcns v) (UVar tcns (v+1))

155 put (v+2, (c:cs))

156 put (v+2, (c:cs))

156 return (TType (UVar tcns v), TType (UVar tcns (v+1)))

157 return (TType (UVar tcns v), TType (UVar tcns (v+1)))

157− chk u env (RUType un)

158+ chk u lvl env (RUType un)

158 | holes = return (UType un, TType (UVal 0))

159 | holes = return (UType un, TType (UVal 0))

159 | otherwise = do -- TODO! Issue #1715 on the issue tracker.

160 | otherwise = do -- TODO! Issue #1715 on the issue tracker.

160 -- https://github.com/idris-lang/Idris-dev/issues/1715

161 -- https://github.com/idris-lang/Idris-dev/issues/1715

@@ -163,8 +164,8 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

163 -- put (v+2, (c:cs))

164 -- put (v+2, (c:cs))

164 -- return (TType (UVar v), TType (UVar (v+1)))

165 -- return (TType (UVar v), TType (UVar (v+1)))

165 return (UType un, TType (UVal 0))

166 return (UType un, TType (UVal 0))

166− chk u env (RConstant Forgot) = return (Erased, Erased)

167+ chk u lvl env (RConstant Forgot) = return (Erased, Erased)

167− chk u env (RConstant c) = return (Constant c, constType c)

168+ chk u lvl env (RConstant c) = return (Constant c, constType c)

168 where constType (I _) = Constant (AType (ATInt ITNative))

169 where constType (I _) = Constant (AType (ATInt ITNative))

169 constType (BI _) = Constant (AType (ATInt ITBig))

170 constType (BI _) = Constant (AType (ATInt ITBig))

170 constType (Fl _) = Constant (AType ATFloat)

171 constType (Fl _) = Constant (AType ATFloat)

@@ -177,13 +178,15 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

177 constType TheWorld = Constant WorldType

178 constType TheWorld = Constant WorldType

178 constType Forgot = Erased

179 constType Forgot = Erased

179 constType _ = TType (UVal 0)

180 constType _ = TType (UVal 0)

180− chk u env (RBind n (Pi i s k) t)

181+ chk u lvl env (RBind n (Pi i s k) t)

181− = do (sv, st) <- chk u env s

182+ = do (sv, st) <- chk u Nothing env s

182 (v, cs) <- get

183 (v, cs) <- get

183− (kv, kt) <- chk u env k -- no need to validate these constraints, they are independent

184+ (kv, kt) <- chk u Nothing env k -- no need to validate these constraints, they are independent

184 put (v+1, cs)

185 put (v+1, cs)

186+ let maxu = case lvl of

185− let maxu = UVar tcns v

187+ Nothing -> UVar tcns v

188+ Just v' -> v'

186− (tv, tt) <- chk st ((n, Pi i sv kv) : env) t

189+ (tv, tt) <- chk st (Just maxu) ((n, Pi i sv kv) : env) t

187

190

188-- convertsC ctxt env st (TType maxu)

191-- convertsC ctxt env st (TType maxu)

189-- convertsC ctxt env tt (TType maxu)

192-- convertsC ctxt env tt (TType maxu)

@@ -219,25 +222,25 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

219 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)

222 mostUnique (Pi _ _ pk : es) k = mostUnique es (smaller pk k)

220 mostUnique (_ : es) k = mostUnique es k

223 mostUnique (_ : es) k = mostUnique es k

221

224

222− chk u env (RBind n b sc)

225+ chk u lvl env (RBind n b sc)

223 = do (b', bt') <- checkBinder b

226 = do (b', bt') <- checkBinder b

224− (scv, sct) <- chk (smaller bt' u) ((n, b'):env) sc

227+ (scv, sct) <- chk (smaller bt' u) Nothing ((n, b'):env) sc

225 discharge n b' bt' (pToV n scv) (pToV n sct)

228 discharge n b' bt' (pToV n scv) (pToV n sct)

226 where checkBinder (Lam t)

229 where checkBinder (Lam t)

227− = do (tv, tt) <- chk u env t

230+ = do (tv, tt) <- chk u Nothing env t

228 let tv' = normalise ctxt env tv

231 let tv' = normalise ctxt env tv

229 convType tcns ctxt env tt

232 convType tcns ctxt env tt

230 return (Lam tv, tt)

233 return (Lam tv, tt)

231 checkBinder (Let t v)

234 checkBinder (Let t v)

232− = do (tv, tt) <- chk u env t

235+ = do (tv, tt) <- chk u Nothing env t

233− (vv, vt) <- chk u env v

236+ (vv, vt) <- chk u Nothing env v

234 let tv' = normalise ctxt env tv

237 let tv' = normalise ctxt env tv

235 convertsC ctxt env vt tv

238 convertsC ctxt env vt tv

236 convType tcns ctxt env tt

239 convType tcns ctxt env tt

237 return (Let tv vv, tt)

240 return (Let tv vv, tt)

238 checkBinder (NLet t v)

241 checkBinder (NLet t v)

239− = do (tv, tt) <- chk u env t

242+ = do (tv, tt) <- chk u Nothing env t

240− (vv, vt) <- chk u env v

243+ (vv, vt) <- chk u Nothing env v

241 let tv' = normalise ctxt env tv

244 let tv' = normalise ctxt env tv

242 convertsC ctxt env vt tv

245 convertsC ctxt env vt tv

243 convType tcns ctxt env tt

246 convType tcns ctxt env tt

@@ -245,33 +248,33 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) env top where

245 checkBinder (Hole t)

248 checkBinder (Hole t)

246 | not holes = lift $ tfail (IncompleteTerm undefined)

249 | not holes = lift $ tfail (IncompleteTerm undefined)

247 | otherwise

250 | otherwise

248− = do (tv, tt) <- chk u env t

251+ = do (tv, tt) <- chk u Nothing env t

249 let tv' = normalise ctxt env tv

252 let tv' = normalise ctxt env tv

250 convType tcns ctxt env tt

253 convType tcns ctxt env tt

251 return (Hole tv, tt)

254 return (Hole tv, tt)

252 checkBinder (GHole i ns t)

255 checkBinder (GHole i ns t)

253− = do (tv, tt) <- chk u env t

256+ = do (tv, tt) <- chk u Nothing env t

254 let tv' = normalise ctxt env tv

257 let tv' = normalise ctxt env tv

255 convType tcns ctxt env tt

258 convType tcns ctxt env tt

256 return (GHole i ns tv, tt)

259 return (GHole i ns tv, tt)

257 checkBinder (Guess t v)

260 checkBinder (Guess t v)

258 | not holes = lift $ tfail (IncompleteTerm undefined)

261 | not holes = lift $ tfail (IncompleteTerm undefined)

259 | otherwise

262 | otherwise

260− = do (tv, tt) <- chk u env t

263+ = do (tv, tt) <- chk u Nothing env t

261− (vv, vt) <- chk u env v

264+ (vv, vt) <- chk u Nothing env v

262 let tv' = normalise ctxt env tv

265 let tv' = normalise ctxt env tv

263 convertsC ctxt env vt tv

266 convertsC ctxt env vt tv

264 convType tcns ctxt env tt

267 convType tcns ctxt env tt

265 return (Guess tv vv, tt)

268 return (Guess tv vv, tt)

266 checkBinder (PVar t)

269 checkBinder (PVar t)

267− = do (tv, tt) <- chk u env t

270+ = do (tv, tt) <- chk u Nothing env t

268 let tv' = normalise ctxt env tv

271 let tv' = normalise ctxt env tv

269 convType tcns ctxt env tt

272 convType tcns ctxt env tt

270 -- Normalised version, for erasure purposes (it's easier

273 -- Normalised version, for erasure purposes (it's easier

271 -- to tell if it's a collapsible variable)

274 -- to tell if it's a collapsible variable)

272 return (PVar tv, tt)

275 return (PVar tv, tt)

273 checkBinder (PVTy t)

276 checkBinder (PVTy t)

274− = do (tv, tt) <- chk u env t

277+ = do (tv, tt) <- chk u Nothing env t

275 let tv' = normalise ctxt env tv

278 let tv' = normalise ctxt env tv

276 convType tcns ctxt env tt

279 convType tcns ctxt env tt

277 return (PVTy tv, tt)

280 return (PVTy tv, tt)

src/Idris/Elab/Clause.hs+2−1

@@ -735,8 +735,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

735

736 ctxt <- getContext

737 let constv = next_tvar ctxt

738+ tit <- typeInType

738 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

739 case LState.runStateT (convertsC ctxt [] crhsty clhsty) (constv, []) of

739− OK (_, cs) -> when (PEGenerated `notElem` opts) $ do

740+ OK (_, cs) -> when (PEGenerated `notElem` opts && not tit) $ do

740 addConstraints fc cs

741 addConstraints fc cs

741 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

742 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

742 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

743 logElab 6 $ "CONSTRAINTS ADDED: " ++ show cs ++ "\n" ++ show (clhsty, crhsty)

src/Idris/Elab/Data.hs+9−7

@@ -281,13 +281,15 @@ addParamConstraints fc ps cty cons

281 where

282 constraintTy (Bind n (Pi _ ty _) sc)

283 = case getRetTy ty of

284+ TType avar -> do tit <- typeInType

285+ when (not tit) $ do

284− TType avar -> do ctxt <- getContext

286+ ctxt <- getContext

285− let tv = next_tvar ctxt

287+ let tv = next_tvar ctxt

286− let con = if n `elem` pnames

288+ let con = if n `elem` pnames

287− then ULE avar cvar

289+ then ULE avar cvar

288− else ULT avar cvar

290+ else ULT avar cvar

289− addConstraints fc (tv, [con])

291+ addConstraints fc (tv, [con])

290− addIBC (IBCConstraint fc con)

292+ addIBC (IBCConstraint fc con)

291 _ -> return ()

293 _ -> return ()

292 constraintTy t = return ()

294 constraintTy t = return ()

293

295

src/Idris/Elab/Utils.hs+3−1

@@ -46,7 +46,9 @@ recheckC_borrowing uniq_check addConstrs bs tcns fc mkerr env t

46 Error e -> tfail (At fc (mkerr e))

47 OK x -> return x

48 logElab 6 $ "CONSTRAINTS ADDED: " ++ show (tm, ty, cs)

49+ tit <- typeInType

50+ when (not tit && addConstrs) $

49− when addConstrs $ do addConstraints fc cs

51+ do addConstraints fc cs

50 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

52 mapM_ (\c -> addIBC (IBCConstraint fc c)) (snd cs)

51 mapM_ (checkDeprecated fc) (allTTNames tm)

53 mapM_ (checkDeprecated fc) (allTTNames tm)

52 mapM_ (checkDeprecated fc) (allTTNames ty)

54 mapM_ (checkDeprecated fc) (allTTNames ty)

src/Idris/REPL.hs+1−1

@@ -1047,7 +1047,7 @@ process fn Universes

1047 let cs = idris_constraints i

1048 let cslist = S.toAscList cs

1049-- iputStrLn $ showSep "\n" (map show cs)

1050− iputStrLn $ show (map uconstraint cslist)

1050+ iputStrLn $ showSep "\n" (map show cslist)

1051 let n = length cslist

1052 iputStrLn $ "(" ++ show n ++ " constraints)"

1053 case ucheck cs of

test/totality014/expected+3−4

@@ -1,9 +1,8 @@

1−totality014.idr:6:9:Universe inconsistency.

1+totality014.idr:1:6:Universe inconsistency.

2− Working on: ./totality014.idr.u

2+ Working on: ./totality014.idr.w

3 Old domain: (5,5)

4 New domain: (5,4)

5 Involved constraints:

6− ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

6+ ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

7− ConstraintFC {uconstraint = ./totality014.idr.u < ./totality014.idr.v, ufc = totality014.idr:1:6}

8 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

7 ConstraintFC {uconstraint = ./totality014.idr.w < ./totality014.idr.u, ufc = totality014.idr:1:6}

9 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

8 ConstraintFC {uconstraint = ./totality014.idr.u <= ./totality014.idr.w, ufc = totality014.idr:6:9}

test/universes002/expected+5−5

@@ -1,9 +1,9 @@

1universes002.idr:45:9:Universe inconsistency.

2− Working on: ./universes002.idr.c7

2+ Working on: ./universes002.idr.b1

3 Old domain: (5,5)

4 New domain: (5,4)

5 Involved constraints:

6− ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}

6+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9}

7− ConstraintFC {uconstraint = ./universes002.idr.c7 < ./universes002.idr.d7, ufc = universes002.idr:15:6}

7+ ConstraintFC {uconstraint = ./universes002.idr.b1 < ./universes002.idr.c1, ufc = universes002.idr:3:6}

8− ConstraintFC {uconstraint = ./universes002.idr.e7 < ./universes002.idr.c7, ufc = universes002.idr:15:6}

8+ ConstraintFC {uconstraint = ./universes002.idr.b1 <= ./universes002.idr.e7, ufc = universes002.idr:45:9}

9− ConstraintFC {uconstraint = ./universes002.idr.c7 <= ./universes002.idr.d1, ufc = universes002.idr:45:9}

9+ ConstraintFC {uconstraint = ./universes002.idr.d1 <= ./universes002.idr.b1, ufc = universes002.idr:3:6}