diff --git a/playground/samples/aoc2024/Day17.newt b/playground/samples/aoc2024/Day17.newt new file mode 120000 index 0000000..a935098 --- /dev/null +++ b/playground/samples/aoc2024/Day17.newt @@ -0,0 +1 @@ +../../../aoc2024/Day17.newt \ No newline at end of file diff --git a/playground/samples/aoc2024/day17 b/playground/samples/aoc2024/day17 new file mode 120000 index 0000000..6390349 --- /dev/null +++ b/playground/samples/aoc2024/day17 @@ -0,0 +1 @@ +../../../aoc2024/day17 \ No newline at end of file diff --git a/src/Lib/Compile.idr b/src/Lib/Compile.idr index 39d5693..1056001 100644 --- a/src/Lib/Compile.idr +++ b/src/Lib/Compile.idr @@ -85,6 +85,21 @@ fresh nm env = if free env.env nm then nm else go nm 1 go : String -> Nat -> String go nm k = let nm' = "\{nm}\{show k}" in if free env.env nm' then nm' else go nm (S k) +fresh' : String -> JSEnv -> (String, JSEnv) +fresh' nm env = + let nm' = fresh nm env -- "\{nm}$\{show $ length env}" + env' = push env (Var nm') + in (nm', env') + +freshNames : List String -> JSEnv -> (List String, JSEnv) +freshNames nms env = go nms env [<] + where + go : List Name -> JSEnv -> SnocList Name -> (List String, JSEnv) + go Nil env acc = (acc <>> Nil, env) + go (n :: ns) env acc = + let (n', env') = fresh' n env + in go ns env' (acc :< n') + -- This is inspired by A-normalization, look into the continuation monad -- There is an index on JSStmt, adopted from Stefan Hoeck's code. -- @@ -97,12 +112,10 @@ termToJS env (CBnd k) f = case getAt k env.env of Nothing => ?bad_bounds termToJS env CErased f = f JUndefined termToJS env (CLam nm t) f = - let nm' = fresh nm env -- "\{nm}$\{show $ length env}" - env' = push env (Var nm') + let (nm',env') = fresh' nm env -- "\{nm}$\{show $ length env}" in f $ JLam [nm'] (termToJS env' t JReturn) termToJS env (CFun nms t) f = - let nms' = map (\nm => fresh nm env) nms - env' = foldl (\ e, nm => push e (Var nm)) env nms' + let (nms', env') = freshNames nms env in f $ JLam nms' (termToJS env' t JReturn) termToJS env (CRef nm) f = f $ Var nm termToJS env (CMeta k) f = f $ LitString "META \{show k}"