Lines Matching defs:acc
785 fun funcs (lit,acc) = NameAritySet.union (functionsLiteral lit) acc
792 fun rels (lit,acc) =
794 NONE => acc
795 | SOME r => NameAritySet.add acc r
802 fun fvs (lit,acc) = NameSet.union (freeVarsLiteral lit) acc
1214 fun funcs (fm,acc) = NameAritySet.union (functionsFormula fm) acc
1221 fun rels (fm,acc) = NameAritySet.union (relationsFormula fm) acc
1903 fun addClauses role clauses acc : normalization =
1908 val {problem,sources} : normalization = acc
1952 fun addFofAxiom ((_,fm),acc) =
1953 addFof AxiomRole (Normalize.mkAxiom fm, acc);
1968 fun splitProblem acc =
1976 val acc = addFof NegatedConjectureRole (th,acc)
1978 normProblem (subgoal,parents) acc
2034 val acc = (initialNormalization, Normalize.initialCnf)
2035 val acc = List.foldl addCnfAxiom acc cnfAxioms
2036 val acc = List.foldl addFofAxiom acc fofAxioms
2039 NoGoal => [normProblemFalse acc]
2040 | CnfGoal cls => [normProblemFalse (List.foldl addCnfGoal acc cls)]
2041 | FofGoal goals => splitProblem acc goals
2052 fun stripLineComments acc strm =
2054 Stream.Nil => (List.rev acc, Stream.Nil)
2057 SOME s => stripLineComments (s :: acc) (rest ())
2058 | NONE => (List.rev acc, Stream.filter (not o isLineComment) strm);
2405 fun addNormalizeFormula avoid prefix ((fm,inf,fms),acc) =
2407 val (formulas,i,fmNames) = acc
2441 fun addProofFormula avoid sources fmNames prefix ((th,inf),acc) =
2443 val (formulas,i,clNames) = acc