# HG changeset patch # User Christian Urban # Date 1274438418 -3600 # Node ID aecebd5ed424ac397d1dd3308a9b9e207c29269b # Parent d134bd4f6d1b0566dcd42c0a5e2f99c89830e01c hving a working fv-definition without the export diff -r d134bd4f6d1b -r aecebd5ed424 Nominal/Ex/SingleLet.thy --- a/Nominal/Ex/SingleLet.thy Fri May 21 05:58:23 2010 +0100 +++ b/Nominal/Ex/SingleLet.thy Fri May 21 11:40:18 2010 +0100 @@ -19,7 +19,7 @@ where "bn (As x t) = {atom x}" -thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] +thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars] ML {* Inductive.the_inductive *} thm trm_assg.fv diff -r d134bd4f6d1b -r aecebd5ed424 Nominal/NewParser.thy --- a/Nominal/NewParser.thy Fri May 21 05:58:23 2010 +0100 +++ b/Nominal/NewParser.thy Fri May 21 11:40:18 2010 +0100 @@ -251,7 +251,7 @@ val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs - val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds + val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_env binds val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs) val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy @@ -261,7 +261,7 @@ fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr; in - (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy2) + (raw_dt_names, raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_bn_funs2, raw_bn_eqs2, raw_bn_descr_exp, raw_bn_descr, lthy1) end *} @@ -312,7 +312,7 @@ val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr) val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2) - val _ = tracing ("bclauses " ^ @{make_string} bclauses) + val _ = tracing ("raw_bclauses " ^ @{make_string} raw_bclauses) val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs) val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs) val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2) @@ -349,7 +349,7 @@ val (fv, fvbn, fv_def, lthy3a) = if get_STEPS lthy2 > 3 - then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) bn_funs) (map snd bn_eqs) descr sorts raw_bn_descr raw_bn_descr2 raw_bclauses lthy3 + then define_raw_fvs (map (fn (x, _, _) => Binding.name_of x) raw_bn_funs2) (map snd raw_bn_eqs2) descr sorts raw_bn_descr2 raw_bn_descr2 raw_bclauses lthy3 else raise TEST lthy3 @@ -575,7 +575,7 @@ fun prep_binder env bn_str = case (Syntax.read_term lthy bn_str) of Free (x, _) => (NONE, index_lookup env x) - | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) + | Const (a, T) $ Free (x, _) => (SOME (Free (Long_Name.base_name a, T)), index_lookup env x) | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") fun prep_body env bn_str = index_lookup env bn_str diff -r d134bd4f6d1b -r aecebd5ed424 Nominal/nominal_dt_rawfuns.ML --- a/Nominal/nominal_dt_rawfuns.ML Fri May 21 05:58:23 2010 +0100 +++ b/Nominal/nominal_dt_rawfuns.ML Fri May 21 11:40:18 2010 +0100 @@ -123,6 +123,17 @@ NONE => mk_supp arg | SOME fv => fv $ arg end +handle Option => error "fv_map lookup " + +fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = +let + val arg = nth args i +in + case bn_option of + NONE => (setify lthy arg, @{term "{}::atom set"}) + | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) +end +handle Option => error "fv_bn_map lookup " fun mk_fv_bn_body fv_map fv_bn_map bn_args args i = let @@ -136,15 +147,7 @@ | SOME (NONE) => @{term "{}::atom set"} | SOME (SOME bn) => the (AList.lookup (op=) fv_bn_map bn) $ arg end - -fun mk_fv_binder lthy fv_bn_map args (bn_option, i) = -let - val arg = nth args i -in - case bn_option of - NONE => (setify lthy arg, @{term "{}::atom set"}) - | SOME bn => (to_set (bn $ arg), the (AList.lookup (op=) fv_bn_map bn) $ arg) -end +handle Option => error "fv_map/fv_bn_map lookup " fun mk_fv_rhs lthy fv_map fv_bn_map args (BC (_, binders, bodies)) = let @@ -154,16 +157,13 @@ fold_union (mk_diff (fold_union t1, fold_union t2)::t3) end +(* in case of fv_bn we have to treat the case special, where an + "empty" binding clause is given *) fun mk_fv_bn_rhs lthy fv_map fv_bn_map bn_args args bclause = case bclause of BC (_, [], bodies) => fold_union (map (mk_fv_bn_body fv_map fv_bn_map bn_args args) bodies) - | BC (_, binders, bodies) => - let - val t1 = map (mk_fv_body fv_map args) bodies - val (t2, t3) = split_list (map (mk_fv_binder lthy fv_bn_map args) binders) - in - fold_union (mk_diff (fold_union t1, fold_union t2)::t3) - end + | _ => mk_fv_rhs lthy fv_map fv_bn_map args bclause + fun mk_fv_eq lthy fv_map fv_bn_map (constr, ty, arg_tys) bclauses = let @@ -223,14 +223,15 @@ val constrs_info = all_dtyp_constrs_types dt_descr sorts - val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map2)) constrs_info bclausesss + val fv_eqs2 = map2 (map2 (mk_fv_eq lthy fv_map fv_bn_map3)) constrs_info bclausesss val fv_bn_eqs2 = map (mk_fv_bn_eqs lthy fv_map fv_bn_map3 constrs_info bclausesss) bn_funs2 - val _ = tracing ("functions to be defined\n " ^ @{make_string} (fv_names @ fv_bn_names2)) - val _ = tracing ("equations\n " ^ cat_lines (map (Syntax.string_of_term lthy) (flat fv_eqs2 @ flat fv_bn_eqs2))) + val _ = tracing ("functions to be defined\n " ^ @{make_string} (t1 @ fv_names @ fv_bn_names2)) + val _ = tracing ("equations\n " ^ + cat_lines (map (Syntax.string_of_term lthy) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2))) - val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (fv_names @ fv_bn_names2) - val all_fv_eqs = map (pair Attrib.empty_binding) (flat fv_eqs2 @ flat fv_bn_eqs2) + val all_fv_names = map (fn s => (Binding.name s, NONE, NoSyn)) (t1 @ fv_names @ fv_bn_names2) + val all_fv_eqs = map (pair Attrib.empty_binding) (t2 @ flat fv_eqs2 @ flat fv_bn_eqs2) fun pat_completeness_auto lthy = Pat_Completeness.pat_completeness_tac lthy 1