238 |
236 |
239 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) |
237 val _ = tracing ("eqs\n" ^ cat_lines (map (Syntax.string_of_term lthy) eqs)) |
240 val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs)) |
238 val _ = tracing ("map eqs\n" ^ @{make_string} (map aux2 eqs)) |
241 val _ = tracing ("ordered'\n" ^ @{make_string} ordered') |
239 val _ = tracing ("ordered'\n" ^ @{make_string} ordered') |
242 in |
240 in |
243 ordered' (*map aux2 eqs*) |
241 ordered' |
244 end |
242 end |
245 *} |
243 *} |
246 |
244 |
247 ML {* |
245 ML {* |
248 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
246 fun raw_nominal_decls dts bn_funs bn_eqs binds lthy = |
376 |
374 |
377 ML {* |
375 ML {* |
378 (* for testing porposes - to exit the procedure early *) |
376 (* for testing porposes - to exit the procedure early *) |
379 exception TEST of Proof.context |
377 exception TEST of Proof.context |
380 |
378 |
381 val STEPS = 10 |
379 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10); |
382 *} |
380 |
|
381 fun get_STEPS ctxt = Config.get ctxt STEPS |
|
382 *} |
|
383 |
|
384 setup STEPS_setup |
|
385 |
383 |
386 |
384 ML {* |
387 ML {* |
385 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
388 fun nominal_datatype2 dts bn_funs bn_eqs bclauses lthy = |
386 let |
389 let |
387 (* definition of the raw datatype and raw bn-functions *) |
390 (* definition of the raw datatype and raw bn-functions *) |
388 val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = |
391 val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = |
389 if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
392 if get_STEPS lthy > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
390 else raise TEST lthy |
393 else raise TEST lthy |
391 |
394 |
392 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
395 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
393 val {descr, sorts, ...} = dtinfo; |
396 val {descr, sorts, ...} = dtinfo; |
394 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
397 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
404 val induct_thm = #induct dtinfo; |
407 val induct_thm = #induct dtinfo; |
405 val exhaust_thms = map #exhaust dtinfos; |
408 val exhaust_thms = map #exhaust dtinfos; |
406 |
409 |
407 (* definitions of raw permutations *) |
410 (* definitions of raw permutations *) |
408 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
411 val ((raw_perm_def, raw_perm_simps, perms), lthy2) = |
409 if STEPS > 2 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
412 if get_STEPS lthy > 2 |
|
413 then Local_Theory.theory_result (define_raw_perms descr sorts induct_thm (length dts)) lthy1 |
410 else raise TEST lthy1 |
414 else raise TEST lthy1 |
411 |
415 |
412 (* definition of raw fv_functions *) |
416 (* definition of raw fv_functions *) |
413 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
417 val morphism_2_0 = ProofContext.export_morphism lthy2 lthy |
414 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
418 fun export_fun f (t, n , l) = (f t, n, map (map (apsnd (Option.map f))) l); |
424 |
428 |
425 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
429 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
426 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
430 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
427 |
431 |
428 val ((fv, fvbn), fv_def, lthy3a) = |
432 val ((fv, fvbn), fv_def, lthy3a) = |
429 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
433 if get_STEPS lthy > 3 |
|
434 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
430 else raise TEST lthy3 |
435 else raise TEST lthy3 |
431 |
436 |
432 |
437 |
433 (* definition of raw alphas *) |
438 (* definition of raw alphas *) |
434 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
439 val (((alpha_ts, alpha_intros), (alpha_cases, alpha_induct)), lthy4) = |
435 if STEPS > 4 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a |
440 if get_STEPS lthy > 4 |
|
441 then define_raw_alpha dtinfo bn_funs_decls raw_bclauses fv lthy3a |
436 else raise TEST lthy3a |
442 else raise TEST lthy3a |
437 |
443 |
438 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
444 val (alpha_ts_nobn, alpha_ts_bn) = chop (length fv) alpha_ts |
439 |
445 |
440 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |
446 val dts_names = map (fn (i, (s, _, _)) => (s, i)) (#descr dtinfo); |