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