Skip to content

Commit

Permalink
add 'log' functionality
Browse files Browse the repository at this point in the history
example:

main
= log (String/append "foo" "bar")
  12

will print "foobar"
  • Loading branch information
VictorTaelin committed Oct 21, 2024
1 parent 3e587de commit 3514a52
Show file tree
Hide file tree
Showing 8 changed files with 75 additions and 4 deletions.
1 change: 1 addition & 0 deletions src/Kind/API.hs
Original file line number Diff line number Diff line change
Expand Up @@ -194,6 +194,7 @@ getDeps term = case term of
Src _ val -> getDeps val
Hol _ args -> concatMap getDeps args
Met _ args -> concatMap getDeps args
Log msg nxt -> getDeps msg ++ getDeps nxt
Var _ _ -> []
Set -> []
U32 -> []
Expand Down
6 changes: 6 additions & 0 deletions src/Kind/Check.hs
Original file line number Diff line number Diff line change
Expand Up @@ -117,6 +117,9 @@ infer src term dep = debug ("infer: " ++ termShower False term dep) $ go src ter
envLog (Error src (Ref "annotation") (Ref "meta") (Met uid spn) dep)
envFail

go src (Log msg nxt) dep =
go src nxt dep

go src (Var nam idx) dep = do
envLog (Error src (Ref "annotation") (Ref "variable") (Var nam idx) dep)
envFail
Expand Down Expand Up @@ -268,6 +271,9 @@ check src val typ dep = debug ("check: " ++ termShower False val dep ++ "\n :
go src (Met uid spn) typx dep = do
return ()

go src (Log msg nxt) typx dep = do
go src nxt typx dep

go src tm@(Txt txt) typx dep = do
book <- envGetBook
fill <- envGetFill
Expand Down
6 changes: 6 additions & 0 deletions src/Kind/Compile.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
-- //./Type.hs//

module Kind.Compile where

import Kind.Type
Expand Down Expand Up @@ -76,6 +78,10 @@ termToJS term dep = case term of
"null"
Met _ _ ->
"null"
Log msg nxt ->
let msg' = termToJS msg dep
nxt' = termToJS nxt dep
in concat ["(console.log(", msg', "), ", nxt', ")"]
Var nam idx ->
nameToJS nam ++ "$" ++ show idx
Src _ val ->
Expand Down
17 changes: 17 additions & 0 deletions src/Kind/Equal.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,5 @@
-- //./Type.hs//

module Kind.Equal where

import Control.Monad (zipWithM)
Expand Down Expand Up @@ -100,6 +102,10 @@ identical a b dep = do
case IM.lookup bUid fill of
Just sol -> identical a sol dep
Nothing -> unify bUid bSpn a dep
go (Log aMsg aNxt) b dep =
identical aNxt b dep
go a (Log bMsg bNxt) dep =
identical a bNxt dep
go (Hol aNam aCtx) b dep =
return True
go a (Hol bNam bCtx) dep =
Expand Down Expand Up @@ -298,6 +304,10 @@ occur book fill uid term dep = go term dep where
let o_val = go val dep
o_bod = go (bod (Var nam dep)) (dep + 1)
in o_val || o_bod
go (Log msg nxt) dep =
let o_msg = go msg dep
o_nxt = go nxt dep
in o_msg || o_nxt
go (Hol nam ctx) dep =
False
go (Op2 opr fst snd) dep =
Expand Down Expand Up @@ -380,6 +390,11 @@ same (Met aUid aSpn) b dep =
False
same a (Met bUid bSpn) dep =
False
-- TODO: Log
same (Log aMsg aNxt) b dep =
same aNxt b dep
same a (Log bMsg bNxt) dep =
same a bNxt dep
same (Hol aNam aCtx) b dep =
True
same a (Hol bNam bCtx) dep =
Expand Down Expand Up @@ -446,6 +461,7 @@ subst lvl neo term = go term where
go (Let nam val bod) = Let nam (go val) (\x -> go (bod x))
go (Use nam val bod) = Use nam (go val) (\x -> go (bod x))
go (Met uid spn) = Met uid (map go spn)
go (Log msg nxt) = Log (go msg) (go nxt)
go (Hol nam ctx) = Hol nam (map go ctx)
go Set = Set
go U32 = U32
Expand Down Expand Up @@ -478,6 +494,7 @@ replace old neo term dep = if same old term dep then neo else go term where
go (Let nam val bod) = Let nam (replace old neo val dep) (\x -> replace old neo (bod x) (dep+1))
go (Use nam val bod) = Use nam (replace old neo val dep) (\x -> replace old neo (bod x) (dep+1))
go (Met uid spn) = Met uid (map (\x -> replace old neo x (dep+1)) spn)
go (Log msg nxt) = Log (replace old neo msg dep) (replace old neo nxt dep)
go (Hol nam ctx) = Hol nam (map (\x -> replace old neo x (dep+1)) ctx)
go Set = Set
go U32 = U32
Expand Down
10 changes: 6 additions & 4 deletions src/Kind/Parse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ parseTerm = (do
, parseLst
, parseChr
, parseHol
-- , parseMet
, parseLog
, parseRef
] <* skip
parseSuffix term) <?> "Term"
Expand Down Expand Up @@ -470,9 +470,11 @@ parseHol = withSrc $ do
return terms
return $ Hol nam ctx

