b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# main entry point of the strategy.
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# Here, the Haskell reductions (all ending in Reduction) are called, that _must_ be called in this order, since there are some dependencies.
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The HaskellSplit processor takes the set of start terms and makes multiple problems with one start term each.
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The HaskellNarrowing processor is the core of the termination proof: It applies evaluations to the start term, looking for
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# loops in the call structure. Here the Haskell lazy evaluation, (type) case splitting, and generalizations are performed.
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The last command, mainQDP, calls the subfunction declared later; this will work on the DP Problems generated by the HaskellNarrowing processor
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liumain = HaskellLambdaReduction:HaskellCaseReduction:HaskellIfReduction:HaskellIrrPatReduction:HaskellBindingReduction:HaskellCondReduction:HaskellNewTypeReduction:HaskellIrrPatReduction:HaskellLetReduction:HaskellNumReduction:HaskellSplit:HaskellNarrowing[AddTypes = False]:workOnQDP
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# subfunction workOnQDP
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# Here, the processors QDPDependencyGraph, QDPATransformaion, QDPSizeChange (in different configurations),
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# the subfunction parallel, and QDPPolo are called in the order listed. The first one to succeed
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# is taken (because of the keyword First) and the process is started over (because of the keyword Repeat).
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The arguments 0,* of Repeat mean that as long as there is one processor inside the First that succeeds, try again
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The QDPDependencyGraph processor looks at the DP problem and builds a new estimation of the Dependency Graph
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The QDPATransformation processor can transform a non-higher-order program into standard form (eliminating the app-symbol)
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The QDPSizeChange processor looks for decreases in the term structure
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# The QDPPolo processor searches for a polynomial ordering such that all left hand sides are greater or equal than right hand sides
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# and removes the strictly ordered ones. The coefficients are from range {0,1,2}, the maximum degree is 1 and argument filterings are
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# considered when looking for usable rules
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi LiuworkOnQDP = RepeatS(0,*,First(QDPDependencyGraph, QDPATransformation, QDPSizeChange[Subterm=True], QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=0,AfsRestriction=2], parallel,QDPPolo[Range=2,Degree=1,Active=True]))
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# subfunction parallel
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# tries in parallel the Size Change and RuleRemoval processors for a maximum of 5000 ms
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# thereafter, a polynomial ordering is searched, where the coefficients are from the
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# range {0,1}, maximum degree is 1, and if there is an argument filtering, take this into
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liu# account when searching for usable rules
b25d85bf345ca7bf9dd626e1032048458db74f3cMingyi Liuparallel = First(Timer(5000,Any(QDPSizeChange[Subterm=False,Range=1,UsableArgumentsRestriction=2,AfsRestriction=2], QDPRuleRemoval[Range=2])), Timer(30000,QDPPolo[Range=1,Degree=1,Active=True]))