HOTerm atom fixes #8

+31

index.html

reviewed

··· 307 307 -------- sucnatt 308 308 (natt x (S n)) 309 309 </hol-inductive> 310 310 + <hol-inductive id="index.html/mexp-hol" deps="index.html/myconfig"> 311 311 + ---- M-Empty 312 312 + (M "") 313 313 + s. 314 314 + (M "$s") 315 315 + -------- M-Surround 316 316 + (M "( $s )") 317 317 + s1.s2. 318 318 + (M "$s1") 319 319 + (M "$s2") 320 320 + --------- M-Juxtapose 321 321 + (M "$s1 $s2") 322 322 + s. 323 323 + (L "$s") 324 324 + -------- N-Surr 325 325 + (N "( $s )") 326 326 + 327 327 + ---- L-Empty 328 328 + (L "") 329 329 + s1.s2. 330 330 + (N "$s1") 331 331 + (L "$s2") 332 332 + --------- L-Juxtapose 333 333 + (L "$s1 $s2") 334 334 + </hol-inductive> 335 335 + <hol-proof id="index.html/lexp-n-hol" deps="index.html/myconfig index.html/mexp-hol"> 336 336 + s. (N "$s") 337 337 + --------N-L 338 338 + (L "$s") 339 339 + s. sn |- ? 340 340 + </hol-proof> 310 341 <hol-comp id="index.html/baz" deps="index.html/myconfig"> 311 342 x.y. 312 343 (/\ x y)

+46 -67

src/HOTerm.res

reviewed

