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