Jordan/parse_ext_override_interface.ml

   1 (*
   2         Author: Thomas C. Hales
   3
   4         As a new user of HOL-light, I have had a difficult time distinguishing
   5         between the different uses of overloaded operators such as
   6         (+), ( * ), (abs) (&), and so forth.
   7
   8         Their interpretation is context dependent, according to which of
   9         prioritize_num, prioritize_int, and prioritize_real was most
  10         recently called.
  11
  12         This file removes all ambiguities in notation.
  13         Following the usage of CAML, we append a dot to operations on real
  14         numbers so that addition is (+.), etc.
  15
  16         In the same way, we remove ambiguities between natural numbers and
  17         integers by appending a character.  We have chosen to use
  18         the character `|` for natural number operations
  19         and the character `:` for integer operations.
  20
  21         The character `&` continues to denote the embedding of
  22         natural numbers into the integers or reals.
  23
  24         HOL-light parsing does not permit an operator mixing alphanumeric
  25         characters with symbols.  Thus, we were not able to use (abs.)
  26         and (abs:) for the absolute value.  Instead we adapt the usual notation
  27         |x| for absolute value and write it in prefix notation ||: and
  28         ||. for the integer and real absolute value functions respectively.
  29
  30         In deference to HOL-light notation, we use ** for the exponential
  31         function.  There are three versions: ( **| ), ( **: ), and ( **. ).
  32
  33 *)
  34
  35 (* natural number operations *)
  36
  37
  38
  39 let unambiguous_interface() =
  40 parse_as_infix("+|",(16,"right"));
  41 parse_as_infix("-|",(18,"left"));
  42 parse_as_infix("*|",(20,"right"));
  43 parse_as_infix("**|",(24,"left")); (* EXP *)
  44 parse_as_infix("/|",(22,"right")); (* DIV *)
  45 parse_as_infix("%|",(22,"left"));  (* MOD *)
  46 parse_as_infix("<|",(12,"right"));
  47 parse_as_infix("<=|",(12,"right"));
  48 parse_as_infix(">|",(12,"right"));
  49 parse_as_infix(">=|",(12,"right"));
  50 override_interface("+|",`(+):num->(num->num)`);
  51 override_interface("-|",`(-):num->(num->num)`);
  52 override_interface("*|",`( * ):num->(num->num)`);
  53 override_interface("**|",`(EXP):num->(num->num)`);
  54 override_interface("/|",`(DIV):num->(num->num)`);
  55 override_interface("%|",`(MOD):num->(num->num)`);
  56 override_interface("<|",`(<):num->(num->bool)`);
  57 override_interface("<=|",`(<=):num->(num->bool)`);
  58 override_interface(">|",`(>):num->(num->bool)`);
  59 override_interface(">=|",`(>=):num->(num->bool)`);
  60 (* integer operations *)
  61 parse_as_infix("+:",(16,"right"));
  62 parse_as_infix("-:",(18,"left"));
  63 parse_as_infix("*:",(20,"right"));
  64 parse_as_infix("**:",(24,"left"));
  65 parse_as_infix("<:",(12,"right"));
  66 parse_as_infix("<=:",(12,"right"));
  67 parse_as_infix(">:",(12,"right"));
  68 parse_as_infix(">=:",(12,"right"));
  69 override_interface("+:",`int_add:int->int->int`);
  70 override_interface("-:",`int_sub:int->int->int`);
  71 override_interface("*:",`int_mul:int->int->int`);
  72 override_interface("**:",`int_pow:int->num->int`);
  73 (* boolean *)
  74 override_interface("<:",`int_lt:int->int->bool`);
  75 override_interface("<=:",`int_le:int->int->bool`);
  76 override_interface(">:",`int_gt:int->int->bool`);
  77 override_interface(">=:",`int_ge:int->int->bool`);
  78 (* unary *)
  79 override_interface("--:",`int_neg:int->int`);
  80 override_interface("&:",`int_of_num:num->int`);
  81 override_interface("||:",`int_abs:int->int`);
  82 (* real number operations *)
  83 parse_as_infix("+.",(16,"right"));
  84 parse_as_infix("-.",(18,"left"));
  85 parse_as_infix("*.",(20,"right"));
  86 parse_as_infix("**.",(24,"left"));
  87 parse_as_infix("<.",(12,"right"));
  88 parse_as_infix("<=.",(12,"right"));
  89 parse_as_infix(">.",(12,"right"));
  90 parse_as_infix(">=.",(12,"right"));
  91 override_interface("+.",`real_add:real->real->real`);
  92 override_interface("-.",`real_sub:real->real->real`);
  93 override_interface("*.",`real_mul:real->real->real`);
  94 override_interface("**.",`real_pow:real->num->real`);
  95 (* boolean *)
  96 override_interface("<.",`real_lt:real->real->bool`);
  97 override_interface("<=.",`real_le:real->real->bool`);
  98 override_interface(">.",`real_gt:real->real->bool`);
  99 override_interface(">=.",`real_ge:real->real->bool`);
 100 (* unary *)
 101 override_interface("--.",`real_neg:real->real`);
 102 override_interface("&.",`real_of_num:num->real`);
 103 override_interface("||.",`real_abs:real->real`);;
 104
 105 let ambiguous_interface() =
 106 reduce_interface("+|",`(+):num->(num->num)`);
 107 reduce_interface("-|",`(-):num->(num->num)`);
 108 reduce_interface("*|",`( * ):num->(num->num)`);
 109 reduce_interface("**|",`(EXP):num->(num->num)`);
 110 reduce_interface("/|",`(DIV):num->(num->num)`);
 111 reduce_interface("%|",`(MOD):num->(num->num)`);
 112 reduce_interface("<|",`(<):num->(num->bool)`);
 113 reduce_interface("<=|",`(<=):num->(num->bool)`);
 114 reduce_interface(">|",`(>):num->(num->bool)`);
 115 reduce_interface(">=|",`(>=):num->(num->bool)`);
 116 (* integer operations *)
 117 reduce_interface("+:",`int_add:int->int->int`);
 118 reduce_interface("-:",`int_sub:int->int->int`);
 119 reduce_interface("*:",`int_mul:int->int->int`);
 120 reduce_interface("**:",`int_pow:int->num->int`);
 121 (* boolean *)
 122 reduce_interface("<:",`int_lt:int->int->bool`);
 123 reduce_interface("<=:",`int_le:int->int->bool`);
 124 reduce_interface(">:",`int_gt:int->int->bool`);
 125 reduce_interface(">=:",`int_ge:int->int->bool`);
 126 (* unary *)
 127 reduce_interface("--:",`int_neg:int->int`);
 128 reduce_interface("&:",`int_of_num:num->int`);
 129 reduce_interface("||:",`int_abs:int->int`);
 130 (* real *)
 131 reduce_interface("+.",`real_add:real->real->real`);
 132 reduce_interface("-.",`real_sub:real->real->real`);
 133 reduce_interface("*.",`real_mul:real->real->real`);
 134 reduce_interface("**.",`real_pow:real->num->real`);
 135 (* boolean *)
 136 reduce_interface("<.",`real_lt:real->real->bool`);
 137 reduce_interface("<=.",`real_le:real->real->bool`);
 138 reduce_interface(">.",`real_gt:real->real->bool`);
 139 reduce_interface(">=.",`real_ge:real->real->bool`);
 140 (* unary *)
 141 reduce_interface("--.",`real_neg:real->real`);
 142 reduce_interface("&.",`real_of_num:num->real`);
 143 reduce_interface("||.",`real_abs:real->real`);;
 144
 145 (* add to Harrison's priorities the functions pop_priority and get_priority *)
 146 let prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority =
 147   let v = ref ([]:string list) in
 148   let prioritize_int() =
 149   v:= "int"::!v;
 150   overload_interface ("+",`int_add:int->int->int`);
 151   overload_interface ("-",`int_sub:int->int->int`);
 152   overload_interface ("*",`int_mul:int->int->int`);
 153   overload_interface ("<",`int_lt:int->int->bool`);
 154   overload_interface ("<=",`int_le:int->int->bool`);
 155   overload_interface (">",`int_gt:int->int->bool`);
 156   overload_interface (">=",`int_ge:int->int->bool`);
 157   overload_interface ("--",`int_neg:int->int`);
 158   overload_interface ("pow",`int_pow:int->num->int`);
 159   overload_interface ("abs",`int_abs:int->int`);
 160   override_interface ("&",`int_of_num:num->int`) and
 161   prioritize_num() =
 162   v:= "num"::!v;
 163   overload_interface ("+",`(+):num->num->num`);
 164   overload_interface ("-",`(-):num->num->num`);
 165   overload_interface ("*",`(*):num->num->num`);
 166   overload_interface ("<",`(<):num->num->bool`);
 167   overload_interface ("<=",`(<=):num->num->bool`);
 168   overload_interface (">",`(>):num->num->bool`);
 169   overload_interface (">=",`(>=):num->num->bool`) and
 170   prioritize_real() =
 171   v:= "real"::!v;
 172   overload_interface ("+",`real_add:real->real->real`);
 173   overload_interface ("-",`real_sub:real->real->real`);
 174   overload_interface ("*",`real_mul:real->real->real`);
 175   overload_interface ("/",`real_div:real->real->real`);
 176   overload_interface ("<",`real_lt:real->real->bool`);
 177   overload_interface ("<=",`real_le:real->real->bool`);
 178   overload_interface (">",`real_gt:real->real->bool`);
 179   overload_interface (">=",`real_ge:real->real->bool`);
 180   overload_interface ("--",`real_neg:real->real`);
 181   overload_interface ("pow",`real_pow:real->num->real`);
 182   overload_interface ("inv",`real_inv:real->real`);
 183   overload_interface ("abs",`real_abs:real->real`);
 184   override_interface ("&",`real_of_num:num->real`) and
 185   pop_priority() =
 186   if (length !v <= 1) then (print_string "priority unchanged\n") else
 187   let (a::b::c) = !v in
 188   v:= (b::c);
 189   print_string ("priority is now "^b^"\n");
 190   match a with
 191     "num" -> prioritize_num() |
 192     "int" -> prioritize_int() |
 193     "real"-> prioritize_real()|
 194     _ -> () and
 195   get_priority() =
 196   if (!v=[]) then "unknown" else
 197   let (a::b) = !v in a
 198   in
 199   prioritize_int,prioritize_num,prioritize_real,pop_priority,get_priority;;
 200
 201
 202
 203
 204