···4444 let upshift: (t, int, ~from: int=?) => t
4545 let upshiftSubstCodom: (substCodom, int, ~from: int=?) => substCodom
4646 let placeSubstCodom: (schematic, ~scope: array<meta>) => substCodom
4747+ // Map a function over all terms in the judgment
4848+ let mapTerms: (t, Term.t => Term.t) => t
4749 let parse: (string, ~scope: array<Term.meta>, ~gen: Term.gen=?) => result<(t, string), string>
4850 let parseSubstCodom: (
4951 string,
···4040 }
4141 )
4242let maxSchematicCount = (term: t) => {
4343- schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(snd)->Option.getOr(0)
4343+ schematicsCountsIn(term)->Belt.Map.Int.maximum->Option.map(Pair.second)->Option.getOr(0)
4444}
4545let reduce = t => t
4646let freeVarsIn = (term: t): Belt.Set.t<int, IntCmp.identity> =>
···350350}
351351352352let parseMeta = (str: string) => {
353353- let re = %re("/^([^\s.\[\]()]+)\./y")
353353+ let re = /^([^\s.\[\]()]+)\./y
354354 switch re->RegExp.exec(str->String.trim) {
355355 | None => Error("not a meta name")
356356 | Some(res) =>
···416416 let execRe = re => execRe(re, String.sliceToEnd(str, ~start=pos.contents))
417417 let stringLit = () => {
418418 let identRegex = RegExp.fromString(`^${Util.identRegexStr}`)
419419- let symbolRegex = %re(`/^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/`)
420420- let numberRegex = %re(`/^(\d+)/`)
419419+ let symbolRegex = /^([!@#\$%\^~&*_+\-={};':|,.<>\/?]+)/
420420+ let numberRegex = /^(\d+)/
421421 switch execRe(identRegex)
422422 ->Option.orElse(execRe(symbolRegex))
423423 ->Option.orElse(execRe(numberRegex)) {
···427427 }
428428 }
429429 let escaped = () => {
430430- let escapedRegex = %re(`/\\([\$\?\\\"])/`)
430430+ let escapedRegex = /\\([\$\?\\\"])/
431431 switch execRe(escapedRegex) {
432432 | Some([char], l) => add(String(char), ~nAdvance=l)
433433 | Some(_) => error("regex escaped error")
···436436 }
437437 let readInt = s => Int.fromString(s)->Option.getExn
438438 let schema = () => {
439439- let schemaRegex = %re("/\?(\d+)\(((?:\d+\s*)*)\)/")
439439+ let schemaRegex = /\?(\d+)\(((?:\d+\s*)*)\)/
440440 switch execRe(schemaRegex) {
441441 | Some([idStr, allowedStr], l) => {
442442 let schematic = readInt(idStr)
443443 let allowed =
444444 allowedStr
445445 ->String.trim
446446- ->String.splitByRegExp(%re("/\s+/"))
446446+ ->String.splitByRegExp(/\s+/)
447447 ->Array.keepSome
448448 ->Array.filter(s => s != "")
449449 ->Array.map(readInt)
···454454 }
455455 }
456456 let var = () => {
457457- let varLitRegex = %re("/^\$\\(\d+)/")
458458- let varScopeRegex = %re("/^\$([a-zA-Z]\w*)/")
457457+ let varLitRegex = /^\$\\(\d+)/
458458+ let varScopeRegex = /^\$([a-zA-Z]\w*)/
459459 switch execRe(varLitRegex) {
460460 | Some([match], l) => add(Var({idx: readInt(match)}), ~nAdvance=l)
461461 | Some(_) => error("var lit regex error")
···473473 }
474474475475 // consume leading whitespace + open quote
476476- switch execRe(%re(`/^\s*"/`)) {
476476+ switch execRe(/^\s*"/) {
477477 | Some(_, l) => pos := l
478478 | None => error("expected open quote")
479479 }
+7
src/StringTermJudgment.res
···7676 | SExpV(j) => SExpV(SExp.upshift(j, amount, ~from))
7777 }
78787979+let mapTerms = ((t, j): t, f: StringTerm.t => StringTerm.t): t => {
8080+ // Apply the function to both the string term and the sexp (converted to/from string term)
8181+ let newT = f(t)
8282+ let newJ = j->StringTerm.fromSExp->f->StringTerm.toSExp
8383+ (newT, newJ)
8484+}
8585+7986let parse = (str: string, ~scope: array<StringTerm.meta>, ~gen=?) => {
8087 StringTerm.parse(str, ~scope, ~gen?)->Result.flatMap(((t, str)) =>
8188 SExp.parse(str, ~scope)->Result.map(((j, str)) => ((t, j), str))
+4-1
src/TermAsJudgment.res
···11open Signatures
2233-module Make = (Term: TERM): (JUDGMENT with module Term := Term and type t = Term.t) => {
33+module Make = (Term: TERM): (
44+ JUDGMENT with module Term := Term and type t = Term.t and type subst = Term.subst
55+) => {
46 include Term
57 type substCodom = Term.t
68 let prettyPrintSubstCodom = Term.prettyPrint
···810 let placeSubstCodom = Term.place
911 let upshiftSubstCodom = Term.upshift
1012 let substituteSubstCodom = Term.substitute
1313+ let mapTerms = (t: Term.t, f: Term.t => Term.t): Term.t => f(t)
1114}
12151316module SExpJ = Make(SExp)
+1-1
src/Util.res
···113113exception Err(string)
114114let mustFindIndex = (arr, f) => {
115115 switch Array.findIndex(arr, f) {
116116- | -1 => raise(Unreachable("Element not found"))
116116+ | -1 => throw(Unreachable("Element not found"))
117117 | i => i
118118 }
119119}
+53-22
tests/HOTermTest.res
···5151 testUnify0(t, bt, at, ~subst?, ~msg?, ~reduce)
5252}
5353zoraBlock("parse symbol", t => {
5454- t->block("single char", t => t->Util.testParse("x", Symbol({name: "x"})))
5555- t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz"})))
5454+ t->block("single char", t => t->Util.testParse("x", Symbol({name: "x", constructor: false})))
5555+ t->block("multi char", t => t->Util.testParse("xyz", Symbol({name: "xyz", constructor: false})))
5656})
57575858zoraBlock("parse var", t => {
···66666767zoraBlock("parse application", t => {
6868 t->block("multiple", t => {
6969- t->Util.testParse("(a b)", App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})}))
6969+ t->Util.testParse(
7070+ "(a b)",
7171+ App({
7272+ func: Symbol({name: "a", constructor: false}),
7373+ arg: Symbol({name: "b", constructor: false}),
7474+ }),
7575+ )
7076 })
7177 t->block("multiple more", t => {
7278 t->Util.testParse(
7379 "(a b c)",
7480 App({
7575- func: App({func: Symbol({name: "a"}), arg: Symbol({name: "b"})}),
7676- arg: Symbol({name: "c"}),
8181+ func: App({
8282+ func: Symbol({name: "a", constructor: false}),
8383+ arg: Symbol({name: "b", constructor: false}),
8484+ }),
8585+ arg: Symbol({name: "c", constructor: false}),
7786 }),
7887 )
7988 })
···8190 t->Util.testParse(
8291 "(a \\1 ?1)",
8392 App({
8484- func: App({func: Symbol({name: "a"}), arg: Var({idx: 1})}),
9393+ func: App({func: Symbol({name: "a", constructor: false}), arg: Var({idx: 1})}),
8594 arg: Schematic({schematic: 1}),
8695 }),
8796 )
···113122 "x. (x x)",
114123 Lam({name: "x", body: App({func: Var({idx: 0}), arg: Var({idx: 0})})}),
115124 )
125125+ })
126126+ t->block("constructor", t => {
127127+ t->Util.testParse("@cons", Symbol({name: "cons", constructor: true}))
116128 })
117129 // TODO: test if remaining strings are returned correctly
118130})
···121133 t->block("examples", t => {
122134 t->Util.testParsePrettyPrint("\\1", "\\1")
123135 t->Util.testParsePrettyPrint("?1", "?1")
136136+ t->Util.testParsePrettyPrint("@cons", "@cons")
124137 t->Util.testParsePrettyPrint("(x. x)", "(x. x)")
125138 t->Util.testParsePrettyPrint("(x. x. \\0)", "(x. x. x)")
126139 t->Util.testParsePrettyPrint("(x. x. \\1)", "(x. x. \\1)")
···150163 t->block("flex-rigid", t => {
151164 let x = "?0"
152165 let y = "y"
153153- t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y"})))
166166+ t->testUnify(x, y, ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})))
154167 })
155168 t->block("flex-rigid2", t => {
156169 let x = "(x. ?0 x)"
···162175 ~reduce=false,
163176 ~subst=emptySubst->substAdd(
164177 0,
165165- Lam({name: "x", body: App({func: Symbol({name: "y"}), arg: Var({idx: 0})})}),
178178+ Lam({
179179+ name: "x",
180180+ body: App({func: Symbol({name: "y", constructor: false}), arg: Var({idx: 0})}),
181181+ }),
166182 ),
167183 )
168168- t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "y"})))
184184+ t->testUnify(
185185+ x,
186186+ y,
187187+ ~reduce=true,
188188+ ~subst=emptySubst->substAdd(0, Symbol({name: "y", constructor: false})),
189189+ )
169190 })
170191 t->block("flex-rigid3", t => {
171192 let x = "(?0 \\10)"
172193 let y = "(fst \\10)"
173173- t->testUnify(x, y, ~reduce=true, ~subst=emptySubst->substAdd(0, Symbol({name: "fst"})))
194194+ t->testUnify(
195195+ x,
196196+ y,
197197+ ~reduce=true,
198198+ ~subst=emptySubst->substAdd(0, Symbol({name: "fst", constructor: false})),
199199+ )
174200 })
175201 t->block("flex-rigid", t => {
176202 let x = "(?0 \\10)"
···183209 Lam({
184210 name: "x",
185211 body: App({
186186- func: Symbol({name: "r"}),
187187- arg: App({func: Symbol({name: "fst"}), arg: Var({idx: 0})}),
212212+ func: Symbol({name: "r", constructor: false}),
213213+ arg: App({func: Symbol({name: "fst", constructor: false}), arg: Var({idx: 0})}),
188214 }),
189215 }),
190216 ),
···198224 y,
199225 ~subst=emptySubst->substAdd(
200226 0,
201201- HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->fst,
227227+ HOTerm.parse("(x. (r (fst x)))", ~scope=[])->Result.getExn->Pair.first,
202228 ),
203229 )
204230 })
···210236 y,
211237 ~subst=emptySubst->substAdd(
212238 1,
213213- HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->fst,
239239+ HOTerm.parse("(x. x. (r (q \\0 \\1)))", ~scope=[])->Result.getExn->Pair.first,
214240 ),
215241 )
216242 })
···222248 y,
223249 ~subst=emptySubst->substAdd(
224250 1,
225225- HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->fst,
251251+ HOTerm.parse("(x. x. (r (q (snd \\0) \\1)))", ~scope=[])->Result.getExn->Pair.first,
226252 ),
227253 )
228254 })
···265291 "(x. ?0 x)",
266292 "a",
267293 ~reduce=true,
268268- ~subst=emptySubst->substAdd(0, Symbol({name: "a"})),
294294+ ~subst=emptySubst->substAdd(0, Symbol({name: "a", constructor: false})),
269295 )
270296 })
271271- t->block("divergent", t => {
272272- let divergent = "((x. x x) (x. x x))"
273273- let a = "((x. ?0 x) (x. x x))"
297297+ t->block("divergent", _t => {
298298+ let _divergent = "((x. x x) (x. x x))"
299299+ let _a = "((x. ?0 x) (x. x x))"
274300 // we don't care
275301 // t->Util.testNotUnify(a, divergent)
276302 })
···278304 let a = "(?0 \\0 \\0)"
279305 let b = "\\0"
280306 t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. \\0)")))
307307+ })
308308+ t->block("dup var 2", t => {
309309+ let a = "(k. ?0 k k)"
310310+ let b = "(k. G k)"
311311+ t->testUnify(a, b, ~subst=emptySubst->substAdd(0, t->Util.parse("(x. x. G x)")))
281312 })
282313 // Yokoyama et al.'s example in A Functional Implementation of Function-as-Constructor Higher-Order Unification Makoto Hamana1
283314 t->block("break global resctriction", t => {
···312343 t->Util.testUnifyFail(a, b)
313344 t->testUnify(c, b, ~subst=emptySubst->substAdd(6, t->Util.parse("(x. S \\0)")))
314345 })
315315- t->block("tests from induction examples", t => {
316316- let r = ("((?0 \\0) (?1 \\0))")
317317- let g = ("(f \\0)")
346346+ t->block("tests from induction examples", _t => {
347347+ let _r = "((?0 \\0) (?1 \\0))"
348348+ let _g = "(f \\0)"
318349 // what it's currently doing:
319350 // 0 := (x. y. f x)
320351 // 1 := doesn't matter