-let is_identity ((_, context, ugraph) as env) = function
- | ((_, (ty, left, right), _, _) as equality) ->
- let res =
- (left = right ||
- (fst (CicReduction.are_convertible context left right ugraph)))
- in
-(* if res then ( *)
-(* Printf.printf "is_identity: %s" (string_of_equality ~env equality); *)
-(* print_newline (); *)
-(* ); *)
- res
-;;
-
-
-let demodulation newmeta (metasenv, context, ugraph) target source =
- let module C = Cic in
- let module S = CicSubstitution in
- let module M = CicMetaSubst in
- let module HL = HelmLibraryObjects in
- let module CR = CicReduction in
-
- let proof, (eq_ty, left, right), metas, args = target
- and proof', (ty, t1, t2), metas', args' = source in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty then
- newmeta, target
- else
- let first_step, get_params =
- match compare_terms t1 t2 with
- | Gt -> 1, (function
- | 1 -> true, t1, t2, HL.Logic.eq_ind_URI
- | 0 -> false, t1, t2, HL.Logic.eq_ind_URI
- | _ -> assert false)
- | Lt -> 1, (function
- | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
- | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
- | _ -> assert false)
- | _ ->
- let first_step = 3 in
- let get_params step =
- match step with
- | 3 -> true, t1, t2, HL.Logic.eq_ind_URI
- | 2 -> false, t1, t2, HL.Logic.eq_ind_URI
- | 1 -> true, t2, t1, HL.Logic.eq_ind_r_URI
- | 0 -> false, t2, t1, HL.Logic.eq_ind_r_URI
- | _ -> assert false
- in
- first_step, get_params
- in
- let rec demodulate newmeta step metasenv target =
- let proof, (eq_ty, left, right), metas, args = target in
- let is_left, what, other, eq_URI = get_params step in
-
- let env = metasenv, context, ugraph in
- let names = names_of_context context in
-(* Printf.printf *)
-(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (string_of_equality ~env target) (CicPp.pp what names) *)
-(* (CicPp.pp other names) (string_of_bool is_left); *)
-(* Printf.printf "step: %d" step; *)
-(* print_newline (); *)
-
- let ok (t, s, m, ug) =
- compare_terms (M.apply_subst s what) (M.apply_subst s other) = Gt
- in
- let res =
- let r = (beta_expand ~metas_ok:false ~match_only:true
- what ty (if is_left then left else right)
- context (metasenv @ metas) ugraph)
- in
-(* let m' = metas_of_term what *)
-(* and m'' = metas_of_term (if is_left then left else right) in *)
-(* if (List.mem 527 m'') && (List.mem 6 m') then ( *)
-(* Printf.printf *)
-(* "demodulate\ntarget: %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (string_of_equality ~env target) (CicPp.pp what names) *)
-(* (CicPp.pp other names) (string_of_bool is_left); *)
-(* Printf.printf "step: %d" step; *)
-(* print_newline (); *)
-(* print_endline "res:"; *)
-(* List.iter (fun (t, s, m, ug) -> print_endline (CicPp.pp t names)) r; *)
-(* print_newline (); *)
-(* Printf.printf "metasenv:\n%s\n" (print_metasenv (metasenv @ metas)); *)
-(* print_newline (); *)
-(* ); *)
- List.filter ok r
- in
- match res with
- | [] ->
- if step = 0 then newmeta, target
- else demodulate newmeta (step-1) metasenv target
- | (t, s, m, ug)::_ ->
- let newterm, newproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
-(* let bo' = M.apply_subst s (S.subst other bo) in *)
- let bo' = S.subst (M.apply_subst s other) bo in
- let bo'' =
- C.Appl (
- [C.MutInd (HL.Logic.eq_URI, 0, []);
- S.lift 1 eq_ty] @
- if is_left then [bo'; S.lift 1 right]
- else [S.lift 1 left; bo'])
- in
- let t' = C.Lambda (nn, ty, bo'') in
-(* M.apply_subst s (S.subst other bo), *)
- bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; proof'])
- | _ -> assert false
- in
- let newmeta, newtarget =
- let left, right =
-(* if is_left then (newterm, M.apply_subst s right) *)
-(* else (M.apply_subst s left, newterm) in *)
- if is_left then newterm, right
- else left, newterm
- in
-(* let newmetasenv = metasenv @ metas in *)
-(* let newargs = args @ args' in *)
-(* fix_metas newmeta *)
-(* (newproof, (eq_ty, left, right), newmetasenv, newargs) *)
- let m = (metas_of_term left) @ (metas_of_term right) in
- let newmetasenv = List.filter (fun (i, _, _) -> List.mem i m) metas
- and newargs =
- List.filter
- (function C.Meta (i, _) -> List.mem i m | _ -> assert false)
- args
- in
- newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
- in
-(* Printf.printf *)
-(* "demodulate, newtarget: %s\ntarget was: %s\n" *)
-(* (string_of_equality ~env newtarget) *)
-(* (string_of_equality ~env target); *)
-(* (\* let _, _, newm, newa = newtarget in *\) *)
-(* (\* Printf.printf "newmetasenv:\n%s\nnewargs:\n%s\n" *\) *)
-(* (\* (print_metasenv newm) *\) *)
-(* (\* (String.concat "\n" (List.map CicPp.ppterm newa)); *\) *)
-(* print_newline (); *)
- if is_identity env newtarget then
- newmeta, newtarget
- else
- demodulate newmeta first_step metasenv newtarget
- in
- demodulate newmeta first_step (metasenv @ metas') target
-;;
-
-
-(*
-let demodulation newmeta env target source =
- newmeta, target
-;;
-*)
-
-
-let subsumption env target source =
- let _, (ty, tl, tr), tmetas, _ = target
- and _, (ty', sl, sr), smetas, _ = source in
- if ty <> ty' then
- false
- else
- let metasenv, context, ugraph = env in
- let metasenv = metasenv @ tmetas @ smetas in
- let names = names_of_context context in
- let samesubst subst subst' =
-(* Printf.printf "samesubst:\nsubst: %s\nsubst': %s\n" *)
-(* (print_subst subst) (print_subst subst'); *)
-(* print_newline (); *)
- let tbl = Hashtbl.create (List.length subst) in
- List.iter (fun (m, (c, t1, t2)) -> Hashtbl.add tbl m (c, t1, t2)) subst;
- List.for_all
- (fun (m, (c, t1, t2)) ->
- try
- let c', t1', t2' = Hashtbl.find tbl m in
- if (c = c') && (t1 = t1') && (t2 = t2') then true
- else false
- with Not_found ->
- true)
- subst'
- in
- let subsaux left right left' right' =
- try
- let subst, menv, ug = matching metasenv context left left' ugraph
- and subst', menv', ug' = matching metasenv context right right' ugraph
- in
-(* Printf.printf "left = right: %s = %s\n" *)
-(* (CicPp.pp left names) (CicPp.pp right names); *)
-(* Printf.printf "left' = right': %s = %s\n" *)
-(* (CicPp.pp left' names) (CicPp.pp right' names); *)
- samesubst subst subst'
- with e ->
-(* print_endline (Printexc.to_string e); *)
- false
- in
- let res =
- if subsaux tl tr sl sr then true
- else subsaux tl tr sr sl
- in
- if res then (
- Printf.printf "subsumption!:\ntarget: %s\nsource: %s\n"
- (string_of_equality ~env target) (string_of_equality ~env source);
- print_newline ();
- );
- res