92 [enum " o" "(" ")" (map (str o deresolve) classrels), v_p] |
92 [enum " o" "(" ")" (map (str o deresolve) classrels), v_p] |
93 end |
93 end |
94 and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); |
94 and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); |
95 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR |
95 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR |
96 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); |
96 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); |
97 fun print_term is_pseudo_fun thm vars fxy (IConst c) = |
97 fun print_term is_pseudo_fun some_thm vars fxy (IConst c) = |
98 print_app is_pseudo_fun thm vars fxy (c, []) |
98 print_app is_pseudo_fun some_thm vars fxy (c, []) |
99 | print_term is_pseudo_fun thm vars fxy (IVar NONE) = |
99 | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = |
100 str "_" |
100 str "_" |
101 | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = |
101 | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) = |
102 str (lookup_var vars v) |
102 str (lookup_var vars v) |
103 | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = |
103 | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = |
104 (case Code_Thingol.unfold_const_app t |
104 (case Code_Thingol.unfold_const_app t |
105 of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts |
105 of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts |
106 | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1, |
106 | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, |
107 print_term is_pseudo_fun thm vars BR t2]) |
107 print_term is_pseudo_fun some_thm vars BR t2]) |
108 | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = |
108 | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) = |
109 let |
109 let |
110 val (binds, t') = Code_Thingol.unfold_pat_abs t; |
110 val (binds, t') = Code_Thingol.unfold_pat_abs t; |
111 fun print_abs (pat, ty) = |
111 fun print_abs (pat, ty) = |
112 print_bind is_pseudo_fun thm NOBR pat |
112 print_bind is_pseudo_fun some_thm NOBR pat |
113 #>> (fn p => concat [str "fn", p, str "=>"]); |
113 #>> (fn p => concat [str "fn", p, str "=>"]); |
114 val (ps, vars') = fold_map print_abs binds vars; |
114 val (ps, vars') = fold_map print_abs binds vars; |
115 in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end |
115 in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end |
116 | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = |
116 | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) = |
117 (case Code_Thingol.unfold_const_app t0 |
117 (case Code_Thingol.unfold_const_app t0 |
118 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
118 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
119 then print_case is_pseudo_fun thm vars fxy cases |
119 then print_case is_pseudo_fun some_thm vars fxy cases |
120 else print_app is_pseudo_fun thm vars fxy c_ts |
120 else print_app is_pseudo_fun some_thm vars fxy c_ts |
121 | NONE => print_case is_pseudo_fun thm vars fxy cases) |
121 | NONE => print_case is_pseudo_fun some_thm vars fxy cases) |
122 and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = |
122 and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) = |
123 if is_cons c then |
123 if is_cons c then |
124 let val k = length tys in |
124 let val k = length tys in |
125 if k < 2 orelse length ts = k |
125 if k < 2 orelse length ts = k |
126 then (str o deresolve) c |
126 then (str o deresolve) c |
127 :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts) |
127 :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts) |
128 else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] |
128 else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] |
129 end |
129 end |
130 else if is_pseudo_fun c |
130 else if is_pseudo_fun c |
131 then (str o deresolve) c @@ str "()" |
131 then (str o deresolve) c @@ str "()" |
132 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss |
132 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss |
133 @ map (print_term is_pseudo_fun thm vars BR) ts |
133 @ map (print_term is_pseudo_fun some_thm vars BR) ts |
134 and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun) |
134 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) |
135 (print_term is_pseudo_fun) syntax_const thm vars |
135 (print_term is_pseudo_fun) syntax_const some_thm vars |
136 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) |
136 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) |
137 and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = |
137 and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) = |
138 let |
138 let |
139 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
139 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
140 fun print_match ((pat, ty), t) vars = |
140 fun print_match ((pat, ty), t) vars = |
141 vars |
141 vars |
142 |> print_bind is_pseudo_fun thm NOBR pat |
142 |> print_bind is_pseudo_fun some_thm NOBR pat |
143 |>> (fn p => semicolon [str "val", p, str "=", |
143 |>> (fn p => semicolon [str "val", p, str "=", |
144 print_term is_pseudo_fun thm vars NOBR t]) |
144 print_term is_pseudo_fun some_thm vars NOBR t]) |
145 val (ps, vars') = fold_map print_match binds vars; |
145 val (ps, vars') = fold_map print_match binds vars; |
146 in |
146 in |
147 Pretty.chunks [ |
147 Pretty.chunks [ |
148 Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], |
148 Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps], |
149 Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body], |
149 Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body], |
150 str "end" |
150 str "end" |
151 ] |
151 ] |
152 end |
152 end |
153 | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = |
153 | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) = |
154 let |
154 let |
155 fun print_select delim (pat, body) = |
155 fun print_select delim (pat, body) = |
156 let |
156 let |
157 val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars; |
157 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; |
158 in |
158 in |
159 concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body] |
159 concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body] |
160 end; |
160 end; |
161 in |
161 in |
162 brackets ( |
162 brackets ( |
163 str "case" |
163 str "case" |
164 :: print_term is_pseudo_fun thm vars NOBR t |
164 :: print_term is_pseudo_fun some_thm vars NOBR t |
165 :: print_select "of" clause |
165 :: print_select "of" clause |
166 :: map (print_select "|") clauses |
166 :: map (print_select "|") clauses |
167 ) |
167 ) |
168 end |
168 end |
169 | print_case is_pseudo_fun thm vars fxy ((_, []), _) = |
169 | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) = |
170 (concat o map str) ["raise", "Fail", "\"empty case\""]; |
170 (concat o map str) ["raise", "Fail", "\"empty case\""]; |
171 fun print_val_decl print_typscheme (name, typscheme) = concat |
171 fun print_val_decl print_typscheme (name, typscheme) = concat |
172 [str "val", str (deresolve name), str ":", print_typscheme typscheme]; |
172 [str "val", str (deresolve name), str ":", print_typscheme typscheme]; |
173 fun print_datatype_decl definer (tyco, (vs, cos)) = |
173 fun print_datatype_decl definer (tyco, (vs, cos)) = |
174 let |
174 let |
391 |> fold_rev (fn classrel => fn p => |
391 |> fold_rev (fn classrel => fn p => |
392 Pretty.block [p, str ".", (str o deresolve) classrel]) classrels |
392 Pretty.block [p, str ".", (str o deresolve) classrel]) classrels |
393 and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); |
393 and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun); |
394 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR |
394 val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR |
395 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); |
395 (map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort)); |
396 fun print_term is_pseudo_fun thm vars fxy (IConst c) = |
396 fun print_term is_pseudo_fun some_thm vars fxy (IConst c) = |
397 print_app is_pseudo_fun thm vars fxy (c, []) |
397 print_app is_pseudo_fun some_thm vars fxy (c, []) |
398 | print_term is_pseudo_fun thm vars fxy (IVar NONE) = |
398 | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) = |
399 str "_" |
399 str "_" |
400 | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) = |
400 | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) = |
401 str (lookup_var vars v) |
401 str (lookup_var vars v) |
402 | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) = |
402 | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) = |
403 (case Code_Thingol.unfold_const_app t |
403 (case Code_Thingol.unfold_const_app t |
404 of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts |
404 of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts |
405 | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1, |
405 | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1, |
406 print_term is_pseudo_fun thm vars BR t2]) |
406 print_term is_pseudo_fun some_thm vars BR t2]) |
407 | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) = |
407 | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) = |
408 let |
408 let |
409 val (binds, t') = Code_Thingol.unfold_pat_abs t; |
409 val (binds, t') = Code_Thingol.unfold_pat_abs t; |
410 val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars; |
410 val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars; |
411 in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end |
411 in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end |
412 | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) = |
412 | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) = |
413 (case Code_Thingol.unfold_const_app t0 |
413 (case Code_Thingol.unfold_const_app t0 |
414 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
414 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
415 then print_case is_pseudo_fun thm vars fxy cases |
415 then print_case is_pseudo_fun some_thm vars fxy cases |
416 else print_app is_pseudo_fun thm vars fxy c_ts |
416 else print_app is_pseudo_fun some_thm vars fxy c_ts |
417 | NONE => print_case is_pseudo_fun thm vars fxy cases) |
417 | NONE => print_case is_pseudo_fun some_thm vars fxy cases) |
418 and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) = |
418 and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) = |
419 if is_cons c then |
419 if is_cons c then |
420 let val k = length tys in |
420 let val k = length tys in |
421 if length ts = k |
421 if length ts = k |
422 then (str o deresolve) c |
422 then (str o deresolve) c |
423 :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts) |
423 :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts) |
424 else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)] |
424 else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)] |
425 end |
425 end |
426 else if is_pseudo_fun c |
426 else if is_pseudo_fun c |
427 then (str o deresolve) c @@ str "()" |
427 then (str o deresolve) c @@ str "()" |
428 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss |
428 else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss |
429 @ map (print_term is_pseudo_fun thm vars BR) ts |
429 @ map (print_term is_pseudo_fun some_thm vars BR) ts |
430 and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun) |
430 and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun) |
431 (print_term is_pseudo_fun) syntax_const thm vars |
431 (print_term is_pseudo_fun) syntax_const some_thm vars |
432 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) |
432 and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun) |
433 and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) = |
433 and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) = |
434 let |
434 let |
435 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
435 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
436 fun print_let ((pat, ty), t) vars = |
436 fun print_let ((pat, ty), t) vars = |
437 vars |
437 vars |
438 |> print_bind is_pseudo_fun thm NOBR pat |
438 |> print_bind is_pseudo_fun some_thm NOBR pat |
439 |>> (fn p => concat |
439 |>> (fn p => concat |
440 [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"]) |
440 [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"]) |
441 val (ps, vars') = fold_map print_let binds vars; |
441 val (ps, vars') = fold_map print_let binds vars; |
442 in |
442 in |
443 brackify_block fxy (Pretty.chunks ps) [] |
443 brackify_block fxy (Pretty.chunks ps) [] |
444 (print_term is_pseudo_fun thm vars' NOBR body) |
444 (print_term is_pseudo_fun some_thm vars' NOBR body) |
445 end |
445 end |
446 | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) = |
446 | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) = |
447 let |
447 let |
448 fun print_select delim (pat, body) = |
448 fun print_select delim (pat, body) = |
449 let |
449 let |
450 val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars; |
450 val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars; |
451 in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end; |
451 in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end; |
452 in |
452 in |
453 brackets ( |
453 brackets ( |
454 str "match" |
454 str "match" |
455 :: print_term is_pseudo_fun thm vars NOBR t |
455 :: print_term is_pseudo_fun some_thm vars NOBR t |
456 :: print_select "with" clause |
456 :: print_select "with" clause |
457 :: map (print_select "|") clauses |
457 :: map (print_select "|") clauses |
458 ) |
458 ) |
459 end |
459 end |
460 | print_case is_pseudo_fun thm vars fxy ((_, []), _) = |
460 | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) = |
461 (concat o map str) ["failwith", "\"empty case\""]; |
461 (concat o map str) ["failwith", "\"empty case\""]; |
462 fun print_val_decl print_typscheme (name, typscheme) = concat |
462 fun print_val_decl print_typscheme (name, typscheme) = concat |
463 [str "val", str (deresolve name), str ":", print_typscheme typscheme]; |
463 [str "val", str (deresolve name), str ":", print_typscheme typscheme]; |
464 fun print_datatype_decl definer (tyco, (vs, cos)) = |
464 fun print_datatype_decl definer (tyco, (vs, cos)) = |
465 let |
465 let |
475 ) |
475 ) |
476 end; |
476 end; |
477 fun print_def is_pseudo_fun needs_typ definer |
477 fun print_def is_pseudo_fun needs_typ definer |
478 (ML_Function (name, (vs_ty as (vs, ty), eqs))) = |
478 (ML_Function (name, (vs_ty as (vs, ty), eqs))) = |
479 let |
479 let |
480 fun print_eqn ((ts, t), (thm, _)) = |
480 fun print_eqn ((ts, t), (some_thm, _)) = |
481 let |
481 let |
482 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
482 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
483 val vars = reserved |
483 val vars = reserved |
484 |> intro_vars ((fold o Code_Thingol.fold_varnames) |
484 |> intro_vars ((fold o Code_Thingol.fold_varnames) |
485 (insert (op =)) ts []); |
485 (insert (op =)) ts []); |
486 in concat [ |
486 in concat [ |
487 (Pretty.block o Pretty.commas) |
487 (Pretty.block o Pretty.commas) |
488 (map (print_term is_pseudo_fun thm vars NOBR) ts), |
488 (map (print_term is_pseudo_fun some_thm vars NOBR) ts), |
489 str "->", |
489 str "->", |
490 print_term is_pseudo_fun thm vars NOBR t |
490 print_term is_pseudo_fun some_thm vars NOBR t |
491 ] end; |
491 ] end; |
492 fun print_eqns is_pseudo [((ts, t), (thm, _))] = |
492 fun print_eqns is_pseudo [((ts, t), (some_thm, _))] = |
493 let |
493 let |
494 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
494 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
495 val vars = reserved |
495 val vars = reserved |
496 |> intro_base_names |
496 |> intro_base_names |
497 (is_none o syntax_const) deresolve consts |
497 (is_none o syntax_const) deresolve consts |
498 |> intro_vars ((fold o Code_Thingol.fold_varnames) |
498 |> intro_vars ((fold o Code_Thingol.fold_varnames) |
499 (insert (op =)) ts []); |
499 (insert (op =)) ts []); |
500 in |
500 in |
501 concat ( |
501 concat ( |
502 (if is_pseudo then [str "()"] |
502 (if is_pseudo then [str "()"] |
503 else map (print_term is_pseudo_fun thm vars BR) ts) |
503 else map (print_term is_pseudo_fun some_thm vars BR) ts) |
504 @ str "=" |
504 @ str "=" |
505 @@ print_term is_pseudo_fun thm vars NOBR t |
505 @@ print_term is_pseudo_fun some_thm vars NOBR t |
506 ) |
506 ) |
507 end |
507 end |
508 | print_eqns _ ((eq as (([_], _), _)) :: eqs) = |
508 | print_eqns _ ((eq as (([_], _), _)) :: eqs) = |
509 Pretty.block ( |
509 Pretty.block ( |
510 str "=" |
510 str "=" |
756 in (base'', nsp') end; |
756 in (base'', nsp') end; |
757 fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) = |
757 fun ml_binding_of_stmt (name, Code_Thingol.Fun (_, (tysm as (vs, ty), raw_eqs))) = |
758 let |
758 let |
759 val eqs = filter (snd o snd) raw_eqs; |
759 val eqs = filter (snd o snd) raw_eqs; |
760 val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs |
760 val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs |
761 of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty |
761 of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty |
762 then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE) |
762 then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE) |
763 else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) |
763 else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name)) |
764 | _ => (eqs, NONE) |
764 | _ => (eqs, NONE) |
765 else (eqs, NONE) |
765 else (eqs, NONE) |
766 in (ML_Function (name, (tysm, eqs')), is_value) end |
766 in (ML_Function (name, (tysm, eqs')), is_value) end |
767 | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = |
767 | ml_binding_of_stmt (name, Code_Thingol.Classinst (stmt as ((_, (_, vs)), _))) = |