Skip to content

Commit 1fe9203

Browse files
explnexpln
authored
Merge pull request #167 from expln/feature/166-Bottom-up-prover-adds-unnecessary-disjoints
Fix #166 Bottom-up prover adds unnecessary disjoints
2 parents b3debce + ad37581 commit 1fe9203

28 files changed

+391
-170
lines changed

‎src/metamath/mm-utils/MM_asrt_apply.res

+11-26
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ open MM_parser
88
type applyAssertionResult = {
99
newVars: array<int>,
1010
newVarTypes: array<int>,
11-
newDisj:disjMutable,
1211
frame: frame,
1312
subs: subs,
1413
err:option<unifErr>,
@@ -368,26 +367,17 @@ let checkDisj = (
368367
~allowNewDisjForExistingVars:bool,
369368
~isDisjInCtx:(int,int)=>bool,
370369
~debugLevel:int,
371-
):result<disjMutable,unifErr> => {
372-
let resultDisj = disjMake()
373-
let verifRes = verifyDisjoints(~frmDisj, ~subs, ~debugLevel, ~isDisjInCtx = (n,m) => {
374-
if (n <= maxCtxVar && m <= maxCtxVar) {
375-
if (isDisjInCtx(n,m)) {
376-
true
377-
} else if (allowNewDisjForExistingVars) {
378-
resultDisj->disjAddPair(n,m)
379-
true
370+
):option<unifErr> => {
371+
if (allowNewDisjForExistingVars) {
372+
None
373+
} else {
374+
verifyDisjoints(~frmDisj, ~subs, ~debugLevel, ~isDisjInCtx = (n,m) => {
375+
if (n <= maxCtxVar && m <= maxCtxVar) {
376+
isDisjInCtx(n,m)
380377
} else {
381-
false
378+
true
382379
}
383-
} else {
384-
resultDisj->disjAddPair(n,m)
385-
true
386-
}
387-
})
388-
switch verifRes {
389-
| None => Ok(resultDisj)
390-
| Some(err) => Error(err)
380+
})
391381
}
392382
}
393383

@@ -439,7 +429,6 @@ let applyAssertions = (
439429
{
440430
newVars: [],
441431
newVarTypes: [],
442-
newDisj: disjMake(),
443432
frame: frm.frame,
444433
subs: subsClone(frm.subs),
445434
err:Some(NoUnifForAsrt({asrtExpr:frm.frame.asrt, expr}))
@@ -497,7 +486,6 @@ let applyAssertions = (
497486
{
498487
newVars: [],
499488
newVarTypes: [],
500-
newDisj: disjMake(),
501489
frame: frm.frame,
502490
subs: subsClone(frm.subs),
503491
err: Some(err)
@@ -519,7 +507,6 @@ let applyAssertions = (
519507
{
520508
newVars: [],
521509
newVarTypes: [],
522-
newDisj: disjMake(),
523510
frame: frm.frame,
524511
subs: subsClone(frm.subs),
525512
err: Some(err)
@@ -535,11 +522,10 @@ let applyAssertions = (
535522
~allowNewDisjForExistingVars,
536523
~debugLevel,
537524
) {
538-
| Ok(newDisj) => {
525+
| None => {
539526
let res = {
540527
newVars: workVars.newVars->Js.Array2.copy,
541528
newVarTypes: workVars.newVarTypes->Js.Array2.copy,
542-
newDisj,
543529
frame: frm.frame,
544530
subs: subsClone(frm.subs),
545531
err:None
@@ -551,14 +537,13 @@ let applyAssertions = (
551537
Continue
552538
}
553539
}
554-
| Error(err) => {
540+
| Some(err) => {
555541
if (debugLevel == 0) {
556542
Continue
557543
} else {
558544
let res = {
559545
newVars: workVars.newVars->Js.Array2.copy,
560546
newVarTypes: workVars.newVarTypes->Js.Array2.copy,
561-
newDisj: disjMake(),
562547
frame: frm.frame,
563548
subs: subsClone(frm.subs),
564549
err:Some(err)

‎src/metamath/mm-utils/MM_asrt_apply.resi

-1
Original file line numberDiff line numberDiff line change
@@ -6,7 +6,6 @@ open MM_unification_debug
66
type applyAssertionResult = {
77
newVars: array<int>,
88
newVarTypes: array<int>,
9-
newDisj:disjMutable,
109
frame: frame,
1110
subs: subs,
1211
err:option<unifErr>,

‎src/metamath/mm-utils/MM_context.res

+10-3
Original file line numberDiff line numberDiff line change
@@ -894,12 +894,19 @@ let renumberVarsInHypothesis = (ctxToFrameRenum: Belt_HashMapInt.t<int>, hyp: hy
894894
}
895895

896896
let renumberVarsInDisj = (ctxToFrameRenum: Belt_HashMapInt.t<int>, disj:disjMutable): Belt_MapInt.t<Belt_SetInt.t> => {
897-
disj
897+
let res = disjMake()
898+
disj->disjForEach((n,m) => {
899+
res->disjAddPair(
900+
ctxToFrameRenum->ctxIntToFrameInt(n),
901+
ctxToFrameRenum->ctxIntToFrameInt(m)
902+
)
903+
})
904+
res
898905
->Belt_HashMapInt.toArray
899906
->Js.Array2.map(((n,ms)) => {
900907
(
901-
ctxToFrameRenum->ctxIntToFrameInt(n),
902-
ctxToFrameRenum->renumberVarsInExpr(ms->Belt_HashSetInt.toArray)->Belt_SetInt.fromArray
908+
n,
909+
ms->Belt_HashSetInt.toArray->Belt_SetInt.fromArray
903910
)
904911
})
905912
->Belt_MapInt.fromArray

‎src/metamath/mm-utils/MM_proof_tree.res

+5-15
Original file line numberDiff line numberDiff line change
@@ -18,7 +18,6 @@ type proofNodeDbg = {
1818

1919
type proofTreeDbg = {
2020
newVars: array<string>,
21-
disj: array<string>,
2221
exprToStr: expr=>string,
2322
}
2423

@@ -45,9 +44,9 @@ and proofTree = {
4544
hypsByExpr: Belt_HashMap.t<expr,hypothesis,ExprHash.identity>,
4645
hypsByLabel: Belt_HashMapString.t<hypothesis>,
4746
ctxMaxVar:int,
47+
ctxDisj: disjMutable,
4848
mutable maxVar:int,
4949
newVars: Belt_HashSet.t<expr,ExprHash.identity>,
50-
disj: disjMutable,
5150
parenCnt:parenCnt,
5251
mutable nextNodeId: int,
5352
nodes: Belt_HashMap.t<expr,proofNode,ExprHash.identity>,
@@ -106,7 +105,7 @@ let pnGetDbg = node => node.pnDbg
106105
let emptyFrmArr = []
107106
let ptGetFrms = (tree,typ) => tree.frms->Belt_HashMapInt.get(typ)->Belt.Option.getWithDefault(emptyFrmArr)
108107
let ptGetParenCnt = tree => tree.parenCnt
109-
let ptIsDisj = (tree:proofTree, n, m) => tree.disj->disjContains(n,m)
108+
let ptIsDisjInCtx = (tree:proofTree, n, m) => tree.ctxDisj->disjContains(n,m)
110109
let ptIsNewVarDef = (tree:proofTree, expr) => tree.newVars->Belt_HashSet.has(expr)
111110
let ptGetHypByExpr = ( tree:proofTree, expr:expr ):option<hypothesis> => tree.hypsByExpr->Belt_HashMap.get(expr)
112111
let ptGetHypByLabel = ( tree:proofTree, label:string ):option<hypothesis> =>
@@ -116,13 +115,13 @@ let ptGetCtxMaxVar = tree => tree.ctxMaxVar
116115
let ptGetRootStmts = tree => tree.rootStmts
117116
let ptGetDbg = (tree:proofTree) => tree.ptDbg
118117
let ptGetCopyOfNewVars = tree => tree.newVars->Belt_HashSet.toArray
119-
let ptGetDisj = tree => tree.disj
118+
let ptGetCtxDisj = tree => tree.ctxDisj
120119

121120
let ptMake = (
122121
~frms: frms,
123122
~hyps: Belt_MapString.t<hypothesis>,
124123
~ctxMaxVar: int,
125-
~disj: disjMutable,
124+
~ctxDisj: disjMutable,
126125
~parenCnt: parenCnt,
127126
~exprToStr: option<expr=>string>,
128127
) => {
@@ -136,7 +135,7 @@ let ptMake = (
136135
ctxMaxVar,
137136
maxVar:ctxMaxVar,
138137
newVars: Belt_HashSet.make(~id=module(ExprHash), ~hintSize=16),
139-
disj,
138+
ctxDisj,
140139
parenCnt,
141140
nextNodeId: 0,
142141
nodes: Belt_HashMap.make(~id=module(ExprHash), ~hintSize=128),
@@ -145,7 +144,6 @@ let ptMake = (
145144
ptDbg: exprToStr->Belt_Option.map(exprToStr => {
146145
{
147146
newVars: [],
148-
disj: [],
149147
exprToStr,
150148
}
151149
})
@@ -310,14 +308,6 @@ let ptAddNewVar = (tree, typ):int => {
310308
newVar
311309
}
312310

313-
let ptAddDisjPair = (tree, n, m) => {
314-
tree.disj->disjAddPair( n,m )
315-
switch tree.ptDbg {
316-
| None => ()
317-
| Some({exprToStr, disj}) => disj->Js.Array2.push(exprToStr([n,m]))->ignore
318-
}
319-
}
320-
321311
let jstfEqSrc = (jstfArgs:array<expr>, jstfLabel:string, src:exprSrc):bool => {
322312
switch src {
323313
| VarType | Hypothesis(_) | AssertionWithErr(_) => false

‎src/metamath/mm-utils/MM_proof_tree.resi

+3-5
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ type proofNodeDbg = {
1717

1818
type proofTreeDbg = {
1919
newVars: array<string>,
20-
disj: array<string>,
2120
exprToStr: expr=>string,
2221
}
2322

@@ -35,7 +34,7 @@ let ptMake: (
3534
~frms: frms,
3635
~hyps: Belt_MapString.t<hypothesis>,
3736
~ctxMaxVar: int,
38-
~disj: disjMutable,
37+
~ctxDisj: disjMutable,
3938
~parenCnt: parenCnt,
4039
~exprToStr: option<expr=>string>,
4140
) => proofTree
@@ -46,12 +45,11 @@ let ptGetHypByLabel: (proofTree, string) => option<hypothesis>
4645
let ptGetMaxVar: proofTree => int
4746
let ptGetCtxMaxVar: proofTree => int
4847
let ptGetParenCnt: proofTree => parenCnt
49-
let ptIsDisj: (proofTree, int, int) => bool
48+
let ptIsDisjInCtx: (proofTree, int, int) => bool
5049
let ptIsNewVarDef: (proofTree, expr) => bool
5150
let ptGetRootStmts: proofTree => array<rootStmt>
5251
let ptGetNode: (proofTree, expr) => proofNode
5352
let ptAddNewVar: (proofTree, int) => int
54-
let ptAddDisjPair: (proofTree, int, int) => unit
5553
let ptAddRootStmt: (proofTree, rootStmt) => unit
5654
let ptAddSyntaxProof: (proofTree, expr, proofNode) => unit
5755
let ptGetSyntaxProof: (proofTree, expr) => option<proofNode>
@@ -60,7 +58,7 @@ let ptClearDists: proofTree => unit
6058
let ptGetDbg: proofTree => option<proofTreeDbg>
6159

6260
let ptGetCopyOfNewVars: proofTree => array<expr>
63-
let ptGetDisj: proofTree => disjMutable
61+
let ptGetCtxDisj: proofTree => disjMutable
6462

6563
let pnGetId: proofNode => int
6664
let pnGetExpr: proofNode => expr

‎src/metamath/mm-utils/MM_proof_tree_dto.res

-4
Original file line numberDiff line numberDiff line change
@@ -16,7 +16,6 @@ type proofNodeDbgDto = {
1616

1717
type proofTreeDbgDto = {
1818
newVars: array<string>,
19-
disj: array<string>,
2019
}
2120

2221
type proofNodeDto = {
@@ -28,7 +27,6 @@ type proofNodeDto = {
2827

2928
type proofTreeDto = {
3029
newVars: array<expr>,
31-
disj: disjMutable,
3230
nodes: array<proofNodeDto>,
3331
syntaxProofs: array<(expr,proofNodeDto)>,
3432
dbg: option<proofTreeDbgDto>,
@@ -139,13 +137,11 @@ let proofTreeToDto = (
139137

140138
{
141139
newVars: tree->ptGetCopyOfNewVars,
142-
disj: tree->ptGetDisj,
143140
nodes,
144141
syntaxProofs: createSyntaxProofsDto( ~tree, ~exprToIdx, ~nodes, ),
145142
dbg: tree->ptGetDbg->Belt_Option.map(dbg => {
146143
{
147144
newVars: dbg.newVars,
148-
disj: dbg.disj,
149145
}
150146
})
151147
}

‎src/metamath/mm-utils/MM_proof_tree_dto.resi

-2
Original file line numberDiff line numberDiff line change
@@ -15,7 +15,6 @@ type proofNodeDbgDto = {
1515

1616
type proofTreeDbgDto = {
1717
newVars: array<string>,
18-
disj: array<string>,
1918
}
2019

2120
type proofNodeDto = {
@@ -27,7 +26,6 @@ type proofNodeDto = {
2726

2827
type proofTreeDto = {
2928
newVars: array<expr>,
30-
disj: disjMutable,
3129
nodes: array<proofNodeDto>,
3230
syntaxProofs: array<(expr,proofNodeDto)>,
3331
dbg: option<proofTreeDbgDto>,

‎src/metamath/mm-utils/MM_proof_verifier.resi

+7
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,6 @@
11
open MM_parser
22
open MM_context
3+
open MM_unification_debug
34

45
type proofNodeDbg = {
56
exprStr: string,
@@ -21,3 +22,9 @@ let verifyProof: (
2122
let compressedProofBlockToArray: string => array<string>
2223
let compressedProofStrToInt: string => int
2324
let intToCompressedProofStr: int => string
25+
26+
let verifyDisjoints: (
27+
~subs:array<expr>,
28+
~frmDisj:Belt_MapInt.t<Belt_SetInt.t>,
29+
~isDisjInCtx: (int,int) => bool,
30+
) => option<unifErr>

‎src/metamath/mm-utils/MM_provers.res

+3-9
Original file line numberDiff line numberDiff line change
@@ -84,7 +84,7 @@ let findAsrtParentsWithoutNewVars = (
8484
&& verifyDisjoints(
8585
~frmDisj=frm.frame.disj,
8686
~subs,
87-
~isDisjInCtx=tree->ptIsDisj,
87+
~isDisjInCtx=tree->ptIsDisjInCtx,
8888
~debugLevel=0
8989
)->Belt.Option.isNone
9090
) {
@@ -241,7 +241,7 @@ let findAsrtParentsWithNewVars = (
241241
applyAssertions(
242242
~maxVar = maxVarBeforeSearch,
243243
~frms = tree->ptGetFrms(expr[0]),
244-
~isDisjInCtx = tree->ptIsDisj,
244+
~isDisjInCtx = tree->ptIsDisjInCtx,
245245
~parenCnt=tree->ptGetParenCnt,
246246
~statements = args,
247247
~exactOrderOfStmts = exactOrderOfArgs,
@@ -289,12 +289,6 @@ let findAsrtParentsWithNewVars = (
289289
let treeNewVar = tree->ptAddNewVar(newVarType)
290290
applNewVarToTreeNewVar->Belt_MutableMapInt.set(applResNewVar,treeNewVar)
291291
})
292-
applResult.newDisj->disjForEach((n,m) => {
293-
tree->ptAddDisjPair(
294-
applNewVarToTreeNewVar->Belt_MutableMapInt.getWithDefault(n, n),
295-
applNewVarToTreeNewVar->Belt_MutableMapInt.getWithDefault(m, m),
296-
)
297-
})
298292
let numOfArgs = frame.hyps->Js_array2.length
299293
let args = Expln_utils_common.createArray(numOfArgs)
300294
let unprovedFloating = ref(None)
@@ -654,7 +648,7 @@ let createProofTree = (
654648
~frms,
655649
~hyps,
656650
~ctxMaxVar,
657-
~disj=proofCtx->getAllDisj,
651+
~ctxDisj=proofCtx->getAllDisj,
658652
~parenCnt,
659653
~exprToStr=makeExprToStr(proofCtx, ctxMaxVar),
660654
)

0 commit comments

Comments
 (0)