-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), newmetas, args = target in
- let eqp', (ty', t1, t2), newm', args' = source in
- let maxmeta = ref newmeta in
-
- (* TODO check if ty and ty' are equal... *)
- assert (eq_ty = ty');
-
-(* 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 = nonrec_kbo (subst what) (subst other) in
- let cmp2 = nonrec_kbo (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 res1 =
- List.filter
- (condition left right t1 t2)
- (beta_expand t1 eq_ty left context metasenv' ugraph)
- and res2 =
- List.filter
- (condition left right t2 t1)
- (beta_expand t2 eq_ty left context metasenv' ugraph)
- and res3 =
- List.filter
- (condition right left t1 t2)
- (beta_expand t1 eq_ty right context metasenv' ugraph)
- and res4 =
- List.filter
- (condition right left t2 t1)
- (beta_expand t2 eq_ty right context metasenv' ugraph)
- 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
- fix_metas !maxmeta
- (neweqproof, (eq_ty, left, right), 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 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
- if eq_ty <> ty then
- newmeta, target
- else
- 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
- 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
-(* Printf.printf *)
-(* "demodulate\ntarget: %s = %s\nwhat: %s\nother: %s\nis_left: %s\n" *)
-(* (CicPp.ppterm left) (CicPp.ppterm right) (CicPp.ppterm what) *)
-(* (CicPp.ppterm other) (string_of_bool is_left); *)
-(* Printf.printf "step: %d\n" step; *)
-(* print_newline (); *)
- let ok (t, s, m, ug) =
- nonrec_kbo (M.apply_subst s what) (M.apply_subst s other) = Gt
- in
- let res =
- List.filter ok
- (beta_expand ~metas_ok:false ~match_only:true
- what ty left context (metasenv @ metas) ugraph)
- 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'' =
- 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),
- 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
- let newmetasenv = metasenv @ metas in
- let newargs = args @ args' in
- fix_metas newmeta
- (newproof, (eq_ty, left, right), newmetasenv, newargs)
- in
- let _, (_, left, right), _, _ = newtarget
- and _, (_, oldleft, oldright), _, _ = target in
-(* Printf.printf *)
-(* "demodulate, newtarget: %s = %s\ntarget was: %s = %s\n" *)
-(* (CicPp.ppterm left) (CicPp.ppterm right) *)
-(* (CicPp.ppterm oldleft) (CicPp.ppterm oldright); *)
-(* print_newline (); *)
- demodulate newmeta step metasenv newtarget
- in
- demodulate newmeta 3 (metasenv @ metas') target
-;;
-
-
-(*
-let demodulation newmeta env target source =
- newmeta, target