1structure integer_wordSyntax :> integer_wordSyntax = 2struct 3 4open HolKernel boolLib 5open wordsSyntax integer_wordTheory 6 7val ERR = Feedback.mk_HOL_ERR "integer_wordSyntax" 8 9fun syntax_fns n d m = 10 HolKernel.syntax_fns {n = n, dest = d, make = m} "integer_word" 11 12(*------------------------------------------------------------------------- *) 13 14val s = HolKernel.syntax_fns1 "integer_word" 15 16val (toString_tm, mk_toString, dest_toString, is_toString) = s "toString" 17 18val (fromString_tm, mk_fromString, dest_fromString, is_fromString) = 19 s "fromString" 20 21val (w2i_tm, mk_w2i, dest_w2i, is_w2i) = s "w2i" 22 23(* - - - - - - - - - - - - - - - - - - - - - - - *) 24 25val s = syntax_fns 1 26 (fn tm1 => fn e => boolSyntax.dest_itself o HolKernel.dest_monop tm1 e) 27 (fn tm => fn ty => 28 Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, boolSyntax.mk_itself ty)) 29 30val (int_min_tm, mk_int_min, dest_int_min, is_int_min) = s "INT_MIN" 31val (int_max_tm, mk_int_max, dest_int_max, is_int_max) = s "INT_MAX" 32val (uint_max_tm, mk_uint_max, dest_uint_max, is_uint_max) = s "UINT_MAX" 33 34(* - - - - - - - - - - - - - - - - - - - - - - - *) 35 36val s = syntax_fns 1 37 (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w)) 38 (fn tm => fn (w, ty) => Term.mk_comb (Term.inst [Type.alpha |-> ty] tm, w)) 39 40val (i2w_tm, mk_i2w, dest_i2w, is_i2w) = s "i2w" 41 42val (saturate_i2sw_tm, mk_saturate_i2sw, 43 dest_saturate_i2sw, is_saturate_i2sw) = s "saturate_i2sw" 44 45val (saturate_i2w_tm, mk_saturate_i2w, dest_saturate_i2w, is_saturate_i2w) = 46 s "saturate_i2w" 47 48(* - - - - - - - - - - - - - - - - - - - - - - - *) 49 50val s = syntax_fns 1 51 (fn tm1 => fn e => fn w => (HolKernel.dest_monop tm1 e w, dim_of w)) 52 (fn tm => fn (w, ty) => 53 Term.mk_comb (Term.inst [Type.alpha |-> wordsSyntax.dim_of w, 54 Type.beta |-> ty] tm, w)) 55 56val (saturate_sw2sw_tm, mk_saturate_sw2sw, 57 dest_saturate_sw2sw, is_saturate_sw2sw) = s "saturate_sw2sw" 58 59val (saturate_sw2w_tm, mk_saturate_sw2w, 60 dest_saturate_sw2w, is_saturate_sw2w) = s "saturate_sw2w" 61 62val (saturate_w2sw_tm, mk_saturate_w2sw, 63 dest_saturate_w2sw, is_saturate_w2sw) = s "saturate_w2sw" 64 65(* - - - - - - - - - - - - - - - - - - - - - - - *) 66 67val s = HolKernel.syntax_fns2 "integer_word" 68 69val (signed_saturate_add_tm, mk_signed_saturate_add, 70 dest_signed_saturate_add, is_signed_saturate_add) = s "signed_saturate_add" 71 72val (signed_saturate_sub_tm, mk_signed_saturate_sub, 73 dest_signed_saturate_sub, is_signed_saturate_sub) = s "signed_saturate_sub" 74 75val (word_sdiv_tm, mk_word_sdiv, dest_word_sdiv, is_word_sdiv) = s "word_sdiv" 76val (word_smod_tm, mk_word_smod, dest_word_smod, is_word_smod) = s "word_smod" 77 78(*------------------------------------------------------------------------- *) 79 80end 81