249 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
249 val bn_fun_full_env = map (pairself (Long_Name.qualify thy_name)) |
250 (bn_fun_strs ~~ bn_fun_strs') |
250 (bn_fun_strs ~~ bn_fun_strs') |
251 |
251 |
252 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
252 val (raw_dt_names, raw_dts) = rawify_dts dt_names dts dts_env |
253 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
253 val (raw_bn_funs, raw_bn_eqs) = rawify_bn_funs dts_env cnstrs_env bn_fun_env bn_funs bn_eqs |
254 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_full_env binds |
254 val raw_bclauses = rawify_bclauses dts_env cnstrs_env bn_fun_env binds |
255 val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
255 val raw_bn_descr = prep_bn_descr lthy dt_full_names' raw_dts (map snd raw_bn_eqs) |
256 |
256 |
257 val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
257 val (raw_dt_names, lthy1) = add_datatype_wrapper raw_dt_names raw_dts lthy |
258 val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
258 val (raw_bn_funs2, raw_bn_eqs2, lthy2) = add_primrec_wrapper raw_bn_funs raw_bn_eqs lthy1 |
259 |
259 |
260 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
260 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
261 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
261 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
262 val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr; |
262 val raw_bn_descr_exp = map (export_fun (Morphism.term morphism_2_0)) raw_bn_descr; |
263 in |
263 in |
264 (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) |
264 (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) |
265 end |
265 end |
266 *} |
266 *} |
267 |
267 |
268 lemma equivp_hack: "equivp x" |
268 lemma equivp_hack: "equivp x" |
269 sorry |
269 sorry |
310 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
310 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
311 else raise TEST lthy |
311 else raise TEST lthy |
312 |
312 |
313 val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr) |
313 val _ = tracing ("raw_bn_descr " ^ @{make_string} raw_bn_descr) |
314 val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2) |
314 val _ = tracing ("raw_bn_descr2 " ^ @{make_string} raw_bn_descr2) |
315 val _ = tracing ("bclauses " ^ @{make_string} bclauses) |
315 val _ = tracing ("raw_bclauses " ^ @{make_string} raw_bclauses) |
316 val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs) |
316 val _ = tracing ("raw_bn_fund " ^ @{make_string} raw_bn_funs) |
317 val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs) |
317 val _ = tracing ("raw_bn_eqs " ^ @{make_string} raw_bn_eqs) |
318 val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2) |
318 val _ = tracing ("raw_bn_fund2 " ^ @{make_string} raw_bn_funs2) |
319 val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2)) |
319 val _ = tracing ("raw_bn_eqs2 " ^ cat_lines (map (Syntax.string_of_term lthy o snd) raw_bn_eqs2)) |
320 |
320 |
347 (* definition of raw fv_functions *) |
347 (* definition of raw fv_functions *) |
348 val lthy3 = Theory_Target.init NONE thy; |
348 val lthy3 = Theory_Target.init NONE thy; |
349 |
349 |
350 val (fv, fvbn, fv_def, lthy3a) = |
350 val (fv, fvbn, fv_def, lthy3a) = |
351 if get_STEPS lthy2 > 3 |
351 if get_STEPS lthy2 > 3 |
352 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 |
352 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 |
353 else raise TEST lthy3 |
353 else raise TEST lthy3 |
354 |
354 |
355 |
355 |
356 (* definition of raw alphas *) |
356 (* definition of raw alphas *) |
357 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
357 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
573 |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) |
573 |> map (map (fn (_, antys, _, bns) => (map fst antys, bns))) |
574 |
574 |
575 fun prep_binder env bn_str = |
575 fun prep_binder env bn_str = |
576 case (Syntax.read_term lthy bn_str) of |
576 case (Syntax.read_term lthy bn_str) of |
577 Free (x, _) => (NONE, index_lookup env x) |
577 Free (x, _) => (NONE, index_lookup env x) |
578 | Const (a, T) $ Free (x, _) => (SOME (Const (a, T)), index_lookup env x) |
578 | Const (a, T) $ Free (x, _) => (SOME (Free (Long_Name.base_name a, T)), index_lookup env x) |
579 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
579 | _ => error ("The term " ^ bn_str ^ " is not allowed as binding function.") |
580 |
580 |
581 fun prep_body env bn_str = index_lookup env bn_str |
581 fun prep_body env bn_str = index_lookup env bn_str |
582 |
582 |
583 fun prep_mode "bind" = Lst |
583 fun prep_mode "bind" = Lst |