initial associative-commutative atom definition #1

+57 -39

index.html

reviewed

··· 47 47 --bound-col: #9343a7; 48 48 --placeholder-fg-col: #aaa; 49 49 --symbol-col: #990000; 50 50 + --symbol-nat-col: #ffaa00; 50 51 --item-inserting-col: #aa00cc; 51 52 --sidebar-header-col: #c9c9d8; 52 53 --error-bg-col: #ffaaaa; ··· 244 245 .symbol { 245 246 color: var(--symbol-col); 246 247 } 248 248 + .symbol-nat { 249 249 + color: var(--symbol-nat-col) 250 250 + } 247 251 .symbol-turnstile { 248 252 padding-left: 6px; 249 253 padding-right: 6px; ··· 597 601 s. 0 1 |- elim (M-Surround 1 "$s") {}} 598 602 </hol-string-proof> 599 603 <hol-string id="index.html/string-arithmetic" deps="index.html/myconfig"> 600 600 - -------- nat-z 601 601 - (Nat Z) 602 602 - 603 603 - n. (Nat n) 604 604 - -------- nat-s 605 605 - (Nat (S n)) 606 606 - 607 607 - n1. 608 608 - -------- nat-plus-z 609 609 - (Eval (Plus n1 Z) n1) 610 610 - 611 611 - n1. n2. res. 612 612 - (Eval (Plus n1 n2) res) 613 613 - --------- nat-plus-s 614 614 - (Eval (Plus n1 (S n2)) (S res)) 615 615 - 616 616 - ------- string-zero 617 617 - (Parse "0" Z) 618 618 - 619 619 - ------- string-one 620 620 - (Parse "1" (S Z)) 621 621 - 622 622 - -------- string-two 623 623 - (Parse "2" (S (S Z))) 624 624 - 625 625 - -------- string-three 626 626 - (Parse "3" (S (S (S Z)))) 627 627 - 628 628 - s1. s2. n2. 629 629 - (Parse s2 n2) 604 604 + s. n. 630 605 --------- string-prod 631 631 - (Parse "$s1 * $s2" (Prod s1 n2)) 606 606 + (Parse "$s * $n" (Prod s nat(n))) 632 607 633 608 s1. 634 609 ---------- eval-prod-Z 635 635 - (Eval (Prod s1 Z) "") 610 610 + (Eval (Prod s1 nat(0)) "") 636 611 637 612 s1. s1n. n. 638 638 - (Eval (Prod s1 n) s1n) 613 613 + (Eval (Prod s1 nat(n)) s1n) 639 614 ----------- eval-prod-S 640 640 - (Eval (Prod s1 (S n)) "$s1$s1n") 615 615 + (Eval (Prod s1 nat(n + 1)) "$s1$s1n") 641 616 642 617 s. ast. res. 643 618 (Parse s ast) ··· 646 621 (PEval s res) 647 622 648 623 </hol-string> 649 649 - <hol-string-proof id="index.html/sexp-nat-toy" deps="index.html/myconfig index.html/string-arithmetic"> 650 650 - ----------- mexp-lexp 651 651 - (Eval (Plus (S Z) (S (S Z))) (S (S (S Z)))) 652 652 - |- ? 653 653 - </hol-string-proof> 654 624 <hol-string-proof id="index.html/string-prod-toy" deps="index.html/myconfig index.html/string-arithmetic"> 655 625 ------------- foo-3 656 626 (PEval "foo * 3" "foo foo foo") 657 627 |- ? 658 628 659 629 </hol-string-proof> 630 630 + <hol-string id="index.html/types" deps="index.html/myconfig"> 631 631 + n. (Type n Nat) 632 632 + ------------ Var 633 633 + (Var n) 634 634 + 635 635 + ------------ Sig-Empty 636 636 + (Sig Empty) 637 637 + 638 638 + f. n. sig. (Sig sig) 639 639 + ------------ Sig-Cons 640 640 + (Sig (Cons (f nat(n)) sig)) 641 641 + 642 642 + f. n. sig. 643 643 + (Sig sig) 644 644 + ------------ InSig-Head 645 645 + (InSig (f nat(n)) (Cons (f nat(n)) sig)) 646 646 + 647 647 + f. n. g. sig. 648 648 + (Sig sig) 649 649 + (InSig (f nat(n)) sig) 650 650 + ------------ InSig-Next 651 651 + (InSig (f nat(n)) (Cons g (f nat(n)))) 652 652 + 653 653 + v. sig. (Sig sig) (Var v) 654 654 + ------------ Term-Var 655 655 + (Term sig (Var v)) 656 656 + 657 657 + a. sig. (Sig sig) (InSig (a nat(0)) sig) 658 658 + ------------ Term-Const 659 659 + (Term sig (Const a)) 660 660 + 661 661 + sig. 662 662 + ------------ Term-List-0 663 663 + (TermList sig nat(0) Empty) 664 664 + 665 665 + f. n. t. ts. sig. (Term sig t) (TermList nat(n) ts) 666 666 + ------------ Term-List-n 667 667 + (TermList sig nat(n + 1) (Cons t ts)) 668 668 + 669 669 + f. n. ts. sig. (Sig sig) (InSig (f nat(n)) sig) (TermList sig nat(n) ts) 670 670 + ------------ Term-Func 671 671 + (Term sig (Func f ts)) 672 672 + </hol-string> 673 673 + <hol-string-proof id="index.html/play-sig" deps="index.html/myconfig index.html/types"> 674 674 + ------------- penips 675 675 + (Term (Cons (f nat(2)) (Cons (a nat(0)) Empty)) (Func f (Cons (Const a) (Cons (Var nat(1)) Empty)))) 676 676 + |- ? 677 677 + </hol-string-proof> 660 678 <hol-string id="index.html/string-silliness" deps="index.html/myconfig"> 661 679 a. 662 680 -------------- eq-refl

