64389

1 
(* Title: HOL/Nunchaku/Tools/nunchaku_collect.ML


2 
Author: Jasmin Blanchette, Inria Nancy, LORIA, MPII


3 
Copyright 2015, 2016


4 


5 
Collecting of Isabelle/HOL definitions etc. for Nunchaku.


6 
*)


7 


8 
signature NUNCHAKU_COLLECT =


9 
sig


10 
val dest_co_datatype_case: Proof.context > string * typ > (string * typ) list


11 


12 
type isa_type_spec =


13 
{abs_typ: typ,


14 
rep_typ: typ,


15 
wrt: term,


16 
abs: term,


17 
rep: term}


18 


19 
type isa_co_data_spec =


20 
{typ: typ,


21 
ctrs: term list}


22 


23 
type isa_const_spec =


24 
{const: term,


25 
props: term list}


26 


27 
type isa_rec_spec =


28 
{const: term,


29 
props: term list,


30 
pat_complete: bool}


31 


32 
type isa_consts_spec =


33 
{consts: term list,


34 
props: term list}


35 


36 
datatype isa_command =


37 
ITVal of typ * (int option * int option)


38 
 ICopy of isa_type_spec


39 
 IQuotient of isa_type_spec


40 
 ICoData of BNF_Util.fp_kind * isa_co_data_spec list


41 
 IVal of term


42 
 ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list


43 
 IRec of isa_rec_spec list


44 
 ISpec of isa_consts_spec


45 
 IAxiom of term


46 
 IGoal of term


47 
 IEval of term


48 


49 
type isa_problem =


50 
{commandss: isa_command list list,


51 
sound: bool,


52 
complete: bool}


53 


54 
exception CYCLIC_DEPS of unit


55 
exception TOO_DEEP_DEPS of unit


56 
exception TOO_META of term


57 
exception UNEXPECTED_POLYMORPHISM of term


58 
exception UNEXPECTED_VAR of term


59 
exception UNSUPPORTED_FUNC of term


60 


61 
val isa_problem_of_subgoal: Proof.context > bool > ((string * typ) option * bool option) list >


62 
(term option * bool) list > (typ option * (int option * int option)) list > bool >


63 
Time.time > term list > term list > term > term list * isa_problem


64 
val pat_completes_of_isa_problem: isa_problem > term list


65 
val str_of_isa_problem: Proof.context > isa_problem > string


66 
end;


67 


68 
structure Nunchaku_Collect : NUNCHAKU_COLLECT =


69 
struct


70 


71 
open Nunchaku_Util;


72 


73 
type isa_type_spec =


74 
{abs_typ: typ,


75 
rep_typ: typ,


76 
wrt: term,


77 
abs: term,


78 
rep: term};


79 


80 
type isa_co_data_spec =


81 
{typ: typ,


82 
ctrs: term list};


83 


84 
type isa_const_spec =


85 
{const: term,


86 
props: term list};


87 


88 
type isa_rec_spec =


89 
{const: term,


90 
props: term list,


91 
pat_complete: bool};


92 


93 
type isa_consts_spec =


94 
{consts: term list,


95 
props: term list};


96 


97 
datatype isa_command =


98 
ITVal of typ * (int option * int option)


99 
 ICopy of isa_type_spec


100 
 IQuotient of isa_type_spec


101 
 ICoData of BNF_Util.fp_kind * isa_co_data_spec list


102 
 IVal of term


103 
 ICoPred of BNF_Util.fp_kind * bool * isa_const_spec list


104 
 IRec of isa_rec_spec list


105 
 ISpec of isa_consts_spec


106 
 IAxiom of term


107 
 IGoal of term


108 
 IEval of term;


109 


110 
type isa_problem =


111 
{commandss: isa_command list list,


112 
sound: bool,


113 
complete: bool};


114 


115 
exception CYCLIC_DEPS of unit;


116 
exception TOO_DEEP_DEPS of unit;


117 
exception TOO_META of term;


118 
exception UNEXPECTED_POLYMORPHISM of term;


119 
exception UNEXPECTED_VAR of term;


120 
exception UNSUPPORTED_FUNC of term;


121 


122 
fun str_of_and_list str_of_elem =


123 
map str_of_elem #> space_implode ("\nand ");


124 


125 
val key_of_typ =


126 
let


127 
fun key_of (Type (s, [])) = s


128 
 key_of (Type (s, Ts)) = s ^ "(" ^ commas (map key_of Ts) ^ ")"


129 
 key_of (TFree (s, _)) = s;


130 
in


131 
prefix "y" o key_of


132 
end;


133 


134 
fun key_of_const ctxt =


135 
let


136 
val thy = Proof_Context.theory_of ctxt;


137 


138 
fun key_of (Const (x as (s, _))) =


139 
(case Sign.const_typargs thy x of


140 
[] => s


141 
 Ts => s ^ "(" ^ commas (map key_of_typ Ts) ^ ")")


142 
 key_of (Free (s, _)) = s;


143 
in


144 
prefix "t" o key_of


145 
end;


146 


147 
val add_type_keys = fold_subtypes (insert (op =) o key_of_typ);


148 


149 
fun add_aterm_keys ctxt t =


150 
if is_Const t orelse is_Free t then insert (op =) (key_of_const ctxt t) else I;


151 


152 
fun add_keys ctxt t =


153 
fold_aterms (add_aterm_keys ctxt) t


154 
#> fold_types add_type_keys t;


155 


156 
fun close_form except t =


