fix issue with dup names in output
This commit is contained in:
1
playground/samples/aoc2024/Day17.newt
Symbolic link
1
playground/samples/aoc2024/Day17.newt
Symbolic link
@@ -0,0 +1 @@
|
|||||||
|
../../../aoc2024/Day17.newt
|
||||||
1
playground/samples/aoc2024/day17
Symbolic link
1
playground/samples/aoc2024/day17
Symbolic link
@@ -0,0 +1 @@
|
|||||||
|
../../../aoc2024/day17
|
||||||
@@ -85,6 +85,21 @@ fresh nm env = if free env.env nm then nm else go nm 1
|
|||||||
go : String -> Nat -> String
|
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)
|
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
|
-- This is inspired by A-normalization, look into the continuation monad
|
||||||
-- There is an index on JSStmt, adopted from Stefan Hoeck's code.
|
-- 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
|
Nothing => ?bad_bounds
|
||||||
termToJS env CErased f = f JUndefined
|
termToJS env CErased f = f JUndefined
|
||||||
termToJS env (CLam nm t) f =
|
termToJS env (CLam nm t) f =
|
||||||
let nm' = fresh nm env -- "\{nm}$\{show $ length env}"
|
let (nm',env') = fresh' nm env -- "\{nm}$\{show $ length env}"
|
||||||
env' = push env (Var nm')
|
|
||||||
in f $ JLam [nm'] (termToJS env' t JReturn)
|
in f $ JLam [nm'] (termToJS env' t JReturn)
|
||||||
termToJS env (CFun nms t) f =
|
termToJS env (CFun nms t) f =
|
||||||
let nms' = map (\nm => fresh nm env) nms
|
let (nms', env') = freshNames nms env
|
||||||
env' = foldl (\ e, nm => push e (Var nm)) env nms'
|
|
||||||
in f $ JLam nms' (termToJS env' t JReturn)
|
in f $ JLam nms' (termToJS env' t JReturn)
|
||||||
termToJS env (CRef nm) f = f $ Var nm
|
termToJS env (CRef nm) f = f $ Var nm
|
||||||
termToJS env (CMeta k) f = f $ LitString "META \{show k}"
|
termToJS env (CMeta k) f = f $ LitString "META \{show k}"
|
||||||
|
|||||||
Reference in New Issue
Block a user