--------------------------------------------------------------------------------
-- | Environments
--- data Env = Empty
--- | Upd Env (Ident,Val)
--- | Def [Decl] Env
--- | Sub Env (Name,Formula)
--- deriving Eq
-
data Ctxt = Empty
| Upd Ident Ctxt
| Sub Name Ctxt
| Def [Decl] Ctxt
deriving (Show,Eq)
-type Env = (Ctxt,[Val],[Formula])
+-- The Idents and Names in the Ctxt refer to the elements in the two
+-- lists. This is more efficient because acting on an environment now
+-- only need to affect the lists and not the whole context.
+type Env = (Ctxt,[Val],[Formula])
+
+empty :: Env
+empty = (Empty,[],[])
def :: [Decl] -> Env -> Env
def ds (rho,vs,fs) = (Def ds rho,vs,fs)
upd :: (Ident,Val) -> Env -> Env
upd (x,v) (rho,vs,fs) = (Upd x rho,v:vs,fs)
-empty :: Env
-empty = (Empty,[],[])
+upds :: [(Ident,Val)] -> Env -> Env
+upds xus rho = foldl (flip upd) rho xus
-upds :: Env -> [(Ident,Val)] -> Env
-upds rho [] = rho
-upds rho (xu:xus) = upds (upd xu rho) xus
+updsTele :: Tele -> [Val] -> Env -> Env
+updsTele tele vs = upds (zip (map fst tele) vs)
-updsTele :: Env -> Tele -> [Val] -> Env
-updsTele rho tele vs = upds rho (zip (map fst tele) vs)
-
-subs :: Env -> [(Name,Formula)] -> Env
-subs env [] = env
-subs (g,vs,fs) ((i,phi):iphis) = subs (Sub i g,vs,phi:fs) iphis
+subs :: [(Name,Formula)] -> Env -> Env
+subs iphis rho = foldl (flip sub) rho iphis
mapEnv :: (Val -> Val) -> (Formula -> Formula) -> Env -> Env
mapEnv f g (rho,vs,fs) = (rho,map f vs,map g fs)
Def ts e -> domCtxt e
Sub i e -> i : domCtxt e
--- TODO: Fix
-- Extract the context from the environment, used when printing holes
contextOfEnv :: Env -> [String]
-contextOfEnv rho = undefined -- case rho of
- -- Empty -> []
- -- Upd e (x, VVar n t) -> (n ++ " : " ++ show t) : contextOfEnv e
- -- Upd e (x, v) -> (x ++ " = " ++ show v) : contextOfEnv e
- -- Def ts e -> contextOfEnv e
- -- Sub e (i,phi) -> (show i ++ " = " ++ show phi) : contextOfEnv e
+contextOfEnv rho = case rho of
+ (Empty,_,_) -> []
+ (Upd x e,VVar n t:vs,fs) -> (n ++ " : " ++ show t) : contextOfEnv (e,vs,fs)
+ (Upd x e,v:vs,fs) -> (x ++ " = " ++ show v) : contextOfEnv (e,vs,fs)
+ (Def _ e,vs,fs) -> contextOfEnv (e,vs,fs)
+ (Sub i e,vs,phi:fs) -> (show i ++ " = " ++ show phi) : contextOfEnv (e,vs,fs)
--------------------------------------------------------------------------------
-- | Pretty printing
Var x -> text x
Con c es -> text c <+> showTers es
PCon c a es phis -> text c <+> braces (showTer a) <+> showTers es
- <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
+ <+> hsep (map ((char '@' <+>) . showFormula) phis)
Split f _ _ _ -> text f
Sum _ n _ -> text n
Undef{} -> text "undefined"
Ter t rho -> showTer1 t <+> showEnv True rho
VCon c us -> text c <+> showVals us
VPCon c a us phis -> text c <+> braces (showVal a) <+> showVals us
- <+> (hsep $ map ((char '@' <+>) . showFormula) phis)
+ <+> hsep (map ((char '@' <+>) . showFormula) phis)
VPi a l@(VLam x t b)
| "_" `isPrefixOf` x -> showVal a <+> text "->" <+> showVal1 b
| otherwise -> char '(' <> showLam v
showVals :: [Val] -> Doc
showVals = hsep . map showVal1
-
import Control.Applicative
import Data.List
import Data.Map (Map,(!),keys)
-import Data.Set (Set)
+import Data.Set (Set,isProperSubsetOf)
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Maybe
, b <- Set.toList (dnf psi) ]
fromDNF :: Set (Set (Name,Dir)) -> Formula
-fromDNF s = foldr orFormula (Dir Zero) (map (foldr andFormula (Dir One)) fs)
+fromDNF s = foldr (orFormula . foldr andFormula (Dir One)) (Dir Zero) fs
where xss = map Set.toList $ Set.toList s
fs = [ [ if d == Zero then NegAtom n else Atom n | (n,d) <- xs ] | xs <- xss ]
merge a b =
let as = Set.toList a
bs = Set.toList b
- in Set.fromList [ ai | ai <- as, not (any (\bj -> bj `Set.isProperSubsetOf` ai) bs) ] `Set.union`
- Set.fromList [ bi | bi <- bs, not (any (\aj -> aj `Set.isProperSubsetOf` bi) as) ]
+ in Set.fromList [ ai | ai <- as, not (any (`isProperSubsetOf` ai) bs) ] `Set.union`
+ Set.fromList [ bi | bi <- bs, not (any (`isProperSubsetOf` bi) as) ]
-- evalFormula :: Formula -> Face -> Formula
-- evalFormula phi alpha =
showSystem :: Show a => System a -> String
showSystem ts =
- "[ " ++ concat (intersperse ", " [ showFace alpha ++ " -> " ++ show u
- | (alpha,u) <- Map.toList ts ]) ++ " ]"
+ "[ " ++ intercalate ", " [ showFace alpha ++ " -> " ++ show u
+ | (alpha,u) <- Map.toList ts ] ++ " ]"
insertSystem :: Face -> a -> System a -> System a
insertSystem alpha v ts = case find (comparable alpha) (Map.keys ts) of
Nothing -> Map.insert alpha v ts
insertsSystem :: [(Face, a)] -> System a -> System a
-insertsSystem faces us =
- foldr (\(alpha, ualpha) -> insertSystem alpha ualpha) us faces
+insertsSystem faces us = foldr (uncurry insertSystem) us faces
mkSystem :: [(Face, a)] -> System a
mkSystem = flip insertsSystem Map.empty
let j = fresh rho
in VPath j (eval (sub (i,Atom j) rho) t)
Trans u v -> transLine (eval rho u) (eval rho v)
- AppFormula e phi -> (eval rho e) @@ (evalFormula rho phi)
+ AppFormula e phi -> eval rho e @@ evalFormula rho phi
Comp a t0 ts -> compLine (eval rho a) (eval rho t0) (evalSystem rho ts)
Glue a ts -> glue (eval rho a) (evalSystem rho ts)
GlueElem a ts -> glueElem (eval rho a) (evalSystem rho ts)
app u v = case (u,v) of
(Ter (Lam x _ t) e,_) -> eval (upd (x,v) e) t
(Ter (Split _ _ _ nvs) e,VCon c vs) -> case lookupBranch c nvs of
- Just (OBranch _ xs t) -> eval (upds e (zip xs vs)) t
+ Just (OBranch _ xs t) -> eval (upds (zip xs vs) e) t
_ -> error $ "app: missing case in split for " ++ c
(Ter (Split _ _ _ nvs) e,VPCon c _ us phis) -> case lookupBranch c nvs of
- Just (PBranch _ xs is t) -> eval (subs (upds e (zip xs us)) (zip is phis)) t
+ Just (PBranch _ xs is t) -> eval (subs (zip is phis) (upds (zip xs us) e)) t
_ -> error $ "app: missing case in split for " ++ c
(Ter (Split _ _ ty hbr) e,VComp a w ws) -> case eval e ty of
VPi _ f -> let j = fresh (e,v)
-- TODO: is this correct? Double check!
Just (tele,is,ts) | eps `Map.member` vs -> vs ! eps
| otherwise -> VPCon c a us phis
- where rho' = subs (updsTele rho tele us) (zip is phis)
+ where rho' = subs (zip is phis) (updsTele tele us rho)
vs = evalSystem rho' ts
Nothing -> error "pcon"
-- pcon c a us phi = VPCon c a us phi
k = fresh (v0,v1,Atom i)
transp alpha w = trans i (v0 `face` alpha) (w @@ k)
ws' = mapWithKey transp ws
- _ | otherwise -> error $ "trans not implemented for v0 = " ++ show v0
- ++ "\n and v1 = " ++ show v1
+ _ -> error $ "trans not implemented for v0 = " ++ show v0
+ ++ "\n and v1 = " ++ show v1
transNeg :: Name -> Val -> Val -> Val
transNeg i a u = trans i (a `sym` i) u
ls' = mapWithKey (\gamma isoG ->
VPath i $ squeeze i (b `face` gamma)
- ((hisoFun isoG) `app` (us' ! gamma)))
+ (hisoFun isoG `app` (us' ! gamma)))
hisos'
bi1 = b `face` (i ~> 1)
vi1' = compLine bi1 vi1 ls'
theta = genFill i ei a vs
t = genComp i ei a vs
theta' = transFillNeg i ei t
- ws = insertSystem (j ~> 1) theta' $
- insertSystem (j ~> 0) theta $ vs
+ ws = insertSystem (j ~> 1) theta' $ insertSystem (j ~> 0) theta vs
theta'' = genCompNeg i ei t ws
normal _ = fromDNF . dnf
instance Normal a => Normal (Map k a) where
- normal ns us = Map.map (normal ns) us
+ normal ns = Map.map (normal ns)
instance (Normal a,Normal b) => Normal (a,b) where
normal ns (u,v) = (normal ns u,normal ns v)
(normal ns u,normal ns v,normal ns w, normal ns x)
instance Normal a => Normal [a] where
- normal ns us = map (normal ns) us
+ normal ns = map (normal ns)
\r
addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv\r
addBranch nvs env (TEnv ns ind rho v) =\r
- TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds rho nvs) v\r
+ TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v\r
\r
addDecls :: [Decl] -> TEnv -> TEnv\r
addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v\r
checkTele tele\r
rho <- asks env\r
unless (all (`elem` is) (domain ts)) $\r
- throwError $ "names in path label system" -- TODO\r
+ throwError "names in path label system" -- TODO\r
mapM_ checkFresh is\r
let iis = zip is (map Atom is)\r
local (addSubs iis . addTele tele) $ do\r
checkSystemWith ts $ \alpha talpha ->\r
- local (faceEnv alpha) $ do\r
+ local (faceEnv alpha) $\r
-- NB: the type doesn't depend on is\r
check (Ter t rho) talpha\r
rho' <- asks env\r
(VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do\r
check vb r\r
unlessM ((phi,psi) === (phi',psi')) $\r
- throwError $ "GlueLineElem: formulas don't match"\r
+ throwError "GlueLineElem: formulas don't match"\r
_ -> do\r
v <- infer t\r
unlessM (v === a) $\r
let us = mkVars ns' tele nu\r
vus = map snd us\r
js' = map Atom js\r
- vts = evalSystem (subs (upds nu us) (zip is js')) ts\r
+ vts = evalSystem (subs (zip is js') (upds us nu)) ts\r
vgts = intersectionWith app (border g vts) vts\r
local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do\r
check (app f (VPCon c va vus js')) e\r
checkFormula phi = do\r
rho <- asks env\r
let dom = domainEnv rho\r
- unless (all (\x -> x `elem` dom) (support phi)) $\r
+ unless (all (`elem` dom) (support phi)) $\r
throwError $ "checkFormula: " ++ show phi\r
\r
checkFresh :: Name -> Typing ()\r
(throwError ("Keys don't match in " ++ show es ++ " and " ++ show us))\r
check va u\r
let vu = eval rho u\r
- checkSystemsWith ts us (\_ -> check)\r
+ checkSystemsWith ts us (const check)\r
let vus = evalSystem rho us\r
checkCompSystem vus\r
checkSystemsWith ves vus (\alpha eA vuA ->\r
projects / cubicaltt.git / commitdiff