-3

index.html

reviewed

··· 226 226 font-family: "Computer Modern Sans"; 227 227 color: var(--constructor-col); 228 228 } 229 229 - .term-app-telescope { 230 230 - vertical-align: sub; 231 231 - } 232 229 .term-constructor { 233 230 font-family: "Computer Modern Sans"; 234 231 color: var(--constructor-col);

+7 -3

src/HOTerm.res

reviewed

··· 462 462 | UnifyFail(_) => [] 463 463 } 464 464 } 465 465 - let place = (x: int, ~scope as _: array<string>) => Schematic({ 466 466 - schematic: x, 467 467 - }) 465 465 + let place = (x: int, ~scope: array<string>) => 466 466 + app( 467 467 + Schematic({ 468 468 + schematic: x, 469 469 + }), 470 470 + Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})), 471 471 + ) 468 472 let prettyPrintVar = (idx: int, scope: array<string>) => 469 473 switch scope[idx] { 470 474 | Some(n) if Array.indexOf(scope, n) == idx => n

+9 -2

tests/HOTermTest.res

reviewed

··· 271 271 t->block("divergent", t => { 272 272 let divergent = "((x. x x) (x. x x))" 273 273 let a = "((x. ?0 x) (x. x x))" 274 274 - // TODO: should it not unify or not? 275 275 - t->Util.testNotUnify(a, divergent) 274 274 + // we don't care 275 275 + // t->Util.testNotUnify(a, divergent) 276 276 }) 277 277 t->block("dup var", t => { 278 278 let a = "(?0 \\0 \\0)" ··· 304 304 let a = "(?0 (fst l) l)" 305 305 let b = "(cons l)" 306 306 t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. cons x)"))) 307 307 + }) 308 308 + t->block("nat tests", t => { 309 309 + let a = "(Nat (S ?6))" 310 310 + let b = "(Nat (S (S \\0)))" 311 311 + let c = "(Nat (S (?6 \\0)))" 312 312 + t->Util.testNotUnify(a, b) 313 313 + t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)"))) 307 314 }) 308 315 })