···339339 (= a b) (f a)
340340 -------- eq-ap
341341 (f b)
342342+343343+ a.
344344+ -------- eqab
345345+ (= (A a) (B a))
342346 </hol-comp>
343347 <hol-config id="index.html/myconfig">Gentzen</hol-config>
344348 <hol-proof id="index.html/prooftest" deps="index.html/myconfig index.html/baz index.html/nat">
···367371 (= a c)
368372369373 a. b. c. ab bc |- ?
374374+ </hol-proof>
375375+ <hol-proof id="index.html/eq-high" deps="index.html/myconfig index.html/baz index.html/nat">
376376+ ------- A0B0
377377+ (= (A 0) (B 0))
378378+379379+ |- ?
370380 </hol-proof>
371381 <h1>String</h1>
372382 <h2>Basic</h2>
···491491}
492492493493module MakeRewriteHOTerm = (
494494- Judgment: JUDGMENT with module Term := HOTerm,
494494+ Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
495495 Config: {
496496 let keyword: string
497497 let reversed: bool
···501501 module Rule = Rule.Make(HOTerm, Judgment)
502502 module Context = Context(HOTerm, Judgment)
503503504504- let isEqualityRule = (rule: Rule.t): bool => {
505505- Array.length(rule.vars) == 0 && Array.length(rule.premises) == 0
506506- }
507507-508508- let extractEqualityTerms = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => {
509509- let term: HOTerm.t = Obj.magic(judgment)
504504+ let extractEqualityTermsFromJudgment = (judgment: Judgment.t): option<(HOTerm.t, HOTerm.t)> => {
505505+ let term: HOTerm.t = judgment
510506 switch HOTerm.strip(term) {
511507 | (HOTerm.Symbol({name: "="}), args) if Array.length(args) == 2 =>
512508 Some((args->Array.getUnsafe(0), args->Array.getUnsafe(1)))
···514510 }
515511 }
516512513513+ let extractEqualityTerms = (rule: Rule.t): option<(HOTerm.t, HOTerm.t)> => {
514514+ if Array.length(rule.premises) != 0 {
515515+ None
516516+ } else {
517517+ extractEqualityTermsFromJudgment(rule.conclusion)
518518+ }
519519+ }
520520+521521+ let extractEqualityTermsFromBare = (rule: Rule.bare): option<(HOTerm.t, HOTerm.t)> => {
522522+ if Array.length(rule.premises) != 0 {
523523+ None
524524+ } else {
525525+ extractEqualityTermsFromJudgment(rule.conclusion)
526526+ }
527527+ }
528528+529529+ let isEqualityRule = (rule: Rule.t): bool => {
530530+ extractEqualityTerms(rule)->Option.isSome
531531+ }
532532+517533 type t<'a> = {
518534 equalityName: string,
535535+ instantiation: array<Judgment.substCodom>,
519536 subgoal: 'a,
520537 }
521538···524541 let map = (it: t<'a>, f) => {
525542 {
526543 equalityName: it.equalityName,
544544+ instantiation: it.instantiation,
527545 subgoal: f(it.subgoal),
528546 }
529547 }
530548531531- let substitute = (it: t<'a>, _subst: Judgment.subst) => {
532532- // Rewrite method itself doesn't contain terms that need substitution
533533- it
549549+ let substitute = (it: t<'a>, subst: Judgment.subst) => {
550550+ {
551551+ equalityName: it.equalityName,
552552+ instantiation: it.instantiation->Array.map(t => t->Judgment.substituteSubstCodom(subst)),
553553+ subgoal: it.subgoal,
554554+ }
534555 }
535556536557 let prettyPrint = (
···540561 ~subprinter: ('a, ~scope: array<HOTerm.meta>, ~indentation: int=?) => string,
541562 ) => {
542563 let ind = String.repeat(" ", indentation)
543543- `${ind}${Config.keyword} ${it.equalityName} {\n`
564564+ let args = it.instantiation->Array.map(t => Judgment.prettyPrintSubstCodom(t, ~scope))
565565+ let argsStr = if Array.length(args) > 0 {
566566+ " " ++ Array.join(args, " ")
567567+ } else {
568568+ ""
569569+ }
570570+ `${ind}${Config.keyword} (${it.equalityName}${argsStr}) {\n`
544571 ->String.concat(subprinter(it.subgoal, ~scope, ~indentation=indentation + 2))
545572 ->String.concat("\n")
546573 ->String.concat(ind)
···552579 let parse = (input, ~keyword as _, ~scope, ~gen, ~subparser) => {
553580 let cur = ref(String.trim(input))
554581555555- switch Rule.parseRuleName(cur.contents) {
556556- | Error(e) => Error(e)
557557- | Ok((equalityName, rest)) => {
558558- cur := String.trim(rest)
582582+ if cur.contents->String.get(0) == Some("(") {
583583+ switch Rule.parseRuleName(cur.contents->String.sliceToEnd(~start=1)) {
584584+ | Error(e) => Error(e)
585585+ | Ok((equalityName, rest)) => {
586586+ cur := rest
587587+ let instantiation = []
588588+ let it = ref(Error(""))
589589+ while {
590590+ it := Judgment.parseSubstCodom(cur.contents, ~scope, ~gen)
591591+ it.contents->Result.isOk
592592+ } {
593593+ let (val, rest) = it.contents->Result.getExn
594594+ Array.push(instantiation, val)
595595+ cur := String.trim(rest)
596596+ }
597597+ if cur.contents->String.get(0) == Some(")") {
598598+ cur := String.trim(cur.contents->String.sliceToEnd(~start=1))
559599560560- if cur.contents->String.get(0) == Some("{") {
561561- cur := String.trim(String.sliceToEnd(cur.contents, ~start=1))
600600+ if cur.contents->String.get(0) == Some("{") {
601601+ cur := String.trim(String.sliceToEnd(cur.contents, ~start=1))
562602563563- try {
564564- switch subparser(cur.contents, ~scope, ~gen) {
565565- | Error(e) => raise(InternalParseError(e))
566566- | Ok((subgoal, rest2)) => {
567567- cur := String.trim(rest2)
603603+ try {
604604+ switch subparser(cur.contents, ~scope, ~gen) {
605605+ | Error(e) => raise(InternalParseError(e))
606606+ | Ok((subgoal, rest2)) => {
607607+ cur := String.trim(rest2)
568608569569- if cur.contents->String.get(0) == Some("}") {
570570- cur := String.trim(String.sliceToEnd(cur.contents, ~start=1))
571571- Ok(({equalityName, subgoal}, cur.contents))
572572- } else {
573573- Error("Expected } after subgoal")
609609+ if cur.contents->String.get(0) == Some("}") {
610610+ cur := String.trim(String.sliceToEnd(cur.contents, ~start=1))
611611+ Ok(({equalityName, instantiation, subgoal}, cur.contents))
612612+ } else {
613613+ Error("Expected } after subgoal")
614614+ }
615615+ }
574616 }
617617+ } catch {
618618+ | InternalParseError(e) => Error(e)
575619 }
620620+ } else {
621621+ Error("Expected { after equality instantiation")
576622 }
577577- } catch {
578578- | InternalParseError(e) => Error(e)
623623+ } else {
624624+ Error(") or term expected")
579625 }
580580- } else {
581581- Error("Expected { after equality name")
582626 }
583627 }
628628+ } else {
629629+ Error("Expected (")
584630 }
585631 }
586632587587- let rewriteJudgmentTerms = (judgment: Judgment.t, from: HOTerm.t, to: HOTerm.t): Judgment.t => {
588588- Judgment.mapTerms(judgment, term => HOTerm.discharge([(from, to)], term, ~prune=false))
633633+ let rewriteJudgmentTerms = (
634634+ judgment: Judgment.t,
635635+ from: HOTerm.t,
636636+ to: HOTerm.t,
637637+ ~gen: option<HOTerm.gen>,
638638+ ): (HOTerm.subst, Judgment.t) => {
639639+ let subst: ref<HOTerm.subst> = ref(HOTerm.makeSubst())
640640+ let j = Judgment.mapTerms(judgment, term => {
641641+ let (subst', newTerm) = HOTerm.rewrite(term, from, to, ~subst=subst.contents, ~gen)
642642+ subst := subst'
643643+ newTerm
644644+ })
645645+ (subst.contents, j)
589646 }
590647591591- let apply = (ctx: Context.t, j: Judgment.t, _gen: HOTerm.gen, f: Rule.t => 'a) => {
592592- let ret = Dict.make()
593593- // For HOTermJ, Judgment.subst is the same as HOTerm.subst
594594- let emptySubst: Judgment.subst = Obj.magic(HOTerm.makeSubst())
648648+ let apply = (ctx: Context.t, j: Judgment.t, gen: HOTerm.gen, f: Rule.t => 'a) => {
649649+ let ret: Dict.t<(t<'a>, Judgment.subst)> = Dict.make()
595650596651 ctx.facts->Dict.forEachWithKey((eqRule, name) => {
597652 if isEqualityRule(eqRule) {
598598- switch extractEqualityTerms(eqRule.conclusion) {
653653+ let insts = eqRule->Rule.schematise(gen, ~scope=ctx.fixes)
654654+ let instantiatedRule = eqRule->Rule.instantiate(insts)
655655+656656+ switch extractEqualityTermsFromBare(instantiatedRule) {
599657 | Some((lhs, rhs)) => {
600658 let (from, to) = if Config.reversed {
601659 (rhs, lhs)
···603661 (lhs, rhs)
604662 }
605663606606- let rewrittenGoal = rewriteJudgmentTerms(j, from, to)
607607- if !Judgment.equivalent(j, rewrittenGoal) {
664664+ let (subst, rewrittenGoal) = rewriteJudgmentTerms(j, from, to, ~gen=Some(gen))
665665+666666+ // If the rewritten one is the same as the original, for example rewriting with reflexivity, skip it
667667+ if (
668668+ !Judgment.equivalent(
669669+ j->Judgment.substitute(subst)->Judgment.reduce,
670670+ rewrittenGoal->Judgment.substitute(subst)->Judgment.reduce,
671671+ )
672672+ ) {
673673+ let rewrittenRule: Rule.t = {
674674+ vars: [],
675675+ premises: [],
676676+ conclusion: rewrittenGoal,
677677+ }
608678 let method = {
609679 equalityName: name,
610610- subgoal: f(eqRule),
680680+ instantiation: insts,
681681+ subgoal: f(rewrittenRule),
611682 }
612612- ret->Dict.set(`${Config.keyword} ${name}`, (method, emptySubst))
683683+ ret->Dict.set(`${Config.keyword} ${name}`, (method, subst))
613684 }
614685 }
615686 | None => ()
···624695 switch ctx.facts->Dict.get(it.equalityName) {
625696 | None => Error(`Cannot find equality '${it.equalityName}'`)
626697 | Some(eqRule) if !isEqualityRule(eqRule) =>
627627- Error(`'${it.equalityName}' is not a valid equality (has variables or premises)`)
628628- | Some(eqRule) =>
629629- switch extractEqualityTerms(eqRule.conclusion) {
630630- | None =>
631631- Error(`Cannot extract equality from '${it.equalityName}' - not in expected equality form`)
632632- | Some((lhs, rhs)) => {
633633- let (from, to) = if Config.reversed {
634634- (rhs, lhs)
635635- } else {
636636- (lhs, rhs)
637637- }
698698+ Error(`'${it.equalityName}' is not a valid equality (has premises)`)
699699+ | Some(eqRule) if Array.length(eqRule.vars) != Array.length(it.instantiation) =>
700700+ Error(`Incorrect number of instantiation arguments for '${it.equalityName}'`)
701701+ | Some(eqRule) => {
702702+ let instantiatedRule = Rule.instantiate(eqRule, it.instantiation)
703703+704704+ switch extractEqualityTermsFromBare(instantiatedRule) {
705705+ | None =>
706706+ Error(`Cannot extract equality from '${it.equalityName}' - not in expected equality form`)
707707+ | Some((lhs, rhs)) => {
708708+ let (from, to) = if Config.reversed {
709709+ (rhs, lhs)
710710+ } else {
711711+ (lhs, rhs)
712712+ }
713713+714714+ // TODO: what gen to use?
715715+ let (_, rewrittenGoal) = rewriteJudgmentTerms(goal, from, to, ~gen=None)
638716639639- let rewrittenGoal = rewriteJudgmentTerms(goal, from, to)
717717+ let rewrittenRule: Rule.t = {
718718+ vars: [],
719719+ premises: [],
720720+ conclusion: rewrittenGoal,
721721+ }
640722641641- let rewrittenRule: Rule.t = {
642642- vars: [],
643643- premises: [],
644644- conclusion: rewrittenGoal,
723723+ Ok({
724724+ equalityName: it.equalityName,
725725+ instantiation: it.instantiation,
726726+ subgoal: f(it.subgoal, rewrittenRule),
727727+ })
645728 }
646646-647647- Ok({
648648- equalityName: it.equalityName,
649649- subgoal: f(it.subgoal, rewrittenRule),
650650- })
651729 }
652730 }
653731 }
654732 }
655733}
656734657657-module Rewrite = (Judgment: JUDGMENT with module Term := HOTerm) => MakeRewriteHOTerm(
735735+module Rewrite = (
736736+ Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
737737+) => MakeRewriteHOTerm(
658738 Judgment,
659739 {
660740 let keyword = "rewrite"
···662742 },
663743)
664744665665-module RewriteReverse = (Judgment: JUDGMENT with module Term := HOTerm) => MakeRewriteHOTerm(
745745+module RewriteReverse = (
746746+ Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
747747+) => MakeRewriteHOTerm(
666748 Judgment,
667749 {
668750 let keyword = "rewrite_reverse"
+6-2
src/MethodView.res
···158158 }
159159}
160160161161-module RewriteView = (Judgment: JUDGMENT with module Term := HOTerm) => {
161161+module RewriteView = (
162162+ Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
163163+) => {
162164 module Method = Rewrite(Judgment)
163165 type props<'a> = {
164166 method: Method.t<'a>,
···197199 }
198200}
199201200200-module RewriteReverseView = (Judgment: JUDGMENT with module Term := HOTerm) => {
202202+module RewriteReverseView = (
203203+ Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t,
204204+) => {
201205 module Method = RewriteReverse(Judgment)
202206 type props<'a> = {
203207 method: Method.t<'a>,
+3-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