150 (typs |> map scala_of_typ |> commas |> enclose "List(" ")")) |
150 (typs |> map scala_of_typ |> commas |> enclose "List(" ")")) |
151 | scala_of_typ (TFree (s, sort)) = |
151 | scala_of_typ (TFree (s, sort)) = |
152 enclose "TFree(" ")" (quote s ^ ", " ^ (sort |> map quote |> commas |> enclose "List(" ")")) |
152 enclose "TFree(" ")" (quote s ^ ", " ^ (sort |> map quote |> commas |> enclose "List(" ")")) |
153 | scala_of_typ (TVar ((s, i), sort)) = |
153 | scala_of_typ (TVar ((s, i), sort)) = |
154 enclose "TVar(" ")" ( |
154 enclose "TVar(" ")" ( |
155 enclose "(" ")," (quote s ^ "," ^ quote (string_of_int i)) ^ |
155 enclose "(" ")," (quote s ^ ", " ^ quote (string_of_int i)) ^ |
156 (sort |> map quote |> commas |> enclose "List(" ")")) |
156 (sort |> map quote |> commas |> enclose "List(" ")")) |
157 fun scala_of_term (Const (s, T)) = |
157 fun scala_of_term (Const (s, T)) = |
158 enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T) |
158 enclose "Const(" ")" (quote s ^ ", " ^ scala_of_typ T) |
159 | scala_of_term (Free (s, T)) = |
159 | scala_of_term (Free (s, T)) = |
160 enclose "Free(" ")" (quote s ^ ", " ^ scala_of_typ T) |
160 enclose "Free(" ")" (quote s ^ ", " ^ scala_of_typ T) |
161 | scala_of_term (Var ((s, i), T)) = |
161 | scala_of_term (Var ((s, i), T)) = |
162 enclose "TVar(" ")" ( |
162 enclose "TVar(" ")" ( |
163 enclose "(" ")," (quote s ^ "," ^ quote (string_of_int i)) ^ |
163 enclose "(" ")," (quote s ^ ", " ^ quote (string_of_int i)) ^ |
164 scala_of_typ T) |
164 scala_of_typ T) |
165 | scala_of_term (Bound i) = enclose "Bound(" ")" (string_of_int i) |
165 | scala_of_term (Bound i) = enclose "Bound(" ")" (string_of_int i) |
166 | scala_of_term (Abs (s, T, t)) = |
166 | scala_of_term (Abs (s, T, t)) = |
167 enclose "Abs(" ")" ( |
167 enclose "Abs(" ")" ( |
168 quote s ^ ", " ^ |
168 quote s ^ ", " ^ |
175 for Isabelle standard output compare 2017 "structure ML_PP" *) |
175 for Isabelle standard output compare 2017 "structure ML_PP" *) |
176 fun atomtyp t = |
176 fun atomtyp t = |
177 let |
177 let |
178 fun ato n (Type (s, [])) = "\n*** " ^ indent n ^ "Type (" ^ s ^",[])" |
178 fun ato n (Type (s, [])) = "\n*** " ^ indent n ^ "Type (" ^ s ^",[])" |
179 | ato n (Type (s, Ts)) = "\n*** " ^ indent n ^ "Type (" ^ s ^ ",[" ^ atol (n + 1) Ts |
179 | ato n (Type (s, Ts)) = "\n*** " ^ indent n ^ "Type (" ^ s ^ ",[" ^ atol (n + 1) Ts |
180 | ato n (TFree (s, sort)) = "\n*** " ^ indent n ^ "TFree (" ^ s ^ "," ^ strs2str' sort |
180 | ato n (TFree (s, sort)) = "\n*** " ^ indent n ^ "TFree (" ^ s ^ ", " ^ strs2str' sort |
181 | ato n (TVar ((s, i), sort)) = |
181 | ato n (TVar ((s, i), sort)) = |
182 "\n*** " ^ indent n ^ "TVar ((" ^ s ^ "," ^ string_of_int i ^ strs2str' sort |
182 "\n*** " ^ indent n ^ "TVar ((" ^ s ^ ", " ^ string_of_int i ^ strs2str' sort |
183 and atol n [] = "\n*** " ^ indent n ^ "]" |
183 and atol n [] = "\n*** " ^ indent n ^ "]" |
184 | atol n (T :: Ts) = (ato n T ^ atol n Ts) |
184 | atol n (T :: Ts) = (ato n T ^ atol n Ts) |
185 in tracing (ato 0 t ^ "\n") end; |
185 in tracing (ato 0 t ^ "\n") end; |
186 |
186 |
187 local |
187 local |