··· 3 3 let cmp = Pervasives.compare 4 4 }) 5 5 6 6 - module type ATOM = AtomDef.ATOM 7 7 - 8 8 - module DefaultAtom = { 9 9 - module Base = AtomBase.Make({ 10 10 - type t = string 11 11 - }) 12 12 - type t = string 13 13 - type subst = Map.t<int, string> 14 14 - let unify = (a, b, ~gen as _=?) => 15 15 - if a == b { 16 16 - Seq.once(Map.make()) 17 17 - } else { 18 18 - Seq.empty 19 19 - } 20 20 - let prettyPrint = (name, ~scope as _: array<string>) => name 21 21 - let symbolRegexpString = "^([^\\s()]+)" 22 22 - let parse = (str0, ~scope as _: array<string>, ~gen as _=?) => { 23 23 - let str = str0->String.trimStart 24 24 - let re = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") 25 25 - switch re->RegExp.exec(str) { 26 26 - | None => Error("invalid symbol") 27 27 - | Some(res) => 28 28 - switch RegExp.Result.matches(res) { 29 29 - | [name] => Ok((name, String.sliceToEnd(str, ~start=RegExp.lastIndex(re)))) 30 30 - | _ => Error("invalid symbol") 31 31 - } 32 32 - } 33 33 - } 34 34 - let substitute = (name, _) => name 35 35 - let substDeBruijn = (name, _, ~from as _=?) => name 36 36 - let concrete = _ => true 37 37 - let upshift = (t, _, ~from as _=?) => t 38 38 - let coerce = _ => None 39 39 - let reduce = t => t 40 40 - } 41 41 - 42 42 - module Make = (Atom: AtomDef.ATOM): { 6 6 + module type S = { 7 7 + module Atom: AtomDef.ATOM_CHOICE 43 8 type rec t = 44 9 | Symbol({name: Atom.t, constructor: bool}) 45 10 | Var({idx: int}) ··· 64 29 let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst> 65 30 let reduceSubst: subst => subst 66 31 let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t) 67 67 - } => { 32 32 + let isEqualityAtom: Atom.t => bool 33 33 + } 34 34 + 35 35 + module Make = (Atom: AtomDef.ATOM_CHOICE): (S with module Atom = Atom) => { 36 36 + module Atom = Atom 68 37 type rec t = 69 38 | Symbol({name: Atom.t, constructor: bool}) 70 39 | Var({idx: int}) ··· 245 214 assert(subst->Belt.Map.Int.has(schematic) == false) 246 215 subst->Belt.Map.Int.set(schematic, term) 247 216 } 217 217 + let rec strip = (term: t): (t, array<t>) => { 218 218 + switch term { 219 219 + | App({func, arg}) => 220 220 + let (peeledFunc, peeledArgs) = strip(func) 221 221 + (peeledFunc, Array.concat(peeledArgs, [arg])) 222 222 + | _ => (term, []) 223 223 + } 224 224 + } 225 225 + let lower = (term: t): option<Atom.t> => 226 226 + switch term { 227 227 + | Symbol(s) => Some(s.name) 228 228 + | Var({idx}) => Atom.coerce(AtomBase.VarBase.wrap(Var({idx: idx}))) 229 229 + | _ => 230 230 + switch strip(term) { 231 231 + | (Schematic({schematic}), ts) => 232 232 + ts 233 233 + ->Array.map(t => 234 234 + switch t { 235 235 + | Var({idx}) => Some(idx) 236 236 + | _ => None 237 237 + } 238 238 + ) 239 239 + ->Util.Option.sequence 240 240 + ->Option.flatMap(allowed => 241 241 + Atom.coerce(AtomBase.VarBase.wrap(Schematic({schematic, allowed}))) 242 242 + ) 243 243 + | _ => None 244 244 + } 245 245 + } 248 246 let rec substitute = (term: t, subst: subst) => 249 247 switch term { 250 248 | Schematic({schematic, _}) => ··· 264 262 arg: substitute(arg, subst), 265 263 }) 266 264 | Symbol({name, constructor}) => { 267 267 - let symbolSubst = subst->Belt.Map.Int.reduce(Map.make(), (acc, k, v) => { 268 268 - switch v { 269 269 - | Symbol({name}) => { 270 270 - acc->Map.set(k, name) 271 271 - acc 272 272 - } 273 273 - | _ => acc 274 274 - } 265 265 + let symbolSubst = Map.make() 266 266 + subst->Belt.Map.Int.forEach((k, v) => { 267 267 + lower(v)->Option.map(v => Map.set(symbolSubst, k, v))->ignore 275 268 }) 276 269 Symbol({name: Atom.substitute(name, symbolSubst), constructor}) 277 270 } ··· 282 275 switch term { 283 276 | Symbol({name, constructor}) => 284 277 Symbol({ 285 285 - name: Atom.substDeBruijn( 286 286 - name, 287 287 - substs->Array.map(t => 288 288 - switch t { 289 289 - | Symbol({name}) => Some(name) 290 290 - | _ => None 291 291 - } 292 292 - ), 293 293 - ~from, 294 294 - ), 278 278 + name: Atom.substDeBruijn(name, substs->Array.map(lower), ~from), 295 279 constructor, 296 280 }) 297 281 | Var({idx: var}) => ··· 400 384 let lam = (is: array<t>, g: t, js: array<t>): t => { 401 385 lams(is->Array.length, app(g, js->Array.map(j => idx1'(is, j)))) 402 386 } 403 403 - let rec strip = (term: t): (t, array<t>) => { 404 404 - switch term { 405 405 - | App({func, arg}) => 406 406 - let (peeledFunc, peeledArgs) = strip(func) 407 407 - (peeledFunc, Array.concat(peeledArgs, [arg])) 408 408 - | _ => (term, []) 409 409 - } 410 410 - } 411 387 let rec devar = (subst: subst, term: t): t => { 412 388 let (func, args) = strip(term) 413 389 switch func { ··· 570 546 } 571 547 | ((a, xs), (b, ys)) => 572 548 switch (a, b) { 573 573 - | (Symbol(_) | Var(_), Symbol(_) | Var(_)) => 549 549 + | (Symbol(_), Symbol(_)) | (Var(_), Var(_)) => 574 550 unifyTerm(a, b, subst, ~gen)->Seq.flatMap(subst => unifyArray(xs, ys, subst, ~gen)) 575 551 | _ => Seq.empty 576 552 } ··· 630 606 Array.fromInitializer(~length=Array.length(scope), i => Var({idx: i})), 631 607 ) 632 608 609 609 + let isEqualityAtom = (AtomBase.AnyValue(tag, v): Atom.t): bool => 610 610 + switch tag { 611 611 + | Symbolic.Base.Tag => v == "=" 612 612 + | _ => false 613 613 + } 633 614 let prettyPrintVar = (idx: int, scope: array<string>) => 634 615 switch scope[idx] { 635 616 | Some(n) if Array.indexOf(scope, n) == idx => n ··· 874 855 } 875 856 let mapTerms = (t, f) => f(t) 876 857 } 877 877 - 878 878 - include Make(DefaultAtom)

+4 -30

src/HOTerm.resi

reviewed

··· 1 1 - module type ATOM = AtomDef.ATOM 2 2 - 3 3 - module Make: (Atom: AtomDef.ATOM) => 4 4 - { 1 1 + module type S = { 2 2 + module Atom: AtomDef.ATOM_CHOICE 5 3 type rec t = 6 4 | Symbol({name: Atom.t, constructor: bool}) 7 5 | Var({idx: int}) ··· 26 24 let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst> 27 25 let reduceSubst: subst => subst 28 26 let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t) 27 27 + let isEqualityAtom: Atom.t => bool 29 28 } 30 29 31 31 - type rec t = 32 32 - | Symbol({name: string, constructor: bool}) 33 33 - | Var({idx: int}) 34 34 - | Schematic({schematic: int}) 35 35 - | Lam({name: string, body: t}) 36 36 - | App({func: t, arg: t}) 37 37 - // Unallowed is used internally in unify, where Nipkow 1993 uses Var(-infinity) 38 38 - | Unallowed 39 39 - 40 40 - include Signatures.TERM 41 41 - with type t := t 42 42 - and type meta = string 43 43 - and type schematic = int 44 44 - and type subst = Belt.Map.Int.t<t> 45 45 - 46 46 - let emptySubst: subst 47 47 - let strip: t => (t, array<t>) 48 48 - let app: (t, array<t>) => t 49 49 - let mkvars: int => array<t> 50 50 - let mapTerms: (t, t => t) => t 51 51 - // exposed for testing purposes 52 52 - exception UnifyFail(string) 53 53 - let substAdd: (subst, schematic, t) => subst 54 54 - let unifyTerm: (t, t, subst, ~gen: option<gen>) => Seq.t<subst> 55 55 - let reduceSubst: subst => subst 56 56 - let rewrite: (t, t, t, ~subst: subst, ~gen: option<gen>) => (subst, t) 30 30 + module Make: (Atom: AtomDef.ATOM_CHOICE) => (S with module Atom = Atom)

-6

src/HOTermJView.res

reviewed

··· 1 1 - module TermView = HOTermView 2 2 - type props = { 3 3 - judgment: HOTerm.t, 4 4 - scope: array<string>, 5 5 - } 6 6 - let make = ({judgment, scope}) => HOTermView.make({term: judgment, scope})

-1

src/HOTermJView.resi

reviewed

··· 1 1 - include Signatures.JUDGMENT_VIEW with module Term := HOTerm and module Judgment := HOTerm

+24 -10

src/HOTermMethod.res

reviewed

··· 2 2 open Method 3 3 4 4 module MakeRewriteHOTerm = ( 5 5 + HOTerm: HOTerm.S, 5 6 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 6 7 Config: { 7 8 let keyword: string ··· 16 17 let extractEqualityTermsFromJudgment = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => { 17 18 let term: HOTerm.t = judgment 18 19 switch HOTerm.strip(term) { 19 19 - | (HOTerm.Symbol({name: "="}), args) if Array.length(args) == 2 => 20 20 + | (HOTerm.Symbol({name}), args) if HOTerm.isEqualityAtom(name) && Array.length(args) == 2 => 20 21 Some((args->Array.getUnsafe(0), args->Array.getUnsafe(1))) 21 22 | _ => None 22 23 } ··· 247 248 } 248 249 249 250 module Rewrite = ( 251 251 + HOTerm: HOTerm.S, 250 252 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 251 253 ) => MakeRewriteHOTerm( 254 254 + HOTerm, 252 255 Judgment, 253 256 { 254 257 let keyword = "rewrite" ··· 257 260 ) 258 261 259 262 module RewriteReverse = ( 263 263 + HOTerm: HOTerm.S, 260 264 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 261 265 ) => MakeRewriteHOTerm( 266 266 + HOTerm, 262 267 Judgment, 263 268 { 264 269 let keyword = "rewrite_reverse" ··· 266 271 }, 267 272 ) 268 273 269 269 - module ConstructorNeq = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 274 274 + module ConstructorNeq = ( 275 275 + HOTerm: HOTerm.S, 276 276 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 277 277 + ) => { 270 278 module Term = HOTerm 271 279 module Rule = Rule.Make(HOTerm, Judgment) 272 280 module Context = Context(HOTerm, Judgment) ··· 278 286 let constructorHead = (term: HOTerm.t): option<constructorHead> => { 279 287 let (head, args) = HOTerm.strip(term) 280 288 switch head { 281 281 - | HOTerm.Symbol({name, constructor: true}) => Some({name, args}) 289 289 + | HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name), constructor: true}) => 290 290 + Some({name, args}) 282 291 | _ => None 283 292 } 284 293 } ··· 291 300 )> => { 292 301 let (head, args) = HOTerm.strip(term) 293 302 switch head { 294 294 - | HOTerm.Symbol({name: "="}) if Array.length(args) == 2 => 303 303 + | HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, "=")}) if Array.length(args) == 2 => 295 304 switch ( 296 305 constructorHead(args->Array.getUnsafe(0)), 297 306 constructorHead(args->Array.getUnsafe(1)), ··· 309 318 | Some((lhs, rhs)) => Some({lhs, rhs, negated: false}) 310 319 | None => 311 320 switch HOTerm.strip(reduced) { 312 312 - | (HOTerm.Symbol({name: "not"}), [inner]) => 321 321 + | (HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, "not")}), [inner]) => 313 322 extractConstructorEqualityFrom(inner)->Option.map(((lhs, rhs)) => {lhs, rhs, negated: true}) 314 323 | _ => None 315 324 } ··· 352 361 } 353 362 } 354 363 355 355 - module ConstructorInj = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 364 364 + module ConstructorInj = ( 365 365 + HOTerm: HOTerm.S, 366 366 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 367 367 + ) => { 356 368 module Rule = Rule.Make(HOTerm, Judgment) 357 369 module Context = Context(HOTerm, Judgment) 358 370 module Results = MethodResults(HOTerm) ··· 416 428 let (lHead, lArgs) = args->Array.getUnsafe(0)->HOTerm.strip 417 429 let (rHead, rArgs) = args->Array.getUnsafe(1)->HOTerm.strip 418 430 switch (lHead, rHead) { 419 419 - | (HOTerm.Symbol({name: ln, constructor: true}), HOTerm.Symbol({name: rn, constructor: true})) 420 420 - if ln == rn && lArgs->Array.length == rArgs->Array.length => 431 431 + | ( 432 432 + HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, ln), constructor: true}), 433 433 + HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, rn), constructor: true}), 434 434 + ) if ln == rn && lArgs->Array.length == rArgs->Array.length => 421 435 Some((ln, lArgs, rArgs)) 422 436 | _ => None 423 437 } ··· 427 441 let apply = (ctx: Context.t, j: Judgment.t, _gen: HOTerm.gen, _f: Rule.t => 'a) => { 428 442 let ret = Dict.make() 429 443 switch j->Judgment.reduce->HOTerm.strip { 430 430 - | (HOTerm.Symbol({name: "="}), [lhs, rhs]) => 444 444 + | (HOTerm.Symbol({name}), [lhs, rhs]) if HOTerm.isEqualityAtom(name) => 431 445 ctx 432 446 ->Context.facts 433 447 ->Dict.forEachWithKey((fact, name) => { ··· 452 466 let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => { 453 467 switch (ctx->Context.facts->Dict.get(it.source), goal->Judgment.reduce->HOTerm.strip) { 454 468 | (None, _) => Error(`Cannot find equality '${it.source}'`) 455 455 - | (Some(fact), (HOTerm.Symbol({name: "="}), [lhs, rhs])) => 469 469 + | (Some(fact), (HOTerm.Symbol({name}), [lhs, rhs])) if HOTerm.isEqualityAtom(name) => 456 470 switch extractConstructorEquality(fact.conclusion) { 457 471 | None => Error(`'${it.source}' is not a constructor equality`) 458 472 | Some((_cName, lArgs, rArgs)) =>

+80 -74

src/HOTermView.res

reviewed

··· 1 1 open Util 2 2 - type idx_props = {idx: int, scope: array<string>} 3 3 - let viewVar = (props: idx_props) => 4 4 - switch props.scope[props.idx] { 5 5 - | Some(n) if Array.indexOf(props.scope, n) == props.idx => 6 6 - <span className="term-metavar"> {React.string(n)} </span> 7 7 - | _ => 8 8 - <span className="term-metavar-unnamed"> 9 9 - {React.string("\\")} 10 10 - {React.int(props.idx)} 11 11 - </span> 12 12 - } 2 2 + module Make = ( 3 3 + Atom: AtomDef.ATOM_CHOICE, 4 4 + AtomView: AtomDef.ATOM_VIEW with module Atom := Atom, 5 5 + HOTerm: HOTerm.S with module Atom := Atom, 6 6 + ) => { 7 7 + type idx_props = {idx: int, scope: array<string>} 8 8 + let viewVar = (props: idx_props) => 9 9 + switch props.scope[props.idx] { 10 10 + | Some(n) if Array.indexOf(props.scope, n) == props.idx => 11 11 + <span className="term-metavar"> {React.string(n)} </span> 12 12 + | _ => 13 13 + <span className="term-metavar-unnamed"> 14 14 + {React.string("\\")} 15 15 + {React.int(props.idx)} 16 16 + </span> 17 17 + } 13 18 14 14 - let makeMeta = (str: string) => 15 15 - <span className="rule-binder"> 16 16 - {React.string(str)} 17 17 - {React.string(".")} 18 18 - </span> 19 19 + let makeMeta = (str: string) => 20 20 + <span className="rule-binder"> 21 21 + {React.string(str)} 22 22 + {React.string(".")} 23 23 + </span> 19 24 20 20 - let parenthesise = f => 21 21 - [ 22 22 - <span className="symbol" key={"-1"}> {React.string("(")} </span>, 23 23 - ...f, 24 24 - <span className="symbol" key={"-2"}> {React.string(")")} </span>, 25 25 - ] 25 25 + let parenthesise = f => 26 26 + [ 27 27 + <span className="symbol" key={"-1"}> {React.string("(")} </span>, 28 28 + ...f, 29 29 + <span className="symbol" key={"-2"}> {React.string(")")} </span>, 30 30 + ] 26 31 27 27 - let intersperse = a => 28 28 - a->Array.flatMapWithIndex((e, i) => 29 29 - if i == 0 { 30 30 - [e] 31 31 - } else { 32 32 - [React.string(" "), e] 33 33 - } 34 34 - ) 35 35 - type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool} 36 36 - @react.componentWithProps 37 37 - let rec make1 = ({term, scope, brackets}) => 38 38 - switch term { 39 39 - | Var({idx}) => viewVar({idx, scope}) 40 40 - | Symbol({name: s}) => <span className="term-const"> {React.string(s)} </span> 41 41 - | Schematic({schematic: s}) => 42 42 - <span className="term-schematic"> 43 43 - {React.string("?")} 44 44 - {React.int(s)} 45 45 - </span> 46 46 - | App(_) => 47 47 - switch HOTerm.strip(term) { 48 48 - | (Symbol({name: "="}), args) if Array.length(args) == 2 => 49 49 - <span className="term-equality"> 50 50 - {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})} 51 51 - {React.string("=")} 52 52 - {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})} 53 53 - </span> 54 54 - | (func, args) => 55 55 - let xs = Array.concat([func], args) 56 56 - let a = 57 57 - <span className="term-app"> 58 58 - {xs 59 59 - ->Array.mapWithIndex((t, i) => 60 60 - React.createElement(make1, withKey({term: t, scope, brackets: true}, i)) 61 61 - ) 62 62 - ->intersperse 63 63 - ->React.array} 64 64 - </span> 65 65 - if brackets { 66 66 - [a]->parenthesise->React.array 32 32 + let intersperse = a => 33 33 + a->Array.flatMapWithIndex((e, i) => 34 34 + if i == 0 { 35 35 + [e] 67 36 } else { 68 68 - a 37 37 + [React.string(" "), e] 69 38 } 70 70 - } 71 71 - | Lam({name, body}) => { 72 72 - let newScope = Array.concat([name], scope) 73 73 - <span className="term-lambda"> 74 74 - {React.string(name)} 75 75 - {React.createElement(make1, {term: body, scope: newScope, brackets: false})} 39 39 + ) 40 40 + type props1 = {term: HOTerm.t, scope: array<string>, brackets: bool} 41 41 + @react.componentWithProps 42 42 + let rec make1 = ({term, scope, brackets}) => 43 43 + switch term { 44 44 + | Var({idx}) => viewVar({idx, scope}) 45 45 + | Symbol({name: s}) => <span className="term-const"> {AtomView.make({atom: s, scope})} </span> 46 46 + | Schematic({schematic: s}) => 47 47 + <span className="term-schematic"> 48 48 + {React.string("?")} 49 49 + {React.int(s)} 76 50 </span> 51 51 + | App(_) => 52 52 + switch HOTerm.strip(term) { 53 53 + | (Symbol({name: s}), args) if HOTerm.isEqualityAtom(s) && Array.length(args) == 2 => 54 54 + <span className="term-equality"> 55 55 + {React.createElement(make1, {term: args->Array.getUnsafe(0), scope, brackets: true})} 56 56 + {React.string("=")} 57 57 + {React.createElement(make1, {term: args->Array.getUnsafe(1), scope, brackets: true})} 58 58 + </span> 59 59 + | (func, args) => 60 60 + let xs = Array.concat([func], args) 61 61 + let a = 62 62 + <span className="term-app"> 63 63 + {xs 64 64 + ->Array.mapWithIndex((t, i) => 65 65 + React.createElement(make1, withKey({term: t, scope, brackets: true}, i)) 66 66 + ) 67 67 + ->intersperse 68 68 + ->React.array} 69 69 + </span> 70 70 + if brackets { 71 71 + [a]->parenthesise->React.array 72 72 + } else { 73 73 + a 74 74 + } 75 75 + } 76 76 + | Lam({name, body}) => { 77 77 + let newScope = Array.concat([name], scope) 78 78 + <span className="term-lambda"> 79 79 + {React.string(name)} 80 80 + {React.createElement(make1, {term: body, scope: newScope, brackets: false})} 81 81 + </span> 82 82 + } 83 83 + | Unallowed => <p> {React.string("Internal error: unallowed")} </p> 77 84 } 78 78 - | Unallowed => <p> {React.string("Internal error: unallowed")} </p> 79 79 - } 80 80 - type props = {term: HOTerm.t, scope: array<string>} 81 81 - @react.componentWithProps 82 82 - let make = ({term, scope}) => make1({term, scope, brackets: false}) 85 85 + type props = {term: HOTerm.t, scope: array<string>} 86 86 + @react.componentWithProps 87 87 + let make = ({term, scope}) => make1({term, scope, brackets: false}) 88 88 + }

