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