Commit 8bfe56d0 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Debugging unification

parent 44bdb84c
......@@ -23,11 +23,6 @@
—————————————————————————————– Factorisation
(C ∨ l₁)σ
;)
def prop := fol.prop.
......@@ -80,7 +75,7 @@ def unify_atoms_pb : clauses.atom -> clauses.atom -> unif.unify_problem.
[p,l,l'] unify_atoms_pb (clauses.mk_atom p l) (clauses.mk_atom p l') -->
unif.unify_cons_terms (fol.pred_arity p) l l' unif.unify_nil.
def unify_atoms (a : clauses.atom) (a' : clauses.atom) : substitution :=
get_subst (unif.unify (unify_atoms_pb a a')).
get_subst (unif.unify' (unify_atoms_pb a a')).
(; a positive litteral is an atom, a negative litteral is the negation
of an atom. ;)
......
......@@ -131,9 +131,6 @@ def subst_proof_rev : s : substitution -> A : prop -> proof (subst_prop s A) ->
unify_result : Type.
unify_success : substitution -> unify_result.
unify_failure : unify_result.
(; This is technically the same type as substitution
list (Σ A : type. term A * term A)
......@@ -144,6 +141,10 @@ unify_problem : Type.
unify_nil : unify_problem.
unify_cons : A : type -> term A -> term A -> unify_problem -> unify_problem.
unify_result : Type.
unify_success : substitution -> unify_result.
unify_failure : unify_result.
def unify_cons_terms : As : types -> terms As -> terms As -> unify_problem -> unify_problem.
[pb] unify_cons_terms fol.nil_type fol.nil_term fol.nil_term pb --> pb
[A,As,a,as,a',as',pb]
......@@ -196,6 +197,17 @@ def subst_in_unify_problem : A : type -> term A -> term A -> unify_problem -> un
(subst_term (cons_subst A x a empty_subst) B b')
(subst_in_unify_problem A x a pb).
(; For debugging_purpose, a version of unify that outputs the
unification problem in case of failure ;)
unify_failure_problem : unify_problem -> unify_result.
def unify'_aux : unify_problem -> unify_result -> unify_result.
[s] unify'_aux _ (unify_success s) --> unify_success s
[pb] unify'_aux pb unify_failure --> unify_failure_problem pb.
def unify' (pb : unify_problem) :=
unify'_aux pb (unify pb).
A : type.
f : function.
......@@ -214,9 +226,9 @@ x : term A.
y : term A.
#SNF unify (unify_cons A x (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply a) x unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply a) unify_nil).
#SNF unify' (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) x) unify_nil).
#SNF unify (unify_cons A x x unify_nil).
#SNF unify (unify_cons A x y unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) y) unify_nil).
#SNF unify (unify_cons A (fun_apply f (fun_apply b) y) (fun_apply f y (fun_apply a)) unify_nil).
#SNF unify' (unify_cons A (fun_apply f (fun_apply b) y) (fun_apply f y (fun_apply a)) unify_nil).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment