# HG changeset patch # User haftmann # Date 1266594157 -3600 # Node ID d4ec25836a787ae332845e344b945fb792b557bc # Parent 4f1fba00f66d9df327b1567c2868c5a57ed8f625# Parent ac2cab4583f4a97ed5ab26e054a513380d6e6f18 merged diff -r 4f1fba00f66d -r d4ec25836a78 etc/isar-keywords.el --- 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" diff -r 4f1fba00f66d -r d4ec25836a78 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r 4f1fba00f66d -r d4ec25836a78 src/HOL/Tools/recfun_codegen.ML --- 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 diff -r 4f1fba00f66d -r d4ec25836a78 src/Pure/Isar/code.ML --- 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 diff -r 4f1fba00f66d -r d4ec25836a78 src/Pure/Isar/isar_syn.ML --- 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 **) diff -r 4f1fba00f66d -r d4ec25836a78 src/Pure/term.ML --- 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; diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_eval.ML --- 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]; diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_haskell.ML --- 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 diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_ml.ML --- 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) diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_preproc.ML --- 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; diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_printer.ML --- 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; diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_scala.ML --- 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; diff -r 4f1fba00f66d -r d4ec25836a78 src/Tools/Code/code_thingol.ML --- 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), _)])) =