# HG changeset patch # User wenzelm # Date 1323954717 -3600 # Node ID 4ff377493dbb0dec0560ddab206b1a23b2b5c1c3 # Parent 66b419de5f38308a2b7e12dc255108cd8afcf42e misc tuning and simplification; diff -r 66b419de5f38 -r 4ff377493dbb src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 13:40:20 2011 +0100 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Dec 15 14:11:57 2011 +0100 @@ -858,14 +858,14 @@ dist_lemma :: rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]) constr_rep_thmss dist_lemmas; - fun prove_distinct_thms _ (_, []) = [] - | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) = + fun prove_distinct_thms _ [] = [] + | prove_distinct_thms (p as (rep_thms, dist_lemma)) (t :: ts) = let val dist_thm = Goal.prove_global thy8 [] [] t (fn _ => simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1) in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: - prove_distinct_thms p (k, ts) + prove_distinct_thms p ts end; val distinct_thms = map2 prove_distinct_thms diff -r 66b419de5f38 -r 4ff377493dbb src/HOL/Tools/Datatype/datatype.ML --- a/src/HOL/Tools/Datatype/datatype.ML Thu Dec 15 13:40:20 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype.ML Thu Dec 15 14:11:57 2011 +0100 @@ -211,7 +211,7 @@ (* constructor definitions *) - fun make_constr_def tname (typedef: Typedef.info) T n + fun make_constr_def (typedef: Typedef.info) T n ((cname, cargs), (cname', mx)) (thy, defs, eqns, i) = let fun constr_arg dt (j, l_args, r_args) = @@ -257,7 +257,7 @@ Drule.export_without_context (cterm_instantiate [(cterm_of thy distinct_f, rep_const)] distinct_lemma); val (thy', defs', eqns', _) = - fold (make_constr_def tname typedef T (length constrs)) + fold (make_constr_def typedef T (length constrs)) (constrs ~~ constr_syntax) (Sign.add_path tname thy, defs, [], 1); in (Sign.parent_path thy', defs', eqns @ [eqns'], @@ -534,7 +534,7 @@ dist_lemma :: (rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0])) (constr_rep_thms ~~ dist_lemmas); - fun prove_distinct_thms dist_rewrites' (k, ts) = + fun prove_distinct_thms dist_rewrites' = let fun prove [] = [] | prove (t :: ts) = @@ -542,7 +542,7 @@ val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ => EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1]) in dist_thm :: Drule.export_without_context (dist_thm RS not_sym) :: prove ts end; - in prove ts end; + in prove end; val distinct_thms = map2 (prove_distinct_thms) dist_rewrites (Datatype_Prop.make_distincts descr); @@ -734,9 +734,9 @@ [] => () | dups => error ("Duplicate datatypes: " ^ commas_quote dups)); - fun prep_dt_spec ((tname, tvs, mx), constrs) (dts', constr_syntax, i) = + fun prep_dt_spec ((tname, tvs, _), constrs) (dts', constr_syntax, i) = let - fun prep_constr (cname, cargs, mx') (constrs, constr_syntax') = + fun prep_constr (cname, cargs, mx) (constrs, constr_syntax') = let val _ = (case subtract (op =) tvs (fold Term.add_tfreesT cargs []) of @@ -745,7 +745,7 @@ val c = Sign.full_name_path thy (Binding.name_of tname) cname; in (constrs @ [(c, map (Datatype_Aux.dtyp_of_typ new_dts) cargs)], - constr_syntax' @ [(cname, mx')]) + constr_syntax' @ [(cname, mx)]) end handle ERROR msg => cat_error msg ("The error above occurred in constructor " ^ Binding.print cname ^ " of datatype " ^ Binding.print tname); diff -r 66b419de5f38 -r 4ff377493dbb src/HOL/Tools/Datatype/datatype_case.ML --- a/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 13:40:20 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_case.ML Thu Dec 15 14:11:57 2011 +0100 @@ -72,7 +72,7 @@ (*Produce an instance of a constructor, plus fresh variables for its arguments.*) fun fresh_constr ty_match ty_inst colty used c = let - val (_, Ty) = dest_Const c + val (_, Ty) = dest_Const c; val Ts = binder_types Ty; val names = Name.variant_list used (Datatype_Prop.make_tnames (map Logic.unvarifyT_global Ts)); @@ -84,7 +84,7 @@ in (c', gvars) end; -(*Goes through a list of rows and picks out the ones beginning with a +(*Go through a list of rows and pick out the ones beginning with a pattern with constructor = name.*) fun mk_group (name, T) rows = let val k = length (binder_types T) in @@ -203,14 +203,16 @@ fun case_error s = error ("Error in case expression:\n" ^ s); +local + (*Repeated variable occurrences in a pattern are not allowed.*) fun no_repeat_vars ctxt pat = fold_aterms (fn x as Free (s, _) => - (fn xs => - if member op aconv xs x then - case_error (quote s ^ " occurs repeatedly in the pattern " ^ - quote (Syntax.string_of_term ctxt pat)) - else x :: xs) + (fn xs => + if member op aconv xs x then + case_error (quote s ^ " occurs repeatedly in the pattern " ^ + quote (Syntax.string_of_term ctxt pat)) + else x :: xs) | _ => I) pat []; fun gen_make_case ty_match ty_inst type_of tab ctxt config used x clauses = @@ -241,6 +243,8 @@ case_tm end; +in + fun make_case tab ctxt = gen_make_case (match_type (Proof_Context.theory_of ctxt)) Envir.subst_term_types fastype_of tab ctxt; @@ -248,6 +252,8 @@ val make_case_untyped = gen_make_case (K (K Vartab.empty)) (K (Term.map_types (K dummyT))) (K dummyT); +end; + (* parse translation *) @@ -297,6 +303,8 @@ (* destruct one level of pattern matching *) +local + (* FIXME proper name context!? *) fun gen_dest_case name_of type_of tab d used t = (case apfst name_of (strip_comb t) of @@ -362,12 +370,18 @@ end | _ => NONE); +in + val dest_case = gen_dest_case (try (dest_Const #> fst)) fastype_of; val dest_case' = gen_dest_case (try (dest_Const #> fst #> Lexicon.unmark_const)) (K dummyT); +end; + (* destruct nested patterns *) +local + fun strip_case'' dest (pat, rhs) = (case dest (Term.add_free_names pat []) rhs of SOME (exp as Free _, clauses) => @@ -385,9 +399,13 @@ SOME (x, clauses) => SOME (x, maps (strip_case'' dest) clauses) | NONE => NONE); +in + val strip_case = gen_strip_case oo dest_case; val strip_case' = gen_strip_case oo dest_case'; +end; + (* print translation *) diff -r 66b419de5f38 -r 4ff377493dbb src/HOL/Tools/Datatype/datatype_codegen.ML --- a/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Dec 15 13:40:20 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Thu Dec 15 14:11:57 2011 +0100 @@ -79,8 +79,7 @@ val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index); fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) = [trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)]; - val distincts = - maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr]) index)); + val distincts = maps prep_distinct (nth (Datatype_Prop.make_distincts [descr]) index); val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty))); val simpset = Simplifier.global_context thy diff -r 66b419de5f38 -r 4ff377493dbb src/HOL/Tools/Datatype/datatype_data.ML --- a/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 13:40:20 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_data.ML Thu Dec 15 14:11:57 2011 +0100 @@ -413,7 +413,7 @@ (i, (tyco, map Datatype_Aux.DtTFree vs, (map o apsnd) dtyps_of_typ constr)); val descr = map_index mk_spec cs; val injs = Datatype_Prop.make_injs [descr]; - val half_distincts = map snd (Datatype_Prop.make_distincts [descr]); + val half_distincts = Datatype_Prop.make_distincts [descr]; val ind = Datatype_Prop.make_ind [descr]; val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts]; diff -r 66b419de5f38 -r 4ff377493dbb src/HOL/Tools/Datatype/datatype_prop.ML --- a/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 13:40:20 2011 +0100 +++ b/src/HOL/Tools/Datatype/datatype_prop.ML Thu Dec 15 14:11:57 2011 +0100 @@ -10,7 +10,7 @@ val indexify_names: string list -> string list val make_tnames: typ list -> string list val make_injs : descr list -> term list list - val make_distincts : descr list -> (int * term list) list (*no symmetric inequalities*) + val make_distincts : descr list -> term list list (*no symmetric inequalities*) val make_ind : descr list -> term val make_casedists : descr list -> term list val make_primrec_Ts : descr list -> string list -> typ list * typ list @@ -99,7 +99,7 @@ in map make_distincts'' constrs @ make_distincts' T constrs end; in map2 (fn ((_, (_, _, constrs))) => fn T => - (length constrs, make_distincts' T (map prep_constr constrs))) (hd descr) newTs + make_distincts' T (map prep_constr constrs)) (hd descr) newTs end;