157 
fold (fn ((s, i), T) => fn t' =>


158 
HOLogic.all_const T $ Abs (s, T, abstract_over (Var ((s, i), T), t')))


159 
(Term.add_vars t [] > subtract (op =) except) t;


160 


161 
(* "imp_conjL[symmetric]" is important for inductive predicates with multiple assumptions. *)


162 
val basic_defs =


163 
@{thms Ball_def[abs_def] Bex_def[abs_def] case_bool_if Ex1_def[abs_def]


164 
imp_conjL[symmetric, abs_def] Let_def[abs_def] rmember_def[symmetric, abs_def]};


165 


166 
fun unfold_basic_def ctxt =


167 
let val thy = Proof_Context.theory_of ctxt in


168 
Pattern.rewrite_term thy (map (Logic.dest_equals o Thm.prop_of) basic_defs) []


169 
end;


170 


171 
val has_polymorphism = exists_type (exists_subtype is_TVar);


172 


173 
fun whack_term thy whacks =


174 
let


175 
fun whk t =


176 
if triple_lookup (term_match thy o swap) whacks t = SOME true then


177 
Const (@{const_name unreachable}, fastype_of t)


178 
else


179 
(case t of


180 
u $ v => whk u $ whk v


181 
 Abs (s, T, u) => Abs (s, T, whk u)


182 
 _ => t);


183 
in


184 
whk


185 
end;


186 


187 
fun preprocess_term_basic falsify ctxt whacks t =


188 
let val thy = Proof_Context.theory_of ctxt in


189 
if has_polymorphism t then


190 
raise UNEXPECTED_POLYMORPHISM t


191 
else


192 
t


193 
> attach_typeS


194 
> whack_term thy whacks


195 
> Object_Logic.atomize_term ctxt


196 
> tap (fn t' => fastype_of t' <> @{typ prop} orelse raise TOO_META t)


197 
> falsify ? HOLogic.mk_not


198 
> unfold_basic_def ctxt


199 
end;


200 


201 
val check_closed = tap (fn t => null (Term.add_vars t []) orelse raise UNEXPECTED_VAR t);


202 


203 
val preprocess_prop = close_form [] oooo preprocess_term_basic;


204 
val preprocess_closed_term = check_closed ooo preprocess_term_basic false;


205 


206 
val is_type_builtin = member (op =) [@{type_name bool}, @{type_name fun}];


207 


208 
val is_const_builtin =


209 
member (op =) [@{const_name All}, @{const_name conj}, @{const_name disj}, @{const_name Eps},


210 
@{const_name HOL.eq}, @{const_name Ex}, @{const_name False}, @{const_name If},


211 
@{const_name implies}, @{const_name Not}, @{const_name The}, @{const_name The_unsafe},


212 
@{const_name True}];


213 


214 
datatype type_classification = Builtin  TVal  Copy  Quotient  Co_Datatype;


215 


216 
fun classify_type_name ctxt T_name =


217 
if is_type_builtin T_name then


218 
Builtin


219 
else if T_name = @{type_name itself} then


220 
Co_Datatype


221 
else


222 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of


223 
SOME _ => Co_Datatype


224 
 NONE =>


225 
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of


226 
SOME _ => Co_Datatype


227 
 NONE =>


228 
(case Quotient_Info.lookup_quotients ctxt T_name of


229 
SOME _ => Quotient


230 
 NONE =>


231 
if T_name = @{type_name set} then


232 
Copy


233 
else


234 
(case Typedef.get_info ctxt T_name of


235 
_ :: _ => Copy


236 
 [] => TVal))));


237 


238 
fun fp_kind_of_ctr_sugar_kind Ctr_Sugar.Codatatype = BNF_Util.Greatest_FP


239 
 fp_kind_of_ctr_sugar_kind _ = BNF_Util.Least_FP;


240 


241 
fun mutual_co_datatypes_of ctxt (T_name, Ts) =


242 
(if T_name = @{type_name itself} then


243 
(BNF_Util.Least_FP, [@{typ "'a itself"}], [[@{const Pure.type ('a)}]])


244 
else


245 
let


246 
val (fp, ctr_sugars) =


247 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt T_name of


248 
SOME (fp_sugar as {fp, fp_res = {Ts, ...}, ...}) =>


249 
(fp,


250 
(case Ts of


251 
[_] => [fp_sugar]


252 
 _ => map (the o BNF_FP_Def_Sugar.fp_sugar_of ctxt o fst o dest_Type) Ts)


253 
> map (#ctr_sugar o #fp_ctr_sugar))


254 
 NONE =>


255 
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of


256 
SOME (ctr_sugar as {kind, ...}) =>


257 
(* Any freely constructed type that is not a codatatype is considered a datatype. This


258 
is sound (but incomplete) for model finding. *)


259 
(fp_kind_of_ctr_sugar_kind kind, [ctr_sugar])));


260 
in


261 
(fp, map #T ctr_sugars, map #ctrs ctr_sugars)


262 
end)


263 
> @{apply 3(2)} (map ((fn Type (s, _) => Type (s, Ts))))


264 
> @{apply 3(3)} (map (map (Ctr_Sugar.mk_ctr Ts)));


265 


266 
fun quotient_of ctxt T_name =


267 
(case Quotient_Info.lookup_quotients ctxt T_name of


268 
SOME {equiv_rel, qtyp, rtyp, quot_thm, ...} =>


269 
let val _ $ (_ $ _ $ abs $ rep) = Thm.prop_of quot_thm in


270 
(qtyp, rtyp, equiv_rel, abs, rep)


271 
end);


272 


273 
fun copy_of ctxt T_name =


274 
if T_name = @{type_name set} then


275 
let


276 
val A = Logic.varifyT_global @{typ 'a};


277 
val absT = Type (@{type_name set}, [A]);


278 
val repT = A > HOLogic.boolT;


279 
val wrt = Abs (Name.uu, repT, @{const True});


280 
val abs = Const (@{const_name Collect}, repT > absT);


281 
val rep = Const (@{const_name rmember}, absT > repT);


282 
in


283 
(absT, repT, wrt, abs, rep)


284 
end


285 
else


286 
(case Typedef.get_info ctxt T_name of


287 
(* When several entries are returned, it shouldn't matter much which one we take (according to


288 
Florian Haftmann). The "Logic.varifyT_global" calls are a workaround because these types'


289 
variables sometimes clash with locally fixed type variables. *)


290 
({abs_type, rep_type, Abs_name, Rep_name, ...}, {Rep, ...}) :: _ =>


291 
let


292 
val absT = Logic.varifyT_global abs_type;


293 
val repT = Logic.varifyT_global rep_type;


294 
val wrt = Thm.prop_of Rep


295 
> HOLogic.dest_Trueprop


296 
> HOLogic.dest_mem


297 
> snd;


298 
val abs = Const (Abs_name, repT > absT);


299 
val rep = Const (Rep_name, absT > repT);


300 
in


301 
(absT, repT, wrt, abs, rep)


302 
end);


303 


304 
fun is_co_datatype_ctr ctxt (s, T) =


305 
(case body_type T of


306 
Type (fpT_name, Ts) =>


307 
classify_type_name ctxt fpT_name = Co_Datatype andalso


308 
let


309 
val ctrs =


310 
if fpT_name = @{type_name itself} then


311 
[Const (@{const_name Pure.type}, @{typ "'a itself"})]


312 
else


313 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of


314 
SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, ...}, ...}, ...} => ctrs


315 
 NONE =>


316 
(case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of


317 
SOME {ctrs, ...} => ctrs


318 
 _ => []));


319 


320 
fun is_right_ctr (t' as Const (s', _)) =


321 
s = s' andalso fastype_of (Ctr_Sugar.mk_ctr Ts t') = T;


322 
in


323 
exists is_right_ctr ctrs


324 
end


325 
 _ => false);


326 


327 
fun dest_co_datatype_case ctxt (s, T) =


328 
let val thy = Proof_Context.theory_of ctxt in


329 
(case strip_fun_type (Sign.the_const_type thy s) of


330 
(gen_branch_Ts, gen_body_fun_T) =>


331 
(case gen_body_fun_T of


332 
Type (@{type_name fun}, [Type (fpT_name, _), _]) =>


333 
if classify_type_name ctxt fpT_name = Co_Datatype then


334 
let


335 
val Type (_, fpTs) = domain_type (funpow (length gen_branch_Ts) range_type T);


336 
val (ctrs0, Const (case_name, _)) =


337 
(case BNF_FP_Def_Sugar.fp_sugar_of ctxt fpT_name of


338 
SOME {fp_ctr_sugar = {ctr_sugar = {ctrs, casex, ...}, ...}, ...} => (ctrs, casex)


339 
 NONE =>


340 
(case Ctr_Sugar.ctr_sugar_of ctxt fpT_name of


341 
SOME {ctrs, casex, ...} => (ctrs, casex)));


342 
in


343 
if s = case_name then map (dest_Const o Ctr_Sugar.mk_ctr fpTs) ctrs0


344 
else raise Fail "noncase"


345 
end


346 
else


347 
raise Fail "noncase"))


348 
end;


349 


350 
val is_co_datatype_case = can o dest_co_datatype_case;


351 


352 
fun is_quotient_abs ctxt (s, T) =


353 
(case T of


354 
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>


355 
classify_type_name ctxt absT_name = Quotient andalso


356 
(case quotient_of ctxt absT_name of


357 
(_, _, _, Const (s', _), _) => s' = s)


358 
 _ => false);


359 


360 
fun is_quotient_rep ctxt (s, T) =


361 
(case T of


362 
Type (@{type_name fun}, [Type (absT_name, _), _]) =>


363 
classify_type_name ctxt absT_name = Quotient andalso


364 
(case quotient_of ctxt absT_name of


365 
(_, _, _, _, Const (s', _)) => s' = s)


366 
 _ => false);


367 


368 
fun is_maybe_copy_abs ctxt absT_name s =


369 
if absT_name = @{type_name set} then


370 
s = @{const_name Collect}


371 
else


372 
(case try (copy_of ctxt) absT_name of


373 
SOME (_, _, _, Const (s', _), _) => s' = s


374 
 NONE => false);


375 


376 
fun is_maybe_copy_rep ctxt absT_name s =


377 
if absT_name = @{type_name set} then


378 
s = @{const_name rmember}


379 
else


380 
(case try (copy_of ctxt) absT_name of


381 
SOME (_, _, _, _, Const (s', _)) => s' = s


382 
 NONE => false);


383 


384 
fun is_copy_abs ctxt (s, T) =


385 
(case T of


386 
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>


387 
classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_abs ctxt absT_name s


388 
 _ => false);


389 


390 
fun is_copy_rep ctxt (s, T) =


391 
(case T of


392 
Type (@{type_name fun}, [Type (absT_name, _), _]) =>


393 
classify_type_name ctxt absT_name = Copy andalso is_maybe_copy_rep ctxt absT_name s


394 
 _ => false);


395 


396 
fun is_stale_copy_abs ctxt (s, T) =


397 
(case T of


398 
Type (@{type_name fun}, [_, Type (absT_name, _)]) =>


399 
classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_abs ctxt absT_name s


400 
 _ => false);


401 


402 
fun is_stale_copy_rep ctxt (s, T) =


403 
(case T of


404 
Type (@{type_name fun}, [Type (absT_name, _), _]) =>


405 
classify_type_name ctxt absT_name <> Copy andalso is_maybe_copy_rep ctxt absT_name s


406 
 _ => false);


407 


408 
fun instantiate_constant_types_in_term ctxt csts target =


409 
let


410 
val thy = Proof_Context.theory_of ctxt;


411 


412 
fun try_const _ _ (res as SOME _) = res


413 
 try_const (s', T') cst NONE =


414 
(case cst of


415 
Const (s, T) =>


416 
if s = s' then


417 
SOME (Sign.typ_match thy (T', T) Vartab.empty)


418 
handle Type.TYPE_MATCH => NONE


419 
else


420 
NONE


421 
 _ => NONE);


422 


423 
fun subst_for (Const x) = fold (try_const x) csts NONE


424 
 subst_for (t as Free _) = if member (op aconv) csts t then SOME Vartab.empty else NONE


425 
 subst_for (t1 $ t2) = (case subst_for t1 of SOME subst => SOME subst  NONE => subst_for t2)


426 
 subst_for (Abs (_, _, t')) = subst_for t'


427 
 subst_for _ = NONE;


428 
in


429 
(case subst_for target of


430 
SOME subst => Envir.subst_term_types subst target


431 
 NONE => raise Type.TYPE_MATCH)


432 
end;


433 


434 
datatype card = One  Fin  Fin_or_Inf  Inf


435 


436 
(* Similar to "ATP_Util.tiny_card_of_type". *)


437 
fun card_of_type ctxt =


438 
let


439 
fun max_card Inf _ = Inf


440 
 max_card _ Inf = Inf


441 
 max_card Fin_or_Inf _ = Fin_or_Inf


442 
 max_card _ Fin_or_Inf = Fin_or_Inf


443 
 max_card Fin _ = Fin


444 
 max_card _ Fin = Fin


445 
 max_card One One = One;


446 


447 
fun card_of avoid T =


448 
if member (op =) avoid T then


449 
Inf


450 
else


451 
(case T of


452 
TFree _ => Fin_or_Inf


453 
 TVar _ => Inf


454 
 Type (@{type_name fun}, [T1, T2]) =>


455 
(case (card_of avoid T1, card_of avoid T2) of


456 
(_, One) => One


457 
 (k1, k2) => max_card k1 k2)


458 
 Type (@{type_name prod}, [T1, T2]) =>


459 
(case (card_of avoid T1, card_of avoid T2) of


460 
(k1, k2) => max_card k1 k2)


461 
 Type (@{type_name set}, [T']) => card_of avoid (T' > HOLogic.boolT)


462 
 Type (T_name, Ts) =>


463 
(case try (mutual_co_datatypes_of ctxt) (T_name, Ts) of


464 
NONE => Inf


465 
 SOME (_, fpTs, ctrss) =>


466 
(case ctrss of [[_]] => One  _ => Fin)


467 
> fold (fold (fold (max_card o card_of (fpTs @ avoid)) o binder_types o fastype_of))


468 
ctrss));


469 
in


470 
card_of []


471 
end;


472 


473 
fun int_of_classif Spec_Rules.Equational = 1


474 
 int_of_classif Spec_Rules.Inductive = 2


475 
 int_of_classif Spec_Rules.Co_Inductive = 3


476 
 int_of_classif Spec_Rules.Unknown = 4;


477 


478 
val classif_ord = int_ord o apply2 int_of_classif;


479 


480 
fun spec_rules_of ctxt (x as (s, T)) =


481 
let


482 
val thy = Proof_Context.theory_of ctxt;


483 


484 
fun subst_of t0 =


485 
try (Sign.typ_match thy (fastype_of t0, T)) Vartab.empty;


486 


487 
fun process_spec _ (res as SOME _) = res


488 
 process_spec (classif, (ts0, ths as _ :: _)) NONE =


489 
(case get_first subst_of ts0 of


490 
SOME subst =>


491 
(let


492 
val ts = map (Envir.subst_term_types subst) ts0;


493 
val poly_props = map Thm.prop_of ths;


494 
val props = map (instantiate_constant_types_in_term ctxt ts) poly_props;


495 
in


496 
if exists (exists (exists_type (exists_subtype is_TVar))) [ts, props] then NONE


497 
else SOME (classif, ts, props, poly_props)


498 
end


499 
handle Type.TYPE_MATCH => NONE)


500 
 NONE => NONE)


501 
 process_spec _ NONE = NONE;


502 


503 
fun spec_rules () =


504 
Spec_Rules.retrieve ctxt (Const x)


505 
> sort (classif_ord o apply2 fst);


506 


507 
val specs =


508 
if s = @{const_name The} then


509 
[(Spec_Rules.Unknown, ([Logic.varify_global @{term The}], [@{thm theI_unique}]))]


510 
else if s = @{const_name finite} then


511 
let val card = card_of_type ctxt T in


512 
if card = Inf orelse card = Fin_or_Inf then


513 
spec_rules ()


514 
else


515 
[(Spec_Rules.Equational, ([Logic.varify_global @{term finite}],


516 
[Skip_Proof.make_thm thy (Logic.varify_global @{prop "finite A = True"})]))]


517 
end


518 
else


519 
spec_rules ();


520 
in


521 
fold process_spec specs NONE


522 
end;


523 


524 
fun lhs_of_equation (Const (@{const_name Pure.eq}, _) $ t $ _) = t


525 
 lhs_of_equation (@{const Trueprop} $ (Const (@{const_name HOL.eq}, _) $ t $ _)) = t;


526 


527 
fun specialize_definition_type thy x def0 =


528 
let


529 
val def = specialize_type thy x def0;


530 
val lhs = lhs_of_equation def;


531 
in


532 
if exists_Const (curry (op =) x) lhs then def else raise Fail "cannot specialize"


533 
end;


534 


535 
fun definition_of thy (x as (s, _)) =


536 
Defs.specifications_of (Theory.defs_of thy) (Defs.Const, s)


537 
> map_filter #def


538 
> map_filter (try (specialize_definition_type thy x o Thm.prop_of o Thm.axiom thy))


539 
> try hd;


540 


541 
fun is_builtin_theory thy_id =


542 
Context.subthy_id (thy_id, Context.theory_id @{theory Hilbert_Choice});


543 


544 
val orphan_axioms_of =


545 
Spec_Rules.get


546 
#> filter (curry (op =) Spec_Rules.Unknown o fst)


547 
#> map snd


548 
#> filter (null o fst)


549 
#> maps snd


550 
#> filter_out (is_builtin_theory o Thm.theory_id_of_thm)


551 
#> map Thm.prop_of;


552 


553 
fun keys_of _ (ITVal (T, _)) = [key_of_typ T]


554 
 keys_of _ (ICopy {abs_typ, ...}) = [key_of_typ abs_typ]


555 
 keys_of _ (IQuotient {abs_typ, ...}) = [key_of_typ abs_typ]


556 
 keys_of _ (ICoData (_, specs)) = map (key_of_typ o #typ) specs


557 
 keys_of ctxt (IVal const) = [key_of_const ctxt const]


558 
 keys_of ctxt (ICoPred (_, _, specs)) = map (key_of_const ctxt o #const) specs


559 
 keys_of ctxt (IRec specs) = map (key_of_const ctxt o #const) specs


560 
 keys_of ctxt (ISpec {consts, ...}) = map (key_of_const ctxt) consts


561 
 keys_of _ (IAxiom _) = []


562 
 keys_of _ (IGoal _) = []


563 
 keys_of _ (IEval _) = [];


564 


565 
fun co_data_spec_deps_of ctxt ({ctrs, ...} : isa_co_data_spec) =


566 
fold (add_keys ctxt) ctrs [];


567 
fun const_spec_deps_of ctxt consts props =


568 
fold (add_keys ctxt) props [] > subtract (op =) (map (key_of_const ctxt) consts);


569 
fun consts_spec_deps_of ctxt {consts, props} =


570 
fold (add_keys ctxt) props [] > subtract (op =) (map (key_of_const ctxt) consts);


571 


572 
fun deps_of _ (ITVal _) = []


573 
 deps_of ctxt (ICopy {wrt, ...}) = add_keys ctxt wrt []


574 
 deps_of ctxt (IQuotient {wrt, ...}) = add_keys ctxt wrt []


575 
 deps_of ctxt (ICoData (_, specs)) = maps (co_data_spec_deps_of ctxt) specs


576 
 deps_of _ (IVal const) = add_type_keys (fastype_of const) []


577 
 deps_of ctxt (ICoPred (_, _, specs)) =


578 
maps (const_spec_deps_of ctxt (map #const specs) o #props) specs


579 
 deps_of ctxt (IRec specs) = maps (const_spec_deps_of ctxt (map #const specs) o #props) specs


580 
 deps_of ctxt (ISpec spec) = consts_spec_deps_of ctxt spec


581 
 deps_of ctxt (IAxiom prop) = add_keys ctxt prop []


582 
 deps_of ctxt (IGoal prop) = add_keys ctxt prop []


583 
 deps_of ctxt (IEval t) = add_keys ctxt t [];


584 


585 
fun consts_of_rec_or_spec (IRec specs) = map #const specs


586 
 consts_of_rec_or_spec (ISpec {consts, ...}) = consts;


587 


588 
fun props_of_rec_or_spec (IRec specs) = maps #props specs


589 
 props_of_rec_or_spec (ISpec {props, ...}) = props;


590 


591 
fun merge_two_rec_or_spec cmd cmd' =


592 
ISpec {consts = consts_of_rec_or_spec cmd @ consts_of_rec_or_spec cmd',


593 
props = props_of_rec_or_spec cmd @ props_of_rec_or_spec cmd'};


594 


595 
fun merge_two (ICoData (fp, specs)) (ICoData (fp', specs'), complete) =


596 
(ICoData (BNF_Util.case_fp fp fp fp', specs @ specs'), complete andalso fp = fp')


597 
 merge_two (IRec specs) (IRec specs', complete) = (IRec (specs @ specs'), complete)


598 
 merge_two (cmd as IRec _) (cmd' as ISpec _, complete) =


599 
(merge_two_rec_or_spec cmd cmd', complete)


600 
 merge_two (cmd as ISpec _) (cmd' as IRec _, complete) =


601 
(merge_two_rec_or_spec cmd cmd', complete)


602 
 merge_two (cmd as ISpec _) (cmd' as ISpec _, complete) =


603 
(merge_two_rec_or_spec cmd cmd', complete)


604 
 merge_two _ _ = raise CYCLIC_DEPS ();


605 


606 
fun sort_isa_commands_topologically ctxt cmds =


607 
let


608 
fun normal_pairs [] = []


609 
 normal_pairs (all as normal :: _) = map (rpair normal) all;


610 


611 
fun add_node [] _ = I


612 
 add_node (normal :: _) cmd = Graph.new_node (normal, cmd);


613 


614 
fun merge_scc (cmd :: cmds) complete = fold merge_two cmds (cmd, complete);


615 


616 
fun sort_problem (cmds, complete) =


617 
let


618 
val keyss = map (keys_of ctxt) cmds;


619 
val normal_keys = Symtab.make (maps normal_pairs keyss);


620 
val normalize = Symtab.lookup normal_keys;


621 


622 
fun add_deps [] _ = I


623 
 add_deps (normal :: _) cmd =


624 
let


625 
val deps = deps_of ctxt cmd


626 
> map_filter normalize


627 
> remove (op =) normal;


628 
in


629 
fold (fn dep => Graph.add_edge (dep, normal)) deps


630 
end;


631 


632 
val cmd_of_key = the o AList.lookup (op =) (map hd keyss ~~ cmds);


633 


634 
val G = Graph.empty


635 
> fold2 add_node keyss cmds


636 
> fold2 add_deps keyss cmds;


637 


638 
val cmd_sccs = rev (Graph.strong_conn G)


639 
> map (map cmd_of_key);


640 
in


641 
if exists (can (fn _ :: _ :: _ => ())) cmd_sccs then


642 
sort_problem (fold_map merge_scc cmd_sccs complete)


643 
else


644 
(Graph.schedule (K snd) G, complete)


645 
end;


646 


647 
val typedecls = filter (can (fn ITVal _ => ())) cmds;


648 
val (mixed, complete) =


649 
(filter (can (fn ICopy _ => ()  IQuotient _ => ()  ICoData _ => ()  IVal _ => ()


650 
 ICoPred _ => ()  IRec _ => ()  ISpec _ => ())) cmds, true)


651 
> sort_problem;


652 
val axioms = filter (can (fn IAxiom _ => ())) cmds;


653 
val goals = filter (can (fn IGoal _ => ())) cmds;


654 
val evals = filter (can (fn IEval _ => ())) cmds;


655 
in


656 
(typedecls @ mixed @ axioms @ goals @ evals, complete)


657 
end;


658 


659 
fun group_of (ITVal _) = 1


660 
 group_of (ICopy _) = 2


661 
 group_of (IQuotient _) = 3


662 
 group_of (ICoData _) = 4


663 
 group_of (IVal _) = 5


664 
 group_of (ICoPred _) = 6


665 
 group_of (IRec _) = 7


666 
 group_of (ISpec _) = 8


667 
 group_of (IAxiom _) = 9


668 
 group_of (IGoal _) = 10


669 
 group_of (IEval _) = 11;


670 


671 
fun group_isa_commands [] = []


672 
 group_isa_commands [cmd] = [[cmd]]


673 
 group_isa_commands (cmd :: cmd' :: cmds) =


674 
let val (group :: groups) = group_isa_commands (cmd' :: cmds) in


675 
if group_of cmd = group_of cmd' then


676 
(cmd :: group) :: groups


677 
else


678 
[cmd] :: (group :: groups)


679 
end;


680 


681 
fun defined_by (Const (@{const_name All}, _) $ t) = defined_by t


682 
 defined_by (Abs (_, _, t)) = defined_by t


683 
 defined_by (@{const implies} $ _ $ u) = defined_by u


684 
 defined_by (Const (@{const_name HOL.eq}, _) $ t $ _) = head_of t


685 
 defined_by t = head_of t;


686 


687 
fun partition_props [_] props = SOME [props]


688 
 partition_props consts props =


689 
let


690 
val propss = map (fn const => filter (fn prop => defined_by prop aconv const) props) consts;


691 
in


692 
if eq_set (op aconv) (props, flat propss) andalso forall (not o null) propss then SOME propss


693 
else NONE


694 
end;


695 


696 
fun hol_concl_head (Const (@{const_name All}, _) $ Abs (_, _, t)) = hol_concl_head t


697 
 hol_concl_head (Const (@{const_name implies}, _) $ _ $ t) = hol_concl_head t


698 
 hol_concl_head (t $ _) = hol_concl_head t


699 
 hol_concl_head t = t;


700 


701 
fun is_inductive_set_intro t =


702 
(case hol_concl_head t of


703 
Const (@{const_name rmember}, _) => true


704 
 _ => false);


705 


706 
exception NO_TRIPLE of unit;


707 


708 
fun triple_for_intro_rule ctxt x rule =


709 
let


710 
val (prems, concl) = Logic.strip_horn rule


711 
>> map (Object_Logic.atomize_term ctxt)


712 
> Object_Logic.atomize_term ctxt;


713 


714 
val (mains, sides) = List.partition (exists_Const (curry (op =) x)) prems;


715 


716 
val is_right_head = curry (op aconv) (Const x) o head_of;


717 
in


718 
if forall is_right_head mains then (sides, mains, concl) else raise NO_TRIPLE ()


719 
end;


720 


721 
val tuple_for_args = HOLogic.mk_tuple o snd o strip_comb;


722 


723 
fun wf_constraint_for rel sides concl mains =


724 
HOLogic.mk_mem (HOLogic.mk_prod (apply2 tuple_for_args (mains, concl)), Var rel)


725 
> fold (curry HOLogic.mk_imp) sides


726 
> close_form [rel];


727 


728 
fun wf_constraint_for_triple rel (sides, mains, concl) =


729 
map (wf_constraint_for rel sides concl) mains


730 
> foldr1 HOLogic.mk_conj;


731 


732 
fun terminates_by ctxt timeout goal tac =


733 
can (SINGLE (Classical.safe_tac ctxt) #> the


734 
#> SINGLE (DETERM_TIMEOUT timeout (tac ctxt (auto_tac ctxt))) #> the


735 
#> Goal.finish ctxt) goal;


736 


737 
val max_cached_wfs = 50;


738 
val cached_timeout = Synchronized.var "Nunchaku_Collect.cached_timeout" Time.zeroTime;


739 
val cached_wf_props = Synchronized.var "Nunchaku_Collect.cached_wf_props" ([] : (term * bool) list);


740 


741 
val termination_tacs = [Lexicographic_Order.lex_order_tac true, ScnpReconstruct.sizechange_tac];


742 


743 
fun is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout const intros =


744 
let


745 
val thy = Proof_Context.theory_of ctxt;


746 


747 
val Const (x as (_, T)) = head_of (HOLogic.dest_Trueprop (Logic.strip_imp_concl (hd intros)));


748 
in


749 
(case triple_lookup (const_match thy o swap) wfs (dest_Const const) of


750 
SOME (SOME wf) => wf


751 
 _ =>


752 
(case map (triple_for_intro_rule ctxt x) intros > filter_out (null o #2) of


753 
[] => true


754 
 triples =>


755 
let


756 
val binders_T = HOLogic.mk_tupleT (binder_types T);


757 
val rel_T = HOLogic.mk_setT (HOLogic.mk_prodT (binders_T, binders_T));


758 
val j = fold (Integer.max o maxidx_of_term) intros 0 + 1;


759 
val rel = (("R", j), rel_T);


760 
val prop =


761 
Const (@{const_name wf}, rel_T > HOLogic.boolT) $ Var rel ::


762 
map (wf_constraint_for_triple rel) triples


763 
> foldr1 HOLogic.mk_conj


764 
> HOLogic.mk_Trueprop;


765 
in


766 
if debug then writeln ("Wellfoundedness goal: " ^ Syntax.string_of_term ctxt prop)


767 
else ();


768 
if wf_timeout = Synchronized.value cached_timeout andalso


769 
length (Synchronized.value cached_wf_props) < max_cached_wfs then


770 
()


771 
else


772 
(Synchronized.change cached_wf_props (K []);


773 
Synchronized.change cached_timeout (K wf_timeout));


774 
(case AList.lookup (op =) (Synchronized.value cached_wf_props) prop of


775 
SOME wf => wf


776 
 NONE =>


777 
let


778 
val goal = Goal.init (Thm.cterm_of ctxt prop);


779 
val wf = exists (terminates_by ctxt wf_timeout goal) termination_tacs;


780 
in


781 
Synchronized.change cached_wf_props (cons (prop, wf)); wf


782 
end)


783 
end)


784 
handle


785 
List.Empty => false


786 
 NO_TRIPLE () => false)


787 
end;


788 


789 
datatype lhs_pat =


790 
Only_Vars


791 
 Prim_Pattern of string


792 
 Any_Pattern;


793 


794 
fun is_likely_pat_complete ctxt props =


795 
let


796 
val is_Var_or_Bound = is_Var orf is_Bound;


797 


798 
fun lhs_pat_of t =


799 
(case t of


800 
Const (@{const_name All}, _) $ Abs (_, _, t) => lhs_pat_of t


801 
 Const (@{const_name HOL.eq}, _) $ u $ _ =>


802 
(case filter_out is_Var_or_Bound (snd (strip_comb u)) of


803 
[] => Only_Vars


804 
 [v] =>


805 
(case strip_comb v of


806 
(cst as Const (_, T), args) =>


807 
(case body_type T of


808 
Type (T_name, _) =>


809 
if can (Ctr_Sugar.dest_ctr ctxt T_name) cst andalso forall is_Var_or_Bound args then


810 
Prim_Pattern T_name


811 
else


812 
Any_Pattern


813 
 _ => Any_Pattern)


814 
 _ => Any_Pattern)


815 
 _ => Any_Pattern)


816 
 _ => Any_Pattern);


817 
in


818 
(case map lhs_pat_of props of


819 
[] => false


820 
 pats as Prim_Pattern T_name :: _ =>


821 
forall (can (fn Prim_Pattern _ => ())) pats andalso


822 
length pats = length (#ctrs (the (Ctr_Sugar.ctr_sugar_of ctxt T_name)))


823 
 pats => forall (curry (op =) Only_Vars) pats)


824 
end;


825 


826 
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)


827 
val axioms_max_depth = 255


828 


829 
fun isa_problem_of_subgoal ctxt falsify wfs whacks cards debug wf_timeout evals0 some_assms0


830 
subgoal0 =


831 
let


832 
val thy = Proof_Context.theory_of ctxt;


833 


834 
fun card_of T =


835 
(case triple_lookup (typ_match thy o swap) cards T of


836 
NONE => (NONE, NONE)


837 
 SOME (c1, c2) => (if c1 = SOME 1 then NONE else c1, c2));


838 


839 
fun axioms_of_class class =


840 
#axioms (Axclass.get_info thy class)


841 
handle ERROR _ => [];


842 


843 
fun monomorphize_class_axiom T t =


844 
(case Term.add_tvars t [] of


845 
[] => t


846 
 [(x, S)] => Envir.subst_term_types (Vartab.make [(x, (S, T))]) t);


847 


848 
fun consider_sort depth T S (seens as (seenS, seenT, seen), problem) =


849 
if member (op =) seenS S then


850 
(seens, problem)


851 
else if depth > axioms_max_depth then


852 
raise TOO_DEEP_DEPS ()


853 
else


854 
let


855 
val seenS = S :: seenS;


856 
val seens = (seenS, seenT, seen);


857 


858 
val supers = Sign.complete_sort thy S;


859 
val axioms0 = maps (map Thm.prop_of o axioms_of_class) supers;


860 
val axioms = map (preprocess_prop false ctxt whacks o monomorphize_class_axiom T) axioms0;


861 
in


862 
(seens, map IAxiom axioms @ problem)


863 
> fold (consider_term (depth + 1)) axioms


864 
end


865 
and consider_type depth T =


866 
(case T of


867 
Type (s, Ts) =>


868 
if is_type_builtin s then fold (consider_type depth) Ts


869 
else consider_non_builtin_type depth T


870 
 _ => consider_non_builtin_type depth T)


871 
and consider_non_builtin_type depth T (seens as (seenS, seenT, seen), problem) =


872 
if member (op =) seenT T then


873 
(seens, problem)


874 
else


875 
let


876 
val seenT = T :: seenT;


877 
val seens = (seenS, seenT, seen);


878 


879 
fun consider_quotient_or_copy tuple_of s =


880 
let


881 
val (T0, repT0, wrt0, abs0, rep0) = tuple_of ctxt s;


882 
val tyenv = Sign.typ_match thy (T0, T) Vartab.empty;


883 
val substT = Envir.subst_type tyenv;


884 
val subst = Envir.subst_term_types tyenv;


885 
val repT = substT repT0;


886 
val wrt = subst wrt0;


887 
val abs = subst abs0;


888 
val rep = subst rep0;


889 
in


890 
apsnd (cons (ICopy {abs_typ = T, rep_typ = repT, wrt = wrt, abs = abs,


891 
rep = rep}))


892 
#> consider_term (depth + 1) wrt


893 
end;


894 
in


895 
(seens, problem)


896 
> (case T of


897 
TFree (_, S) =>


898 
apsnd (cons (ITVal (T, card_of T)))


899 
#> consider_sort depth T S


900 
 TVar (_, S) => consider_sort depth T S


901 
 Type (s, Ts) =>


902 
fold (consider_type depth) Ts


903 
#> (case classify_type_name ctxt s of


904 
Co_Datatype =>


905 
let


906 
val (fp, fpTs, ctrss) = mutual_co_datatypes_of ctxt (s, Ts);


907 
val specs = map2 (fn T => fn ctrs => {typ = T, ctrs = ctrs}) fpTs ctrss;


908 
in


909 
(fn ((seenS, seenT, seen), problem) =>


910 
((seenS, union (op =) fpTs seenT, seen), ICoData (fp, specs) :: problem))


911 
#> fold (fold (consider_type (depth + 1) o fastype_of)) ctrss


912 
end


913 
 Quotient => consider_quotient_or_copy quotient_of s


914 
 Copy => consider_quotient_or_copy copy_of s


915 
 TVal => apsnd (cons (ITVal (T, card_of T)))))


916 
end


917 
and consider_term depth t =


918 
(case t of


919 
t1 $ t2 => fold (consider_term depth) [t1, t2]


920 
 Var (_, T) => consider_type depth T


921 
 Bound _ => I


922 
 Abs (_, T, t') =>


923 
consider_term depth t'


924 
#> consider_type depth T


925 
 _ => (fn (seens as (seenS, seenT, seen), problem) =>


926 
if member (op aconv) seen t then


927 
(seens, problem)


928 
else if depth > axioms_max_depth then


929 
raise TOO_DEEP_DEPS ()


930 
else


931 
let


932 
val seen = t :: seen;


933 
val seens = (seenS, seenT, seen);


934 
in


935 
(case t of


936 
Const (x as (s, T)) =>


937 
(if is_const_builtin s orelse is_co_datatype_ctr ctxt x orelse


938 
is_co_datatype_case ctxt x orelse is_quotient_abs ctxt x orelse


939 
is_quotient_rep ctxt x orelse is_copy_abs ctxt x orelse


940 
is_copy_rep ctxt x then


941 
(seens, problem)


942 
else if is_stale_copy_abs ctxt x orelse is_stale_copy_rep ctxt x then


943 
raise UNSUPPORTED_FUNC t


944 
else


945 
(case spec_rules_of ctxt x of


946 
SOME (classif, consts, props0, poly_props) =>


947 
let


948 
val props = map (preprocess_prop false ctxt whacks) props0;


949 


950 
fun def_or_spec () =


951 
(case definition_of thy x of


952 
SOME eq0 =>


953 
let val eq = preprocess_prop false ctxt whacks eq0 in


954 
([eq], [IRec [{const = t, props = [eq], pat_complete = true}]])


955 
end


956 
 NONE => (props, [ISpec {consts = consts, props = props}]));


957 


958 
val (props', cmds) =


959 
if null props then


960 
([], map IVal consts)


961 
else if classif = Spec_Rules.Equational then


962 
(case partition_props consts props of


963 
SOME propss =>


964 
(props,


965 
[IRec (map2 (fn const => fn props =>


966 
{const = const, props = props,


967 
pat_complete = is_likely_pat_complete ctxt props})


968 
consts propss)])


969 
 NONE => def_or_spec ())


970 
else if member (op =) [Spec_Rules.Inductive, Spec_Rules.Co_Inductive]


971 
classif then


972 
if is_inductive_set_intro (hd props) then


973 
def_or_spec ()


974 
else


975 
(case partition_props consts props of


976 
SOME propss =>


977 
(props,


978 
[ICoPred (if classif = Spec_Rules.Inductive then BNF_Util.Least_FP


979 
else BNF_Util.Greatest_FP,


980 
length consts = 1 andalso


981 
is_wellfounded_inductive_predicate ctxt wfs debug wf_timeout


982 
(the_single consts) poly_props,


983 
map2 (fn const => fn props => {const = const, props = props})


984 
consts propss)])


985 
 NONE => def_or_spec ())


986 
else


987 
def_or_spec ();


988 
in


989 
((seenS, seenT, union (op aconv) consts seen), cmds @ problem)


990 
> fold (consider_term (depth + 1)) props'


991 
end


992 
 NONE =>


993 
(case definition_of thy x of


994 
SOME eq0 =>


995 
let val eq = preprocess_prop false ctxt whacks eq0 in


996 
(seens, IRec [{const = t, props = [eq], pat_complete = true}] :: problem)


997 
> consider_term (depth + 1) eq


998 
end


999 
 NONE => (seens, IVal t :: problem))))


1000 
> consider_type depth T


1001 
 Free (_, T) =>


1002 
(seens, IVal t :: problem)


1003 
> consider_type depth T)


1004 
end));


1005 


1006 
val (poly_axioms, mono_axioms0) = orphan_axioms_of ctxt


1007 
> List.partition has_polymorphism;


1008 


1009 
fun implicit_evals_of pol (@{const Not} $ t) = implicit_evals_of (not pol) t


1010 
 implicit_evals_of pol (@{const implies} $ t $ u) =


1011 
(case implicit_evals_of pol u of


1012 
[] => implicit_evals_of (not pol) t


1013 
 ts => ts)


1014 
 implicit_evals_of pol (@{const conj} $ t $ u) =


1015 
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)


1016 
 implicit_evals_of pol (@{const disj} $ t $ u) =


1017 
union (op aconv) (implicit_evals_of pol t) (implicit_evals_of pol u)


1018 
 implicit_evals_of false (Const (@{const_name HOL.eq}, _) $ t $ u) =


1019 
distinct (op aconv) [t, u]


1020 
 implicit_evals_of true (Const (@{const_name HOL.eq}, _) $ t $ _) = [t]


1021 
 implicit_evals_of _ _ = [];


1022 


1023 
val mono_axioms_and_some_assms =


1024 
map (preprocess_prop false ctxt whacks) (mono_axioms0 @ some_assms0);


1025 
val subgoal = preprocess_prop falsify ctxt whacks subgoal0;


1026 
val implicit_evals = implicit_evals_of true subgoal;


1027 
val evals = map (preprocess_closed_term ctxt whacks) evals0;


1028 
val seens = ([], [], []);


1029 


1030 
val (commandss, complete) =


1031 
(seens,


1032 
map IAxiom mono_axioms_and_some_assms @ [IGoal subgoal] @ map IEval (implicit_evals @ evals))


1033 
> fold (consider_term 0) (subgoal :: evals @ mono_axioms_and_some_assms)


1034 
> snd


1035 
> rev (* prettier *)


1036 
> sort_isa_commands_topologically ctxt


1037 
>> group_isa_commands;


1038 
in


1039 
(poly_axioms, {commandss = commandss, sound = true, complete = complete})


1040 
end;


1041 


1042 
fun add_pat_complete_of_command cmd =


1043 
(case cmd of


1044 
ICoPred (_, _, specs) => union (op =) (map #const specs)


1045 
 IRec specs =>


1046 
union (op =) (map_filter (try (fn {const, pat_complete = true, ...} => const)) specs)


1047 
 _ => I);


1048 


1049 
fun pat_completes_of_isa_problem {commandss, ...} =


1050 
fold (fold add_pat_complete_of_command) commandss [];


1051 


1052 
fun str_of_isa_term_with_type ctxt t =


1053 
Syntax.string_of_term ctxt t ^ " : " ^ Syntax.string_of_typ ctxt (fastype_of t);


1054 


1055 
fun is_triv_wrt (Abs (_, _, body)) = is_triv_wrt body


1056 
 is_triv_wrt @{const True} = true


1057 
 is_triv_wrt _ = false;


1058 


1059 
fun str_of_isa_type_spec ctxt {abs_typ, rep_typ, wrt, abs, rep} =


1060 
Syntax.string_of_typ ctxt abs_typ ^ " := " ^ Syntax.string_of_typ ctxt rep_typ ^


1061 
(if is_triv_wrt wrt then "" else "\n wrt " ^ Syntax.string_of_term ctxt wrt) ^


1062 
"\n abstract " ^ Syntax.string_of_term ctxt abs ^


1063 
"\n concrete " ^ Syntax.string_of_term ctxt rep;


1064 


1065 
fun str_of_isa_co_data_spec ctxt {typ, ctrs} =


1066 
Syntax.string_of_typ ctxt typ ^ " :=\n " ^


1067 
space_implode "\n " (map (str_of_isa_term_with_type ctxt) ctrs);


1068 


1069 
fun str_of_isa_const_spec ctxt {const, props} =


1070 
str_of_isa_term_with_type ctxt const ^ " :=\n " ^


1071 
space_implode ";\n " (map (Syntax.string_of_term ctxt) props);


1072 


1073 
fun str_of_isa_rec_spec ctxt {const, props, pat_complete} =


1074 
str_of_isa_term_with_type ctxt const ^ (if pat_complete then " [pat_complete]" else "") ^


1075 
" :=\n " ^ space_implode ";\n " (map (Syntax.string_of_term ctxt) props);


1076 


1077 
fun str_of_isa_consts_spec ctxt {consts, props} =


1078 
space_implode " and\n " (map (str_of_isa_term_with_type ctxt) consts) ^ " :=\n " ^


1079 
space_implode ";\n " (map (Syntax.string_of_term ctxt) props);


1080 


1081 
fun str_of_isa_card NONE = ""


1082 
 str_of_isa_card (SOME k) = signed_string_of_int k;


1083 


1084 
fun str_of_isa_cards_suffix (NONE, NONE) = ""


1085 
 str_of_isa_cards_suffix (c1, c2) = " " ^ str_of_isa_card c1 ^ "" ^ str_of_isa_card c2;


1086 


1087 
fun str_of_isa_command ctxt (ITVal (T, cards)) =


1088 
"type " ^ Syntax.string_of_typ ctxt T ^ str_of_isa_cards_suffix cards


1089 
 str_of_isa_command ctxt (ICopy spec) = "copy " ^ str_of_isa_type_spec ctxt spec


1090 
 str_of_isa_command ctxt (IQuotient spec) = "quotient " ^ str_of_isa_type_spec ctxt spec


1091 
 str_of_isa_command ctxt (ICoData (fp, specs)) =


1092 
BNF_Util.case_fp fp "data" "codata" ^ " " ^ str_of_and_list (str_of_isa_co_data_spec ctxt) specs


1093 
 str_of_isa_command ctxt (IVal t) = "val " ^ str_of_isa_term_with_type ctxt t


1094 
 str_of_isa_command ctxt (ICoPred (fp, wf, specs)) =


1095 
BNF_Util.case_fp fp "pred" "copred" ^ " " ^ (if wf then "[wf] " else "") ^


1096 
str_of_and_list (str_of_isa_const_spec ctxt) specs


1097 
 str_of_isa_command ctxt (IRec specs) = "rec " ^ str_of_and_list (str_of_isa_rec_spec ctxt) specs


1098 
 str_of_isa_command ctxt (ISpec spec) = "spec " ^ str_of_isa_consts_spec ctxt spec


1099 
 str_of_isa_command ctxt (IAxiom prop) = "axiom " ^ Syntax.string_of_term ctxt prop


1100 
 str_of_isa_command ctxt (IGoal prop) = "goal " ^ Syntax.string_of_term ctxt prop


1101 
 str_of_isa_command ctxt (IEval t) = "eval " ^ Syntax.string_of_term ctxt t;


1102 


1103 
fun str_of_isa_problem ctxt {commandss, sound, complete} =


1104 
map (cat_lines o map (suffix "." o str_of_isa_command ctxt)) commandss


1105 
> space_implode "\n\n" > suffix "\n"


1106 
> prefix ("# " ^ (if sound then "sound" else "unsound") ^ "\n")


1107 
> prefix ("# " ^ (if complete then "complete" else "incomplete") ^ "\n");


1108 


1109 
end;
