1structure markerSyntax :> markerSyntax =
2struct
3
4open HolKernel boolLib markerTheory
5
6val ERR = mk_HOL_ERR "markerSyntax";
7
8val stmarker_tm = prim_mk_const{Name="stmarker", Thy="marker"};
9val AC_tm       = prim_mk_const{Name="AC",       Thy="marker"};
10val Cong_tm     = prim_mk_const{Name="Cong",     Thy="marker"};
11val abbrev_tm   = prim_mk_const{Name="Abbrev",   Thy="marker"};
12val label_tm    = prim_mk_const{Name=":-",       Thy="marker"};
13
14(*---------------------------------------------------------------------------*)
15(* Abbrev (n = M) can appear as a hypothesis in a goal.                      *)
16(*---------------------------------------------------------------------------*)
17
18fun mk_abbrev (s,tm) =
19 let val l = mk_var(s,type_of tm)
20     val eq = mk_eq (l,tm)
21 in mk_comb (abbrev_tm,eq)
22 end;
23
24fun dest_abbrev tm =
25  ((fst o dest_var)##I)
26   (dest_eq(dest_monop abbrev_tm (ERR "" "") tm))
27  handle HOL_ERR _ => raise ERR "dest_abbrev" "";
28
29val is_abbrev = Lib.can dest_abbrev;
30
31fun compare_abbrev a1 a2 =
32 let val (s1,rhs1) = dest_abbrev a1
33     val (s2,rhs2) = dest_abbrev a2
34     val v1 = mk_var(s1,type_of rhs1)
35     val v2 = mk_var(s2,type_of rhs2)
36 in
37   mem v1 (free_vars rhs2)
38 end;
39
40(*---------------------------------------------------------------------------*)
41(* Abbr `n` is used as an element of a simplification list in order to have  *)
42(* the abbreviation (Abbrev (n = M)) in the hypotheses of the goal be        *)
43(* expanded before simplification.                                           *)
44(*---------------------------------------------------------------------------*)
45
46fun Abbr q =
47 let val parse = Lib.with_flag(Feedback.emit_MESG,false) Parse.Term
48 in case total parse q
49   of NONE => raise ERR "Abbr" "Ill-formed quotation"
50    | SOME tm =>
51       if is_var tm then
52          REFL(mk_var(fst(dest_var tm),mk_vartype "'abbrev"))
53        else raise ERR "Abbr" "Ill-formed quotation"
54 end;
55
56fun is_abbr th = let
57  val (l,r,ty) = dest_eq_ty (concl th)
58  val vname = dest_vartype ty
59in
60  vname = "'abbrev" andalso #1 (dest_var l) = #1 (dest_var r)
61end handle HOL_ERR _ => false
62
63fun dest_abbr th = let
64  val _ = assert is_abbr th
65in
66  fst(dest_var(lhs (concl th)))
67end
68
69(*---------------------------------------------------------------------------*)
70(* Support for user-controlled labelled assumptions.                         *)
71(*---------------------------------------------------------------------------*)
72
73val label_ty = fst(dom_rng(type_of label_tm))
74
75fun mk_label (s, t) =
76    if type_of t <> bool then
77      raise ERR "mk_label" "First argument not boolean"
78    else
79      list_mk_comb(label_tm, [mk_var(s, label_ty), t]);
80
81fun dest_label tm =
82 ((fst o dest_var)##I)
83 (dest_binop label_tm (ERR "" "") tm)
84 handle HOL_ERR _ => raise ERR "dest_label" "" ;
85
86val is_label = can dest_label;
87
88fun dest_label_ref th = let
89  val p as (l,r) = dest_eq (concl th)
90  val _ =
91      is_var l andalso is_var r andalso Term.compare p = EQUAL andalso
92      Type.compare(type_of l, label_ty) = EQUAL orelse
93      raise ERR "dest_label_ref" "Theorem not a label reference"
94in
95  #1 (dest_var l)
96end
97
98val is_label_ref = can dest_label_ref
99
100end
101