wneuper/isa: comparison src/HOL/Tools/ATP/atp_problem

equal deleted inserted replaced

-:9aa0fad4e864
+:a5ab5964065f
 fun make_all_bound_var x = all_bound_var_prefix ^ ascii_of x
 fun make_exist_bound_var x = exist_bound_var_prefix ^ ascii_of x
 fun make_schematic_var v = schematic_var_prefix ^ ascii_of_indexname v
 fun make_fixed_var x = fixed_var_prefix ^ ascii_of x
-fun make_schematic_type_var (x, i) =
+fun make_tvar (s, i) = tvar_prefix ^ (ascii_of_indexname (unprefix "'" s, i))
-tvar_prefix ^ (ascii_of_indexname (unprefix "'" x, i))
+fun make_tfree s = tfree_prefix ^ (ascii_of (unprefix "'" s))
-fun make_fixed_type_var x = tfree_prefix ^ (ascii_of (unprefix "'" x))
+fun tvar_name (x as (s, _)) = (make_tvar x, s)
 (* "HOL.eq" and choice are mapped to the ATP's equivalents *)
 local
 val choice_const = (fst o dest_Const o HOLogic.choice_const) Term.dummyT
 fun default c = const_prefix ^ lookup_const c
 not (member (op =) atp_monomorph_bad_consts s)
 ? add_schematic_const x
 | _ => I)
 fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
