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