365 (* definition of the raw datatype and raw bn-functions *) |
365 (* definition of the raw datatype and raw bn-functions *) |
366 val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = |
366 val ((((raw_dt_names, (raw_bn_funs, raw_bn_eqs)), raw_bclauses), raw_bns), lthy1) = |
367 if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
367 if STEPS > 1 then raw_nominal_decls dts bn_funs bn_eqs bclauses lthy |
368 else raise TEST lthy |
368 else raise TEST lthy |
369 |
369 |
370 val _ = tracing ("raw_bn_eqs\n" ^ cat_lines (map (@{make_string} o prop_of) raw_bn_eqs)) |
|
371 |
|
372 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
|
373 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
|
374 |
|
375 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
370 val dtinfo = Datatype.the_info (ProofContext.theory_of lthy1) (hd raw_dt_names); |
376 val {descr, sorts, ...} = dtinfo; |
371 val {descr, sorts, ...} = dtinfo; |
377 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
372 val raw_tys = map (fn (i, _) => nth_dtyp descr sorts i) descr; |
378 val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) |
373 val all_typs = map (fn i => Datatype_Aux.typ_of_dtyp descr sorts (Datatype_Aux.DtRec i)) (map fst descr) |
379 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
374 val all_full_tnames = map (fn (_, (n, _, _)) => n) descr; |
404 val thy_name = Context.theory_name thy |
399 val thy_name = Context.theory_name thy |
405 |
400 |
406 val lthy3 = Theory_Target.init NONE thy; |
401 val lthy3 = Theory_Target.init NONE thy; |
407 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
402 val raw_bn_funs = map (fn (f, _, _) => f) bn_funs_decls; |
408 |
403 |
409 (* |
|
410 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
404 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns) |
411 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp) |
405 val _ = tracing ("raw_bns\n" ^ @{make_string} raw_bns_exp) |
412 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
406 val _ = tracing ("bn_funs\n" ^ @{make_string} bn_funs_decls) |
413 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
407 val _ = tracing ("raw_bclauses\n" ^ @{make_string} raw_bclauses) |
414 *) |
408 |
415 val ((fv, fvbn), fv_def, lthy3a) = |
409 val ((fv, fvbn), fv_def, lthy3a) = |
416 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
410 if STEPS > 3 then define_raw_fv descr sorts bn_funs_decls raw_bclauses lthy3 |
417 else raise TEST lthy3 |
411 else raise TEST lthy3 |
418 |
412 |
419 |
413 |