1structure ParseExtras :> ParseExtras =
2struct
3
4open Parse HolKernel boolSyntax
5
6val grammar_loose_equality =
7    let
8      open term_grammar
9    in
10      add_deltas [
11             RMTMTOK {term_name = "=", tok = "="},
12             GRULE (standard_mapped_spacing {term_name = "=",
13                                             tok = "=",
14                                             fixity = Infix(NONASSOC,100)})
15      ]
16    end
17
18val grammar_tight_equality =
19    let
20      open term_grammar
21    in
22      add_deltas [
23             RMTMTOK {term_name = "=", tok = "="},
24             GRULE (standard_mapped_spacing {term_name = "=",
25                                             tok = "=",
26                                             fixity = Infix(NONASSOC,450)})
27      ]
28    end
29
30
31
32fun tight_equality() = set_fixity "=" (Infix(NONASSOC, 450))
33fun temp_tight_equality() = temp_set_fixity "=" (Infix(NONASSOC, 450))
34
35fun loose_equality () = set_fixity "=" (Infix(NONASSOC, 100))
36fun temp_loose_equality () = temp_set_fixity "=" (Infix(NONASSOC, 100))
37
38fun condprinter (tyg, tmg) backend printer ppfns (pgr,lgr,rgr) depth tm = let
39  open term_pp_types smpp
40  infix >>
41  val _ =
42      case Overload.oi_strip_comb (term_grammar.overload_info tmg) tm of
43          SOME(f, _) =>
44            if term_grammar.grammar_name tmg f = SOME "case"
45            then ()
46            else raise UserPP_Failed
47        | NONE => raise UserPP_Failed
48  val {add_string, ublock, add_break, ...} = ppfns:ppstream_funs
49  val paren_required =
50      (case rgr of
51         Prec(p, _) => p > 70
52       | _ => false) orelse
53      (case lgr of
54         Prec(_, n) => n = GrammarSpecials.fnapp_special
55       | _ => false)
56  val doparen = if paren_required then (fn c => add_string c)
57                else (fn c => nothing)
58  fun syspr gravs t =
59    printer { gravs = gravs, depth = depth - 1, binderp = false } t
60  fun doguard needs_else (g,t) =
61      block PP.CONSISTENT 0
62            (block PP.CONSISTENT 0
63                   ((if needs_else then
64                       add_string "else" >> add_string " " >>
65                       add_string "if"
66                     else
67                       add_string "if") >>
68                    add_break (1,2) >>
69                    syspr (Top,Top,Top) g >>
70                    add_break (1,0) >>
71                    add_string "then") >>
72             add_break (1,2) >>
73             syspr (Top,Top,Top) t)
74
75  fun doelse e = let
76    val prec = Prec(70, "COND")
77  in
78    case Lib.total dest_cond e of
79        SOME (g,t,e_next) => (doguard true (g,t) >> add_break(1,0) >>
80                              doelse e_next)
81      | NONE => block PP.CONSISTENT 0
82                      (add_string "else" >> add_break (1,2) >>
83                       syspr (prec,prec,rgr) e)
84  end
85  val (g,t,e) = dest_cond tm
86in
87  doparen "(" >>
88  block PP.CONSISTENT 0
89    (doguard false (g,t) >> add_break(1,0) >> doelse e) >>
90  doparen ")"
91end
92
93end
94