Skip to content
Browse files

Record bound names in schemes

Ignore-this: f9d77a794aab0be1addad47da5fce7c

darcs-hash:20091219211504-228f4-a67a89852b7e2b392abcd9bd277acae14e505765.gz
  • Loading branch information...
1 parent 4c391d2 commit 3c85c146d23d8cbc2c46a247047e9e603ca47a14 eb committed Dec 19, 2009
Showing with 29 additions and 22 deletions.
  1. +3 −3 Ivor/Datatype.lhs
  2. +1 −1 Ivor/Evaluator.lhs
  3. +5 −3 Ivor/ICompile.lhs
  4. +1 −1 Ivor/Nobby.lhs
  5. +5 −5 Ivor/PatternDefs.lhs
  6. +3 −3 Ivor/Shell.lhs
  7. +1 −1 Ivor/ShellParser.lhs
  8. +9 −4 Ivor/TT.lhs
  9. +1 −1 Ivor/TTCore.lhs
View
6 Ivor/Datatype.lhs
@@ -43,8 +43,8 @@ Elaborated version with elimination rule and iota schemes.
> }
> deriving Show
-> getPat (Sch p i) = p
-> getRed (Sch p i) = i
+> getPat (Sch p _ i) = p
+> getRed (Sch p _ i) = i
> getArity [] = 2 -- empty data type should have elim rule of arity 2!
> -- (actually not if they're dependent. Fix this.)
@@ -103,7 +103,7 @@ then pattern variables are retrieved by projection with Proj in typechecked t.
> do let ps = map (mkPat gamma) pats
> let rhsvars = getPatVars gamma ps
> let rhs = substVars gamma n rhsvars ret
-> return (Sch (reverse ps) (Ind rhs))
+> return (Sch (reverse ps) [] (Ind rhs))
Make a pattern from a raw term. Anything weird, just make it a "PTerm".
View
2 Ivor/Evaluator.lhs
@@ -173,7 +173,7 @@ Code Stack Env Result
> match :: Scheme Name -> [TT Name] -> SEnv ->
> [(Name, TT Name)] ->
> State (Maybe [(Name, Int)]) (Maybe (TT Name, [(Name, TT Name)], Stack))
-> match (Sch pats rhs) xs env patvars
+> match (Sch pats _ rhs) xs env patvars
> = matchargs pats xs rhs env patvars []
> matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs)
> matchargs (p:ps) (x:xs) rhs env patvars pv'
View
8 Ivor/ICompile.lhs
@@ -1,3 +1,5 @@
+FIXME: I don't believe this is used. Make it go away.
+
> module Ivor.ICompile where
> import Ivor.TTCore
@@ -32,8 +34,8 @@ families, although we should do better later.
> let top = map schhead ss'
> rest = map schtail ss' in
> icomp' top rest es'
-> schhead (Sch x red) = (head x, red)
-> schtail (Sch x red) = Sch (tail x) red
+> schhead (Sch x bs red) = (head x, red)
+> schtail (Sch x bs red) = Sch (tail x) bs red
> icomp' x xs (e:es) | allDisjoint (map fst x) = doCase1 e x
> | otherwise = error "Can't find a scrutinee"
> orderPatts = sortBy cmpPat
@@ -44,7 +46,7 @@ I wish I'd written a comment here when I wrote this...
> mangleArgOrder :: [Scheme Name] -> [Int] -> [Scheme Name]
> mangleArgOrder [] _ = []
> mangleArgOrder (x:xs) es = (ma' x es):(mangleArgOrder xs es)
-> where ma' (Sch ps ired) es = Sch (reorder ps es) ired
+> where ma' (Sch ps bs ired) es = Sch (reorder ps es) bs ired
> reorder ps xs = foldl (\ih x -> (ps!!x):ih) [] xs
> allDisjoint ps = numDisjoint ps == length ps
View
2 Ivor/Nobby.lhs
@@ -168,7 +168,7 @@ Do the actual evaluation
> patmatch :: Gamma Name -> Ctxt -> [PMDef Name] -> [Value] -> Maybe Value
> patmatch gam g [] _ = Nothing
-> patmatch gam g ((Sch pats ret):ps) vs = case pm gam g pats vs ret [] of
+> patmatch gam g ((Sch pats _ ret):ps) vs = case pm gam g pats vs ret [] of
> Nothing -> patmatch gam g ps vs
> Just v -> Just v
View
10 Ivor/PatternDefs.lhs
@@ -87,7 +87,7 @@ there are no increasing arguments and at least one decreasing argument.
Check for definition 1 above: one argument position is well founded
-> wfClause args (Sch pats (Ind t)) = do
+> wfClause args (Sch pats _ (Ind t)) = do
> let recs = findRec [] t
> case recs of
> [] -> return args
@@ -96,7 +96,7 @@ Check for definition 1 above: one argument position is well founded
Check for definition 2 above: all recursive calls have a decreasing argument
and no increasing arguments
-> allDec (Sch pats (Ind t)) err = do
+> allDec (Sch pats _ (Ind t)) err = do
> let recs = findRec [] t
> case allRecDec pats recs of
> Success v -> return v
@@ -216,8 +216,8 @@ Each clause may generate auxiliary definitions, so return all definitons created
> let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt')
> let namesbound = getNames (Sc tmtt)
> checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty
-> -- trace (show (unified, rtmtt, tm, rtmtt')) $
-> return ((tm, Ind rtmtt', newdefs), [], newdefs, True)
+> -- trace (show env) $
+> return ((tm, Ind rtmtt', env), [], newdefs, True)
> mytypecheck gam (clause, (RWith addprf scr pats)) i =
> do -- Get the type of scrutinee, construct the type of the auxiliary definition
> (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn
@@ -299,7 +299,7 @@ Each clause may generate auxiliary definitions, so return all definitons created
> addContext (Just (f,l)) err = IContext (f ++ ":" ++ show l ++ ":") err
> mkScheme :: Gamma Name -> (Indexed Name, Indexed Name) -> PMDef Name
-> mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) ret
+> mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) [] ret
> where mkpat (P n) = PVar n
> mkpat (App f a) = addPatArg (mkpat f) (mkpat a)
> mkpat (Con i nm ar) = mkPatV nm (lookupval nm gam)
View
6 Ivor/Shell.lhs
@@ -158,9 +158,9 @@
> (Name DataCon _) -> return (respondLn st "Data constructor")
> _ -> fail "Unknown definition"
> where printPats (Patterns cs) = unlines (map printClause cs)
-> printClause (PClause args ret) = n ++ " " ++
-> unwords (map argshow args) ++
-> " = " ++ show ret
+> printClause (PClause args _ ret) = n ++ " " ++
+> unwords (map argshow args) ++
+> " = " ++ show ret
> argshow x | ' ' `elem` show x = "(" ++ show x ++ ")"
> | otherwise = show x
View
2 Ivor/ShellParser.lhs
@@ -131,7 +131,7 @@ which runs it.
> pclauseret :: [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause
> pclauseret args ext = do lchar '='
> ret <- pTerm ext
-> return $ PClause args ret
+> return $ PClause args [] ret
> pclausewith :: String -> [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause
> pclausewith nm args ext = do lchar '|'
View
13 Ivor/TT.lhs
@@ -267,6 +267,7 @@
> data PClause = PClause {
> arguments :: [ViewTerm],
+> boundnames :: [(Name, ViewTerm)],
> returnval :: ViewTerm
> }
> | PWithClause {
@@ -281,7 +282,7 @@
> deriving Show
> mkRawClause :: PClause -> RawScheme
-> mkRawClause (PClause args ret) =
+> mkRawClause (PClause args _ ret) =
> RSch (map forget args) (RWRet (forget ret))
> mkRawClause (PWithClause prf args scr (Patterns rest)) =
> RSch (map forget args) (RWith prf (forget scr) (map mkRawClause rest))
@@ -904,8 +905,12 @@ Give a parseable but ugly representation of a term.
> Patterns [mkCAFpat ind])
> _ -> fail "Not a pattern matching definition"
> where getPats (PMFun _ ps) = ps
-> mkPat (Sch ps ret) = PClause (map viewPat ps) (view (Term (ret, (Ind TTCore.Star))))
-> mkCAFpat tm = PClause [] (view (Term (tm, (Ind TTCore.Star))))
+> mkPat (Sch ps bs ret)
+> = PClause (map viewPat ps)
+> (map (\ (n, B _ t) ->
+> (n, (view (Term (Ind t, (Ind TTCore.Star)))))) bs)
+> (view (Term (ret, (Ind TTCore.Star))))
+> mkCAFpat tm = PClause [] [] (view (Term (tm, (Ind TTCore.Star))))
> viewPat (PVar n) = Name Bound n --(name (show n))
> viewPat (PCon t n ty ts) = VTerm.apply (Name Bound (name (show n))) (map viewPat ts)
> viewPat (PConst c) = Constant c
@@ -998,7 +1003,7 @@ Examine pattern matching elimination rules
> elim <- lookupM rule (eliminators st)
> return $ Patterns $ map mkRed (fst $ snd elim)
> Nothing -> fail $ (show nm) ++ " is not a type constructor"
-> where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) (viewRaw ret)
+> where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) [] (viewRaw ret)
> -- a reduction will only have variables and applications
> viewRaw (Var n) = Name Free n
> viewRaw (RApp f a) = VTerm.App (viewRaw f) (viewRaw a)
View
2 Ivor/TTCore.lhs
@@ -162,7 +162,7 @@ Data declarations and pattern matching
> data RawScheme = RSch [Raw] RawWith
> deriving Show
-> data Scheme n = Sch [Pattern n] {- With -} (Indexed n)
+> data Scheme n = Sch [Pattern n] (Env n) (Indexed n)
> deriving Show
> type PMRaw = RawScheme

0 comments on commit 3c85c14

Please sign in to comment.
Something went wrong with that request. Please try again.