the next generation of the in-browser educational proof assistant
1
fork

Configure Feed

Select the types of activity you want to include in your feed.

it is substDeBruijn

12078d2f f1b1926e

+34 -34
+34 -34
src/HOTerm.res
··· 217 217 s->Map.set(schematic, term) 218 218 s 219 219 } 220 + let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 221 + switch term { 222 + | Symbol(_) => term 223 + | Var({idx: var}) => 224 + if var < from { 225 + term 226 + } else if var - from < Array.length(substs) && var - from >= 0 { 227 + Option.getUnsafe(substs[var - from]) 228 + } else { 229 + Var({idx: var - Array.length(substs)}) 230 + } 231 + | Schematic({schematic, allowed}) => 232 + Schematic({ 233 + schematic, 234 + allowed: Array.filterMap(allowed, i => 235 + if i < from + Array.length(substs) { 236 + None 237 + } else { 238 + Some(i - (from + Array.length(substs))) 239 + } 240 + ), 241 + }) 242 + | Lam({name, body}) => 243 + Lam({ 244 + name, 245 + body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from=from + 1), 246 + }) 247 + | App({func, arg}) => 248 + App({ 249 + func: substDeBruijn(func, substs, ~from), 250 + arg: substDeBruijn(arg, substs, ~from), 251 + }) 252 + } 220 253 let rec lam = (amount: int, term: t): t => 221 254 if amount <= 0 { 222 255 term ··· 240 273 switch term { 241 274 | App({func, arg}) => 242 275 switch reduce(func) { 243 - | Lam({body}) => reduce(downshift(substitute(body, singletonSubst(0, upshift(arg, 1))), 1)) 276 + | Lam({body}) => reduce(downshift(substDeBruijn(body, [upshift(arg, 1)], ~from=0), 1)) 244 277 | func => App({func, arg}) 245 278 } 246 279 | term => term ··· 342 375 | Some(s) => [s] 343 376 } 344 377 } 345 - let rec substDeBruijn = (term: t, substs: array<t>, ~from: int=0) => 346 - switch term { 347 - | Symbol(_) => term 348 - | Var({idx: var}) => 349 - if var < from { 350 - term 351 - } else if var - from < Array.length(substs) && var - from >= 0 { 352 - Option.getUnsafe(substs[var - from]) 353 - } else { 354 - Var({idx: var - Array.length(substs)}) 355 - } 356 - | Schematic({schematic, allowed}) => 357 - Schematic({ 358 - schematic, 359 - allowed: Array.filterMap(allowed, i => 360 - if i < from + Array.length(substs) { 361 - None 362 - } else { 363 - Some(i - (from + Array.length(substs))) 364 - } 365 - ), 366 - }) 367 - | Lam({name, body}) => 368 - Lam({ 369 - name, 370 - body: substDeBruijn(body, substs->Array.map(term => upshift(term, 1)), ~from), 371 - }) 372 - | App({func, arg}) => 373 - App({ 374 - func: substDeBruijn(func, substs, ~from), 375 - arg: substDeBruijn(arg, substs, ~from), 376 - }) 377 - } 378 378 let place = (x: int, ~scope: array<string>) => Schematic({ 379 379 schematic: x, 380 380 allowed: Array.fromInitializer(~length=Array.length(scope), i => i),