847 chop_fun (n - 1) ran_T |>> cons dom_T |
847 chop_fun (n - 1) ran_T |>> cons dom_T |
848 | chop_fun _ T = ([], T) |
848 | chop_fun _ T = ([], T) |
849 |
849 |
850 fun filter_type_args thy constrs type_enc s ary T_args = |
850 fun filter_type_args thy constrs type_enc s ary T_args = |
851 let val poly = polymorphism_of_type_enc type_enc in |
851 let val poly = polymorphism_of_type_enc type_enc in |
852 if s = type_tag_name then (* ### FIXME: why not "type_guard_name" as well? *) |
852 if s = type_tag_name then (* FIXME: why not "type_guard_name" as well? *) |
853 T_args |
853 T_args |
854 else case type_enc of |
854 else case type_enc of |
855 Native (_, Raw_Polymorphic _, _) => T_args |
855 Native (_, Raw_Polymorphic _, _) => T_args |
856 | Native (_, Type_Class_Polymorphic, _) => T_args |
856 | Native (_, Type_Class_Polymorphic, _) => T_args |
857 | _ => |
857 | _ => |
1578 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts = |
1578 fun sym_table_for_facts ctxt type_enc app_op_level conjs facts = |
1579 let |
1579 let |
1580 fun add_iterm_syms conj_fact = |
1580 fun add_iterm_syms conj_fact = |
1581 add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true |
1581 add_iterm_syms_to_sym_table ctxt app_op_level conj_fact true |
1582 fun add_fact_syms conj_fact = |
1582 fun add_fact_syms conj_fact = |
1583 K (add_iterm_syms conj_fact) |> formula_fold NONE |> ifact_lift |
1583 ifact_lift (formula_fold NONE (K (add_iterm_syms conj_fact))) |
1584 in |
1584 in |
1585 ((false, []), Symtab.empty) |
1585 ((false, []), Symtab.empty) |
1586 |> fold (add_fact_syms true) conjs |
1586 |> fold (add_fact_syms true) conjs |
1587 |> fold (add_fact_syms false) facts |
1587 |> fold (add_fact_syms false) facts |
1588 ||> fold Symtab.update (default_sym_tab_entries type_enc) |
1588 ||> fold Symtab.update (default_sym_tab_entries type_enc) |
2241 end |
2241 end |
2242 | IAbs (_, tm) => add_iterm_syms tm |
2242 | IAbs (_, tm) => add_iterm_syms tm |
2243 | _ => I) |
2243 | _ => I) |
2244 #> fold add_iterm_syms args |
2244 #> fold add_iterm_syms args |
2245 end |
2245 end |
2246 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift |
2246 val add_fact_syms = ifact_lift (formula_fold NONE (K add_iterm_syms)) |
2247 fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi |
2247 fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi |
2248 | add_formula_var_types (AQuant (_, xs, phi)) = |
2248 | add_formula_var_types (AQuant (_, xs, phi)) = |
2249 fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs |
2249 fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs |
2250 #> add_formula_var_types phi |
2250 #> add_formula_var_types phi |
2251 | add_formula_var_types (AConn (_, phis)) = |
2251 | add_formula_var_types (AConn (_, phis)) = |
2289 case level of |
2289 case level of |
2290 Nonmono_Types (Strict, _) => [] |
2290 Nonmono_Types (Strict, _) => [] |
2291 | _ => known_infinite_types, |
2291 | _ => known_infinite_types, |
2292 maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]} |
2292 maybe_nonmono_Ts = [if completish then tvar_a else @{typ bool}]} |
2293 |
2293 |
2294 (* This inference is described in section 2.3 of Claessen et al.'s "Sorting it |
2294 (* This inference is described in section 4 of Blanchette et al., "Encoding |
2295 out with monotonicity" paper presented at CADE 2011. *) |
2295 monomorphic and polymorphic types", TACAS 2013. *) |
2296 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono |
2296 fun add_iterm_mononotonicity_info _ _ (SOME false) _ mono = mono |
2297 | add_iterm_mononotonicity_info ctxt level _ |
2297 | add_iterm_mononotonicity_info ctxt level _ |
2298 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) |
2298 (IApp (IApp (IConst ((s, _), Type (_, [T, _]), _), tm1), tm2)) |
2299 (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) = |
2299 (mono as {maybe_finite_Ts, surely_infinite_Ts, maybe_nonmono_Ts}) = |
2300 let val thy = Proof_Context.theory_of ctxt in |
2300 let val thy = Proof_Context.theory_of ctxt in |
2336 fun add_type T = not (should_encode T) ? insert_type thy I T |
2336 fun add_type T = not (should_encode T) ? insert_type thy I T |
2337 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2 |
2337 fun add_args (IApp (tm1, tm2)) = add_args tm1 #> add_term tm2 |
2338 | add_args _ = I |
2338 | add_args _ = I |
2339 and add_term tm = add_type (ityp_of tm) #> add_args tm |
2339 and add_term tm = add_type (ityp_of tm) #> add_args tm |
2340 in formula_fold NONE (K add_term) end |
2340 in formula_fold NONE (K add_term) end |
|
2341 |
2341 fun add_fact_monotonic_types ctxt mono type_enc = |
2342 fun add_fact_monotonic_types ctxt mono type_enc = |
2342 add_iformula_monotonic_types ctxt mono type_enc |> ifact_lift |
2343 ifact_lift (add_iformula_monotonic_types ctxt mono type_enc) |
|
2344 |
2343 fun monotonic_types_for_facts ctxt mono type_enc facts = |
2345 fun monotonic_types_for_facts ctxt mono type_enc facts = |
2344 let val level = level_of_type_enc type_enc in |
2346 let val level = level_of_type_enc type_enc in |
2345 [] |> (is_type_enc_polymorphic type_enc andalso |
2347 [] |> (is_type_enc_polymorphic type_enc andalso |
2346 is_type_level_monotonicity_based level) |
2348 is_type_level_monotonicity_based level) |
2347 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts |
2349 ? fold (add_fact_monotonic_types ctxt mono type_enc) facts |
2394 |> native_ho_type_from_typ type_enc pred_sym ary |
2396 |> native_ho_type_from_typ type_enc pred_sym ary |
2395 |> not (null T_args) |
2397 |> not (null T_args) |
2396 ? curry APi (map (tvar_name o dest_TVar) T_args)) |
2398 ? curry APi (map (tvar_name o dest_TVar) T_args)) |
2397 end |
2399 end |
2398 |
2400 |
2399 fun honor_conj_sym_role in_conj = |
2401 fun honor_conj_sym_role in_conj = (if in_conj then Hypothesis else Axiom, I) |
2400 if in_conj then (Hypothesis, I) else (Axiom, I) |
|
2401 |
2402 |
2402 fun line_for_guards_sym_decl ctxt mono type_enc n s j |
2403 fun line_for_guards_sym_decl ctxt mono type_enc n s j |
2403 (s', T_args, T, _, ary, in_conj) = |
2404 (s', T_args, T, _, ary, in_conj) = |
2404 let |
2405 let |
2405 val thy = Proof_Context.theory_of ctxt |
2406 val thy = Proof_Context.theory_of ctxt |