1 (* type naif_indexing =
2 (Cic.term * ((bool * Inference.equality) list)) list
5 type pos = Left | Right ;;
7 let head_of_term = function
8 | Cic.Appl (hd::tl) -> hd
13 let index table (sign, eq) =
14 let _, (_, l, r, ordering), _, _ = eq in
15 let hl = head_of_term l in
16 let hr = head_of_term r in
18 let x_entry = try Hashtbl.find table x with Not_found -> [] in
19 Hashtbl.replace table x ((pos, sign, eq)::x_entry)
21 (* (match ordering with *)
26 (* | _ -> index hl Left; *)
27 (* index hr Right); *)
34 let remove_index table (sign, eq) =
35 let _, (_, l, r, ordering), _, _ = eq in
36 let hl = head_of_term l
37 and hr = head_of_term r in
38 let remove_index x pos =
39 let x_entry = try Hashtbl.find table x with Not_found -> [] in
40 let newentry = List.filter (fun e -> e <> (pos, sign, eq)) x_entry in
41 Hashtbl.replace table x newentry
44 remove_index hr Right;
49 let rec find_matches metasenv context ugraph lift_amount term =
51 let module U = Utils in
52 let module S = CicSubstitution in
53 let module M = CicMetaSubst in
54 let module HL = HelmLibraryObjects in
55 let cmp = !Utils.compare_terms in
58 | (_, U.Negative, _)::tl ->
59 find_matches metasenv context ugraph lift_amount term tl
60 | (pos, U.Positive, (_, (_, _, _, o), _, _))::tl
61 when (pos = Left && o = U.Lt) || (pos = Right && o = U.Gt) ->
62 find_matches metasenv context ugraph lift_amount term tl
63 | (pos, U.Positive, (proof, (ty, left, right, o), metas, args))::tl ->
64 let do_match c other eq_URI =
65 let subst', metasenv', ugraph' =
66 Inference.matching (metasenv @ metas) context term
67 (S.lift lift_amount c) ugraph
69 Some (C.Rel (1 + lift_amount), subst', metasenv', ugraph',
70 (proof, ty, c, other, eq_URI))
72 let c, other, eq_URI =
73 if pos = Left then left, right, HL.Logic.eq_ind_URI
74 else right, left, HL.Logic.eq_ind_r_URI
76 if o <> U.Incomparable then
77 try do_match c other eq_URI
78 with e -> find_matches metasenv context ugraph lift_amount term tl
80 let res = try do_match c other eq_URI with e -> None in
82 | Some (_, s, _, _, _) ->
83 if cmp (M.apply_subst s left) (M.apply_subst s right) =
84 (if pos = Left then U.Gt else U.Lt) then
87 find_matches metasenv context ugraph lift_amount term tl
89 find_matches metasenv context ugraph lift_amount term tl
93 let rec demodulate_term metasenv context ugraph table lift_amount term =
95 let module S = CicSubstitution in
96 let module M = CicMetaSubst in
97 let module HL = HelmLibraryObjects in
98 let hd_term = head_of_term term in
99 let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
104 find_matches metasenv context ugraph lift_amount term candidates
115 (res, tl @ [S.lift 1 t])
118 demodulate_term metasenv context ugraph table
122 | None -> (None, tl @ [S.lift 1 t])
123 | Some (rel, _, _, _, _) -> (r, tl @ [rel]))
128 | Some (_, subst, menv, ug, info) ->
129 Some (C.Appl ll, subst, menv, ug, info)
131 | C.Prod (nn, s, t) ->
133 demodulate_term metasenv context ugraph table lift_amount s in (
137 demodulate_term metasenv
138 ((Some (nn, C.Decl s))::context) ugraph
139 table (lift_amount+1) t
143 | Some (t', subst, menv, ug, info) ->
144 Some (C.Prod (nn, (S.lift 1 s), t'),
145 subst, menv, ug, info)
147 | Some (s', subst, menv, ug, info) ->
148 Some (C.Prod (nn, s', (S.lift 1 t)), subst, menv, ug, info)
151 Printf.printf "Ne` Appl ne` Prod: %s\n"
152 (CicPp.pp t (Utils.names_of_context context));
157 let rec demodulate newmeta env table target =
158 let module C = Cic in
159 let module S = CicSubstitution in
160 let module M = CicMetaSubst in
161 let module HL = HelmLibraryObjects in
162 let metasenv, context, ugraph = env in
163 let proof, (eq_ty, left, right, order), metas, args = target in
164 let metasenv = metasenv @ metas in
165 let build_newtarget is_left
166 (t, subst, menv, ug, (proof', ty, what, other, eq_URI)) =
167 let newterm, newproof =
168 let bo = S.subst (M.apply_subst subst other) t in
170 C.Appl ([C.MutInd (HL.Logic.eq_URI, 0, []);
172 if is_left then [bo; S.lift 1 right] else [S.lift 1 left; bo])
174 let t' = C.Lambda (C.Anonymous, ty, bo'') in
176 M.apply_subst subst (C.Appl [C.Const (eq_URI, []); ty; what; t';
177 proof; other; proof'])
179 let newmeta, newtarget =
180 let left, right = if is_left then newterm, right else left, newterm in
182 (Inference.metas_of_term left) @ (Inference.metas_of_term right)
184 let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
187 (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
190 let ordering = !Utils.compare_terms left right in
191 newmeta, (newproof, (eq_ty, left, right, ordering), newmetasenv, newargs)
195 let res = demodulate_term metasenv context ugraph table 0 left in
198 let newmeta, newtarget = build_newtarget true t in
199 if Inference.is_identity (metasenv, context, ugraph) newtarget then
202 demodulate newmeta env table newtarget
204 let res = demodulate_term metasenv context ugraph table 0 right in
207 let newmeta, newtarget = build_newtarget false t in
208 if Inference.is_identity (metasenv, context, ugraph) newtarget then
211 demodulate newmeta env table newtarget
217 let rec betaexpand_term metasenv context ugraph table lift_amount term =
218 let module C = Cic in
219 let module S = CicSubstitution in
220 let module M = CicMetaSubst in
221 let module HL = HelmLibraryObjects in
222 let hd_term = head_of_term term in
223 let candidates = try Hashtbl.find table hd_term with Not_found -> [] in
224 let res, lifted_term =
229 | Some t -> Some (S.lift lift_amount t)
235 [], if m <= lift_amount then C.Rel m else C.Rel (m+1)
237 | C.Prod (nn, s, t) ->
239 betaexpand_term metasenv context ugraph table lift_amount s in
241 betaexpand_term metasenv ((Some (nn, C.Decl s))::context) ugraph
242 table (lift_amount+1) t in
245 (fun (t, s, m, ug, info) ->
246 C.Prod (nn, t, lifted_t), s, m, ug, info) l1
249 (fun (t, s, m, ug, info) ->
250 C.Prod (nn, lifted_s, t), s, m, ug, info) l2 in
251 l1' @ l2', C.Prod (nn, lifted_s, lifted_t)
256 (fun arg (res, lifted_tl) ->
257 let arg_res, lifted_arg =
258 betaexpand_term metasenv context ugraph table lift_amount arg
262 (fun (a, s, m, ug, info) -> a::lifted_tl, s, m, ug, info)
267 (fun (r, s, m, ug, info) -> lifted_arg::r, s, m, ug, info)
269 lifted_arg::lifted_tl)
272 (List.map (fun (l, s, m, ug, info) -> (C.Appl l, s, m, ug, info)) l',
275 | t -> [], (S.lift lift_amount t)
278 | C.Meta _ -> res, lifted_term
281 find_matches metasenv context ugraph lift_amount term candidates
283 | None -> res, lifted_term
284 | Some r -> r::res, lifted_term
288 let superposition_left (metasenv, context, ugraph) table target =
289 let module C = Cic in
290 let module S = CicSubstitution in
291 let module M = CicMetaSubst in
292 let module HL = HelmLibraryObjects in
293 let module CR = CicReduction in
294 let module U = Utils in
295 let proof, (eq_ty, left, right, ordering), _, _ = target in
297 let term = if ordering = U.Gt then left else right in
298 betaexpand_term metasenv context ugraph table 0 term
300 let build_new (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
301 let newgoal, newproof =
302 let bo' = S.subst (M.apply_subst s other) bo in
305 [C.MutInd (HL.Logic.eq_URI, 0, []);
307 if ordering = U.Gt then [bo'; S.lift 1 right]
308 else [S.lift 1 left; bo'])
310 let t' = C.Lambda (C.Anonymous, ty, bo'') in
311 S.subst (M.apply_subst s other) bo,
313 (C.Appl [C.Const (eq_URI, []); ty; what; t';
314 proof; other; proof'])
316 let left, right, newordering =
317 if ordering = U.Gt then
318 newgoal, right, !Utils.compare_terms newgoal right
320 left, newgoal, !Utils.compare_terms left newgoal
322 (newproof, (eq_ty, left, right, ordering), [], [])
324 List.map build_new expansions
328 let superposition_right newmeta (metasenv, context, ugraph) table target =
329 let module C = Cic in
330 let module S = CicSubstitution in
331 let module M = CicMetaSubst in
332 let module HL = HelmLibraryObjects in
333 let module CR = CicReduction in
334 let module U = Utils in
335 let eqproof, (eq_ty, left, right, ordering), newmetas, args = target in
336 let maxmeta = ref newmeta in
339 | U.Gt -> fst (betaexpand_term metasenv context ugraph table 0 left), []
340 | U.Lt -> [], fst (betaexpand_term metasenv context ugraph table 0 right)
344 (fun (_, subst, _, _, _) ->
345 let subst = M.apply_subst subst in
346 let o = !Utils.compare_terms (subst l) (subst r) in
347 o <> U.Lt && o <> U.Le)
348 (fst (betaexpand_term metasenv context ugraph table 0 l))
350 (res left right), (res right left)
352 let build_new ordering (bo, s, m, ug, (proof', ty, what, other, eq_URI)) =
353 let newgoal, newproof =
354 let bo' = S.subst (M.apply_subst s other) bo in
357 [C.MutInd (HL.Logic.eq_URI, 0, []);
359 if ordering = U.Gt then [bo'; S.lift 1 right]
360 else [S.lift 1 left; bo'])
362 let t' = C.Lambda (C.Anonymous, ty, bo'') in
363 S.subst (M.apply_subst s other) bo,
365 (C.Appl [C.Const (eq_URI, []); ty; what; t';
366 eqproof; other; proof'])
368 let newmeta, newequality =
369 let left, right, newordering =
370 if ordering = U.Gt then
371 newgoal, right, !Utils.compare_terms newgoal right
373 left, newgoal, !Utils.compare_terms left newgoal
375 Inference.fix_metas !maxmeta
376 (newproof, (eq_ty, left, right, ordering), [], [])
381 let new1 = List.map (build_new U.Gt) res1
382 and new2 = List.map (build_new U.Lt) res2 in
384 | _, (_, left, right, _), _, _ ->
385 not (fst (CR.are_convertible context left right ugraph))
388 (List.filter ok (new1 @ new2)))