1\DOC
2
3\TYPE {syntax_fns : {dest: term -> exn -> term -> 'a, make: term -> 'b -> term, n: int} -> string -> string ->
4             term * ('b -> term) * (term -> 'a) * (term -> bool)}
5
6\SYNOPSIS
7Helps in providing syntax support for theory constants.
8
9\KEYWORDS
10Syntax.
11
12\DESCRIBE
13{syntax_fns syntax thy name} returns a 4-tuple, consisting of: a term, a term destructor function, a term constructor function and a term recogniser function. These provide syntax support for operation {name} from theory {thy}. The record argument {syntax} consists of {dest: term -> exn -> term -> 'a} and {make: term -> 'b -> term} functions, together with an "expected arity" value {n}.
14Through a sequence of instantiations, the {syntax_fns} function can be used to quickly and reliably write a {thySyntax.sml} file.
15
16\EXAMPLE
17
18To provide syntax support for unary operations from the theory {num}, one can use the following function:
19{
20> val num1 = HolKernel.syntax_fns {n = 1, make = HolKernel.mk_monop, dest = HolKernel.dest_monop} "num";
21val num1 = fn:
22   string -> term * (term -> term) * (term -> term) * (term -> bool)
23}
24The following call then provides support for the {SUC} constant:
25{
26> val (suc_tm, mk_suc, dest_suc, is_suc) = num1 "SUC";
27val dest_suc = fn: term -> term
28val is_suc = fn: term -> bool
29val mk_suc = fn: term -> term
30val suc_tm = ``SUC``: term
31}
32A {SUC} term can be constructed with
33{
34> val tm = mk_suc ``4n``;
35val tm = ``SUC 4``: term
36}
37The resulting term {tm} can be identified and destructed as follows:
38{
39> is_suc tm;
40val it = true: bool
41> val v = dest_suc tm;
42val v = ``4``: term
43}
44A standard error message is raised when {dest_suc} fails, e.g.
45{
46> is_suc ``SUC``;
47val it = false: bool
48> val v = dest_suc ``SUC``;
49Exception-
50   HOL_ERR
51     {message = "", origin_function = "dest_SUC", origin_structure =
52     "numSyntax"} raised
53}
54
55The value {n} in the call to {syntax_fns} acts purely as a sanity check. For example, the following fails because {SUC} is not a binary operation:
56{
57> HolKernel.syntax_fns {n = 2, make = HolKernel.mk_binop, dest = HolKernel.dest_binop} "num" "SUC";
58Exception-
59   HOL_ERR
60     {message = "bad number of arguments", origin_function = "systax_fns",
61       origin_structure = "numSyntax"} raised
62}
63Typically, the {dest} and {make} functions will be complementary (with type variables {'a} and {'b} being the same), however this need not be the case. Advanced uses of {syntax_fns} can take types into consideration. For example, the constant {bitstring$v2w} with type {bitstring->'a word} is supported as follows:
64{
65> val tm = bitstringSyntax.mk_v2w (``l:bitstring``, ``:32``);
66val tm = ``v2w l``: term
67> type_of tm;
68val it = ``:word32``: hol_type
69> bitstringSyntax.dest_v2w tm;
70val it = (``l``, ``:32``): term * hol_type
71}
72This is implemented as follows:
73{
74val (v2w_tm, mk_v2w, dest_v2w, is_v2w) =
75   HolKernel.syntax_fns
76     {n = 1,
77      dest = fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, wordsSyntax.dim_of w),
78      make = fn tm => fn (v, ty) => Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, v)}
79     "bitstring" "v2w"
80}
81
82\ENDDOC
83