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