+5 -1

src/HOTermView.resi

reviewed

··· 1 1 - include Signatures.TERM_VIEW with module Term := HOTerm 1 1 + module Make: ( 2 2 + Atom: AtomDef.ATOM_CHOICE, 3 3 + AtomView: AtomDef.ATOM_VIEW with module Atom := Atom, 4 4 + HOTerm: HOTerm.S with module Atom := Atom, 5 5 + ) => (Signatures.TERM_VIEW with module Term := HOTerm)

+15 -9

src/InductiveSet.res

reviewed

··· 3 3 4 4 // InductiveSet is specific to HOTerm to allow pattern matching on term structure 5 5 module Make = ( 6 6 - Term: TERM with type t = HOTerm.t and type meta = string, 7 7 - Judgment: JUDGMENT with module Term := Term and type t = HOTerm.t, 6 6 + Term: HOTerm.S, 7 7 + Judgment: JUDGMENT with module Term := Term and type t = Term.t, 8 8 JudgmentView: JUDGMENT_VIEW with module Term := Term and module Judgment := Judgment, 9 9 ) => { 10 10 + module HOTerm = Term 10 11 module Rule = Rule.Make(Term, Judgment) 11 12 module RuleView = RuleView.Make(Term, Judgment, JudgmentView) 12 13 module Ports = Ports(Term, Judgment) ··· 31 32 let extractPredicateSignature = (rule: Rule.t): option<(string, int)> => { 32 33 let (head, args) = HOTerm.strip(rule.conclusion) 33 34 switch head { 34 34 - | Symbol({name}) => Some((name, Array.length(args))) 35 35 + | Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name)}) => Some((name, Array.length(args))) 35 36 | _ => None 36 37 } 37 38 } ··· 64 65 let generateInductiveHypothesis = (premise: Rule.t, offset: int): option<Rule.t> => { 65 66 let (head, args) = HOTerm.strip(premise.conclusion) 66 67 switch head { 67 67 - | Symbol({name}) => 68 68 + | Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name)}) => 68 69 let formerIndex = findFormerIndex(name, Array.length(args)) 69 70 Some({ 70 71 Rule.vars: premise.vars, ··· 87 88 88 89 let (conclusionHead, conclusionArgs) = HOTerm.strip(constructorRule.conclusion) 89 90 let typeIndex = switch conclusionHead { 90 90 - | Symbol({name}) => findFormerIndex(name, Array.length(conclusionArgs)) 91 91 + | Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name)}) => 92 92 + findFormerIndex(name, Array.length(conclusionArgs)) 91 93 | _ => throw(Util.Unreachable("Constructor conclusion must have a Symbol head")) 92 94 } 93 95 ··· 110 112 { 111 113 Rule.vars: [], 112 114 premises: [], 113 113 - conclusion: HOTerm.app(HOTerm.Symbol({name: str, constructor: false}), makeVarArgs(i)), 115 115 + conclusion: HOTerm.app( 116 116 + HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, str), constructor: false}), 117 117 + makeVarArgs(i), 118 118 + ), 114 119 }, 115 120 ...subgoals, 116 121 ], ··· 126 131 let extractInductiveType = (premise: Rule.t): option<(string, int)> => { 127 132 let (head, args) = HOTerm.strip(premise.conclusion) 128 133 switch head { 129 129 - | Symbol({name}) => Some((name, Array.length(args))) 134 134 + | Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, name), constructor: false}) => 135 135 + Some((name, Array.length(args))) 130 136 | _ => None 131 137 } 132 138 } ··· 192 198 Rule.vars: [], 193 199 premises: [], 194 200 conclusion: HOTerm.app( 195 195 - HOTerm.Symbol({name: "=", constructor: false}), 201 201 + HOTerm.Symbol({name: AtomBase.AnyValue(Symbolic.Base.Tag, "="), constructor: false}), 196 202 [HOTerm.Var({idx: offset + idx}), arg], 197 203 ), 198 204 } ··· 214 220 Rule.vars: [], 215 221 premises: [], 216 222 conclusion: HOTerm.app( 217 217 - HOTerm.Symbol({name: str, constructor: false}), 223 223 + HOTerm.Symbol({name: Symbolic.Base.wrap(str), constructor: false}), 218 224 makeVarArgs(arity), 219 225 ), 220 226 },

