c-semantics/semantics/c/library/math.k at master · kframework/c-semantics · GitHub

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
module LIBC-MATH
     imports C-CONVERSION-SYNTAX
     imports C-DYNAMIC-SYNTAX
     imports C-TYPING-SYNTAX
     imports FLOAT
     imports LIBC-BUILTIN-SYNTAX

     rule [sqrt]:
          builtin("sqrt", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), sqrtFloat(F))
          [structural]

     rule [log]:
          builtin("log", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), logFloat(F))
          [structural]

     rule [exp]:
          builtin("exp", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), expFloat(F))
          [structural]

     rule [atan]:
          builtin("atan", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), atanFloat(F))
          [structural]

     rule [asin]:
          builtin("asin", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), asinFloat(F))
          [structural]

     rule [atan2]:
          builtin("atan2", tv(F:Float, ut(_, double)), tv(F':Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), atan2Float(F, F'))
          [structural]

     rule [tan]:
          builtin("tan", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), tanFloat(F))
          [structural]

     rule [floor]:
          builtin("floor", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), floorFloat(F))
          [structural]

     rule [cos]:
          builtin("cos", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), cosFloat(F))
          [structural]

     rule [fmod]:
          builtin("fmod", tv(F:Float, ut(_, double)), tv(F':Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), F %Float F')
          [structural]

     rule [sin]:
          builtin("sin", tv(F:Float, ut(_, double)))
          => floatArithInterpret(ut(.Set, double), sinFloat(F))
          [structural]

endmodule