equal
deleted
inserted
replaced
68 pr_term tyvars thm vars NOBR t1, |
68 pr_term tyvars thm vars NOBR t1, |
69 pr_term tyvars thm vars BR t2 |
69 pr_term tyvars thm vars BR t2 |
70 ]) |
70 ]) |
71 | pr_term tyvars thm vars fxy (IVar v) = |
71 | pr_term tyvars thm vars fxy (IVar v) = |
72 (str o Code_Printer.lookup_var vars) v |
72 (str o Code_Printer.lookup_var vars) v |
73 | pr_term tyvars thm vars fxy (t as _ `|-> _) = |
73 | pr_term tyvars thm vars fxy (t as _ `|=> _) = |
74 let |
74 let |
75 val (binds, t') = Code_Thingol.unfold_abs t; |
75 val (binds, t') = Code_Thingol.unfold_abs t; |
76 fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty); |
76 fun pr ((v, pat), ty) = pr_bind tyvars thm BR ((SOME v, pat), ty); |
77 val (ps, vars') = fold_map pr binds vars; |
77 val (ps, vars') = fold_map pr binds vars; |
78 in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end |
78 in brackets (str "\\" :: ps @ str "->" @@ pr_term tyvars thm vars' NOBR t') end |
238 str "};" |
238 str "};" |
239 ) (map pr_classparam classparams) |
239 ) (map pr_classparam classparams) |
240 end |
240 end |
241 | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = |
241 | pr_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, classparam_insts))) = |
242 let |
242 let |
243 val split_abs_pure = (fn (v, _) `|-> t => SOME (v, t) | _ => NONE); |
243 val split_abs_pure = (fn (v, _) `|=> t => SOME (v, t) | _ => NONE); |
244 val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure; |
244 val unfold_abs_pure = Code_Thingol.unfoldr split_abs_pure; |
245 val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; |
245 val tyvars = Code_Printer.intro_vars (map fst vs) init_syms; |
246 fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam |
246 fun pr_instdef ((classparam, c_inst), (thm, _)) = case syntax_const classparam |
247 of NONE => semicolon [ |
247 of NONE => semicolon [ |
248 (str o deresolve_base) classparam, |
248 (str o deresolve_base) classparam, |