From 796d93d7d93ed802ad8983011f650e0121b4fe5d Mon Sep 17 00:00:00 2001 From: Steve Dunham Date: Sat, 7 Sep 2024 11:26:11 -0700 Subject: [PATCH] tighten up generated code --- newt/testcase.newt | 3 --- src/Lib/Compile.idr | 11 +++++++++-- 2 files changed, 9 insertions(+), 5 deletions(-) diff --git a/newt/testcase.newt b/newt/testcase.newt index b437cad..6a0c939 100644 --- a/newt/testcase.newt +++ b/newt/testcase.newt @@ -43,9 +43,6 @@ length = \ v => case v of data Unit : U where MkUnit : Unit -foo : Vect (S Z) Unit -foo = Cons MkUnit Nil - -- This should fail (and does!) -- bar : Vect (S Z) Unit -- bar = (Cons MkUnit (Cons MkUnit Nil)) diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index feb916c..8df3c50 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -94,10 +94,17 @@ termToJS env (CRef nm) f = f $ Var nm termToJS env (CMeta k) f = f $ LitString "META \{show k}" termToJS env (CLit (LString str)) f = f (LitString str) termToJS env (CLit (LInt i)) f = f (LitInt i) +-- if it's a var, just use the original +termToJS env (CLet nm (CBnd k) u) f = case getAt k env of + Just e => termToJS (e :: env) u f + Nothing => ?bad_bounds2 termToJS env (CLet nm t u) f = let nm' = fresh nm env env' = (Var nm' :: env) - in JSnoc (JLet nm' $ termToJS env t (JAssign nm')) (termToJS env' u f) + -- If it's a simple term, use const + in case termToJS env t (JAssign nm') of + (JAssign _ exp) => JSnoc (JConst nm' exp) (termToJS env' u f) + t' => JSnoc (JLet nm' t') (termToJS env' u f) termToJS env (CApp t args) f = termToJS env t (\ t' => argsToJS args [<] (\ args' => f (Apply t' args'))) where @@ -120,7 +127,7 @@ termToJS env (CCase t alts) f = where termToJSAlt : String -> CAlt -> JAlt termToJSAlt nm (CConAlt name args u) = JConAlt name (termToJS (mkEnv nm 0 env args) u f) - -- intentially reusing scrutinee name here + -- intentionally reusing scrutinee name here termToJSAlt nm (CDefAlt u) = JDefAlt (termToJS (Var nm :: env) u f) label : JSExp -> (String -> JSStmt e) -> JSStmt e label (Var nm) f = f nm