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

-----------------------------------------------------------------------------
--- Definition of some names of primitive operations occurring in FlatCurry
--- programs, like arithmetic and relational operators, and their
--- counterparts used in SMT solvers.
---
--- @author  Michael Hanus
--- @version September 2024
---------------------------------------------------------------------------

module FlatCurry.Names2SMT where

----------------------------------------------------------------------------
--- Primitive unary operations of the prelude and their SMT names.
unaryPrimOps :: [(String,String)]
unaryPrimOps =
  [("_impl#negate#Prelude.Num#Prelude.Int#","-")
  ,("_impl#sqrt#Prelude.Floating#Prelude.Float#","sqrt")
  ,("not","not")
  ]

--- Primitive binary operations of the prelude and their SMT names.
binaryPrimOps :: [(String,String)]
binaryPrimOps =
  [("&&","and")
  ,("||","or")
  ,("==","=")
  ,("constrEq","=")
  ,("_impl#==#Prelude.Eq#Prelude.Int#","=")
  ,("_impl#==#Prelude.Eq#Prelude.Float#","=")
  ,("_impl#==#Prelude.Eq#Prelude.Char#","=")
  ,("/=","/=")  -- should be translated as negated '='
  ,("_impl#/=#Prelude.Eq#Prelude.Int#","/=")
  ,("_impl#/=#Prelude.Eq#Prelude.Float#","/=")
  ,("_impl#/=#Prelude.Eq#Prelude.Char#","/=")
  ,("_impl#+#Prelude.Num#Prelude.Int#","+")
  ,("_impl#-#Prelude.Num#Prelude.Int#","-")
  ,("_impl#*#Prelude.Num#Prelude.Int#","*")
  ,("_impl#negate#Prelude.Num#Prelude.Int#","-")
  ,("_impl#div#Prelude.Integral#Prelude.Int#","div")
  ,("_impl#mod#Prelude.Integral#Prelude.Int#","mod")
  ,("_impl#rem#Prelude.Integral#Prelude.Int#","rem")
  ,("_impl#>#Prelude.Ord#Prelude.Int#",">")
  ,("_impl#<#Prelude.Ord#Prelude.Int#","<")
  ,("_impl#>=#Prelude.Ord#Prelude.Int#",">=")
  ,("_impl#<=#Prelude.Ord#Prelude.Int#","<=")
  ,("_impl#+#Prelude.Num#Prelude.Float#","+")
  ,("_impl#-#Prelude.Num#Prelude.Float#","-")
  ,("_impl#*#Prelude.Num#Prelude.Float#","*")
  ,("_impl#/#Prelude.Num#Prelude.Float#","/")
  ,("_impl#>#Prelude.Ord#Prelude.Float#",">")
  ,("_impl#<#Prelude.Ord#Prelude.Float#","<")
  ,("_impl#>=#Prelude.Ord#Prelude.Float#",">=")
  ,("_impl#<=#Prelude.Ord#Prelude.Float#","<=")
  ,("_impl#>#Prelude.Ord#Prelude.Char#",">")
  ,("_impl#<#Prelude.Ord#Prelude.Char#","<")
  ,("_impl#>=#Prelude.Ord#Prelude.Char#",">=")
  ,("_impl#<=#Prelude.Ord#Prelude.Char#","<=")
  ]

----------------------------------------------------------------------------