1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72

--- --------------------------------------------------------------------------
--- This module defines some configuration options for the partial evaluator.
--- It is to shared by the partial evaluator itself and the test driver
--- to allow some reuse of option parsing.
---
--- @author  Björn Peemöller
--- @version April 2015
--- --------------------------------------------------------------------------
module Configuration where

--- Mode to control coloring of output.
--- @cons CMAlways - Always color the output.
--- @cons CMAuto   - Only color when stdout is connected to a terminal
--- @cons CMNever  - Never color the output.
data ColorMode = CMAlways | CMAuto | CMNever
 deriving Eq

--- Description and flag of coloring modes
colorModes :: [(ColorMode, String, String)]
colorModes =
  [ (CMAlways, "always", "Always color the output"                          )
  , (CMAuto  , "auto"  , "Only color when stdout is connected to a terminal")
  , (CMNever , "never" , "Never color the output"                           )
  ]

--- Semantics used for unfolding.
--- @cons RLNT         - see paper xxx
--- @cons Natural      - see paper yyy
--- @cons LetRewriting - see paper zzz
data Semantics = RLNT | Natural | LetRW
  deriving (Eq,Show)

--- Description and flag of optimization levels
semantics :: [(Semantics, String, String)]
semantics =
  [ (RLNT   , "rlnt"   , "RLNT semantics"   )
  , (Natural, "natural", "Natural semantics")
  , (LetRW  , "letrw"  , "Let rewriting"    )
  ]

--- Kind of abstraction operator.
--- @cons None - no generalization (termination is not ensured).
--- @cons WFO  - generalization based on a well-founded order
---              (termination ensured).
--- @cons WQO  - generalization based on a well-quasi order.
---              Termination is ensured even for integers by
---              translating them to expressions.
--- Note that only None and WQO really pass the "KMP-test".
data Abstraction = None | WFO | WQO
 deriving (Eq,Show)

--- Description and flag of abstractions
abstractions :: [(Abstraction, String, String)]
abstractions =
  [ (None, "none", "no generalization (termination is not ensured)")
  , (WFO , "wfo" , "generalization based on a well-founded order"  )
  , (WQO , "wqo" , "generalization based on a well-quasi order"    )
  ]

--- Mode to control function unfolding.
--- @cons One  - Unfold only one function call at all
--- @cons Each - Unfold only one call for each function
--- @cons All  - Unfold all function calls, may not terminate!
data ProceedMode = PMNone | PMOne | PMEach | PMAll

--- Description and flag of optimization levels
proceedModes :: [(ProceedMode, String, String)]
proceedModes =
  [ (PMOne , "one" , "Perform only one unfolding"               )
  , (PMEach, "each", "Perform one unfolding for each function"  )
  , (PMAll , "all" , "Perform all unfoldings, may not terminate")
  ]