remove dead code

This commit is contained in:
Krasimir Angelov
2026-02-05 14:57:08 +01:00
parent 3b3979bf42
commit 19774ebcd3
3 changed files with 14 additions and 93 deletions
+14 -2
View File
@@ -89,7 +89,7 @@ sizeTerm t = case t of
R r -> 1 + sum [1 + sizeTerm a | (_,(_,a)) <- r] -- label counts as 1, type ignored
RecType r -> 1 + sum [1 + sizeTerm a | (_,_,a) <- r] -- label counts as 1
P t i -> 2 + sizeTerm t
T _ cc -> 1 + sum [1 + sizeTerm (patt2term p) + sizeTerm v | (p,v) <- cc]
T _ cc -> 1 + sum [1 + sizePatt p + sizeTerm v | (p,v) <- cc]
V ty cc -> 1 + sizeTerm ty + sum [1 + sizeTerm v | v <- cc]
Let (x,(mt,a)) b -> 2 + maybe 0 sizeTerm mt + sizeTerm a + sizeTerm b
C s1 s2 -> 1 + sizeTerm s1 + sizeTerm s2
@@ -99,13 +99,25 @@ sizeTerm t = case t of
Strs tt -> 1 + sum (map sizeTerm tt)
_ -> 1
sizePatt :: Patt -> Int
sizePatt p = case p of
PC c pp -> 1 + sum (map sizePatt pp)
PP c pp -> 1 + sum (map sizePatt pp)
PR r -> 1 + sum [sizePatt p | (l,p) <- r]
PT _ p -> sizePatt p
PAs _ p -> sizePatt p
PSeq _ _ a _ _ b -> 1 + sizePatt a + sizePatt b
PAlt a b -> 1 + sizePatt a + sizePatt b
PRep _ _ a-> 1 + sizePatt a
PNeg a -> 1 + sizePatt a
_ -> 1
-- the size of a judgement
sizeInfo :: Info -> Int
sizeInfo i = case i of
AbsCat (Just (L _ co)) -> 1 + sum [1 + sizeTerm ty | (_,_,ty) <- co]
AbsFun mt mi me mb -> 1 + msize mt +
sum [sum (map (sizeTerm . patt2term) ps) + sizeTerm t | Just es <- [me], L _ (ps,t) <- es]
sum [sum (map sizePatt ps) + sizeTerm t | Just es <- [me], L _ (ps,t) <- es]
ResParam mp mt ->
1 + sum [1 + sum [1 + sizeTerm ty | (_,_,ty) <- co] | Just (L _ ps) <- [mp], (_,co) <- ps]
ResValue _ _ -> 0
-77
View File
@@ -312,83 +312,6 @@ mkFreshVar olds x =
mkFreshVarX :: [Ident] -> Ident -> Ident
mkFreshVarX olds x = if (elem x olds) then (varX (maximum ((-1) : (map varIndex olds)) + 1)) else x
-- *** Term and pattern conversion
term2patt :: Term -> Err Patt
term2patt trm = case termForm trm of
Ok ([], Vr x, []) | x == identW -> return PW
| otherwise -> return (PV x)
Ok ([], Con c, aa) -> do
aa' <- mapM term2patt aa
return (PC c aa')
Ok ([], QC c, aa) -> do
aa' <- mapM term2patt aa
return (PP c aa')
Ok ([], Q c, []) -> do
return (PM c)
Ok ([], R r, []) -> do
let (ll,aa) = unzipR r
aa' <- mapM term2patt aa
return (PR (zip ll aa'))
Ok ([],EInt i,[]) -> return $ PInt i
Ok ([],EFloat i,[]) -> return $ PFloat i
Ok ([],K s, []) -> return $ PString s
--- encodings due to excessive use of term-patt convs. AR 7/1/2005
Ok ([], Cn id, [Vr a,b]) | id == cAs -> do
b' <- term2patt b
return (PAs a b')
Ok ([], Cn id, [a]) | id == cNeg -> do
a' <- term2patt a
return (PNeg a')
Ok ([], Cn id, [a]) | id == cRep -> do
a' <- term2patt a
return (PRep 0 Nothing a')
Ok ([], Cn id, []) | id == cRep -> do
return PChar
Ok ([], Cn id,[K s]) | id == cChars -> do
return $ PChars s
Ok ([], Cn id, [a,b]) | id == cSeq -> do
a' <- term2patt a
b' <- term2patt b
return (PSeq 0 Nothing a' 0 Nothing b')
Ok ([], Cn id, [a,b]) | id == cAlt -> do
a' <- term2patt a
b' <- term2patt b
return (PAlt a' b')
Ok ([], Cn c, []) -> do
return (PMacro c)
_ -> Bad $ render ("no pattern corresponds to term" <+> ppTerm Unqualified 0 trm)
patt2term :: Patt -> Term
patt2term pt = case pt of
PV x -> Vr x
PW -> Vr identW --- not parsable, should not occur
PMacro c -> Cn c
PM c -> Q c
PC c pp -> mkApp (Con c) (map patt2term pp)
PP c pp -> mkApp (QC c) (map patt2term pp)
PR r -> R [assign l (patt2term p) | (l,p) <- r]
PT _ p -> patt2term p
PInt i -> EInt i
PFloat i -> EFloat i
PString s -> K s
PAs x p -> appCons cAs [Vr x, patt2term p] --- an encoding
PChar -> appCons cChar [] --- an encoding
PChars s -> appCons cChars [K s] --- an encoding
PSeq _ _ a _ _ b -> appCons cSeq [(patt2term a), (patt2term b)] --- an encoding
PAlt a b -> appCons cAlt [(patt2term a), (patt2term b)] --- an encoding
PRep _ _ a-> appCons cRep [(patt2term a)] --- an encoding
PNeg a -> appCons cNeg [(patt2term a)] --- an encoding
-- *** Almost compositional
-- | to define compositional term functions
-14
View File
@@ -77,17 +77,3 @@ cConst = identS "const"
cp1 = identS "p1"
cp2 = identS "p2"
-- * Hacks: dummy identifiers used in various places.
-- Not very nice!
cMeta = identS "?"
cAs = identS "@"
cChar = identS "?"
cChars = identS "[]"
cSeq = identS "+"
cAlt = identS "|"
cRep = identS "*"
cNeg = identS "-"
cCNC = identS "CNC"
cConflict = identS "#conflict"