equal
deleted
inserted
replaced
245 |
245 |
246 ML {* |
246 ML {* |
247 (* for testing porposes - to exit the procedure early *) |
247 (* for testing porposes - to exit the procedure early *) |
248 exception TEST of Proof.context |
248 exception TEST of Proof.context |
249 |
249 |
250 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 10); |
250 val (STEPS, STEPS_setup) = Attrib.config_int "STEPS" (K 0); |
251 |
251 |
252 fun get_STEPS ctxt = Config.get ctxt STEPS |
252 fun get_STEPS ctxt = Config.get ctxt STEPS |
253 *} |
253 *} |
254 |
254 |
255 setup STEPS_setup |
255 setup STEPS_setup |
624 fun prepare_dts dt_strs lthy = |
624 fun prepare_dts dt_strs lthy = |
625 let |
625 let |
626 val thy = ProofContext.theory_of lthy |
626 val thy = ProofContext.theory_of lthy |
627 |
627 |
628 fun mk_type full_tname tvrs = |
628 fun mk_type full_tname tvrs = |
629 Type (full_tname, map (fn a => TVar ((a, 0), [])) tvrs) |
629 Type (full_tname, map (fn a => TFree (a, @{sort "{pt, fs}"})) tvrs) |
630 |
630 |
631 fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = |
631 fun prep_cnstr full_tname tvs (cname, anno_tys, mx, _) = |
632 let |
632 let |
633 val tys = map (Syntax.read_typ lthy o snd) anno_tys |
633 val tys = map (Syntax.read_typ lthy o snd) anno_tys |
634 val ty = mk_type full_tname tvs |
634 val ty = mk_type full_tname tvs |
644 in |
644 in |
645 (cnstrs', (tvs, tname, mx, cnstrs'')) |
645 (cnstrs', (tvs, tname, mx, cnstrs'')) |
646 end |
646 end |
647 |
647 |
648 val (cnstrs, dts) = split_list (map prep_dt dt_strs) |
648 val (cnstrs, dts) = split_list (map prep_dt dt_strs) |
|
649 |
|
650 val _ = tracing ("Contructors:\n" ^ cat_lines (map @{make_string} cnstrs)) |
649 in |
651 in |
650 lthy |
652 lthy |
651 |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) |
653 |> Local_Theory.theory (Sign.add_consts_i (flat cnstrs)) |
652 |> pair dts |
654 |> pair dts |
653 end |
655 end |