-(*
-let superposition_left (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
- (* we assume that target is ground (does not contain metavariables): this
- * should always be the case (I hope, at least) *)
- let proof, (eq_ty, left, right, t_order), _, _ = target in
- let eqproof, (ty, t1, t2, s_order), newmetas, args = source in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty then
- []
- else
- let where, is_left =
- match t_order (* compare_terms left right *) with
- | Lt -> right, false
- | Gt -> left, true
- | _ -> (
- Printf.printf "????????? %s = %s" (CicPp.ppterm left)
- (CicPp.ppterm right);
- print_newline ();
- assert false (* again, for ground terms this shouldn't happen... *)
- )
- in
- let metasenv' = newmetas @ metasenv in
- let result = s_order (* compare_terms t1 t2 *) in
- let res1, res2 =
- match result with
- | Gt -> (beta_expand t1 ty where context metasenv' ugraph), []
- | Lt -> [], (beta_expand t2 ty where context metasenv' ugraph)
- | _ ->
- let res1 =
- List.filter
- (fun (t, s, m, ug) ->
- compare_terms (M.apply_subst s t1) (M.apply_subst s t2) = Gt)
- (beta_expand t1 ty where context metasenv' ugraph)
- and res2 =
- List.filter
- (fun (t, s, m, ug) ->
- compare_terms (M.apply_subst s t2) (M.apply_subst s t1) = Gt)
- (beta_expand t2 ty where context metasenv' ugraph)
- in
- res1, res2
- in
- (* let what, other = *)
- (* if is_left then left, right *)
- (* else right, left *)
- (* in *)
- let build_new what other eq_URI (t, s, m, ug) =
- let newgoal, newgoalproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
- 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
- S.subst (M.apply_subst s other) bo,
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- proof; other; eqproof])
- | _ -> assert false
- in
- let equation =
- if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
- else (eq_ty, left, newgoal, compare_terms left newgoal)
- in
- (newgoalproof (* eqproof *), equation, [], [])
- in
- let new1 = List.map (build_new t1 t2 HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 HL.Logic.eq_ind_r_URI) res2 in
- new1 @ new2
-;;
-
-
-let superposition_right 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 eqproof, (eq_ty, left, right, t_order), newmetas, args = target in
- let eqp', (ty', t1, t2, s_order), newm', args' = source in
- let maxmeta = ref newmeta in
-
- let compare_terms = !Utils.compare_terms in
-
- if eq_ty <> ty' then
- newmeta, []
- else
- (* let ok term subst other other_eq_side ugraph = *)
- (* match term with *)
- (* | C.Lambda (nn, ty, bo) -> *)
- (* let bo' = S.subst (M.apply_subst subst other) bo in *)
- (* let res, _ = CR.are_convertible context bo' other_eq_side ugraph in *)
- (* not res *)
- (* | _ -> assert false *)
- (* in *)
- let condition left right what other (t, s, m, ug) =
- let subst = M.apply_subst s in
- let cmp1 = compare_terms (subst what) (subst other) in
- let cmp2 = compare_terms (subst left) (subst right) in
- (* cmp1 = Gt && cmp2 = Gt *)
- cmp1 <> Lt && cmp1 <> Le && cmp2 <> Lt && cmp2 <> Le
- (* && (ok t s other right ug) *)
- in
- let metasenv' = metasenv @ newmetas @ newm' in
- let beta_expand = beta_expand ~metas_ok:false in
- let cmp1 = t_order (* compare_terms left right *)
- and cmp2 = s_order (* compare_terms t1 t2 *) in
- let res1, res2, res3, res4 =
- let res l r s t =
- List.filter
- (condition l r s t)
- (beta_expand s eq_ty l context metasenv' ugraph)
- in
- match cmp1, cmp2 with
- | Gt, Gt ->
- (beta_expand t1 eq_ty left context metasenv' ugraph), [], [], []
- | Gt, Lt ->
- [], (beta_expand t2 eq_ty left context metasenv' ugraph), [], []
- | Lt, Gt ->
- [], [], (beta_expand t1 eq_ty right context metasenv' ugraph), []
- | Lt, Lt ->
- [], [], [], (beta_expand t2 eq_ty right context metasenv' ugraph)
- | Gt, _ ->
- let res1 = res left right t1 t2
- and res2 = res left right t2 t1 in
- res1, res2, [], []
- | Lt, _ ->
- let res3 = res right left t1 t2
- and res4 = res right left t2 t1 in
- [], [], res3, res4
- | _, Gt ->
- let res1 = res left right t1 t2
- and res3 = res right left t1 t2 in
- res1, [], res3, []
- | _, Lt ->
- let res2 = res left right t2 t1
- and res4 = res right left t2 t1 in
- [], res2, [], res4
- | _, _ ->
- let res1 = res left right t1 t2
- and res2 = res left right t2 t1
- and res3 = res right left t1 t2
- and res4 = res right left t2 t1 in
- res1, res2, res3, res4
- in
- let newmetas = newmetas @ newm' in
- let newargs = args @ args' in
- let build_new what other is_left eq_URI (t, s, m, ug) =
- (* let what, other = *)
- (* if is_left then left, right *)
- (* else right, left *)
- (* in *)
- let newterm, neweqproof =
- match t with
- | C.Lambda (nn, ty, bo) ->
- let bo' = M.apply_subst s (S.subst 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
- bo',
- M.apply_subst s
- (C.Appl [C.Const (eq_URI, []); ty; what; t';
- eqproof; other; eqp'])
- | _ -> assert false
- in
- let newmeta, newequality =
- let left, right =
- if is_left then (newterm, M.apply_subst s right)
- else (M.apply_subst s left, newterm) in
- let neworder = compare_terms left right in
- fix_metas !maxmeta
- (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
- in
- maxmeta := newmeta;
- newequality
- in
- let new1 = List.map (build_new t1 t2 true HL.Logic.eq_ind_URI) res1
- and new2 = List.map (build_new t2 t1 true HL.Logic.eq_ind_r_URI) res2
- and new3 = List.map (build_new t1 t2 false HL.Logic.eq_ind_URI) res3
- and new4 = List.map (build_new t2 t1 false HL.Logic.eq_ind_r_URI) res4 in
- let ok = function
- | _, (_, left, right, _), _, _ ->
- not (fst (CR.are_convertible context left right ugraph))
- in
- (!maxmeta,
- (List.filter ok (new1 @ new2 @ new3 @ new4)))
-;;
-*)
-
-
-let is_identity ((_, context, ugraph) as env) = function
- | ((_, _, (ty, left, right, _), _, _) as equality) ->
- (left = right ||
- (fst (CicReduction.are_convertible context left right ugraph)))
-;;
-
-
-(*
-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, t_order), metas, args = target
- and proof', (ty, t1, t2, s_order), 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 s_order (* 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, t_order), 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 neworder = compare_terms left right 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, neworder), 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