--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 13:29:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 16:50:09 2010 +0100
@@ -2,16 +2,15 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2009, 2010
-Monotonicity predicate for higher-order logic.
+Monotonicity inference for higher-order logic.
*)
signature NITPICK_MONO =
sig
- datatype sign = Plus | Minus
type hol_context = Nitpick_HOL.hol_context
val formulas_monotonic :
- hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
+ hol_context -> bool -> typ -> term list * term list -> bool
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -27,22 +26,27 @@
type literal = var * sign
-datatype ctype =
- CAlpha |
- CFun of ctype * sign_atom * ctype |
- CPair of ctype * ctype |
- CType of string * ctype list |
- CRec of string * typ list
+datatype mtyp =
+ MAlpha |
+ MFun of mtyp * sign_atom * mtyp |
+ MPair of mtyp * mtyp |
+ MType of string * mtyp list |
+ MRec of string * typ list
-type cdata =
+datatype mterm =
+ MRaw of term * mtyp |
+ MAbs of string * typ * mtyp * sign_atom * mterm |
+ MApp of mterm * mterm
+
+type mdata =
{hol_ctxt: hol_context,
binarize: bool,
alpha_T: typ,
max_fresh: int Unsynchronized.ref,
- datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
- constr_cache: (styp * ctype) list Unsynchronized.ref}
+ datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
+ constr_cache: (styp * mtyp) list Unsynchronized.ref}
-exception CTYPE of string * ctype list
+exception MTYPE of string * mtyp list
(* string -> unit *)
fun print_g (_ : string) = ()
@@ -71,55 +75,95 @@
(* literal -> string *)
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
-val bool_C = CType (@{type_name bool}, [])
+val bool_M = MType (@{type_name bool}, [])
+val dummy_M = MType (nitpick_prefix ^ "dummy", [])
-(* ctype -> bool *)
-fun is_CRec (CRec _) = true
- | is_CRec _ = false
+(* mtyp -> bool *)
+fun is_MRec (MRec _) = true
+ | is_MRec _ = false
+(* mtyp -> mtyp * sign_atom * mtyp *)
+fun dest_MFun (MFun z) = z
+ | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
val no_prec = 100
-val prec_CFun = 1
-val prec_CPair = 2
-(* tuple_set -> int *)
-fun precedence_of_ctype (CFun _) = prec_CFun
- | precedence_of_ctype (CPair _) = prec_CPair
- | precedence_of_ctype _ = no_prec
+(* mtyp -> int *)
+fun precedence_of_mtype (MFun _) = 1
+ | precedence_of_mtype (MPair _) = 2
+ | precedence_of_mtype _ = no_prec
-(* ctype -> string *)
-val string_for_ctype =
+(* mtyp -> string *)
+val string_for_mtype =
let
- (* int -> ctype -> string *)
- fun aux outer_prec C =
+ (* int -> mtyp -> string *)
+ fun aux outer_prec M =
let
- val prec = precedence_of_ctype C
+ val prec = precedence_of_mtype M
val need_parens = (prec < outer_prec)
in
(if need_parens then "(" else "") ^
- (case C of
- CAlpha => "\<alpha>"
- | CFun (C1, a, C2) =>
- aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^
- string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
- | CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
- | CType (s, []) =>
- if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
- | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
- | CRec (s, _) => "[" ^ s ^ "]") ^
+ (if M = dummy_M then
+ "_"
+ else case M of
+ MAlpha => "\<alpha>"
+ | MFun (M1, a, M2) =>
+ aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
+ string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
+ | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
+ | MType (s, []) =>
+ if s = @{type_name prop} orelse s = @{type_name bool} then "o"
+ else s
+ | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
+ | MRec (s, _) => "[" ^ s ^ "]") ^
(if need_parens then ")" else "")
end
in aux 0 end
-(* ctype -> ctype list *)
-fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2]
- | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
- | flatten_ctype C = [C]
+(* mtyp -> mtyp list *)
+fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
+ | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
+ | flatten_mtype M = [M]
+
+(* mterm -> bool *)
+fun precedence_of_mterm (MRaw _) = no_prec
+ | precedence_of_mterm (MAbs _) = 1
+ | precedence_of_mterm (MApp _) = 2
-(* hol_context -> bool -> typ -> cdata *)
-fun initial_cdata hol_ctxt binarize alpha_T =
+(* Proof.context -> mterm -> string *)
+fun string_for_mterm ctxt =
+ let
+ (* mtype -> string *)
+ fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
+ (* int -> mterm -> string *)
+ fun aux outer_prec m =
+ let
+ val prec = precedence_of_mterm m
+ val need_parens = (prec < outer_prec)
+ in
+ (if need_parens then "(" else "") ^
+ (case m of
+ MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
+ | MAbs (s, _, M, a, m) =>
+ "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
+ string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
+ | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
+ (if need_parens then ")" else "")
+ end
+ in aux 0 end
+
+(* mterm -> mtyp *)
+fun mtype_of_mterm (MRaw (_, M)) = M
+ | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
+ | mtype_of_mterm (MApp (m1, _)) =
+ case mtype_of_mterm m1 of
+ MFun (_, _, M12) => M12
+ | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
+
+(* hol_context -> bool -> typ -> mdata *)
+fun initial_mdata hol_ctxt binarize alpha_T =
({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
- constr_cache = Unsynchronized.ref []} : cdata)
+ constr_cache = Unsynchronized.ref []} : mdata)
(* typ -> typ -> bool *)
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
@@ -127,172 +171,179 @@
exists (could_exist_alpha_subtype alpha_T) Ts)
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
(* theory -> typ -> typ -> bool *)
-fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
+fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
could_exist_alpha_subtype alpha_T T
- | could_exist_alpha_sub_ctype thy alpha_T T =
+ | could_exist_alpha_sub_mtype thy alpha_T T =
(T = alpha_T orelse is_datatype thy [(NONE, true)] T)
-(* ctype -> bool *)
-fun exists_alpha_sub_ctype CAlpha = true
- | exists_alpha_sub_ctype (CFun (C1, _, C2)) =
- exists exists_alpha_sub_ctype [C1, C2]
- | exists_alpha_sub_ctype (CPair (C1, C2)) =
- exists exists_alpha_sub_ctype [C1, C2]
- | exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs
- | exists_alpha_sub_ctype (CRec _) = true
+(* mtyp -> bool *)
+fun exists_alpha_sub_mtype MAlpha = true
+ | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
+ exists exists_alpha_sub_mtype [M1, M2]
+ | exists_alpha_sub_mtype (MPair (M1, M2)) =
+ exists exists_alpha_sub_mtype [M1, M2]
+ | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
+ | exists_alpha_sub_mtype (MRec _) = true
-(* ctype -> bool *)
-fun exists_alpha_sub_ctype_fresh CAlpha = true
- | exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true
- | exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) =
- exists_alpha_sub_ctype_fresh C2
- | exists_alpha_sub_ctype_fresh (CPair (C1, C2)) =
- exists exists_alpha_sub_ctype_fresh [C1, C2]
- | exists_alpha_sub_ctype_fresh (CType (_, Cs)) =
- exists exists_alpha_sub_ctype_fresh Cs
- | exists_alpha_sub_ctype_fresh (CRec _) = true
+(* mtyp -> bool *)
+fun exists_alpha_sub_mtype_fresh MAlpha = true
+ | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
+ | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
+ exists_alpha_sub_mtype_fresh M2
+ | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
+ exists exists_alpha_sub_mtype_fresh [M1, M2]
+ | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
+ exists exists_alpha_sub_mtype_fresh Ms
+ | exists_alpha_sub_mtype_fresh (MRec _) = true
-(* string * typ list -> ctype list -> ctype *)
-fun constr_ctype_for_binders z Cs =
- fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
+(* string * typ list -> mtyp list -> mtyp *)
+fun constr_mtype_for_binders z Ms =
+ fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
-(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
-fun repair_ctype _ _ CAlpha = CAlpha
- | repair_ctype cache seen (CFun (C1, a, C2)) =
- CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2)
- | repair_ctype cache seen (CPair Cp) =
- CPair (pairself (repair_ctype cache seen) Cp)
- | repair_ctype cache seen (CType (s, Cs)) =
- CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs)
- | repair_ctype cache seen (CRec (z as (s, _))) =
+(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *)
+fun repair_mtype _ _ MAlpha = MAlpha
+ | repair_mtype cache seen (MFun (M1, a, M2)) =
+ MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
+ | repair_mtype cache seen (MPair Mp) =
+ MPair (pairself (repair_mtype cache seen) Mp)
+ | repair_mtype cache seen (MType (s, Ms)) =
+ MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
+ | repair_mtype cache seen (MRec (z as (s, _))) =
case AList.lookup (op =) cache z |> the of
- CRec _ => CType (s, [])
- | C => if member (op =) seen C then CType (s, [])
- else repair_ctype cache (C :: seen) C
+ MRec _ => MType (s, [])
+ | M => if member (op =) seen M then MType (s, [])
+ else repair_mtype cache (M :: seen) M
-(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
+(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
fun repair_datatype_cache cache =
let
- (* (string * typ list) * ctype -> unit *)
- fun repair_one (z, C) =
+ (* (string * typ list) * mtyp -> unit *)
+ fun repair_one (z, M) =
Unsynchronized.change cache
- (AList.update (op =) (z, repair_ctype (!cache) [] C))
+ (AList.update (op =) (z, repair_mtype (!cache) [] M))
in List.app repair_one (rev (!cache)) end
-(* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *)
+(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
fun repair_constr_cache dtype_cache constr_cache =
let
- (* styp * ctype -> unit *)
- fun repair_one (x, C) =
+ (* styp * mtyp -> unit *)
+ fun repair_one (x, M) =
Unsynchronized.change constr_cache
- (AList.update (op =) (x, repair_ctype dtype_cache [] C))
+ (AList.update (op =) (x, repair_mtype dtype_cache [] M))
in List.app repair_one (!constr_cache) end
-(* cdata -> typ -> ctype *)
-fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh,
- datatype_cache, constr_cache, ...} : cdata) =
+(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
+fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
let
- (* typ -> typ -> ctype *)
- fun do_fun T1 T2 =
- let
- val C1 = do_type T1
- val C2 = do_type T2
- val a = if is_boolean_type (body_type T2) andalso
- exists_alpha_sub_ctype_fresh C1 then
- V (Unsynchronized.inc max_fresh)
- else
- S Minus
- in CFun (C1, a, C2) end
- (* typ -> ctype *)
- and do_type T =
+ val M1 = fresh_mtype_for_type mdata T1
+ val M2 = fresh_mtype_for_type mdata T2
+ val a = if is_boolean_type (body_type T2) andalso
+ exists_alpha_sub_mtype_fresh M1 then
+ V (Unsynchronized.inc max_fresh)
+ else
+ S Minus
+ in (M1, a, M2) end
+(* mdata -> typ -> mtyp *)
+and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
+ datatype_cache, constr_cache, ...}) =
+ let
+ (* typ -> typ -> mtyp *)
+ val do_fun = MFun oo fresh_mfun_for_fun_type mdata
+ (* typ -> mtyp *)
+ fun do_type T =
if T = alpha_T then
- CAlpha
+ MAlpha
else case T of
Type ("fun", [T1, T2]) => do_fun T1 T2
| Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
- | Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2))
+ | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
| Type (z as (s, _)) =>
- if could_exist_alpha_sub_ctype thy alpha_T T then
+ if could_exist_alpha_sub_mtype thy alpha_T T then
case AList.lookup (op =) (!datatype_cache) z of
- SOME C => C
+ SOME M => M
| NONE =>
let
- val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
+ val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
- val (all_Cs, constr_Cs) =
- fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
+ val (all_Ms, constr_Ms) =
+ fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
let
- val binder_Cs = map do_type (binder_types T')
- val new_Cs = filter exists_alpha_sub_ctype_fresh
- binder_Cs
- val constr_C = constr_ctype_for_binders z
- binder_Cs
+ val binder_Ms = map do_type (binder_types T')
+ val new_Ms = filter exists_alpha_sub_mtype_fresh
+ binder_Ms
+ val constr_M = constr_mtype_for_binders z
+ binder_Ms
in
- (union (op =) new_Cs all_Cs,
- constr_C :: constr_Cs)
+ (union (op =) new_Ms all_Ms,
+ constr_M :: constr_Ms)
end)
xs ([], [])
- val C = CType (s, all_Cs)
+ val M = MType (s, all_Ms)
val _ = Unsynchronized.change datatype_cache
- (AList.update (op =) (z, C))
+ (AList.update (op =) (z, M))
val _ = Unsynchronized.change constr_cache
- (append (xs ~~ constr_Cs))
+ (append (xs ~~ constr_Ms))
in
- if forall (not o is_CRec o snd) (!datatype_cache) then
+ if forall (not o is_MRec o snd) (!datatype_cache) then
(repair_datatype_cache datatype_cache;
repair_constr_cache (!datatype_cache) constr_cache;
AList.lookup (op =) (!datatype_cache) z |> the)
else
- C
+ M
end
else
- CType (s, [])
- | _ => CType (Refute.string_of_typ T, [])
+ MType (s, [])
+ | _ => MType (Refute.string_of_typ T, [])
in do_type end
-(* ctype -> ctype list *)
-fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
- | prodC_factors C = [C]
-(* ctype -> ctype list * ctype *)
-fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
- curried_strip_ctype C2 |>> append (prodC_factors C1)
- | curried_strip_ctype C = ([], C)
-(* string -> ctype -> ctype *)
-fun sel_ctype_from_constr_ctype s C =
- let val (arg_Cs, dataC) = curried_strip_ctype C in
- CFun (dataC, S Minus,
- case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
+(* mtyp -> mtyp list *)
+fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
+ | prodM_factors M = [M]
+(* mtyp -> mtyp list * mtyp *)
+fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
+ curried_strip_mtype M2 |>> append (prodM_factors M1)
+ | curried_strip_mtype M = ([], M)
+(* string -> mtyp -> mtyp *)
+fun sel_mtype_from_constr_mtype s M =
+ let val (arg_Ms, dataM) = curried_strip_mtype M in
+ MFun (dataM, S Minus,
+ case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
end
-(* cdata -> styp -> ctype *)
-fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
+(* mdata -> styp -> mtyp *)
+fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
...}) (x as (_, T)) =
- if could_exist_alpha_sub_ctype thy alpha_T T then
+ if could_exist_alpha_sub_mtype thy alpha_T T then
case AList.lookup (op =) (!constr_cache) x of
- SOME C => C
- | NONE => (fresh_ctype_for_type cdata (body_type T);
- AList.lookup (op =) (!constr_cache) x |> the)
+ SOME M => M
+ | NONE => if T = alpha_T then
+ let val M = fresh_mtype_for_type mdata T in
+ (Unsynchronized.change constr_cache (cons (x, M)); M)
+ end
+ else
+ (fresh_mtype_for_type mdata (body_type T);
+ AList.lookup (op =) (!constr_cache) x |> the)
else
- fresh_ctype_for_type cdata T
-fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
+ fresh_mtype_for_type mdata T
+fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
- |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
+ |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
-(* literal list -> ctype -> ctype *)
-fun instantiate_ctype lits =
+(* literal list -> mtyp -> mtyp *)
+fun instantiate_mtype lits =
let
- (* ctype -> ctype *)
- fun aux CAlpha = CAlpha
- | aux (CFun (C1, V x, C2)) =
+ (* mtyp -> mtyp *)
+ fun aux MAlpha = MAlpha
+ | aux (MFun (M1, V x, M2)) =
let
val a = case AList.lookup (op =) lits x of
SOME sn => S sn
| NONE => V x
- in CFun (aux C1, a, aux C2) end
- | aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2)
- | aux (CPair Cp) = CPair (pairself aux Cp)
- | aux (CType (s, Cs)) = CType (s, map aux Cs)
- | aux (CRec z) = CRec z
+ in MFun (aux M1, a, aux M2) end
+ | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
+ | aux (MPair Mp) = MPair (pairself aux Mp)
+ | aux (MType (s, Ms)) = MType (s, map aux Ms)
+ | aux (MRec z) = MRec z
in aux end
datatype comp_op = Eq | Leq
@@ -342,105 +393,106 @@
| do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
-(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
+(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option
-> (literal list * comp list) option *)
-fun do_ctype_comp _ _ _ _ NONE = NONE
- | do_ctype_comp _ _ CAlpha CAlpha accum = accum
- | do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
+fun do_mtype_comp _ _ _ _ NONE = NONE
+ | do_mtype_comp _ _ MAlpha MAlpha accum = accum
+ | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
(SOME accum) =
- accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21
- |> do_ctype_comp Eq xs C12 C22
- | do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
+ accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
+ |> do_mtype_comp Eq xs M12 M22
+ | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
(SOME accum) =
- (if exists_alpha_sub_ctype C11 then
+ (if exists_alpha_sub_mtype M11 then
accum |> do_sign_atom_comp Leq xs a1 a2
- |> do_ctype_comp Leq xs C21 C11
+ |> do_mtype_comp Leq xs M21 M11
|> (case a2 of
S Minus => I
- | S Plus => do_ctype_comp Leq xs C11 C21
- | V x => do_ctype_comp Leq (x :: xs) C11 C21)
+ | S Plus => do_mtype_comp Leq xs M11 M21
+ | V x => do_mtype_comp Leq (x :: xs) M11 M21)
else
SOME accum)
- |> do_ctype_comp Leq xs C12 C22
- | do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22))
+ |> do_mtype_comp Leq xs M12 M22
+ | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
accum =
- (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
+ (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
handle Library.UnequalLengths =>
- raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
- | do_ctype_comp _ _ (CType _) (CType _) accum =
+ raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
+ | do_mtype_comp _ _ (MType _) (MType _) accum =
accum (* no need to compare them thanks to the cache *)
- | do_ctype_comp _ _ C1 C2 _ =
- raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
+ | do_mtype_comp _ _ M1 M2 _ =
+ raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
-(* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
-fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
- | add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) =
- (print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^
- " " ^ string_for_ctype C2);
- case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of
+(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
+fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
+ | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) =
+ (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
+ " " ^ string_for_mtype M2);
+ case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
| SOME (lits, comps) => CSet (lits, comps, sexps))
-(* ctype -> ctype -> constraint_set -> constraint_set *)
-val add_ctypes_equal = add_ctype_comp Eq
-val add_is_sub_ctype = add_ctype_comp Leq
+(* mtyp -> mtyp -> constraint_set -> constraint_set *)
+val add_mtypes_equal = add_mtype_comp Eq
+val add_is_sub_mtype = add_mtype_comp Leq
-(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
+(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option
-> (literal list * sign_expr list) option *)
-fun do_notin_ctype_fv _ _ _ NONE = NONE
- | do_notin_ctype_fv Minus _ CAlpha accum = accum
- | do_notin_ctype_fv Plus [] CAlpha _ = NONE
- | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
+fun do_notin_mtype_fv _ _ _ NONE = NONE
+ | do_notin_mtype_fv Minus _ MAlpha accum = accum
+ | do_notin_mtype_fv Plus [] MAlpha _ = NONE
+ | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
- | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
+ | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
SOME (lits, insert (op =) sexp sexps)
- | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
+ | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
accum |> (if sn' = Plus andalso sn = Plus then
- do_notin_ctype_fv Plus sexp C1
+ do_notin_mtype_fv Plus sexp M1
else
I)
|> (if sn' = Minus orelse sn = Plus then
- do_notin_ctype_fv Minus sexp C1
+ do_notin_mtype_fv Minus sexp M1
else
I)
- |> do_notin_ctype_fv sn sexp C2
- | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
+ |> do_notin_mtype_fv sn sexp M2
+ | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
accum |> (case do_literal (x, Minus) (SOME sexp) of
NONE => I
- | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
- |> do_notin_ctype_fv Minus sexp C1
- |> do_notin_ctype_fv Plus sexp C2
- | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
+ | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
+ |> do_notin_mtype_fv Minus sexp M1
+ |> do_notin_mtype_fv Plus sexp M2
+ | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
accum |> (case do_literal (x, Plus) (SOME sexp) of
NONE => I
- | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
- |> do_notin_ctype_fv Minus sexp C2
- | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
- accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
- | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
- accum |> fold (do_notin_ctype_fv sn sexp) Cs
- | do_notin_ctype_fv _ _ C _ =
- raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
+ | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
+ |> do_notin_mtype_fv Minus sexp M2
+ | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum =
+ accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2]
+ | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
+ accum |> fold (do_notin_mtype_fv sn sexp) Ms
+ | do_notin_mtype_fv _ _ M _ =
+ raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
-(* sign -> ctype -> constraint_set -> constraint_set *)
-fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
- | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
- (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
+(* sign -> mtyp -> constraint_set -> constraint_set *)
+fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
+ | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
+ (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
(case sn of Minus => "unique" | Plus => "total") ^ ".");
- case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
+ case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
| SOME (lits, sexps) => CSet (lits, comps, sexps))
-(* ctype -> constraint_set -> constraint_set *)
-val add_ctype_is_right_unique = add_notin_ctype_fv Minus
-val add_ctype_is_right_total = add_notin_ctype_fv Plus
+(* mtyp -> constraint_set -> constraint_set *)
+val add_mtype_is_right_unique = add_notin_mtype_fv Minus
+val add_mtype_is_right_total = add_notin_mtype_fv Plus
+
+val bool_from_minus = true
(* sign -> bool *)
-fun bool_from_sign Plus = false
- | bool_from_sign Minus = true
+fun bool_from_sign Plus = not bool_from_minus
+ | bool_from_sign Minus = bool_from_minus
(* bool -> sign *)
-fun sign_from_bool false = Plus
- | sign_from_bool true = Minus
+fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
(* literal -> PropLogic.prop_formula *)
fun prop_for_literal (x, sn) =
@@ -492,228 +544,264 @@
"-: " ^ commas (map (string_for_var o fst) neg))
end
-(* var -> constraint_set -> literal list list option *)
+(* var -> constraint_set -> literal list option *)
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
| solve max_var (CSet (lits, comps, sexps)) =
let
+ (* (int -> bool option) -> literal list option *)
+ fun do_assigns assigns =
+ SOME (literals_from_assignments max_var assigns lits
+ |> tap print_solution)
val _ = print_problem lits comps sexps
val prop = PropLogic.all (map prop_for_literal lits @
map prop_for_comp comps @
map prop_for_sign_expr sexps)
- (* use the first ML solver (to avoid startup overhead) *)
- val solvers = !SatSolver.solvers
- |> filter (member (op =) ["dptsat", "dpll"] o fst)
+ val default_val = bool_from_sign Minus
in
- case snd (hd solvers) prop of
- SatSolver.SATISFIABLE assigns =>
- SOME (literals_from_assignments max_var assigns lits
- |> tap print_solution)
- | _ => NONE
+ if PropLogic.eval (K default_val) prop then
+ do_assigns (K (SOME default_val))
+ else
+ let
+ (* use the first ML solver (to avoid startup overhead) *)
+ val solvers = !SatSolver.solvers
+ |> filter (member (op =) ["dptsat", "dpll"] o fst)
+ in
+ case snd (hd solvers) prop of
+ SatSolver.SATISFIABLE assigns => do_assigns assigns
+ | _ => NONE
+ end
end
-type ctype_schema = ctype * constraint_set
-type ctype_context =
- {bounds: ctype list,
- frees: (styp * ctype) list,
- consts: (styp * ctype) list}
+type mtype_schema = mtyp * constraint_set
+type mtype_context =
+ {bounds: mtyp list,
+ frees: (styp * mtyp) list,
+ consts: (styp * mtyp) list}
-type accumulator = ctype_context * constraint_set
+type accumulator = mtype_context * constraint_set
val initial_gamma = {bounds = [], frees = [], consts = []}
val unsolvable_accum = (initial_gamma, UnsolvableCSet)
-(* ctype -> ctype_context -> ctype_context *)
-fun push_bound C {bounds, frees, consts} =
- {bounds = C :: bounds, frees = frees, consts = consts}
-(* ctype_context -> ctype_context *)
+(* mtyp -> mtype_context -> mtype_context *)
+fun push_bound M {bounds, frees, consts} =
+ {bounds = M :: bounds, frees = frees, consts = consts}
+(* mtype_context -> mtype_context *)
fun pop_bound {bounds, frees, consts} =
{bounds = tl bounds, frees = frees, consts = consts}
handle List.Empty => initial_gamma
-(* cdata -> term -> accumulator -> ctype * accumulator *)
-fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
+(* mdata -> term -> accumulator -> mterm * accumulator *)
+fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
def_table, ...},
alpha_T, max_fresh, ...}) =
let
- (* typ -> ctype *)
- val ctype_for = fresh_ctype_for_type cdata
- (* ctype -> ctype *)
- fun pos_set_ctype_for_dom C =
- CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
- (* typ -> accumulator -> ctype * accumulator *)
- fun do_quantifier T (gamma, cset) =
+ (* typ -> typ -> mtyp * sign_atom * mtyp *)
+ val mfun_for = fresh_mfun_for_fun_type mdata
+ (* typ -> mtyp *)
+ val mtype_for = fresh_mtype_for_type mdata
+ (* mtyp -> mtyp *)
+ fun pos_set_mtype_for_dom M =
+ MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
+ (* typ -> accumulator -> mterm * accumulator *)
+ fun do_all T (gamma, cset) =
let
- val abs_C = ctype_for (domain_type (domain_type T))
- val body_C = ctype_for (range_type T)
+ val abs_M = mtype_for (domain_type (domain_type T))
+ val body_M = mtype_for (body_type T)
in
- (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
- (gamma, cset |> add_ctype_is_right_total abs_C))
+ (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
+ (gamma, cset |> add_mtype_is_right_total abs_M))
end
fun do_equals T (gamma, cset) =
- let val C = ctype_for (domain_type T) in
- (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
- ctype_for (nth_range_type 2 T))),
- (gamma, cset |> add_ctype_is_right_unique C))
+ let val M = mtype_for (domain_type T) in
+ (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
+ mtype_for (nth_range_type 2 T))),
+ (gamma, cset |> add_mtype_is_right_unique M))
end
fun do_robust_set_operation T (gamma, cset) =
let
val set_T = domain_type T
- val C1 = ctype_for set_T
- val C2 = ctype_for set_T
- val C3 = ctype_for set_T
+ val M1 = mtype_for set_T
+ val M2 = mtype_for set_T
+ val M3 = mtype_for set_T
in
- (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
- (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
+ (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
+ (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
end
fun do_fragile_set_operation T (gamma, cset) =
let
val set_T = domain_type T
- val set_C = ctype_for set_T
- (* typ -> ctype *)
- fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
- if T = set_T then set_C
- else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
- | custom_ctype_for T = ctype_for T
+ val set_M = mtype_for set_T
+ (* typ -> mtyp *)
+ fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
+ if T = set_T then set_M
+ else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
+ | custom_mtype_for T = mtype_for T
in
- (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
+ (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
end
- (* typ -> accumulator -> ctype * accumulator *)
+ (* typ -> accumulator -> mtyp * accumulator *)
fun do_pair_constr T accum =
- case ctype_for (nth_range_type 2 T) of
- C as CPair (a_C, b_C) =>
- (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
- | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
- (* int -> typ -> accumulator -> ctype * accumulator *)
+ case mtype_for (nth_range_type 2 T) of
+ M as MPair (a_M, b_M) =>
+ (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
+ | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
+ (* int -> typ -> accumulator -> mtyp * accumulator *)
fun do_nth_pair_sel n T =
- case ctype_for (domain_type T) of
- C as CPair (a_C, b_C) =>
- pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
- | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
- val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
- (* typ -> term -> accumulator -> ctype * accumulator *)
- fun do_bounded_quantifier abs_T bound_t body_t accum =
+ case mtype_for (domain_type T) of
+ M as MPair (a_M, b_M) =>
+ pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
+ | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
+ (* mtyp * accumulator *)
+ val mtype_unsolvable = (dummy_M, unsolvable_accum)
+ (* term -> mterm * accumulator *)
+ fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum)
+ (* term -> string -> typ -> term -> term -> term -> accumulator
+ -> mterm * accumulator *)
+ fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
let
- val abs_C = ctype_for abs_T
- val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t
- val expected_bound_C = pos_set_ctype_for_dom abs_C
+ val abs_M = mtype_for abs_T
+ val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
+ val expected_bound_M = pos_set_mtype_for_dom abs_M
+ val (body_m, accum) =
+ accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
+ |> do_term body_t ||> apfst pop_bound
+ val bound_M = mtype_of_mterm bound_m
+ val (M1, a, M2) = dest_MFun bound_M
in
- accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t
- ||> apfst pop_bound
+ (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
+ MAbs (abs_s, abs_T, M1, a,
+ MApp (MApp (MRaw (connective_t,
+ mtype_for (fastype_of connective_t)),
+ MApp (bound_m, MRaw (Bound 0, M1))),
+ body_m))), accum)
end
- (* term -> accumulator -> ctype * accumulator *)
- and do_term _ (_, UnsolvableCSet) = unsolvable
+ (* term -> accumulator -> mterm * accumulator *)
+ and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
| do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
(case t of
Const (x as (s, T)) =>
(case AList.lookup (op =) consts x of
- SOME C => (C, accum)
+ SOME M => (M, accum)
| NONE =>
if not (could_exist_alpha_subtype alpha_T T) then
- (ctype_for T, accum)
+ (mtype_for T, accum)
else case s of
- @{const_name all} => do_quantifier T accum
+ @{const_name all} => do_all T accum
| @{const_name "=="} => do_equals T accum
- | @{const_name All} => do_quantifier T accum
- | @{const_name Ex} => do_quantifier T accum
+ | @{const_name All} => do_all T accum
+ | @{const_name Ex} =>
+ let val set_T = domain_type T in
+ do_term (Abs (Name.uu, set_T,
+ @{const Not} $ (HOLogic.mk_eq
+ (Abs (Name.uu, domain_type set_T,
+ @{const False}),
+ Bound 0)))) accum
+ |>> mtype_of_mterm
+ end
| @{const_name "op ="} => do_equals T accum
- | @{const_name The} => (print_g "*** The"; unsolvable)
- | @{const_name Eps} => (print_g "*** Eps"; unsolvable)
+ | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
+ | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
| @{const_name If} =>
do_robust_set_operation (range_type T) accum
- |>> curry3 CFun bool_C (S Minus)
+ |>> curry3 MFun bool_M (S Minus)
| @{const_name Pair} => do_pair_constr T accum
| @{const_name fst} => do_nth_pair_sel 0 T accum
| @{const_name snd} => do_nth_pair_sel 1 T accum
| @{const_name Id} =>
- (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
+ (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
| @{const_name insert} =>
let
val set_T = domain_type (range_type T)
- val C1 = ctype_for (domain_type set_T)
- val C1' = pos_set_ctype_for_dom C1
- val C2 = ctype_for set_T
- val C3 = ctype_for set_T
+ val M1 = mtype_for (domain_type set_T)
+ val M1' = pos_set_mtype_for_dom M1
+ val M2 = mtype_for set_T
+ val M3 = mtype_for set_T
in
- (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
- (gamma, cset |> add_ctype_is_right_unique C1
- |> add_is_sub_ctype C1' C3
- |> add_is_sub_ctype C2 C3))
+ (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
+ (gamma, cset |> add_mtype_is_right_unique M1
+ |> add_is_sub_mtype M1' M3
+ |> add_is_sub_mtype M2 M3))
end
| @{const_name converse} =>
let
val x = Unsynchronized.inc max_fresh
- (* typ -> ctype *)
- fun ctype_for_set T =
- CFun (ctype_for (domain_type T), V x, bool_C)
- val ab_set_C = domain_type T |> ctype_for_set
- val ba_set_C = range_type T |> ctype_for_set
- in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
+ (* typ -> mtyp *)
+ fun mtype_for_set T =
+ MFun (mtype_for (domain_type T), V x, bool_M)
+ val ab_set_M = domain_type T |> mtype_for_set
+ val ba_set_M = range_type T |> mtype_for_set
+ in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
| @{const_name trancl} => do_fragile_set_operation T accum
- | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
+ | @{const_name rtrancl} =>
+ (print_g "*** rtrancl"; mtype_unsolvable)
| @{const_name finite} =>
- let val C1 = ctype_for (domain_type (domain_type T)) in
- (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
- end
+ if is_finite_type hol_ctxt T then
+ let val M1 = mtype_for (domain_type (domain_type T)) in
+ (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
+ end
+ else
+ (print_g "*** finite"; mtype_unsolvable)
| @{const_name rel_comp} =>
let
val x = Unsynchronized.inc max_fresh
- (* typ -> ctype *)
- fun ctype_for_set T =
- CFun (ctype_for (domain_type T), V x, bool_C)
- val bc_set_C = domain_type T |> ctype_for_set
- val ab_set_C = domain_type (range_type T) |> ctype_for_set
- val ac_set_C = nth_range_type 2 T |> ctype_for_set
+ (* typ -> mtyp *)
+ fun mtype_for_set T =
+ MFun (mtype_for (domain_type T), V x, bool_M)
+ val bc_set_M = domain_type T |> mtype_for_set
+ val ab_set_M = domain_type (range_type T) |> mtype_for_set
+ val ac_set_M = nth_range_type 2 T |> mtype_for_set
in
- (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
+ (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
accum)
end
| @{const_name image} =>
let
- val a_C = ctype_for (domain_type (domain_type T))
- val b_C = ctype_for (range_type (domain_type T))
+ val a_M = mtype_for (domain_type (domain_type T))
+ val b_M = mtype_for (range_type (domain_type T))
in
- (CFun (CFun (a_C, S Minus, b_C), S Minus,
- CFun (pos_set_ctype_for_dom a_C, S Minus,
- pos_set_ctype_for_dom b_C)), accum)
+ (MFun (MFun (a_M, S Minus, b_M), S Minus,
+ MFun (pos_set_mtype_for_dom a_M, S Minus,
+ pos_set_mtype_for_dom b_M)), accum)
end
| @{const_name Sigma} =>
let
val x = Unsynchronized.inc max_fresh
- (* typ -> ctype *)
- fun ctype_for_set T =
- CFun (ctype_for (domain_type T), V x, bool_C)
+ (* typ -> mtyp *)
+ fun mtype_for_set T =
+ MFun (mtype_for (domain_type T), V x, bool_M)
val a_set_T = domain_type T
- val a_C = ctype_for (domain_type a_set_T)
- val b_set_C = ctype_for_set (range_type (domain_type
+ val a_M = mtype_for (domain_type a_set_T)
+ val b_set_M = mtype_for_set (range_type (domain_type
(range_type T)))
- val a_set_C = ctype_for_set a_set_T
- val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
- val ab_set_C = ctype_for_set (nth_range_type 2 T)
+ val a_set_M = mtype_for_set a_set_T
+ val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
+ val ab_set_M = mtype_for_set (nth_range_type 2 T)
in
- (CFun (a_set_C, S Minus,
- CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
+ (MFun (a_set_M, S Minus,
+ MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
end
| @{const_name Tha} =>
let
- val a_C = ctype_for (domain_type (domain_type T))
- val a_set_C = pos_set_ctype_for_dom a_C
- in (CFun (a_set_C, S Minus, a_C), accum) end
+ val a_M = mtype_for (domain_type (domain_type T))
+ val a_set_M = pos_set_mtype_for_dom a_M
+ in (MFun (a_set_M, S Minus, a_M), accum) end
| @{const_name FunBox} =>
- let val dom_C = ctype_for (domain_type T) in
- (CFun (dom_C, S Minus, dom_C), accum)
+ let val dom_M = mtype_for (domain_type T) in
+ (MFun (dom_M, S Minus, dom_M), accum)
end
| _ =>
if s = @{const_name minus_class.minus} andalso
is_set_type (domain_type T) then
let
val set_T = domain_type T
- val left_set_C = ctype_for set_T
- val right_set_C = ctype_for set_T
+ val left_set_M = mtype_for set_T
+ val right_set_M = mtype_for set_T
in
- (CFun (left_set_C, S Minus,
- CFun (right_set_C, S Minus, left_set_C)),
- (gamma, cset |> add_ctype_is_right_unique right_set_C
- |> add_is_sub_ctype right_set_C left_set_C))
+ (MFun (left_set_M, S Minus,
+ MFun (right_set_M, S Minus, left_set_M)),
+ (gamma, cset |> add_mtype_is_right_unique right_set_M
+ |> add_is_sub_mtype right_set_M left_set_M))
end
else if s = @{const_name ord_class.less_eq} andalso
is_set_type (domain_type T) then
@@ -724,34 +812,37 @@
do_robust_set_operation T accum
else if is_sel s then
if constr_name_for_sel_like s = @{const_name FunBox} then
- let val dom_C = ctype_for (domain_type T) in
- (CFun (dom_C, S Minus, dom_C), accum)
+ let val dom_M = mtype_for (domain_type T) in
+ (MFun (dom_M, S Minus, dom_M), accum)
end
else
- (ctype_for_sel cdata x, accum)
+ (mtype_for_sel mdata x, accum)
else if is_constr thy stds x then
- (ctype_for_constr cdata x, accum)
+ (mtype_for_constr mdata x, accum)
else if is_built_in_const thy stds fast_descrs x then
case def_of_const thy def_table x of
- SOME t' => do_term t' accum
- | NONE => (print_g ("*** built-in " ^ s); unsolvable)
+ SOME t' => do_term t' accum |>> mtype_of_mterm
+ | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
else
- let val C = ctype_for T in
- (C, ({bounds = bounds, frees = frees,
- consts = (x, C) :: consts}, cset))
- end)
+ let val M = mtype_for T in
+ (M, ({bounds = bounds, frees = frees,
+ consts = (x, M) :: consts}, cset))
+ end) |>> curry MRaw t
| Free (x as (_, T)) =>
(case AList.lookup (op =) frees x of
- SOME C => (C, accum)
+ SOME M => (M, accum)
| NONE =>
- let val C = ctype_for T in
- (C, ({bounds = bounds, frees = (x, C) :: frees,
+ let val M = mtype_for T in
+ (M, ({bounds = bounds, frees = (x, M) :: frees,
consts = consts}, cset))
- end)
- | Var _ => (print_g "*** Var"; unsolvable)
- | Bound j => (nth bounds j, accum)
- | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
- | Abs (_, T, t') =>
+ end) |>> curry MRaw t
+ | Var _ => (print_g "*** Var"; mterm_unsolvable t)
+ | Bound j => (MRaw (t, nth bounds j), accum)
+ | Abs (s, T, t' as @{const False}) =>
+ let val (M1, a, M2) = mfun_for T bool_T in
+ (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
+ end
+ | Abs (s, T, t') =>
((case t' of
t1' $ Bound 0 =>
if not (loose_bvar1 (t1', 0)) then
@@ -761,107 +852,127 @@
| _ => raise SAME ())
handle SAME () =>
let
- val C = ctype_for T
- val (C', accum) = do_term t' (accum |>> push_bound C)
- in (CFun (C, S Minus, C'), accum |>> pop_bound) end)
- | Const (@{const_name All}, _)
- $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
- do_bounded_quantifier T' t1 t2 accum
- | Const (@{const_name Ex}, _)
- $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) =>
- do_bounded_quantifier T' t1 t2 accum
+ val M = mtype_for T
+ val (m', accum) = do_term t' (accum |>> push_bound M)
+ in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
+ | (t0 as Const (@{const_name All}, _))
+ $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
+ do_bounded_quantifier t0 s' T' t10 t11 t12 accum
+ | (t0 as Const (@{const_name Ex}, _))
+ $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
+ do_bounded_quantifier t0 s' T' t10 t11 t12 accum
| Const (@{const_name Let}, _) $ t1 $ t2 =>
do_term (betapply (t2, t1)) accum
| t1 $ t2 =>
let
- val (C1, accum) = do_term t1 accum
- val (C2, accum) = do_term t2 accum
+ val (m1, accum) = do_term t1 accum
+ val (m2, accum) = do_term t2 accum
in
case accum of
- (_, UnsolvableCSet) => unsolvable
- | _ => case C1 of
- CFun (C11, _, C12) =>
- (C12, accum ||> add_is_sub_ctype C2 C11)
- | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
- \(op $)", [C1])
+ (_, UnsolvableCSet) => mterm_unsolvable t
+ | _ =>
+ let
+ val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
+ val M2 = mtype_of_mterm m2
+ in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
end)
- |> tap (fn (C, _) =>
- print_g (" \<Gamma> \<turnstile> " ^
- Syntax.string_of_term ctxt t ^ " : " ^
- string_for_ctype C))
+ |> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m))
in do_term end
-(* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
+(* mdata -> styp -> term -> term -> mterm * accumulator *)
+fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
let
- (* typ -> ctype *)
- val ctype_for = fresh_ctype_for_type cdata
- (* term -> accumulator -> ctype * accumulator *)
- val do_term = consider_term cdata
- (* sign -> term -> accumulator -> accumulator *)
- fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
- | do_formula sn t (accum as (gamma, cset)) =
+ val (m1, accum) = consider_term mdata t1 accum
+ val (m2, accum) = consider_term mdata t2 accum
+ val M1 = mtype_of_mterm m1
+ val M2 = mtype_of_mterm m2
+ val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+ in
+ (MApp (MApp (MRaw (Const x,
+ MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
+ accum ||> add_mtypes_equal M1 M2)
+ end
+
+(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
+fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
+ let
+ (* typ -> mtyp *)
+ val mtype_for = fresh_mtype_for_type mdata
+ (* term -> accumulator -> mterm * accumulator *)
+ val do_term = consider_term mdata
+ (* sign -> term -> accumulator -> mterm * accumulator *)
+ fun do_formula _ t (_, UnsolvableCSet) =
+ (MRaw (t, dummy_M), unsolvable_accum)
+ | do_formula sn t accum =
let
- (* term -> accumulator -> accumulator *)
- val do_co_formula = do_formula sn
- val do_contra_formula = do_formula (negate sn)
- (* string -> typ -> term -> accumulator *)
- fun do_quantifier quant_s abs_T body_t =
+ (* styp -> string -> typ -> term -> mterm * accumulator *)
+ fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
let
- val abs_C = ctype_for abs_T
+ val abs_M = mtype_for abs_T
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
- val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
+ val (body_m, accum) =
+ accum ||> side_cond ? add_mtype_is_right_total abs_M
+ |>> push_bound abs_M |> do_formula sn body_t
+ val body_M = mtype_of_mterm body_m
in
- (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
- |>> pop_bound
+ (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
+ MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
+ accum |>> pop_bound)
end
- (* typ -> term -> accumulator *)
- fun do_bounded_quantifier abs_T body_t =
- accum |>> push_bound (ctype_for abs_T) |> do_co_formula body_t
- |>> pop_bound
- (* term -> term -> accumulator *)
- fun do_equals t1 t2 =
+ (* styp -> term -> term -> mterm * accumulator *)
+ fun do_equals x t1 t2 =
case sn of
- Plus => do_term t accum |> snd
- | Minus => let
- val (C1, accum) = do_term t1 accum
- val (C2, accum) = do_term t2 accum
- in accum ||> add_ctypes_equal C1 C2 end
+ Plus => do_term t accum
+ | Minus => consider_general_equals mdata x t1 t2 accum
in
case t of
- Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
- do_quantifier s0 T1 t1
- | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
- | @{const "==>"} $ t1 $ t2 =>
- accum |> do_contra_formula t1 |> do_co_formula t2
- | @{const Trueprop} $ t1 => do_co_formula t1 accum
- | @{const Not} $ t1 => do_contra_formula t1 accum
- | Const (@{const_name All}, _)
- $ Abs (_, T1, t1 as @{const "op -->"} $ (_ $ Bound 0) $ _) =>
- do_bounded_quantifier T1 t1
- | Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) =>
- do_quantifier s0 T1 t1
- | Const (@{const_name Ex}, _)
- $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
- do_bounded_quantifier T1 t1
- | Const (s0 as @{const_name Ex}, _) $ Abs (_, T1, t1) =>
- do_quantifier s0 T1 t1
- | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
- | @{const "op &"} $ t1 $ t2 =>
- accum |> do_co_formula t1 |> do_co_formula t2
- | @{const "op |"} $ t1 $ t2 =>
- accum |> do_co_formula t1 |> do_co_formula t2
- | @{const "op -->"} $ t1 $ t2 =>
- accum |> do_contra_formula t1 |> do_co_formula t2
- | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
- accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
- | Const (@{const_name Let}, _) $ t1 $ t2 =>
- do_co_formula (betapply (t2, t1)) accum
- | _ => do_term t accum |> snd
+ Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
+ | @{const Trueprop} $ t1 =>
+ let val (m1, accum) = do_formula sn t1 accum in
+ (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+ m1), accum)
+ end
+ | @{const Not} $ t1 =>
+ let val (m1, accum) = do_formula (negate sn) t1 accum in
+ (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
+ accum)
+ end
+ | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x0 as (s0 as @{const_name Ex}, T0))
+ $ (t1 as Abs (s1, T1, t1')) =>
+ (case sn of
+ Plus => do_quantifier x0 s1 T1 t1'
+ | Minus =>
+ (* ### do elsewhere *)
+ do_term (@{const Not}
+ $ (HOLogic.eq_const (domain_type T0) $ t1
+ $ Abs (Name.uu, T1, @{const False}))) accum)
+ | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ do_equals x t1 t2
+ | (t0 as Const (s0, _)) $ t1 $ t2 =>
+ if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
+ s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
+ let
+ val impl = (s0 = @{const_name "==>"} orelse
+ s0 = @{const_name "op -->"})
+ val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
+ val (m2, accum) = do_formula sn t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
+ accum)
+ end
+ else
+ do_term t accum
+ | _ => do_term t accum
end
- |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
- Syntax.string_of_term ctxt t ^
- " : o\<^sup>" ^ string_for_sign sn))
+ |> tap (fn (m, _) =>
+ print_g ("\<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m ^ " : o\<^sup>" ^
+ string_for_sign sn))
in do_formula end
(* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -877,79 +988,110 @@
|> (forall (member (op =) harmless_consts o original_name o fst)
orf exists (member (op =) bounteous_consts o fst))
-(* cdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
- not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
+(* mdata -> term -> accumulator -> mterm * accumulator *)
+fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
+ if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
+ else consider_general_formula mdata Plus t
-(* cdata -> term -> accumulator -> accumulator *)
-fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
+(* mdata -> term -> accumulator -> mterm * accumulator *)
+fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
- consider_nondefinitional_axiom cdata Plus t
+ consider_nondefinitional_axiom mdata t
else if is_harmless_axiom hol_ctxt t then
- I
+ pair (MRaw (t, dummy_M))
else
let
- (* term -> accumulator -> ctype * accumulator *)
- val do_term = consider_term cdata
- (* typ -> term -> accumulator -> accumulator *)
- fun do_all abs_T body_t accum =
- let val abs_C = fresh_ctype_for_type cdata abs_T in
- accum |>> push_bound abs_C |> do_formula body_t |>> pop_bound
+ (* typ -> mtyp *)
+ val mtype_for = fresh_mtype_for_type mdata
+ (* term -> accumulator -> mterm * accumulator *)
+ val do_term = consider_term mdata
+ (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
+ fun do_all quant_t abs_s abs_T body_t accum =
+ let
+ val abs_M = mtype_for abs_T
+ val (body_m, accum) =
+ accum |>> push_bound abs_M |> do_formula body_t
+ val body_M = mtype_of_mterm body_m
+ in
+ (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
+ MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
+ accum |>> pop_bound)
end
- (* term -> term -> accumulator -> accumulator *)
- and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
- and do_equals t1 t2 accum =
+ (* term -> term -> term -> accumulator -> mterm * accumulator *)
+ and do_conjunction t0 t1 t2 accum =
let
- val (C1, accum) = do_term t1 accum
- val (C2, accum) = do_term t2 accum
- in accum ||> add_ctypes_equal C1 C2 end
+ val (m1, accum) = do_formula t1 accum
+ val (m2, accum) = do_formula t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
+ end
+ and do_implies t0 t1 t2 accum =
+ let
+ val (m1, accum) = do_term t1 accum
+ val (m2, accum) = do_formula t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
+ end
(* term -> accumulator -> accumulator *)
- and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
+ and do_formula t (_, UnsolvableCSet) =
+ (MRaw (t, dummy_M), unsolvable_accum)
| do_formula t accum =
case t of
- Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
+ (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+ do_all t0 s1 T1 t1 accum
| @{const Trueprop} $ t1 => do_formula t1 accum
- | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum
- | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
- | @{const Pure.conjunction} $ t1 $ t2 =>
- accum |> do_formula t1 |> do_formula t2
- | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
- | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
- | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
- | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
+ | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
+ consider_general_equals mdata x t1 t2 accum
+ | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+ | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
+ do_conjunction t0 t1 t2 accum
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
+ do_all t0 s0 T1 t1 accum
+ | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ consider_general_equals mdata x t1 t2 accum
+ | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
-(* Proof.context -> literal list -> term -> ctype -> string *)
-fun string_for_ctype_of_term ctxt lits t C =
+(* Proof.context -> literal list -> term -> mtyp -> string *)
+fun string_for_mtype_of_term ctxt lits t M =
Syntax.string_of_term ctxt t ^ " : " ^
- string_for_ctype (instantiate_ctype lits C)
+ string_for_mtype (instantiate_mtype lits M)
-(* theory -> literal list -> ctype_context -> unit *)
-fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
- map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
- map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
+(* theory -> literal list -> mtype_context -> unit *)
+fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
+ map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
+ map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
|> cat_lines |> print_g
-(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
- -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
- nondef_ts core_t =
+(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
+fun gather f t (ms, accum) =
+ let val (m, accum) = f t accum in (m :: ms, accum) end
+
+(* hol_context -> bool -> typ -> term list * term list -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
+ (nondef_ts, def_ts) =
let
- val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
+ val _ = print_g ("****** Monotonicity analysis: " ^
+ string_for_mtype MAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
- val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
- val (gamma, cset) =
- (initial_gamma, slack)
- |> fold (consider_definitional_axiom cdata) def_ts
- |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
- |> consider_general_formula cdata sn core_t
+ val mdata as {max_fresh, constr_cache, ...} =
+ initial_mdata hol_ctxt binarize alpha_T
+
+ val accum = (initial_gamma, slack)
+ val (nondef_ms, accum) =
+ ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
+ |> fold (gather (consider_nondefinitional_axiom mdata))
+ (tl nondef_ts)
+ val (def_ms, (gamma, cset)) =
+ ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
in
case solve (!max_fresh) cset of
- SOME lits => (print_ctype_context ctxt lits gamma; true)
+ SOME lits => (print_mtype_context ctxt lits gamma; true)
| _ => false
end
- handle CTYPE (loc, Cs) => raise BAD (loc, commas (map string_for_ctype Cs))
+ handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
end;
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 13:29:43 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 16:50:09 2010 +0100
@@ -9,8 +9,7 @@
sig
type hol_context = Nitpick_HOL.hol_context
val preprocess_term :
- hol_context -> term
- -> ((term list * term list) * (bool * bool)) * term * bool
+ hol_context -> term -> term list * term list * bool * bool * bool
end
structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -136,6 +135,59 @@
(index_seq 0 (length arg_Ts)) arg_Ts)
end
+(* (term -> term) -> int -> term -> term *)
+fun coerce_bound_no f j t =
+ case t of
+ t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+ | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+ | Bound j' => if j' = j then f t else t
+ | _ => t
+(* hol_context -> typ -> typ -> term -> term *)
+fun coerce_bound_0_in_term hol_ctxt new_T old_T =
+ old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
+(* hol_context -> typ list -> typ -> typ -> term -> term *)
+and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+ if old_T = new_T then
+ t
+ else
+ case (new_T, old_T) of
+ (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type ("fun", [old_T1, old_T2])) =>
+ (case eta_expand Ts t 1 of
+ Abs (s, _, t') =>
+ Abs (s, new_T1,
+ t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
+ |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
+ |> Envir.eta_contract
+ |> new_s <> "fun"
+ ? construct_value thy stds
+ (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+ o single
+ | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
+ | (Type (new_s, new_Ts as [new_T1, new_T2]),
+ Type (old_s, old_Ts as [old_T1, old_T2])) =>
+ if old_s = @{type_name fun_box} orelse
+ old_s = @{type_name pair_box} orelse old_s = "*" then
+ case constr_expand hol_ctxt old_T t of
+ Const (old_s, _) $ t1 =>
+ if new_s = "fun" then
+ coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
+ else
+ construct_value thy stds
+ (old_s, Type ("fun", new_Ts) --> new_T)
+ [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
+ (Type ("fun", old_Ts)) t1]
+ | Const _ $ t1 $ t2 =>
+ construct_value thy stds
+ (if new_s = "*" then @{const_name Pair}
+ else @{const_name PairBox}, new_Ts ---> new_T)
+ [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
+ coerce_term hol_ctxt Ts new_T2 old_T2 t2]
+ | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
+ else
+ raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
+ | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
+
(* hol_context -> bool -> term -> term *)
fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
orig_t =
@@ -146,60 +198,6 @@
| box_relational_operator_type (Type ("*", Ts)) =
Type ("*", map (box_type hol_ctxt InPair) Ts)
| box_relational_operator_type T = T
- (* (term -> term) -> int -> term -> term *)
- fun coerce_bound_no f j t =
- case t of
- t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
- | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
- | Bound j' => if j' = j then f t else t
- | _ => t
- (* typ -> typ -> term -> term *)
- fun coerce_bound_0_in_term new_T old_T =
- old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
- (* typ list -> typ -> term -> term *)
- and coerce_term Ts new_T old_T t =
- if old_T = new_T then
- t
- else
- case (new_T, old_T) of
- (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type ("fun", [old_T1, old_T2])) =>
- (case eta_expand Ts t 1 of
- Abs (s, _, t') =>
- Abs (s, new_T1,
- t' |> coerce_bound_0_in_term new_T1 old_T1
- |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
- |> Envir.eta_contract
- |> new_s <> "fun"
- ? construct_value thy stds
- (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
- o single
- | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
- \coerce_term", [t']))
- | (Type (new_s, new_Ts as [new_T1, new_T2]),
- Type (old_s, old_Ts as [old_T1, old_T2])) =>
- if old_s = @{type_name fun_box} orelse
- old_s = @{type_name pair_box} orelse old_s = "*" then
- case constr_expand hol_ctxt old_T t of
- Const (@{const_name FunBox}, _) $ t1 =>
- if new_s = "fun" then
- coerce_term Ts new_T (Type ("fun", old_Ts)) t1
- else
- construct_value thy stds
- (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
- [coerce_term Ts (Type ("fun", new_Ts))
- (Type ("fun", old_Ts)) t1]
- | Const _ $ t1 $ t2 =>
- construct_value thy stds
- (if new_s = "*" then @{const_name Pair}
- else @{const_name PairBox}, new_Ts ---> new_T)
- [coerce_term Ts new_T1 old_T1 t1,
- coerce_term Ts new_T2 old_T2 t2]
- | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
- \coerce_term", [t'])
- else
- raise TYPE ("coerce_term", [new_T, old_T], [t])
- | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
(* indexname * typ -> typ * term -> typ option list -> typ option list *)
fun add_boxed_types_for_var (z as (_, T)) (T', t') =
case t' of
@@ -252,7 +250,7 @@
val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
in
list_comb (Const (s0, T --> T --> body_type T0),
- map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
+ map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
end
(* string -> typ -> term *)
and do_description_operator s T =
@@ -320,7 +318,7 @@
val T' = hd (snd (dest_Type (hd Ts1)))
val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
val T2 = fastype_of1 (new_Ts, t2)
- val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+ val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
in
betapply (if s1 = "fun" then
t1
@@ -336,7 +334,7 @@
val (s1, Ts1) = dest_Type T1
val t2 = do_term new_Ts old_Ts Neut t2
val T2 = fastype_of1 (new_Ts, t2)
- val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+ val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
in
betapply (if s1 = "fun" then
t1
@@ -474,6 +472,19 @@
(list_comb (t, args), seen)
in aux [] 0 t [] [] |> fst end
+val let_var_prefix = nitpick_prefix ^ "l"
+val let_inline_threshold = 32
+
+(* int -> typ -> term -> (term -> term) -> term *)
+fun hol_let n abs_T body_T f t =
+ if n * size_of_term t <= let_inline_threshold then
+ f t
+ else
+ let val z = ((let_var_prefix, 0), abs_T) in
+ Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
+ $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
+ end
+
(* hol_context -> bool -> term -> term *)
fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
let
@@ -508,14 +519,19 @@
if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
else raise SAME ()
| (Const (x as (s, T)), args) =>
- let val arg_Ts = binder_types T in
- if length arg_Ts = length args andalso
- (is_constr thy stds x orelse s = @{const_name Pair}) andalso
+ let
+ val (arg_Ts, dataT) = strip_type T
+ val n = length arg_Ts
+ in
+ if length args = n andalso
+ (is_constr thy stds x orelse s = @{const_name Pair} orelse
+ x = (@{const_name Suc}, nat_T --> nat_T)) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- discriminate_value hol_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
- |> foldr1 s_conj
+ hol_let (n + 1) dataT bool_T
+ (fn t1 => discriminate_value hol_ctxt x t1 ::
+ map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
+ |> foldr1 s_conj) t1
else
raise SAME ()
end
@@ -1020,7 +1036,7 @@
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
val axioms_max_depth = 255
-(* hol_context -> term -> (term list * term list) * (bool * bool) *)
+(* hol_context -> term -> term list * term list * bool * bool *)
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
fast_descrs, evals, def_table, nondef_table, user_nondefs,
@@ -1170,10 +1186,9 @@
|> user_axioms = SOME true
? fold (add_nondef_axiom 1) mono_user_nondefs
val defs = defs @ special_congruence_axioms hol_ctxt xs
- in
- ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
- null poly_user_nondefs))
- end
+ val got_all_mono_user_axioms =
+ (user_axioms = SOME true orelse null mono_user_nondefs)
+ in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
(** Simplification of constructor/selector terms **)
@@ -1275,7 +1290,7 @@
(* Maximum number of quantifiers in a cluster for which the exponential
algorithm is used. Larger clusters use a heuristic inspired by Claessen &
- Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
+ Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
paper). *)
val quantifier_cluster_threshold = 7
@@ -1386,29 +1401,29 @@
(** Preprocessor entry point **)
-(* hol_context -> term
- -> ((term list * term list) * (bool * bool)) * term * bool *)
+(* hol_context -> term -> term list * term list * bool * bool * bool *)
fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
boxes, skolemize, uncurry, ...}) t =
let
val skolem_depth = if skolemize then 4 else ~1
- val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = t |> unfold_defs_in_term hol_ctxt
- |> close_form
- |> skolemize_term_and_more hol_ctxt skolem_depth
- |> specialize_consts_in_term hol_ctxt 0
- |> `(axioms_for_term hol_ctxt)
+ val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
+ t |> unfold_defs_in_term hol_ctxt
+ |> close_form
+ |> skolemize_term_and_more hol_ctxt skolem_depth
+ |> specialize_consts_in_term hol_ctxt 0
+ |> axioms_for_term hol_ctxt
val binarize =
is_standard_datatype thy stds nat_T andalso
case binary_ints of
SOME false => false
- | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+ | _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso
(binary_ints = SOME true orelse
- exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ exists should_use_binary_ints (nondef_ts @ def_ts))
val box = exists (not_equal (SOME false) o snd) boxes
+ val uncurry = uncurry andalso box
val table =
- Termtab.empty |> uncurry
- ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
+ Termtab.empty
+ |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
(* bool -> term -> term *)
fun do_rest def =
binarize ? binarize_nat_and_int_in_term
@@ -1425,10 +1440,10 @@
#> push_quantifiers_inward
#> close_form
#> Term.map_abs_vars shortest_name
+ val nondef_ts = map (do_rest false) nondef_ts
+ val def_ts = map (do_rest true) def_ts
in
- (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
- (got_all_mono_user_axioms, no_poly_user_axioms)),
- do_rest false core_t, binarize)
+ (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
end
end;