+387

src/AssocComm.res

reviewed

··· 1 1 + module type AC_ATOM = { 2 2 + module ACBase: AssocCommBase.AC_BASE_ATOM 3 3 + include AtomDef.ATOM with module Base = ACBase 4 4 + let identity: t 5 5 + let add: (t, t) => t 6 6 + } 7 7 + 8 8 + module Make = ( 9 9 + BaseAtom: AssocCommBase.AC_BASE_ATOM, 10 10 + C: { 11 11 + let coerce: AtomBase.anyValue => option<BaseAtom.t> 12 12 + }, 13 13 + ): (AC_ATOM with module ACBase = BaseAtom) => { 14 14 + module ACBase = BaseAtom 15 15 + module Base = BaseAtom 16 16 + module Const = BaseAtom.Const 17 17 + module IntMap = Belt.Map.Int 18 18 + type t = Base.t 19 19 + type subst = Map.t<int, t> 20 20 + type gen = ref<int> 21 21 + let identity = Base.identity 22 22 + let add = (a1: t, a2: t) => { 23 23 + Base.schemas: IntMap.merge(a1.schemas, a2.schemas, (_, o1, o2) => 24 24 + switch (o1, o2) { 25 25 + | (Some({allowed, count}), None) | (None, Some({allowed, count})) => 26 26 + Some({Base.allowed, count}) 27 27 + | (Some({allowed, count: count1}), Some({count: count2})) => 28 28 + Some({allowed, count: count1 + count2}) 29 29 + | (None, None) => throw(Util.Unreachable("belt map error")) 30 30 + } 31 31 + ), 32 32 + vars: IntMap.merge(a1.vars, a2.vars, (_, o1, o2) => 33 33 + switch (o1, o2) { 34 34 + | (Some(count), None) | (None, Some(count)) => Some(count) 35 35 + | (Some(count1), Some(count2)) => Some(count1 + count2) 36 36 + | (None, None) => throw(Util.Unreachable("belt map error")) 37 37 + } 38 38 + ), 39 39 + const: a1.const + a2.const, 40 40 + } 41 41 + let multiply = (a: t, n: int) => { 42 42 + Base.schemas: a.schemas->IntMap.map(({allowed, count}) => {Base.allowed, count: count * n}), 43 43 + vars: a.vars->IntMap.map(count => count * n), 44 44 + const: a.const * n, 45 45 + } 46 46 + let singletonSubst: (int, t) => subst = (schematic, term) => { 47 47 + let subst = Map.make() 48 48 + subst->Map.set(schematic, term) 49 49 + subst 50 50 + } 51 51 + let prettyPrint = (t: t, ~scope: array<string>) => { 52 52 + open Const 53 53 + let opString = ` ${opString} ` 54 54 + let schemas = switch t.schemas->IntMap.size { 55 55 + | 0 => None 56 56 + | _ => 57 57 + t.schemas 58 58 + ->IntMap.toArray 59 59 + ->Array.map(((schematic, {allowed, count})) => 60 60 + Util.prettyPrintSchematic(schematic, allowed, scope)->formatMultiple(count) 61 61 + ) 62 62 + ->Array.join(opString) 63 63 + ->Some 64 64 + } 65 65 + 66 66 + let vars = switch t.vars->IntMap.size { 67 67 + | 0 => None 68 68 + | _ => 69 69 + t.vars 70 70 + ->IntMap.toArray 71 71 + ->Array.map(((idx, count)) => Util.prettyPrintVar(idx, scope)->formatMultiple(count)) 72 72 + ->Array.join(opString) 73 73 + ->Some 74 74 + } 75 75 + let const = switch t.const { 76 76 + | 0 => None 77 77 + | _ => t.const->formatMultipleConst->Some 78 78 + } 79 79 + let inner = [schemas, vars, const]->Array.keepSome->Array.join(opString) 80 80 + `${openTerm} ${inner} ${closeTerm}` 81 81 + } 82 82 + // {0, 1, ..., n - 1}^m 83 83 + let latticePoints = (n: int, m: int): Seq.t<array<int>> => 84 84 + Seq.init(n ** m, i => { 85 85 + let vec = [] 86 86 + let x = ref(i) 87 87 + for _ in 0 to m - 1 { 88 88 + vec->Array.push(x.contents % n) 89 89 + x := x.contents / n 90 90 + } 91 91 + vec 92 92 + }) 93 93 + let compWiseGt = (v1: array<int>, v2: array<int>): bool => 94 94 + Belt.Array.zip(v1, v2)->Array.every(((x, y)) => x > y) 95 95 + let dot = (v1: array<int>, v2: array<int>): int => 96 96 + Belt.Array.zipBy(v1, v2, (a, b) => a * b)->Array.reduce(0, (a, b) => a + b) 97 97 + let unify = (a: t, b: t, ~gen as _=?) => { 98 98 + let solveNaive = (a: t, b: t) => { 99 99 + let schema = a.schemas->IntMap.minKey->Option.getExn 100 100 + Base.Const.opInv(b.const, a.const) 101 101 + ->Option.map(n => Seq.once(singletonSubst(schema, Base.const(n)))) 102 102 + ->Option.getOr(Seq.empty) 103 103 + } 104 104 + let isNaiveCase = (a: t, b: t): bool => { 105 105 + a.schemas->IntMap.size == 1 && 106 106 + b.schemas->IntMap.size == 0 && 107 107 + a.vars->IntMap.size == 0 && 108 108 + b.vars->IntMap.size == 0 && 109 109 + (a.schemas->IntMap.get(a.schemas->IntMap.minKey->Option.getExn)->Option.getExn).count == 1 110 110 + } 111 111 + 112 112 + // steps in elementary algorithm 113 113 + // 1. gen schema vector `schemas` by lhs - rhs. this has length n 114 114 + // 2. test all vectors in {0, 1, ..., max(schemas) + 1}^n for eq to 0 115 115 + // vectors that match should be filtered as we go for being (component-wise) minimal 116 116 + // 3. reconstruct sub: for each v_i from previous step, 117 117 + // schema_i |-> sum(v_j[i] * schema_j for j in 0..n) 118 118 + // 119 119 + // we /should/ be able to extend this to elemtary w/ constants 120 120 + // bc that just requires an inhomogeneous eqn solver, but i'm nto so 121 121 + // sure about the vectors above giving a minimal compelte set of sols 122 122 + let homogeneousSolve = () => { 123 123 + let eqnLhs = a.schemas->IntMap.merge(b.schemas, (_, o1, o2) => { 124 124 + switch (o1, o2) { 125 125 + | (Some({allowed, count}), None) => Some({Base.allowed, count}) 126 126 + | (None, Some({allowed, count})) => Some({Base.allowed, count: -count}) 127 127 + | (Some({allowed, count: count1}), Some({count: count2})) => 128 128 + Some({allowed, count: count1 - count2}) 129 129 + | (None, None) => throw(Util.Unreachable("belt map error")) 130 130 + } 131 131 + }) 132 132 + let eqnEntries = eqnLhs->IntMap.toArray 133 133 + let counts = eqnEntries->Array.map(((_, entry)) => entry.count) 134 134 + let maxCount = counts->Array.reduce(0, (curMax, next) => max(curMax, abs(next))) 135 135 + let minimalSols = [] 136 136 + let addIfMinimal = (sols: array<array<int>>, candidate) => 137 137 + if sols->Array.every(sol => !(candidate->compWiseGt(sol))) { 138 138 + sols->Array.push(candidate) 139 139 + } 140 140 + latticePoints(maxCount + 1, eqnEntries->Array.length) 141 141 + // skip [0, ..., 0] (trivial solution to homogeneous eqn) 142 142 + ->Seq.tail 143 143 + ->Seq.forEach(vec => { 144 144 + if dot(vec, counts) == 0 { 145 145 + minimalSols->addIfMinimal(vec) 146 146 + } 147 147 + }) 148 148 + let solutionToSubst = (sol: array<int>, target: t): Map.t<int, t> => { 149 149 + eqnEntries 150 150 + ->Belt.Array.zipBy(sol, ((schematic, _), count) => 151 151 + if count > 0 { 152 152 + Some((schematic, multiply(target, count))) 153 153 + } else { 154 154 + None 155 155 + } 156 156 + ) 157 157 + ->Array.keepSome 158 158 + ->Map.fromArray 159 159 + } 160 160 + let res = 161 161 + minimalSols 162 162 + ->Belt.Array.mapWithIndex((i, sol) => { 163 163 + let target = switch Belt.Array.get(eqnEntries, i) { 164 164 + | Some((schematic, {allowed})) => Base.schematic(schematic, allowed) 165 165 + | None => identity 166 166 + } 167 167 + solutionToSubst(sol, target) 168 168 + }) 169 169 + ->Array.reduce(Map.make(), (sig1, sig2) => Util.mapUnionWith(sig1, sig2, add)) 170 170 + res->Seq.once 171 171 + } 172 172 + if a.schemas->IntMap.size == 0 && b.schemas->IntMap.size == 0 { 173 173 + Seq.once(Map.make()) 174 174 + } else if isNaiveCase(a, b) { 175 175 + solveNaive(a, b) 176 176 + } else if isNaiveCase(b, a) { 177 177 + solveNaive(b, a) 178 178 + } else if a.const - b.const == 0 { 179 179 + homogeneousSolve() 180 180 + } else { 181 181 + Seq.empty 182 182 + } 183 183 + } 184 184 + 185 185 + let parse = (str, ~scope: array<string>, ~gen: option<gen>=?) => { 186 186 + open Parser 187 187 + let var = 188 188 + Const.parseVar(~scope) 189 189 + ->map(Base.var) 190 190 + ->label("var") 191 191 + let schemaLit = 192 192 + Const.parseSchema(~gen?, ~scope) 193 193 + ->map(((schematic, allowed)) => Base.schematic(schematic, allowed)) 194 194 + ->label("schematic") 195 195 + let const = 196 196 + Const.parseConst 197 197 + ->map(Base.const) 198 198 + ->label("const") 199 199 + let factor = choice([var, schemaLit, const])->lexeme 200 200 + let term = 201 201 + factor->bind(f => 202 202 + many(token(Const.opString)->then(factor))->map(fs => fs->Array.reduce(f, add)) 203 203 + ) 204 204 + let full = term->between(token(Const.openTerm), token(Const.closeTerm)) 205 205 + Parser.runParser(full, str) 206 206 + } 207 207 + 208 208 + let substitute = (atom: t, subst: subst): t => { 209 209 + let substituted = 210 210 + atom.schemas 211 211 + ->IntMap.toArray 212 212 + ->Array.map(((key, {allowed, count})) => 213 213 + switch Map.get(subst, key) { 214 214 + | None => multiply(Base.schematic(key, allowed), count) 215 215 + | Some(sub) => multiply(sub, count) 216 216 + } 217 217 + ) 218 218 + ->Array.reduce(identity, add) 219 219 + substituted->add({...identity, vars: atom.vars, const: atom.const}) 220 220 + } 221 221 + let substDeBruijn = (atom: t, substs: array<option<t>>, ~from: int=0): t => { 222 222 + let substituted = 223 223 + atom.vars 224 224 + ->IntMap.toArray 225 225 + ->Array.map(((idx, count)) => 226 226 + if idx < from { 227 227 + multiply(Base.var(idx), count) 228 228 + } else if idx - from < Array.length(substs) { 229 229 + switch substs[idx - from]->Option.getExn { 230 230 + | Some(a) => multiply(a, count) 231 231 + | None => 232 232 + throw(SExp.SubstNotCompatible(`index ${Int.toString(idx - from)} not of sort blah`)) 233 233 + } 234 234 + } else { 235 235 + multiply(Base.var(idx - Array.length(substs)), count) 236 236 + } 237 237 + ) 238 238 + ->Array.reduce(identity, add) 239 239 + let schemas = atom.schemas->IntMap.map(({count, allowed}) => { 240 240 + Base.count, 241 241 + allowed: allowed->Array.filterMap(i => 242 242 + if i < from + Array.length(substs) { 243 243 + None 244 244 + } else { 245 245 + Some(i - (from + Array.length(substs))) 246 246 + } 247 247 + ), 248 248 + }) 249 249 + substituted->add({...identity, schemas, const: atom.const}) 250 250 + } 251 251 + let concrete = (atom: t) => atom.vars->IntMap.size > 0 || atom.const > 0 252 252 + 253 253 + let upshift = (atom: t, amount: int, ~from: int=0) => { 254 254 + let vars = 255 255 + atom.vars 256 256 + ->IntMap.toArray 257 257 + ->Array.map(((idx, count)) => 258 258 + if idx >= from { 259 259 + (idx + amount, count) 260 260 + } else { 261 261 + (idx, count) 262 262 + } 263 263 + ) 264 264 + ->IntMap.fromArray 265 265 + let schemas = atom.schemas->IntMap.map(({allowed, count}) => { 266 266 + Base.count, 267 267 + allowed: allowed->Array.map(i => 268 268 + if i >= from { 269 269 + i + amount 270 270 + } else { 271 271 + i 272 272 + } 273 273 + ), 274 274 + }) 275 275 + {Base.vars, schemas, const: atom.const} 276 276 + } 277 277 + let coerce = C.coerce 278 278 + } 279 279 + 280 280 + module MakeView = ( 281 281 + Base: AssocCommBase.AC_BASE_ATOM, 282 282 + Atom: AtomDef.ATOM with module Base = Base, 283 283 + ) => { 284 284 + module Const = Base.Const 285 285 + type props = {atom: Atom.t, scope: array<string>} 286 286 + let renderIf = (component, cond) => 287 287 + if cond { 288 288 + component 289 289 + } else { 290 290 + React.null 291 291 + } 292 292 + module Var = { 293 293 + type props = {idx: int, count?: int, scope: array<string>} 294 294 + let make = (props: props) => { 295 295 + let count = 296 296 + props.count 297 297 + ->Option.map(n => React.int(n)->renderIf(n > 1)) 298 298 + ->Option.getOr(React.null) 299 299 + switch props.scope[props.idx] { 300 300 + | Some(n) if Array.indexOf(props.scope, n) == props.idx => 301 301 + <span className="term-metavar"> 302 302 + {count} 303 303 + {React.string(n)} 304 304 + </span> 305 305 + | _ => 306 306 + <span className="term-metavar-unnamed"> 307 307 + {count} 308 308 + {React.string("\\")} 309 309 + {React.int(props.idx)} 310 310 + </span> 311 311 + } 312 312 + } 313 313 + } 314 314 + 315 315 + let parenthesise = f => 316 316 + React.array([ 317 317 + <span className="symbol-nat" key={"-1"}> {React.string("(")} </span>, 318 318 + f, 319 319 + <span className="symbol-nat" key={"-2"}> {React.string(")")} </span>, 320 320 + ]) 321 321 + 322 322 + let intersperseOp = (a: array<React.element>) => 323 323 + Util.intersperse(a, ~with=React.string(Const.opString))->React.array 324 324 + let make = ({atom, scope}: props) => { 325 325 + let schemas = switch atom.schemas->Belt.Map.Int.size { 326 326 + | 0 => None 327 327 + | _ => 328 328 + atom.schemas 329 329 + ->Belt.Map.Int.toArray 330 330 + ->Array.map(((schematic, {allowed, count})) => 331 331 + <span className="term-schematic"> 332 332 + {React.string(`${count->Int.toString}?`)} 333 333 + {React.int(schematic)} 334 334 + <span className="term-schematic-telescope"> 335 335 + {allowed 336 336 + ->Array.mapWithIndex((idx, _) => <Var idx scope />) 337 337 + ->intersperseOp} 338 338 + </span> 339 339 + </span> 340 340 + ) 341 341 + ->React.array 342 342 + ->Some 343 343 + } 344 344 + let vars = switch atom.vars->Belt.Map.Int.size { 345 345 + | 0 => None 346 346 + | _ => 347 347 + atom.vars 348 348 + ->Belt.Map.Int.toArray 349 349 + ->Array.map(((idx, count)) => <Var idx scope count key={idx->Int.toString} />) 350 350 + ->intersperseOp 351 351 + ->Some 352 352 + } 353 353 + let const = switch (schemas, vars) { 354 354 + | (_, Some(_)) | (Some(_), _) if atom.const > 0 => Some(React.int(atom.const)) 355 355 + | (None, None) => Some(React.int(atom.const)) 356 356 + | _ => None 357 357 + } 358 358 + <span className="term-compound"> 359 359 + {[schemas, vars, const]->Array.keepSome->intersperseOp->parenthesise} 360 360 + </span> 361 361 + } 362 362 + } 363 363 + 364 364 + module Nat = { 365 365 + module Base = AssocCommBase.Nat 366 366 + module Atom = Make( 367 367 + AssocCommBase.Nat, 368 368 + { 369 369 + let coerce = (AtomBase.AnyValue(tag, a)) => 370 370 + switch tag { 371 371 + | Symbolic.Base.Tag => Int.fromString(a)->Option.map(Base.const) 372 372 + | AtomBase.VarBase.Tag => 373 373 + switch a { 374 374 + | Var({idx}) => Some(Base.var(idx)) 375 375 + | Schematic({schematic, allowed}) => Some(Base.schematic(schematic, allowed)) 376 376 + } 377 377 + | AtomBase.String.Tag => 378 378 + switch a { 379 379 + | [String(s)] => Int.fromString(s)->Option.map(Base.const) 380 380 + | _ => None 381 381 + } 382 382 + | _ => None 383 383 + } 384 384 + }, 385 385 + ) 386 386 + module AtomView = MakeView(AssocCommBase.Nat, Atom) 387 387 + }

+74

src/AssocCommBase.res

reviewed

··· 1 1 + module type AC_CONST = { 2 2 + let op: (int, int) => int 3 3 + let opInv: (int, int) => option<int> 4 4 + let opString: string 5 5 + let openTerm: string 6 6 + let closeTerm: string 7 7 + let formatMultiple: (string, int) => string 8 8 + let formatMultipleConst: int => string 9 9 + let parseConst: Parser.t<int> 10 10 + let parseVar: (~scope: array<string>) => Parser.t<int> 11 11 + let parseSchema: (~gen: ref<int>=?, ~scope: array<string>) => Parser.t<(int, array<int>)> 12 12 + } 13 13 + 14 14 + module type AC_BASE_ATOM = { 15 15 + module Const: AC_CONST 16 16 + type base = { 17 17 + schemas: Belt.Map.Int.t<{allowed: array<int>, count: int}>, 18 18 + vars: Belt.Map.Int.t<int>, 19 19 + const: int, 20 20 + } 21 21 + let identity: base 22 22 + let const: int => base 23 23 + let var: int => base 24 24 + let schematic: (int, array<int>) => base 25 25 + include module type of AtomBase.Make({ 26 26 + type t = base 27 27 + }) 28 28 + } 29 29 + 30 30 + module Make = (Const: AC_CONST): AC_BASE_ATOM => { 31 31 + module Const = Const 32 32 + type base = { 33 33 + schemas: Belt.Map.Int.t<{allowed: array<int>, count: int}>, 34 34 + vars: Belt.Map.Int.t<int>, 35 35 + const: int, 36 36 + } 37 37 + module IntMap = Belt.Map.Int 38 38 + let identity = {schemas: IntMap.empty, vars: IntMap.empty, const: 0} 39 39 + let const = n => {...identity, const: n} 40 40 + let var = idx => {...identity, vars: IntMap.empty->IntMap.set(idx, 1)} 41 41 + let schematic = (schematic, allowed) => { 42 42 + ...identity, 43 43 + schemas: IntMap.empty->IntMap.set(schematic, {allowed, count: 1}), 44 44 + } 45 45 + include AtomBase.Make({type t = base}) 46 46 + } 47 47 + 48 48 + module Nat = Make({ 49 49 + let op = (a, b) => a + b 50 50 + let opInv = (a, b) => 51 51 + if a - b < 0 { 52 52 + None 53 53 + } else { 54 54 + Some(a - b) 55 55 + } 56 56 + let opString: string = "+" 57 57 + let openTerm: string = "nat(" 58 58 + let closeTerm: string = ")" 59 59 + let formatMultiple: (string, int) => string = (s, n) => `${n->Int.toString}${s}` 60 60 + let formatMultipleConst: int => string = n => Int.toString(n) 61 61 + let parseConst: Parser.t<int> = Parser.decimal 62 62 + let parseVar = (~scope) => Parser.Util.varIdx(~scope) 63 63 + let seen = (g: ref<int>, s: int) => { 64 64 + if s >= g.contents { 65 65 + g := s + 1 66 66 + } 67 67 + } 68 68 + let parseSchema = (~gen=?, ~scope: array<string>): Parser.t<(int, array<int>)> => { 69 69 + Parser.Util.schemaLit(~scope)->Parser.map(((schematic, allowed)) => { 70 70 + gen->Option.map(g => allowed->Array.forEach(n => seen(g, n)))->ignore 71 71 + (schematic, allowed) 72 72 + }) 73 73 + } 74 74 + })

-1

src/Method.res

reviewed

··· 335 335 if cur.contents->String.get(0) == Some("}") { 336 336 cur := String.trim(cur.contents->String.sliceToEnd(~start=1)) 337 337 let res = {ruleName, elimName, instantiation, subgoals} 338 338 - Console.log(("parsed elim", res)) 339 338 Ok((res, cur.contents)) 340 339 } else { 341 340 Error("} or subgoal proof expected")

+30 -1

src/Parser.res

reviewed

··· 106 106 } 107 107 ) 108 108 )->map(List.toArray) 109 109 + let sepBy = (t, delim) => t->bind(p => many(delim->then(t))->map(ps => Array.concat([p], ps))) 109 110 let between = (inner: t<'a>, o1: t<string>, o2: t<string>): t<'a> => o1->then(inner)->thenIgnore(o2) 110 111 let consume = (l: int): t<string> => 111 112 getCurrentStr->bind(str => { ··· 142 143 if str->String.startsWith(s) { 143 144 consume(String.length(s))->then(pure(s)) 144 145 } else { 145 145 - expected([`literal ${s}`]) 146 146 + expected([`"${s}"`]) 146 147 } 147 148 ) 148 149 ··· 212 213 Console.log(("successfully parsed", res)) 213 214 dbgInfo("exit")->map(_ => res) 214 215 }) 216 216 + ->mapError(err => { 217 217 + Console.log(("error", infoPretty(err.info))) 218 218 + err 219 219 + }) 215 220 } 216 221 217 222 let lexeme = p => p->thenIgnore(regex(/^\s*/)->void) ··· 235 240 ~scope: array<'m>, 236 241 ~gen: option<'g>=?, 237 242 ): t<'a> => lift(s => f(s, ~scope, ~gen?)) 243 243 + 244 244 + module Util = { 245 245 + let varLit = string("\\")->then(decimal)->lexeme 246 246 + let ident = regex1(/([^\s\(\)]+)/)->lexeme 247 247 + let varIdx = (~scope: array<string>) => 248 248 + varLit->or( 249 249 + ident->bind(id => 250 250 + switch scope->Array.indexOfOpt(id) { 251 251 + | Some(idx) => pure(idx) 252 252 + | None => expected(["in-scope variable"]) 253 253 + } 254 254 + ), 255 255 + ) 256 256 + let schemaLit = (~scope: array<string>) => 257 257 + string("?") 258 258 + ->then(decimal) 259 259 + ->bind(schematic => 260 260 + many(varIdx(~scope)) 261 261 + ->between(token("("), token(")")) 262 262 + ->map(allowed => { 263 263 + (schematic, allowed) 264 264 + }) 265 265 + ) 266 266 + }

