1structure fracSyntax :> fracSyntax =
2struct
3
4open HolKernel boolLib Parse;
5
6(* interactive mode
7app load ["fracTheory"];
8*)
9
10open fracTheory;
11
12
13val ERR = mk_HOL_ERR "fracSyntax";
14
15(*--------------------------------------------------------------------------*
16 * constants
17 *--------------------------------------------------------------------------*)
18
19val int_ty = intSyntax.int_ty;
20val frac = mk_thy_type{Tyop = "frac", Thy="frac", Args = []};
21
22val frac_0_tm = prim_mk_const {Name="frac_0",Thy="frac"};
23val frac_1_tm = prim_mk_const {Name="frac_1",Thy="frac"};
24
25val frac_nmr_tm = prim_mk_const {Name="frac_nmr",Thy="frac"};
26val frac_dnm_tm = prim_mk_const {Name="frac_dnm",Thy="frac"};
27val frac_sgn_tm = prim_mk_const {Name="frac_sgn",Thy="frac"};
28
29val frac_ainv_tm = prim_mk_const {Name="frac_ainv",Thy="frac"};
30val frac_minv_tm = prim_mk_const {Name="frac_minv",Thy="frac"};
31
32val frac_add_tm = prim_mk_const {Name="frac_add",Thy="frac"};
33val frac_sub_tm = prim_mk_const {Name="frac_sub",Thy="frac"};
34val frac_mul_tm = prim_mk_const {Name="frac_mul",Thy="frac"};
35val frac_div_tm = prim_mk_const {Name="frac_div",Thy="frac"};
36
37val frac_save_tm = prim_mk_const {Name="frac_save",Thy="frac"};
38
39(*--------------------------------------------------------------------------*
40 * constructors
41 *--------------------------------------------------------------------------*)
42
43fun mk_monop c tm = mk_comb(c,tm);
44fun mk_binop c (tm1,tm2) = mk_comb(mk_comb(c,tm1),tm2);
45
46val mk_frac_nmr = mk_monop frac_nmr_tm;
47val mk_frac_dnm = mk_monop frac_dnm_tm;
48val mk_frac_sgn = mk_monop frac_sgn_tm;
49
50val mk_frac_ainv = mk_monop frac_ainv_tm;
51val mk_frac_minv = mk_monop frac_minv_tm;
52
53val mk_frac_add = mk_binop frac_add_tm;
54val mk_frac_sub = mk_binop frac_sub_tm;
55val mk_frac_mul = mk_binop frac_mul_tm;
56val mk_frac_div = mk_binop frac_div_tm;
57
58val mk_frac_save = mk_binop frac_save_tm;
59
60(*--------------------------------------------------------------------------*
61 * destructors
62 *--------------------------------------------------------------------------*)
63
64val dest_frac_nmr = dest_monop frac_nmr_tm (ERR "dest_frac_nmr" "");
65val dest_frac_dnm = dest_monop frac_dnm_tm (ERR "dest_frac_dnm" "");
66val dest_frac_sgn = dest_monop frac_sgn_tm (ERR "dest_frac_sgn" "");
67
68val dest_frac_ainv = dest_monop frac_ainv_tm (ERR "dest_frac_ainv" "");
69val dest_frac_minv = dest_monop frac_minv_tm (ERR "dest_frac_minv" "");
70
71val dest_frac_add = dest_binop frac_add_tm (ERR "dest_frac_add" "");
72val dest_frac_sub = dest_binop frac_sub_tm (ERR "dest_frac_sub" "");
73val dest_frac_mul = dest_binop frac_mul_tm (ERR "dest_frac_mul" "");
74val dest_frac_div = dest_binop frac_div_tm (ERR "dest_frac_div" "");
75
76val dest_frac_save = dest_binop frac_save_tm (ERR "dest_frac_save" "");
77
78(*--------------------------------------------------------------------------*
79 * query operations
80 *--------------------------------------------------------------------------*)
81
82val is_frac_nmr = can dest_frac_nmr;
83val is_frac_dnm = can dest_frac_dnm;
84val is_frac_sgn = can dest_frac_sgn;
85
86val is_frac_ainv = can dest_frac_ainv;
87val is_frac_minv = can dest_frac_minv;
88
89val is_frac_add = can dest_frac_add;
90val is_frac_sub = can dest_frac_sub;
91val is_frac_mul = can dest_frac_mul;
92val is_frac_div = can dest_frac_div;
93
94val is_frac_save = can dest_frac_save;
95
96(*==========================================================================
97 * end of structure
98 *==========================================================================*)
99end;
100