# HG changeset patch # User paulson # Date 1178549202 -7200 # Node ID 7b7d6e1c70b6536b10f576548bcb25349b1527ce # Parent e795b5a031af623fc48b0423a4e4c7a5eccf5013 First-order variant of the fully-typed translation diff -r e795b5a031af -r 7b7d6e1c70b6 src/HOL/Tools/res_hol_clause.ML --- a/src/HOL/Tools/res_hol_clause.ML Mon May 07 14:20:32 2007 +0200 +++ b/src/HOL/Tools/res_hol_clause.ML Mon May 07 16:46:42 2007 +0200 @@ -56,7 +56,7 @@ (*True if the constant ever appears outside of the top-level position in literals. If false, the constant always receives all of its arguments and is used as a predicate.*) -fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level<>T_CONST orelse +fun needs_hBOOL c = not (!minimize_applies) orelse !typ_level=T_PARTIAL orelse getOpt (Symtab.lookup(!const_needs_hBOOL) c, false); fun init thy = @@ -292,17 +292,6 @@ (* DFG used by SPASS *) (**********************************************************************) -val type_wrapper = "ti"; - -fun wrap_type (c,tp) = case !typ_level of - T_FULL => type_wrapper ^ RC.paren_pack [c, RC.string_of_fol_type tp] - | _ => c; - - -val bool_tp = RC.make_fixed_type_const "bool"; - -val app_str = "hAPP"; - (*Result of a function type; no need to check that the argument type matches.*) fun result_type (RC.Comp ("tc_fun", [_, tp2])) = tp2 | result_type _ = raise ERROR "result_type" @@ -318,7 +307,19 @@ | stripc x = x in stripc(u,[]) end; -(*Full and partial-typed transations*) +val type_wrapper = "ti"; + +fun head_needs_hBOOL (CombConst(c,_,_)) = needs_hBOOL c + | head_needs_hBOOL _ = true; + +fun wrap_type (s, tp) = + if !typ_level=T_FULL then + type_wrapper ^ RC.paren_pack [s, RC.string_of_fol_type tp] + else s; + +fun apply ss = "hAPP" ^ RC.paren_pack ss; + +(*Full (non-optimized) and partial-typed transations*) fun string_of_combterm1 (CombConst(c,tp,_)) = let val c' = if c = "equal" then "c_fequal" else c in wrap_type (c',tp) end @@ -329,45 +330,50 @@ and s2 = string_of_combterm1 t2 in case !typ_level of - T_FULL => type_wrapper ^ - RC.paren_pack - [app_str ^ RC.paren_pack [s1,s2], - RC.string_of_fol_type (result_type (type_of_combterm t1))] - | T_PARTIAL => app_str ^ RC.paren_pack - [s1,s2, RC.string_of_fol_type (type_of_combterm t1)] + T_FULL => wrap_type (apply [s1,s2], result_type (type_of_combterm t1)) + | T_PARTIAL => apply [s1,s2, RC.string_of_fol_type (type_of_combterm t1)] | T_CONST => raise ERROR "string_of_combterm1" end; fun rev_apply (v, []) = v - | rev_apply (v, arg::args) = app_str ^ RC.paren_pack [rev_apply (v, args), arg]; + | rev_apply (v, arg::args) = apply [rev_apply (v, args), arg]; fun string_apply (v, args) = rev_apply (v, rev args); (*Apply an operator to the argument strings, using either the "apply" operator or direct function application.*) -fun string_of_applic (CombConst(c,_,tvars), args) = +fun string_of_applic (CombConst(c,tp,tvars), args) = let val c = if c = "equal" then "c_fequal" else c val nargs = min_arity_of c - val args1 = List.take(args, nargs) @ (map RC.string_of_fol_type tvars) + val args1 = List.take(args, nargs) handle Subscript => raise ERROR ("string_of_applic: " ^ c ^ " has arity " ^ Int.toString nargs ^ " but is applied to " ^ space_implode ", " args) val args2 = List.drop(args, nargs) + val targs = if !typ_level = T_CONST then map RC.string_of_fol_type tvars + else [] in - string_apply (c ^ RC.paren_pack args1, args2) + string_apply (c ^ RC.paren_pack (args1@targs), args2) end - | string_of_applic (CombFree(v,_), args) = string_apply (v, args) - | string_of_applic (CombVar(v,_), args) = string_apply (v, args) + | string_of_applic (CombFree(v,tp), args) = string_apply (v, args) + | string_of_applic (CombVar(v,tp), args) = string_apply (v, args) | string_of_applic _ = raise ERROR "string_of_applic"; -(*Constant-typed transation*) +fun wrap_type_if (head, s, tp) = if head_needs_hBOOL head then wrap_type (s, tp) else s; + +(*Full (if optimized) and constant-typed transations*) fun string_of_combterm2 t = let val (head, args) = strip_comb t - in string_of_applic (head, map string_of_combterm2 args) end; + in wrap_type_if (head, + string_of_applic (head, map string_of_combterm2 args), + type_of_combterm t) + end; fun string_of_combterm t = - case !typ_level of T_CONST => string_of_combterm2 t - | _ => string_of_combterm1 t; + case (!typ_level,!minimize_applies) of + (T_PARTIAL, _) => string_of_combterm1 t + | (T_FULL, false) => string_of_combterm1 t + | _ => string_of_combterm2 t; (*Boolean-valued terms are here converted to literals.*) fun boolify t = "hBOOL" ^ RC.paren_pack [string_of_combterm t]; @@ -457,14 +463,15 @@ if c = "equal" then (addtypes tvars funcs, preds) else (case !typ_level of - T_CONST => - let val arity = min_arity_of c + length tvars - val addit = Symtab.update(c,arity) + T_PARTIAL => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds) + | _ => + let val arity = min_arity_of c + val ntys = if !typ_level = T_CONST then length tvars else 0 + val addit = Symtab.update(c, arity+ntys) in if needs_hBOOL c then (addtypes tvars (addit funcs), preds) else (addtypes tvars funcs, addit preds) - end - | _ => (RC.add_foltype_funcs (tp, Symtab.update(c,0) funcs), preds)) + end) | add_decls (CombFree(v,ctp), (funcs,preds)) = (RC.add_foltype_funcs (ctp,Symtab.update (v,0) funcs), preds) | add_decls (CombVar(_,ctp), (funcs,preds)) = @@ -582,7 +589,7 @@ (if needs_hBOOL c then " needs hBOOL" else "")); fun count_constants (conjectures, axclauses, helper_clauses) = - if !minimize_applies andalso !typ_level=T_CONST then + if !minimize_applies andalso !typ_level<>T_PARTIAL then (List.app count_constants_clause conjectures; List.app count_constants_clause axclauses; List.app count_constants_clause helper_clauses;