dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

[ codegen ] PiType no longer hard-coded JS

Browse Source
This commit is contained in:
Steve Dunham
2025-07-26 07:23:16 -07:00
parent 43c06e7377
commit 1bdac27097
3 changed files with 4 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

2
src/Lib/Compile.newt
View File

@@ -302,7 +302,7 @@ getNames : Tm -> List QName -> List QName
getNames (Ref x nm) acc = nm :: acc getNames (Ref x nm) acc = nm :: acc
getNames (Lam x str _ _ t) acc = getNames t acc getNames (Lam x str _ _ t) acc = getNames t acc
getNames (App x t u) acc = getNames u $ getNames t acc getNames (App x t u) acc = getNames u $ getNames t acc
getNames (Pi x str icit y t u) acc = getNames u $ getNames t acc getNames (Pi x str icit y t u) acc = getNames u $ getNames t $ QN primNS "PiType" :: acc
getNames (Let x str t u) acc = getNames u $ getNames t acc getNames (Let x str t u) acc = getNames u $ getNames t acc
getNames (LetRec x str _ t u) acc = getNames u $ getNames t acc getNames (LetRec x str _ t u) acc = getNames u $ getNames t acc
getNames (Case x t alts) acc = foldl getAltNames acc alts getNames (Case x t alts) acc = foldl getAltNames acc alts

2
src/Lib/CompileExp.newt
View File

@@ -143,7 +143,7 @@ compileTerm (UU _) = pure $ CRef (QN Nil "U")
compileTerm (Pi _ nm icit rig t u) = do compileTerm (Pi _ nm icit rig t u) = do
t' <- compileTerm t t' <- compileTerm t
u' <- compileTerm u u' <- compileTerm u
pure $ CAppRef (QN Nil "PiType") (t' :: CLam nm u' :: Nil) 0 pure $ CAppRef (QN primNS "PiType") (t' :: CLam nm u' :: Nil) 0
compileTerm (Case fc t alts) = do compileTerm (Case fc t alts) = do
t' <- compileTerm t t' <- compileTerm t
alts' <- for alts $ \case alts' <- for alts $ \case

4
src/Main.newt
View File

@@ -21,6 +21,7 @@ import Lib.Syntax
import Node import Node
import Serialize import Serialize
-- For editors, dump some information about the context (fc, name, type)
jsonTopContext : M Json jsonTopContext : M Json
jsonTopContext = do jsonTopContext = do
top <- getTop top <- getTop
@@ -50,7 +51,6 @@ writeSource fn = do
docs <- compile docs <- compile
let src = unlines $ let src = unlines $
( "\"use strict\";" ( "\"use strict\";"
:: "const PiType = (h0, h1) => ({ tag: \"PiType\", h0, h1 });"
:: "const bouncer = (f,ini) => { let obj = ini; while (obj.tag !== 'return') obj = f(obj); return obj.h0 };" :: "const bouncer = (f,ini) => { let obj = ini; while (obj.tag !== 'return') obj = f(obj); return obj.h0 };"
:: Nil) :: Nil)
++ map (render 90 ∘ noAlt) docs ++ map (render 90 ∘ noAlt) docs
@@ -230,6 +230,7 @@ processFile fn = do
processDecl primNS (PType emptyFC "Int" Nothing) processDecl primNS (PType emptyFC "Int" Nothing)
processDecl primNS (PType emptyFC "String" Nothing) processDecl primNS (PType emptyFC "String" Nothing)
processDecl primNS (PType emptyFC "Char" Nothing) processDecl primNS (PType emptyFC "Char" Nothing)
setDef (QN primNS "PiType") emptyFC (Erased emptyFC) (PrimFn "(h0, h1) => ({ tag: \"PiType\", h0, h1 });" (S (S Z)) Nil) Nil
top <- getTop top <- getTop
let modules = updateMap primNS (MkModCtx "" top.defs (MC EmptyMap Nil 0 CheckAll) top.ops) top.modules let modules = updateMap primNS (MkModCtx "" top.defs (MC EmptyMap Nil 0 CheckAll) top.ops) top.modules
@@ -241,7 +242,6 @@ processFile fn = do
showErrors fn src showErrors fn src
pure MkUnit pure MkUnit
cmdLine : List String -> M (Maybe String × List String) cmdLine : List String -> M (Maybe String × List String)
cmdLine Nil = pure (Nothing, Nil) cmdLine Nil = pure (Nothing, Nil)
cmdLine ("--top" :: args) = cmdLine args -- handled later cmdLine ("--top" :: args) = cmdLine args -- handled later