src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
changeset 37007 116670499530
parent 37006 25fdef26b460
child 37009 4ba91ea2bf6d
     1.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:08 2010 +0200
     1.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Wed May 19 18:24:09 2010 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    val modes_of: compilation -> Proof.context -> string -> mode list
     1.5    val all_modes_of : compilation -> Proof.context -> (string * mode list) list
     1.6    val all_random_modes_of : Proof.context -> (string * mode list) list
     1.7 -  val intros_of : theory -> string -> thm list
     1.8 +  val intros_of : Proof.context -> string -> thm list
     1.9    val add_intro : thm -> theory -> theory
    1.10    val set_elim : thm -> theory -> theory
    1.11    val register_alternative_function : string -> mode -> string -> theory -> theory
    1.12 @@ -39,7 +39,7 @@
    1.13    val force_modes_and_compilations : string ->
    1.14      (mode * ((compilation_funs -> typ -> term) * bool)) list -> theory -> theory
    1.15    val preprocess_intro : theory -> thm -> thm
    1.16 -  val print_stored_rules : theory -> unit
    1.17 +  val print_stored_rules : Proof.context -> unit
    1.18    val print_all_modes : compilation -> Proof.context -> unit
    1.19    val mk_casesrule : Proof.context -> term -> thm list -> term
    1.20    val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref
    1.21 @@ -230,27 +230,27 @@
    1.22  
    1.23  (* queries *)
    1.24  
    1.25 -fun lookup_pred_data thy name =
    1.26 -  Option.map rep_pred_data (try (Graph.get_node (PredData.get thy)) name)
    1.27 +fun lookup_pred_data ctxt name =
    1.28 +  Option.map rep_pred_data (try (Graph.get_node (PredData.get (ProofContext.theory_of ctxt))) name)
    1.29  
    1.30 -fun the_pred_data thy name = case lookup_pred_data thy name
    1.31 +fun the_pred_data ctxt name = case lookup_pred_data ctxt name
    1.32   of NONE => error ("No such predicate " ^ quote name)  
    1.33    | SOME data => data;
    1.34  
    1.35 -val is_registered = is_some oo lookup_pred_data o ProofContext.theory_of
    1.36 +val is_registered = is_some oo lookup_pred_data
    1.37  
    1.38  val all_preds_of = Graph.keys o PredData.get o ProofContext.theory_of
    1.39  
    1.40 -fun intros_of thy = #intros o the_pred_data thy
    1.41 +val intros_of = #intros oo the_pred_data
    1.42  
    1.43 -fun the_elim_of thy name = case #elim (the_pred_data thy name)
    1.44 +fun the_elim_of ctxt name = case #elim (the_pred_data ctxt name)
    1.45   of NONE => error ("No elimination rule for predicate " ^ quote name)
    1.46 -  | SOME thm => Thm.transfer thy thm
    1.47 +  | SOME thm => thm
    1.48    
    1.49 -val has_elim = is_some o #elim oo the_pred_data;
    1.50 +val has_elim = is_some o #elim oo the_pred_data
    1.51  
    1.52  fun function_names_of compilation ctxt name =
    1.53 -  case AList.lookup (op =) (#function_names (the_pred_data (ProofContext.theory_of ctxt) name)) compilation of
    1.54 +  case AList.lookup (op =) (#function_names (the_pred_data ctxt name)) compilation of
    1.55      NONE => error ("No " ^ string_of_compilation compilation
    1.56        ^ "functions defined for predicate " ^ quote name)
    1.57    | SOME fun_names => fun_names
    1.58 @@ -270,30 +270,30 @@
    1.59  
    1.60  val all_random_modes_of = all_modes_of Random
    1.61  
    1.62 -fun defined_functions compilation ctxt name = case lookup_pred_data (ProofContext.theory_of ctxt) name of
    1.63 +fun defined_functions compilation ctxt name = case lookup_pred_data ctxt name of
    1.64      NONE => false
    1.65    | SOME data => AList.defined (op =) (#function_names data) compilation
    1.66  
    1.67  fun needs_random ctxt s m =
    1.68 -  member (op =) (#needs_random (the_pred_data (ProofContext.theory_of ctxt) s)) m
    1.69 +  member (op =) (#needs_random (the_pred_data ctxt s)) m
    1.70  
    1.71 -fun lookup_predfun_data thy name mode =
    1.72 +fun lookup_predfun_data ctxt name mode =
    1.73    Option.map rep_predfun_data
    1.74 -    (AList.lookup (op =) (#predfun_data (the_pred_data thy name)) mode)
    1.75 +    (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
    1.76  
    1.77 -fun the_predfun_data thy name mode =
    1.78 -  case lookup_predfun_data thy name mode of
    1.79 +fun the_predfun_data ctxt name mode =
    1.80 +  case lookup_predfun_data ctxt name mode of
    1.81      NONE => error ("No function defined for mode " ^ string_of_mode mode ^
    1.82        " of predicate " ^ name)
    1.83    | SOME data => data;
    1.84  
    1.85 -val predfun_definition_of = #definition ooo the_predfun_data o ProofContext.theory_of
    1.86 +val predfun_definition_of = #definition ooo the_predfun_data
    1.87  
    1.88 -val predfun_intro_of = #intro ooo the_predfun_data o ProofContext.theory_of
    1.89 +val predfun_intro_of = #intro ooo the_predfun_data
    1.90  
    1.91 -val predfun_elim_of = #elim ooo the_predfun_data o ProofContext.theory_of
    1.92 +val predfun_elim_of = #elim ooo the_predfun_data
    1.93  
    1.94 -val predfun_neg_intro_of = #neg_intro ooo the_predfun_data o ProofContext.theory_of
    1.95 +val predfun_neg_intro_of = #neg_intro ooo the_predfun_data
    1.96  
    1.97  (* diagnostic display functions *)
    1.98  
    1.99 @@ -331,17 +331,17 @@
   1.100      print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term ctxt)
   1.101    else K ()
   1.102  
   1.103 -fun print_stored_rules thy =
   1.104 +fun print_stored_rules ctxt =
   1.105    let
   1.106 -    val preds = (Graph.keys o PredData.get) thy
   1.107 +    val preds = Graph.keys (PredData.get (ProofContext.theory_of ctxt))
   1.108      fun print pred () = let
   1.109        val _ = writeln ("predicate: " ^ pred)
   1.110        val _ = writeln ("introrules: ")
   1.111 -      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm_global thy thm))
   1.112 -        (rev (intros_of thy pred)) ()
   1.113 +      val _ = fold (fn thm => fn u => writeln (Display.string_of_thm ctxt thm))
   1.114 +        (rev (intros_of ctxt pred)) ()
   1.115      in
   1.116 -      if (has_elim thy pred) then
   1.117 -        writeln ("elimrule: " ^ Display.string_of_thm_global thy (the_elim_of thy pred))
   1.118 +      if (has_elim ctxt pred) then
   1.119 +        writeln ("elimrule: " ^ Display.string_of_thm ctxt (the_elim_of ctxt pred))
   1.120        else
   1.121          writeln ("no elimrule defined")
   1.122      end
   1.123 @@ -613,21 +613,21 @@
   1.124  
   1.125  val no_compilation = ([], ([], []))
   1.126  
   1.127 -fun fetch_pred_data thy name =
   1.128 -  case try (Inductive.the_inductive (ProofContext.init_global thy)) name of
   1.129 +fun fetch_pred_data ctxt name =
   1.130 +  case try (Inductive.the_inductive ctxt) name of
   1.131      SOME (info as (_, result)) => 
   1.132        let
   1.133          fun is_intro_of intro =
   1.134            let
   1.135              val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro))
   1.136 -          in (fst (dest_Const const) = name) end;      
   1.137 +          in (fst (dest_Const const) = name) end;
   1.138 +        val thy = ProofContext.theory_of ctxt
   1.139          val intros =
   1.140            (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result)))
   1.141          val index = find_index (fn s => s = name) (#names (fst info))
   1.142          val pre_elim = nth (#elims result) index
   1.143          val pred = nth (#preds result) index
   1.144          val nparams = length (Inductive.params_of (#raw_induct result))
   1.145 -        val ctxt = ProofContext.init_global thy
   1.146          val elim_t = mk_casesrule ctxt pred intros
   1.147          val elim =
   1.148            prove_casesrule ctxt (pred, (pre_elim, nparams)) elim_t
   1.149 @@ -2409,10 +2409,9 @@
   1.150  
   1.151  fun prove_one_direction options ctxt clauses preds pred mode moded_clauses =
   1.152    let
   1.153 -    val thy = ProofContext.theory_of ctxt
   1.154      val T = the (AList.lookup (op =) preds pred)
   1.155      val nargs = length (binder_types T)
   1.156 -    val pred_case_rule = the_elim_of thy pred
   1.157 +    val pred_case_rule = the_elim_of ctxt pred
   1.158    in
   1.159      REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))
   1.160      THEN print_tac options "before applying elim rule"
   1.161 @@ -2519,7 +2518,7 @@
   1.162    
   1.163  fun prove_clause2 options ctxt pred mode (ts, ps) i =
   1.164    let
   1.165 -    val pred_intro_rule = nth (intros_of (ProofContext.theory_of ctxt) pred) (i - 1)
   1.166 +    val pred_intro_rule = nth (intros_of ctxt pred) (i - 1)
   1.167      val (in_ts, clause_out_ts) = split_mode mode ts;
   1.168      fun prove_prems2 out_ts [] =
   1.169        print_tac options "before prove_match2 - last call:"
   1.170 @@ -2762,9 +2761,8 @@
   1.171  
   1.172  (* create code equation *)
   1.173  
   1.174 -fun add_code_equations thy preds result_thmss =
   1.175 +fun add_code_equations ctxt preds result_thmss =
   1.176    let
   1.177 -    val ctxt = ProofContext.init_global thy
   1.178      fun add_code_equation (predname, T) (pred, result_thms) =
   1.179        let
   1.180          val full_mode = fold_rev (curry Fun) (map (K Input) (binder_types T)) Bool
   1.181 @@ -2801,7 +2799,7 @@
   1.182    define_functions : options -> (string * typ) list -> string * (bool * mode) list -> theory -> theory,
   1.183    prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list
   1.184      -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table,
   1.185 -  add_code_equations : theory -> (string * typ) list
   1.186 +  add_code_equations : Proof.context -> (string * typ) list
   1.187      -> (string * thm list) list -> (string * thm list) list,
   1.188    comp_modifiers : Comp_Mod.comp_modifiers,
   1.189    use_random : bool,
   1.190 @@ -2812,6 +2810,7 @@
   1.191    let
   1.192      fun dest_steps (Steps s) = s
   1.193      val compilation = Comp_Mod.compilation (#comp_modifiers (dest_steps steps))
   1.194 +    val ctxt = ProofContext.init_global thy
   1.195      val _ = print_step options
   1.196        ("Starting predicate compiler (compilation: " ^ string_of_compilation compilation
   1.197          ^ ") for predicates " ^ commas prednames ^ "...")
   1.198 @@ -2819,10 +2818,10 @@
   1.199        (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*)
   1.200      val _ =
   1.201        if show_intermediate_results options then
   1.202 -        tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames)))
   1.203 +        tracing (commas (map (Display.string_of_thm ctxt) (maps (intros_of ctxt) prednames)))
   1.204        else ()
   1.205      val (preds, all_vs, param_vs, all_modes, clauses) =
   1.206 -      prepare_intrs options compilation thy prednames (maps (intros_of thy) prednames)
   1.207 +      prepare_intrs options compilation thy prednames (maps (intros_of ctxt) prednames)
   1.208      val _ = print_step options "Infering modes..."
   1.209      val ((moded_clauses, errors), thy') =
   1.210        Output.cond_timeit true "Infering modes"
   1.211 @@ -2848,7 +2847,7 @@
   1.212      val result_thms =
   1.213        Output.cond_timeit (!Quickcheck.timing) "Proving equations...." (fn _ =>
   1.214        #prove (dest_steps steps) options thy'' clauses preds moded_clauses compiled_terms)
   1.215 -    val result_thms' = #add_code_equations (dest_steps steps) thy'' preds
   1.216 +    val result_thms' = #add_code_equations (dest_steps steps) ctxt'' preds
   1.217        (maps_modes result_thms)
   1.218      val qname = #qname (dest_steps steps)
   1.219      val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute
   1.220 @@ -2883,7 +2882,7 @@
   1.221      val defined = defined_functions (Comp_Mod.compilation (#comp_modifiers (dest_steps steps)))
   1.222      val ctxt = ProofContext.init_global thy
   1.223      val thy' = thy
   1.224 -      |> PredData.map (fold (extend (fetch_pred_data thy) (depending_preds_of ctxt)) names)
   1.225 +      |> PredData.map (fold (extend (fetch_pred_data ctxt) (depending_preds_of ctxt)) names)
   1.226        |> Theory.checkpoint;
   1.227      fun strong_conn_of gr keys =
   1.228        Graph.strong_conn (Graph.subgraph (member (op =) (Graph.all_succs gr keys)) gr)
   1.229 @@ -3036,14 +3035,15 @@
   1.230      val const = prep_const thy raw_const
   1.231      val ctxt = ProofContext.init_global thy
   1.232      val lthy' = Local_Theory.theory (PredData.map
   1.233 -        (extend (fetch_pred_data thy) (depending_preds_of ctxt) const)) lthy
   1.234 +        (extend (fetch_pred_data ctxt) (depending_preds_of ctxt) const)) lthy
   1.235      val thy' = ProofContext.theory_of lthy'
   1.236 -    val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim thy')
   1.237 +    val ctxt' = ProofContext.init_global thy'
   1.238 +    val preds = Graph.all_succs (PredData.get thy') [const] |> filter_out (has_elim ctxt')
   1.239      fun mk_cases const =
   1.240        let
   1.241          val T = Sign.the_const_type thy const
   1.242          val pred = Const (const, T)
   1.243 -        val intros = intros_of thy' const
   1.244 +        val intros = intros_of ctxt' const
   1.245        in mk_casesrule lthy' pred intros end  
   1.246      val cases_rules = map mk_cases preds
   1.247      val cases =