From 3514a520fe2c0408fa8b396168c84882256ee6e9 Mon Sep 17 00:00:00 2001 From: Victor Taelin Date: Mon, 21 Oct 2024 16:46:48 -0300 Subject: [PATCH] add 'log' functionality example: main = log (String/append "foo" "bar") 12 will print "foobar" --- src/Kind/API.hs | 1 + src/Kind/Check.hs | 6 ++++++ src/Kind/Compile.hs | 6 ++++++ src/Kind/Equal.hs | 17 +++++++++++++++++ src/Kind/Parse.hs | 10 ++++++---- src/Kind/Reduce.hs | 32 ++++++++++++++++++++++++++++++++ src/Kind/Show.hs | 4 ++++ src/Kind/Type.hs | 3 +++ 8 files changed, 75 insertions(+), 4 deletions(-) diff --git a/src/Kind/API.hs b/src/Kind/API.hs index f05209160..ac19585a7 100644 --- a/src/Kind/API.hs +++ b/src/Kind/API.hs @@ -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 -> [] diff --git a/src/Kind/Check.hs b/src/Kind/Check.hs index ad1de6b7c..80e84cb0d 100644 --- a/src/Kind/Check.hs +++ b/src/Kind/Check.hs @@ -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 @@ -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 diff --git a/src/Kind/Compile.hs b/src/Kind/Compile.hs index 74d0f5d3e..b35089631 100644 --- a/src/Kind/Compile.hs +++ b/src/Kind/Compile.hs @@ -1,3 +1,5 @@ +-- //./Type.hs// + module Kind.Compile where import Kind.Type @@ -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 -> diff --git a/src/Kind/Equal.hs b/src/Kind/Equal.hs index 2b0d3fb4a..91c691eda 100644 --- a/src/Kind/Equal.hs +++ b/src/Kind/Equal.hs @@ -1,3 +1,5 @@ +-- //./Type.hs// + module Kind.Equal where import Control.Monad (zipWithM) @@ -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 = @@ -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 = @@ -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 = @@ -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 @@ -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 diff --git a/src/Kind/Parse.hs b/src/Kind/Parse.hs index f67dca17d..ad09255da 100644 --- a/src/Kind/Parse.hs +++ b/src/Kind/Parse.hs @@ -172,7 +172,7 @@ parseTerm = (do , parseLst , parseChr , parseHol - -- , parseMet + , parseLog , parseRef ] <* skip parseSuffix term) "Term" @@ -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 diff --git a/src/Kind/Reduce.hs b/src/Kind/Reduce.hs index c9bbb2583..e09405993 100644 --- a/src/Kind/Reduce.hs +++ b/src/Kind/Reduce.hs @@ -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 @@ -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 -- ------------- @@ -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 @@ -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 @@ -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) diff --git a/src/Kind/Show.hs b/src/Kind/Show.hs index 3683fd630..759a4d031 100644 --- a/src/Kind/Show.hs +++ b/src/Kind/Show.hs @@ -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 diff --git a/src/Kind/Type.hs b/src/Kind/Type.hs index 3055e57ef..a7b1f7ac1 100644 --- a/src/Kind/Type.hs +++ b/src/Kind/Type.hs @@ -65,6 +65,9 @@ data Term -- Unification Metavar | Met Int [Term] + -- Logging + | Log Term Term + -- Variable | Var String Int