22 infixr 5 @|; |
22 infixr 5 @|; |
23 |
23 |
24 |
24 |
25 (** Haskell serializer **) |
25 (** Haskell serializer **) |
26 |
26 |
27 fun print_haskell_stmt labelled_name syntax_class syntax_tyco syntax_const |
27 fun print_haskell_stmt labelled_name class_syntax tyco_syntax const_syntax |
28 reserved deresolve contr_classparam_typs deriving_show = |
28 reserved deresolve contr_classparam_typs deriving_show = |
29 let |
29 let |
30 val deresolve_base = Long_Name.base_name o deresolve; |
30 val deresolve_base = Long_Name.base_name o deresolve; |
31 fun class_name class = case syntax_class class |
31 fun class_name class = case class_syntax class |
32 of NONE => deresolve class |
32 of NONE => deresolve class |
33 | SOME class => class; |
33 | SOME class => class; |
34 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs |
34 fun print_typcontext tyvars vs = case maps (fn (v, sort) => map (pair v) sort) vs |
35 of [] => [] |
35 of [] => [] |
36 | constraints => enum "," "(" ")" ( |
36 | constraints => enum "," "(" ")" ( |
41 of [] => [] |
41 of [] => [] |
42 | vnames => str "forall " :: Pretty.breaks |
42 | vnames => str "forall " :: Pretty.breaks |
43 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; |
43 (map (str o lookup_var tyvars) vnames) @ str "." @@ Pretty.brk 1; |
44 fun print_tyco_expr tyvars fxy (tyco, tys) = |
44 fun print_tyco_expr tyvars fxy (tyco, tys) = |
45 brackify fxy (str tyco :: map (print_typ tyvars BR) tys) |
45 brackify fxy (str tyco :: map (print_typ tyvars BR) tys) |
46 and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case syntax_tyco tyco |
46 and print_typ tyvars fxy (tycoexpr as tyco `%% tys) = (case tyco_syntax tyco |
47 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) |
47 of NONE => print_tyco_expr tyvars fxy (deresolve tyco, tys) |
48 | SOME (i, print) => print (print_typ tyvars) fxy tys) |
48 | SOME (i, print) => print (print_typ tyvars) fxy tys) |
49 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; |
49 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v; |
50 fun print_typdecl tyvars (vs, tycoexpr) = |
50 fun print_typdecl tyvars (vs, tycoexpr) = |
51 Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); |
51 Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr); |
70 val (binds, t') = Code_Thingol.unfold_pat_abs t; |
70 val (binds, t') = Code_Thingol.unfold_pat_abs t; |
71 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; |
71 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars; |
72 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end |
72 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end |
73 | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) = |
73 | print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) = |
74 (case Code_Thingol.unfold_const_app t0 |
74 (case Code_Thingol.unfold_const_app t0 |
75 of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c) |
75 of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c) |
76 then print_case tyvars some_thm vars fxy cases |
76 then print_case tyvars some_thm vars fxy cases |
77 else print_app tyvars some_thm vars fxy c_ts |
77 else print_app tyvars some_thm vars fxy c_ts |
78 | NONE => print_case tyvars some_thm vars fxy cases) |
78 | NONE => print_case tyvars some_thm vars fxy cases) |
79 and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c |
79 and print_app_expr tyvars some_thm vars ((c, (_, function_typs)), ts) = case contr_classparam_typs c |
80 of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts |
80 of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts |
88 in |
88 in |
89 if needs_annotation then |
89 if needs_annotation then |
90 (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs) |
90 (str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) function_typs) |
91 else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts |
91 else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts |
92 end |
92 end |
93 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const |
93 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax |
94 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p |
94 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p |
95 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
95 and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) = |
96 let |
96 let |
97 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
97 val (binds, body) = Code_Thingol.unfold_let (ICase cases); |
98 fun print_match ((pat, ty), t) vars = |
98 fun print_match ((pat, ty), t) vars = |
131 fun print_eqn ((ts, t), (some_thm, _)) = |
131 fun print_eqn ((ts, t), (some_thm, _)) = |
132 let |
132 let |
133 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
133 val consts = fold Code_Thingol.add_constnames (t :: ts) []; |
134 val vars = reserved |
134 val vars = reserved |
135 |> intro_base_names |
135 |> intro_base_names |
136 (is_none o syntax_const) deresolve consts |
136 (is_none o const_syntax) deresolve consts |
137 |> intro_vars ((fold o Code_Thingol.fold_varnames) |
137 |> intro_vars ((fold o Code_Thingol.fold_varnames) |
138 (insert (op =)) ts []); |
138 (insert (op =)) ts []); |
139 in |
139 in |
140 semicolon ( |
140 semicolon ( |
141 (str o deresolve_base) name |
141 (str o deresolve_base) name |
216 ) (map print_classparam classparams) |
216 ) (map print_classparam classparams) |
217 end |
217 end |
218 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) = |
218 | print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) = |
219 let |
219 let |
220 val tyvars = intro_vars (map fst vs) reserved; |
220 val tyvars = intro_vars (map fst vs) reserved; |
221 fun requires_args classparam = case syntax_const classparam |
221 fun requires_args classparam = case const_syntax classparam |
222 of NONE => 0 |
222 of NONE => 0 |
223 | SOME (Code_Printer.Plain_const_syntax _) => 0 |
223 | SOME (Code_Printer.Plain_const_syntax _) => 0 |
224 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k; |
224 | SOME (Code_Printer.Complex_const_syntax (k,_ )) => k; |
225 fun print_classparam_instance ((classparam, const), (thm, _)) = |
225 fun print_classparam_instance ((classparam, const), (thm, _)) = |
226 case requires_args classparam |
226 case requires_args classparam |
232 | k => |
232 | k => |
233 let |
233 let |
234 val (c, (_, tys)) = const; |
234 val (c, (_, tys)) = const; |
235 val (vs, rhs) = (apfst o map) fst |
235 val (vs, rhs) = (apfst o map) fst |
236 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); |
236 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, []))); |
237 val s = if (is_some o syntax_const) c |
237 val s = if (is_some o const_syntax) c |
238 then NONE else (SOME o Long_Name.base_name o deresolve) c; |
238 then NONE else (SOME o Long_Name.base_name o deresolve) c; |
239 val vars = reserved |
239 val vars = reserved |
240 |> intro_vars (map_filter I (s :: vs)); |
240 |> intro_vars (map_filter I (s :: vs)); |
241 val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; |
241 val lhs = IConst (classparam, (([], []), tys)) `$$ map IVar vs; |
242 (*dictionaries are not relevant at this late stage*) |
242 (*dictionaries are not relevant at this late stage*) |
313 handle Option => error ("Unknown statement name: " ^ labelled_name name); |
313 handle Option => error ("Unknown statement name: " ^ labelled_name name); |
314 in (deresolver, hs_program) end; |
314 in (deresolver, hs_program) end; |
315 |
315 |
316 fun serialize_haskell module_prefix module_name string_classes labelled_name |
316 fun serialize_haskell module_prefix module_name string_classes labelled_name |
317 raw_reserved includes module_alias |
317 raw_reserved includes module_alias |
318 syntax_class syntax_tyco syntax_const program |
318 class_syntax tyco_syntax const_syntax program |
319 (stmt_names, presentation_stmt_names) = |
319 (stmt_names, presentation_stmt_names) = |
320 let |
320 let |
321 val reserved = fold (insert (op =) o fst) includes raw_reserved; |
321 val reserved = fold (insert (op =) o fst) includes raw_reserved; |
322 val (deresolver, hs_program) = haskell_program_of_program labelled_name |
322 val (deresolver, hs_program) = haskell_program_of_program labelled_name |
323 module_prefix reserved module_alias program; |
323 module_prefix reserved module_alias program; |
335 andalso forall (deriv' tycos) tys |
335 andalso forall (deriv' tycos) tys |
336 | deriv' _ (ITyVar _) = true |
336 | deriv' _ (ITyVar _) = true |
337 in deriv [] tyco end; |
337 in deriv [] tyco end; |
338 val reserved = make_vars reserved; |
338 val reserved = make_vars reserved; |
339 fun print_stmt qualified = print_haskell_stmt labelled_name |
339 fun print_stmt qualified = print_haskell_stmt labelled_name |
340 syntax_class syntax_tyco syntax_const reserved |
340 class_syntax tyco_syntax const_syntax reserved |
341 (if qualified then deresolver else Long_Name.base_name o deresolver) |
341 (if qualified then deresolver else Long_Name.base_name o deresolver) |
342 contr_classparam_typs |
342 contr_classparam_typs |
343 (if string_classes then deriving_show else K false); |
343 (if string_classes then deriving_show else K false); |
344 fun print_module name content = |
344 fun print_module name content = |
345 (name, Pretty.chunks2 [ |
345 (name, Pretty.chunks2 [ |
456 fun add_monad target' raw_c_bind thy = |
456 fun add_monad target' raw_c_bind thy = |
457 let |
457 let |
458 val c_bind = Code.read_const thy raw_c_bind; |
458 val c_bind = Code.read_const thy raw_c_bind; |
459 in if target = target' then |
459 in if target = target' then |
460 thy |
460 thy |
461 |> Code_Target.add_syntax_const target c_bind |
461 |> Code_Target.add_const_syntax target c_bind |
462 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind))) |
462 (SOME (Code_Printer.complex_const_syntax (pretty_haskell_monad c_bind))) |
463 else error "Only Haskell target allows for monad syntax" end; |
463 else error "Only Haskell target allows for monad syntax" end; |
464 |
464 |
465 |
465 |
466 (** Isar setup **) |
466 (** Isar setup **) |
481 Code_Target.add_target |
481 Code_Target.add_target |
482 (target, { serializer = isar_serializer, literals = literals, |
482 (target, { serializer = isar_serializer, literals = literals, |
483 check = { env_var = "EXEC_GHC", make_destination = I, |
483 check = { env_var = "EXEC_GHC", make_destination = I, |
484 make_command = fn ghc => fn module_name => |
484 make_command = fn ghc => fn module_name => |
485 ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } }) |
485 ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } }) |
486 #> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
486 #> Code_Target.add_tyco_syntax target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] => |
487 brackify_infix (1, R) fxy ( |
487 brackify_infix (1, R) fxy ( |
488 print_typ (INFX (1, X)) ty1, |
488 print_typ (INFX (1, X)) ty1, |
489 str "->", |
489 str "->", |
490 print_typ (INFX (1, R)) ty2 |
490 print_typ (INFX (1, R)) ty2 |
491 ))) |
491 ))) |