+val tvar_a_str = "'a"
+val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
+val tvar_a_name = tvar_name (tvar_a_str, 0)
+val itself_name = `make_fixed_type_const @{type_name itself}
+val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
+val tvar_a_atype = AType (tvar_a_name, [])
+val a_itself_atype = AType (itself_name, [tvar_a_atype])
 (** Definitions and functions for FOL clauses and formulas for TPTP **)
 (** Isabelle arities **)
-type arity_atom = name * name * name list
 val type_class = the_single @{sort type}
 type arity_clause =
 {name : string,
-prem_atoms : arity_atom list,
+prems : (string * typ) list,
-concl_atom : arity_atom}
+concl : string * typ}
-fun add_prem_atom tvar =
+fun add_prem_atom T = fold (fn s => s <> type_class ? cons (s, T))
-fold (fn s => s <> type_class ? cons (`make_type_class s, `I tvar, []))
 (* Arity of type constructor "tcon :: (arg1, ..., argN) res" *)
-fun make_axiom_arity_clause (tcons, name, (cls, args)) =
+fun make_axiom_arity_clause (tc, name, (class, args)) =
 let
-val tvars = map (prefix tvar_prefix o string_of_int) (1 upto length args)
+val tvars =
-val tvars_srts = ListPair.zip (tvars, args)
+map (fn j => TVar ((tvar_a_str, j), @{sort HOL.type}))
+(1 upto length args)
 in
-{name = name,
+{name = name, prems = fold (uncurry add_prem_atom) (tvars ~~ args) [],
-prem_atoms = [] |> fold (uncurry add_prem_atom) tvars_srts,
+concl = (class, Type (tc, tvars))}
-concl_atom = (`make_type_class cls, `make_fixed_type_const tcons,
-tvars ~~ tvars)}
 end
 fun arity_clause _ _ (_, []) = []
 | arity_clause seen n (tcons, ("HOL.type", _) :: ars) =  (* ignore *)
 arity_clause seen n (tcons, ars)
 (** Isabelle class relations **)
 type class_rel_clause =
 {name : string,
-subclass : name,
+subclass : string,
-superclass : name}
+superclass : string}
 (* Generate all pairs (sub, super) such that sub is a proper subclass of super
 in theory "thy". *)
 fun class_pairs _ [] _ = []
 | class_pairs thy subs supers =
 fun add_super sub super = class_less (sub, super) ? cons (sub, super)
 fun add_supers sub = fold (add_super sub) supers
 in fold add_supers subs [] end
 fun make_class_rel_clause (sub, super) =
-{name = sub ^ "_" ^ super, subclass = `make_type_class sub,
+{name = sub ^ "_" ^ super, subclass = sub, superclass = super}
-superclass = `make_type_class super}
 fun make_class_rel_clauses thy subs supers =
 map make_class_rel_clause (class_pairs thy subs supers)
 (* intermediate terms *)
 fun stripc (IApp (t, u), ts) = stripc (t, u :: ts)
 | stripc x = x
 in stripc (u, []) end
 fun atomic_types_of T = fold_atyps (insert (op =)) T []
-val tvar_a_str = "'a"
-val tvar_a = TVar ((tvar_a_str, 0), HOLogic.typeS)
-val tvar_a_name = (make_schematic_type_var (tvar_a_str, 0), tvar_a_str)
-val itself_name = `make_fixed_type_const @{type_name itself}
-val TYPE_name = `(make_fixed_const NONE) @{const_name TYPE}
-val tvar_a_atype = AType (tvar_a_name, [])
-val a_itself_atype = AType (itself_name, [tvar_a_atype])
 fun new_skolem_const_name s num_T_args =
 [new_skolem_const_prefix, s, string_of_int num_T_args]
 |> Long_Name.implode
 else
 All_Type_Args
 end
 end
-(* Make atoms for sorted type variables. *)
-fun generic_add_sorts_on_type (_, []) = I
-| generic_add_sorts_on_type ((x, i), s :: ss) =
-generic_add_sorts_on_type ((x, i), ss)
-#> (if s = the_single @{sort HOL.type} then
-I
-else if i = ~1 then
-insert (op =) (`make_type_class s, `make_fixed_type_var x)
-else
-insert (op =) (`make_type_class s,
-(make_schematic_type_var (x, i), x)))
-fun add_sorts_on_tfree (TFree (s, S)) = generic_add_sorts_on_type ((s, ~1), S)
-| add_sorts_on_tfree _ = I
-fun add_sorts_on_tvar (TVar z) = generic_add_sorts_on_type z
-| add_sorts_on_tvar _ = I
-fun type_class_formula type_enc class arg =
-AAtom (ATerm ((class, []), arg ::
-(case type_enc of
-Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
-[ATerm ((TYPE_name, []), [arg])]
-| _ => [])))
-fun formulas_for_types type_enc add_sorts_on_typ Ts =
-[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
-|> map (fn (class, name) =>
-type_class_formula type_enc class (ATerm ((name, []), [])))
-fun mk_aconns c phis =
-let val (phis', phi') = split_last phis in
-fold_rev (mk_aconn c) phis' phi'
-end
-fun mk_ahorn [] phi = phi
-| mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
-fun mk_aquant _ [] phi = phi
-| mk_aquant q xs (phi as AQuant (q', xs', phi')) =
-if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
-| mk_aquant q xs phi = AQuant (q, xs, phi)
-fun close_universally add_term_vars phi =
-let
-fun add_formula_vars bounds (AQuant (_, xs, phi)) =
-add_formula_vars (map fst xs @ bounds) phi
-| add_formula_vars bounds (AConn (_, phis)) =
-fold (add_formula_vars bounds) phis
-| add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
-in mk_aquant AForall (add_formula_vars [] phi []) phi end
-fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
-(if is_tptp_variable s andalso
-not (String.isPrefix tvar_prefix s) andalso
-not (member (op =) bounds name) then
-insert (op =) (name, NONE)
-else
-I)
-#> fold (add_term_vars bounds) tms
-| add_term_vars bounds (AAbs (((name, _), tm), args)) =
-add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
-fun close_formula_universally phi = close_universally add_term_vars phi
-fun add_iterm_vars bounds (IApp (tm1, tm2)) =
-fold (add_iterm_vars bounds) [tm1, tm2]
-| add_iterm_vars _ (IConst _) = I
-| add_iterm_vars bounds (IVar (name, T)) =
-not (member (op =) bounds name) ? insert (op =) (name, SOME T)
-| add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
-fun close_iformula_universally phi = close_universally add_iterm_vars phi
 val fused_infinite_type_name = "ATP.fused_inf" (* shouldn't clash *)
 val fused_infinite_type = Type (fused_infinite_type_name, [])
-fun tvar_name (x as (s, _)) = (make_schematic_type_var x, s)
 fun ho_term_from_typ type_enc =
 let
 fun term (Type (s, Ts)) =
 ATerm ((case (is_type_enc_higher_order type_enc, s) of
 is_type_enc_native type_enc then
 `I tptp_individual_type
 else
 `make_fixed_type_const s,
 []), map term Ts)
-| term (TFree (s, _)) = ATerm ((`make_fixed_type_var s, []), [])
+| term (TFree (s, _)) = ATerm ((`make_tfree s, []), [])
 | term (TVar (x, _)) = ATerm ((tvar_name x, []), [])
 in term end
 fun ho_term_for_type_arg type_enc T =
 if T = dummyT then NONE else SOME (ho_term_from_typ type_enc T)
 in if is_type_enc_higher_order type_enc then to_ho else to_fo ary end
 fun ho_type_from_typ type_enc pred_sym ary =
 ho_type_from_ho_term type_enc pred_sym ary
 o ho_term_from_typ type_enc
+(* Make atoms for sorted type variables. *)
+fun generic_add_sorts_on_type _ [] = I
+| generic_add_sorts_on_type T (s :: ss) =
+generic_add_sorts_on_type T ss
+#> (if s = the_single @{sort HOL.type} then I else insert (op =) (s, T))
+fun add_sorts_on_tfree (T as TFree (_, S)) = generic_add_sorts_on_type T S
+| add_sorts_on_tfree _ = I
+fun add_sorts_on_tvar (T as TVar (_, S)) = generic_add_sorts_on_type T S
+| add_sorts_on_tvar _ = I
+fun process_type_args type_enc T_args =
+if is_type_enc_native type_enc then
+(map (ho_type_from_typ type_enc false 0) T_args, [])
+else
+([], map_filter (ho_term_for_type_arg type_enc) T_args)
+fun type_class_atom type_enc (class, T) =
+let
+val class = `make_type_class class
+val (ty_args, tm_args) = process_type_args type_enc [T]
+val tm_args =
+tm_args @
+(case type_enc of
+Native (First_Order, Raw_Polymorphic Without_Phantom_Type_Vars, _) =>
+[ATerm ((TYPE_name, ty_args), [])]
+| _ => [])
+in AAtom (ATerm ((class, ty_args), tm_args)) end
+fun formulas_for_types type_enc add_sorts_on_typ Ts =
+[] |> level_of_type_enc type_enc <> No_Types ? fold add_sorts_on_typ Ts
+|> map (type_class_atom type_enc)
+fun mk_aconns c phis =
+let val (phis', phi') = split_last phis in
+fold_rev (mk_aconn c) phis' phi'
+end
+fun mk_ahorn [] phi = phi
+| mk_ahorn phis psi = AConn (AImplies, [mk_aconns AAnd phis, psi])
+fun mk_aquant _ [] phi = phi
+| mk_aquant q xs (phi as AQuant (q', xs', phi')) =
+if q = q' then AQuant (q, xs @ xs', phi') else AQuant (q, xs, phi)
+| mk_aquant q xs phi = AQuant (q, xs, phi)
+fun mk_atyquant _ [] phi = phi
+| mk_atyquant q xs (phi as ATyQuant (q', xs', phi')) =
+if q = q' then ATyQuant (q, xs @ xs', phi') else ATyQuant (q, xs, phi)
+| mk_atyquant q xs phi = ATyQuant (q, xs, phi)
+fun close_universally add_term_vars phi =
+let
+fun add_formula_vars bounds (ATyQuant (_, _, phi)) =
+add_formula_vars bounds phi
+| add_formula_vars bounds (AQuant (_, xs, phi)) =
+add_formula_vars (map fst xs @ bounds) phi
+| add_formula_vars bounds (AConn (_, phis)) =
+fold (add_formula_vars bounds) phis
+| add_formula_vars bounds (AAtom tm) = add_term_vars bounds tm
+in mk_aquant AForall (add_formula_vars [] phi []) phi end
+fun add_term_vars bounds (ATerm ((name as (s, _), _), tms)) =
+(if is_tptp_variable s andalso
+not (String.isPrefix tvar_prefix s) andalso
+not (member (op =) bounds name) then
+insert (op =) (name, NONE)
+else
+I)
+#> fold (add_term_vars bounds) tms
+| add_term_vars bounds (AAbs (((name, _), tm), args)) =
+add_term_vars (name :: bounds) tm #> fold (add_term_vars bounds) args
+fun close_formula_universally phi = close_universally add_term_vars phi
+fun add_iterm_vars bounds (IApp (tm1, tm2)) =
+fold (add_iterm_vars bounds) [tm1, tm2]
+| add_iterm_vars _ (IConst _) = I
+| add_iterm_vars bounds (IVar (name, T)) =
+not (member (op =) bounds name) ? insert (op =) (name, SOME T)
+| add_iterm_vars bounds (IAbs (_, tm)) = add_iterm_vars bounds tm
+fun close_iformula_universally phi = close_universally add_iterm_vars phi
 fun aliased_uncurried ary (s, s') =
 (s ^ ascii_of_uncurried_alias_sep ^ string_of_int ary, s' ^ string_of_int ary)
 fun unaliased_uncurried (s, s') =
 case space_explode uncurried_alias_sep s of
 @{thms fAll_table fComp_law fAll_law fEx_law} |> map (pair Def)),
 (("fEx", false),
 @{thms fEx_table fComp_law fAll_law fEx_law} |> map (pair Def))]
 |> map (apsnd (map (apsnd zero_var_indexes)))
-fun atype_of_type_vars (Native (_, Raw_Polymorphic _, _)) = SOME atype_of_types
-| atype_of_type_vars (Native (_, Type_Class_Polymorphic, _)) =
-SOME atype_of_types (* ### FIXME *)
-| atype_of_type_vars _ = NONE
 fun bound_tvars type_enc sorts Ts =
-(sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
+case filter is_TVar Ts of
-#> mk_aquant AForall
+[] => I
-(map_filter (fn TVar (x as (s, _), _) =>
+| Ts =>
-SOME ((make_schematic_type_var x, s),
+(sorts ? mk_ahorn (formulas_for_types type_enc add_sorts_on_tvar Ts))
-atype_of_type_vars type_enc)
+#> (if is_type_enc_native type_enc then
-| _ => NONE) Ts)
+mk_atyquant AForall
+(map (fn TVar (x, _) => AType (tvar_name x, [])) Ts)
+else
+mk_aquant AForall (map (fn TVar (x, _) => (tvar_name x, NONE)) Ts))
 fun eq_formula type_enc atomic_Ts bounds pred_sym tm1 tm2 =
 (if pred_sym then AConn (AIff, [AAtom tm1, AAtom tm2])
 else AAtom (ATerm ((`I tptp_equal, []), [tm1, tm2])))
 |> mk_aquant AForall bounds
 granularity_of_type_level level <> All_Vars andalso
 should_encode_type ctxt mono level T
 | should_generate_tag_bound_decl _ _ _ _ _ = false
 fun mk_aterm type_enc name T_args args =