+11 -5

src/MethodView.res

reviewed

··· 162 162 } 163 163 } 164 164 165 165 - module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t) => { 166 166 - module Method = Rewrite(Judgment) 165 165 + module RewriteView = ( 166 166 + HOTerm: HOTerm.S, 167 167 + Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 168 168 + ) => { 169 169 + module Method = Rewrite(HOTerm, Judgment) 167 170 type props<'a> = { 168 171 method: Method.t<'a>, 169 172 scope: array<HOTerm.meta>, ··· 203 206 } 204 207 205 208 module RewriteReverseView = ( 209 209 + HOTerm: HOTerm.S, 206 210 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 207 211 ) => { 208 208 - module Method = RewriteReverse(Judgment) 212 212 + module Method = RewriteReverse(HOTerm, Judgment) 209 213 type props<'a> = { 210 214 method: Method.t<'a>, 211 215 scope: array<HOTerm.meta>, ··· 245 249 } 246 250 247 251 module ConstructorNeqView = ( 252 252 + HOTerm: HOTerm.S, 248 253 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 249 254 ) => { 250 250 - module Method = ConstructorNeq(Judgment) 255 255 + module Method = ConstructorNeq(HOTerm, Judgment) 251 256 type props<'a> = { 252 257 method: Method.t<'a>, 253 258 scope: array<HOTerm.meta>, ··· 271 276 } 272 277 273 278 module ConstructorInjView = ( 279 279 + HOTerm: HOTerm.S, 274 280 Judgment: JUDGMENT with module Term := HOTerm and type t = HOTerm.t, 275 281 ) => { 276 276 - module Method = ConstructorInj(Judgment) 282 282 + module Method = ConstructorInj(HOTerm, Judgment) 277 283 type props<'a> = { 278 284 method: Method.t<'a>, 279 285 scope: array<HOTerm.meta>,

+33 -28

src/Scratch.res

reviewed

··· 1 1 + module Symbol = AtomDef.MakeAtomChoiceAndView( 2 2 + Symbolic.Atom, 3 3 + Symbolic.AtomView, 4 4 + AtomDef.EmptyAtomChoice, 5 5 + AtomDef.EmptyAtomChoiceView, 6 6 + ) 7 7 + module StringSymbol = AtomDef.MakeAtomChoiceAndView( 8 8 + StringA.Atom, 9 9 + StringA.AtomView, 10 10 + Symbol.Atom, 11 11 + Symbol.AtomView, 12 12 + ) 13 13 + module StringNatSymbol = AtomDef.MakeAtomChoiceAndView( 14 14 + AssocComm.Nat.Atom, 15 15 + AssocComm.Nat.AtomView, 16 16 + StringSymbol.Atom, 17 17 + StringSymbol.AtomView, 18 18 + ) 19 19 + module Final = AtomDef.MakeAtomChoiceAndView( 20 20 + Preludic.Atom, 21 21 + Preludic.AtomView, 22 22 + StringNatSymbol.Atom, 23 23 + StringNatSymbol.AtomView, 24 24 + ) 25 25 + 26 26 + module HOTerm = HOTerm.Make(StringSymbol.Atom) 27 27 + module HOTermView = HOTermView.Make(StringSymbol.Atom, StringSymbol.AtomView, HOTerm) 28 28 + 29 29 + module HOTermJView = TermViewAsJudgmentView.Make(HOTerm, HOTerm, HOTermView) 1 30 module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTerm, HOTermJView)) 2 31 module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTerm, HOTermJView)) 3 32 4 33 module EqualityViews = MethodView.CombineMethodView( 5 34 HOTerm, 6 35 HOTerm, 7 7 - MethodView.RewriteView(HOTerm), 8 8 - MethodView.RewriteReverseView(HOTerm), 36 36 + MethodView.RewriteView(HOTerm, HOTerm), 37 37 + MethodView.RewriteReverseView(HOTerm, HOTerm), 9 38 ) 10 39 module ConstructorEqualityViews = MethodView.CombineMethodView( 11 40 HOTerm, 12 41 HOTerm, 13 42 EqualityViews, 14 14 - MethodView.ConstructorNeqView(HOTerm), 43 43 + MethodView.ConstructorNeqView(HOTerm, HOTerm), 15 44 ) 16 45 module RewritesView = MethodView.CombineMethodView( 17 46 HOTerm, 18 47 HOTerm, 19 48 ConstructorEqualityViews, 20 20 - MethodView.ConstructorInjView(HOTerm), 49 49 + MethodView.ConstructorInjView(HOTerm, HOTerm), 21 50 ) 22 51 module DerivationsOrLemmasView = MethodView.CombineMethodView( 23 52 HOTerm, ··· 42 71 module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView)) 43 72 module ConfS = ConfigBlock.Make(HOTerm, HOTerm) 44 73 45 45 - module Symbol = AtomDef.MakeAtomChoiceAndView( 46 46 - Symbolic.Atom, 47 47 - Symbolic.AtomView, 48 48 - AtomDef.EmptyAtomChoice, 49 49 - AtomDef.EmptyAtomChoiceView, 50 50 - ) 51 51 - module StringSymbol = AtomDef.MakeAtomChoiceAndView( 52 52 - StringA.Atom, 53 53 - StringA.AtomView, 54 54 - Symbol.Atom, 55 55 - Symbol.AtomView, 56 56 - ) 57 57 - module StringNatSymbol = AtomDef.MakeAtomChoiceAndView( 58 58 - AssocComm.Nat.Atom, 59 59 - AssocComm.Nat.AtomView, 60 60 - StringSymbol.Atom, 61 61 - StringSymbol.AtomView, 62 62 - ) 63 63 - module Final = AtomDef.MakeAtomChoiceAndView( 64 64 - Preludic.Atom, 65 65 - Preludic.AtomView, 66 66 - StringNatSymbol.Atom, 67 67 - StringNatSymbol.AtomView, 68 68 - ) 69 74 module StringSExp = SExp.Make(Final.Atom) 70 75 module TermView = SExpView.Make(Final.Atom, Final.AtomView, StringSExp) 71 76 module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView)