+5 -24

src/SExp.res

reviewed

··· 267 267 } 268 268 let mkParser = (~scope: array<string>, ~gen=?): Parser.t<t> => { 269 269 open Parser 270 270 - let varLit = string("\\")->then(decimal) 271 271 - let ident = regex1(/([^\s\(\)]+)/) 272 272 - let varIdx = 273 273 - varLit 274 274 - ->or( 275 275 - ident->bind(id => 276 276 - switch scope->Array.indexOfOpt(id) { 277 277 - | Some(idx) => pure(idx) 278 278 - | None => fail("expected variable") 279 279 - } 280 280 - ), 281 281 - ) 282 282 - ->lexeme 270 270 + let varIdx = Parser.Util.varIdx(~scope) 283 271 let var = varIdx->map(idx => Var({idx: idx})) 272 272 + let schemaLit = Parser.Util.schemaLit(~scope)->Parser.map(((schematic, allowed)) => { 273 273 + gen->Option.map(g => allowed->Array.forEach(n => seen(g, n)))->ignore 274 274 + Schematic({schematic, allowed}) 275 275 + }) 284 276 285 285 - let schemaLit = 286 286 - string("?") 287 287 - ->then(decimal) 288 288 - ->bind(schematic => 289 289 - many(varIdx) 290 290 - ->between(token("("), token(")")) 291 291 - ->map(allowed => { 292 292 - gen->Option.map(g => allowed->Array.forEach(n => seen(g, n)))->ignore 293 293 - Schematic({schematic, allowed}) 294 294 - }) 295 295 - ) 296 277 let inner = fix(f => 297 278 choice([ 298 279 schemaLit->label("schematic"),

+9 -3

src/Scratch.res

reviewed

··· 54 54 Symbol.Atom, 55 55 Symbol.AtomView, 56 56 ) 57 57 - module StringSExp = SExp.Make(StringSymbol.Atom) 58 58 - module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) 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 StringSExp = SExp.Make(StringNatSymbol.Atom) 64 64 + module TermView = SExpView.Make(StringNatSymbol.Atom, StringNatSymbol.AtomView, StringSExp) 59 65 module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) 60 66 module AxiomStr = Editable.TextArea( 61 61 - StringAxiomSet.Make(StringSymbol.Atom, StringSExp, StringSExpJView), 67 67 + StringAxiomSet.Make(StringNatSymbol.Atom, StringSExp, StringSExpJView), 62 68 ) 63 69 64 70 module DerivationsOrLemmasStrView = MethodView.CombineMethodView(

+8

src/StringA.res

reviewed

··· 471 471 | Schematic({schematic, allowed}) => Schematic({schematic, allowed}) 472 472 }, 473 473 ]) 474 474 + | AssocCommBase.Nat.Tag => { 475 475 + module IntMap = Belt.Map.Int 476 476 + if a.schemas->IntMap.size == 0 && a.vars->IntMap.size == 0 { 477 477 + Some([String(Int.toString(a.const))]) 478 478 + } else { 479 479 + None 480 480 + } 481 481 + } 474 482 | _ => None 475 483 } 476 484 }

