# HG changeset patch # User haftmann # Date 1235151218 -3600 # Node ID be13af70c27c13a6beeafaa6b1d4d123f99d4076 # Parent 80db6f3c523ef969c24179746371fa6e8e017200# Parent 52b93309fdebe16d3662355cab6d86f44325011d merged diff -r 80db6f3c523e -r be13af70c27c src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/HOL/Tools/datatype_package.ML Fri Feb 20 18:33:38 2009 +0100 @@ -659,7 +659,7 @@ | pretty_constr (co, [ty']) = (Pretty.block o Pretty.breaks) [Syntax.pretty_term ctxt (Const (co, ty' --> ty)), - Syntax.pretty_typ ctxt ty'] + pretty_typ_br ty'] | pretty_constr (co, tys) = (Pretty.block o Pretty.breaks) (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) :: diff -r 80db6f3c523e -r be13af70c27c src/HOL/ex/Eval_Examples.thy --- a/src/HOL/ex/Eval_Examples.thy Fri Feb 20 09:15:23 2009 -0800 +++ b/src/HOL/ex/Eval_Examples.thy Fri Feb 20 18:33:38 2009 +0100 @@ -1,6 +1,4 @@ -(* ID: $Id$ - Author: Florian Haftmann, TU Muenchen -*) +(* Author: Florian Haftmann, TU Muenchen *) header {* Small examples for evaluation mechanisms *} diff -r 80db6f3c523e -r be13af70c27c src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Pure/Isar/code.ML Fri Feb 20 18:33:38 2009 +0100 @@ -35,7 +35,7 @@ val these_raw_eqns: theory -> string -> (thm * bool) list val get_datatype: theory -> string -> ((string * sort) list * (string * typ list) list) val get_datatype_of_constr: theory -> string -> string option - val get_case_scheme: theory -> string -> (int * string list) option + val get_case_scheme: theory -> string -> (int * (int * string list)) option val is_undefined: theory -> string -> bool val default_typscheme: theory -> string -> (string * sort) list * typ @@ -111,7 +111,7 @@ (** logical and syntactical specification of executable code **) -(* defining equations *) +(* code equations *) type eqns = bool * (thm * bool) list lazy; (*default flag, theorems with linear flag (perhaps lazy)*) @@ -136,7 +136,7 @@ Pattern.matchess thy (args, (map incr_idx o curry Library.take (length args)) args'); fun drop (thm', linear') = if (linear orelse not linear') andalso matches_args (args_of thm') then - (warning ("Code generator: dropping redundant defining equation\n" ^ Display.string_of_thm thm'); true) + (warning ("Code generator: dropping redundant code equation\n" ^ Display.string_of_thm thm'); true) else false; in (thm, linear) :: filter_out drop thms end; @@ -409,7 +409,7 @@ in (Pretty.writeln o Pretty.chunks) [ Pretty.block ( - Pretty.str "defining equations:" + Pretty.str "code equations:" :: Pretty.fbrk :: (Pretty.fbreaks o map pretty_eqn) eqns ), @@ -452,7 +452,7 @@ val ty1 :: tys = map (snd o Code_Unit.const_typ_eqn) thms'; fun unify ty env = Sign.typ_unify thy (ty1, ty) env handle Type.TUNIFY => - error ("Type unificaton failed, while unifying defining equations\n" + error ("Type unificaton failed, while unifying code equations\n" ^ (cat_lines o map Display.string_of_thm) thms ^ "\nwith types\n" ^ (cat_lines o map (Code_Unit.string_of_typ thy)) (ty1 :: tys)); @@ -463,7 +463,7 @@ fun check_linear (eqn as (thm, linear)) = if linear then eqn else Code_Unit.bad_thm - ("Duplicate variables on left hand side of defining equation:\n" + ("Duplicate variables on left hand side of code equation:\n" ^ Display.string_of_thm thm); fun mk_eqn thy linear = @@ -525,22 +525,13 @@ then SOME tyco else NONE | _ => NONE; -fun get_constr_typ thy c = - case get_datatype_of_constr thy c - of SOME tyco => let - val (vs, cos) = get_datatype thy tyco; - val SOME tys = AList.lookup (op =) cos c; - val ty = tys ---> Type (tyco, map TFree vs); - in SOME (Logic.varifyT ty) end - | NONE => NONE; - fun recheck_eqn thy = Code_Unit.error_thm (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy)); fun recheck_eqns_const thy c eqns = let fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm - then eqn else error ("Wrong head of defining equation,\nexpected constant " + then eqn else error ("Wrong head of code equation,\nexpected constant " ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm) in map (cert o recheck_eqn thy) eqns end; @@ -554,11 +545,11 @@ let val c = Code_Unit.const_eqn thm; val _ = if not default andalso (is_some o AxClass.class_of_param thy) c - then error ("Rejected polymorphic equation for overloaded constant:\n" + then error ("Rejected polymorphic code equation for overloaded constant:\n" ^ Display.string_of_thm thm) else (); val _ = if not default andalso (is_some o get_datatype_of_constr thy) c - then error ("Rejected equation for datatype constructor:\n" + then error ("Rejected code equation for datatype constructor:\n" ^ Display.string_of_thm thm) else (); in change_eqns false c (add_thm thy default (thm, linear)) thy end @@ -583,7 +574,12 @@ fun del_eqns c = change_eqns true c (K (false, Lazy.value [])); -fun get_case_scheme thy = Symtab.lookup ((fst o the_cases o the_exec) thy); +fun get_case_scheme thy c = case Symtab.lookup ((fst o the_cases o the_exec) thy) c + of SOME (base_case_scheme as (_, case_pats)) => + if forall (is_some o get_datatype_of_constr thy) case_pats + then SOME (1 + Int.max (1, length case_pats), base_case_scheme) + else NONE + | NONE => NONE; val is_undefined = Symtab.defined o snd o the_cases o the_exec; @@ -727,18 +723,16 @@ fun default_typscheme thy c = let - val typscheme = curry (Code_Unit.typscheme thy) c - val the_const_type = snd o dest_Const o TermSubst.zero_var_indexes - o curry Const "" o Sign.the_const_type thy; + fun the_const_typscheme c = (curry (Code_Unit.typscheme thy) c o snd o dest_Const + o TermSubst.zero_var_indexes o curry Const "" o Sign.the_const_type thy) c; + fun strip_sorts (vs, ty) = (map (fn (v, _) => (v, [])) vs, ty); in case AxClass.class_of_param thy c - of SOME class => the_const_type c - |> Term.map_type_tvar (K (TVar ((Name.aT, 0), [class]))) - |> typscheme - | NONE => (case get_constr_typ thy c - of SOME ty => typscheme ty - | NONE => (case get_eqns thy c - of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm)) - | [] => typscheme (the_const_type c))) end; + of SOME class => ([(Name.aT, [class])], snd (the_const_typscheme c)) + | NONE => if is_some (get_datatype_of_constr thy c) + then strip_sorts (the_const_typscheme c) + else case get_eqns thy c + of (thm, _) :: _ => snd (Code_Unit.head_eqn thy (Drule.zero_var_indexes thm)) + | [] => strip_sorts (the_const_typscheme c) end; end; (*local*) diff -r 80db6f3c523e -r be13af70c27c src/Pure/Isar/code_unit.ML --- a/src/Pure/Isar/code_unit.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Pure/Isar/code_unit.ML Fri Feb 20 18:33:38 2009 +0100 @@ -34,7 +34,7 @@ val constrset_of_consts: theory -> (string * typ) list -> string * ((string * sort) list * (string * typ list) list) - (*defining equations*) + (*code equations*) val assert_eqn: theory -> thm -> thm val mk_eqn: theory -> thm -> thm * bool val assert_linear: (string -> bool) -> thm * bool -> thm * bool @@ -76,10 +76,11 @@ fun typscheme thy (c, ty) = let - fun dest (TVar ((v, 0), sort)) = (v, sort) + val ty' = Logic.unvarifyT ty; + fun dest (TFree (v, sort)) = (v, sort) | dest ty = error ("Illegal type parameter in type scheme: " ^ Syntax.string_of_typ_global thy ty); - val vs = map dest (Sign.const_typargs thy (c, ty)); - in (vs, ty) end; + val vs = map dest (Sign.const_typargs thy (c, ty')); + in (vs, Type.strip_sorts ty') end; fun inst_thm thy tvars' thm = let @@ -313,10 +314,10 @@ 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, cs''')) end; + in (tyco, (vs, rev cs''')) end; -(* defining equations *) +(* code equations *) fun assert_eqn thy thm = let @@ -351,7 +352,7 @@ ^ Display.string_of_thm thm) | check 0 (Var _) = () | check _ (Var _) = bad_thm - ("Variable with application on left hand side of defining equation\n" + ("Variable with application on left hand side of code equation\n" ^ Display.string_of_thm thm) | check n (t1 $ t2) = (check (n+1) t1; check 0 t2) | check n (Const (_, ty)) = if n <> (length o fst o strip_type) ty @@ -363,7 +364,7 @@ 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 - ^ "\nof defining equation\n" + ^ "\nof code equation\n" ^ Display.string_of_thm thm ^ "\nis incompatible with declared function type\n" ^ string_of_typ thy ty_decl) @@ -388,7 +389,7 @@ fun assert_linear is_cons (thm, false) = (thm, false) | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true) else bad_thm - ("Duplicate variables on left hand side of defining equation:\n" + ("Duplicate variables on left hand side of code equation:\n" ^ Display.string_of_thm thm); diff -r 80db6f3c523e -r be13af70c27c src/Tools/code/code_funcgr.ML --- a/src/Tools/code/code_funcgr.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Tools/code/code_funcgr.ML Fri Feb 20 18:33:38 2009 +0100 @@ -317,13 +317,13 @@ in val _ = - OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); val _ = - OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); diff -r 80db6f3c523e -r be13af70c27c src/Tools/code/code_target.ML --- a/src/Tools/code/code_target.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Tools/code/code_target.ML Fri Feb 20 18:33:38 2009 +0100 @@ -418,7 +418,7 @@ val program4 = Graph.subgraph (member (op =) names_all) program3; val empty_funs = filter_out (member (op =) abortable) (Code_Thingol.empty_funs program3); - val _ = if null empty_funs then () else error ("No defining equations for " + val _ = if null empty_funs then () else error ("No code equations for " ^ commas (map (Sign.extern_const thy) empty_funs)); in serializer module args (labelled_name thy program2) reserved includes diff -r 80db6f3c523e -r be13af70c27c src/Tools/code/code_thingol.ML --- a/src/Tools/code/code_thingol.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Tools/code/code_thingol.ML Fri Feb 20 18:33:38 2009 +0100 @@ -453,7 +453,7 @@ let val err_class = Sorts.class_error (Syntax.pp_global thy) e; val err_thm = case thm - of SOME thm => "\n(in defining equation " ^ Display.string_of_thm thm ^ ")" | NONE => ""; + of SOME thm => "\n(in code equation " ^ Display.string_of_thm 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; @@ -582,9 +582,8 @@ fun stmt_classparam class = ensure_class thy algbr funcgr class #>> (fn class => Classparam (c, class)); - fun stmt_fun ((vs, raw_ty), raw_thms) = + fun stmt_fun ((vs, ty), raw_thms) = let - val ty = Logic.unvarifyT raw_ty; (*FIXME change convention here*) val thms = if null (Term.add_tfreesT ty []) orelse (null o fst o strip_type) ty then raw_thms else (map o apfst) (Code_Unit.expand_eta thy 1) raw_thms; @@ -643,11 +642,6 @@ val ts_clause = nth_drop t_pos ts; fun mk_clause (co, num_co_args) t = let - val _ = if (is_some o Code.get_datatype_of_constr thy) co then () - else error ("Non-constructor " ^ quote co - ^ " encountered in case pattern" - ^ (case thm of NONE => "" - | SOME thm => ", in equation\n" ^ Display.string_of_thm thm)) val (vs, body) = Term.strip_abs_eta num_co_args t; val not_undefined = case body of (Const (c, _)) => not (Code.is_undefined thy c) @@ -702,9 +696,7 @@ translate_case thy algbr funcgr thm case_scheme ((c, ty), ts) and translate_app thy algbr funcgr thm (c_ty_ts as ((c, _), _)) = case Code.get_case_scheme thy c - of SOME (base_case_scheme as (_, case_pats)) => - translate_app_case thy algbr funcgr thm - (1 + Int.max (1, length case_pats), base_case_scheme) c_ty_ts + of SOME case_scheme => translate_app_case thy algbr funcgr thm case_scheme c_ty_ts | NONE => translate_app_const thy algbr funcgr thm c_ty_ts; diff -r 80db6f3c523e -r be13af70c27c src/Tools/code/code_wellsorted.ML --- a/src/Tools/code/code_wellsorted.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Tools/code/code_wellsorted.ML Fri Feb 20 18:33:38 2009 +0100 @@ -388,13 +388,13 @@ in val _ = - OuterSyntax.improper_command "code_thms" "print system of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_thms" "print system of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of))); val _ = - OuterSyntax.improper_command "code_deps" "visualize dependencies of defining equations for code" OuterKeyword.diag + OuterSyntax.improper_command "code_deps" "visualize dependencies of code equations for code" OuterKeyword.diag (Scan.repeat P.term_group >> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of))); diff -r 80db6f3c523e -r be13af70c27c src/Tools/nbe.ML --- a/src/Tools/nbe.ML Fri Feb 20 09:15:23 2009 -0800 +++ b/src/Tools/nbe.ML Fri Feb 20 18:33:38 2009 +0100 @@ -389,8 +389,8 @@ val ts' = take_until is_dict ts; val c = const_of_idx idx; val (_, T) = Code.default_typscheme thy c; - val T' = map_type_tvar (fn ((v, i), S) => TypeInfer.param (typidx + i) (v, [])) T; - val typidx' = typidx + maxidx_of_typ T' + 1; + val T' = map_type_tfree (fn (v, _) => TypeInfer.param typidx (v, [])) T; + val typidx' = typidx + 1; in of_apps bounds (Term.Const (c, T'), ts') typidx' end | of_univ bounds (Free (name, ts)) typidx = of_apps bounds (Term.Free (name, dummyT), ts) typidx