1structure optionSyntax :> optionSyntax = 2struct 3 4local open sumTheory optionTheory in end; 5 6open HolKernel Abbrev; 7 8val ERR = mk_HOL_ERR "optionSyntax"; 9 10(*--------------------------------------------------------------------------- 11 option types 12 ---------------------------------------------------------------------------*) 13 14fun mk_option ty = mk_thy_type{Tyop="option",Thy="option",Args=[ty]}; 15 16fun dest_option ty = 17 case total dest_thy_type ty 18 of SOME{Tyop="option", Thy="option", Args=[ty]} => ty 19 | other => raise ERR "dest_option" "not an option type"; 20 21val is_option = can dest_option; 22 23 24(*--------------------------------------------------------------------------- 25 Constants of the theory 26 ---------------------------------------------------------------------------*) 27 28val none_tm = prim_mk_const{Name="NONE", Thy="option"} 29val some_tm = prim_mk_const{Name="SOME", Thy="option"} 30val the_tm = prim_mk_const{Name="THE", Thy="option"} 31val option_map_tm = prim_mk_const{Name="OPTION_MAP", Thy="option"} 32val option_join_tm = prim_mk_const{Name="OPTION_JOIN", Thy="option"} 33val is_some_tm = prim_mk_const{Name="IS_SOME", Thy="option"} 34val is_none_tm = prim_mk_const{Name="IS_NONE", Thy="option"} 35val option_case_tm = prim_mk_const{Name="option_CASE", Thy="option"} 36 37 38(*--------------------------------------------------------------------------- 39 Applications of constants 40 ---------------------------------------------------------------------------*) 41 42fun mk_none ty = inst [alpha |-> ty] none_tm 43fun mk_some tm = mk_comb(inst [alpha |-> type_of tm] some_tm, tm) 44 45fun mk_the tm = 46 mk_comb(inst[alpha |-> dest_option (type_of tm)] the_tm,tm) 47 handle HOL_ERR _ => raise ERR "mk_the" ""; 48 49fun mk_option_map (f,opt) = 50 case total (dom_rng o type_of) f 51 of SOME (d,r) => list_mk_comb(inst[alpha|->d,beta|->r]option_map_tm,[f,opt]) 52 | NONE => raise ERR "mk_option_map" ""; 53 54fun mk_option_join tm = 55 mk_comb 56 (inst[alpha |-> dest_option(dest_option(type_of tm))] option_join_tm, tm) 57 handle HOL_ERR _ => raise ERR "mk_option_join" ""; 58 59fun mk_is_none tm = 60 mk_comb(inst[alpha |-> dest_option(type_of tm)]is_none_tm, tm) 61 handle HOL_ERR _ => raise ERR "mk_is_none" ""; 62 63fun mk_is_some tm = 64 mk_comb(inst[alpha |-> dest_option(type_of tm)]is_some_tm, tm) 65 handle HOL_ERR _ => raise ERR "mk_is_some" ""; 66 67fun mk_option_case (n,s,p) = 68 case total dest_thy_type (type_of p) 69 of SOME{Tyop="option", Thy="option", Args=[ty]} 70 => list_mk_comb 71 (inst[beta |-> type_of n, alpha |-> ty]option_case_tm, [p,n,s]) 72 | otherwise => raise ERR "mk_option_case" ""; 73 74 75(*--------------------------------------------------------------------------- 76 Destructor operations 77 ---------------------------------------------------------------------------*) 78 79fun dest_none tm = 80 if same_const none_tm tm then 81 hd (#2 (dest_type (type_of tm))) 82 else raise ERR "dest_none" ""; 83 84val dest_some = dest_monop some_tm (ERR "dest_some" "") 85val dest_the = dest_monop the_tm (ERR "dest_the" "") 86val dest_is_none = dest_monop is_none_tm (ERR "dest_is_none" "") 87val dest_is_some = dest_monop is_some_tm (ERR "dest_is_some" "") 88 89val dest_option_map = dest_binop option_map_tm (ERR "dest_option_map" "") 90val dest_option_join = dest_monop option_join_tm (ERR "dest_option_join" "") 91 92fun dest_option_case tm = 93 let val (f,z) = with_exn dest_comb tm (ERR "dest_option_case" "") 94 val (x,y) = dest_binop option_case_tm (ERR "dest_option_case" "") f 95 in (z,x,y) 96 end 97 98(*--------------------------------------------------------------------------- 99 Query operations 100 ---------------------------------------------------------------------------*) 101 102val is_none = can dest_none 103val is_some = can dest_some 104val is_the = can dest_the 105val is_is_none = can dest_is_none 106val is_is_some = can dest_is_some 107val is_option_map = can dest_option_map 108val is_option_join = can dest_option_join 109val is_option_case = can dest_option_case 110 111 112(*---------------------------------------------------------------------------*) 113(* Lifting from ML options to HOL options *) 114(*---------------------------------------------------------------------------*) 115 116fun lift_option ty = 117 let open TypeBasePure 118 val none = cinst ty none_tm 119 val some = cinst ty some_tm 120 fun lift f NONE = none 121 | lift f (SOME x) = mk_comb(some,f x) 122 in lift 123 end 124 125end 126