diff options
Diffstat (limited to 'app')
| -rw-r--r-- | app/Builtins.hs | 171 | ||||
| -rw-r--r-- | app/Code.hs | 6 | ||||
| -rw-r--r-- | app/Compiler.hs | 24 | ||||
| -rw-r--r-- | app/Frontend.hs | 6 | ||||
| -rw-r--r-- | app/IR.hs | 4 | ||||
| -rw-r--r-- | app/Interpreter.hs | 14 | ||||
| -rw-r--r-- | app/Parser.hs | 26 |
7 files changed, 139 insertions, 112 deletions
diff --git a/app/Builtins.hs b/app/Builtins.hs index 0cdd7cd..2b7f08e 100644 --- a/app/Builtins.hs +++ b/app/Builtins.hs @@ -46,9 +46,9 @@ printLocals = do scope <- gets (gvar . cur) heap <- gets (heap . cur) IR.StrTable _ _ itos <- gets strtable - flip traverse (M.elems scope) $ \(ref, name) -> + flip traverse (M.assocs scope) $ \(local, ref) -> lift . outputStrLn $ - (maybe "_" id $ itos M.!? name) ++ " = " ++ showTerm itos heap ref + "_Local" ++ show local ++ " = " ++ showTerm itos heap ref return Nothing promptRetry :: InterpFn @@ -65,15 +65,22 @@ promptRetry' = do Just ';' -> backtrack _ -> return Nothing -write :: InterpFn -write - --TODO: prlgError on write(Unbound) - = do +withArgs :: [Int] -> ([Int] -> InterpFn) -> InterpFn +withArgs as f = do scope <- gets (hvar . cur) - heap <- gets (heap . cur) - IR.StrTable _ _ itos <- gets strtable - lift . outputStr . showTerm itos heap . fst $ scope M.! 0 - return Nothing + if all (`M.member` scope) as + then f $ map (scope M.!) as + else prlgError "arguments not bound" + +write' :: InterpFn -> InterpFn +write' c = + withArgs [0] $ \[arg] -> do + heap <- gets (heap . cur) + IR.StrTable _ _ itos <- gets strtable + lift . outputStr $ showTerm itos heap arg + c --this now allows error fallthrough but we might like EitherT + +write = write' $ return Nothing nl :: InterpFn nl = do @@ -81,59 +88,71 @@ nl = do return Nothing writeln :: InterpFn -writeln = write >> nl +writeln = write' nl assertFact :: InterpFn -assertFact = do - scope <- gets (hvar . cur) - heap <- gets (heap . cur) - case Co.compileGoal . Co.squashVars <$> - Co.heapStructPrlgInt Nothing heap (fst $ scope M.! 0) of - Just (U (Struct s):head) -> do - addClause s $ head ++ [NoGoal] - return Nothing - _ -> prlgError "assert fact failure" +assertFact = + withArgs [0] $ \[arg] -> do + heap <- gets (heap . cur) + case Co.compileGoal . Co.squashVars <$> + Co.heapStructPrlgInt Nothing heap arg of + Just (U (Struct s):head) -> do + addClause s $ head ++ [NoGoal] + return Nothing + _ -> prlgError "assert fact failure" assertClause :: InterpFn -assertClause = do - scope <- gets (hvar . cur) - heap <- gets (heap . cur) - commaId <- findStruct "," 2 - cut <- findAtom "!" - case Co.squashVars . IR.CallI (IR.Id 0 0) <$> - traverse (Co.heapStructPrlgInt Nothing heap . fst . (M.!) scope) [0, 1] of - Just (IR.CallI (IR.Id 0 0) [hs, gs]) -> - let (U (Struct s):cs) = - Co.compileGoal hs ++ Co.seqGoals (Co.compileGoals commaId cut gs) - in do addClause s cs - return Nothing - _ -> prlgError "assert clause failure" +assertClause = + withArgs [0, 1] $ \args -> do + scope <- gets (hvar . cur) + heap <- gets (heap . cur) + comma <- findAtom "," + cut <- findAtom "!" + case Co.squashVars . IR.CallI 0 <$> + traverse (Co.heapStructPrlgInt Nothing heap) args of + Just (IR.CallI 0 [hs, gs]) -> + let (U (Struct s):cs) = + Co.compileGoal hs ++ Co.seqGoals (Co.compileGoals comma cut gs) + in do addClause s cs + return Nothing + _ -> prlgError "assert clause failure" retractall :: InterpFn -retractall = prlgError "no retractall yet" +retractall = + withArgs [0] $ \[arg] -> do + heap <- gets (heap . cur) + case derefHeap heap arg of + BoundRef _ (Atom a) -> dropProcedure (IR.Id {IR.arity = 0, IR.str = a}) + BoundRef _ (Struct id) -> dropProcedure id + _ -> prlgError "retractall needs a struct" call :: InterpFn -call = do - ref <- gets (fst . (M.! 0) . hvar . cur) - heap@(Heap _ hmap) <- gets (heap . cur) - let exec base struct arity = do - cur <- gets cur - modify $ \s -> - s - { cur = - cur - { gol = - [Call, Goal, U struct] ++ - [U $ hmap M.! (base + i) | i <- [1 .. arity]] ++ gol cur - } - } - return Nothing - case derefHeap heap ref of - BoundRef addr struct@(Struct IR.Id {IR.arity = arity}) -> - exec addr struct arity - BoundRef addr (Atom a) -> - exec addr (Struct IR.Id {IR.arity = 0, IR.str = a}) 0 - _ -> prlgError "not callable" +call = + withArgs [0] $ \[arg] -> do + heap@(Heap _ hmap) <- gets (heap . cur) + let exec base struct arity = do + cur <- gets cur + modify $ \s -> + s + { cur = + cur + { gol = + [Call, Goal, U struct] ++ + [U $ hmap M.! (base + i) | i <- [1 .. arity]] ++ gol cur + } + } + return Nothing + case derefHeap heap arg of + BoundRef addr struct@(Struct IR.Id {IR.arity = arity}) -> + exec addr struct arity + BoundRef addr (Atom a) -> + exec addr (Struct IR.Id {IR.arity = 0, IR.str = a}) 0 + _ -> prlgError "not callable" + +struct :: InterpFn +struct = do + scope <- gets (hvar . cur) + prlgError "not yet" {- adding the builtins -} addOp op = modify $ \s -> s {ops = op : ops s} @@ -145,20 +164,29 @@ addClause struct code = addProcedure struct heads = modify $ \s -> s {defs = M.insert struct heads $ defs s} +dropProcedure struct = do + d <- gets defs + if struct `M.member` d + then do + modify $ \s -> s {defs = M.delete struct d} + return Nothing + else prlgError "no such definition" -- this should backtrack? + addProc n a c = do sym <- findStruct n a addProcedure sym c -addBi0 n b = addProc n 0 [[Invoke $ bi b]] +addBi n i b = + addProc n i [[U (LocalRef $ r - 1) | r <- [1 .. i]] ++ [Invoke $ bi b]] addPrelude :: PrlgEnv () addPrelude = do pure undefined {- primitives -} - addBi0 "true" (pure Nothing) - addBi0 "fail" backtrack + addBi "true" 0 (pure Nothing) + addBi "fail" 0 backtrack addOp $ O.xfx "=" 700 - addProc "=" 2 [[U (LocalRef 0 0), U (LocalRef 0 0), NoGoal]] + addProc "=" 2 [[U (LocalRef 0), U (LocalRef 0), NoGoal]] {- clauses -} addOp $ O.xfy "," 1000 addOp $ O.xfx ":-" 1200 @@ -168,22 +196,23 @@ addPrelude = do "assert" 1 [ [ U (Struct horn2) - , U (LocalRef 0 0) - , U (LocalRef 1 0) + , U (LocalRef 0) + , U (LocalRef 1) , Cut , Invoke (bi assertClause) ] - , [U (LocalRef 0 0), Invoke (bi assertFact)] + , [U (LocalRef 0), Invoke (bi assertFact)] ] - addProc "retractall" 1 [[U (LocalRef 0 0), Invoke (bi retractall)]] - addProc "call" 1 [[U (LocalRef 0 0), Invoke (bi call)]] + addBi "retractall" 1 retractall + addBi "call" 1 call + addBi "struct" 3 struct {- query tools -} - addBi0 "print_locals" printLocals - addBi0 "prompt_retry" promptRetry' - addBi0 "query" (printLocals >> promptRetry) + addBi "print_locals" 0 printLocals + addBi "prompt_retry" 0 promptRetry' + addBi "query" 0 (printLocals >> promptRetry) {- IO -} - addProc "write" 1 [[U (LocalRef 0 0), Invoke (bi write)]] - addProc "writeln" 1 [[U (LocalRef 0 0), Invoke (bi writeln)]] - addBi0 "nl" nl + addBi "write" 1 write + addBi "writeln" 1 writeln + addBi "nl" 0 nl {- debug -} - addBi0 "interpreter_trace" (get >>= liftIO . print >> pure Nothing) + addBi "interpreter_trace" 0 (get >>= liftIO . print >> pure Nothing) diff --git a/app/Code.hs b/app/Code.hs index 0556415..eecd5b6 100644 --- a/app/Code.hs +++ b/app/Code.hs @@ -12,7 +12,7 @@ data Datum = Atom Int -- unifies a constant | Struct Id -- unifies a structure with arity | VoidRef -- unifies with anything - | LocalRef Int Int -- code-local variable idx (should never occur on heap) + | LocalRef Int -- code-local variable idx (should never occur on heap) | HeapRef Int -- something further on the heap deriving (Show, Eq, Ord) @@ -36,7 +36,7 @@ data Heap = emptyHeap = Heap 1 M.empty -type Scope = M.Map Int (Int, Int) +type Scope = M.Map Int Int emptyScope :: Scope emptyScope = M.empty @@ -103,7 +103,7 @@ codeStruct :: codeStruct atom struct local rec end heap = go where go [] = ([], ) <$> end - go (U lr@(LocalRef _ _):cs) = do + go (U lr@(LocalRef _):cs) = do x <- local lr case x of Left ref -> (cs, ) <$> heapStruct atom struct rec heap ref diff --git a/app/Compiler.hs b/app/Compiler.hs index 84a63a4..6d104a9 100644 --- a/app/Compiler.hs +++ b/app/Compiler.hs @@ -10,8 +10,7 @@ desugarPrlg :: Int -> PrlgInt -> PrlgInt desugarPrlg list = go where go (CallI id ps) = CallI id $ map go ps - go (ListI (x:xs) t) = - CallI Id {str = list, arity = 2} [go x, go (ListI xs t)] + go (ListI (x:xs) t) = CallI list [go x, go (ListI xs t)] go (ListI [] Nothing) = LiteralI list go (ListI [] (Just x)) = go x go x = x @@ -29,7 +28,7 @@ varOccurs _ = M.empty variablizePrlg :: Int -> StrTable -> PrlgInt -> PrlgInt variablizePrlg void (StrTable _ _ itos) = go where - go (CallI id ps) = CallI id $ map go ps + go (CallI i ps) = CallI i $ map go ps go (LiteralI i) | i == void = VoidI | varname (itos M.! i) = VarI i i @@ -38,7 +37,7 @@ variablizePrlg void (StrTable _ _ itos) = go renumVars :: (Int -> Maybe PrlgInt) -> PrlgInt -> PrlgInt renumVars rename = go where - go (CallI id ps) = CallI id $ map go ps + go (CallI i ps) = CallI i $ map go ps go (VarI idx i) | Just new <- rename idx = new go x = x @@ -52,13 +51,13 @@ squashVars x = [(idx, VarI idx' 0) | ((idx, n), idx') <- zip occurs [1 ..], n > 1] in renumVars (m' M.!?) x -compileGoals :: Id -> Int -> PrlgInt -> [Code] +compileGoals :: Int -> Int -> PrlgInt -> [Code] compileGoals andop cut = go' where go' = go . struct2goal - go p@(CallI x args) + go p@(CallI x args@[_, _]) | x == andop = concatMap go' args - go p@(CallI (Id x 0) []) + go p@(CallI x []) | x == cut = [[Cut]] go x = [compileGoal x] @@ -66,9 +65,10 @@ compileGoal :: PrlgInt -> Code compileGoal = compileArg . struct2goal compileArg :: PrlgInt -> Code -compileArg (CallI s args) = U (Struct s) : concatMap compileArg args +compileArg (CallI i args) = + U (Struct Id {str = i, arity = length args}) : concatMap compileArg args compileArg (LiteralI s) = [U (Atom s)] -compileArg (VarI x s) = [U (LocalRef x s)] +compileArg (VarI x _) = [U (LocalRef x)] compileArg (VoidI) = [U VoidRef] seqGoals :: [Code] -> Code @@ -84,16 +84,16 @@ heapStructPrlgInt heaperr heap ref = heapStruct atom struct hrec heap ref where atom (Atom s) = pure $ LiteralI s atom VoidRef = pure $ VoidI - struct (Struct s) args = pure $ CallI s args + struct (Struct s) args = pure $ CallI (str s) args hrec (HeapRef r) ref | r == ref = pure $ VarI r 0 | otherwise = heaperr -- TODO check if this is used goal2struct :: PrlgInt -> PrlgInt -goal2struct (CallI (Id s 0) []) = LiteralI s +goal2struct (CallI s []) = LiteralI s goal2struct x = x struct2goal :: PrlgInt -> PrlgInt -struct2goal (LiteralI s) = CallI (Id s 0) [] +struct2goal (LiteralI s) = CallI s [] struct2goal x = x diff --git a/app/Frontend.hs b/app/Frontend.hs index 8f908ef..d4c3dbd 100644 --- a/app/Frontend.hs +++ b/app/Frontend.hs @@ -8,7 +8,7 @@ import Control.Monad.Trans.Class (lift) import Control.Monad.Trans.State.Lazy (evalStateT, gets) import Data.Foldable (traverse_) import qualified Data.Map as M -import Env (PrlgEnv, findAtom, findStruct, withStrTable) +import Env (PrlgEnv, findAtom, withStrTable) import qualified IR import qualified Interpreter as I import qualified Parser as P @@ -55,9 +55,9 @@ interpret = (>> return True) . lex C.variablizePrlg underscore st $ C.desugarPrlg list prlgi) compile prlgv compile prlgv = do - commaId <- findStruct "," 2 + comma <- findAtom "," cut <- findAtom "!" - let code = C.seqGoals $ C.compileGoals commaId cut prlgv + let code = C.seqGoals $ C.compileGoals comma cut prlgv execute code execute code = do res <- I.prove code @@ -17,7 +17,7 @@ data Id = deriving (Show, Eq, Ord) data PrlgInt - = CallI Id [PrlgInt] --TODO this should be Int + = CallI Int [PrlgInt] | LiteralI Int | ListI [PrlgInt] (Maybe PrlgInt) -- only exists before desugaring | VarI Int Int -- VarI localIndex strTableString @@ -41,7 +41,7 @@ internPrlg = go go t (LiteralS str) = LiteralI <$> strtablize t str go t (CallS str ps) = let (t', i) = strtablize t str - in CallI (Id i $ length ps) <$> mapAccumL go t' ps + in CallI i <$> mapAccumL go t' ps go t (ListS elems Nothing) = flip ListI Nothing <$> mapAccumL go t elems go t (ListS elems (Just tail)) = let (t', tail') = go t tail diff --git a/app/Interpreter.hs b/app/Interpreter.hs index 7192c7b..15ab1e5 100644 --- a/app/Interpreter.hs +++ b/app/Interpreter.hs @@ -89,10 +89,10 @@ proveStep = St.get >>= go in ( Heap (nxt + n) $ foldr (uncurry M.insert) m [(a, HeapRef a) | a <- addrs] , addrs) - allocLocal (LocalRef reg ident) scope cont - | Just (addr, _) <- scope M.!? reg = cont scope heap addr + allocLocal (LocalRef reg) scope cont + | Just addr <- scope M.!? reg = cont scope heap addr | (heap', addr) <- newHeapVar heap = - cont (M.insert reg (addr, ident) scope) heap' addr + cont (M.insert reg addr scope) heap' addr newHeapStruct addr s@(Struct Id {arity = arity}) cont = let (Heap nxt' m', addrs) = newHeapVars (arity + 1) heap m'' = @@ -113,10 +113,10 @@ proveStep = St.get >>= go unify (Struct Id {arity = a}) VoidRef = c i {cur = cur {hed = hs, gol = replicate a (U VoidRef) ++ gs}} {- handle local refs; first ignore their combination with voids to save memory -} - unify (LocalRef _ _) VoidRef = uok - unify VoidRef (LocalRef _ _) = uok + unify (LocalRef _) VoidRef = uok -- TRICKY: builtins need to check if locals actually exist because of this + unify VoidRef (LocalRef _) = uok {- allocate heap for LocalRefs and retry with HeapRefs -} - unify lr@(LocalRef _ _) _ = + unify lr@(LocalRef _) _ = allocLocal lr (hvar cur) $ \hvar' heap' addr -> c i @@ -124,7 +124,7 @@ proveStep = St.get >>= go cur {hed = U (HeapRef addr) : hs, hvar = hvar', heap = heap'} } - unify _ lr@(LocalRef _ _) = + unify _ lr@(LocalRef _) = allocLocal lr (gvar cur) $ \gvar' heap' addr -> c i diff --git a/app/Parser.hs b/app/Parser.hs index 864cdc5..acc8104 100644 --- a/app/Parser.hs +++ b/app/Parser.hs @@ -172,29 +172,27 @@ literal = Literal . unTok <$> free (satisfy isNormalTok <* notFollowedBy lParen) call = do fn <- unTok <$> satisfy isNormalTok -- not free - Seq inner <- free parens - return $ Call fn $ splitOn [Literal ","] inner + (Call fn [] <$ try emptyParens) <|> do + Seq inner <- free parens + return $ Call fn $ splitOn [Literal ","] inner parens = Seq <$> (free lParen *> some seqItem <* free rParen) +emptyParens = Literal "()" <$ (free lParen >> free rParen) + list = do free lBracket - choice - [ List [] Nothing <$ free rBracket - , do items <- splitOn [Literal ","] <$> some seqItem - choice - [ List items Nothing <$ free rBracket - , List items . Just <$> - (free listTail *> some seqItem <* free rBracket) - ] - ] + (List [] Nothing <$ free rBracket) <|> do + items <- splitOn [Literal ","] <$> some seqItem + (List items Nothing <$ free rBracket) <|> + (List items . Just <$> (free listTail *> some seqItem <* free rBracket)) -seqItem = choice [try call, literal, parens, list] +seqItem = choice [try call, literal, try emptyParens, parens, list] simpleTok :: String -> Parser () simpleTok s = void $ single (Tok s) -comma = simpleTok "." +period = simpleTok "." lParen = simpleTok "(" @@ -207,7 +205,7 @@ listTail = simpleTok "|" rBracket = simpleTok "]" clause :: Parser PAST -clause = Seq <$> some (free seqItem) <* free comma +clause = Seq <$> some (free seqItem) <* free period parsePrlg :: Parser [PAST] parsePrlg = ws *> many clause <* eof |