-
Notifications
You must be signed in to change notification settings - Fork 81
/
transcLangScript.sml
134 lines (117 loc) · 2.65 KB
/
transcLangScript.sml
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
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
(**
Define a simple "language" for describing elementary
functions. For now we only allow combinations, i.e.
exp (sin (cos ...) but no additional operators like +,-,*,/
**)
open realPolyTheory;
open preambleDandelion;
val _ = new_theory "transcLang";
val _ = monadsyntax.enable_monadsyntax();
val _ = monadsyntax.enable_monad "option";
Datatype:
binop = Add | Sub | Mul | Div
End
Datatype:
unop = Neg | Inv
End
(* Log = natural logarithm *)
Datatype:
trFun = Exp | Sin | Cos | Tan | Atn | Sqrt | Log
End
Datatype:
transc =
Fun trFun transc
| Poly poly transc
| Bop binop transc transc
| Uop unop transc
| Cst real
| Var string
End
Datatype:
approxAnn =
FunAnn 'a trFun approxAnn
| PolyAnn 'a poly approxAnn
| BopAnn 'a binop approxAnn approxAnn
| UopAnn 'a unop approxAnn
| CstAnn 'a real
| VarAnn 'a string
End
Definition getAnn_def:
getAnn (FunAnn a _ _) = a ∧
getAnn (PolyAnn a _ _) = a ∧
getAnn (BopAnn a _ _ _) = a ∧
getAnn (UopAnn a _ _) = a ∧
getAnn (CstAnn a _) = a ∧
getAnn (VarAnn a _) = a
End
Definition erase_def:
erase (FunAnn _ f e) = Fun f (erase e) ∧
erase (PolyAnn _ p e) = Poly p (erase e) ∧
erase (BopAnn _ b e1 e2) = Bop b (erase e1) (erase e2) ∧
erase (UopAnn _ u e) = Uop u (erase e) ∧
erase (CstAnn _ r) = Cst r ∧
erase (VarAnn _ s) = Var s
End
Definition getFun_def:
getFun Exp = exp ∧
getFun Sin = sin ∧
getFun Cos = cos ∧
getFun Tan = tan ∧
getFun Atn = atn ∧
getFun Sqrt = sqrt ∧
getFun Log = ln
End
Definition appUop_def:
appUop Neg r = - r ∧
appUop Inv r = inv r
End
Definition appBop_def:
appBop Add = realax$real_add ∧
appBop Sub = $- ∧
appBop Mul = $* ∧
appBop Div = $/
End
Definition interp_def:
interp (Var x) env =
do v <- FIND (λ (y,r). y = x) env;
return (SND v);
od ∧
interp (Cst c) env = SOME c ∧
interp (Uop uop t) env =
do
r <- interp t env;
assert (uop = Inv ⇒ r ≠ 0);
return (appUop uop r)
od ∧
interp (Bop bop t1 t2) env =
do
r1 <- interp t1 env;
r2 <- interp t2 env;
assert (bop = Div ⇒ r2 ≠ 0);
return (appBop bop r1 r2);
od ∧
interp (Fun s t) env =
do
r <- interp t env;
return ((getFun s) r);
od ∧
interp (Poly p t) env =
do
r <- interp t env;
return (evalPoly p r)
od
End
Datatype:
transcProg =
Let string transc transcProg
| Ret transc
End
Definition interpProg_def:
interpProg (Let x e p) env =
do
r <- interp e env;
interpProg p ((x, r)::env)
od ∧
interpProg (Ret e) env = interp e env
End
val _ = export_theory();