1(* ========================================================================= *) 2(* FILE : smlPrettify.sml *) 3(* DESCRIPTION : Prettify SML strings *) 4(* AUTHOR : (c) Thibault Gauthier, University of Innsbruck *) 5(* DATE : 2018 *) 6(* ========================================================================= *) 7 8structure smlPrettify :> smlPrettify = 9struct 10 11open HolKernel Abbrev boolLib Tactical aiLib smlTimeout smlLexer smlExecute 12 13val ERR = mk_HOL_ERR "smlPrettify" 14 15(* -------------------------------------------------------------------------- 16 Removing unnecessary parentheses 17 --------------------------------------------------------------------------*) 18 19fun is_par s = mem s ["(",")"] 20 21fun elim_par sl = case sl of 22 [] => [] 23 | ["(",a,")"] => if is_par a then sl else [a] 24 | ["(","(",a,")",")"] => if is_par a then sl else [a] 25 | "(" :: a :: ")" :: m => 26 if is_par a 27 then "(" :: a :: ")" :: elim_par m 28 else a :: elim_par m 29 | "(" :: "(" :: a :: ")" :: ")" :: m => 30 if is_par a 31 then "(" :: "(" :: a :: ")" :: ")" :: elim_par m 32 else a :: elim_par m 33 | a :: m => a :: elim_par m 34 35(* ------------------------------------------------------------------------- 36 Remove infix guards 37 ------------------------------------------------------------------------- *) 38 39fun is_infix_open s = 40 String.isPrefix "sml_infix" s andalso 41 String.isSuffix "open" s 42 43fun is_infix_close s = 44 String.isPrefix "sml_infix" s andalso 45 String.isSuffix "close" s 46 47fun elim_infix sl = case sl of 48 [] => [] 49 | a :: b :: c :: m => 50 if is_infix_open a andalso is_infix_close c 51 then b :: elim_infix m 52 else a :: elim_infix (b :: c :: m) 53 | a :: m => a :: elim_infix m 54 55(* ------------------------------------------------------------------------- 56 Removing structure prefixes. Also prefers lower case if available. 57 ------------------------------------------------------------------------- *) 58 59fun drop_struct long = 60 let 61 val sl = String.tokens (fn x => x = #".") long 62 val short = last sl 63 val lower = String.translate (Char.toString o Char.toLower) short 64 in 65 if length sl = 1 then long 66 else if is_local_value lower andalso is_pointer_eq long lower 67 then lower 68 else if is_local_value short andalso is_pointer_eq long short 69 then short 70 else long 71 end 72 73fun elim_struct sl = map drop_struct sl 74 75(* ------------------------------------------------------------------------- 76 Prettify theorems 77 ------------------------------------------------------------------------- *) 78 79fun elim_dbfetch sl = case sl of 80 [] => [] 81 | ["DB.fetch",a,b] => 82 (( 83 if unquote_string a = current_theory () 84 then ["DB.fetch",a,b] 85 else [unquote_string a ^ "Theory." ^ unquote_string b] 86 ) 87 handle _ => ["DB.fetch",a,b]) 88 | "DB.fetch" :: a :: b :: m => 89 (( 90 if unquote_string a = current_theory () 91 then ["DB.fetch",a,b] 92 else [unquote_string a ^ "Theory." ^ unquote_string b] 93 ) 94 handle _ => ["DB.fetch",a,b]) 95 @ 96 elim_dbfetch m 97 | a :: m => a :: elim_dbfetch m 98 99(* ------------------------------------------------------------------------- 100 Requoting terms 101 ------------------------------------------------------------------------- *) 102 103fun is_quoted s = String.sub (s,0) = #"\"" 104 handle Interrupt => raise Interrupt | _ => false 105 106fun requote sl = case sl of 107 [] => [] 108 | "[" :: "QUOTE" :: s :: "]" :: m => 109 if is_quoted s 110 then ("`" ^ rm_space (rm_comment (rm_squote s)) ^ "`") :: requote m 111 else hd sl :: requote (tl sl) 112 | "Term" :: "[" :: "QUOTE" :: s :: "]" :: m => 113 if is_quoted s 114 then ("``" ^ rm_space (rm_comment (rm_squote s)) ^ "``") :: requote m 115 else hd sl :: requote (tl sl) 116 | a :: m => a :: requote m 117 118(* ------------------------------------------------------------------------- 119 Concatenate tokens with smart spaces 120 ------------------------------------------------------------------------- *) 121 122fun smart_space sl = case sl of 123 [] => "" 124 | [a] => a 125 | a :: b :: m => 126 ( 127 if mem a ["[","("] orelse mem b ["]",")",",",";"] 128 then a ^ smart_space (b :: m) 129 else a ^ " " ^ smart_space (b :: m) 130 ) 131 132 133end (* struct *) 134