wneuper/isa: comparison src/Tools/Code/code

equal deleted inserted replaced

-:d7864276bca8
+:ace701efe203
 | print_typ tyvars fxy (ITyVar v) = (str o lookup_var tyvars) v;
 fun print_typdecl tyvars (tyco, vs) =
 print_tyco_expr tyvars NOBR (tyco, map ITyVar vs);
 fun print_typscheme tyvars (vs, ty) =
 Pretty.block (print_typforall tyvars vs @ print_typcontext tyvars vs @| print_typ tyvars NOBR ty);
-fun print_term tyvars some_thm vars fxy (IConst c) =
+fun print_term tyvars some_thm vars fxy (IConst const) =
-print_app tyvars some_thm vars fxy (c, [])
+print_app tyvars some_thm vars fxy (const, [])
 | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
 (case Code_Thingol.unfold_const_app t
 of SOME app => print_app tyvars some_thm vars fxy app
 | _ =>
 brackify fxy [
 | print_term tyvars some_thm vars fxy (t as _ `|=> _) =
 let
 val (binds, t') = Code_Thingol.unfold_pat_abs t;
 val (ps, vars') = fold_map (print_bind tyvars some_thm BR o fst) binds vars;
 in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars some_thm vars' NOBR t') end
-| print_term tyvars some_thm vars fxy (ICase (cases as (_, t0))) =
+| print_term tyvars some_thm vars fxy (ICase case_expr) =
-(case Code_Thingol.unfold_const_app t0
+(case Code_Thingol.unfold_const_app (#primitive case_expr)
-of SOME (c_ts as ((c, _), _)) => if is_none (const_syntax c)
+of SOME (app as ({ name = c, ... }, _)) => if is_none (const_syntax c)
-then print_case tyvars some_thm vars fxy cases
+then print_case tyvars some_thm vars fxy case_expr
-else print_app tyvars some_thm vars fxy c_ts
+else print_app tyvars some_thm vars fxy app
-| NONE => print_case tyvars some_thm vars fxy cases)
+| NONE => print_case tyvars some_thm vars fxy case_expr)
-and print_app_expr tyvars some_thm vars ((c, ((_, (arg_tys, result_ty)), annotate)), ts) =
+and print_app_expr tyvars some_thm vars ({ name = c, dom, range, annotate, ... }, ts) =
 let
-val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (arg_tys, result_ty)
+val ty = Library.foldr (fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (dom, range)
 val printed_const =
 if annotate then
 brackets [(str o deresolve) c, str "::", print_typ tyvars NOBR ty]
 else
 (str o deresolve) c
 in
 printed_const :: map (print_term tyvars some_thm vars BR) ts
 end
 and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) const_syntax
 and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars) some_thm fxy p
-and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
+and print_case tyvars some_thm vars fxy { clauses = [], ... } =
-let
+(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""]
-val (binds, body) = Code_Thingol.unfold_let (ICase cases);
+| print_case tyvars some_thm vars fxy (case_expr as { clauses = [_], ... }) =
+let
+val (binds, body) = Code_Thingol.unfold_let (ICase case_expr);
 fun print_match ((pat, _), t) vars =
 vars
 |> print_bind tyvars some_thm BR pat
 |>> (fn p => semicolon [p, str "=", print_term tyvars some_thm vars NOBR t])
 val (ps, vars') = fold_map print_match binds vars;
 in brackify_block fxy (str "let {")
 ps
 (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
 end
-| print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
+| print_case tyvars some_thm vars fxy { term = t, typ = ty, clauses = clauses as _ :: _, ... } =
 let
 fun print_select (pat, body) =
 let
 val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
 in semicolon [p, str "->", print_term tyvars some_thm vars' NOBR body] end;
 in Pretty.block_enclose
 (concat [str "(case", print_term tyvars some_thm vars NOBR t, str "of", str "{"], str "})")
 (map print_select clauses)
-end
+end;
-| print_case tyvars some_thm vars fxy ((_, []), _) =
-(brackify fxy o Pretty.breaks o map str) ["error", "\"empty case\""];
 fun print_stmt (name, Code_Thingol.Fun (_, (((vs, ty), raw_eqs), _))) =
 let
 val tyvars = intro_vars (map fst vs) reserved;
 fun print_err n =
 semicolon (
 str " where {"
 ],
 str "};"
 ) (map print_classparam classparams)
 end
-| print_stmt (_, Code_Thingol.Classinst ((class, (tyco, vs)), (_, (classparam_instances, _)))) =
+| print_stmt (_, Code_Thingol.Classinst { class, tyco, vs, inst_params, ... }) =
 let
 val tyvars = intro_vars (map fst vs) reserved;
 fun requires_args classparam = case const_syntax classparam
 of NONE => NONE
 | SOME (Code_Printer.Plain_const_syntax _) => SOME 0
 str "=",
 print_app tyvars (SOME thm) reserved NOBR (const, [])
 ]
 | SOME k =>
 let
-val (c, ((_, tys), _)) = const;
+val { name = c, dom, range, ... } = const;
 val (vs, rhs) = (apfst o map) fst
 (Code_Thingol.unfold_abs (Code_Thingol.eta_expand k (const, [])));
 val s = if (is_some o const_syntax) c
 then NONE else (SOME o Long_Name.base_name o deresolve) c;
 val vars = reserved
 |> intro_vars (map_filter I (s :: vs));
-val lhs = IConst (classparam, ((([], []), tys), false)) `$$ map IVar vs;
+val lhs = IConst { name = classparam, typargs = [],
+dicts = [], dom = dom, range = range, annotate = false } `$$ map IVar vs;
 (*dictionaries are not relevant at this late stage,
 and these consts never need type annotations for disambiguation *)
 in
 semicolon [
 print_term tyvars (SOME thm) vars NOBR lhs,
 str (class_name class ^ " "),
 print_typ tyvars BR (tyco `%% map (ITyVar o fst) vs),
 str " where {"
 ],
 str "};"
-) (map print_classparam_instance classparam_instances)
+) (map print_classparam_instance inst_params)
 end;
 in print_stmt end;
 fun haskell_program_of_program labelled_name module_alias module_prefix reserved =
 let
 let
 fun dest_bind t1 t2 = case Code_Thingol.split_pat_abs t2
 of SOME ((pat, ty), t') =>
 SOME ((SOME ((pat, ty), true), t1), t')
 | NONE => NONE;
-fun dest_monad c_bind_name (IConst (c, _) `$ t1 `$ t2) =
+fun dest_monad c_bind_name (IConst { name = c, ... } `$ t1 `$ t2) =
 if c = c_bind_name then dest_bind t1 t2
 else NONE
 | dest_monad _ t = case Code_Thingol.split_let t
 of SOME (((pat, ty), tbind), t') =>
 SOME ((SOME ((pat, ty), false), tbind), t')

changeset 49087	ace701efe203
parent 49018	1d11af40b106
child 49446	6efff142bb54