762 in if nG aconv G then (changed, (G,md)::pairs) |
761 in if nG aconv G then (changed, (G,md)::pairs) |
763 else ((nG,md)::changed, pairs) |
762 else ((nG,md)::changed, pairs) |
764 end |
763 end |
765 (*substitute throughout "stack frame"; extract affected formulae*) |
764 (*substitute throughout "stack frame"; extract affected formulae*) |
766 fun subFrame ((Gs,Hs), (changed, frames)) = |
765 fun subFrame ((Gs,Hs), (changed, frames)) = |
767 let val (changed', Gs') = foldr subForm (changed, []) Gs |
766 let val (changed', Gs') = List.foldr subForm (changed, []) Gs |
768 val (changed'', Hs') = foldr subForm (changed', []) Hs |
767 val (changed'', Hs') = List.foldr subForm (changed', []) Hs |
769 in (changed'', (Gs',Hs')::frames) end |
768 in (changed'', (Gs',Hs')::frames) end |
770 (*substitute throughout literals; extract affected ones*) |
769 (*substitute throughout literals; extract affected ones*) |
771 fun subLit (lit, (changed, nlits)) = |
770 fun subLit (lit, (changed, nlits)) = |
772 let val nlit = subst lit |
771 let val nlit = subst lit |
773 in if nlit aconv lit then (changed, nlit::nlits) |
772 in if nlit aconv lit then (changed, nlit::nlits) |
774 else ((nlit,true)::changed, nlits) |
773 else ((nlit,true)::changed, nlits) |
775 end |
774 end |
776 val (changed, lits') = foldr subLit ([], []) lits |
775 val (changed, lits') = List.foldr subLit ([], []) lits |
777 val (changed', pairs') = foldr subFrame (changed, []) pairs |
776 val (changed', pairs') = List.foldr subFrame (changed, []) pairs |
778 in if !trace then writeln ("Substituting " ^ traceTerm thy u ^ |
777 in if !trace then writeln ("Substituting " ^ traceTerm thy u ^ |
779 " for " ^ traceTerm thy t ^ " in branch" ) |
778 " for " ^ traceTerm thy t ^ " in branch" ) |
780 else (); |
779 else (); |
781 {pairs = (changed',[])::pairs', (*affected formulas, and others*) |
780 {pairs = (changed',[])::pairs', (*affected formulas, and others*) |
782 lits = lits', (*unaffected literals*) |
781 lits = lits', (*unaffected literals*) |
911 | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us; |
910 | matchs (t :: ts) (u :: us) = match t u andalso matchs ts us; |
912 |
911 |
913 |
912 |
914 fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = |
913 fun printStats (State {ntried, nclosed, ...}) (b, start, tacs) = |
915 if b then |
914 if b then |
916 writeln (end_timing start ^ " for search. Closed: " |
915 writeln (#message (end_timing start) ^ " for search. Closed: " |
917 ^ Int.toString (!nclosed) ^ |
916 ^ Int.toString (!nclosed) ^ |
918 " tried: " ^ Int.toString (!ntried) ^ |
917 " tried: " ^ Int.toString (!ntried) ^ |
919 " tactics: " ^ Int.toString (length tacs)) |
918 " tactics: " ^ Int.toString (length tacs)) |
920 else (); |
919 else (); |
921 |
920 |
969 let val updated = ntrl < !ntrail (*branch updated*) |
968 let val updated = ntrl < !ntrail (*branch updated*) |
970 val lim' = if updated |
969 val lim' = if updated |
971 then lim - (1+log(length rules)) |
970 then lim - (1+log(length rules)) |
972 else lim (*discourage branching updates*) |
971 else lim (*discourage branching updates*) |
973 val vars = vars_in_vars vars |
972 val vars = vars_in_vars vars |
974 val vars' = foldr add_terms_vars vars prems |
973 val vars' = List.foldr add_terms_vars vars prems |
975 val choices' = (ntrl, nbrs, PRV) :: choices |
974 val choices' = (ntrl, nbrs, PRV) :: choices |
976 val tacs' = (tac(updated,false,true)) |
975 val tacs' = (tac(updated,false,true)) |
977 :: tacs (*no duplication; rotate*) |
976 :: tacs (*no duplication; rotate*) |
978 in |
977 in |
979 traceNew prems; traceVars state ntrl; |
978 traceNew prems; traceVars state ntrl; |
1096 | deeper (((P,prems),tac)::grls) = |
1095 | deeper (((P,prems),tac)::grls) = |
1097 if unify state (add_term_vars(P,[]), P, H) |
1096 if unify state (add_term_vars(P,[]), P, H) |
1098 then |
1097 then |
1099 let val updated = ntrl < !ntrail (*branch updated*) |
1098 let val updated = ntrl < !ntrail (*branch updated*) |
1100 val vars = vars_in_vars vars |
1099 val vars = vars_in_vars vars |
1101 val vars' = foldr add_terms_vars vars prems |
1100 val vars' = List.foldr add_terms_vars vars prems |
1102 (*duplicate H if md permits*) |
1101 (*duplicate H if md permits*) |
1103 val dup = md (*earlier had "andalso vars' <> vars": |
1102 val dup = md (*earlier had "andalso vars' <> vars": |
1104 duplicate only if the subgoal has new vars*) |
1103 duplicate only if the subgoal has new vars*) |
1105 (*any instances of P in the subgoals? |
1104 (*any instances of P in the subgoals? |
1106 NB: boolean "recur" affects tracing only!*) |
1105 NB: boolean "recur" affects tracing only!*) |
1262 Int.toString lim); |
1261 Int.toString lim); |
1263 if !trace then error "************************\n" |
1262 if !trace then error "************************\n" |
1264 else (); |
1263 else (); |
1265 backtrack choices) |
1264 backtrack choices) |
1266 | cell => (if (!trace orelse !stats) |
1265 | cell => (if (!trace orelse !stats) |
1267 then writeln (end_timing start ^ " for reconstruction") |
1266 then writeln (#message (end_timing start) ^ " for reconstruction") |
1268 else (); |
1267 else (); |
1269 Seq.make(fn()=> cell)) |
1268 Seq.make(fn()=> cell)) |
1270 end |
1269 end |
1271 in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end |
1270 in prove (state, start, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) end |
1272 handle PROVE => Seq.empty |
1271 handle PROVE => Seq.empty |