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