diff --git a/src/Parser.res b/src/Parser.res index a82b167..de2e0b6 100644 --- a/src/Parser.res +++ b/src/Parser.res @@ -21,11 +21,11 @@ let runParser = (p: t<'a>, str: string): result<('a, string), err> => { )) } -let map = (p: t<'a>, f: 'a => 'b): t<'b> => (str, state) => - p(str, state)->Result.map(((res, state)) => (f(res), state)) +let map = (p: t<'a>, f: 'a => 'b): t<'b> => + (str, state) => p(str, state)->Result.map(((res, state)) => (f(res), state)) let pure = (a): t<'a> => (_, state) => Ok((a, state)) -let bind = (p1: t<'a>, p2: 'a => t<'b>): t<'b> => (str, state) => - p1(str, state)->Result.flatMap(((res, state)) => p2(res)(str, state)) +let bind = (p1: t<'a>, p2: 'a => t<'b>): t<'b> => + (str, state) => p1(str, state)->Result.flatMap(((res, state)) => p2(res)(str, state)) let apply = (p: t<'a>, pf: t<'a => 'b>): t<'b> => p->bind(a => pf->map(f => f(a))) let then = (p1: t<'a>, p2: t<'b>): t<'b> => p1->bind(_ => p2) let thenIgnore = (p1: t<'a>, p2: t<'b>): t<'a> => p1->bind(res => p2->map(_ => res)) @@ -33,17 +33,19 @@ let thenIgnore = (p1: t<'a>, p2: t<'b>): t<'a> => p1->bind(res => p2->map(_ => r let fail = (info): t<'a> => (_, state) => Error({message: info, pos: state.pos}) let void = (p: t<'a>): t => p->map(_ => ()) // backtracks by default -let optional = (p: t<'a>): t> => (str, state) => { - switch p(str, state) { - | Ok((res, state)) => Ok((Some(res), state)) - | Error(_) => Ok((None, state)) - } -} -let or = (p1: t<'a>, p2: t<'a>): t<'a> => (str, state) => - switch p1(str, state) { - | Ok(r) => Ok(r) - | Error(_) => p2(str, state) +let optional = (p: t<'a>): t> => + (str, state) => { + switch p(str, state) { + | Ok((res, state)) => Ok((Some(res), state)) + | Error(_) => Ok((None, state)) + } } +let or = (p1: t<'a>, p2: t<'a>): t<'a> => + (str, state) => + switch p1(str, state) { + | Ok(r) => Ok(r) + | Error(_) => p2(str, state) + } let choice = (ps: array>): t<'a> => { ps->Array.reduce(fail("no matches"), or) } @@ -142,10 +144,11 @@ let regex1 = (re: RegExp.t): t => } ) -let peek = (n): t => (str, state) => { - let res = str->String.slice(~start=state.pos.idx, ~end=state.pos.idx + n) - Ok((res, state)) -} +let peek = (n): t => + (str, state) => { + let res = str->String.slice(~start=state.pos.idx, ~end=state.pos.idx + n) + Ok((res, state)) + } type length = int let takeWhileMany = (f: string => option) => @@ -167,7 +170,7 @@ let takeWhile = (f: string => bool) => } ) -let dbg = (p: t<'a>, ~label): t<'a> => { +let dbg = (p: t<'a>, label): t<'a> => { let dbgInfo = title => getCurrentStr->bind(str => getState->map(state => { @@ -184,8 +187,24 @@ let dbg = (p: t<'a>, ~label): t<'a> => { }) } -let lexeme = p => p->thenIgnore(regex(%re(`/^\s*/`))->void) +let lexeme = p => p->thenIgnore(regex(/^\s*/)->void) let token = s => string(s)->lexeme -let decimal = regex1(%re(`/(\d+)/`))->map(xStr => xStr->Int.fromString->Option.getExn) -let whitespace = regex(%re(`/\s*/`))->void +let decimal = regex1(/(\d+)/)->map(xStr => xStr->Int.fromString->Option.getExn) +let whitespace = regex(/\s*/)->void + +let lift = (f: string => result<('a, string), string>): t<'a> => + getCurrentStr->bind(str => + switch f(str) { + | Ok((res, remaining)) => { + let length = String.length(str) - String.length(remaining) + consume(length)->map(_ => res) + } + | Error(msg) => fail(msg) + } + ) +let liftParse = ( + f: (string, ~scope: array<'m>, ~gen: 'g=?) => result<('a, string), string>, + ~scope: array<'m>, + ~gen: option<'g>=?, +): t<'a> => lift(s => f(s, ~scope, ~gen?)) diff --git a/src/SExp.res b/src/SExp.res index 836f6b5..e1a4138 100644 --- a/src/SExp.res +++ b/src/SExp.res @@ -250,10 +250,6 @@ module Make = (Atom: AtomDef.COERCIBLE_ATOM): { let prettyPrintSubst = (sub, ~scope) => Util.prettyPrintMap(sub, ~showV=t => prettyPrint(t, ~scope)) - let symbolRegexpString = `^([^\\s()\\[\\]]+)` - let varRegexpString = "^\\\\([0-9]+)$" - let schematicRegexpString = "^\\?([0-9]+)$" - type lexeme = LParen | RParen | VarT(int) | AtomT(Atom.t) | SchematicT(int) let nameRES = "^([^\\s.\\[\\]()]+)\\." let prettyPrintMeta = (str: string) => { String.concat(str, ".") @@ -269,149 +265,49 @@ module Make = (Atom: AtomDef.COERCIBLE_ATOM): { } } } - let parse = (str: string, ~scope: array, ~gen=?) => { - let cur = ref(String.make(str)) - let lex: unit => option = () => { - let str = String.trim(cur.contents) - cur := str - let checkVariable = (candidate: string) => { - let varRegexp = RegExp.fromString(varRegexpString) - switch Array.indexOf(scope, candidate) { - | -1 => - switch varRegexp->RegExp.exec(candidate) { - | Some(res') => - switch RegExp.Result.matches(res') { - | [idx] => Some(idx->Int.fromString->Option.getUnsafe) - | _ => None - } - | None => None - } - | idx => Some(idx) - } - } - if String.get(str, 0) == Some("(") { - cur := String.sliceToEnd(str, ~start=1) - Some(LParen) - } else if String.get(str, 0) == Some(")") { - cur := String.sliceToEnd(str, ~start=1) - Some(RParen) - } else { - let symbolRegexp = RegExp.fromStringWithFlags(symbolRegexpString, ~flags="y") - switch symbolRegexp->RegExp.exec(str) { - | None => None - | Some(res) => - switch RegExp.Result.matches(res) { - | [symb] => { - let specialSymb = tok => { - cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp)) - Some(tok) - } - let regularSymb = () => { - // FIX: not ideal to throw away symbol error message - Console.log(("current", cur.contents)) - Atom.parse(cur.contents, ~scope) - ->Util.Result.ok - ->Option.map(((s, rest)) => { - cur := rest - Console.log(("parsed", s, cur.contents)) - AtomT(s) - }) - } - switch checkVariable(symb) { - | Some(idx) => specialSymb(VarT(idx)) - | None => { - let schematicRegexp = RegExp.fromString(schematicRegexpString) - switch schematicRegexp->RegExp.exec(symb) { - | None => regularSymb() - | Some(res') => - switch RegExp.Result.matches(res') { - | [s] => specialSymb(SchematicT(s->Int.fromString->Option.getUnsafe)) - | _ => regularSymb() - } - } - } - } - } - | _ => None + let mkParser = (~scope: array, ~gen=?): Parser.t => { + open Parser + let varLit = string("\\")->then(decimal) + let ident = regex1(/([^\s\(\)]+)/) + let varIdx = + varLit + ->or( + ident->bind(id => + switch scope->Array.indexOfOpt(id) { + | Some(idx) => pure(idx) + | None => fail("expected variable") } - } - } - } + ), + ) + ->lexeme + let var = varIdx->map(idx => Var({idx: idx})) - let peek = () => { - // a bit slow, better would be to keep a backlog of lexed tokens.. - let str = String.make(cur.contents) - let tok = lex() - cur := str - tok - } - exception ParseError(string) - let rec parseExp = () => { - let tok = peek() - switch tok { - | Some(AtomT(s)) => { - let _ = lex() - Some(Atom(s)) - } - | Some(VarT(idx)) => { - let _ = lex() - Some(Var({idx: idx})) - } - | Some(SchematicT(num)) => { - let _ = lex() - switch lex() { - | Some(LParen) => { - let it = ref(None) - let bits = [] - let getVar = (t: option) => - switch t { - | Some(VarT(idx)) => Some(idx) - | _ => None - } - while { - it := lex() - it.contents->getVar->Option.isSome - } { - Array.push(bits, it.contents->getVar->Option.getUnsafe) - } - switch it.contents { - | Some(RParen) => - switch gen { - | Some(g) => { - seen(g, num) - Some(Schematic({schematic: num, allowed: bits})) - } - | None => throw(ParseError("Schematics not allowed here")) - } - | _ => throw(ParseError("Expected closing parenthesis")) - } - } - | _ => throw(ParseError("Expected opening parenthesis")) - } - } - | Some(LParen) => { - let _ = lex() - let bits = [] - let it = ref(None) - while { - it := parseExp() - it.contents->Option.isSome - } { - Array.push(bits, it.contents->Option.getUnsafe) - } - switch lex() { - | Some(RParen) => Some(Compound({subexps: bits})) - | _ => throw(ParseError("Expected closing parenthesis")) - } - } - | _ => None - } - } - switch parseExp() { - | exception ParseError(s) => Error(s) - | None => Error("No expression to parse") - | Some(e) => Ok((e, cur.contents)) - } + let schemaLit = + string("?") + ->then(decimal) + ->bind(schematic => + many(varIdx) + ->between(token("("), token(")")) + ->map(allowed => { + gen->Option.map(g => allowed->Array.forEach(n => seen(g, n)))->ignore + Schematic({schematic, allowed}) + }) + ) + let inner = fix(f => + choice([ + schemaLit, + var, + liftParse(Atom.parse, ~scope, ~gen?)->map(a => Atom(a)), + many(f) + ->between(token("("), token(")")) + ->map(subexps => Compound({subexps: subexps})), + ])->lexeme + ) + whitespace->then(inner) + } + + let parse = (str: string, ~scope: array, ~gen=?) => { + Parser.runParser(mkParser(~scope, ~gen?), str)->Result.mapError(e => e.message) } let rec concrete = t => diff --git a/src/StringA.res b/src/StringA.res index 654a50f..85604d3 100644 --- a/src/StringA.res +++ b/src/StringA.res @@ -479,11 +479,11 @@ module AtomView = { } let parenthesise = f => - [ - {React.string("(")} , - ...f, - {React.string(")")} , - ] + Array.flat([ + [ {React.string("(")} ], + f, + [ {React.string(")")} ], + ]) let intersperse = a => Util.intersperse(a, ~with=React.string(" ")) diff --git a/tests/RuleTest.res b/tests/RuleTest.res index 9b9d23e..7ca2e56 100644 --- a/tests/RuleTest.res +++ b/tests/RuleTest.res @@ -31,26 +31,39 @@ module MakeTest = (Term: TERM, Judgment: JUDGMENT with module Term := Term) => { } } -// zoraBlock("string terms", t => { -// module T = MakeTest(StringSExp, StringSExpJ) -// t->T.testParseInner( -// `[s1. ("$s1" p) |- ("($s1)" p)]`, -// { -// vars: ["s1"], -// premises: [ -// { -// vars: [], -// premises: [], -// conclusion: StringSExp.Compound( -// [StringA.Atom.Var({idx: 0})], -// SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom, -// ), -// }, -// ], -// conclusion: ( -// [StringA.Atom.String("("), StringA.Atom.Var({idx: 0}), StringA.Atom.String(")")], -// SExp.pAtom("p")->StringA.AtomJudgment.ConstS->StringSymbolic.Atom, -// ), -// }, -// ) -// }) +zoraBlock("string terms", t => { + module StringSymbol = AtomDef.MakeAtomAndView( + Coercible.StringA, + StringA.AtomView, + Coercible.Symbolic, + Symbolic.AtomView, + ) + module StringSExp = SExp.Make(StringSymbol.Atom) + module T = MakeTest(StringSExp, StringSExp) + t->T.testParseInner( + `[s1. ("$s1" p) |- ("($s1)" p)]`, + { + vars: ["s1"], + premises: [ + { + vars: [], + premises: [], + conclusion: StringSExp.Compound({ + subexps: [ + [StringA.Var({idx: 0})]->StringSymbol.Atom.Left->StringSExp.Atom, + "p"->StringSymbol.Atom.Right->StringSExp.Atom, + ], + }), + }, + ], + conclusion: StringSExp.Compound({ + subexps: [ + [StringA.String("("), StringA.Var({idx: 0}), StringA.String(")")] + ->StringSymbol.Atom.Left + ->StringSExp.Atom, + "p"->StringSymbol.Atom.Right->StringSExp.Atom, + ], + }), + }, + ) +})