match env with
| None -> (
function
- | _, (ty, left, right), _, _ ->
- Printf.sprintf "{%s}: %s = %s" (CicPp.ppterm ty)
- (CicPp.ppterm left) (CicPp.ppterm right)
+ | _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.ppterm ty)
+ (CicPp.ppterm left) (string_of_comparison o) (CicPp.ppterm right)
)
| Some (_, context, _) -> (
let names = names_of_context context in
function
- | _, (ty, left, right), _, _ ->
- Printf.sprintf "{%s}: %s = %s" (CicPp.pp ty names)
- (CicPp.pp left names) (CicPp.pp right names)
+ | _, (ty, left, right, o), _, _ ->
+ Printf.sprintf "{%s}: %s =(%s) %s" (CicPp.pp ty names)
+ (CicPp.pp left names) (string_of_comparison o)
+ (CicPp.pp right names)
)
;;
let meta_convertibility_eq eq1 eq2 =
- let _, (ty, left, right), _, _ = eq1
- and _, (ty', left', right'), _, _ = eq2 in
+ let _, (ty, left, right, _), _, _ = eq1
+ and _, (ty', left', right', _), _, _ = eq2 in
if ty <> ty' then
false
else if (left = left') && (right = right') then
subst
;;
-
+
+exception MatchingFailure;;
+
+let matching metasenv context t1 t2 ugraph =
+ try
+ let subst, metasenv, ugraph =
+ CicUnification.fo_unif metasenv context t1 t2 ugraph
+ in
+ let t' = CicMetaSubst.apply_subst subst t1 in
+ if not (meta_convertibility t1 t') then
+ raise MatchingFailure
+ else
+ let metas = metas_of_term t1 in
+ let fix_subst = function
+ | (i, (c, Cic.Meta (j, lc), ty)) when List.mem i metas ->
+ (j, (c, Cic.Meta (i, lc), ty))
+ | s -> s
+ in
+ let subst = List.map fix_subst subst in
+ subst, metasenv, ugraph
+ with e ->
+ raise MatchingFailure
+;;
+
+
let beta_expand ?(metas_ok=true) ?(match_only=false)
what type_of_what where context metasenv ugraph =
let module S = CicSubstitution in
let subst', metasenv', ugraph' =
(* Printf.printf "provo a unificare %s e %s\n" *)
(* (CicPp.ppterm (S.lift lift_amount what)) (CicPp.ppterm term); *)
- CicUnification.fo_unif metasenv context
- (S.lift lift_amount what) term ugraph
+ if match_only then
+ matching metasenv context term (S.lift lift_amount what) ugraph
+ else
+ CicUnification.fo_unif metasenv context
+ (S.lift lift_amount what) term ugraph
in
(* Printf.printf "Ok, trovato: %s\n\nwhat: %s" (CicPp.ppterm term) *)
(* (CicPp.ppterm (S.lift lift_amount what)); *)
(* Printf.printf "substitution:\n%s\n\n" (print_subst subst'); *)
(* Printf.printf "metasenv': %s\n" (print_metasenv metasenv'); *)
(* Printf.printf "metasenv: %s\n\n" (print_metasenv metasenv); *)
- if match_only then
- let t' = CicMetaSubst.apply_subst subst' term in
- if not (meta_convertibility term t') then (
-(* if print_info then ( *)
-(* let names = names_of_context context in *)
-(* Printf.printf *)
-(* "\nbeta_expand: term e t' sono diversi!:\n%s\n%s\n\n" *)
-(* (CicPp.pp term names) (CicPp.pp t' names) *)
-(* ); *)
- res, lifted_term
- ) else (
- let metas = metas_of_term term in
-(* let ok = ref false in *)
- let fix_subst = function
- | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas ->
-(* Printf.printf "fix_subst: scambio ?%d e ?%d\n" i j; *)
-(* ok := true; *)
- (j, (c, C.Meta (i, lc), ty))
- | s -> s
- in
- let subst' = List.map fix_subst subst' in
-(* if !ok then ( *)
-(* Printf.printf "aaa:\nterm: %s\nt'%s\n term subst': %s\n" *)
-(* (CicPp.ppterm term) *)
-(* (CicPp.ppterm t') *)
-(* (CicPp.ppterm (CicMetaSubst.apply_subst subst' term)) *)
-(* ); *)
- ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
- lifted_term)
- )
-(* ((C.Rel (1 + lift_amount), restore_subst context subst', *)
-(* metasenv', ugraph')::res, lifted_term) *)
- else
+(* if match_only then *)
+(* let t' = CicMetaSubst.apply_subst subst' term in *)
+(* if not (meta_convertibility term t') then ( *)
+(* res, lifted_term *)
+(* ) else ( *)
+(* let metas = metas_of_term term in *)
+(* let fix_subst = function *)
+(* | (i, (c, C.Meta (j, lc), ty)) when List.mem i metas -> *)
+(* (j, (c, C.Meta (i, lc), ty)) *)
+(* | s -> s *)
+(* in *)
+(* let subst' = List.map fix_subst subst' in *)
+(* ((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res, *)
+(* lifted_term) *)
+(* ) *)
+(* else *)
((C.Rel (1 + lift_amount), subst', metasenv', ugraph')::res,
lifted_term)
with e ->
type equality =
- Cic.term * (* proof *)
- (Cic.term * (* type *)
- Cic.term * (* left side *)
- Cic.term) * (* right side *)
- Cic.metasenv * (* environment for metas *)
- Cic.term list (* arguments *)
+ Cic.term * (* proof *)
+ (Cic.term * (* type *)
+ Cic.term * (* left side *)
+ Cic.term * (* right side *)
+ Utils.comparison) * (* ordering *)
+ Cic.metasenv * (* environment for metas *)
+ Cic.term list (* arguments *)
;;
match head with
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
Printf.printf "OK: %s\n" (CicPp.ppterm term);
- Some (p, (ty, t1, t2), newmetas, args), (newmeta+1)
+ let o = !Utils.compare_terms t1 t2 in
+ Some (p, (ty, t1, t2, o), newmetas, args), (newmeta+1)
| _ -> None, newmeta
)
| C.Appl [C.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- Some (C.Rel index,
- (ty, S.lift index t1, S.lift index t2), [], []), (newmeta+1)
+ let t1 = S.lift index t1
+ and t2 = S.lift index t2 in
+ let o = !Utils.compare_terms t1 t2 in
+ Some (C.Rel index, (ty, t1, t2, o), [], []), (newmeta+1)
| _ -> None, newmeta
in (
match do_find context term with
;;
-let fix_metas newmeta ((proof, (ty, left, right), menv, args) as equality) =
+let fix_metas newmeta ((proof, (ty, left, right, o), menv, args) as equality) =
let table = Hashtbl.create (List.length args) in
let newargs, _ =
List.fold_right
(function Cic.Meta (i, _) -> List.mem i metas | _ -> assert false) newargs
in
(newmeta + (List.length newargs) + 1,
- (repl proof, (ty, left, right), menv', newargs))
+ (repl proof, (ty, left, right, o), menv', newargs))
;;
let equality_of_term ?(eq_uri=HelmLibraryObjects.Logic.eq_URI) proof = function
| Cic.Appl [Cic.MutInd (uri, _, _); ty; t1; t2] when uri = eq_uri ->
- (proof, (ty, t1, t2), [], [])
+ let o = !Utils.compare_terms t1 t2 in
+ (proof, (ty, t1, t2, o), [], [])
| _ ->
raise TermIsNotAnEquality
;;
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), _, _ = target in
- let eqproof, (ty, t1, t2), newmetas, args = source in
+ 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
[]
else
let where, is_left =
- match compare_terms left right with
+ match t_order (* compare_terms left right *) with
| Lt -> right, false
| Gt -> left, true
| _ -> (
)
in
let metasenv' = newmetas @ metasenv in
- let result = compare_terms t1 t2 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), []
| _ -> assert false
in
let equation =
- if is_left then (eq_ty, newgoal, right)
- else (eq_ty, left, newgoal)
+ if is_left then (eq_ty, newgoal, right, compare_terms newgoal right)
+ else (eq_ty, left, newgoal, compare_terms left newgoal)
in
- (eqproof, equation, [], [])
+ (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
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 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
in
let metasenv' = metasenv @ newmetas @ newm' in
let beta_expand = beta_expand ~metas_ok:false in
- let cmp1 = compare_terms left right
- and cmp2 = compare_terms t1 t2 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
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), newmetas, newargs)
+ (neweqproof, (eq_ty, left, right, neworder), newmetas, newargs)
in
maxmeta := newmeta;
newequality
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), _, _ ->
+ | _, (_, left, right, _), _, _ ->
not (fst (CR.are_convertible context left right ugraph))
in
- !maxmeta, (List.filter ok (new1 @ new2 @ new3 @ new4))
+ (!maxmeta,
+ (List.filter ok (new1 @ new2 @ new3 @ new4)))
;;
let is_identity ((_, context, ugraph) as env) = function
- | ((_, (ty, left, right), _, _) as equality) ->
+ | ((_, (ty, left, right, _), _, _) as equality) ->
let res =
(left = right ||
(fst (CicReduction.are_convertible context left right ugraph)))
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 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
newmeta, target
else
let first_step, get_params =
- match compare_terms t1 t2 with
+ 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
first_step, get_params
in
let rec demodulate newmeta step metasenv target =
- let proof, (eq_ty, left, right), metas, args = target in
+ 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
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 *)
(function C.Meta (i, _) -> List.mem i m | _ -> assert false)
args
in
- newmeta, (newproof, (eq_ty, left, right), newmetasenv, newargs)
+ newmeta,
+ (newproof, (eq_ty, left, right, neworder), newmetasenv, newargs)
in
(* Printf.printf *)
(* "demodulate, newtarget: %s\ntarget was: %s\n" *)
*)
+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
+;;
+
+
+let extract_differing_subterms t1 t2 =
+ let module C = Cic in
+ let rec aux t1 t2 =
+ match t1, t2 with
+ | C.Appl l1, C.Appl l2 when (List.length l1) <> (List.length l2) ->
+ [(t1, t2)]
+ | C.Appl (h1::tl1), C.Appl (h2::tl2) ->
+ let res = List.concat (List.map2 aux tl1 tl2) in
+ if h1 <> h2 then
+ if res = [] then [(h1, h2)] else [(t1, t2)]
+ else
+ if List.length res > 1 then [(t1, t2)] else res
+ | t1, t2 ->
+ if t1 <> t2 then [(t1, t2)] else []
+ in
+ let res = aux t1 t2 in
+ match res with
+ | hd::[] -> Some hd
+ | _ -> None
+;;
projects / helm.git / blobdiff