-- parseMet = withSrc $ do
-- char_end '_'
-- return $ Met 0 []
parseLog = withSrc $ do
P.try $ string_skp "log"
msg <- parseTerm
val <- parseTerm
return $ Log msg val

parseOper = P.choice
[ P.try (string_skp "+") >> return ADD
Expand Down
32 changes: 32 additions & 0 deletions src/Kind/Reduce.hs
Original file line number Diff line number Diff line change
Expand Up @@ -35,6 +35,7 @@ reduce book fill lv term = red term where
red (Nat val) = nat val
red (Src src val) = red val
red (Met uid spn) = met uid spn
red (Log msg nxt) = log msg nxt
red val = val

app (Ref nam) arg | lv > 0 = app (ref nam) arg
Expand Down Expand Up @@ -96,6 +97,18 @@ reduce book fill lv term = red term where
nat 0 = Con "Zero" []
nat n = Con "Succ" [(Nothing, Nat (n - 1))]

log msg nxt = logMsg book fill lv msg nxt ""

-- Logging
-- -------

logMsg :: Book -> Fill -> Int -> Term -> Term -> String -> Term
logMsg book fill lv msg nxt txt = case (reduce book fill lv msg) of
Con "Cons" [(_, head), (_, tail)] -> case (reduce book fill lv head) of
Num chr -> logMsg book fill lv tail nxt (txt ++ [toEnum (fromIntegral chr)])
Con "Nil" [] ->
trace txt nxt
_ -> nxt

-- Normalization
-- -------------
Expand Down Expand Up @@ -169,6 +182,10 @@ normal book fill lv term dep = go (reduce book fill lv term) dep where
let nf_val = normal book fill lv val dep in
Src src nf_val
go (Met uid spn) dep = Met uid spn -- TODO: normalize spine
go (Log msg nxt) dep =
let nf_msg = normal book fill lv msg dep in
let nf_nxt = normal book fill lv nxt dep in
Log nf_msg nf_nxt

normalTele :: Book -> Fill -> Int -> Tele -> Int -> Tele
normalTele book fill lv tele dep = case tele of
Expand Down Expand Up @@ -252,6 +269,10 @@ bind (Lst lst) ctx =
bind (Nat val) ctx = Nat val
bind (Hol nam ctxs) ctx = Hol nam (reverse (map snd ctx))
bind (Met uid spn) ctx = Met uid []
bind (Log msg nxt) ctx =
let msg' = bind msg ctx in
let nxt' = bind nxt ctx in
Log msg' nxt'
bind (Var nam idx) ctx =
case lookup nam ctx of
Just x -> x
Expand Down Expand Up @@ -312,6 +333,17 @@ genMetasGo (Use nam val bod) c =
genMetasGo (Met _ spn) c =
let (spn', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) spn
in (Met c1 spn', c1 + 1)
genMetasGo (Op2 opr fst snd) c =
let (fst', c1) = genMetasGo fst c
(snd', c2) = genMetasGo snd c1
in (Op2 opr fst' snd', c2)
genMetasGo (Lst lst) c =
let (lst', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) lst
in (Lst lst', c1)
genMetasGo (Log msg nxt) c =
let (msg', c1) = genMetasGo msg c
(nxt', c2) = genMetasGo nxt c1
in (Log msg' nxt', c2)
genMetasGo (Hol nam ctx) c =
let (ctx', c1) = foldr (\t (acc, c') -> let (t', c'') = genMetasGo t c' in (t':acc, c'')) ([], c) ctx
in (Hol nam ctx', c1)
Expand Down
4 changes: 4 additions & 0 deletions src/Kind/Show.hs
Original file line number Diff line number Diff line change
Expand Up @@ -106,6 +106,10 @@ termShower small term dep =
Hol nam ctx -> concat ["?" , nam]
-- Met uid spn -> concat ["_", show uid, "[", strSpn spn dep, " ]"]
Met uid spn -> concat ["_", show uid]
Log msg nxt ->
let msg' = termShower small msg dep
nxt' = termShower small nxt dep
in concat ["log ", msg', " ", nxt']
Var nam idx -> nam
Src src val -> if small
then termShower small val dep
Expand Down
3 changes: 3 additions & 0 deletions src/Kind/Type.hs
Original file line number Diff line number Diff line change
Expand Up @@ -65,6 +65,9 @@ data Term
-- Unification Metavar
| Met Int [Term]

-- Logging
| Log Term Term

-- Variable
| Var String Int

Expand Down

0 comments on commit 3514a52

Please sign in to comment.