+4

src/Util.res

reviewed

··· 108 108 ->Iterator.toArrayWithMapper(((i, v)) => f(i, v)->Option.map(v => (i, v))) 109 109 ->Array.keepSome 110 110 ->Map.fromArray 111 111 + let update = (m: t<'k, 'v>, k: 'k, f: 'v => 'v, ~default: 'v) => { 112 112 + m->Map.set(k, Map.get(m, k)->Option.map(f)->Option.getOr(default)) 113 113 + } 114 114 + let clone = (m: t<'k, 'v>) => m->Map.entries->Map.fromIterator 111 115 } 112 116 113 117 let arrayWithIndex = (arr: array<React.element>) => {

+49

tests/NatTest.res

reviewed

··· 1 1 + open Zora 2 2 + 3 3 + module NatBase = AssocCommBase.Nat 4 4 + module Nat = AssocComm.Nat.Atom 5 5 + module Util = TestUtil.MakeAtomTester(Nat) 6 6 + module ParseUtil = Util.ParseTester 7 7 + module UnifyUtil = Util.UnifyTester 8 8 + 9 9 + module IntMap = Belt.Map.Int 10 10 + let const = NatBase.const 11 11 + let var = NatBase.var 12 12 + let schematic = NatBase.schematic 13 13 + 14 14 + zoraBlock("parse nat", t => { 15 15 + let testParse = (t, str, expected, ~scope=?) => 16 16 + t->ParseUtil.testParse(`nat(${str})`, expected, ~scope?) 17 17 + let testParseFail = (t, str, ~scope=?) => t->ParseUtil.testParseFail(`nat(${str})`, ~scope?) 18 18 + t->block("const", t => { 19 19 + t->block("single digit", t => t->testParse("1", const(1))) 20 20 + t->block("multi digit", t => t->testParse("123", const(123))) 21 21 + t->block("negative", t => t->testParseFail("-1")) 22 22 + }) 23 23 + t->block("var", t => { 24 24 + t->block("in scope", t => t->testParse("x", var(0), ~scope=["x"])) 25 25 + t->block("not in scope", t => t->testParseFail("x")) 26 26 + t->block("const", t => t->testParse(`\\1`, var(1))) 27 27 + t->block("const multi digit", t => t->testParse(`\\10`, var(10))) 28 28 + }) 29 29 + t->block("schematic", t => { 30 30 + t->block("valid empty allowed", t => t->testParse(`?1()`, schematic(1, []))) 31 31 + t->block("invalid no allowed", t => t->testParseFail(`?1`)) 32 32 + t->block("valid empty allowed multi digit", t => t->testParse(`?10()`, schematic(10, []))) 33 33 + t->block( 34 34 + "valid with non-empty allowed", 35 35 + t => t->testParse(`?10(\\1 \\23 \\4)`, schematic(10, [1, 23, 4])), 36 36 + ) 37 37 + }) 38 38 + t->block("single add", t => t->testParse("1 + 2", Nat.add(const(1), const(2)))) 39 39 + t->block("multi add", t => { 40 40 + t->testParse("1 + 2 + x", Nat.add(Nat.add(const(1), const(2)), var(0)), ~scope=["x"]) 41 41 + t->testParse("?1(x) + ?1()", Nat.add(schematic(1, [0]), schematic(1, [])), ~scope=["x"]) 42 42 + }) 43 43 + }) 44 44 + 45 45 + zoraBlock("unify nat", t => { 46 46 + let parse = s => Nat.parse(`nat(${s})`, ~scope=[])->Result.getExn->Pair.first 47 47 + t->block("test", t => t->UnifyUtil.testUnify(parse("?1()"), parse("?2()"))) 48 48 + t->block("test", t => t->UnifyUtil.testUnify(parse("?1() + ?2()"), parse("?3() + ?3()"))) 49 49 + })

+1 -1

tests/ParserTests.res

reviewed

··· 5 5 switch P.runParser(p, str) { 6 6 | Ok((res, "")) => expect->Option.map(expect => t->equal(res, expect))->ignore 7 7 | Ok((_, rem)) => t->fail(~msg=`failed to consume remaining input: ${rem}`) 8 8 - | Error(e) => t->fail(~msg=`parse failed`) 8 8 + | Error(msg) => t->fail(~msg=`parse failed: ${msg}`) 9 9 } 10 10 } 11 11