784 |-> (fn thing => fn (_, program) => (thing, program))); |
784 |-> (fn thing => fn (_, program) => (thing, program))); |
785 |
785 |
786 |
786 |
787 (* program generation *) |
787 (* program generation *) |
788 |
788 |
|
789 fun check_abstract_constructors thy consts = |
|
790 case filter (Code.is_abstr thy) consts of |
|
791 [] => () |
|
792 | abstrs => error ("Cannot export abstract constructor(s): " |
|
793 ^ commas (map (Code.string_of_const thy) abstrs)); |
|
794 |
789 fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts = |
795 fun invoke_generation_for_consts ctxt { ignore_cache, permissive } { algebra, eqngr } consts = |
790 Code_Preproc.timed "translating program" #ctxt |
796 let |
791 (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt |
797 val thy = Proof_Context.theory_of ctxt; |
792 (fold_map (ensure_const ctxt algebra eqngr permissive)) consts) |
798 val _ = if permissive then () |
793 { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts }; |
799 else check_abstract_constructors thy consts; |
|
800 in |
|
801 Code_Preproc.timed "translating program" #ctxt |
|
802 (fn { ctxt, algebra, eqngr, consts } => invoke_generation ignore_cache ctxt |
|
803 (fold_map (ensure_const ctxt algebra eqngr permissive)) consts) |
|
804 { ctxt = ctxt, algebra = algebra, eqngr = eqngr, consts = consts } |
|
805 end; |
794 |
806 |
795 fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts = |
807 fun invoke_generation_for_consts' ctxt ignore_cache_and_permissive consts = |
796 invoke_generation_for_consts ctxt |
808 invoke_generation_for_consts ctxt |
797 { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive } |
809 { ignore_cache = ignore_cache_and_permissive, permissive = ignore_cache_and_permissive } |
798 (Code_Preproc.obtain ignore_cache_and_permissive |
810 (Code_Preproc.obtain ignore_cache_and_permissive |
912 fun read_const_exprs_internal ctxt = |
924 fun read_const_exprs_internal ctxt = |
913 let |
925 let |
914 val thy = Proof_Context.theory_of ctxt; |
926 val thy = Proof_Context.theory_of ctxt; |
915 fun consts_of thy' = |
927 fun consts_of thy' = |
916 fold (fn (c, (_, NONE)) => cons c | _ => I) |
928 fold (fn (c, (_, NONE)) => cons c | _ => I) |
917 (#constants (Consts.dest (Sign.consts_of thy'))) []; |
929 (#constants (Consts.dest (Sign.consts_of thy'))) [] |
|
930 |> filter_out (Code.is_abstr thy); |
918 fun belongs_here thy' c = forall |
931 fun belongs_here thy' c = forall |
919 (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); |
932 (fn thy'' => not (Sign.declared_const thy'' c)) (Theory.parents_of thy'); |
920 fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); |
933 fun consts_of_select thy' = filter (belongs_here thy') (consts_of thy'); |
921 fun read_const_expr str = |
934 fun read_const_expr str = |
922 (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of |
935 (case Syntax.parse_input ctxt (K NONE) (K Markup.empty) (SOME o Symbol_Pos.implode o #1) str of |
932 |
945 |
933 fun read_const_exprs ctxt const_exprs = |
946 fun read_const_exprs ctxt const_exprs = |
934 let |
947 let |
935 val (consts, consts_permissive) = |
948 val (consts, consts_permissive) = |
936 read_const_exprs_internal ctxt const_exprs; |
949 read_const_exprs_internal ctxt const_exprs; |
937 val consts' = implemented_deps |
950 val consts' = |
938 (consts_program_permissive ctxt consts_permissive); |
951 consts_program_permissive ctxt consts_permissive |
|
952 |> implemented_deps |
|
953 |> filter_out (Code.is_abstr (Proof_Context.theory_of ctxt)); |
939 in union (op =) consts' consts end; |
954 in union (op =) consts' consts end; |
940 |
955 |
941 |
956 |
942 (** diagnostic commands **) |
957 (** diagnostic commands **) |
943 |
958 |