1(* ========================================================================= *) 2(* FILE : hhTranslate.sml *) 3(* DESCRIPTION : HOL to FOL translation *) 4(* AUTHOR : (c) Thibault Gauthier, Czech Technical University *) 5(* DATE : 2018 *) 6(* ========================================================================= *) 7 8structure hhTranslate :> hhTranslate = 9struct 10 11open HolKernel boolLib aiLib 12 13val ERR = mk_HOL_ERR "hhTranslate" 14val translate_cache_glob = ref (dempty Term.compare) 15 16(* ------------------------------------------------------------------------- 17 Eliminating some lambdas without lambda-lifting 18 ------------------------------------------------------------------------- *) 19 20fun ELIM_LAMBDA_EQ tm = 21 let val (l, r) = dest_eq tm in 22 ( 23 if is_abs l orelse is_abs r then 24 CHANGED_CONV (ONCE_REWRITE_CONV [FUN_EQ_THM] THENC 25 REDEPTH_CONV BETA_CONV) 26 else NO_CONV 27 ) 28 tm 29 end 30 31fun PREP_CONV tm = 32 (REDEPTH_CONV ELIM_LAMBDA_EQ THENC REDEPTH_CONV BETA_CONV) tm 33 34fun prep_rw tm = rand (only_concl (QCONV PREP_CONV tm)) 35 36(* ------------------------------------------------------------------------- 37 Variable names 38 ------------------------------------------------------------------------- *) 39 40(* lifting *) 41fun genvar_lifting iref ty = 42 let val r = mk_var ("F" ^ its (!iref), ty) in 43 incr iref; r 44 end 45 46(* arity *) 47fun genvarl_arity tyl = 48 let fun f i ty = mk_var ("X" ^ int_to_string i, ty) in 49 mapi f tyl 50 end 51 52(* ------------------------------------------------------------------------- 53 First-order atoms 54 Warning: a and b are considered atoms is !a. a = b instead of a = b 55 ------------------------------------------------------------------------- *) 56 57fun must_pred tm = 58 is_forall tm orelse is_exists tm orelse is_conj tm orelse is_disj tm orelse 59 is_imp tm orelse is_eq tm orelse is_neg tm 60 61local 62 val (atoml: term list ref) = ref [] 63 fun atoms_aux tm = 64 if is_conj tm orelse is_disj tm orelse is_imp_only tm orelse is_eq tm 65 then (atoms_aux (lhand tm); atoms_aux (rand tm)) 66 else if is_neg tm then atoms_aux (rand tm) 67 else if is_forall tm then atoms_aux (snd (dest_forall tm)) 68 else if is_exists tm then atoms_aux (snd (dest_exists tm)) 69 else atoml := tm :: (!atoml) 70in 71 fun atoms tm = (atoml := []; atoms_aux tm; !atoml) 72end 73 74(* ------------------------------------------------------------------------- 75 Extract constants in a term 76 ------------------------------------------------------------------------- *) 77 78fun is_app tm = is_var tm andalso fst (dest_var tm) = "app" 79 80fun is_tptp_fv tm = 81 is_var tm andalso Char.isLower (String.sub (fst (dest_var tm),0)) 82 andalso fst (dest_var tm) <> "app" 83fun is_tptp_bv tm = 84 is_var tm andalso Char.isUpper (String.sub (fst (dest_var tm),0)) 85 86fun all_fosubtm tm = 87 let val (oper,argl) = strip_comb tm in 88 tm :: List.concat (map all_fosubtm argl) 89 end 90 91(* ignores app *) 92fun collect_arity_noapp tm = 93 let 94 val tml1 = List.concat (map all_fosubtm (atoms tm)) 95 val tml2 = mk_term_set tml1 96 fun f subtm = 97 let val (oper,argl) = strip_comb subtm in 98 if is_tptp_fv oper orelse is_const oper 99 then SOME (oper,length argl) 100 else NONE 101 end 102 in 103 mk_fast_set (cpl_compare Term.compare Int.compare) (List.mapPartial f tml2) 104 end 105 106(* ------------------------------------------------------------------------- 107 Lifting proposition and lambdas 108 ------------------------------------------------------------------------- *) 109 110fun ATOM_CONV conv tm = 111 if is_forall tm orelse is_exists tm 112 then QUANT_CONV (ATOM_CONV conv) tm 113 else if is_conj tm orelse is_disj tm orelse is_imp_only tm orelse is_eq tm 114 then BINOP_CONV (ATOM_CONV conv) tm else 115 if is_neg tm 116 then RAND_CONV (ATOM_CONV conv) tm 117 else conv tm 118 119fun FUN_EQ_CONVL vl eq = case vl of 120 [] => REFL eq 121 | a :: m => (STRIP_QUANT_CONV (X_FUN_EQ_CONV a) THENC FUN_EQ_CONVL m) eq 122 123fun LIFT_CONV iref tm = 124 let 125 fun test x = must_pred x orelse is_abs x 126 val subtm = find_term test tm 127 handle Interrupt => raise Interrupt 128 | _ => raise ERR "LIFT_CONV" "" 129 val fvl = filter is_tptp_bv (free_vars_lr subtm) 130 val v = genvar_lifting iref (type_of (list_mk_abs (fvl,subtm))) 131 val rep = list_mk_comb (v,fvl) 132 val eq = list_mk_forall (fvl, (mk_eq (subtm,rep))) 133 val thm = ASSUME eq 134 in 135 if is_abs subtm then 136 let 137 val (vl,bod) = strip_abs subtm 138 val ethm1 = (FUN_EQ_CONVL vl THENC TOP_DEPTH_CONV BETA_CONV) eq 139 val ethm2 = UNDISCH (snd (EQ_IMP_RULE ethm1)) 140 val cthm = PURE_REWRITE_CONV [thm] tm 141 in 142 PROVE_HYP ethm2 cthm 143 end 144 else PURE_REWRITE_CONV [thm] tm 145 end 146 147fun RPT_LIFT_CONV iref tm = 148 let 149 val thmo = SOME (REPEATC (ATOM_CONV (TRY_CONV (LIFT_CONV iref))) tm) 150 handle UNCHANGED => NONE 151 in 152 case thmo of 153 SOME thm => 154 let 155 val (asl,w) = dest_thm thm 156 val thml1 = List.concat (map (RPT_LIFT_CONV iref) asl) 157 in 158 thm :: thml1 159 end 160 | NONE => [REFL tm] 161 end 162 163(* ------------------------------------------------------------------------- 164 Lowest arity for bound variables. Arity 0. 165 ------------------------------------------------------------------------- *) 166 167fun APP_CONV_ONCE tm = 168 let 169 val (rator,rand) = dest_comb tm 170 val f = mk_var ("f",type_of rator) 171 val v = mk_var ("v",type_of rand) 172 val bod = mk_comb (f,v) 173 val lam = list_mk_abs (free_vars_lr bod, bod) 174 val app = mk_var ("app",type_of lam) 175 val eq = mk_eq (app, lam) 176 val thm1 = ASSUME eq 177 val thm2 = AP_THM (AP_THM thm1 f) v 178 val thm3 = CONV_RULE (REDEPTH_CONV BETA_CONV) thm2 179 val thm4 = GENL [f,v] thm3 180 in 181 SYM (ISPECL [rator,rand] thm4) 182 end 183 184fun APP_CONV_STRIPCOMB tm = 185 (TRY_CONV (RATOR_CONV APP_CONV_STRIPCOMB) THENC APP_CONV_ONCE) tm 186 187fun APP_CONV_BV tm = 188 if not (is_comb tm) then NO_CONV tm else 189 let val (oper,_) = strip_comb tm in 190 if is_tptp_bv oper then APP_CONV_STRIPCOMB tm else NO_CONV tm 191 end 192 193val APP_CONV_BV_REC = TRY_CONV (TOP_SWEEP_CONV APP_CONV_BV) THENC REFL 194 195(* ------------------------------------------------------------------------- 196 Optional (included by default): 197 Prevents polymorphic higher-order constants from exceeding max arity 198 (e.g. "I_2 I_1 1 => app (I_1 I_0) 1" ) 199 ------------------------------------------------------------------------- *) 200 201fun strip_funty_aux ty = 202 if is_vartype ty then [ty] else 203 let val {Args, Thy, Tyop} = dest_thy_type ty in 204 if Thy = "min" andalso Tyop = "fun" then 205 let val (tya,tyb) = pair_of_list Args in 206 tya :: strip_funty_aux tyb 207 end 208 else [ty] 209 end 210 211fun strip_funty ty = case strip_funty_aux ty of 212 [] => raise ERR "strip_funty" "" 213 | x => (last x, butlast x) 214 215fun mgty_of c = 216 let val {Thy, Name, Ty} = dest_thy_const c in 217 type_of (prim_mk_const {Thy = Thy, Name = Name}) 218 end 219 220fun max_arity c = length (snd (strip_funty (mgty_of c))) 221 222fun APP_CONV_MAX tm = 223 if not (is_comb tm) then NO_CONV tm else 224 let val (oper,argl) = strip_comb tm in 225 if is_const oper andalso length argl > max_arity oper 226 then APP_CONV_ONCE tm 227 else NO_CONV tm 228 end 229 230val APP_CONV_MAX_REC = TRY_CONV (TOP_SWEEP_CONV APP_CONV_MAX) THENC REFL 231 232(* ------------------------------------------------------------------------- 233 FOF Translation 234 ------------------------------------------------------------------------- *) 235 236fun prepare_tm tm = 237 let val tm' = prep_rw tm in 238 rename_bvarl escape (list_mk_forall (free_vars_lr tm', tm')) 239 end 240 241fun rw_conv conv tm = (rhs o concl o conv) tm 242fun sym_def tm = rw_conv (STRIP_QUANT_CONV SYM_CONV) tm 243 244fun translate_nocache tm = 245 let 246 val iref = ref 0 247 val tm1 = prepare_tm tm 248 val tml1 = map (rand o concl) (RPT_LIFT_CONV iref tm1) 249 val tml2 = map (rw_conv APP_CONV_BV_REC) tml1 250 val tml3 = map (rw_conv APP_CONV_MAX_REC) tml2 251 val tm2 = list_mk_imp (map sym_def (rev (tl tml3)), hd tml3) 252 val fvl = filter is_tptp_bv (free_vars_lr tm2) 253 in 254 list_mk_forall (fvl,tm2) 255 end 256 257fun translate tm = 258 dfind tm (!translate_cache_glob) handle NotFound => 259 let val x = translate_nocache tm in 260 translate_cache_glob := dadd tm x (!translate_cache_glob); x 261 end 262 263fun translate_thm thm = 264 let val tm = (concl o GEN_ALL o DISCH_ALL) thm in translate tm end 265 266(* ------------------------------------------------------------------------- 267 Arity equations for constants and free variables. 268 ------------------------------------------------------------------------- *) 269 270fun mk_arity_eq (f,n) = 271 let 272 val (tyl,_) = strip_type (type_of f) 273 val vl = genvarl_arity tyl 274 val vl' = List.take (vl,n) 275 val tm = list_mk_comb (f,vl') 276 in 277 concl (GENL vl' (APP_CONV_STRIPCOMB tm)) 278 end 279 280 281end 282