+8

src/Util.res

reviewed

··· 168 168 | Some(a) => a 169 169 | None => f() 170 170 } 171 171 + let sequence = (xs: array<option<'a>>): option<array<'a>> => { 172 172 + let filtered = xs->Array.keepSome 173 173 + if Array.length(xs) == Array.length(filtered) { 174 174 + Some(filtered) 175 175 + } else { 176 176 + None 177 177 + } 178 178 + } 171 179 }

+40 -44

tests/HOTermTest.res

reviewed

··· 1 1 open Zora 2 2 - open HOTerm 3 3 - 4 4 - module Util = TestUtil.MakeTerm(HOTerm) 5 2 6 3 module Symbol = AtomDef.MakeAtomChoiceAndView( 7 4 Symbolic.Atom, ··· 9 6 AtomDef.EmptyAtomChoice, 10 7 AtomDef.EmptyAtomChoiceView, 11 8 ) 9 9 + module RegularHOTerm = HOTerm.Make(Symbol.Atom) 10 10 + module Util = TestUtil.MakeTerm(RegularHOTerm) 12 11 module StringSymbol = AtomDef.MakeAtomChoiceAndView( 13 12 StringA.Atom, 14 13 StringA.AtomView, ··· 27 26 }) 28 27 29 28 let testUnify0 = (t: Zora.t, at: string, bt: string, ~subst=?, ~msg=?, ~reduce=false) => { 30 30 - let gen = HOTerm.makeGen() 31 31 - let (a, _) = HOTerm.parse(at, ~scope=[], ~gen)->Result.getExn 32 32 - let (b, _) = HOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn 29 29 + let gen = RegularHOTerm.makeGen() 30 30 + let (a, _) = RegularHOTerm.parse(at, ~scope=[], ~gen)->Result.getExn 31 31 + let (b, _) = RegularHOTerm.parse(bt, ~scope=[], ~gen)->Result.getExn 33 32 try { 34 34 - let res0 = HOTerm.unifyTerm(a, b, HOTerm.emptySubst, ~gen=Some(gen))->Seq.head->Option.getExn 33 33 + let res0 = 34 34 + RegularHOTerm.unifyTerm(a, b, RegularHOTerm.emptySubst, ~gen=Some(gen)) 35 35 + ->Seq.head 36 36 + ->Option.getExn 35 37 let res = if reduce { 36 36 - HOTerm.reduceSubst(res0) 38 38 + RegularHOTerm.reduceSubst(res0) 37 39 } else { 38 40 res0 39 41 } ··· 58 60 }) 59 61 } 60 62 } catch { 61 61 - | HOTerm.UnifyFail(failed) => 63 63 + | RegularHOTerm.UnifyFail(failed) => 62 64 t->fail( 63 65 ~msg="unification failed: " ++ 64 66 TestUtil.stringifyExn(a) ++ ··· 73 75 testUnify0(t, at, bt, ~subst?, ~msg?, ~reduce) 74 76 testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce) 75 77 } 78 78 + let s = s => RegularHOTerm.Symbol({name: Symbolic.Base.wrap(s), constructor: false}) 76 79 zoraBlock("parse symbol", t => { 77 77 - t->block("single char", t => t->Util.testParse("x", Symbol({name: "x", constructor: false}))) 78 78 - t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz", constructor: false}))) 80 80 + t->block("single char", t => t->Util.testParse("x", s("x"))) 81 81 + t->block("multi char", t => t->Util.testParse("xyz", s("xyz"))) 79 82 }) 80 83 81 84 zoraBlock("parse var", t => { ··· 93 96 t->Util.testParse( 94 97 "(a b)", 95 98 App({ 96 96 - func: Symbol({name: "a", constructor: false}), 97 97 - arg: Symbol({name: "b", constructor: false}), 99 99 + func: s("a"), 100 100 + arg: s("b"), 98 101 }), 99 102 ) 100 103 }) ··· 103 106 "(a b c)", 104 107 App({ 105 108 func: App({ 106 106 - func: Symbol({name: "a", constructor: false}), 107 107 - arg: Symbol({name: "b", constructor: false}), 109 109 + func: s("a"), 110 110 + arg: s("b"), 108 111 }), 109 109 - arg: Symbol({name: "c", constructor: false}), 112 112 + arg: s("c"), 110 113 }), 111 114 ) 112 115 }) ··· 114 117 t->Util.testParse( 115 118 "(a \\1 ?1)", 116 119 App({ 117 117 - func: App({func: Symbol({name: "a", constructor: false}), arg: Var({idx: 1})}), 120 120 + func: App({func: s("a"), arg: Var({idx: 1})}), 118 121 arg: Schematic({schematic: 1}), 119 122 }), 120 123 ) ··· 148 151 ) 149 152 }) 150 153 t->block("constructor", t => { 151 151 - t->Util.testParse("@cons", Symbol({name: "cons", constructor: true})) 154 154 + t->Util.testParse("@cons", Symbol({name: Symbolic.Base.wrap("cons"), constructor: true})) 152 155 }) 153 156 // TODO: test if remaining strings are returned correctly 154 157 }) ··· 190 193 ) 191 194 }) 192 195 t->block("unify string atom", t => { 193 193 - let parse = input => t->StringUtil.parse(input) 196 196 + let parse = (input, ~scope=[]) => t->StringUtil.parse(input, ~scope) 194 197 let emptySubst = StringHOTerm.emptySubst 195 198 let substAdd = StringHOTerm.substAdd 196 199 t->equal( 197 200 StringHOTerm.unify(parse(`"a ?0() c"`), parse(`"a b c"`))->Seq.head, 198 201 Some(emptySubst->substAdd(0, wrapString([String("b")]))), 199 202 ) 203 203 + t->equal( 204 204 + StringHOTerm.unify(parse(`(L "$s")`, ~scope=["s"]), parse(`(L "?0(0) ?1(0)")`))->Seq.toArray, 205 205 + [ 206 206 + emptySubst->substAdd(0, wrapString([]))->substAdd(1, wrapString([Var({idx: 0})])), 207 207 + emptySubst->substAdd(0, wrapString([Var({idx: 0})]))->substAdd(1, wrapString([])), 208 208 + ], 209 209 + ) 200 210 t->equal( 201 211 StringHOTerm.unify(parse(`(P "?1() a" "?1()")`), parse(`(P "a ?1()" "a")`))->Seq.head, 202 212 Some(emptySubst->substAdd(1, wrapString([String("a")]))), ··· 215 225 216 226 zoraBlock("unify test", t => { 217 227 let testUnifyFail = Util.testUnifyFailString 228 228 + open RegularHOTerm 218 229 t->block("symbols", t => { 219 230 let x = "x" 220 231 let y = "y" ··· 233 244 t->block("flex-rigid", t => { 234 245 let x = "?0" 235 246 let y = "y" 236 236 - t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false}))) 247 247 + t->testUnify(x, y, ~subst=RegularHOTerm.emptySubst->RegularHOTerm.substAdd(0, s("y"))) 237 248 }) 238 249 t->block("flex-rigid2", t => { 239 250 let x = "(x. ?0 x)" ··· 247 258 0, 248 259 Lam({ 249 260 name: "x", 250 250 - body: App({func: Symbol({name: "y", constructor: false}), arg: Var({idx: 0})}), 261 261 + body: App({func: s("y"), arg: Var({idx: 0})}), 251 262 }), 252 263 ), 253 264 ) 254 254 - t->testUnify( 255 255 - x, 256 256 - y, 257 257 - ~reduce=true, 258 258 - ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})), 259 259 - ) 265 265 + t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, s("y"))) 260 266 }) 261 267 t->block("flex-rigid3", t => { 262 268 let x = "(?0 \\10)" 263 269 let y = "(fst \\10)" 264 264 - t->testUnify( 265 265 - x, 266 266 - y, 267 267 - ~reduce=true, 268 268 - ~subst=emptySubst->substAdd(0, Symbol({name: "fst", constructor: false})), 269 269 - ) 270 270 + t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, s("fst"))) 270 271 }) 271 272 t->block("flex-rigid", t => { 272 273 let x = "(?0 \\10)" ··· 279 280 Lam({ 280 281 name: "x", 281 282 body: App({ 282 282 - func: Symbol({name: "r", constructor: false}), 283 283 - arg: App({func: Symbol({name: "fst", constructor: false}), arg: Var({idx: 0})}), 283 283 + func: s("r"), 284 284 + arg: App({func: s("fst"), arg: Var({idx: 0})}), 284 285 }), 285 286 }), 286 287 ), ··· 294 295 y, 295 296 ~subst=emptySubst->substAdd( 296 297 0, 297 297 - HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->Pair.first, 298 298 + RegularHOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->Pair.first, 298 299 ), 299 300 ) 300 301 }) ··· 306 307 y, 307 308 ~subst=emptySubst->substAdd( 308 309 1, 309 309 - HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->Pair.first, 310 310 + RegularHOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->Pair.first, 310 311 ), 311 312 ) 312 313 }) ··· 318 319 y, 319 320 ~subst=emptySubst->substAdd( 320 321 1, 321 321 - HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->Pair.first, 322 322 + RegularHOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->Pair.first, 322 323 ), 323 324 ) 324 325 }) ··· 357 358 t->testUnifyFail(a, b) 358 359 }) 359 360 t->block("eta", t => { 360 360 - t->testUnify( 361 361 - "(x. ?0 x)", 362 362 - "a", 363 363 - ~reduce=true, 364 364 - ~subst=emptySubst->substAdd(0, Symbol({name: "a", constructor: false})), 365 365 - ) 361 361 + t->testUnify("(x. ?0 x)", "a", ~reduce=true, ~subst=emptySubst->substAdd(0, s("a"))) 366 362 }) 367 363 t->block("divergent", _t => { 368 364 let _divergent = "((x. x x) (x. x x))"

+2 -2

tests/TestUtil.res

reviewed

··· 205 205 | Error(msg) => t->fail(~msg="parse failed: " ++ msg) 206 206 } 207 207 } 208 208 - let parse = (t: Zora.t, input: string): Term.t => { 209 209 - let res = Term.parse(input, ~scope=[], ~gen=Term.makeGen()) 208 208 + let parse = (t: Zora.t, input: string, ~scope=[]): Term.t => { 209 209 + let res = Term.parse(input, ~scope, ~gen=Term.makeGen()) 210 210 switch res { 211 211 | Ok((term, "")) => term 212 212 | Ok((_, rest)) => {