--- a/src/Tools/Code/code_eval.ML Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_eval.ML Fri Feb 19 11:06:22 2010 +0100
@@ -53,7 +53,7 @@
val value_name = "Value.VALUE.value"
val program' = program
|> Graph.new_node (value_name,
- Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (Drule.dummy_thm, true))])))
+ Code_Thingol.Fun (Term.dummy_patternN, (([], ty), [(([], t), (NONE, true))])))
|> fold (curry Graph.add_edge value_name) deps;
val (value_code, [SOME value_name']) = Code_ML.evaluation_code_of thy
(the_default target some_target) "" naming program' [value_name];
--- a/src/Tools/Code/code_haskell.ML Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML Fri Feb 19 11:06:22 2010 +0100
@@ -50,71 +50,71 @@
Pretty.block (print_typcontext tyvars vs @| print_tyco_expr tyvars NOBR tycoexpr);
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 thm vars fxy (IConst c) =
- print_app tyvars thm vars fxy (c, [])
- | print_term tyvars thm vars fxy (t as (t1 `$ t2)) =
+ fun print_term tyvars some_thm vars fxy (IConst c) =
+ print_app tyvars some_thm vars fxy (c, [])
+ | print_term tyvars some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
- of SOME app => print_app tyvars thm vars fxy app
+ of SOME app => print_app tyvars some_thm vars fxy app
| _ =>
brackify fxy [
- print_term tyvars thm vars NOBR t1,
- print_term tyvars thm vars BR t2
+ print_term tyvars some_thm vars NOBR t1,
+ print_term tyvars some_thm vars BR t2
])
- | print_term tyvars thm vars fxy (IVar NONE) =
+ | print_term tyvars some_thm vars fxy (IVar NONE) =
str "_"
- | print_term tyvars thm vars fxy (IVar (SOME v)) =
+ | print_term tyvars some_thm vars fxy (IVar (SOME v)) =
(str o lookup_var vars) v
- | print_term tyvars thm vars fxy (t as _ `|=> _) =
+ | 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 thm BR o fst) binds vars;
- in brackets (str "\\" :: ps @ str "->" @@ print_term tyvars thm vars' NOBR t') end
- | print_term tyvars thm vars fxy (ICase (cases as (_, t0))) =
+ 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))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then print_case tyvars thm vars fxy cases
- else print_app tyvars thm vars fxy c_ts
- | NONE => print_case tyvars thm vars fxy cases)
- and print_app_expr tyvars thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
- of [] => (str o deresolve) c :: map (print_term tyvars thm vars BR) ts
+ then print_case tyvars some_thm vars fxy cases
+ else print_app tyvars some_thm vars fxy c_ts
+ | NONE => print_case tyvars some_thm vars fxy cases)
+ and print_app_expr tyvars some_thm vars ((c, (_, tys)), ts) = case contr_classparam_typs c
+ of [] => (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
| fingerprint => let
val ts_fingerprint = ts ~~ take (length ts) fingerprint;
val needs_annotation = forall (fn (_, NONE) => true | (t, SOME _) =>
(not o Code_Thingol.locally_monomorphic) t) ts_fingerprint;
- fun print_term_anno (t, NONE) _ = print_term tyvars thm vars BR t
+ fun print_term_anno (t, NONE) _ = print_term tyvars some_thm vars BR t
| print_term_anno (t, SOME _) ty =
- brackets [print_term tyvars thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
+ brackets [print_term tyvars some_thm vars NOBR t, str "::", print_typ tyvars NOBR ty];
in
if needs_annotation then
(str o deresolve) c :: map2 print_term_anno ts_fingerprint (take (length ts) tys)
- else (str o deresolve) c :: map (print_term tyvars thm vars BR) ts
+ else (str o deresolve) c :: map (print_term tyvars some_thm vars BR) ts
end
and print_app tyvars = gen_print_app (print_app_expr tyvars) (print_term tyvars) syntax_const
- and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars) thm fxy p
- and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
+ 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 ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun print_match ((pat, ty), t) vars =
vars
- |> print_bind tyvars thm BR pat
- |>> (fn p => semicolon [p, str "=", print_term tyvars thm vars NOBR t])
+ |> 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 thm vars' NOBR body])
+ (concat [str "}", str "in", print_term tyvars some_thm vars' NOBR body])
end
- | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
+ | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
let
fun print_select (pat, body) =
let
- val (p, vars') = print_bind tyvars thm NOBR pat vars;
- in semicolon [p, str "->", print_term tyvars thm vars' NOBR body] end;
+ 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 brackify_block fxy
- (concat [str "case", print_term tyvars thm vars NOBR t, str "of", str "{"])
+ (concat [str "case", print_term tyvars some_thm vars NOBR t, str "of", str "{"])
(map print_select clauses)
(str "}")
end
- | print_case tyvars thm vars fxy ((_, []), _) =
+ | 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
@@ -128,7 +128,7 @@
@@ (str o ML_Syntax.print_string
o Long_Name.base_name o Long_Name.qualifier) name
);
- fun print_eqn ((ts, t), (thm, _)) =
+ fun print_eqn ((ts, t), (some_thm, _)) =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
@@ -139,9 +139,9 @@
in
semicolon (
(str o deresolve_base) name
- :: map (print_term tyvars thm vars BR) ts
+ :: map (print_term tyvars some_thm vars BR) ts
@ str "="
- @@ print_term tyvars thm vars NOBR t
+ @@ print_term tyvars some_thm vars NOBR t
)
end;
in
@@ -222,7 +222,7 @@
of NONE => semicolon [
(str o deresolve_base) classparam,
str "=",
- print_app tyvars thm reserved NOBR (c_inst, [])
+ print_app tyvars (SOME thm) reserved NOBR (c_inst, [])
]
| SOME (k, pr) =>
let
@@ -238,9 +238,9 @@
(*dictionaries are not relevant at this late stage*)
in
semicolon [
- print_term tyvars thm vars NOBR lhs,
+ print_term tyvars (SOME thm) vars NOBR lhs,
str "=",
- print_term tyvars thm vars NOBR rhs
+ print_term tyvars (SOME thm) vars NOBR rhs
]
end;
in
--- a/src/Tools/Code/code_ml.ML Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_ml.ML Fri Feb 19 11:06:22 2010 +0100
@@ -28,7 +28,7 @@
val target_OCaml = "OCaml";
datatype ml_binding =
- ML_Function of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+ ML_Function of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| ML_Instance of string * ((class * (string * (vname * sort) list))
* ((class * (string * (string * dict list list))) list
* ((string * const) * (thm * bool)) list));
@@ -94,79 +94,79 @@
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
- fun print_term is_pseudo_fun thm vars fxy (IConst c) =
- print_app is_pseudo_fun thm vars fxy (c, [])
- | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
+ fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
+ print_app is_pseudo_fun some_thm vars fxy (c, [])
+ | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
str "_"
- | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
+ | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
- | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
+ | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
- | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
- print_term is_pseudo_fun thm vars BR t2])
- | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
+ of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+ | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
+ print_term is_pseudo_fun some_thm vars BR t2])
+ | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
fun print_abs (pat, ty) =
- print_bind is_pseudo_fun thm NOBR pat
+ print_bind is_pseudo_fun some_thm NOBR pat
#>> (fn p => concat [str "fn", p, str "=>"]);
val (ps, vars') = fold_map print_abs binds vars;
- in brackets (ps @ [print_term is_pseudo_fun thm vars' NOBR t']) end
- | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
+ in brackets (ps @ [print_term is_pseudo_fun some_thm vars' NOBR t']) end
+ | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then print_case is_pseudo_fun thm vars fxy cases
- else print_app is_pseudo_fun thm vars fxy c_ts
- | NONE => print_case is_pseudo_fun thm vars fxy cases)
- and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ then print_case is_pseudo_fun some_thm vars fxy cases
+ else print_app is_pseudo_fun some_thm vars fxy c_ts
+ | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
if is_cons c then
let val k = length tys in
if k < 2 orelse length ts = k
then (str o deresolve) c
- :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
- else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
+ :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+ else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
- @ map (print_term is_pseudo_fun thm vars BR) ts
- and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
- (print_term is_pseudo_fun) syntax_const thm vars
+ @ map (print_term is_pseudo_fun some_thm vars BR) ts
+ and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
+ (print_term is_pseudo_fun) syntax_const some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
- and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun print_match ((pat, ty), t) vars =
vars
- |> print_bind is_pseudo_fun thm NOBR pat
+ |> print_bind is_pseudo_fun some_thm NOBR pat
|>> (fn p => semicolon [str "val", p, str "=",
- print_term is_pseudo_fun thm vars NOBR t])
+ print_term is_pseudo_fun some_thm vars NOBR t])
val (ps, vars') = fold_map print_match binds vars;
in
Pretty.chunks [
Pretty.block [str "let", Pretty.fbrk, Pretty.chunks ps],
- Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun thm vars' NOBR body],
+ Pretty.block [str "in", Pretty.fbrk, print_term is_pseudo_fun some_thm vars' NOBR body],
str "end"
]
end
- | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
+ | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
let
fun print_select delim (pat, body) =
let
- val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
+ val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
in
- concat [str delim, p, str "=>", print_term is_pseudo_fun thm vars' NOBR body]
+ concat [str delim, p, str "=>", print_term is_pseudo_fun some_thm vars' NOBR body]
end;
in
brackets (
str "case"
- :: print_term is_pseudo_fun thm vars NOBR t
+ :: print_term is_pseudo_fun some_thm vars NOBR t
:: print_select "of" clause
:: map (print_select "|") clauses
)
end
- | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
+ | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
(concat o map str) ["raise", "Fail", "\"empty case\""];
fun print_val_decl print_typscheme (name, typscheme) = concat
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
@@ -186,7 +186,7 @@
fun print_def is_pseudo_fun needs_typ definer
(ML_Function (name, (vs_ty as (vs, ty), eq :: eqs))) =
let
- fun print_eqn definer ((ts, t), (thm, _)) =
+ fun print_eqn definer ((ts, t), (some_thm, _)) =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
@@ -202,9 +202,9 @@
prolog
:: (if is_pseudo_fun name then [str "()"]
else print_dict_args vs
- @ map (print_term is_pseudo_fun thm vars BR) ts)
+ @ map (print_term is_pseudo_fun some_thm vars BR) ts)
@ str "="
- @@ print_term is_pseudo_fun thm vars NOBR t
+ @@ print_term is_pseudo_fun some_thm vars NOBR t
)
end
val shift = if null eqs then I else
@@ -229,7 +229,7 @@
concat [
(str o Long_Name.base_name o deresolve) classparam,
str "=",
- print_app (K false) thm reserved NOBR (c_inst, [])
+ print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
];
in pair
(print_val_decl print_dicttypscheme
@@ -393,71 +393,71 @@
and print_dicts is_pseudo_fun = print_tuple (print_dict is_pseudo_fun);
val print_dict_args = map_filter (fn (v, sort) => print_dicts (K false) BR
(map_index (fn (i, _) => DictVar ([], (v, (i, length sort)))) sort));
- fun print_term is_pseudo_fun thm vars fxy (IConst c) =
- print_app is_pseudo_fun thm vars fxy (c, [])
- | print_term is_pseudo_fun thm vars fxy (IVar NONE) =
+ fun print_term is_pseudo_fun some_thm vars fxy (IConst c) =
+ print_app is_pseudo_fun some_thm vars fxy (c, [])
+ | print_term is_pseudo_fun some_thm vars fxy (IVar NONE) =
str "_"
- | print_term is_pseudo_fun thm vars fxy (IVar (SOME v)) =
+ | print_term is_pseudo_fun some_thm vars fxy (IVar (SOME v)) =
str (lookup_var vars v)
- | print_term is_pseudo_fun thm vars fxy (t as t1 `$ t2) =
+ | print_term is_pseudo_fun some_thm vars fxy (t as t1 `$ t2) =
(case Code_Thingol.unfold_const_app t
- of SOME c_ts => print_app is_pseudo_fun thm vars fxy c_ts
- | NONE => brackify fxy [print_term is_pseudo_fun thm vars NOBR t1,
- print_term is_pseudo_fun thm vars BR t2])
- | print_term is_pseudo_fun thm vars fxy (t as _ `|=> _) =
+ of SOME c_ts => print_app is_pseudo_fun some_thm vars fxy c_ts
+ | NONE => brackify fxy [print_term is_pseudo_fun some_thm vars NOBR t1,
+ print_term is_pseudo_fun some_thm vars BR t2])
+ | print_term is_pseudo_fun some_thm vars fxy (t as _ `|=> _) =
let
val (binds, t') = Code_Thingol.unfold_pat_abs t;
- val (ps, vars') = fold_map (print_bind is_pseudo_fun thm BR o fst) binds vars;
- in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun thm vars' NOBR t') end
- | print_term is_pseudo_fun thm vars fxy (ICase (cases as (_, t0))) =
+ val (ps, vars') = fold_map (print_bind is_pseudo_fun some_thm BR o fst) binds vars;
+ in brackets (str "fun" :: ps @ str "->" @@ print_term is_pseudo_fun some_thm vars' NOBR t') end
+ | print_term is_pseudo_fun some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then print_case is_pseudo_fun thm vars fxy cases
- else print_app is_pseudo_fun thm vars fxy c_ts
- | NONE => print_case is_pseudo_fun thm vars fxy cases)
- and print_app_expr is_pseudo_fun thm vars (app as ((c, ((_, iss), tys)), ts)) =
+ then print_case is_pseudo_fun some_thm vars fxy cases
+ else print_app is_pseudo_fun some_thm vars fxy c_ts
+ | NONE => print_case is_pseudo_fun some_thm vars fxy cases)
+ and print_app_expr is_pseudo_fun some_thm vars (app as ((c, ((_, iss), tys)), ts)) =
if is_cons c then
let val k = length tys in
if length ts = k
then (str o deresolve) c
- :: the_list (print_tuple (print_term is_pseudo_fun thm vars) BR ts)
- else [print_term is_pseudo_fun thm vars BR (Code_Thingol.eta_expand k app)]
+ :: the_list (print_tuple (print_term is_pseudo_fun some_thm vars) BR ts)
+ else [print_term is_pseudo_fun some_thm vars BR (Code_Thingol.eta_expand k app)]
end
else if is_pseudo_fun c
then (str o deresolve) c @@ str "()"
else (str o deresolve) c :: map_filter (print_dicts is_pseudo_fun BR) iss
- @ map (print_term is_pseudo_fun thm vars BR) ts
- and print_app is_pseudo_fun thm vars = gen_print_app (print_app_expr is_pseudo_fun)
- (print_term is_pseudo_fun) syntax_const thm vars
+ @ map (print_term is_pseudo_fun some_thm vars BR) ts
+ and print_app is_pseudo_fun some_thm vars = gen_print_app (print_app_expr is_pseudo_fun)
+ (print_term is_pseudo_fun) syntax_const some_thm vars
and print_bind is_pseudo_fun = gen_print_bind (print_term is_pseudo_fun)
- and print_case is_pseudo_fun thm vars fxy (cases as ((_, [_]), _)) =
+ and print_case is_pseudo_fun some_thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun print_let ((pat, ty), t) vars =
vars
- |> print_bind is_pseudo_fun thm NOBR pat
+ |> print_bind is_pseudo_fun some_thm NOBR pat
|>> (fn p => concat
- [str "let", p, str "=", print_term is_pseudo_fun thm vars NOBR t, str "in"])
+ [str "let", p, str "=", print_term is_pseudo_fun some_thm vars NOBR t, str "in"])
val (ps, vars') = fold_map print_let binds vars;
in
brackify_block fxy (Pretty.chunks ps) []
- (print_term is_pseudo_fun thm vars' NOBR body)
+ (print_term is_pseudo_fun some_thm vars' NOBR body)
end
- | print_case is_pseudo_fun thm vars fxy (((t, ty), clause :: clauses), _) =
+ | print_case is_pseudo_fun some_thm vars fxy (((t, ty), clause :: clauses), _) =
let
fun print_select delim (pat, body) =
let
- val (p, vars') = print_bind is_pseudo_fun thm NOBR pat vars;
- in concat [str delim, p, str "->", print_term is_pseudo_fun thm vars' NOBR body] end;
+ val (p, vars') = print_bind is_pseudo_fun some_thm NOBR pat vars;
+ in concat [str delim, p, str "->", print_term is_pseudo_fun some_thm vars' NOBR body] end;
in
brackets (
str "match"
- :: print_term is_pseudo_fun thm vars NOBR t
+ :: print_term is_pseudo_fun some_thm vars NOBR t
:: print_select "with" clause
:: map (print_select "|") clauses
)
end
- | print_case is_pseudo_fun thm vars fxy ((_, []), _) =
+ | print_case is_pseudo_fun some_thm vars fxy ((_, []), _) =
(concat o map str) ["failwith", "\"empty case\""];
fun print_val_decl print_typscheme (name, typscheme) = concat
[str "val", str (deresolve name), str ":", print_typscheme typscheme];
@@ -477,7 +477,7 @@
fun print_def is_pseudo_fun needs_typ definer
(ML_Function (name, (vs_ty as (vs, ty), eqs))) =
let
- fun print_eqn ((ts, t), (thm, _)) =
+ fun print_eqn ((ts, t), (some_thm, _)) =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
@@ -485,11 +485,11 @@
(insert (op =)) ts []);
in concat [
(Pretty.block o Pretty.commas)
- (map (print_term is_pseudo_fun thm vars NOBR) ts),
+ (map (print_term is_pseudo_fun some_thm vars NOBR) ts),
str "->",
- print_term is_pseudo_fun thm vars NOBR t
+ print_term is_pseudo_fun some_thm vars NOBR t
] end;
- fun print_eqns is_pseudo [((ts, t), (thm, _))] =
+ fun print_eqns is_pseudo [((ts, t), (some_thm, _))] =
let
val consts = fold Code_Thingol.add_constnames (t :: ts) [];
val vars = reserved
@@ -500,9 +500,9 @@
in
concat (
(if is_pseudo then [str "()"]
- else map (print_term is_pseudo_fun thm vars BR) ts)
+ else map (print_term is_pseudo_fun some_thm vars BR) ts)
@ str "="
- @@ print_term is_pseudo_fun thm vars NOBR t
+ @@ print_term is_pseudo_fun some_thm vars NOBR t
)
end
| print_eqns _ ((eq as (([_], _), _)) :: eqs) =
@@ -562,7 +562,7 @@
concat [
(str o deresolve) classparam,
str "=",
- print_app (K false) thm reserved NOBR (c_inst, [])
+ print_app (K false) (SOME thm) reserved NOBR (c_inst, [])
];
in pair
(print_val_decl print_dicttypscheme
@@ -758,8 +758,8 @@
let
val eqs = filter (snd o snd) raw_eqs;
val (eqs', is_value) = if null (filter_out (null o snd) vs) then case eqs
- of [(([], t), thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
- then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), thm)], NONE)
+ of [(([], t), some_thm)] => if (not o null o fst o Code_Thingol.unfold_fun) ty
+ then ([(([IVar (SOME "x")], t `$ IVar (SOME "x")), some_thm)], NONE)
else (eqs, SOME (name, member (op =) (Code_Thingol.add_constnames t []) name))
| _ => (eqs, NONE)
else (eqs, NONE)
--- a/src/Tools/Code/code_printer.ML Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_printer.ML Fri Feb 19 11:06:22 2010 +0100
@@ -11,7 +11,7 @@
type const = Code_Thingol.const
type dict = Code_Thingol.dict
- val eqn_error: thm -> string -> 'a
+ val eqn_error: thm option -> string -> 'a
val @@ : 'a * 'a -> 'a list
val @| : 'a list * 'a -> 'a list
@@ -78,12 +78,12 @@
val simple_const_syntax: simple_const_syntax -> proto_const_syntax
val activate_const_syntax: theory -> literals
-> proto_const_syntax -> Code_Thingol.naming -> const_syntax * Code_Thingol.naming
- val gen_print_app: (thm -> var_ctxt -> const * iterm list -> Pretty.T list)
- -> (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
+ val gen_print_app: (thm option -> var_ctxt -> const * iterm list -> Pretty.T list)
+ -> (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
-> (string -> const_syntax option)
- -> thm -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
- val gen_print_bind: (thm -> var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm -> fixity
+ -> thm option -> var_ctxt -> fixity -> const * iterm list -> Pretty.T
+ val gen_print_bind: (thm option -> var_ctxt -> fixity -> iterm -> Pretty.T)
+ -> thm option -> fixity
-> iterm -> var_ctxt -> Pretty.T * var_ctxt
val mk_name_module: Name.context -> string option -> (string -> string option)
@@ -96,7 +96,8 @@
open Code_Thingol;
-fun eqn_error thm s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm);
+fun eqn_error (SOME thm) s = error (s ^ ",\nin equation " ^ Display.string_of_thm_without_context thm)
+ | eqn_error NONE s = error s;
(** assembling and printing text pieces **)
@@ -243,9 +244,9 @@
-> fixity -> (iterm * itype) list -> Pretty.T);
type proto_const_syntax = int * (string list * (literals -> string list
-> (var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T));
type const_syntax = int * ((var_ctxt -> fixity -> iterm -> Pretty.T)
- -> thm -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
+ -> thm option -> var_ctxt -> fixity -> (iterm * itype) list -> Pretty.T);
fun simple_const_syntax syn =
apsnd (fn f => ([], (fn _ => fn _ => fn print => fn _ => fn vars => f (print vars)))) syn;
--- a/src/Tools/Code/code_scala.ML Fri Feb 19 11:06:22 2010 +0100
+++ b/src/Tools/Code/code_scala.ML Fri Feb 19 11:06:22 2010 +0100
@@ -34,33 +34,33 @@
Pretty.block [p, str ":", Pretty.brk 1, print_typ tyvars NOBR ty]
fun print_var vars NONE = str "_"
| print_var vars (SOME v) = (str o lookup_var vars) v
- fun print_term tyvars is_pat thm vars fxy (IConst c) =
- print_app tyvars is_pat thm vars fxy (c, [])
- | print_term tyvars is_pat thm vars fxy (t as (t1 `$ t2)) =
+ fun print_term tyvars is_pat some_thm vars fxy (IConst c) =
+ print_app tyvars is_pat some_thm vars fxy (c, [])
+ | print_term tyvars is_pat some_thm vars fxy (t as (t1 `$ t2)) =
(case Code_Thingol.unfold_const_app t
- of SOME app => print_app tyvars is_pat thm vars fxy app
+ of SOME app => print_app tyvars is_pat some_thm vars fxy app
| _ => applify "(" ")" fxy
- (print_term tyvars is_pat thm vars BR t1)
- [print_term tyvars is_pat thm vars NOBR t2])
- | print_term tyvars is_pat thm vars fxy (IVar v) =
+ (print_term tyvars is_pat some_thm vars BR t1)
+ [print_term tyvars is_pat some_thm vars NOBR t2])
+ | print_term tyvars is_pat some_thm vars fxy (IVar v) =
print_var vars v
- | print_term tyvars is_pat thm vars fxy ((v, ty) `|=> t) =
+ | print_term tyvars is_pat some_thm vars fxy ((v, ty) `|=> t) =
let
val vars' = intro_vars (the_list v) vars;
in
concat [
Pretty.block [str "(", print_typed tyvars (print_var vars' v) ty, str ")"],
str "=>",
- print_term tyvars false thm vars' NOBR t
+ print_term tyvars false some_thm vars' NOBR t
]
end
- | print_term tyvars is_pat thm vars fxy (ICase (cases as (_, t0))) =
+ | print_term tyvars is_pat some_thm vars fxy (ICase (cases as (_, t0))) =
(case Code_Thingol.unfold_const_app t0
of SOME (c_ts as ((c, _), _)) => if is_none (syntax_const c)
- then print_case tyvars thm vars fxy cases
- else print_app tyvars is_pat thm vars fxy c_ts
- | NONE => print_case tyvars thm vars fxy cases)
- and print_app tyvars is_pat thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
+ then print_case tyvars some_thm vars fxy cases
+ else print_app tyvars is_pat some_thm vars fxy c_ts
+ | NONE => print_case tyvars some_thm vars fxy cases)
+ and print_app tyvars is_pat some_thm vars fxy (app as ((c, ((tys, _), tys_args)), ts)) =
let
val k = length ts;
val l = case syntax_const c of NONE => args_num c | SOME (l, _) => l;
@@ -69,47 +69,47 @@
val (no_syntax, print') = case syntax_const c
of NONE => (true, fn ts => applify "(" ")" fxy
(applify "[" "]" NOBR ((str o deresolve) c) (map (print_typ tyvars NOBR) tys'))
- (map (print_term tyvars is_pat thm vars NOBR) ts))
+ (map (print_term tyvars is_pat some_thm vars NOBR) ts))
| SOME (_, print) => (false, fn ts =>
- print (print_term tyvars is_pat thm) thm vars fxy (ts ~~ take l tys_args));
+ print (print_term tyvars is_pat some_thm) some_thm vars fxy (ts ~~ take l tys_args));
in if k = l then print' ts
else if k < l then
- print_term tyvars is_pat thm vars fxy (Code_Thingol.eta_expand l app)
+ print_term tyvars is_pat some_thm vars fxy (Code_Thingol.eta_expand l app)
else let
val (ts1, ts23) = chop l ts;
in
Pretty.block (print' ts1 :: map (fn t => Pretty.block
- [str ".apply(", print_term tyvars is_pat thm vars NOBR t, str ")"]) ts23)
+ [str ".apply(", print_term tyvars is_pat some_thm vars NOBR t, str ")"]) ts23)
end end
- and print_bind tyvars thm fxy p = gen_print_bind (print_term tyvars true) thm fxy p
- and print_case tyvars thm vars fxy (cases as ((_, [_]), _)) =
+ and print_bind tyvars some_thm fxy p = gen_print_bind (print_term tyvars true) some_thm fxy p
+ and print_case tyvars some_thm vars fxy (cases as ((_, [_]), _)) =
let
val (binds, body) = Code_Thingol.unfold_let (ICase cases);
fun print_match ((pat, ty), t) vars =
vars
- |> print_bind tyvars thm BR pat
+ |> print_bind tyvars some_thm BR pat
|>> (fn p => semicolon [Pretty.block [str "val", Pretty.brk 1, p,
str ":", Pretty.brk 1, print_typ tyvars NOBR ty],
- str "=", print_term tyvars false thm vars NOBR t])
+ str "=", print_term tyvars false some_thm vars NOBR t])
val (ps, vars') = fold_map print_match binds vars;
in
brackify_block fxy
(str "{")
- (ps @| print_term tyvars false thm vars' NOBR body)
+ (ps @| print_term tyvars false some_thm vars' NOBR body)
(str "}")
end
- | print_case tyvars thm vars fxy (((t, ty), clauses as _ :: _), _) =
+ | print_case tyvars some_thm vars fxy (((t, ty), clauses as _ :: _), _) =
let
fun print_select (pat, body) =
let
- val (p, vars') = print_bind tyvars thm NOBR pat vars;
- in concat [str "case", p, str "=>", print_term tyvars false thm vars' NOBR body] end;
+ val (p, vars') = print_bind tyvars some_thm NOBR pat vars;
+ in concat [str "case", p, str "=>", print_term tyvars false some_thm vars' NOBR body] end;
in brackify_block fxy
- (concat [print_term tyvars false thm vars NOBR t, str "match", str "{"])
+ (concat [print_term tyvars false some_thm vars NOBR t, str "match", str "{"])
(map print_select clauses)
(str "}")
end
- | print_case tyvars thm vars fxy ((_, []), _) =
+ | print_case tyvars some_thm vars fxy ((_, []), _) =
(brackify fxy o Pretty.breaks o map str) ["error(\"empty case\")"];
fun implicit_arguments tyvars vs vars =
let
@@ -140,7 +140,7 @@
end
| eqs =>
let
- val tycos = fold (fn ((ts, t), (thm, _)) =>
+ val tycos = fold (fn ((ts, t), _) =>
fold Code_Thingol.add_tyconames (t :: ts)) eqs [];
val tyvars = reserved
|> intro_base_names
@@ -164,12 +164,12 @@
(fn (ty1, ty2) => Code_Thingol.fun_tyco `%% [ty1, ty2]) (tys2, ty1);
fun print_tuple [p] = p
| print_tuple ps = enum "," "(" ")" ps;
- fun print_rhs vars' ((_, t), (thm, _)) = print_term tyvars false thm vars' NOBR t;
- fun print_clause (eq as ((ts, _), (thm, _))) =
+ fun print_rhs vars' ((_, t), (some_thm, _)) = print_term tyvars false some_thm vars' NOBR t;
+ fun print_clause (eq as ((ts, _), (some_thm, _))) =
let
val vars' = intro_vars ((fold o Code_Thingol.fold_varnames) (insert (op =)) ts []) vars2;
in
- concat [str "case", print_tuple (map (print_term tyvars true thm vars' NOBR) ts),
+ concat [str "case", print_tuple (map (print_term tyvars true some_thm vars' NOBR) ts),
str "=>", print_rhs vars' eq]
end;
val head = print_defhead tyvars vars3 ((str o deresolve) name) vs params tys1 implicit_ps ty2;
@@ -267,7 +267,7 @@
auxs tys), str "=>"]];
in
concat ([str "val", (str o suffix "$" o deresolve_base) classparam,
- str "="] @ args @ [print_app tyvars false thm vars NOBR (const, map (IVar o SOME) auxs)])
+ str "="] @ args @ [print_app tyvars false (SOME thm) vars NOBR (const, map (IVar o SOME) auxs)])
end;
in
Pretty.chunks [
@@ -352,15 +352,15 @@
of Code_Thingol.Fun (_, ((_, ty), [])) => (length o fst o Code_Thingol.unfold_fun) ty
| Code_Thingol.Fun (_, (_, ((ts, _), _) :: _)) => length ts
| Code_Thingol.Datatypecons (_, tyco) =>
- let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
- in (length o the o AList.lookup (op =) dtcos) c end
+ let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
+ in (length o the o AList.lookup (op =) constrs) c end
| Code_Thingol.Classparam (_, class) =>
let val Code_Thingol.Class (_, (_, (_, classparams))) = Graph.get_node program class
in (length o fst o Code_Thingol.unfold_fun o the o AList.lookup (op =) classparams) c end;
fun is_singleton c = case Graph.get_node program c
of Code_Thingol.Datatypecons (_, tyco) =>
- let val Code_Thingol.Datatype (_, (_, dtcos)) = Graph.get_node program tyco
- in (null o the o AList.lookup (op =) dtcos) c end
+ let val Code_Thingol.Datatype (_, (_, constrs)) = Graph.get_node program tyco
+ in (null o the o AList.lookup (op =) constrs) c end
| _ => false;
val print_stmt = print_scala_stmt labelled_name syntax_tyco syntax_const
reserved args_num is_singleton deresolver;