-(* ### FIXME
+let val (ty_args, tm_args) = process_type_args type_enc T_args in
-if is_type_enc_polymorphic type_enc then
+ATerm ((name, ty_args), tm_args @ args)
-ATerm ((name, map (ho_type_from_typ type_enc false 0) T_args), args)
+end
-else *)
-ATerm ((name, []), map_filter (ho_term_for_type_arg type_enc) T_args @ args)
 fun do_bound_type ctxt mono type_enc =
 case type_enc of
 Native (_, _, level) =>
 fused_type ctxt mono level 0 #> ho_type_from_typ type_enc false 0 #> SOME
 in map (term arg_site) args |> mk_aterm type_enc name T_args end
 | IVar (name, _) =>
 map (term Elsewhere) args |> mk_aterm type_enc name []
 | IAbs ((name, T), tm) =>
 if is_type_enc_higher_order type_enc then
-AAbs (((name, ho_type_from_typ type_enc true 0 T),
+AAbs (((name, ho_type_from_typ type_enc true (* FIXME? why "true"? *) 0 T),
 term Elsewhere tm), map (term Elsewhere) args)
 else
 raise Fail "unexpected lambda-abstraction"
 | IApp _ => raise Fail "impossible \"IApp\""
 val T = ityp_of u
 val var = ATerm ((name, []), [])
 val tagged_var = tag_with_type ctxt mono type_enc pos T var
 in SOME (AAtom (ATerm ((`I tptp_equal, []), [tagged_var, var]))) end
 else
 NONE
-fun do_formula pos (AQuant (q, xs, phi)) =
+fun do_formula pos (ATyQuant (q, xs, phi)) =
+ATyQuant (q, map (ho_type_from_typ type_enc false 0) xs,
+do_formula pos phi)
+| do_formula pos (AQuant (q, xs, phi)) =
 let
 val phi = phi |> do_formula pos
 val universal = Option.map (q = AExists ? not) pos
 val do_bound_type = do_bound_type ctxt mono type_enc
 in
 end)
 |> Formula
 fun formula_line_for_class_rel_clause type_enc
 ({name, subclass, superclass, ...} : class_rel_clause) =
-let val ty_arg = ATerm ((tvar_a_name, []), []) in
+Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
-Formula (class_rel_clause_prefix ^ ascii_of name, Axiom,
+AConn (AImplies,
-AConn (AImplies,
+[type_class_atom type_enc (subclass, tvar_a),
-[type_class_formula type_enc subclass ty_arg,
+type_class_atom type_enc (superclass, tvar_a)])
-type_class_formula type_enc superclass ty_arg])
+|> bound_tvars type_enc false [tvar_a],
-|> mk_aquant AForall
+NONE, isabelle_info inductiveN helper_rank)
-[(tvar_a_name, atype_of_type_vars type_enc)],
+fun formula_line_for_arity_clause type_enc
+({name, prems, concl} : arity_clause) =
+let
+val atomic_Ts = fold (fold_atyps (insert (op =)) o snd) (concl :: prems) []
+in
+Formula (arity_clause_prefix ^ name, Axiom,
+mk_ahorn (map (type_class_atom type_enc) prems)
+(type_class_atom type_enc concl)
+|> bound_tvars type_enc true atomic_Ts,
 NONE, isabelle_info inductiveN helper_rank)
 end
-fun formula_from_arity_atom type_enc (class, t, args) =
-ATerm ((t, []), map (fn arg => ATerm ((arg, []), [])) args)
-|> type_class_formula type_enc class
-fun formula_line_for_arity_clause type_enc
-({name, prem_atoms, concl_atom} : arity_clause) =
-Formula (arity_clause_prefix ^ name, Axiom,
-mk_ahorn (map (formula_from_arity_atom type_enc) prem_atoms)
-(formula_from_arity_atom type_enc concl_atom)
-|> mk_aquant AForall
-(map (rpair (atype_of_type_vars type_enc)) (#3 concl_atom)),
-NONE, isabelle_info inductiveN helper_rank)
 fun formula_line_for_conjecture ctxt mono type_enc
 ({name, role, iformula, atomic_types, ...} : ifact) =
 Formula (conjecture_prefix ^ name, role,
 iformula
 |> formula_from_iformula ctxt mono type_enc
 should_guard_var_in_formula (SOME false)
 |> close_formula_universally
 |> bound_tvars type_enc true atomic_types, NONE, [])
-fun type_enc_needs_free_types (Native (_, Raw_Polymorphic _, _)) = true
-| type_enc_needs_free_types (Native _) = false
-| type_enc_needs_free_types _ = true
-fun formula_line_for_free_type j phi =
-Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
 fun formula_lines_for_free_types type_enc (facts : ifact list) =
-if type_enc_needs_free_types type_enc then
+let
-let
+fun line j phi =
-val phis =
+Formula (tfree_clause_prefix ^ string_of_int j, Hypothesis, phi, NONE, [])
-fold (union (op =)) (map #atomic_types facts) []
+val phis =
-|> formulas_for_types type_enc add_sorts_on_tfree
+fold (union (op =)) (map #atomic_types facts) []
-in map2 formula_line_for_free_type (0 upto length phis - 1) phis end
+|> formulas_for_types type_enc add_sorts_on_tfree
-else
+in map2 line (0 upto length phis - 1) phis end
-[]
 (** Symbol declarations **)
 fun decl_line_for_class order phantoms s =
 let val name as (s, _) = `make_type_class s in
 Decl (sym_decl_prefix ^ s, name,
 if order = First_Order then
-ATyAbs ([tvar_a_name],
+APi ([tvar_a_name],
 if phantoms = Without_Phantom_Type_Vars then
 AFun (a_itself_atype, bool_atype)
 else
 bool_atype)
 else
 AFun (atype_of_types, bool_atype))
 end
 fun decl_lines_for_classes type_enc classes =
 | IAbs (_, tm) => add_iterm_syms tm
 | _ => I)
 #> fold add_iterm_syms args
 end
 val add_fact_syms = K add_iterm_syms |> formula_fold NONE |> ifact_lift
-fun add_formula_var_types (AQuant (_, xs, phi)) =
+fun add_formula_var_types (ATyQuant (_, _, phi)) = add_formula_var_types phi
+| add_formula_var_types (AQuant (_, xs, phi)) =
 fold (fn (_, SOME T) => insert_type thy I T | _ => I) xs
 #> add_formula_var_types phi
 | add_formula_var_types (AConn (_, phis)) =
 fold add_formula_var_types phis
 | add_formula_var_types _ = I
 in
 Decl (sym_decl_prefix ^ s, (s, s'),
 T |> fused_type ctxt mono (level_of_type_enc type_enc) ary
 |> ho_type_from_typ type_enc pred_sym ary
 |> not (null T_args)
-? curry ATyAbs (map (tvar_name o fst o dest_TVar) T_args))
+? curry APi (map (tvar_name o fst o dest_TVar) T_args))
 end
 fun honor_conj_sym_role in_conj =
 if in_conj then (Hypothesis, I) else (Axiom, I)
 String.isPrefix tfree_prefix s then
 atype_of_types
 else
 individual_atype
 | _ => individual_atype
-fun typ 0 = if pred_sym then bool_atype else ind
+fun typ 0 0 = if pred_sym then bool_atype else ind
-| typ ary = AFun (ind, typ (ary - 1))
+| typ 0 tm_ary = AFun (ind, typ 0 (tm_ary - 1))
+| typ ty_ary tm_ary = APi (replicate ty_ary tvar_a_name, typ 0 tm_ary)
 in typ end
 fun nary_type_constr_type n =
 funpow n (curry AFun atype_of_types) atype_of_types
 I
 fun do_type (AType (name, tys)) =
 do_sym name (fn () => nary_type_constr_type (length tys))
 #> fold do_type tys
 | do_type (AFun (ty1, ty2)) = do_type ty1 #> do_type ty2
-| do_type (ATyAbs (_, ty)) = do_type ty
+| do_type (APi (_, ty)) = do_type ty
 fun do_term pred_sym (ATerm ((name as (s, _), tys), tms)) =
-do_sym name (fn _ => default_type type_enc pred_sym s (length tms))
+do_sym name
+(fn _ => default_type type_enc pred_sym s (length tys) (length tms))
 #> fold do_type tys #> fold (do_term false) tms
 | do_term _ (AAbs (((_, ty), tm), args)) =
 do_type ty #> do_term false tm #> fold (do_term false) args
-fun do_formula (AQuant (_, xs, phi)) =
+fun do_formula (ATyQuant (_, _, phi)) = do_formula phi
+| do_formula (AQuant (_, xs, phi)) =
 fold do_type (map_filter snd xs) #> do_formula phi
 | do_formula (AConn (_, phis)) = fold do_formula phis
 | do_formula (AAtom tm) = do_term true tm
 fun do_problem_line (Decl (_, _, ty)) = do_type ty
 | do_problem_line (Formula (_, _, phi, _, _)) = do_formula phi
 fun make_head_roll (ATerm ((s, _), tms)) =
 if may_be_app s tms then make_head_roll (hd tms) ||> append (tl tms)
 else (s, tms)
 | make_head_roll _ = ("", [])
-fun strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
+fun strip_up_to_predicator (ATyQuant (_, _, phi)) = strip_up_to_predicator phi
+| strip_up_to_predicator (AQuant (_, _, phi)) = strip_up_to_predicator phi
 | strip_up_to_predicator (AConn (_, phis)) = maps strip_up_to_predicator phis
 | strip_up_to_predicator (AAtom tm) = [strip_predicator tm]
-fun strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
+fun strip_ahorn_etc (ATyQuant (_, _, phi)) = strip_ahorn_etc phi
+| strip_ahorn_etc (AQuant (_, _, phi)) = strip_ahorn_etc phi
 | strip_ahorn_etc (AConn (AImplies, [phi1, phi2])) =
 strip_ahorn_etc phi2 |>> append (strip_up_to_predicator phi1)
 | strip_ahorn_etc phi = ([], hd (strip_up_to_predicator phi))
-fun strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
+fun strip_iff_etc (ATyQuant (_, _, phi)) = strip_iff_etc phi
+| strip_iff_etc (AQuant (_, _, phi)) = strip_iff_etc phi
 | strip_iff_etc (AConn (AIff, [phi1, phi2])) =
 pairself strip_up_to_predicator (phi1, phi2)
 | strip_iff_etc _ = ([], [])
 val max_term_order_weight = 2147483647

changeset 49148	a5ab5964065f
parent 49147	9aa0fad4e864
child 49149	fa23e699494c