--- a/etc/isar-keywords.el Fri Feb 19 13:54:19 2010 +0100
+++ b/etc/isar-keywords.el Fri Feb 19 16:42:37 2010 +0100
@@ -55,6 +55,7 @@
"classes"
"classrel"
"code_abort"
+ "code_abstype"
"code_class"
"code_const"
"code_datatype"
@@ -537,6 +538,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
"boogie_vc"
+ "code_abstype"
"code_pred"
"corollary"
"cpodef"
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Fri Feb 19 16:42:37 2010 +0100
@@ -314,9 +314,7 @@
else false
*)
-(* must be exported in code.ML *)
-(* TODO: is there copy in the core? *)
-fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
+val is_constr = Code.is_constr;
fun strip_ex (Const ("Ex", _) $ Abs (x, T, t)) =
let
--- a/src/HOL/Tools/recfun_codegen.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Feb 19 16:42:37 2010 +0100
@@ -44,9 +44,7 @@
let
val c = AxClass.unoverload_const thy (raw_c, T);
val raw_thms = Code.get_cert thy (Code_Preproc.preprocess_functrans thy) c
- |> Code.equations_thms_cert thy
- |> snd
- |> map_filter (fn (_, (thm, proper)) => if proper then SOME thm else NONE)
+ |> Code.bare_thms_of_cert thy
|> map (AxClass.overload thy)
|> filter (is_instance T o snd o const_of o prop_of);
val module_name = case Symtab.lookup (ModuleData.get thy) c
--- a/src/Pure/Isar/code.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Pure/Isar/code.ML Fri Feb 19 16:42:37 2010 +0100
@@ -22,6 +22,8 @@
(*constructor sets*)
val constrset_of_consts: theory -> (string * typ) list
-> string * ((string * sort) list * (string * typ list) list)
+ val abstype_cert: theory -> string * typ -> string
+ -> string * ((string * sort) list * ((string * typ) * (string * term)))
(*code equations and certificates*)
val mk_eqn: theory -> thm * bool -> thm * bool
@@ -34,9 +36,10 @@
val empty_cert: theory -> string -> cert
val cert_of_eqns: theory -> string -> (thm * bool) list -> cert
val constrain_cert: theory -> sort list -> cert -> cert
- val typscheme_cert: theory -> cert -> (string * sort) list * typ
- val equations_cert: theory -> cert -> ((string * sort) list * typ) * (term list * term) list
- val equations_thms_cert: theory -> cert -> ((string * sort) list * typ) * ((term list * term) * (thm * bool)) list
+ val typargs_deps_of_cert: theory -> cert -> (string * sort) list * (string * typ list) list
+ val equations_of_cert: theory -> cert ->
+ ((string * sort) list * typ) * ((string option * (term list * term)) * (thm option * bool)) list
+ val bare_thms_of_cert: theory -> cert -> thm list
val pretty_cert: theory -> cert -> Pretty.T list
(*executable code*)
@@ -46,6 +49,8 @@
val add_signature_cmd: string * string -> theory -> theory
val add_datatype: (string * typ) list -> theory -> theory
val add_datatype_cmd: string list -> theory -> theory
+ val add_abstype: string * typ -> string * typ -> theory -> Proof.state
+ val add_abstype_cmd: string -> string -> theory -> Proof.state
val type_interpretation:
(string * ((string * sort) list * (string * typ list) list)
-> theory -> theory) -> theory -> theory
@@ -59,7 +64,9 @@
val add_case: thm -> theory -> theory
val add_undefined: string -> theory -> theory
val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list)
- val get_datatype_of_constr: theory -> string -> string option
+ val get_datatype_of_constr_or_abstr: theory -> string -> (string * bool) option
+ val is_constr: theory -> string -> bool
+ val is_abstr: theory -> string -> bool
val get_cert: theory -> ((thm * bool) list -> (thm * bool) list) -> string -> cert
val get_case_scheme: theory -> string -> (int * (int * string list)) option
val undefineds: theory -> string list
@@ -122,34 +129,31 @@
fun read_const thy = AxClass.unoverload_const thy o read_bare_const thy;
-
(** data store **)
-(* code equations *)
+(* datatypes *)
+
+datatype typ_spec = Constructors of (string * typ list) list
+ | Abstractor of (string * typ) * (string * thm);
-type eqns = bool * (thm * bool) list;
- (*default flag, theorems with proper flag *)
+fun constructors_of (Constructors cos) = (cos, false)
+ | constructors_of (Abstractor ((co, ty), _)) = ([(co, [ty])], true);
+
+
+(* functions *)
-fun add_drop_redundant thy (thm, proper) thms =
- let
- val args_of = snd o strip_comb o map_types Type.strip_sorts
- o fst o Logic.dest_equals o Thm.plain_prop_of;
- val args = args_of thm;
- val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
- fun matches_args args' = length args <= length args' andalso
- Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
- fun drop (thm', proper') = if (proper orelse not proper')
- andalso matches_args (args_of thm') then
- (warning ("Code generator: dropping redundant code equation\n" ^
- Display.string_of_thm_global thy thm'); true)
- else false;
- in (thm, proper) :: filter_out drop thms end;
+datatype fun_spec = Default of (thm * bool) list
+ | Eqns of (thm * bool) list
+ | Proj of term * string
+ | Abstr of thm * string;
-fun add_thm thy _ thm (false, thms) = (false, add_drop_redundant thy thm thms)
- | add_thm thy true thm (true, thms) = (true, thms @ [thm])
- | add_thm thy false thm (true, thms) = (false, [thm]);
+val empty_fun_spec = Default [];
-fun del_thm thm = apsnd (remove (eq_fst Thm.eq_thm_prop) (thm, true));
+fun is_default (Default _) = true
+ | is_default _ = false;
+
+fun associated_abstype (Abstr (_, tyco)) = SOME tyco
+ | associated_abstype _ = NONE;
(* executable code data *)
@@ -157,49 +161,49 @@
datatype spec = Spec of {
history_concluded: bool,
signatures: int Symtab.table * typ Symtab.table,
- eqns: ((bool * eqns) * (serial * eqns) list) Symtab.table
+ functions: ((bool * fun_spec) * (serial * fun_spec) list) Symtab.table
(*with explicit history*),
- dtyps: ((serial * ((string * sort) list * (string * typ list) list)) list) Symtab.table
+ datatypes: ((serial * ((string * sort) list * typ_spec)) list) Symtab.table
(*with explicit history*),
cases: (int * (int * string list)) Symtab.table * unit Symtab.table
};
-fun make_spec (history_concluded, ((signatures, eqns), (dtyps, cases))) =
+fun make_spec (history_concluded, ((signatures, functions), (datatypes, cases))) =
Spec { history_concluded = history_concluded,
- signatures = signatures, eqns = eqns, dtyps = dtyps, cases = cases };
+ signatures = signatures, functions = functions, datatypes = datatypes, cases = cases };
fun map_spec f (Spec { history_concluded = history_concluded, signatures = signatures,
- eqns = eqns, dtyps = dtyps, cases = cases }) =
- make_spec (f (history_concluded, ((signatures, eqns), (dtyps, cases))));
-fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), eqns = eqns1,
- dtyps = dtyps1, cases = (cases1, undefs1) },
- Spec { history_concluded = _, signatures = (tycos2, sigs2), eqns = eqns2,
- dtyps = dtyps2, cases = (cases2, undefs2) }) =
+ functions = functions, datatypes = datatypes, cases = cases }) =
+ make_spec (f (history_concluded, ((signatures, functions), (datatypes, cases))));
+fun merge_spec (Spec { history_concluded = _, signatures = (tycos1, sigs1), functions = functions1,
+ datatypes = datatypes1, cases = (cases1, undefs1) },
+ Spec { history_concluded = _, signatures = (tycos2, sigs2), functions = functions2,
+ datatypes = datatypes2, cases = (cases2, undefs2) }) =
let
val signatures = (Symtab.merge (op =) (tycos1, tycos2),
Symtab.merge typ_equiv (sigs1, sigs2));
- fun merge_eqns ((_, history1), (_, history2)) =
+ fun merge_functions ((_, history1), (_, history2)) =
let
val raw_history = AList.merge (op = : serial * serial -> bool)
- (K true) (history1, history2)
- val filtered_history = filter_out (fst o snd) raw_history
+ (K true) (history1, history2);
+ val filtered_history = filter_out (is_default o snd) raw_history;
val history = if null filtered_history
then raw_history else filtered_history;
in ((false, (snd o hd) history), history) end;
- val eqns = Symtab.join (K merge_eqns) (eqns1, eqns2);
- val dtyps = Symtab.join (K (AList.merge (op =) (K true))) (dtyps1, dtyps2);
+ val functions = Symtab.join (K merge_functions) (functions1, functions2);
+ val datatypes = Symtab.join (K (AList.merge (op =) (K true))) (datatypes1, datatypes2);
val cases = (Symtab.merge (K true) (cases1, cases2),
Symtab.merge (K true) (undefs1, undefs2));
- in make_spec (false, ((signatures, eqns), (dtyps, cases))) end;
+ in make_spec (false, ((signatures, functions), (datatypes, cases))) end;
fun history_concluded (Spec { history_concluded, ... }) = history_concluded;
fun the_signatures (Spec { signatures, ... }) = signatures;
-fun the_eqns (Spec { eqns, ... }) = eqns;
-fun the_dtyps (Spec { dtyps, ... }) = dtyps;
+fun the_functions (Spec { functions, ... }) = functions;
+fun the_datatypes (Spec { datatypes, ... }) = datatypes;
fun the_cases (Spec { cases, ... }) = cases;
val map_history_concluded = map_spec o apfst;
val map_signatures = map_spec o apsnd o apfst o apfst;
-val map_eqns = map_spec o apsnd o apfst o apsnd;
-val map_dtyps = map_spec o apsnd o apsnd o apfst;
+val map_functions = map_spec o apsnd o apfst o apsnd;
+val map_typs = map_spec o apsnd o apsnd o apfst;
val map_cases = map_spec o apsnd o apsnd o apsnd;
@@ -251,6 +255,7 @@
in
+
(* access to executable code *)
val the_exec = fst o Code_Data.get;
@@ -259,9 +264,9 @@
val purge_data = (Code_Data.map o apsnd) (fn _ => empty_dataref ());
-fun change_eqns delete c f = (map_exec_purge o map_eqns
- o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, [])), [])))
- o apfst) (fn (_, eqns) => (true, f eqns));
+fun change_fun_spec delete c f = (map_exec_purge o map_functions
+ o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, empty_fun_spec), [])))
+ o apfst) (fn (_, spec) => (true, f spec));
(* tackling equation history *)
@@ -276,7 +281,7 @@
then NONE
else thy
|> (Code_Data.map o apfst)
- ((map_eqns o Symtab.map) (fn ((changed, current), history) =>
+ ((map_functions o Symtab.map) (fn ((changed, current), history) =>
((false, current),
if changed then (serial (), current) :: history else history))
#> map_history_concluded (K true))
@@ -359,29 +364,32 @@
(* datatypes *)
-fun constrset_of_consts thy cs =
+fun no_constr thy s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
+ ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
+
+fun ty_sorts thy (c, raw_ty) =
let
- val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
- then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
- fun no_constr s (c, ty) = error ("Not a datatype constructor:\n" ^ string_of_const thy c
- ^ " :: " ^ string_of_typ thy ty ^ "\n" ^ enclose "(" ")" s);
+ val _ = Thm.cterm_of thy (Const (c, raw_ty));
+ val ty = subst_signature thy c raw_ty;
+ val ty_decl = (Logic.unvarifyT o const_typ thy) c;
fun last_typ c_ty ty =
let
val tfrees = Term.add_tfreesT ty [];
val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) ty
- handle TYPE _ => no_constr "bad type" c_ty
+ handle TYPE _ => no_constr thy "bad type" c_ty
val _ = if has_duplicates (eq_fst (op =)) vs
- then no_constr "duplicate type variables in datatype" c_ty else ();
+ then no_constr thy "duplicate type variables in datatype" c_ty else ();
val _ = if length tfrees <> length vs
- then no_constr "type variables missing in datatype" c_ty else ();
+ then no_constr thy "type variables missing in datatype" c_ty else ();
in (tyco, vs) end;
- fun ty_sorts (c, raw_ty) =
- let
- val ty = subst_signature thy c raw_ty;
- val ty_decl = (Logic.unvarifyT o const_typ thy) c;
- val (tyco, _) = last_typ (c, ty) ty_decl;
- val (_, vs) = last_typ (c, ty) ty;
- in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
+ val (tyco, _) = last_typ (c, ty) ty_decl;
+ val (_, vs) = last_typ (c, ty) ty;
+ in ((tyco, map snd vs), (c, (map fst vs, ty))) end;
+
+fun constrset_of_consts thy cs =
+ let
+ val _ = map (fn (c, _) => if (is_some o AxClass.class_of_param thy) c
+ then error ("Is a class parameter: " ^ string_of_const thy c) else ()) cs;
fun add ((tyco', sorts'), c) ((tyco, sorts), cs) =
let
val _ = if (tyco' : string) <> tyco
@@ -394,31 +402,68 @@
val the_v = the o AList.lookup (op =) (vs ~~ vs');
val ty' = map_atyps (fn TFree (v, _) => TFree (the_v v)) ty;
in (c, (fst o strip_type) ty') end;
- val c' :: cs' = map ty_sorts cs;
+ val c' :: cs' = map (ty_sorts thy) cs;
val ((tyco, sorts), cs'') = fold add cs' (apsnd single c');
val vs = Name.names Name.context Name.aT sorts;
val cs''' = map (inst vs) cs'';
in (tyco, (vs, rev cs''')) end;
-fun get_datatype thy tyco =
- case these (Symtab.lookup ((the_dtyps o the_exec) thy) tyco)
- of (_, spec) :: _ => spec
- | [] => arity_number thy tyco
- |> Name.invents Name.context Name.aT
- |> map (rpair [])
- |> rpair [];
+fun abstype_cert thy abs_ty rep =
+ let
+ val _ = pairself (fn c => if (is_some o AxClass.class_of_param thy) c
+ then error ("Is a class parameter: " ^ string_of_const thy c) else ()) (fst abs_ty, rep);
+ val ((tyco, sorts), (abs, (vs, ty'))) = ty_sorts thy abs_ty;
+ val (ty, ty_abs) = case ty'
+ of Type ("fun", [ty, ty_abs]) => (ty, ty_abs)
+ | _ => error ("Not a datatype abstractor:\n" ^ string_of_const thy abs
+ ^ " :: " ^ string_of_typ thy ty');
+ val _ = Thm.cterm_of thy (Const (rep, ty_abs --> ty)) handle CTERM _ =>
+ error ("Not a projection:\n" ^ string_of_const thy rep);
+ val cert = Logic.mk_equals (Const (abs, ty --> ty_abs) $ (Const (rep, ty_abs --> ty)
+ $ Free ("x", ty_abs)), Free ("x", ty_abs));
+ in (tyco, (vs ~~ sorts, ((fst abs_ty, ty), (rep, cert)))) end;
+
+fun get_datatype_entry thy tyco = case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
+ of (_, entry) :: _ => SOME entry
+ | _ => NONE;
-fun get_datatype_of_constr thy c =
+fun get_datatype_spec thy tyco = case get_datatype_entry thy tyco
+ of SOME (vs, spec) => apfst (pair vs) (constructors_of spec)
+ | NONE => arity_number thy tyco
+ |> Name.invents Name.context Name.aT
+ |> map (rpair [])
+ |> rpair []
+ |> rpair false;
+
+fun get_abstype_spec thy tyco = case get_datatype_entry thy tyco
+ of SOME (vs, Abstractor spec) => (vs, spec)
+ | NONE => error ("Not an abstract type: " ^ tyco);
+
+fun get_datatype thy = fst o get_datatype_spec thy;
+
+fun get_datatype_of_constr_or_abstr thy c =
case (snd o strip_type o const_typ thy) c
- of Type (tyco, _) => if member (op =) ((map fst o snd o get_datatype thy) tyco) c
- then SOME tyco else NONE
+ of Type (tyco, _) => let val ((vs, cos), abstract) = get_datatype_spec thy tyco
+ in if member (op =) (map fst cos) c then SOME (tyco, abstract) else NONE end
| _ => NONE;
-fun is_constr thy = is_some o get_datatype_of_constr thy;
+fun is_constr thy c = case get_datatype_of_constr_or_abstr thy c
+ of SOME (_, false) => true
+ | _ => false;
+
+fun is_abstr thy c = case get_datatype_of_constr_or_abstr thy c
+ of SOME (_, true) => true
+ | _ => false;
(* bare code equations *)
+(* convention for variables:
+ ?x ?'a for free-floating theorems (e.g. in the data store)
+ ?x 'a for certificates
+ x 'a for final representation of equations
+*)
+
exception BAD_THM of string;
fun bad_thm msg = raise BAD_THM msg;
fun error_thm f thm = f thm handle BAD_THM msg => error msg;
@@ -430,12 +475,9 @@
in not (has_duplicates (op =) ((fold o fold_aterms)
(fn Var (v, _) => cons v | _ => I) args [])) end;
-fun gen_assert_eqn thy check_patterns (thm, proper) =
+fun check_eqn thy { allow_nonlinear, allow_consts, allow_pats } thm (lhs, rhs) =
let
fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
- val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
- handle TERM _ => bad "Not an equation"
- | THM _ => bad "Not an equation";
fun vars_of t = fold_aterms (fn Var (v, _) => insert (op =) v
| Free _ => bad "Illegal free variable in equation"
| _ => I) t [];
@@ -461,21 +503,23 @@
| check _ (Var _) = bad "Variable with application on left hand side of equation"
| check n (t1 $ t2) = (check (n+1) t1; check 0 t2)
| check n (Const (c_ty as (c, ty))) =
- let
+ if allow_pats then let
val c' = AxClass.unoverload_const thy c_ty
in if n = (length o fst o strip_type o subst_signature thy c') ty
- then if not proper orelse not check_patterns orelse is_constr thy c'
+ then if allow_consts orelse is_constr thy c'
then ()
else bad (quote c ^ " is not a constructor, on left hand side of equation")
else bad ("Partially applied constant " ^ quote c ^ " on left hand side of equation")
- end;
+ end else bad ("Pattern not allowed, but constant " ^ quote c ^ " encountered on left hand side")
val _ = map (check 0) args;
- val _ = if not proper orelse is_linear thm then ()
+ val _ = if allow_nonlinear orelse is_linear thm then ()
else bad "Duplicate variables on left hand side of equation";
val _ = if (is_none o AxClass.class_of_param thy) c then ()
else bad "Overloaded constant as head in equation";
val _ = if not (is_constr thy c) then ()
else bad "Constructor as head in equation";
+ val _ = if not (is_abstr thy c) then ()
+ else bad "Abstractor as head in equation";
val ty_decl = Sign.the_const_type thy c;
val _ = if Sign.typ_equiv thy (Type.strip_sorts ty_decl, Type.strip_sorts ty)
then () else bad_thm ("Type\n" ^ string_of_typ thy ty
@@ -483,8 +527,39 @@
^ Display.string_of_thm_global thy thm
^ "\nis incompatible with declared function type\n"
^ string_of_typ thy ty_decl)
+ in () end;
+
+fun gen_assert_eqn thy check_patterns (thm, proper) =
+ let
+ fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
+ val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
+ handle TERM _ => bad "Not an equation"
+ | THM _ => bad "Not a proper equation";
+ val _ = check_eqn thy { allow_nonlinear = not proper,
+ allow_consts = not (proper andalso check_patterns), allow_pats = true } thm (lhs, rhs);
in (thm, proper) end;
+fun assert_abs_eqn thy some_tyco thm =
+ let
+ fun bad s = bad_thm (s ^ ":\n" ^ Display.string_of_thm_global thy thm);
+ val (full_lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm
+ handle TERM _ => bad "Not an equation"
+ | THM _ => bad "Not a proper equation";
+ val (rep, lhs) = dest_comb full_lhs
+ handle TERM _ => bad "Not an abstract equation";
+ val tyco = (fst o dest_Type o domain_type o snd o dest_Const) rep
+ handle TERM _ => bad "Not an abstract equation";
+ val _ = case some_tyco of SOME tyco' => if tyco = tyco' then ()
+ else bad ("Abstract type mismatch:" ^ quote tyco ^ " vs. " ^ quote tyco')
+ | NONE => ();
+ val (_, (_, (rep', _))) = get_abstype_spec thy tyco;
+ val rep_const = (fst o dest_Const) rep;
+ val _ = if rep_const = rep' then ()
+ else bad ("Projection mismatch: " ^ quote rep_const ^ " vs. " ^ quote rep');
+ val _ = check_eqn thy { allow_nonlinear = false,
+ allow_consts = false, allow_pats = false } thm (lhs, rhs);
+ in (thm, tyco) end;
+
fun assert_eqn thy = error_thm (gen_assert_eqn thy true);
fun meta_rewrite thy = LocalDefs.meta_rewrite_rule (ProofContext.init thy);
@@ -498,6 +573,8 @@
fun mk_eqn_liberal thy = Option.map (fn (thm, _) => (thm, is_linear thm))
o try_thm (gen_assert_eqn thy false) o rpair false o meta_rewrite thy;
+fun mk_abs_eqn thy = error_thm (assert_abs_eqn thy NONE) o meta_rewrite thy;
+
val head_eqn = dest_Const o fst o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
fun const_typ_eqn thy thm =
@@ -509,11 +586,20 @@
fun const_eqn thy = fst o const_typ_eqn thy;
+fun const_abs_eqn thy = AxClass.unoverload_const thy o dest_Const o fst o strip_comb o snd
+ o dest_comb o fst o Logic.dest_equals o Thm.plain_prop_of;
+
fun logical_typscheme thy (c, ty) =
(map dest_TFree (Sign.const_typargs thy (c, ty)), Type.strip_sorts ty);
fun typscheme thy (c, ty) = logical_typscheme thy (c, subst_signature thy c ty);
+fun mk_proj tyco vs ty abs rep =
+ let
+ val ty_abs = Type (tyco, map TFree vs);
+ val xarg = Var (("x", 0), ty);
+ in Logic.mk_equals (Const (rep, ty_abs --> ty) $ (Const (abs, ty --> ty_abs) $ xarg), xarg) end;
+
(* technical transformations of code equations *)
@@ -578,7 +664,50 @@
val (_, Const (c, ty)) = (Logic.dest_equals o Thm.term_of) head;
in (typscheme thy (c, ty), head) end;
-abstype cert = Cert of thm * bool list with
+fun typscheme_projection thy =
+ typscheme thy o dest_Const o fst o dest_comb o fst o Logic.dest_equals;
+
+fun typscheme_abs thy =
+ typscheme thy o dest_Const o fst o strip_comb o snd o dest_comb o fst o Logic.dest_equals o Thm.prop_of;
+
+fun constrain_thm thy vs sorts thm =
+ let
+ val mapping = map2 (fn (v, sort) => fn sort' =>
+ (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
+ val inst = map2 (fn (v, sort) => fn (_, sort') =>
+ (((v, 0), sort), TFree (v, sort'))) vs mapping;
+ val subst = (map_types o map_atyps)
+ (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) mapping v)));
+ in
+ thm
+ |> Thm.varifyT
+ |> Thm.certify_instantiate (inst, [])
+ |> pair subst
+ end;
+
+fun concretify_abs thy tyco abs_thm =
+ let
+ val (vs, ((c, _), (_, cert))) = get_abstype_spec thy tyco;
+ val lhs = (fst o Logic.dest_equals o Thm.prop_of) abs_thm
+ val ty = fastype_of lhs;
+ val ty_abs = (fastype_of o snd o dest_comb) lhs;
+ val abs = Thm.cterm_of thy (Const (c, ty --> ty_abs));
+ val raw_concrete_thm = Drule.transitive_thm OF [Thm.symmetric cert, Thm.combination (Thm.reflexive abs) abs_thm];
+ in (c, (Thm.varifyT o zero_var_indexes) raw_concrete_thm) end;
+
+fun add_rhss_of_eqn thy t =
+ let
+ val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy) t;
+ fun add_const (Const (c, ty)) = insert (op =) (c, Sign.const_typargs thy (c, ty))
+ | add_const _ = I
+ in fold_aterms add_const t end;
+
+fun dest_eqn thy = apfst (snd o strip_comb) o Logic.dest_equals o subst_signatures thy o Logic.unvarify;
+
+abstype cert = Equations of thm * bool list
+ | Projection of term * string
+ | Abstract of thm * string
+with
fun empty_cert thy c =
let
@@ -590,7 +719,7 @@
|> map (fn v => TFree (v, []));
val ty = typ_subst_TVars (tvars ~~ tvars') raw_ty;
val chead = build_head thy (c, ty);
- in Cert (Thm.weaken chead Drule.dummy_thm, []) end;
+ in Equations (Thm.weaken chead Drule.dummy_thm, []) end;
fun cert_of_eqns thy c [] = empty_cert thy c
| cert_of_eqns thy c raw_eqns =
@@ -615,65 +744,127 @@
else Conv.rewr_conv head_thm ct;
val rewrite_head = Conv.fconv_rule (Conv.arg1_conv head_conv);
val cert_thm = Conjunction.intr_balanced (map rewrite_head thms);
- in Cert (cert_thm, propers) end;
+ in Equations (cert_thm, propers) end;
-fun constrain_cert thy sorts (Cert (cert_thm, propers)) =
+fun cert_of_proj thy c tyco =
+ let
+ val (vs, ((abs, ty), (rep, cert))) = get_abstype_spec thy tyco;
+ val _ = if c = rep then () else
+ error ("Wrong head of projection,\nexpected constant " ^ string_of_const thy rep);
+ in Projection (mk_proj tyco vs ty abs rep, tyco) end;
+
+fun cert_of_abs thy tyco c raw_abs_thm =
let
- val ((vs, _), head) = get_head thy cert_thm;
- val subst = map2 (fn (v, sort) => fn sort' =>
- (v, Sorts.inter_sort (Sign.classes_of thy) (sort, sort'))) vs sorts;
- val head' = Thm.term_of head
- |> (map_types o map_atyps)
- (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) subst v)))
- |> Thm.cterm_of thy;
- val inst = map2 (fn (v, sort) => fn (_, sort') =>
- (((v, 0), sort), TFree (v, sort'))) vs subst;
- val cert_thm' = cert_thm
- |> Thm.implies_intr head
- |> Thm.varifyT
- |> Thm.certify_instantiate (inst, [])
- |> Thm.elim_implies (Thm.assume head');
- in (Cert (cert_thm', propers)) end;
+ val abs_thm = singleton (canonize_thms thy) raw_abs_thm;
+ val _ = assert_abs_eqn thy (SOME tyco) abs_thm;
+ val _ = if c = const_abs_eqn thy abs_thm then ()
+ else error ("Wrong head of abstract code equation,\nexpected constant "
+ ^ string_of_const thy c ^ "\n" ^ Display.string_of_thm_global thy abs_thm);
+ in Abstract (Thm.freezeT abs_thm, tyco) end;
-fun typscheme_cert thy (Cert (cert_thm, _)) =
- fst (get_head thy cert_thm);
+fun constrain_cert thy sorts (Equations (cert_thm, propers)) =
+ let
+ val ((vs, _), head) = get_head thy cert_thm;
+ val (subst, cert_thm') = cert_thm
+ |> Thm.implies_intr head
+ |> constrain_thm thy vs sorts;
+ val head' = Thm.term_of head
+ |> subst
+ |> Thm.cterm_of thy;
+ val cert_thm'' = cert_thm'
+ |> Thm.elim_implies (Thm.assume head');
+ in Equations (cert_thm'', propers) end
+ | constrain_cert thy _ (cert as Projection _) =
+ cert
+ | constrain_cert thy sorts (Abstract (abs_thm, tyco)) =
+ Abstract (snd (constrain_thm thy (fst (typscheme_abs thy abs_thm)) sorts abs_thm), tyco);
+
+fun typscheme_of_cert thy (Equations (cert_thm, _)) =
+ fst (get_head thy cert_thm)
+ | typscheme_of_cert thy (Projection (proj, _)) =
+ typscheme_projection thy proj
+ | typscheme_of_cert thy (Abstract (abs_thm, _)) =
+ typscheme_abs thy abs_thm;
-fun equations_cert thy (cert as Cert (cert_thm, propers)) =
- let
- val tyscm = typscheme_cert thy cert;
- val equations = if null propers then [] else
- Thm.prop_of cert_thm
- |> Logic.dest_conjunction_balanced (length propers)
- |> map Logic.dest_equals
- |> (map o apfst) (snd o strip_comb)
- in (tyscm, equations) end;
+fun typargs_deps_of_cert thy (Equations (cert_thm, propers)) =
+ let
+ val vs = (fst o fst) (get_head thy cert_thm);
+ val equations = if null propers then [] else
+ Thm.prop_of cert_thm
+ |> Logic.dest_conjunction_balanced (length propers);
+ in (vs, fold (add_rhss_of_eqn thy) equations []) end
+ | typargs_deps_of_cert thy (Projection (t, tyco)) =
+ (fst (typscheme_projection thy t), add_rhss_of_eqn thy t [])
+ | typargs_deps_of_cert thy (Abstract (abs_thm, tyco)) =
+ let
+ val vs = fst (typscheme_abs thy abs_thm);
+ val (_, concrete_thm) = concretify_abs thy tyco abs_thm;
+ in (vs, add_rhss_of_eqn thy (Thm.prop_of abs_thm) []) end;
-fun equations_thms_cert thy (cert as Cert (cert_thm, propers)) =
- let
- val (tyscm, equations) = equations_cert thy cert;
- val thms = if null propers then [] else
- cert_thm
- |> LocalDefs.expand [snd (get_head thy cert_thm)]
- |> Thm.varifyT
- |> Conjunction.elim_balanced (length propers)
- in (tyscm, equations ~~ (thms ~~ propers)) end;
+fun equations_of_cert thy (cert as Equations (cert_thm, propers)) =
+ let
+ val tyscm = typscheme_of_cert thy cert;
+ val thms = if null propers then [] else
+ cert_thm
+ |> LocalDefs.expand [snd (get_head thy cert_thm)]
+ |> Thm.varifyT
+ |> Conjunction.elim_balanced (length propers);
+ in (tyscm, map (pair NONE o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
+ | equations_of_cert thy (Projection (t, tyco)) =
+ let
+ val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
+ val tyscm = typscheme_projection thy t;
+ val t' = map_types Logic.varifyT t;
+ in (tyscm, [((SOME abs, dest_eqn thy t'), (NONE, true))]) end
+ | equations_of_cert thy (Abstract (abs_thm, tyco)) =
+ let
+ val tyscm = typscheme_abs thy abs_thm;
+ val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
+ val _ = fold_aterms (fn Const (c, _) => if c = abs
+ then error ("Abstraction violation in abstract code equation\n" ^ Display.string_of_thm_global thy abs_thm)
+ else I | _ => I) (Thm.prop_of abs_thm);
+ in (tyscm, [((SOME abs, dest_eqn thy (Thm.prop_of concrete_thm)), (SOME (Thm.varifyT abs_thm), true))]) end;
-fun pretty_cert thy = map (Display.pretty_thm_global thy o AxClass.overload thy o fst o snd)
- o snd o equations_thms_cert thy;
+fun pretty_cert thy (cert as Equations _) =
+ (map_filter (Option.map (Display.pretty_thm_global thy o AxClass.overload thy) o fst o snd)
+ o snd o equations_of_cert thy) cert
+ | pretty_cert thy (Projection (t, _)) =
+ [Syntax.pretty_term_global thy (map_types Logic.varifyT t)]
+ | pretty_cert thy (Abstract (abs_thm, tyco)) =
+ [(Display.pretty_thm_global thy o AxClass.overload thy o Thm.varifyT) abs_thm];
+
+fun bare_thms_of_cert thy (cert as Equations _) =
+ (map_filter (fn (_, (some_thm, proper)) => if proper then some_thm else NONE)
+ o snd o equations_of_cert thy) cert
+ | bare_thms_of_cert thy _ = [];
end;
-(* code equation access *)
+(* code certificate access *)
+
+fun retrieve_raw thy c =
+ Symtab.lookup ((the_functions o the_exec) thy) c
+ |> Option.map (snd o fst)
+ |> the_default (Default [])
-fun get_cert thy f c =
- Symtab.lookup ((the_eqns o the_exec) thy) c
- |> Option.map (snd o snd o fst)
- |> these
- |> (map o apfst) (Thm.transfer thy)
- |> f
- |> (map o apfst) (AxClass.unoverload thy)
- |> cert_of_eqns thy c;
+fun get_cert thy f c = case retrieve_raw thy c
+ of Default eqns => eqns
+ |> (map o apfst) (Thm.transfer thy)
+ |> f
+ |> (map o apfst) (AxClass.unoverload thy)
+ |> cert_of_eqns thy c
+ | Eqns eqns => eqns
+ |> (map o apfst) (Thm.transfer thy)
+ |> f
+ |> (map o apfst) (AxClass.unoverload thy)
+ |> cert_of_eqns thy c
+ | Proj (_, tyco) =>
+ cert_of_proj thy c tyco
+ | Abstr (abs_thm, tyco) => abs_thm
+ |> Thm.transfer thy
+ |> AxClass.unoverload thy
+ |> cert_of_abs thy tyco c;
(* cases *)
@@ -729,48 +920,54 @@
let
val ctxt = ProofContext.init thy;
val exec = the_exec thy;
- fun pretty_eqns (s, (_, eqns)) =
+ fun pretty_equations const thms =
(Pretty.block o Pretty.fbreaks) (
- Pretty.str s :: map (Display.pretty_thm ctxt o fst) eqns
+ Pretty.str (string_of_const thy const) :: map (Display.pretty_thm ctxt) thms
);
- fun pretty_dtyp (s, []) =
- Pretty.str s
- | pretty_dtyp (s, cos) =
- (Pretty.block o Pretty.breaks) (
- Pretty.str s
- :: Pretty.str "="
- :: separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
- | (c, tys) =>
- (Pretty.block o Pretty.breaks)
- (Pretty.str (string_of_const thy c)
- :: Pretty.str "of"
- :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
- );
+ fun pretty_function (const, Default eqns) = pretty_equations const (map fst eqns)
+ | pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
+ | pretty_function (const, Proj (proj, _)) = Pretty.block
+ [Pretty.str (string_of_const thy const), Pretty.fbrk, Syntax.pretty_term ctxt proj]
+ | pretty_function (const, Abstr (thm, _)) = pretty_equations const [thm];
+ fun pretty_typ (tyco, vs) = Pretty.str
+ (string_of_typ thy (Type (tyco, map TFree vs)));
+ fun pretty_typspec (typ, (cos, abstract)) = if null cos
+ then pretty_typ typ
+ else (Pretty.block o Pretty.breaks) (
+ pretty_typ typ
+ :: Pretty.str "="
+ :: (if abstract then [Pretty.str "(abstract)"] else [])
+ @ separate (Pretty.str "|") (map (fn (c, []) => Pretty.str (string_of_const thy c)
+ | (c, tys) =>
+ (Pretty.block o Pretty.breaks)
+ (Pretty.str (string_of_const thy c)
+ :: Pretty.str "of"
+ :: map (Pretty.quote o Syntax.pretty_typ_global thy) tys)) cos)
+ );
fun pretty_case (const, (_, (_, []))) = Pretty.str (string_of_const thy const)
| pretty_case (const, (_, (_, cos))) = (Pretty.block o Pretty.breaks) [
Pretty.str (string_of_const thy const), Pretty.str "with",
(Pretty.block o Pretty.commas o map (Pretty.str o string_of_const thy)) cos];
- val eqns = the_eqns exec
+ val functions = the_functions exec
|> Symtab.dest
- |> (map o apfst) (string_of_const thy)
|> (map o apsnd) (snd o fst)
|> sort (string_ord o pairself fst);
- val dtyps = the_dtyps exec
+ val datatypes = the_datatypes exec
|> Symtab.dest
- |> map (fn (dtco, (_, (vs, cos)) :: _) =>
- (string_of_typ thy (Type (dtco, map TFree vs)), cos))
- |> sort (string_ord o pairself fst);
+ |> map (fn (tyco, (_, (vs, spec)) :: _) =>
+ ((tyco, vs), constructors_of spec))
+ |> sort (string_ord o pairself (fst o fst));
val cases = Symtab.dest ((fst o the_cases o the_exec) thy);
val undefineds = Symtab.keys ((snd o the_cases o the_exec) thy);
in
(Pretty.writeln o Pretty.chunks) [
Pretty.block (
Pretty.str "code equations:" :: Pretty.fbrk
- :: (Pretty.fbreaks o map pretty_eqns) eqns
+ :: (Pretty.fbreaks o map pretty_function) functions
),
Pretty.block (
Pretty.str "datatypes:" :: Pretty.fbrk
- :: (Pretty.fbreaks o map pretty_dtyp) dtyps
+ :: (Pretty.fbreaks o map pretty_typspec) datatypes
),
Pretty.block (
Pretty.str "cases:" :: Pretty.fbrk
@@ -816,11 +1013,27 @@
(* code equations *)
-fun gen_add_eqn default (thm, proper) thy =
+fun gen_add_eqn default (raw_thm, proper) thy =
let
- val thm' = Thm.close_derivation thm;
- val c = const_eqn thy thm';
- in change_eqns false c (add_thm thy default (thm', proper)) thy end;
+ val thm = Thm.close_derivation raw_thm;
+ val c = const_eqn thy thm;
+ fun add_eqn' true (Default eqns) = Default (eqns @ [(thm, proper)])
+ | add_eqn' _ (Eqns eqns) =
+ let
+ val args_of = snd o strip_comb o map_types Type.strip_sorts
+ o fst o Logic.dest_equals o Thm.plain_prop_of;
+ val args = args_of thm;
+ val incr_idx = Logic.incr_indexes ([], Thm.maxidx_of thm + 1);
+ fun matches_args args' = length args <= length args' andalso
+ Pattern.matchess thy (args, (map incr_idx o take (length args)) args');
+ fun drop (thm', proper') = if (proper orelse not proper')
+ andalso matches_args (args_of thm') then
+ (warning ("Code generator: dropping redundant code equation\n" ^
+ Display.string_of_thm_global thy thm'); true)
+ else false;
+ in Eqns ((thm, proper) :: filter_out drop eqns) end
+ | add_eqn' false _ = Eqns [(thm, proper)];
+ in change_fun_spec false c (add_eqn' default) thy end;
fun add_eqn thm thy =
gen_add_eqn false (mk_eqn thy (thm, true)) thy;
@@ -842,11 +1055,22 @@
(fn thm => Context.mapping (add_default_eqn thm) I);
val add_default_eqn_attrib = Attrib.internal (K add_default_eqn_attribute);
+fun add_abs_eqn raw_thm thy =
+ let
+ val (abs_thm, tyco) = (apfst Thm.close_derivation o mk_abs_eqn thy) raw_thm;
+ val c = const_abs_eqn thy abs_thm;
+ in change_fun_spec false c (K (Abstr (abs_thm, tyco))) thy end;
+
fun del_eqn thm thy = case mk_eqn_liberal thy thm
- of SOME (thm, _) => change_eqns true (const_eqn thy thm) (del_thm thm) thy
+ of SOME (thm, _) => let
+ fun del_eqn' (Default eqns) = empty_fun_spec
+ | del_eqn' (Eqns eqns) =
+ Eqns (filter_out (fn (thm', _) => Thm.eq_thm_prop (thm, thm')) eqns)
+ | del_eqn' spec = spec
+ in change_fun_spec true (const_eqn thy thm) del_eqn' thy end
| NONE => thy;
-fun del_eqns c = change_eqns true c (K (false, []));
+fun del_eqns c = change_fun_spec true c (K empty_fun_spec);
(* cases *)
@@ -869,32 +1093,69 @@
structure Type_Interpretation =
Interpretation(type T = string * serial val eq = eq_snd (op =) : T * T -> bool);
-fun add_datatype raw_cs thy =
+fun register_datatype (tyco, vs_spec) thy =
let
- val cs = map (fn c_ty as (_, ty) => (AxClass.unoverload_const thy c_ty, ty)) raw_cs;
- val (tyco, vs_cos) = constrset_of_consts thy cs;
- val old_cs = (map fst o snd o get_datatype thy) tyco;
+ val (old_constrs, some_old_proj) =
+ case these (Symtab.lookup ((the_datatypes o the_exec) thy) tyco)
+ of (_, (_, Constructors cos)) :: _ => (map fst cos, NONE)
+ | (_, (_, Abstractor (_, (co, _)))) :: _ => ([], SOME co)
+ | [] => ([], NONE)
+ val outdated_funs = case some_old_proj
+ of NONE => []
+ | SOME old_proj => Symtab.fold
+ (fn (c, ((_, spec), _)) => if member (op =) (the_list (associated_abstype spec)) tyco
+ then insert (op =) c else I)
+ ((the_functions o the_exec) thy) [old_proj];
fun drop_outdated_cases cases = fold Symtab.delete_safe
(Symtab.fold (fn (c, (_, (_, cos))) =>
- if exists (member (op =) old_cs) cos
+ if exists (member (op =) old_constrs) cos
then insert (op =) c else I) cases []) cases;
in
thy
- |> fold (del_eqns o fst) cs
+ |> fold del_eqns outdated_funs
|> map_exec_purge
- ((map_dtyps o Symtab.map_default (tyco, [])) (cons (serial (), vs_cos))
+ ((map_typs o Symtab.map_default (tyco, [])) (cons (serial (), vs_spec))
#> (map_cases o apfst) drop_outdated_cases)
|> Type_Interpretation.data (tyco, serial ())
end;
-fun type_interpretation f = Type_Interpretation.interpretation
+fun type_interpretation f = Type_Interpretation.interpretation
(fn (tyco, _) => fn thy => f (tyco, get_datatype thy tyco) thy);
-fun add_datatype_cmd raw_cs thy =
+fun unoverload_const_typ thy (c, ty) = (AxClass.unoverload_const thy (c, ty), ty);
+
+fun add_datatype proto_constrs thy =
+ let
+ val constrs = map (unoverload_const_typ thy) proto_constrs;
+ val (tyco, (vs, cos)) = constrset_of_consts thy constrs;
+ in
+ thy
+ |> fold (del_eqns o fst) constrs
+ |> register_datatype (tyco, (vs, Constructors cos))
+ end;
+
+fun add_datatype_cmd raw_constrs thy =
+ add_datatype (map (read_bare_const thy) raw_constrs) thy;
+
+fun add_abstype proto_abs proto_rep thy =
let
- val cs = map (read_bare_const thy) raw_cs;
- in add_datatype cs thy end;
+ val (abs, rep) = pairself (unoverload_const_typ thy) (proto_abs, proto_rep);
+ val (tyco, (vs, (abs_ty as (abs, ty), (rep, cert_prop)))) = abstype_cert thy abs (fst rep);
+ fun after_qed [[cert]] = ProofContext.theory
+ (register_datatype (tyco, (vs, Abstractor (abs_ty, (rep, cert))))
+ #> change_fun_spec false rep ((K o Proj)
+ (map_types Logic.varifyT (mk_proj tyco vs ty abs rep), tyco)));
+ in
+ thy
+ |> ProofContext.init
+ |> Proof.theorem_i NONE after_qed [[(cert_prop, [])]]
+ end;
+fun add_abstype_cmd raw_abs raw_rep thy =
+ add_abstype (read_bare_const thy raw_abs) (read_bare_const thy raw_rep) thy;
+
+
+(** infrastructure **)
(* c.f. src/HOL/Tools/recfun_codegen.ML *)
@@ -912,6 +1173,8 @@
let
val attr = the_default ((K o K) I) (Code_Target_Attr.get thy);
in thy |> add_warning_eqn thm |> attr prefix thm end;
+
+
(* setup *)
val _ = Context.>> (Context.map_theory
@@ -920,6 +1183,7 @@
val code_attribute_parser =
Args.del |-- Scan.succeed (mk_attribute del_eqn)
|| Args.$$$ "nbe" |-- Scan.succeed (mk_attribute add_nbe_eqn)
+ || Args.$$$ "abstract" |-- Scan.succeed (mk_attribute add_abs_eqn)
|| (Args.$$$ "target" |-- Args.colon |-- Args.name >>
(mk_attribute o code_target_attr))
|| Scan.succeed (mk_attribute add_warning_eqn);
@@ -932,7 +1196,7 @@
end; (*struct*)
-(** type-safe interfaces for data dependent on executable code **)
+(* type-safe interfaces for data dependent on executable code *)
functor Code_Data(Data: CODE_DATA_ARGS): CODE_DATA =
struct
--- a/src/Pure/Isar/isar_syn.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Feb 19 16:42:37 2010 +0100
@@ -479,6 +479,11 @@
OuterSyntax.command "code_datatype" "define set of code datatype constructors" K.thy_decl
(Scan.repeat1 P.term >> (Toplevel.theory o Code.add_datatype_cmd));
+val _ =
+ OuterSyntax.command "code_abstype" "define abstract code type" K.thy_goal
+ (P.term -- P.term >> (fn (abs, rep) => Toplevel.print
+ o Toplevel.theory_to_proof (Code.add_abstype_cmd abs rep)));
+
(** proof commands **)
--- a/src/Pure/term.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Pure/term.ML Fri Feb 19 16:42:37 2010 +0100
@@ -45,6 +45,7 @@
val dest_Const: term -> string * typ
val dest_Free: term -> string * typ
val dest_Var: term -> indexname * typ
+ val dest_comb: term -> term * term
val domain_type: typ -> typ
val range_type: typ -> typ
val binder_types: typ -> typ list
@@ -278,6 +279,9 @@
fun dest_Var (Var x) = x
| dest_Var t = raise TERM("dest_Var", [t]);
+fun dest_comb (t1 $ t2) = (t1, t2)
+ | dest_comb t = raise TERM("dest_comb", [t]);
+
fun domain_type (Type("fun", [T,_])) = T
and range_type (Type("fun", [_,T])) = T;
--- a/src/Tools/Code/code_eval.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_eval.ML Fri Feb 19 16:42:37 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 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_haskell.ML Fri Feb 19 16:42:37 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 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_ml.ML Fri Feb 19 16:42:37 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_preproc.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_preproc.ML Fri Feb 19 16:42:37 2010 +0100
@@ -216,14 +216,6 @@
map (fn (c, _) => AxClass.param_of_inst thy (c, tyco))
o maps (#params o AxClass.get_info thy);
-fun typargs_rhss thy c cert =
- let
- val ((vs, _), equations) = Code.equations_cert thy cert;
- val rhss = [] |> (fold o fold o fold_aterms)
- (fn Const (c, ty) => insert (op =) (c, Sign.const_typargs thy (c, ty)) | _ => I)
- (map (op :: o swap) equations);
- in (vs, rhss) end;
-
(* data structures *)
@@ -262,7 +254,7 @@
of SOME (lhs, cert) => ((lhs, []), cert)
| NONE => let
val cert = Code.get_cert thy (preprocess thy) c;
- val (lhs, rhss) = typargs_rhss thy c cert;
+ val (lhs, rhss) = Code.typargs_deps_of_cert thy cert;
in ((lhs, rhss), cert) end;
fun obtain_instance thy arities (inst as (class, tyco)) =
@@ -395,7 +387,7 @@
val lhs = map_index (fn (k, (v, _)) =>
(v, snd (Vargraph.get_node vardeps (Fun c, k)))) proto_lhs;
val cert = Code.constrain_cert thy (map snd lhs) proto_cert;
- val (vs, rhss') = typargs_rhss thy c cert;
+ val (vs, rhss') = Code.typargs_deps_of_cert thy cert;
val eqngr' = Graph.new_node (c, (vs, cert)) eqngr;
in (map (pair c) rhss' @ rhss, eqngr') end;
--- a/src/Tools/Code/code_printer.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_printer.ML Fri Feb 19 16:42:37 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 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_scala.ML Fri Feb 19 16:42:37 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;
--- a/src/Tools/Code/code_thingol.ML Fri Feb 19 13:54:19 2010 +0100
+++ b/src/Tools/Code/code_thingol.ML Fri Feb 19 16:42:37 2010 +0100
@@ -66,7 +66,7 @@
datatype stmt =
NoStmt
- | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+ | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| Datatype of string * ((vname * sort) list * (string * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -256,8 +256,8 @@
| thyname :: _ => thyname;
fun thyname_of_const thy c = case AxClass.class_of_param thy c
of SOME class => thyname_of_class thy class
- | NONE => (case Code.get_datatype_of_constr thy c
- of SOME dtco => Codegen.thyname_of_type thy dtco
+ | NONE => (case Code.get_datatype_of_constr_or_abstr thy c
+ of SOME (tyco, _) => Codegen.thyname_of_type thy tyco
| NONE => Codegen.thyname_of_const thy c);
fun purify_base "==>" = "follows"
| purify_base "op &" = "and"
@@ -400,7 +400,7 @@
type typscheme = (vname * sort) list * itype;
datatype stmt =
NoStmt
- | Fun of string * (typscheme * ((iterm list * iterm) * (thm * bool)) list)
+ | Fun of string * (typscheme * ((iterm list * iterm) * (thm option * bool)) list)
| Datatype of string * ((vname * sort) list * (string * itype list) list)
| Datatypecons of string * string
| Class of class * (vname * ((class * string) list * (string * itype) list))
@@ -523,14 +523,18 @@
|> pair name
end;
-fun not_wellsorted thy thm ty sort e =
+fun translation_error thy some_thm msg sub_msg =
+ let
+ val err_thm = case some_thm
+ of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
+ in error (msg ^ err_thm ^ ":\n" ^ sub_msg) end;
+
+fun not_wellsorted thy some_thm ty sort e =
let
val err_class = Sorts.class_error (Syntax.pp_global thy) e;
- val err_thm = case thm
- of SOME thm => "\n(in code equation " ^ Display.string_of_thm_global thy thm ^ ")" | NONE => "";
val err_typ = "Type " ^ Syntax.string_of_typ_global thy ty ^ " not of sort "
^ Syntax.string_of_sort_global thy sort;
- in error ("Wellsortedness error" ^ err_thm ^ ":\n" ^ err_typ ^ "\n" ^ err_class) end;
+ in translation_error thy some_thm "Wellsortedness error" (err_typ ^ "\n" ^ err_class) end;
(* translation *)
@@ -558,16 +562,15 @@
#>> (fn class => Classparam (c, class));
fun stmt_fun cert =
let
- val ((vs, ty), raw_eqns) = Code.equations_thms_cert thy cert;
- val eqns = map snd raw_eqns;
+ val ((vs, ty), eqns) = Code.equations_of_cert thy cert;
in
fold_map (translate_tyvar_sort thy algbr eqngr) vs
##>> translate_typ thy algbr eqngr ty
##>> fold_map (translate_eqn thy algbr eqngr) eqns
#>> (fn info => Fun (c, info))
end;
- val stmt_const = case Code.get_datatype_of_constr thy c
- of SOME tyco => stmt_datatypecons tyco
+ val stmt_const = case Code.get_datatype_of_constr_or_abstr thy c
+ of SOME (tyco, _) => stmt_datatypecons tyco
| NONE => (case AxClass.class_of_param thy c
of SOME class => stmt_classparam class
| NONE => stmt_fun (Code_Preproc.cert eqngr c))
@@ -614,7 +617,7 @@
o Logic.dest_equals o Thm.prop_of) thm;
in
ensure_const thy algbr eqngr c
- ##>> translate_const thy algbr eqngr (SOME thm) c_ty
+ ##>> translate_const thy algbr eqngr NONE (SOME thm) c_ty
#>> (fn (c, IConst c_inst) => ((c, c_inst), (thm, true)))
end;
val stmt_inst =
@@ -632,54 +635,54 @@
ensure_tyco thy algbr eqngr tyco
##>> fold_map (translate_typ thy algbr eqngr) tys
#>> (fn (tyco, tys) => tyco `%% tys)
-and translate_term thy algbr eqngr thm (Const (c, ty)) =
- translate_app thy algbr eqngr thm ((c, ty), [])
- | translate_term thy algbr eqngr thm (Free (v, _)) =
+and translate_term thy algbr eqngr some_abs some_thm (Const (c, ty)) =
+ translate_app thy algbr eqngr some_abs some_thm ((c, ty), [])
+ | translate_term thy algbr eqngr some_abs some_thm (Free (v, _)) =
pair (IVar (SOME v))
- | translate_term thy algbr eqngr thm (Abs (v, ty, t)) =
+ | translate_term thy algbr eqngr some_abs some_thm (Abs (v, ty, t)) =
let
val (v', t') = Syntax.variant_abs (Name.desymbolize false v, ty, t);
val v'' = if member (op =) (Term.add_free_names t' []) v'
then SOME v' else NONE
in
translate_typ thy algbr eqngr ty
- ##>> translate_term thy algbr eqngr thm t'
+ ##>> translate_term thy algbr eqngr some_abs some_thm t'
#>> (fn (ty, t) => (v'', ty) `|=> t)
end
- | translate_term thy algbr eqngr thm (t as _ $ _) =
+ | translate_term thy algbr eqngr some_abs some_thm (t as _ $ _) =
case strip_comb t
of (Const (c, ty), ts) =>
- translate_app thy algbr eqngr thm ((c, ty), ts)
+ translate_app thy algbr eqngr some_abs some_thm ((c, ty), ts)
| (t', ts) =>
- translate_term thy algbr eqngr thm t'
- ##>> fold_map (translate_term thy algbr eqngr thm) ts
+ translate_term thy algbr eqngr some_abs some_thm t'
+ ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
#>> (fn (t, ts) => t `$$ ts)
-and translate_eqn thy algbr eqngr (thm, proper) =
+and translate_eqn thy algbr eqngr ((some_abs, (args, rhs)), (some_thm, proper)) =
+ fold_map (translate_term thy algbr eqngr some_abs some_thm) args
+ ##>> translate_term thy algbr eqngr some_abs some_thm rhs
+ #>> rpair (some_thm, proper)
+and translate_const thy algbr eqngr some_abs some_thm (c, ty) =
let
- val (args, rhs) = (apfst (snd o strip_comb) o Logic.dest_equals
- o Code.subst_signatures thy o Logic.unvarify o prop_of) thm;
- in
- fold_map (translate_term thy algbr eqngr (SOME thm)) args
- ##>> translate_term thy algbr eqngr (SOME thm) rhs
- #>> rpair (thm, proper)
- end
-and translate_const thy algbr eqngr thm (c, ty) =
- let
+ val _ = if (case some_abs of NONE => true | SOME abs => not (c = abs))
+ andalso Code.is_abstr thy c
+ then translation_error thy some_thm
+ "Abstraction violation" ("constant " ^ Code.string_of_const thy c)
+ else ()
val tys = Sign.const_typargs thy (c, ty);
val sorts = Code_Preproc.sortargs eqngr c;
val tys_args = (fst o Term.strip_type) ty;
in
ensure_const thy algbr eqngr c
##>> fold_map (translate_typ thy algbr eqngr) tys
- ##>> fold_map (translate_dicts thy algbr eqngr thm) (tys ~~ sorts)
+ ##>> fold_map (translate_dicts thy algbr eqngr some_thm) (tys ~~ sorts)
##>> fold_map (translate_typ thy algbr eqngr) tys_args
#>> (fn (((c, tys), iss), tys_args) => IConst (c, ((tys, iss), tys_args)))
end
-and translate_app_const thy algbr eqngr thm (c_ty, ts) =
- translate_const thy algbr eqngr thm c_ty
- ##>> fold_map (translate_term thy algbr eqngr thm) ts
+and translate_app_const thy algbr eqngr some_abs some_thm (c_ty, ts) =
+ translate_const thy algbr eqngr some_abs some_thm c_ty
+ ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
#>> (fn (t, ts) => t `$$ ts)
-and translate_case thy algbr eqngr thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
+and translate_case thy algbr eqngr some_abs some_thm (num_args, (t_pos, case_pats)) (c_ty, ts) =
let
fun arg_types num_args ty = (fst o chop num_args o fst o strip_type) ty;
val tys = arg_types num_args (snd c_ty);
@@ -723,14 +726,14 @@
(constrs ~~ ts_clause);
in ((t, ty), clauses) end;
in
- translate_const thy algbr eqngr thm c_ty
- ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr thm constr #>> rpair n) constrs
+ translate_const thy algbr eqngr some_abs some_thm c_ty
+ ##>> fold_map (fn (constr, n) => translate_const thy algbr eqngr some_abs some_thm constr #>> rpair n) constrs
##>> translate_typ thy algbr eqngr ty
- ##>> fold_map (translate_term thy algbr eqngr thm) ts
+ ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) ts
#-> (fn (((t, constrs), ty), ts) =>
`(fn (_, (naming, _)) => ICase (casify naming constrs ty ts, t `$$ ts)))
end
-and translate_app_case thy algbr eqngr thm (case_scheme as (num_args, _)) ((c, ty), ts) =
+and translate_app_case thy algbr eqngr some_abs some_thm (case_scheme as (num_args, _)) ((c, ty), ts) =
if length ts < num_args then
let
val k = length ts;
@@ -739,23 +742,23 @@
val vs = Name.names ctxt "a" tys;
in
fold_map (translate_typ thy algbr eqngr) tys
- ##>> translate_case thy algbr eqngr thm case_scheme ((c, ty), ts @ map Free vs)
+ ##>> translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts @ map Free vs)
#>> (fn (tys, t) => map2 (fn (v, _) => pair (SOME v)) vs tys `|==> t)
end
else if length ts > num_args then
- translate_case thy algbr eqngr thm case_scheme ((c, ty), take num_args ts)
- ##>> fold_map (translate_term thy algbr eqngr thm) (drop num_args ts)
+ translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), take num_args ts)
+ ##>> fold_map (translate_term thy algbr eqngr some_abs some_thm) (drop num_args ts)
#>> (fn (t, ts) => t `$$ ts)
else
- translate_case thy algbr eqngr thm case_scheme ((c, ty), ts)
-and translate_app thy algbr eqngr thm (c_ty_ts as ((c, _), _)) =
+ translate_case thy algbr eqngr some_abs some_thm case_scheme ((c, ty), ts)
+and translate_app thy algbr eqngr some_abs some_thm (c_ty_ts as ((c, _), _)) =
case Code.get_case_scheme thy c
- of SOME case_scheme => translate_app_case thy algbr eqngr thm case_scheme c_ty_ts
- | NONE => translate_app_const thy algbr eqngr thm c_ty_ts
+ of SOME case_scheme => translate_app_case thy algbr eqngr some_abs some_thm case_scheme c_ty_ts
+ | NONE => translate_app_const thy algbr eqngr some_abs some_thm c_ty_ts
and translate_tyvar_sort thy (algbr as (proj_sort, _)) eqngr (v, sort) =
fold_map (ensure_class thy algbr eqngr) (proj_sort sort)
#>> (fn sort => (unprefix "'" v, sort))
-and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr thm (ty, sort) =
+and translate_dicts thy (algbr as (proj_sort, algebra)) eqngr some_thm (ty, sort) =
let
datatype typarg =
Global of (class * string) * typarg list list
@@ -773,7 +776,7 @@
val typargs = Sorts.of_sort_derivation algebra
{class_relation = class_relation, type_constructor = type_constructor,
type_variable = type_variable} (ty, proj_sort sort)
- handle Sorts.CLASS_ERROR e => not_wellsorted thy thm ty sort e;
+ handle Sorts.CLASS_ERROR e => not_wellsorted thy some_thm ty sort e;
fun mk_dict (Global (inst, yss)) =
ensure_inst thy algbr eqngr inst
##>> (fold_map o fold_map) mk_dict yss
@@ -824,9 +827,9 @@
val stmt_value =
fold_map (translate_tyvar_sort thy algbr eqngr) vs
##>> translate_typ thy algbr eqngr ty
- ##>> translate_term thy algbr eqngr NONE (Code.subst_signatures thy t)
+ ##>> translate_term thy algbr eqngr NONE NONE (Code.subst_signatures thy t)
#>> (fn ((vs, ty), t) => Fun
- (Term.dummy_patternN, ((vs, ty), [(([], t), (Drule.dummy_thm, true))])));
+ (Term.dummy_patternN, ((vs, ty), [(([], t), (NONE, true))])));
fun term_value (dep, (naming, program1)) =
let
val Fun (_, (vs_ty, [(([], t), _)])) =