3031 val setup = PredData.put (Graph.empty) #> |
3031 val setup = PredData.put (Graph.empty) #> |
3032 Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro)) |
3032 Attrib.setup @{binding code_pred_intro} (Scan.succeed (attrib add_intro)) |
3033 "adding alternative introduction rules for code generation of inductive predicates" |
3033 "adding alternative introduction rules for code generation of inductive predicates" |
3034 |
3034 |
3035 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *) |
3035 (* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *) |
|
3036 (* FIXME ... this is important to avoid changing the background theory below *) |
3036 fun generic_code_pred prep_const options raw_const lthy = |
3037 fun generic_code_pred prep_const options raw_const lthy = |
3037 let |
3038 let |
3038 val thy = ProofContext.theory_of lthy |
3039 val thy = ProofContext.theory_of lthy |
3039 val const = prep_const thy raw_const |
3040 val const = prep_const thy raw_const |
3040 val ctxt = ProofContext.init_global thy |
3041 val ctxt = ProofContext.init_global thy |
3041 val lthy' = Local_Theory.theory (PredData.map |
3042 val lthy' = Local_Theory.background_theory (PredData.map |
3042 (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy |
3043 (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy |
3043 val thy' = ProofContext.theory_of lthy' |
3044 val thy' = ProofContext.theory_of lthy' |
3044 val ctxt' = ProofContext.init_global thy' |
3045 val ctxt' = ProofContext.init_global thy' |
3045 val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt') |
3046 val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt') |
3046 fun mk_cases const = |
3047 fun mk_cases const = |
3061 fun after_qed thms goal_ctxt = |
3062 fun after_qed thms goal_ctxt = |
3062 let |
3063 let |
3063 val global_thms = ProofContext.export goal_ctxt |
3064 val global_thms = ProofContext.export goal_ctxt |
3064 (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms) |
3065 (ProofContext.init_global (ProofContext.theory_of goal_ctxt)) (map the_single thms) |
3065 in |
3066 in |
3066 goal_ctxt |> Local_Theory.theory (fold set_elim global_thms #> |
3067 goal_ctxt |> Local_Theory.background_theory (fold set_elim global_thms #> |
3067 ((case compilation options of |
3068 ((case compilation options of |
3068 Pred => add_equations |
3069 Pred => add_equations |
3069 | DSeq => add_dseq_equations |
3070 | DSeq => add_dseq_equations |
3070 | Pos_Random_DSeq => add_random_dseq_equations |
3071 | Pos_Random_DSeq => add_random_dseq_equations |
3071 | Depth_Limited => add_depth_limited_equations |
3072 | Depth_Limited => add_depth_limited_equations |