From: Anders Date: Wed, 6 May 2015 11:57:06 +0000 (+0200) Subject: Cleaning X-Git-Url: https://git.ak3n.com/?a=commitdiff_plain;h=bb5d62920b88046ea25fe6e8db3cc5d294c216c6;p=cubicaltt.git Cleaning --- diff --git a/CTT.hs b/CTT.hs index c1c1a3a..0d86209 100644 --- a/CTT.hs +++ b/CTT.hs @@ -246,19 +246,19 @@ isCon _ = False -------------------------------------------------------------------------------- -- | 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) @@ -269,19 +269,14 @@ sub (i,phi) (rho,vs,fs) = (Sub i rho,vs,phi: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) @@ -303,15 +298,14 @@ domainEnv (rho,_,_) = domCtxt rho 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 @@ -364,7 +358,7 @@ showTer v = case v of 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" @@ -415,7 +409,7 @@ showVal v = case v of 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 @@ -474,4 +468,3 @@ showVal1 v = case v of showVals :: [Val] -> Doc showVals = hsep . map showVal1 - diff --git a/Connections.hs b/Connections.hs index e6a5267..9a01639 100644 --- a/Connections.hs +++ b/Connections.hs @@ -5,7 +5,7 @@ module Connections where 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 @@ -206,7 +206,7 @@ dnf (phi :/\: psi) = , 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 ] @@ -214,8 +214,8 @@ merge :: Set (Set (Name,Dir)) -> Set (Set (Name,Dir)) -> Set (Set (Name,Dir)) 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 = @@ -369,8 +369,8 @@ type System a = Map Face a 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 @@ -379,8 +379,7 @@ 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 diff --git a/Eval.hs b/Eval.hs index 10f63fb..b24a98a 100644 --- a/Eval.hs +++ b/Eval.hs @@ -160,7 +160,7 @@ eval rho v = case v of 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) @@ -196,10 +196,10 @@ app :: Val -> Val -> Val 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) @@ -284,7 +284,7 @@ pcon c a@(Ter (Sum _ _ lbls) rho) us phis = case lookupPLabel c lbls of -- 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 @@ -332,8 +332,8 @@ trans i v0 v1 = case (v0,v1) of 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 @@ -506,7 +506,7 @@ transGlue i b hisos wi0 = glueElem vi1'' usi1 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' @@ -798,8 +798,7 @@ eqLemma e ts a = (t,VPath j theta'') 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 @@ -956,7 +955,7 @@ instance Normal Formula where 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) @@ -969,4 +968,4 @@ instance (Normal a,Normal b,Normal c,Normal d) => Normal (a,b,c,d) where (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) diff --git a/TypeChecker.hs b/TypeChecker.hs index 99c1af3..e55ff67 100644 --- a/TypeChecker.hs +++ b/TypeChecker.hs @@ -77,7 +77,7 @@ addType (x,a) tenv@(TEnv _ _ rho _) = addTypeVal (x,eval rho a) tenv addBranch :: [(Ident,Val)] -> Env -> TEnv -> TEnv addBranch nvs env (TEnv ns ind rho v) = - TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds rho nvs) v + TEnv ([n | (_,VVar n _) <- nvs] ++ ns) ind (upds nvs rho) v addDecls :: [Decl] -> TEnv -> TEnv addDecls d (TEnv ns ind rho v) = TEnv ns ind (def d rho) v @@ -157,12 +157,12 @@ check a t = case (a,t) of checkTele tele rho <- asks env unless (all (`elem` is) (domain ts)) $ - throwError $ "names in path label system" -- TODO + throwError "names in path label system" -- TODO mapM_ checkFresh is let iis = zip is (map Atom is) local (addSubs iis . addTele tele) $ do checkSystemWith ts $ \alpha talpha -> - local (faceEnv alpha) $ do + local (faceEnv alpha) $ -- NB: the type doesn't depend on is check (Ter t rho) talpha rho' <- asks env @@ -215,7 +215,7 @@ check a t = case (a,t) of (VGlueLine vb phi psi,GlueLineElem r phi' psi') -> do check vb r unlessM ((phi,psi) === (phi',psi')) $ - throwError $ "GlueLineElem: formulas don't match" + throwError "GlueLineElem: formulas don't match" _ -> do v <- infer t unlessM (v === a) $ @@ -311,7 +311,7 @@ checkBranch (PLabel _ tele is ts,nu) f (PBranch c ns js e) g va = do let us = mkVars ns' tele nu vus = map snd us js' = map Atom js - vts = evalSystem (subs (upds nu us) (zip is js')) ts + vts = evalSystem (subs (zip is js') (upds us nu)) ts vgts = intersectionWith app (border g vts) vts local (addSubs (zip js js') . addBranch (zip ns vus) nu) $ do check (app f (VPCon c va vus js')) e @@ -326,7 +326,7 @@ checkFormula :: Formula -> Typing () checkFormula phi = do rho <- asks env let dom = domainEnv rho - unless (all (\x -> x `elem` dom) (support phi)) $ + unless (all (`elem` dom) (support phi)) $ throwError $ "checkFormula: " ++ show phi checkFresh :: Name -> Typing () @@ -427,7 +427,7 @@ infer e = case e of (throwError ("Keys don't match in " ++ show es ++ " and " ++ show us)) check va u let vu = eval rho u - checkSystemsWith ts us (\_ -> check) + checkSystemsWith ts us (const check) let vus = evalSystem rho us checkCompSystem vus checkSystemsWith ves vus (\alpha eA vuA ->