From 6e1cc85031956563e6e345f70d30f101183b6fa2 Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Thu, 1 Aug 2019 18:17:46 +0200 Subject: [PATCH 01/35] Extending elaboration of a substitution from constraints --- kernel/basic.ml | 10 ++++++++++ kernel/basic.mli | 8 ++++++++ kernel/typing.ml | 42 +++++++++++++++++++++++++++++++++++------- 3 files changed, 53 insertions(+), 7 deletions(-) diff --git a/kernel/basic.ml b/kernel/basic.ml index 78df742b..42a805c3 100644 --- a/kernel/basic.ml +++ b/kernel/basic.ml @@ -150,6 +150,16 @@ let rev_mapi f l = let concat l1 = function [] -> l1 | l2 -> l1@l2 +let rec apply_n_times (n : int) (f : 'a -> 'a) (x : 'a) : 'a = + if n <= 0 then x else apply_n_times (n-1) f (f x) + +let index x = + let rec index_bis i a = function + | [] -> raise Not_found + | x :: tl when x = a -> i + | _ :: tl -> index_bis (i+1) a tl + in index_bis 0 x + (** {2 Printing functions} *) type 'a printer = Format.formatter -> 'a -> unit diff --git a/kernel/basic.mli b/kernel/basic.mli index 1fb7a769..663a6e60 100644 --- a/kernel/basic.mli +++ b/kernel/basic.mli @@ -120,6 +120,14 @@ val rev_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list val concat : 'a list -> 'a list -> 'a list (** [concat l1 l2] returns [l1 @ l2] (testing on l2 empty first) *) +val apply_n_times : int -> ('a -> 'a) -> 'a -> 'a +(** [apply_n_times n f x] returns [f (f... (f x)...)] with [n] application of [f]. *) + +val index : 'a -> 'a list -> int +(** [index x l] returns the index of the first occurrence of [x] in [l] if any. + Raises [Not_found] otherwise. + *) + (** {2 Printing functions} *) type 'a printer = Format.formatter -> 'a -> unit diff --git a/kernel/typing.ml b/kernel/typing.ml index 111c2b47..f93e2023 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -160,6 +160,39 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) if term_eq t1' t2' then keepon () else let warn () = fail (q,t1,t2); keepon () in + let applyDBCase t n x l q = + (* [lambdaLift [x1,...,xn] q t] generates x1 => ... => xn => t + if all the [xi]s are variables of De Bruijn index below [q] and + [t] does not contain any other variable which has a De Bruijn below + [q] *) + let lambdaLift (l : term list) (q : int) (t : term) : term = + (* If [l] is a list of distinct variables with an index smaller + than [q], [allDistinctBounds q [] l] returns the list of the + De Bruijn indices. Otherwise raises [Not_found]. + *) + let rec allDistinctBounds q acc = function + | [] -> acc + | DB (_,_,i)::tl -> + if i raise Not_found + in + let l_DBInd = allDistinctBounds q [] l in + let r = List.length l in + let sub lc id i k = + if i-k < q + then mk_DB lc id ((index (i-k) l_DBInd) + k) + else mk_DB lc id (i+r-q) + in + apply_n_times r (mk_Lam dloc dmark None) (Subst.apply_subst sub 0 t) + in + try (* Because of the [index] and [allDistinctBounds], + [lambdaLift] can raise [Not_found] *) + let t' = lambdaLift (x::l) q t in + pseudo_u sg fail (SS.add sigma (n-q) t') lst + with Not_found -> keepon () + in match t1', t2' with | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) @@ -183,7 +216,6 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) ( match unshift_reduce sg q t with None -> warn () | Some _ -> keepon ()) | t, Const (l,cst) when not (Signature.is_static sg l cst) -> ( match unshift_reduce sg q t with None -> warn () | Some _ -> keepon ()) - | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> let (n,t) = if n1 unit) (sigma:SS.t) : (int*term*term) if Subst.occurs n' t' then warn () else pseudo_u sg fail (SS.add sigma n' t') lst end - - | App (DB (_,_,n),_,_), _ when n >= q -> - if R.are_convertible sg t1' t2' then keepon () else warn () - | _ , App (DB (_,_,n),_,_) when n >= q -> - if R.are_convertible sg t1' t2' then keepon () else warn () - + | App (DB (_,_,n),x,l), t when n >= q -> applyDBCase t n x l q + | t, App (DB (_,_,n),x,l) when n >= q -> applyDBCase t n x l q | App (Const (l,cst),_,_), _ when not (Signature.is_static sg l cst) -> keepon () | _, App (Const (l,cst),_,_) when not (Signature.is_static sg l cst) -> keepon () From 314d364af4c15aac238d24479a1db0113d8a1cbc Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Thu, 1 Aug 2019 19:56:14 +0200 Subject: [PATCH 02/35] Extend pseudo unification, to pseudo-unify (x => A) and (x => B x) --- kernel/typing.ml | 39 ++++++++++++++++++--------------------- 1 file changed, 18 insertions(+), 21 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index f93e2023..1b3a63c6 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -160,7 +160,16 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) if term_eq t1' t2' then keepon () else let warn () = fail (q,t1,t2); keepon () in - let applyDBCase t n x l q = + let varCase def n t = + let n' = n-q in + match unshift_reduce sg q t with + | None -> def + | Some ut -> + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then warn () + else pseudo_u sg fail (SS.add sigma n' t') lst + in + let applyDBCase t n x l = (* [lambdaLift [x1,...,xn] q t] generates x1 => ... => xn => t if all the [xi]s are variables of De Bruijn index below [q] and [t] does not contain any other variable which has a De Bruijn below @@ -221,28 +230,16 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) then (n1,mk_DB l2 x2 (n2-q)) else (n2,mk_DB l1 x1 (n1-q)) in pseudo_u sg fail (SS.add sigma (n-q) t) lst + | DB (l1,x1,n), App(DB(_,_,m),x,l) when n>=q && m >=q -> + varCase (applyDBCase t1' m x l) n t2' | DB (_,_,n), t when n>=q -> - begin - let n' = n-q in - match unshift_reduce sg q t with - | None -> warn () - | Some ut -> - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then warn () - else pseudo_u sg fail (SS.add sigma n' t') lst - end + varCase (keepon ()) n t + | App(DB(_,_,m),x,l), DB (l1,x1,n) when n>=q && m >=q -> + varCase (applyDBCase t2' m x l) n t1' | t, DB (_,_,n) when n>=q -> - begin - let n' = n-q in - match unshift_reduce sg q t with - | None -> warn () - | Some ut -> - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then warn () - else pseudo_u sg fail (SS.add sigma n' t') lst - end - | App (DB (_,_,n),x,l), t when n >= q -> applyDBCase t n x l q - | t, App (DB (_,_,n),x,l) when n >= q -> applyDBCase t n x l q + varCase (keepon ()) n t + | App (DB (_,_,n),x,l), t when n >= q -> applyDBCase t n x l + | t, App (DB (_,_,n),x,l) when n >= q -> applyDBCase t n x l | App (Const (l,cst),_,_), _ when not (Signature.is_static sg l cst) -> keepon () | _, App (Const (l,cst),_,_) when not (Signature.is_static sg l cst) -> keepon () From bc78af4c6e9a8fcf043055651f857494fed589f3 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 08:37:04 +0100 Subject: [PATCH 03/35] Moved back to master. --- kernel/basic.ml | 10 ---------- kernel/basic.mli | 8 -------- kernel/typing.ml | 45 +-------------------------------------------- 3 files changed, 1 insertion(+), 62 deletions(-) diff --git a/kernel/basic.ml b/kernel/basic.ml index f9fadd7d..180424f7 100644 --- a/kernel/basic.ml +++ b/kernel/basic.ml @@ -150,16 +150,6 @@ let rev_mapi f l = let concat l1 = function [] -> l1 | l2 -> l1@l2 -let rec apply_n_times (n : int) (f : 'a -> 'a) (x : 'a) : 'a = - if n <= 0 then x else apply_n_times (n-1) f (f x) - -let index x = - let rec index_bis i a = function - | [] -> raise Not_found - | x :: tl when x = a -> i - | _ :: tl -> index_bis (i+1) a tl - in index_bis 0 x - (** {2 Printing functions} *) type 'a printer = Format.formatter -> 'a -> unit diff --git a/kernel/basic.mli b/kernel/basic.mli index 9ddfa192..033be8cb 100644 --- a/kernel/basic.mli +++ b/kernel/basic.mli @@ -127,14 +127,6 @@ val rev_mapi : (int -> 'a -> 'b) -> 'a list -> 'b list val concat : 'a list -> 'a list -> 'a list (** [concat l1 l2] returns [l1 @ l2] (testing on l2 empty first) *) -val apply_n_times : int -> ('a -> 'a) -> 'a -> 'a -(** [apply_n_times n f x] returns [f (f... (f x)...)] with [n] application of [f]. *) - -val index : 'a -> 'a list -> int -(** [index x l] returns the index of the first occurrence of [x] in [l] if any. - Raises [Not_found] otherwise. - *) - (** {2 Printing functions} *) type 'a printer = Format.formatter -> 'a -> unit diff --git a/kernel/typing.ml b/kernel/typing.ml index 200ce9bd..88d2cafc 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -152,8 +152,6 @@ let unshift_reduce sg q t = ( try Some (Subst.unshift q (R.snf sg t)) with Subst.UnshiftExn -> None ) -exception VarSurelyOccurs - (** Under [d] lambdas, checks whether term [te] *must* contain an occurence of any variable that satisfies the given predicate [p], *even when substituted or reduced*. @@ -165,6 +163,7 @@ exception VarSurelyOccurs of the [vars]. *) let sure_occur_check sg (d:int) (p:int -> bool) (te:term) : bool = + let exception VarSurelyOccurs in let rec aux = function | [] -> () | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) @@ -231,48 +230,6 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) if term_eq t1' t2' then keepon () else let warn () = fail (q,t1,t2); keepon () in - let varCase def n t = - let n' = n-q in - match unshift_reduce sg q t with - | None -> def - | Some ut -> - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then warn () - else pseudo_u sg fail (SS.add sigma n' t') lst - in - let applyDBCase t n x l = - (* [lambdaLift [x1,...,xn] q t] generates x1 => ... => xn => t - if all the [xi]s are variables of De Bruijn index below [q] and - [t] does not contain any other variable which has a De Bruijn below - [q] *) - let lambdaLift (l : term list) (q : int) (t : term) : term = - (* If [l] is a list of distinct variables with an index smaller - than [q], [allDistinctBounds q [] l] returns the list of the - De Bruijn indices. Otherwise raises [Not_found]. - *) - let rec allDistinctBounds q acc = function - | [] -> acc - | DB (_,_,i)::tl -> - if i raise Not_found - in - let l_DBInd = allDistinctBounds q [] l in - let r = List.length l in - let sub lc id i k = - if i-k < q - then mk_DB lc id ((index (i-k) l_DBInd) + k) - else mk_DB lc id (i+r-q) - in - apply_n_times r (mk_Lam dloc dmark None) (Subst.apply_subst sub 0 t) - in - try (* Because of the [index] and [allDistinctBounds], - [lambdaLift] can raise [Not_found] *) - let t' = lambdaLift (x::l) q t in - pseudo_u sg fail (SS.add sigma (n-q) t') lst - with Not_found -> keepon () - in match t1', t2' with | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) From 79e04f823f6f056e59c175c379be0da2e65814b1 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 11:18:46 +0100 Subject: [PATCH 04/35] Added challenging tests. --- tests/OK/binded_cstr.dk | 79 +++++++++++++++++++++++++++++++++++++++++ tests/OK/cstr.dk | 22 ++++++++++++ 2 files changed, 101 insertions(+) create mode 100644 tests/OK/binded_cstr.dk create mode 100644 tests/OK/cstr.dk diff --git a/tests/OK/binded_cstr.dk b/tests/OK/binded_cstr.dk new file mode 100644 index 00000000..1832f810 --- /dev/null +++ b/tests/OK/binded_cstr.dk @@ -0,0 +1,79 @@ +(; OK ;) + +A : Type. +a : A. +b : A. + +T : A -> Type. +t : x:A -> T x. + +def R : A -> A -> Type. +[x] R a x --> T x. + + +def f1 : x:(A->A) -> (z:A -> T (x z)) -> (z:A -> T (x z)). +[x] f1 x (z => t a) --> z => t a. + +def f2 : x:(A->A) -> (z:A -> T (x z)) -> T (x b). +[x] f2 x (z => t a) --> t a. + +def f3 : x:(A->A) -> (z:A -> T (x z)) -> (z:A -> T (x z)). +[x] f3 x (z => t z) --> z => t z. + +def f4 : x:(A->A) -> (z:A -> T (x z)) -> T (x b). +[x] f4 x (z => t z) --> t b. + + + +def g1 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). +[x,y] g1 x y (z => t a) (z => t a) --> z => t a. + +def g2 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). +[x,y] g2 x y (z => t a) (z => t a) --> z => t a. + +def g3 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). +[x,y] g3 x y (z => t z) (z => t a) --> z => t z. + +def g4 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). +[x,y] g4 x y (z => t z) (z => t a) --> z => t b. + + +def h1 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). +[x,y] h1 x y (z => t a) (z => t (x z)) --> z => t a. + +def h2 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). +[x,y] h2 x y (z => t a) (z => t (x z)) --> z => t a. + +def h3 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). +[x,y] h3 x y (z => t z) (z => t (x z)) --> z => t z. + +def h4 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). +[x,y] h4 x y (z => t z) (z => t (x z)) --> z => t b. + + + + +def g'1 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +[x,y] g'1 x y (z => t a) (z => t a) --> z => t a. + +def g'2 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). +[x,y] g'2 x y (z => t a) (z => t a) --> z => t a. + +def g'3 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +[x,y] g'3 x y (z => t a) (z => t z) --> z => t z. + +def g'4 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). +[x,y] g'4 x y (z => t a) (z => t z) --> z => t b. + + +def h'1 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +[x,y] h'1 x y (z => t (x z)) (z => t a) --> z => t a. + +def h'2 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). +[x,y] h'2 x y (z => t (x z)) (z => t a) --> z => t a. + +def h'3 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). +[x,y] h'3 x y (z => t (x z)) (z => t z) --> z => t z. + +def h'4 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). +[x,y] h'4 x y (z => t (x z)) (z => t z) --> z => t b. diff --git a/tests/OK/cstr.dk b/tests/OK/cstr.dk new file mode 100644 index 00000000..c89c6556 --- /dev/null +++ b/tests/OK/cstr.dk @@ -0,0 +1,22 @@ +(; OK ;) + +A : Type. +a : A. + +T : A -> Type. +t : x:A -> T x. + +def R : A -> A -> Type. +[x] R a x --> T x. + +def f : x:A -> y:A -> R x y -> T x -> T y. +[] f _ _ (t a) (t a) --> t a. + +def g : x:A -> y:A -> R x a -> T a -> T y. +[x,y] g x y (t y) (t x) --> t a. + +def h : x:A -> y:A -> T x -> R x y -> T y. +[] h _ _ (t a) (t a) --> t a. + +def i : x:A -> y:A -> T a -> R x a -> T y. +[x,y] i x y (t x) (t y) --> t a. From 6d07b00da47f432e439d216e4a78fb9f23ecee3c Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 11:23:01 +0100 Subject: [PATCH 05/35] Moved tests from type-preserv PR. --- tests/OK/{cstr.dk => first_order_cstr1.dk} | 0 tests/OK/higher_order_cstr1.dk | 25 +++++++++++++++++++ tests/OK/higher_order_cstr2.dk | 25 +++++++++++++++++++ .../{binded_cstr.dk => higher_order_cstr3.dk} | 0 4 files changed, 50 insertions(+) rename tests/OK/{cstr.dk => first_order_cstr1.dk} (100%) create mode 100644 tests/OK/higher_order_cstr1.dk create mode 100644 tests/OK/higher_order_cstr2.dk rename tests/OK/{binded_cstr.dk => higher_order_cstr3.dk} (100%) diff --git a/tests/OK/cstr.dk b/tests/OK/first_order_cstr1.dk similarity index 100% rename from tests/OK/cstr.dk rename to tests/OK/first_order_cstr1.dk diff --git a/tests/OK/higher_order_cstr1.dk b/tests/OK/higher_order_cstr1.dk new file mode 100644 index 00000000..383e3d15 --- /dev/null +++ b/tests/OK/higher_order_cstr1.dk @@ -0,0 +1,25 @@ +(; OK ;) + +N : Type. +A : Type. +T : A -> Type. + +P : (N -> A) -> Type. +p : f : (N -> A) -> P f. + +g : (x : N) -> f : (N -> A) -> T (f x). +def h : f : (N -> A) -> (x : N -> T (f x)) -> P (x => f x). + +(; The following rules are well-typed because + +we infer the constraint + (under 1 lambda) X x[0] = Y x[0] + +and we need to deduce + P (x => X x) = P (x => Y x) +;) + +[X,Y] h Y (z => g z X ) --> p (x => X x). +[X,Y] h (y => Y y) (z => g z X ) --> p (x => X x). +[X,Y] h Y (z => g z (x => X x)) --> p (x => X x). +[X,Y] h (y => Y y) (z => g z (x => X x)) --> p (x => X x). diff --git a/tests/OK/higher_order_cstr2.dk b/tests/OK/higher_order_cstr2.dk new file mode 100644 index 00000000..c23ca54c --- /dev/null +++ b/tests/OK/higher_order_cstr2.dk @@ -0,0 +1,25 @@ +(; OK ;) + +N : Type. +0 : N. + +A : Type. +T : A -> Type. +p : f : (N -> A) -> T (f 0). + +g : (x : N) -> f : (N -> A) -> T (f x). +def h : f : (N -> A) -> (x : N -> T (f x)) -> T (f 0). + +(; The following rules are well-typed because + +we infer the constraint + (under 1 lambda) X x[0] = Y x[0] + +and we need to deduce + T (X 0) = T (Y 0) +;) + +[X,Y] h Y (z => g z X ) --> p X. +[X,Y] h (y => Y y) (z => g z X ) --> p X. +[X,Y] h Y (z => g z (x => X x)) --> p (x => X x). +[X,Y] h (y => Y y) (z => g z (x => X x)) --> p (x => X x). diff --git a/tests/OK/binded_cstr.dk b/tests/OK/higher_order_cstr3.dk similarity index 100% rename from tests/OK/binded_cstr.dk rename to tests/OK/higher_order_cstr3.dk From 313c7c3d2d2b9ed3de93873eb49a9ea670a02d08 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 13:41:53 +0100 Subject: [PATCH 06/35] First implementation passing first order test. --- kernel/typing.ml | 108 ++++++++++++++++++++++++++++++----------------- 1 file changed, 70 insertions(+), 38 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 88d2cafc..2ddb7aa6 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -220,46 +220,58 @@ let gather_free_vars (d:int) (terms:term list) : bool array = | _ -> aux tl in aux (List.map (fun t -> (0,t)) terms); vars -let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) list -> SS.t = function - | [] -> sigma +type cstr = int*term*term +(* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) + +type solver = + { + subst : SS.t; + ho_subst : (int*int*term) list; + unsolved : cstr list; + unsatisf : cstr list + } + +let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function + | [] -> (flag, s) | (q,t1,t2)::lst -> begin - let t1' = R.whnf sg (SS.apply sigma q t1) in - let t2' = R.whnf sg (SS.apply sigma q t2) in - let keepon () = pseudo_u sg fail sigma lst in - if term_eq t1' t2' then keepon () + let t1' = R.whnf sg (SS.apply s.subst q t1) in + let t2' = R.whnf sg (SS.apply s.subst q t2) in + let dropped () = pseudo_u sg flag s lst in + let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in + let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in + if term_eq t1' t2' then dropped () else - let warn () = fail (q,t1,t2); keepon () in match t1', t2' with | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) - | _, Kind | Kind, _ |_, Type _ | Type _, _ -> warn () + | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () | Pi (_,_,a,b), Pi (_,_,a',b') -> - pseudo_u sg fail sigma ((q,a,a')::(q+1,b,b')::lst) + pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) | Lam (_,_,_,b), Lam (_,_,_,b') -> - pseudo_u sg fail sigma ((q+1,b,b')::lst) + pseudo_u sg true s ((q+1,b,b')::lst) (* Potentially eta-equivalent terms *) | Lam (_,i,_,b), a when !Reduction.eta -> let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg fail sigma ((q+1,b,b')::lst) + pseudo_u sg true s ((q+1,b,b')::lst) | a, Lam (_,i,_,b) when !Reduction.eta -> let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg fail sigma ((q+1,b,b')::lst) + pseudo_u sg true s ((q+1,b,b')::lst) (* A definable symbol is only be convertible with closed terms *) | Const (l,cst), t when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then warn() else keepon() + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() | t, Const (l,cst) when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then warn() else keepon() + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() (* X = Y : map either X to Y or Y to X *) | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> let (n,t) = if n1 unit) (sigma:SS.t) : (int*term*term) 3) otherwise drop the constraint *) | DB (_,_,n), t when n>=q -> if sure_occur_check sg q (fun k -> k <= q || k = n) t - then warn() + then unsatisf() else begin match unshift_reduce sg q t with - | None -> keepon() + | None -> unsolved() | Some ut -> let n' = n-q in let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then warn() - else pseudo_u sg fail (SS.add sigma n' t') lst + if Subst.occurs n' t' then unsatisf() + else pseudo_u sg true {s with subst=SS.add s.subst n' t'} lst end | t, DB (_,_,n) when n>=q -> if sure_occur_check sg q (fun k -> k <= q || k = n) t - then warn() + then unsatisf() else begin match unshift_reduce sg q t with - | None -> keepon() + | None -> unsolved() | Some ut -> let n' = n-q in let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then warn() - else pseudo_u sg fail (SS.add sigma n' t') lst + if Subst.occurs n' t' then unsatisf() + else pseudo_u sg true {s with subst=SS.add s.subst n' t'} lst end (* f t1 ... tn / X t1 ... tn = u @@ -296,29 +308,43 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) *) | App (DB (_,_,n),a,args), t when n >= q -> let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t then warn() else keepon() + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() | t, App (DB (_,_,n),a,args) when n >= q -> let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t then warn() else keepon() + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t then warn() else keepon() + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() | t, App (Const (l,cst),a,args) when not (Signature.is_static sg l cst) -> let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t then warn() else keepon() + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() | App (f,a,args), App (f',a',args') -> (* f = Kind | Type | DB n when n warn () (* Different number of arguments. *) - | Some lst2 -> pseudo_u sg fail sigma ((q,f,f')::(q,a,a')::lst2) + | None -> unsatisf() (* Different number of arguments. *) + | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) end - | _, _ -> warn () + | _, _ -> unsatisf() end +let solve_cstr sg cstr = + let rec process_solver sol = + match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with + | false, s -> s + | true, sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} + in + process_solver {subst=SS.identity;ho_subst=[];unsolved=cstr;unsatisf=[]} + + + (* **** TYPE CHECKING/INFERENCE FOR PATTERNS ******************************** *) type constraints = (int * term * term) list @@ -405,6 +431,8 @@ and infer_pattern_aux sg let ctx = (LList.lst sigma)@(pc_to_context_wp delta) in raise (TypingError (ProductExpected (f,ctx,ty_f))) + + and check_pattern sg (delta:partial_context) (sigma:context2) (exp_ty:typ) (lst:constraints) (pat:pattern) : partial_context * constraints = Debug.(debug D_rule "Checking pattern %a:%a" pp_pattern pat pp_term exp_ty); @@ -506,17 +534,21 @@ let check_type_annotations sg sub typed_ctx annot_ctx = let check_rule sg (rule:partially_typed_rule) : SS.t * typed_rule = Debug.(debug D_rule "Inferring variables type and constraints from LHS"); - let fail = if !fail_on_unsatisfiable_constraints - then (fun x -> raise (TypingError (UnsatisfiableConstraints (rule,x)))) - else (fun (q,t1,t2) -> - Debug.(debug D_warn "At %a: unsatisfiable constraint: %a ~ %a%s" - pp_loc (get_loc_rule rule) - pp_term t1 pp_term t2 - (if q > 0 then Format.sprintf " (under %i abstractions)" q else ""))) in let delta = pc_make rule.ctx in let (ty_le,delta,lst) = infer_pattern sg delta LList.nil [] rule.pat in assert ( delta.padding == 0 ); - let sub = SS.mk_idempotent (pseudo_u sg fail SS.identity lst) in + let sol = solve_cstr sg lst in + ( match sol.unsatisf with + | [] -> () + | (q,t1,t2)::_ -> + if !fail_on_unsatisfiable_constraints + then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) + else Debug.(debug D_warn "At %a: unsatisfiable constraint: %a ~ %a%s" + pp_loc (get_loc_rule rule) + pp_term t1 pp_term t2 + (if q > 0 then Format.sprintf " (under %i abstractions)" q else ""))); + + let sub = sol.subst in let ri2 = SS.apply sub 0 rule.rhs in let ty_le2 = SS.apply sub 0 ty_le in let ctx = LList.lst delta.pctx in From fa40d81ac4214c2ff9005e86651d371775555a4d Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 14:31:59 +0100 Subject: [PATCH 07/35] Extended substitution. --- kernel/exsubst.ml | 76 ++++++++++++++++++++++++++++++++++++++++++++++ kernel/exsubst.mli | 51 +++++++++++++++++++++++++++++++ 2 files changed, 127 insertions(+) create mode 100644 kernel/exsubst.ml create mode 100644 kernel/exsubst.mli diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml new file mode 100644 index 00000000..d71b7bde --- /dev/null +++ b/kernel/exsubst.ml @@ -0,0 +1,76 @@ +open Basic +open Format +open Term + +type ex_substitution = loc -> ident -> int -> int -> int -> term + +let apply_exsubst (subst:ex_substitution) : int -> term -> term = + let ct = ref 0 in + (* aux increments this counter every time a substitution occurs. + * Terms are reused when no substitution occurs in recursive calls. *) + let rec aux k t = match t with (* k counts the number of local lambda abstractions *) + | DB (l,x,n) when n >= k -> (* a free variable *) + ( try let res = subst l x n 0 k in incr ct; res with Not_found -> t) + | App (DB (l,x,n),a,args) when n >= k -> (* an applied free variable *) + ( try + let res = subst l x n (1+(List.length args)) k in + incr ct; + let a', args' = aux k a, List.map (aux k) args in + mk_App res a' args' + with Not_found -> t) + | App (f,a,args) -> + let ct' = !ct in + let f', a', args' = aux k f, aux k a, List.map (aux k) args in + if !ct = ct' then t else mk_App f' a' args' + | Lam (l,x,a,f) -> + let ct' = !ct in + let a', f' = map_opt (aux k) a, aux (k+1) f in + if !ct = ct' then t else mk_Lam l x a' f' + | Pi (l,x,a,b) -> + let ct' = !ct in + let a', b' = aux k a, aux (k+1) b in + if !ct = ct' then t else mk_Pi l x a' b' + | _ -> t + in aux + +module IntMap = Map.Make( + struct + type t = int + let compare = compare + end) + +module ExSubst = +struct + type t = (int*term) IntMap.t + let identity = IntMap.empty + + let is_identity = IntMap.is_empty + + let subst (sigma:t) = + fun _ _ n nargs k -> + let (argmin,t) = IntMap.find (n-k) sigma in + if nargs >= argmin then Subst.shift k t else raise Not_found + let subst2 (sigma:t) (i:int) = + fun _ _ n nargs k -> + let (argmin,t) = IntMap.find (n+i+1-k) sigma in + if nargs >= argmin then Subst.shift k (Subst.unshift (i+1) t) else raise Not_found + + let apply (sigma:t) : int -> int*term -> int*term = + if is_identity sigma then (fun _ t -> t) else + (fun i (n,t) -> n,apply_exsubst (subst sigma) i t) + + let add (sigma:t) (n:int) (nargs:int) (t:term) : t = + assert ( not (IntMap.mem n sigma) ); + IntMap.add n (nargs,t) sigma + + let rec mk_idempotent (sigma:t) : t = + let sigma2:t = IntMap.map (apply sigma 0) sigma in + if IntMap.equal (fun (n1,t1) (n2,t2) -> n1 = n2 && term_eq t1 t2) sigma sigma2 then sigma + else mk_idempotent sigma2 + + let pp (name:(int->ident)) (fmt:formatter) (sigma:t) : unit = + let pp_aux i (n,t) = + fprintf fmt " %a[%i](...%i...) -> %a(...)\n" pp_ident (name i) i n pp_term t in + IntMap.iter pp_aux sigma + +end diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli new file mode 100644 index 00000000..a55cfd6f --- /dev/null +++ b/kernel/exsubst.mli @@ -0,0 +1,51 @@ +open Term + +(** An extended substitution is a function mapping + - a variable (location, identifier and DB index) + - applied to a given number of arguments + - under a given number of lambda abstractions + to a term. + A substitution raises Not_found meaning that the variable is not subsituted. *) +type ex_substitution = Basic.loc -> Basic.ident -> int -> int -> int -> term + +(** [apply_subst subst n t] applies [subst] to [t] under [n] lambda abstractions. + - Variables with DB index [k] < [n] are considered "locally bound" and are never substituted. + - Variables with DB index [k] >= [n] may be substituted if [k-n] is mapped in [sigma]. *) +val apply_exsubst : ex_substitution -> int -> term -> term + +(** This modules implements extended substitution of DB variables in a term. + This is typically used to: + 1) infer a "most general" typing substitution from constraints gathered while + inferring the type of the LHS of a rule. + 2) apply the substitution to the RHS of the rule before typechecking it. +*) +module ExSubst : +sig + type t + + val identity : t + (** Empty substitution *) + + val is_identity : t -> bool + (** Checks emptyness *) + + val add : t -> int -> int -> term -> t + (** [add sigma n t] returns the substitution [sigma] with the extra mapping [n] -> [t]. *) + + val subst : t -> ex_substitution + (** Provides substitution from Subst instance. *) + + val subst2 : t -> int -> ex_substitution + (** Provides special substitution from Subst instance. *) + + val apply : t -> int -> int*term -> int*term + (** [apply sigma n t] applies the subsitution [sigma] to [t] considered + under [n] lambda abstractions. *) + + val mk_idempotent : t -> t + (** [mk_idempotent sigma] successively applies sigma to its mapped terms until this operation + has no effect anymore. *) + + val pp : (int->Basic.ident) -> t Basic.printer + (** Prints the substitution using given naming function *) +end From 61ee700505c982697d7ba99f15dce218989f39fc Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 14:39:52 +0100 Subject: [PATCH 08/35] Used extended substitutions. --- api/env.ml | 4 ++-- api/env.mli | 2 +- api/processor.ml | 2 +- kernel/exsubst.ml | 9 ++++----- kernel/exsubst.mli | 2 +- kernel/typing.ml | 12 +++++------- kernel/typing.mli | 2 +- 7 files changed, 15 insertions(+), 18 deletions(-) diff --git a/api/env.ml b/api/env.ml index dc37b112..88084d8b 100644 --- a/api/env.ml +++ b/api/env.ml @@ -62,7 +62,7 @@ sig val import : loc -> mident -> unit val declare : loc -> ident -> Signature.staticity -> term -> unit val define : loc -> ident -> bool -> term -> term option -> unit - val add_rules : Rule.partially_typed_rule list -> (Subst.Subst.t * Rule.typed_rule) list + val add_rules : Rule.partially_typed_rule list -> (Exsubst.ExSubst.t * Rule.typed_rule) list val infer : ?ctx:typed_context -> term -> term val check : ?ctx:typed_context -> term -> term -> unit @@ -190,7 +190,7 @@ struct try _define lc id op te ty_opt with e -> raise_as_env lc e - let add_rules (rules: partially_typed_rule list) : (Subst.Subst.t * typed_rule) list = + let add_rules (rules: partially_typed_rule list) : (Exsubst.ExSubst.t * typed_rule) list = try let rs2 = List.map (T.check_rule !sg) rules in _add_rules rules; diff --git a/api/env.mli b/api/env.mli index 4aebf236..3095129f 100644 --- a/api/env.mli +++ b/api/env.mli @@ -88,7 +88,7 @@ sig val define : loc -> ident -> bool -> term -> term option -> unit (** [define l id body ty] defined the symbol [id] of type [ty] to be an alias of [body]. *) - val add_rules : Rule.partially_typed_rule list -> (Subst.Subst.t * Rule.typed_rule) list + val add_rules : Rule.partially_typed_rule list -> (Exsubst.ExSubst.t * Rule.typed_rule) list (** [add_rules rule_lst] adds a list of rule to a symbol. All rules must be on the same symbol. *) diff --git a/api/processor.ml b/api/processor.ml index 82d40430..77985637 100644 --- a/api/processor.ml +++ b/api/processor.ml @@ -36,7 +36,7 @@ struct let rs = E.add_rules rs in List.iter (fun (s,r) -> Debug.debug Debug.D_notice "%a@.with the following constraints: %a" - pp_typed_rule r (Subst.Subst.pp (fun n -> let _,n,_ = List.nth r.ctx n in n)) s) rs + pp_typed_rule r (Exsubst.ExSubst.pp (fun n -> let _,n,_ = List.nth r.ctx n in n)) s) rs | Eval(_,red,te) -> let te = E.reduction ~red te in Format.printf "%a@." Printer.print_term te diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index d71b7bde..bb7da182 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -55,16 +55,15 @@ struct let (argmin,t) = IntMap.find (n+i+1-k) sigma in if nargs >= argmin then Subst.shift k (Subst.unshift (i+1) t) else raise Not_found - let apply (sigma:t) : int -> int*term -> int*term = - if is_identity sigma then (fun _ t -> t) else - (fun i (n,t) -> n,apply_exsubst (subst sigma) i t) + let apply (sigma:t) : int -> term -> term = + if is_identity sigma then (fun _ t -> t) else apply_exsubst (subst sigma) let add (sigma:t) (n:int) (nargs:int) (t:term) : t = - assert ( not (IntMap.mem n sigma) ); + assert ( not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs ); IntMap.add n (nargs,t) sigma let rec mk_idempotent (sigma:t) : t = - let sigma2:t = IntMap.map (apply sigma 0) sigma in + let sigma2:t = IntMap.map (fun (n,t) -> n,apply sigma 0 t) sigma in if IntMap.equal (fun (n1,t1) (n2,t2) -> n1 = n2 && term_eq t1 t2) sigma sigma2 then sigma else mk_idempotent sigma2 diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli index a55cfd6f..4317d219 100644 --- a/kernel/exsubst.mli +++ b/kernel/exsubst.mli @@ -38,7 +38,7 @@ sig val subst2 : t -> int -> ex_substitution (** Provides special substitution from Subst instance. *) - val apply : t -> int -> int*term -> int*term + val apply : t -> int -> term -> term (** [apply sigma n t] applies the subsitution [sigma] to [t] considered under [n] lambda abstractions. *) diff --git a/kernel/typing.ml b/kernel/typing.ml index 2ddb7aa6..c951f90b 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -3,7 +3,7 @@ open Format open Rule open Term -module SS = Subst.Subst +module SS = Exsubst.ExSubst type Debug.flag += D_typeChecking | D_rule let _ = Debug.register_flag D_typeChecking "TypeChecking" @@ -271,7 +271,7 @@ let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function let (n,t) = if n1 bool*solver = function let n' = n-q in let t' = if Subst.occurs n' ut then ut else R.snf sg ut in if Subst.occurs n' t' then unsatisf() - else pseudo_u sg true {s with subst=SS.add s.subst n' t'} lst + else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst end | t, DB (_,_,n) when n>=q -> if sure_occur_check sg q (fun k -> k <= q || k = n) t @@ -299,7 +299,7 @@ let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function let n' = n-q in let t' = if Subst.occurs n' ut then ut else R.snf sg ut in if Subst.occurs n' t' then unsatisf() - else pseudo_u sg true {s with subst=SS.add s.subst n' t'} lst + else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst end (* f t1 ... tn / X t1 ... tn = u @@ -431,8 +431,6 @@ and infer_pattern_aux sg let ctx = (LList.lst sigma)@(pc_to_context_wp delta) in raise (TypingError (ProductExpected (f,ctx,ty_f))) - - and check_pattern sg (delta:partial_context) (sigma:context2) (exp_ty:typ) (lst:constraints) (pat:pattern) : partial_context * constraints = Debug.(debug D_rule "Checking pattern %a:%a" pp_pattern pat pp_term exp_ty); @@ -506,7 +504,7 @@ let pp_context_inline fmt ctx = let subst_context (sub:SS.t) (ctx:typed_context) : typed_context = if SS.is_identity sub then ctx else - let apply_subst i (l,x,ty) = (l,x,Subst.apply_subst (SS.subst2 sub i) 0 ty) in + let apply_subst i (l,x,ty) = (l,x,Exsubst.apply_exsubst (SS.subst2 sub i) 0 ty) in List.mapi apply_subst ctx let check_type_annotations sg sub typed_ctx annot_ctx = diff --git a/kernel/typing.mli b/kernel/typing.mli index 853a92ec..12239727 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -54,7 +54,7 @@ module type S = sig val inference : Signature.t -> term -> typ (** [inference sg ctx te] infers a type for the term [te] in empty context. *) - val check_rule : Signature.t -> partially_typed_rule -> Subst.Subst.t * typed_rule + val check_rule : Signature.t -> partially_typed_rule -> Exsubst.ExSubst.t * typed_rule (** [check_rule sg ru] checks that a rule is well-typed. *) end From 3f03e094a88f44b7628ec11bce289cfd85f5ed5d Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 6 Dec 2019 15:06:10 +0100 Subject: [PATCH 09/35] Started using exsubst in typing. Some bugs. --- kernel/exsubst.ml | 5 ++++- kernel/typing.ml | 30 ++++++++++++++++++++++++++++-- tests/OK/higher_order_cstr1.dk | 10 +++++----- 3 files changed, 37 insertions(+), 8 deletions(-) diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index bb7da182..052e2e8d 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -59,8 +59,11 @@ struct if is_identity sigma then (fun _ t -> t) else apply_exsubst (subst sigma) let add (sigma:t) (n:int) (nargs:int) (t:term) : t = +(* assert ( not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs ); - IntMap.add n (nargs,t) sigma +*) + if not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs + then IntMap.add n (nargs,t) sigma else sigma let rec mk_idempotent (sigma:t) : t = let sigma2:t = IntMap.map (fun (n,t) -> n,apply sigma 0 t) sigma in diff --git a/kernel/typing.ml b/kernel/typing.ml index c951f90b..03687ed9 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -231,6 +231,12 @@ type solver = unsatisf : cstr list } +let try_solve q args t = + try + let dbs = List.map (function DB(_,_,n) -> n | _ -> raise Matching.NotUnifiable) args in + Some (Matching.solve q (LList.of_list dbs) t) + with Matching.NotUnifiable -> None + let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function | [] -> (flag, s) | (q,t1,t2)::lst -> @@ -309,11 +315,31 @@ let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function | App (DB (_,_,n),a,args), t when n >= q -> let occs = gather_free_vars q (a::args) in if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() + else pseudo_u sg true + {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst + end | t, App (DB (_,_,n),a,args) when n >= q -> let occs = gather_free_vars q (a::args) in if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() + else pseudo_u sg true + {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst + end | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> let occs = gather_free_vars q (a::args) in if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t diff --git a/tests/OK/higher_order_cstr1.dk b/tests/OK/higher_order_cstr1.dk index 383e3d15..bfd06b24 100644 --- a/tests/OK/higher_order_cstr1.dk +++ b/tests/OK/higher_order_cstr1.dk @@ -8,7 +8,7 @@ P : (N -> A) -> Type. p : f : (N -> A) -> P f. g : (x : N) -> f : (N -> A) -> T (f x). -def h : f : (N -> A) -> (x : N -> T (f x)) -> P (x => f x). +def h : f : (N -> A) -> (x : N -> T (f x)) -> P (x:N => f x). (; The following rules are well-typed because @@ -19,7 +19,7 @@ and we need to deduce P (x => X x) = P (x => Y x) ;) -[X,Y] h Y (z => g z X ) --> p (x => X x). -[X,Y] h (y => Y y) (z => g z X ) --> p (x => X x). -[X,Y] h Y (z => g z (x => X x)) --> p (x => X x). -[X,Y] h (y => Y y) (z => g z (x => X x)) --> p (x => X x). +[X,Y] h Y (z => g z X ) --> p (x:N => X x). +[X,Y] h (y => Y y) (z => g z X ) --> p (x:N => X x). +[X,Y] h Y (z => g z (x => X x)) --> p (x:N => X x). +[X,Y] h (y => Y y) (z => g z (x => X x)) --> p (x:N => X x). From 9262f1e36a8c14b13488e9ad91898407a30c01a4 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 10 Dec 2019 14:22:10 +0100 Subject: [PATCH 10/35] Fixed criteria and tests. --- kernel/typing.ml | 4 ++-- tests/KO/SR_unsat_a2_2.dk | 32 ++++++++++++++++++++++++++++++++ tests/OK/SR_sat.dk | 6 +++--- 3 files changed, 37 insertions(+), 5 deletions(-) create mode 100644 tests/KO/SR_unsat_a2_2.dk diff --git a/kernel/typing.ml b/kernel/typing.ml index 03687ed9..e1092d5b 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -322,7 +322,7 @@ let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function | Some ut -> let n' = n-q in let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() + if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) else pseudo_u sg true {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst end @@ -336,7 +336,7 @@ let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function | Some ut -> let n' = n-q in let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() + if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) else pseudo_u sg true {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst end diff --git a/tests/KO/SR_unsat_a2_2.dk b/tests/KO/SR_unsat_a2_2.dk new file mode 100644 index 00000000..5da1301d --- /dev/null +++ b/tests/KO/SR_unsat_a2_2.dk @@ -0,0 +1,32 @@ +(; KO 108 --type-lhs ;) + +A : Type. +T : A -> Type. +t : a:A -> T a. + +a : A. +def b : A -> A -> A. + c : A -> A -> A. + +(; We build definitions with types containing an expression relying on + 2 matching variables + 2 locally bound variables + Generated constraints are not necessary to check the rules but should + generating an "unsatisfiable constraints" warning and fail + when using the --type-lhs flag. + + See SR_sat.dk for examples of satisfiable constraints. +;) + +(; Terms that *must* contain x and *must* contain y + are convertible with + terms that *must* or *may* contain x + and *must* or *may* contain y ;) +def a2 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c (c (c a x) a) (c a y))) -> Type. +[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y))) --> A. +(; From the following constraints: + Y x = c (c a x) a + Y y = c a y + We infer + c a y = c (c a x) a + which is obviously unsatisfiable +;) diff --git a/tests/OK/SR_sat.dk b/tests/OK/SR_sat.dk index 976659cd..f637ec9b 100644 --- a/tests/OK/SR_sat.dk +++ b/tests/OK/SR_sat.dk @@ -93,9 +93,9 @@ def f3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c a a)) -> Type. (; must / must ;) [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c (c a x) a) (c a y))) --> A. (; must / may ;) -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (X x y))) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (b y y))) --> A. +[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (b y y))) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (b x y))) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (b (c y a) y))) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (b x (c y a)))) --> A. @@ -107,7 +107,7 @@ def f3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c a a)) -> Type. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (Y y) )) --> A. +[X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y x) (X x y) )) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x y) (Y y) )) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b x x) (X x y) )) --> A. [X,Y] a2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (b y x) (b (c y y) a) )) --> A. @@ -169,7 +169,7 @@ def f3 : X:(A->A->A) -> Y:(A->A) -> (x:A->y:A-> T (c a a)) -> Type. [X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (c a x) y )) --> A. [X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (b y y) x )) --> A. [X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (b (Y y) x )) --> A. -[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) (Y x) )) --> A. +[X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) (Y x) )) --> A. [X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (Y y) (b x x) )) --> A. [X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (X x y) (b a x) )) --> A. [X,Y] b2 (x=>y=>X x y) (y=>Y y) ( x => y => t (c (c a a) (b y x) )) --> A. From 0af6a6ca2886f88c5e46ca679968bbc107aecb13 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 10 Dec 2019 16:48:47 +0100 Subject: [PATCH 11/35] Added FIXME comment. --- kernel/typing.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index e1092d5b..49cc6573 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -573,8 +573,7 @@ let check_rule sg (rule:partially_typed_rule) : SS.t * typed_rule = (if q > 0 then Format.sprintf " (under %i abstractions)" q else ""))); let sub = sol.subst in - let ri2 = SS.apply sub 0 rule.rhs in - let ty_le2 = SS.apply sub 0 ty_le in + let ty_le2 = SS.apply sub 0 ty_le in let ctx = LList.lst delta.pctx in let ctx2 = try subst_context sub ctx @@ -586,6 +585,11 @@ let check_rule sg (rule:partially_typed_rule) : SS.t * typed_rule = debug D_rule "Tried inferred typing substitution: %a" (SS.pp ctx_name) sub); raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) ) ) in + (* FIXME: Why is the RHS substituted ?! + Instead we should keep the original RHS and perform a check *modulo a substitution* + This simply means extend the check function to apply the substitution to all infered + types. *) + let ri2 = SS.apply sub 0 rule.rhs in Debug.(debug D_rule "Typechecking rule"); check sg ctx2 ri2 ty_le2; check_type_annotations sg sub ctx2 rule.ctx; From ce4791e271cfe239c6bfcad782d52890639bc7ee Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Tue, 10 Dec 2019 17:24:53 +0100 Subject: [PATCH 12/35] Indentation --- kernel/typing.ml | 844 +++++++++++++++++++++++------------------------ 1 file changed, 422 insertions(+), 422 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 49cc6573..3db1a806 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -64,8 +64,8 @@ struct | Type _ -> a::ctx | Kind when !coc -> a::ctx | ty_a -> - let (_,_,te) = a in - raise (TypingError (ConvertibilityError (te, ctx, mk_Type dloc, ty_a))) + let (_,_,te) = a in + raise (TypingError (ConvertibilityError (te, ctx, mk_Type dloc, ty_a))) (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) @@ -77,21 +77,21 @@ struct | DB (l,x,n) -> get_type ctx l x n | Const (l,cst) -> Signature.get_type sg l cst | App (f,a,args) -> - snd (List.fold_left (check_app sg ctx) (f,infer sg ctx f) (a::args)) + snd (List.fold_left (check_app sg ctx) (f,infer sg ctx f) (a::args)) | Pi (l,x,a,b) -> - let ty_a = infer sg ctx a in - let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer sg ctx2 b in - ( match ty_b with - | Kind | Type _ -> ty_b - | _ -> raise (TypingError (SortExpected (b, ctx2, ty_b))) ) + let ty_a = infer sg ctx a in + let ctx2 = extend_ctx (l,x,a) ctx ty_a in + let ty_b = infer sg ctx2 b in + ( match ty_b with + | Kind | Type _ -> ty_b + | _ -> raise (TypingError (SortExpected (b, ctx2, ty_b))) ) | Lam (l,x,Some a,b) -> - let ty_a = infer sg ctx a in - let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer sg ctx2 b in - ( match ty_b with - | Kind -> raise (TypingError (InexpectedKind (b, ctx2))) - | _ -> mk_Pi l x a ty_b ) + let ty_a = infer sg ctx a in + let ctx2 = extend_ctx (l,x,a) ctx ty_a in + let ty_b = infer sg ctx2 b in + ( match ty_b with + | Kind -> raise (TypingError (InexpectedKind (b, ctx2))) + | _ -> mk_Pi l x a ty_b ) | Lam (l,_,None,_) -> raise (TypingError (DomainFreeLambda l)) and check sg (ctx:typed_context) (te:term) (ty_exp:typ) : unit = @@ -99,33 +99,33 @@ struct pp_loc (get_loc te) pp_term te pp_term ty_exp); match te with | Lam (l,x,None,b) -> - begin - match R.whnf sg ty_exp with - | Pi (_,_,a,ty_b) -> check sg ((l,x,a)::ctx) b ty_b - | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) - end + begin + match R.whnf sg ty_exp with + | Pi (_,_,a,ty_b) -> check sg ((l,x,a)::ctx) b ty_b + | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) + end | Lam (l,x,Some a,b) -> - begin - match R.whnf sg ty_exp with - | Pi (_,_,a',ty_b) -> - ignore(infer sg ctx a); - if not (R.are_convertible sg a a') - then raise (TypingError (ConvertibilityError ((mk_DB l x 0),ctx,a',a))) - else check sg ((l,x,a)::ctx) b ty_b - | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) - end + begin + match R.whnf sg ty_exp with + | Pi (_,_,a',ty_b) -> + ignore(infer sg ctx a); + if not (R.are_convertible sg a a') + then raise (TypingError (ConvertibilityError ((mk_DB l x 0),ctx,a',a))) + else check sg ((l,x,a)::ctx) b ty_b + | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) + end | _ -> - let ty_inf = infer sg ctx te in - Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" - pp_term ty_inf pp_term ty_exp); - if not (R.are_convertible sg ty_inf ty_exp) then - let ty_exp' = rename_vars_with_typed_context ctx ty_exp in - raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) + let ty_inf = infer sg ctx te in + Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" + pp_term ty_inf pp_term ty_exp); + if not (R.are_convertible sg ty_inf ty_exp) then + let ty_exp' = rename_vars_with_typed_context ctx ty_exp in + raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) and check_app sg (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = match R.whnf sg ty_f with | Pi (_,_,a,b) -> - let _ = check sg ctx arg a in (mk_App f arg [], Subst.subst b arg ) + let _ = check sg ctx arg a in (mk_App f arg [], Subst.subst b arg ) | _ -> raise (TypingError ( ProductExpected (f,ctx,ty_f))) let inference sg (te:term) : typ = infer sg [] te @@ -142,15 +142,15 @@ struct | a1::args1, a2::args2 -> add_to_list q ((q,a1,a2)::lst) args1 args2 | _, _ -> raise (Invalid_argument "add_to_list") -let safe_add_to_list q lst args1 args2 = - try Some (add_to_list q lst args1 args2) - with Invalid_argument _ -> None + let safe_add_to_list q lst args1 args2 = + try Some (add_to_list q lst args1 args2) + with Invalid_argument _ -> None -let unshift_reduce sg q t = - try Some (Subst.unshift q t) - with Subst.UnshiftExn -> - ( try Some (Subst.unshift q (R.snf sg t)) - with Subst.UnshiftExn -> None ) + let unshift_reduce sg q t = + try Some (Subst.unshift q t) + with Subst.UnshiftExn -> + ( try Some (Subst.unshift q (R.snf sg t)) + with Subst.UnshiftExn -> None ) (** Under [d] lambdas, checks whether term [te] *must* contain an occurence of any variable that satisfies the given predicate [p], @@ -158,257 +158,257 @@ let unshift_reduce sg q t = This check make no assumption on the rewrite system or possible substitution - any definable symbol are "safe" as they may reduce to a term where no variable occur - any applied meta variable (DB index > [d]) are "safe" as they may be - substituted and reduce to a term where no variable occur + substituted and reduce to a term where no variable occur Raises VarSurelyOccurs if the term [te] *surely* contains an occurence of one of the [vars]. - *) -let sure_occur_check sg (d:int) (p:int -> bool) (te:term) : bool = - let exception VarSurelyOccurs in - let rec aux = function - | [] -> () - | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) - match t with - | Kind | Type _ | Const _ -> aux tl - | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) - | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) - | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) - | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl - | App (f,a,args) -> - begin - match f with - | DB (_,_,n) when n >= k + d -> (* a matching variable *) - if p (n-k) then raise VarSurelyOccurs else aux tl - | DB (_,_,n) when n < k + d -> (* a locally bound variable *) - if n >= k && p (n-k) - then raise VarSurelyOccurs - else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) - | Const (l,cst) when Signature.is_static sg l cst -> - ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) - | _ -> aux tl - (* Default case encompasses: - - Meta variables: DB(_,_,n) with n >= k + d - - Definable symbols - - Lambdas (FIXME: when can this happen ?) - - Illegal applications *) - end - in - try aux [(0,te)]; false - with VarSurelyOccurs -> true +*) + let sure_occur_check sg (d:int) (p:int -> bool) (te:term) : bool = + let exception VarSurelyOccurs in + let rec aux = function + | [] -> () + | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) + match t with + | Kind | Type _ | Const _ -> aux tl + | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) + | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) + | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) + | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl + | App (f,a,args) -> + begin + match f with + | DB (_,_,n) when n >= k + d -> (* a matching variable *) + if p (n-k) then raise VarSurelyOccurs else aux tl + | DB (_,_,n) when n < k + d -> (* a locally bound variable *) + if n >= k && p (n-k) + then raise VarSurelyOccurs + else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) + | Const (l,cst) when Signature.is_static sg l cst -> + ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) + | _ -> aux tl + (* Default case encompasses: + - Meta variables: DB(_,_,n) with n >= k + d + - Definable symbols + - Lambdas (FIXME: when can this happen ?) + - Illegal applications *) + end + in + try aux [(0,te)]; false + with VarSurelyOccurs -> true (** Under [d] lambdas, gather all free variables that are *surely* contained in term [te]. That is to say term [te] will contain an occurence of these variables *even when substituted or reduced*. This check make no assumption on the rewrite system or possible substitutions - applied definable symbols *surely* contain no variable as they may - reduce to terms where their arguments are erased + reduce to terms where their arguments are erased - applied meta variable (DB index > [d]) *surely* contain no variable as they - may be substituted and reduce to a term where their arguments are erased + may be substituted and reduce to a term where their arguments are erased Sets the indices of *surely* contained variables to [true] in the [vars] boolean array which is expected to be of size (at least) [d]. - *) -let gather_free_vars (d:int) (terms:term list) : bool array = - let vars = Array.make d false in - let rec aux = function - | [] -> () - | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) - match t with - | DB (_,_,n) -> (if n >= k && n < k + d then vars.(n-k) <- true); aux tl - | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) - | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) - | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) - | App (f,a,args) -> aux ((k,f)::(k,a):: (List.map (fun t -> (k,t)) args) @ tl) - | _ -> aux tl - in aux (List.map (fun t -> (0,t)) terms); vars - -type cstr = int*term*term +*) + let gather_free_vars (d:int) (terms:term list) : bool array = + let vars = Array.make d false in + let rec aux = function + | [] -> () + | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) + match t with + | DB (_,_,n) -> (if n >= k && n < k + d then vars.(n-k) <- true); aux tl + | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) + | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) + | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) + | App (f,a,args) -> aux ((k,f)::(k,a):: (List.map (fun t -> (k,t)) args) @ tl) + | _ -> aux tl + in aux (List.map (fun t -> (0,t)) terms); vars + + type cstr = int*term*term (* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) -type solver = - { - subst : SS.t; - ho_subst : (int*int*term) list; - unsolved : cstr list; - unsatisf : cstr list - } - -let try_solve q args t = - try - let dbs = List.map (function DB(_,_,n) -> n | _ -> raise Matching.NotUnifiable) args in - Some (Matching.solve q (LList.of_list dbs) t) - with Matching.NotUnifiable -> None - -let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function - | [] -> (flag, s) - | (q,t1,t2)::lst -> - begin - let t1' = R.whnf sg (SS.apply s.subst q t1) in - let t2' = R.whnf sg (SS.apply s.subst q t2) in - let dropped () = pseudo_u sg flag s lst in - let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in - let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in - if term_eq t1' t2' then dropped () - else - match t1', t2' with - | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) - | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) - | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () - - | Pi (_,_,a,b), Pi (_,_,a',b') -> - pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) - | Lam (_,_,_,b), Lam (_,_,_,b') -> - pseudo_u sg true s ((q+1,b,b')::lst) + type solver = + { + subst : SS.t; + ho_subst : (int*int*term) list; + unsolved : cstr list; + unsatisf : cstr list + } + + let try_solve q args t = + try + let dbs = List.map (function DB(_,_,n) -> n | _ -> raise Matching.NotUnifiable) args in + Some (Matching.solve q (LList.of_list dbs) t) + with Matching.NotUnifiable -> None + + let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function + | [] -> (flag, s) + | (q,t1,t2)::lst -> + begin + let t1' = R.whnf sg (SS.apply s.subst q t1) in + let t2' = R.whnf sg (SS.apply s.subst q t2) in + let dropped () = pseudo_u sg flag s lst in + let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in + let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in + if term_eq t1' t2' then dropped () + else + match t1', t2' with + | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) + | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) + | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () + + | Pi (_,_,a,b), Pi (_,_,a',b') -> + pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) + | Lam (_,_,_,b), Lam (_,_,_,b') -> + pseudo_u sg true s ((q+1,b,b')::lst) (* Potentially eta-equivalent terms *) - | Lam (_,i,_,b), a when !Reduction.eta -> - let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg true s ((q+1,b,b')::lst) - | a, Lam (_,i,_,b) when !Reduction.eta -> - let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg true s ((q+1,b,b')::lst) + | Lam (_,i,_,b), a when !Reduction.eta -> + let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in + pseudo_u sg true s ((q+1,b,b')::lst) + | a, Lam (_,i,_,b) when !Reduction.eta -> + let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in + pseudo_u sg true s ((q+1,b,b')::lst) (* A definable symbol is only be convertible with closed terms *) - | Const (l,cst), t when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() - | t, Const (l,cst) when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() + | Const (l,cst), t when not (Signature.is_static sg l cst) -> + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() + | t, Const (l,cst) when not (Signature.is_static sg l cst) -> + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() (* X = Y : map either X to Y or Y to X *) - | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> - let (n,t) = if n1=q && n2>=q -> + let (n,t) = if n1=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then unsatisf() - else begin - match unshift_reduce sg q t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() - else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst - end - | t, DB (_,_,n) when n>=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then unsatisf() - else begin - match unshift_reduce sg q t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() - else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst - end + | DB (_,_,n), t when n>=q -> + if sure_occur_check sg q (fun k -> k <= q || k = n) t + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() + else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst + end + | t, DB (_,_,n) when n>=q -> + if sure_occur_check sg q (fun k -> k <= q || k = n) t + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() + else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst + end (* f t1 ... tn / X t1 ... tn = u 1) Gather all free variables in t1 ... tn 2) Make sure u only relies on these variables *) - | App (DB (_,_,n),a,args), t when n >= q -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() - else begin - match try_solve q (a::args) t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) - else pseudo_u sg true - {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst - end - | t, App (DB (_,_,n),a,args) when n >= q -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() - else begin - match try_solve q (a::args) t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) - else pseudo_u sg true - {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst - end - | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() - | t, App (Const (l,cst),a,args) when not (Signature.is_static sg l cst) -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() - - | App (f,a,args), App (f',a',args') -> + | App (DB (_,_,n),a,args), t when n >= q -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) + else pseudo_u sg true + {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst + end + | t, App (DB (_,_,n),a,args) when n >= q -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) + else pseudo_u sg true + {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst + end + | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() + | t, App (Const (l,cst),a,args) when not (Signature.is_static sg l cst) -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() + + | App (f,a,args), App (f',a',args') -> (* f = Kind | Type | DB n when n unsatisf() (* Different number of arguments. *) - | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) - end - - | _, _ -> unsatisf() - end - -let solve_cstr sg cstr = - let rec process_solver sol = - match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with - | false, s -> s - | true, sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} - in - process_solver {subst=SS.identity;ho_subst=[];unsolved=cstr;unsatisf=[]} + begin + match safe_add_to_list q lst args args' with + | None -> unsatisf() (* Different number of arguments. *) + | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) + end + + | _, _ -> unsatisf() + end + + let solve_cstr sg cstr = + let rec process_solver sol = + match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with + | false, s -> s + | true, sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} + in + process_solver {subst=SS.identity;ho_subst=[];unsolved=cstr;unsatisf=[]} (* **** TYPE CHECKING/INFERENCE FOR PATTERNS ******************************** *) -type constraints = (int * term * term) list -type context2 = (loc * ident * typ) LList.t + type constraints = (int * term * term) list + type context2 = (loc * ident * typ) LList.t (* Partial Context *) -type partial_context = - { - padding : int; (* expected size *) - pctx : context2; (* partial context *) - bracket : bool - } + type partial_context = + { + padding : int; (* expected size *) + pctx : context2; (* partial context *) + bracket : bool + } -let pc_make (ctx:partially_typed_context) : partial_context = - let size = List.length ctx in - assert ( size >= 0 ); - { padding=size; pctx=LList.nil; bracket=false } + let pc_make (ctx:partially_typed_context) : partial_context = + let size = List.length ctx in + assert ( size >= 0 ); + { padding=size; pctx=LList.nil; bracket=false } -let pc_in (delta:partial_context) (n:int) : bool = n >= delta.padding + let pc_in (delta:partial_context) (n:int) : bool = n >= delta.padding -let pc_get (delta:partial_context) (n:int) : term = - let (_,_,ty) = LList.nth delta.pctx (n-delta.padding) - in Subst.shift (n+1) ty + let pc_get (delta:partial_context) (n:int) : term = + let (_,_,ty) = LList.nth delta.pctx (n-delta.padding) + in Subst.shift (n+1) ty -let pc_add (delta:partial_context) (n:int) (l:loc) (id:ident) (ty0:typ) : partial_context = - assert ( n == delta.padding-1 && n >= 0 ); - let ty = Subst.unshift (n+1) ty0 in - { padding = delta.padding - 1; - pctx = LList.cons (l,id,ty) delta.pctx; - bracket = false } + let pc_add (delta:partial_context) (n:int) (l:loc) (id:ident) (ty0:typ) : partial_context = + assert ( n == delta.padding-1 && n >= 0 ); + let ty = Subst.unshift (n+1) ty0 in + { padding = delta.padding - 1; + pctx = LList.cons (l,id,ty) delta.pctx; + bracket = false } -let pc_to_context (delta:partial_context) : typed_context = LList.lst delta.pctx + let pc_to_context (delta:partial_context) : typed_context = LList.lst delta.pctx -let pc_to_context_wp (delta:partial_context) : typed_context = - let dummy = (dloc, dmark, mk_DB dloc dmark (-1)) in - let rec aux lst = function 0 -> lst | n -> aux (dummy::lst) (n-1) in - aux (pc_to_context delta) delta.padding + let pc_to_context_wp (delta:partial_context) : typed_context = + let dummy = (dloc, dmark, mk_DB dloc dmark (-1)) in + let rec aux lst = function 0 -> lst | n -> aux (dummy::lst) (n-1) in + aux (pc_to_context delta) delta.padding (* let pp_pcontext fmt delta = * let lst = List.rev (LList.lst delta.pctx) in @@ -419,189 +419,189 @@ let pc_to_context_wp (delta:partial_context) : typed_context = (* *** *) -let get_last = - let rec aux acc = function - | [] -> assert false - | [a] -> (List.rev acc, a) - | hd::tl -> aux (hd::acc) tl in - aux [] - -let unshift_n sg n te = - try Subst.unshift n te - with Subst.UnshiftExn -> Subst.unshift n (R.snf sg te) - -let rec infer_pattern sg (delta:partial_context) (sigma:context2) - (lst:constraints) (pat:pattern) : typ * partial_context * constraints = - match pat with - | Pattern (l,cst,args) -> - let (_,_,ty,delta2,lst2) = List.fold_left (infer_pattern_aux sg) - ( sigma, mk_Const l cst , Signature.get_type sg l cst , delta , lst ) args - in (ty,delta2,lst2) - | Var (l,x,n,args) when n < LList.len sigma -> - let (_,_,ty,delta2,lst2) = List.fold_left (infer_pattern_aux sg) - ( sigma, mk_DB l x n, get_type (LList.lst sigma) l x n , delta , lst ) args - in (ty,delta2,lst2) - | Var _ | Brackets _ | Lambda _ -> - let ctx = (LList.lst sigma)@(pc_to_context_wp delta) in - raise (TypingError (CannotInferTypeOfPattern (pat,ctx))) - -and infer_pattern_aux sg - (sigma,f,ty_f,delta,lst : context2*term*typ*partial_context*constraints) - (arg:pattern) : context2*term*typ*partial_context*constraints = - match R.whnf sg ty_f with - | Pi (_,_,a,b) -> - let (delta2,lst2) = check_pattern sg delta sigma a lst arg in - let arg' = pattern_to_term arg in - ( sigma, Term.mk_App f arg' [], Subst.subst b arg', delta2 , lst2 ) - | ty_f -> - let ctx = (LList.lst sigma)@(pc_to_context_wp delta) in - raise (TypingError (ProductExpected (f,ctx,ty_f))) - -and check_pattern sg (delta:partial_context) (sigma:context2) (exp_ty:typ) - (lst:constraints) (pat:pattern) : partial_context * constraints = - Debug.(debug D_rule "Checking pattern %a:%a" pp_pattern pat pp_term exp_ty); - let ctx () = (LList.lst sigma)@(pc_to_context_wp delta) in - match pat with - | Lambda (l,x,p) -> - begin - match R.whnf sg exp_ty with - | Pi (_,_,a,b) -> check_pattern sg delta (LList.cons (l,x,a) sigma) b lst p - | _ -> raise (TypingError ( ProductExpected (pattern_to_term pat,ctx (),exp_ty))) - end - | Brackets te -> - let _ = - try Subst.unshift (LList.len sigma) te - with Subst.UnshiftExn -> raise (TypingError (BracketExprBoundVar (te,ctx()))) - in - let exp_ty2 = - try unshift_n sg (LList.len sigma) exp_ty - with Subst.UnshiftExn -> - raise (TypingError (BracketExpectedTypeBoundVar (te,ctx(),exp_ty))) - in - let _ = - try unshift_n sg delta.padding exp_ty2 - with Subst.UnshiftExn -> - raise (TypingError (BracketExpectedTypeRightVar (te,ctx(),exp_ty))) - in - ( {delta with bracket = true}, lst) - | Var (l,x,n,[]) when n >= LList.len sigma -> - begin - let k = LList.len sigma in + let get_last = + let rec aux acc = function + | [] -> assert false + | [a] -> (List.rev acc, a) + | hd::tl -> aux (hd::acc) tl in + aux [] + + let unshift_n sg n te = + try Subst.unshift n te + with Subst.UnshiftExn -> Subst.unshift n (R.snf sg te) + + let rec infer_pattern sg (delta:partial_context) (sigma:context2) + (lst:constraints) (pat:pattern) : typ * partial_context * constraints = + match pat with + | Pattern (l,cst,args) -> + let (_,_,ty,delta2,lst2) = List.fold_left (infer_pattern_aux sg) + ( sigma, mk_Const l cst , Signature.get_type sg l cst , delta , lst ) args + in (ty,delta2,lst2) + | Var (l,x,n,args) when n < LList.len sigma -> + let (_,_,ty,delta2,lst2) = List.fold_left (infer_pattern_aux sg) + ( sigma, mk_DB l x n, get_type (LList.lst sigma) l x n , delta , lst ) args + in (ty,delta2,lst2) + | Var _ | Brackets _ | Lambda _ -> + let ctx = (LList.lst sigma)@(pc_to_context_wp delta) in + raise (TypingError (CannotInferTypeOfPattern (pat,ctx))) + + and infer_pattern_aux sg + (sigma,f,ty_f,delta,lst : context2*term*typ*partial_context*constraints) + (arg:pattern) : context2*term*typ*partial_context*constraints = + match R.whnf sg ty_f with + | Pi (_,_,a,b) -> + let (delta2,lst2) = check_pattern sg delta sigma a lst arg in + let arg' = pattern_to_term arg in + ( sigma, Term.mk_App f arg' [], Subst.subst b arg', delta2 , lst2 ) + | ty_f -> + let ctx = (LList.lst sigma)@(pc_to_context_wp delta) in + raise (TypingError (ProductExpected (f,ctx,ty_f))) + + and check_pattern sg (delta:partial_context) (sigma:context2) (exp_ty:typ) + (lst:constraints) (pat:pattern) : partial_context * constraints = + Debug.(debug D_rule "Checking pattern %a:%a" pp_pattern pat pp_term exp_ty); + let ctx () = (LList.lst sigma)@(pc_to_context_wp delta) in + match pat with + | Lambda (l,x,p) -> + begin + match R.whnf sg exp_ty with + | Pi (_,_,a,b) -> check_pattern sg delta (LList.cons (l,x,a) sigma) b lst p + | _ -> raise (TypingError ( ProductExpected (pattern_to_term pat,ctx (),exp_ty))) + end + | Brackets te -> + let _ = + try Subst.unshift (LList.len sigma) te + with Subst.UnshiftExn -> raise (TypingError (BracketExprBoundVar (te,ctx()))) + in + let exp_ty2 = + try unshift_n sg (LList.len sigma) exp_ty + with Subst.UnshiftExn -> + raise (TypingError (BracketExpectedTypeBoundVar (te,ctx(),exp_ty))) + in + let _ = + try unshift_n sg delta.padding exp_ty2 + with Subst.UnshiftExn -> + raise (TypingError (BracketExpectedTypeRightVar (te,ctx(),exp_ty))) + in + ( {delta with bracket = true}, lst) + | Var (l,x,n,[]) when n >= LList.len sigma -> + begin + let k = LList.len sigma in (* Bracket may introduce circularity (variable's expected type depending on itself *) - if delta.bracket && Subst.occurs (n-k) exp_ty - then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); - if pc_in delta (n-k) - then - let inf_ty = Subst.shift k (pc_get delta (n-k)) in - ( delta, (k,inf_ty,exp_ty)::lst ) - else - ( try ( pc_add delta (n-k) l x (unshift_n sg k exp_ty), lst ) - with Subst.UnshiftExn -> - raise (TypingError (FreeVariableDependsOnBoundVariable (l,x,n,ctx(),exp_ty))) ) - end - | Var (l,x,n,args) when n >= LList.len sigma -> - begin - let k = LList.len sigma in + if delta.bracket && Subst.occurs (n-k) exp_ty + then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); + if pc_in delta (n-k) + then + let inf_ty = Subst.shift k (pc_get delta (n-k)) in + ( delta, (k,inf_ty,exp_ty)::lst ) + else + ( try ( pc_add delta (n-k) l x (unshift_n sg k exp_ty), lst ) + with Subst.UnshiftExn -> + raise (TypingError (FreeVariableDependsOnBoundVariable (l,x,n,ctx(),exp_ty))) ) + end + | Var (l,x,n,args) when n >= LList.len sigma -> + begin + let k = LList.len sigma in (* Bracket may introduce circularity (variable's expected type depending on itself *) - if delta.bracket && Subst.occurs (n-k) exp_ty - then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); - let (args2, last) = get_last args in - match last with - | Var (l2,x2,n2,[]) -> - check_pattern sg delta sigma - (mk_Pi l2 x2 (get_type (LList.lst sigma) l2 x2 n2) (Subst.subst_n n2 x2 exp_ty) ) - lst (Var(l,x,n,args2)) - | _ -> raise (TypingError (CannotInferTypeOfPattern (pat,ctx ()))) (* not a pattern *) - end - | _ -> - begin - let (inf_ty,delta2,lst2) = infer_pattern sg delta sigma lst pat in - let q = LList.len sigma in - ( delta2 , (q,inf_ty,exp_ty)::lst2 ) - end + if delta.bracket && Subst.occurs (n-k) exp_ty + then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); + let (args2, last) = get_last args in + match last with + | Var (l2,x2,n2,[]) -> + check_pattern sg delta sigma + (mk_Pi l2 x2 (get_type (LList.lst sigma) l2 x2 n2) (Subst.subst_n n2 x2 exp_ty) ) + lst (Var(l,x,n,args2)) + | _ -> raise (TypingError (CannotInferTypeOfPattern (pat,ctx ()))) (* not a pattern *) + end + | _ -> + begin + let (inf_ty,delta2,lst2) = infer_pattern sg delta sigma lst pat in + let q = LList.len sigma in + ( delta2 , (q,inf_ty,exp_ty)::lst2 ) + end (* ************************************************************************** *) -let pp_context_inline fmt ctx = - pp_list ", " - (fun fmt (_,x,ty) -> fprintf fmt "%a: %a" pp_ident x pp_term ty ) - fmt (List.rev ctx) - -let subst_context (sub:SS.t) (ctx:typed_context) : typed_context = - if SS.is_identity sub then ctx - else - let apply_subst i (l,x,ty) = (l,x,Exsubst.apply_exsubst (SS.subst2 sub i) 0 ty) in - List.mapi apply_subst ctx - -let check_type_annotations sg sub typed_ctx annot_ctx = - Debug.(debug D_rule "Typechecking type annotations"); - let rec aux ctx depth ctx1 ctx2 = - match ctx1, ctx2 with - | (l,x,ty)::ctx1' , (_,_,ty')::ctx2' -> - begin - match ty' with - | None -> () - | Some ty' -> - Debug.(debug D_typeChecking "Checking type annotation (%a): %a ~ %a" - pp_loc l pp_term ty pp_term ty'); - if not (R.are_convertible sg ty ty') - then - let ty2 = SS.apply sub 0 (Subst.shift depth ty ) in - let ty2' = SS.apply sub 0 (Subst.shift depth ty') in - if not (R.are_convertible sg ty2 ty2') - then raise (TypingError (AnnotConvertibilityError (l,x,ctx,ty',ty))) - end; - aux ((l,x,ty)::ctx) (depth+1) ctx1' ctx2' - | [], [] -> () - | _ -> assert false - in aux [] 1 typed_ctx annot_ctx - -let check_rule sg (rule:partially_typed_rule) : SS.t * typed_rule = - Debug.(debug D_rule "Inferring variables type and constraints from LHS"); - let delta = pc_make rule.ctx in - let (ty_le,delta,lst) = infer_pattern sg delta LList.nil [] rule.pat in - assert ( delta.padding == 0 ); - let sol = solve_cstr sg lst in - ( match sol.unsatisf with + let pp_context_inline fmt ctx = + pp_list ", " + (fun fmt (_,x,ty) -> fprintf fmt "%a: %a" pp_ident x pp_term ty ) + fmt (List.rev ctx) + + let subst_context (sub:SS.t) (ctx:typed_context) : typed_context = + if SS.is_identity sub then ctx + else + let apply_subst i (l,x,ty) = (l,x,Exsubst.apply_exsubst (SS.subst2 sub i) 0 ty) in + List.mapi apply_subst ctx + + let check_type_annotations sg sub typed_ctx annot_ctx = + Debug.(debug D_rule "Typechecking type annotations"); + let rec aux ctx depth ctx1 ctx2 = + match ctx1, ctx2 with + | (l,x,ty)::ctx1' , (_,_,ty')::ctx2' -> + begin + match ty' with + | None -> () + | Some ty' -> + Debug.(debug D_typeChecking "Checking type annotation (%a): %a ~ %a" + pp_loc l pp_term ty pp_term ty'); + if not (R.are_convertible sg ty ty') + then + let ty2 = SS.apply sub 0 (Subst.shift depth ty ) in + let ty2' = SS.apply sub 0 (Subst.shift depth ty') in + if not (R.are_convertible sg ty2 ty2') + then raise (TypingError (AnnotConvertibilityError (l,x,ctx,ty',ty))) + end; + aux ((l,x,ty)::ctx) (depth+1) ctx1' ctx2' + | [], [] -> () + | _ -> assert false + in aux [] 1 typed_ctx annot_ctx + + let check_rule sg (rule:partially_typed_rule) : SS.t * typed_rule = + Debug.(debug D_rule "Inferring variables type and constraints from LHS"); + let delta = pc_make rule.ctx in + let (ty_le,delta,lst) = infer_pattern sg delta LList.nil [] rule.pat in + assert ( delta.padding == 0 ); + let sol = solve_cstr sg lst in + ( match sol.unsatisf with | [] -> () | (q,t1,t2)::_ -> - if !fail_on_unsatisfiable_constraints - then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) - else Debug.(debug D_warn "At %a: unsatisfiable constraint: %a ~ %a%s" - pp_loc (get_loc_rule rule) - pp_term t1 pp_term t2 - (if q > 0 then Format.sprintf " (under %i abstractions)" q else ""))); - - let sub = sol.subst in - let ty_le2 = SS.apply sub 0 ty_le in - let ctx = LList.lst delta.pctx in - let ctx2 = - try subst_context sub ctx - with Subst.UnshiftExn -> (* TODO make Dedukti handle this case *) - Debug.( - debug D_rule "Failed to infer a typing context for the rule:\n%a" - pp_part_typed_rule rule; - let ctx_name n = let _,name,_ = List.nth ctx n in name in - debug D_rule "Tried inferred typing substitution: %a" (SS.pp ctx_name) sub); - raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) ) ) - in + if !fail_on_unsatisfiable_constraints + then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) + else Debug.(debug D_warn "At %a: unsatisfiable constraint: %a ~ %a%s" + pp_loc (get_loc_rule rule) + pp_term t1 pp_term t2 + (if q > 0 then Format.sprintf " (under %i abstractions)" q else ""))); + + let sub = sol.subst in + let ty_le2 = SS.apply sub 0 ty_le in + let ctx = LList.lst delta.pctx in + let ctx2 = + try subst_context sub ctx + with Subst.UnshiftExn -> (* TODO make Dedukti handle this case *) + Debug.( + debug D_rule "Failed to infer a typing context for the rule:\n%a" + pp_part_typed_rule rule; + let ctx_name n = let _,name,_ = List.nth ctx n in name in + debug D_rule "Tried inferred typing substitution: %a" (SS.pp ctx_name) sub); + raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) ) ) + in (* FIXME: Why is the RHS substituted ?! Instead we should keep the original RHS and perform a check *modulo a substitution* This simply means extend the check function to apply the substitution to all infered types. *) - let ri2 = SS.apply sub 0 rule.rhs in - Debug.(debug D_rule "Typechecking rule"); - check sg ctx2 ri2 ty_le2; - check_type_annotations sg sub ctx2 rule.ctx; - Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" - pp_context_inline ctx2 pp_pattern rule.pat pp_term ri2); - - sub, - { name = rule.name; - ctx = ctx2; - pat = rule.pat; - rhs = rule.rhs - } + let ri2 = SS.apply sub 0 rule.rhs in + Debug.(debug D_rule "Typechecking rule"); + check sg ctx2 ri2 ty_le2; + check_type_annotations sg sub ctx2 rule.ctx; + Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" + pp_context_inline ctx2 pp_pattern rule.pat pp_term ri2); + + sub, + { name = rule.name; + ctx = ctx2; + pat = rule.pat; + rhs = rule.rhs + } end From d72f2f195a47fa9674cc1f0e4325b3bdf4394896 Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Tue, 10 Dec 2019 17:35:39 +0100 Subject: [PATCH 13/35] A naive use of the unsolved constraints --- kernel/typing.ml | 106 +++++++++++++++++++++++++++++------------------ 1 file changed, 65 insertions(+), 41 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 3db1a806..5b5fc699 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -67,9 +67,34 @@ struct let (_,_,te) = a in raise (TypingError (ConvertibilityError (te, ctx, mk_Type dloc, ty_a))) + type cstr = int*term*term + (* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) + + let csq_of_eq (sg:Signature.t) (ty_inf:typ) (ty_exp:typ) (addi_eq:cstr list) : bool = + let is_same_cstr ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = + let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in + let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in + (term_eq t1' t2' && term_eq u1' u2') || + (term_eq t1' u2' && term_eq u1' t2') + in + let addi_eq_nrm = List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) addi_eq in + let rec bis n ty1 ty2 = + List.exists (is_same_cstr (n,ty1,ty2)) addi_eq_nrm || + match ty1,ty2 with + | App(h1,a1,l1), App(h2,a2,l2) -> + List.for_all2 (bis n) (h1::a1::l1) (h2::a2::l2) + | Lam(_,_,_,t1), Lam(_,_,_,t2) -> bis (n+1) t1 t2 + | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> bis n a1 a2 && bis (n+1) b1 b2 + | _ -> false + in + R.are_convertible sg ty_inf ty_exp || + bis 0 (R.snf sg ty_inf) (R.snf sg ty_exp) + (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) - let rec infer sg (ctx:typed_context) (te:term) : typ = + (* The functions [check'] and [infer'] have an additional argument compared [check] and [infer] + which is a list of additional equality, which are useful when checking subject reduction *) + let rec infer' sg (ctx:typed_context) (te:term) (addi_eq:cstr list) : typ = Debug.(debug D_typeChecking "Inferring: %a" pp_term te); match te with | Kind -> raise (TypingError KindIsNotTypable) @@ -77,57 +102,61 @@ struct | DB (l,x,n) -> get_type ctx l x n | Const (l,cst) -> Signature.get_type sg l cst | App (f,a,args) -> - snd (List.fold_left (check_app sg ctx) (f,infer sg ctx f) (a::args)) + snd (List.fold_left (check_app sg ctx addi_eq) (f,infer' sg ctx f addi_eq) (a::args)) | Pi (l,x,a,b) -> - let ty_a = infer sg ctx a in + let ty_a = infer' sg ctx a addi_eq in let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer sg ctx2 b in + let ty_b = infer' sg ctx2 b addi_eq in ( match ty_b with | Kind | Type _ -> ty_b | _ -> raise (TypingError (SortExpected (b, ctx2, ty_b))) ) | Lam (l,x,Some a,b) -> - let ty_a = infer sg ctx a in + let ty_a = infer' sg ctx a addi_eq in let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer sg ctx2 b in + let ty_b = infer' sg ctx2 b addi_eq in ( match ty_b with | Kind -> raise (TypingError (InexpectedKind (b, ctx2))) | _ -> mk_Pi l x a ty_b ) | Lam (l,_,None,_) -> raise (TypingError (DomainFreeLambda l)) - and check sg (ctx:typed_context) (te:term) (ty_exp:typ) : unit = + and check' sg (ctx:typed_context) (te:term) (ty_exp:typ) (addi_eq:cstr list) : unit = Debug.(debug D_typeChecking "Checking (%a): %a : %a" pp_loc (get_loc te) pp_term te pp_term ty_exp); match te with | Lam (l,x,None,b) -> begin match R.whnf sg ty_exp with - | Pi (_,_,a,ty_b) -> check sg ((l,x,a)::ctx) b ty_b + | Pi (_,_,a,ty_b) -> check' sg ((l,x,a)::ctx) b ty_b addi_eq | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) end | Lam (l,x,Some a,b) -> begin match R.whnf sg ty_exp with | Pi (_,_,a',ty_b) -> - ignore(infer sg ctx a); - if not (R.are_convertible sg a a') + ignore(infer' sg ctx a addi_eq); + if not (csq_of_eq sg a a' addi_eq) then raise (TypingError (ConvertibilityError ((mk_DB l x 0),ctx,a',a))) - else check sg ((l,x,a)::ctx) b ty_b + else check' sg ((l,x,a)::ctx) b ty_b addi_eq | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) end | _ -> - let ty_inf = infer sg ctx te in + let ty_inf = infer' sg ctx te addi_eq in Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" pp_term ty_inf pp_term ty_exp); - if not (R.are_convertible sg ty_inf ty_exp) then + if not (csq_of_eq sg ty_inf ty_exp addi_eq) + then let ty_exp' = rename_vars_with_typed_context ctx ty_exp in raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) - and check_app sg (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = + and check_app sg (ctx:typed_context) (addi_eq:cstr list) (f,ty_f:term*typ) (arg:term) : term*typ = match R.whnf sg ty_f with | Pi (_,_,a,b) -> - let _ = check sg ctx arg a in (mk_App f arg [], Subst.subst b arg ) + let _ = check' sg ctx arg a addi_eq in (mk_App f arg [], Subst.subst b arg ) | _ -> raise (TypingError ( ProductExpected (f,ctx,ty_f))) + let check sg ctx te ty = check' sg ctx te ty [] + let infer sg ctx te = infer' sg ctx te [] + let inference sg (te:term) : typ = infer sg [] te let checking sg (te:term) (ty:term) : unit = @@ -152,16 +181,16 @@ struct ( try Some (Subst.unshift q (R.snf sg t)) with Subst.UnshiftExn -> None ) -(** Under [d] lambdas, checks whether term [te] *must* contain an occurence - of any variable that satisfies the given predicate [p], - *even when substituted or reduced*. - This check make no assumption on the rewrite system or possible substitution - - any definable symbol are "safe" as they may reduce to a term where no variable occur - - any applied meta variable (DB index > [d]) are "safe" as they may be - substituted and reduce to a term where no variable occur - Raises VarSurelyOccurs if the term [te] *surely* contains an occurence of one - of the [vars]. -*) + (** Under [d] lambdas, checks whether term [te] *must* contain an occurence + of any variable that satisfies the given predicate [p], + *even when substituted or reduced*. + This check make no assumption on the rewrite system or possible substitution + - any definable symbol are "safe" as they may reduce to a term where no variable occur + - any applied meta variable (DB index > [d]) are "safe" as they may be + substituted and reduce to a term where no variable occur + Raises VarSurelyOccurs if the term [te] *surely* contains an occurence of one + of the [vars]. + *) let sure_occur_check sg (d:int) (p:int -> bool) (te:term) : bool = let exception VarSurelyOccurs in let rec aux = function @@ -220,9 +249,6 @@ struct | _ -> aux tl in aux (List.map (fun t -> (0,t)) terms); vars - type cstr = int*term*term -(* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) - type solver = { subst : SS.t; @@ -361,7 +387,7 @@ struct | _, _ -> unsatisf() end - let solve_cstr sg cstr = + let solve_cstr (sg : Signature.t) (cstr : cstr list) : solver = let rec process_solver sol = match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with | false, s -> s @@ -567,13 +593,16 @@ struct | (q,t1,t2)::_ -> if !fail_on_unsatisfiable_constraints then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) - else Debug.(debug D_warn "At %a: unsatisfiable constraint: %a ~ %a%s" - pp_loc (get_loc_rule rule) - pp_term t1 pp_term t2 - (if q > 0 then Format.sprintf " (under %i abstractions)" q else ""))); - + else + Debug.(debug D_warn) + "At %a: unsatisfiable constraint: %a ~ %a%s" + pp_loc (get_loc_rule rule) + pp_term t1 pp_term t2 + (if q > 0 then Format.sprintf " (under %i abstractions)" q else "") + ); let sub = sol.subst in - let ty_le2 = SS.apply sub 0 ty_le in + let ri2 = SS.apply sub 0 rule.rhs in + let ty_le2 = SS.apply sub 0 ty_le in let ctx = LList.lst delta.pctx in let ctx2 = try subst_context sub ctx @@ -585,13 +614,8 @@ struct debug D_rule "Tried inferred typing substitution: %a" (SS.pp ctx_name) sub); raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) ) ) in - (* FIXME: Why is the RHS substituted ?! - Instead we should keep the original RHS and perform a check *modulo a substitution* - This simply means extend the check function to apply the substitution to all infered - types. *) - let ri2 = SS.apply sub 0 rule.rhs in Debug.(debug D_rule "Typechecking rule"); - check sg ctx2 ri2 ty_le2; + check' sg ctx2 ri2 ty_le2 sol.unsolved; check_type_annotations sg sub ctx2 rule.ctx; Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" pp_context_inline ctx2 pp_pattern rule.pat pp_term ri2); From 987e3f063ac6ec0ed8ade4813fb1389c0c4c0595 Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Tue, 10 Dec 2019 17:38:35 +0100 Subject: [PATCH 14/35] Due to my very bad practice, the previous commit of Gaspard was lost --- kernel/typing.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 5b5fc699..a48fc42b 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -601,7 +601,6 @@ struct (if q > 0 then Format.sprintf " (under %i abstractions)" q else "") ); let sub = sol.subst in - let ri2 = SS.apply sub 0 rule.rhs in let ty_le2 = SS.apply sub 0 ty_le in let ctx = LList.lst delta.pctx in let ctx2 = @@ -614,6 +613,11 @@ struct debug D_rule "Tried inferred typing substitution: %a" (SS.pp ctx_name) sub); raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) ) ) in + (* FIXME: Why is the RHS substituted ?! + Instead we should keep the original RHS and perform a check *modulo a substitution* + This simply means extend the check function to apply the substitution to all infered + types. *) + let ri2 = SS.apply sub 0 rule.rhs in Debug.(debug D_rule "Typechecking rule"); check' sg ctx2 ri2 ty_le2 sol.unsolved; check_type_annotations sg sub ctx2 rule.ctx; From 6d86c2fcfeb250fc741fc83518b6b23880454197 Mon Sep 17 00:00:00 2001 From: GuillaumeGen Date: Tue, 10 Dec 2019 17:40:43 +0100 Subject: [PATCH 15/35] Update typing.ml Fixing comment --- kernel/typing.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index a48fc42b..3476ee1d 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -92,8 +92,8 @@ struct (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) - (* The functions [check'] and [infer'] have an additional argument compared [check] and [infer] - which is a list of additional equality, which are useful when checking subject reduction *) + (* The functions [check'] and [infer'] have an additional argument compared to [check] and [infer] + which is a list of additional equalities, which are useful when checking subject reduction *) let rec infer' sg (ctx:typed_context) (te:term) (addi_eq:cstr list) : typ = Debug.(debug D_typeChecking "Inferring: %a" pp_term te); match te with From 540279f2b39eb98e106e42791832cc2a4ae14f6d Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 11 Dec 2019 10:45:53 +0100 Subject: [PATCH 16/35] Made cstr_comparison global. --- kernel/typing.ml | 23 +++++++++++------------ 1 file changed, 11 insertions(+), 12 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 3476ee1d..1d0fc505 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -70,25 +70,23 @@ struct type cstr = int*term*term (* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) - let csq_of_eq (sg:Signature.t) (ty_inf:typ) (ty_exp:typ) (addi_eq:cstr list) : bool = - let is_same_cstr ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = - let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in - let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in - (term_eq t1' t2' && term_eq u1' u2') || + let is_same_cstr ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = + let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in + let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in + (term_eq t1' t2' && term_eq u1' u2') || (term_eq t1' u2' && term_eq u1' t2') - in - let addi_eq_nrm = List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) addi_eq in + + let csq_of_eq (sg:Signature.t) (ty_inf:typ) (ty_exp:typ) (addi_eq:cstr list) : bool = let rec bis n ty1 ty2 = - List.exists (is_same_cstr (n,ty1,ty2)) addi_eq_nrm || + List.exists (is_same_cstr (n,ty1,ty2)) addi_eq || match ty1,ty2 with - | App(h1,a1,l1), App(h2,a2,l2) -> - List.for_all2 (bis n) (h1::a1::l1) (h2::a2::l2) + | App(h1,a1,l1), App(h2,a2,l2) -> List.for_all2 (bis n) (h1::a1::l1) (h2::a2::l2) | Lam(_,_,_,t1), Lam(_,_,_,t2) -> bis (n+1) t1 t2 | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> bis n a1 a2 && bis (n+1) b1 b2 | _ -> false in R.are_convertible sg ty_inf ty_exp || - bis 0 (R.snf sg ty_inf) (R.snf sg ty_exp) + (addi_eq <> [] && bis 0 (R.snf sg ty_inf) (R.snf sg ty_exp)) (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) @@ -619,7 +617,8 @@ struct types. *) let ri2 = SS.apply sub 0 rule.rhs in Debug.(debug D_rule "Typechecking rule"); - check' sg ctx2 ri2 ty_le2 sol.unsolved; + let cstr_nf = List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) sol.unsolved in + check' sg ctx2 ri2 ty_le2 cstr_nf; check_type_annotations sg sub ctx2 rule.ctx; Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" pp_context_inline ctx2 pp_pattern rule.pat pp_term ri2); From d40110b045ea3bafb696f95197e5c0b7f79623fd Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 11 Dec 2019 11:54:36 +0100 Subject: [PATCH 17/35] Added tests and fixed bis function. --- kernel/typing.ml | 8 ++- tests/OK/{SR_sat.dk => SR_sat_bv1.dk} | 0 tests/OK/SR_sat_bv2.dk | 76 +++++++++++++++++++++++++++ tests/OK/SR_sat_eq1.dk | 8 +++ tests/OK/SR_sat_eq2.dk | 23 ++++++++ 5 files changed, 113 insertions(+), 2 deletions(-) rename tests/OK/{SR_sat.dk => SR_sat_bv1.dk} (100%) create mode 100644 tests/OK/SR_sat_bv2.dk create mode 100644 tests/OK/SR_sat_eq1.dk create mode 100644 tests/OK/SR_sat_eq2.dk diff --git a/kernel/typing.ml b/kernel/typing.ml index 1d0fc505..dc9ff778 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -70,6 +70,11 @@ struct type cstr = int*term*term (* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) + (* + let pp_cstr fmt (n,t1,t2) = + fprintf fmt "[%i] %a ~ %a" n pp_term t1 pp_term t2 + *) + let is_same_cstr ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in @@ -83,7 +88,7 @@ struct | App(h1,a1,l1), App(h2,a2,l2) -> List.for_all2 (bis n) (h1::a1::l1) (h2::a2::l2) | Lam(_,_,_,t1), Lam(_,_,_,t2) -> bis (n+1) t1 t2 | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> bis n a1 a2 && bis (n+1) b1 b2 - | _ -> false + | _ -> term_eq ty1 ty2 in R.are_convertible sg ty_inf ty_exp || (addi_eq <> [] && bis 0 (R.snf sg ty_inf) (R.snf sg ty_exp)) @@ -622,7 +627,6 @@ struct check_type_annotations sg sub ctx2 rule.ctx; Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" pp_context_inline ctx2 pp_pattern rule.pat pp_term ri2); - sub, { name = rule.name; ctx = ctx2; diff --git a/tests/OK/SR_sat.dk b/tests/OK/SR_sat_bv1.dk similarity index 100% rename from tests/OK/SR_sat.dk rename to tests/OK/SR_sat_bv1.dk diff --git a/tests/OK/SR_sat_bv2.dk b/tests/OK/SR_sat_bv2.dk new file mode 100644 index 00000000..529dfe23 --- /dev/null +++ b/tests/OK/SR_sat_bv2.dk @@ -0,0 +1,76 @@ +(; OK --type-lhs ;) + +A : Type. +T : A -> Type. +t : a:A -> T a. + +a : A. +def b : A -> A -> A. + c : A -> A -> A. + +(; We build definitions with types containing an expression relying on + 2 matching variables + 2 locally bound variables + Generated constraints are not necessary to check the rules but should + be discarded without generating any warning (satisfiable constraints). + + See SR_unsat_cstr_i.dk for examples of unsatisfiable constraints. +;) + + +(; Terms that *must* contain x and *must* contain y + are convertible with + terms that *must* or *may* contain x + and *must* or *may* contain y ;) +def a1 : X:(A->A->A) -> Y:(A->A) -> + (x:A -> y:A -> + T (c x + (c y + (c (b x x) + (c (b a y) + (c (b x y) + (b a a))))))) -> Type. + +[X,Y] a1 X Y (x => y => + t (c x + (c y + (c (b x x) + (c (b a y) + (c (b x y) + (b a a))))))) --> A. + +[X,Y] a1 X Y (x => y => + t (c (b a (c x x)) + (c y + (c (b x x) + (c (b a y) + (c (b x y) + (b a a))))))) --> A. + +[X,Y] a1 X (x => Y x) (x => y => + t (c (Y x) + (c y + (c (b x x) + (c (b a y) + (c (b x y) + (b a a))))))) --> A. + +(; Terms that *must* contain x and *must* contain y + are convertible with + terms that *must* or *may* contain x + and *must* or *may* contain y ;) +def a2 : X1:(A->A->A) -> X2:(A->A->A) -> X3:(A->A->A) -> X4:(A->A->A) -> + (x:A -> y:A -> + T (c x + (c y + (c (X1 x x) + (c (X2 a y) + (c (X3 x y) + (X4 a a))))))) -> Type. + + +def b1 : X:(A->A->A) -> Y:(A->A) -> + (x:A -> y:A -> f : (A->A->A) -> + T (f (c x y) + (f + (c (b x x) (b a y)) + (f (b x y) (b a a))))) -> Type. diff --git a/tests/OK/SR_sat_eq1.dk b/tests/OK/SR_sat_eq1.dk new file mode 100644 index 00000000..acbe1ec3 --- /dev/null +++ b/tests/OK/SR_sat_eq1.dk @@ -0,0 +1,8 @@ +(; OK --type-lhs ;) + +A : Type. +def T : A -> Type. +t : x : A -> T x. + +def f : x : A -> T x -> T x. +[X,Y] f X (t Y) --> t Y. diff --git a/tests/OK/SR_sat_eq2.dk b/tests/OK/SR_sat_eq2.dk new file mode 100644 index 00000000..cfc3a7ed --- /dev/null +++ b/tests/OK/SR_sat_eq2.dk @@ -0,0 +1,23 @@ +(; OK --type-lhs ;) + +A : Type. +a : A. +c : A -> A -> A. + +T : A -> Type. +t : x : A -> T x. + +def f : A -> A. + + +def test1 : x : A -> T (c (f x) a) -> T (f (f x)). +[X,Y] test1 X (t (c Y a)) --> t (f Y ). + +def test2 : x : A -> T (c (f x) a) -> T (f (f x)). +[X,Y] test2 X (t (c (f Y) a)) --> t (f (f Y)). + +def test3 : x : A -> T (f (c (f x) (f (f x)))) -> T (f (c (f x) (f (f x)))). +[X,Y] test3 X (t (f Y) ) --> t (f Y). + +def test4 : x : A -> T (c a (f (c (f x) (f (f x))))) -> T (f (c (f x) (f (f x)))). +[X,Y] test4 X (t (c a (f Y) )) --> t (f Y). From e4b65175f8a3dd32547a074d58626b72a66ca700 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 11 Dec 2019 12:07:04 +0100 Subject: [PATCH 18/35] Added some tests. --- tests/OK/SR_sat_bv2.dk | 43 +++++++++++++++++++++--------------------- tests/OK/SR_sat_eq2.dk | 25 ++++++++++++++++-------- 2 files changed, 39 insertions(+), 29 deletions(-) diff --git a/tests/OK/SR_sat_bv2.dk b/tests/OK/SR_sat_bv2.dk index 529dfe23..9b40984d 100644 --- a/tests/OK/SR_sat_bv2.dk +++ b/tests/OK/SR_sat_bv2.dk @@ -6,6 +6,7 @@ t : a:A -> T a. a : A. def b : A -> A -> A. +def b': A -> A -> A. c : A -> A -> A. (; We build definitions with types containing an expression relying on @@ -30,29 +31,29 @@ def a1 : X:(A->A->A) -> Y:(A->A) -> (c (b x y) (b a a))))))) -> Type. -[X,Y] a1 X Y (x => y => - t (c x - (c y - (c (b x x) - (c (b a y) - (c (b x y) - (b a a))))))) --> A. +[X,Y] a1 (x=>y=>X x y) (x=>Y x) (x=>y=>t + (c x + (c y + (c (b x x) + (c (b a y) + (c (b x y) + (b a a))))))) --> A. -[X,Y] a1 X Y (x => y => - t (c (b a (c x x)) - (c y - (c (b x x) - (c (b a y) - (c (b x y) - (b a a))))))) --> A. +[X,Y] a1 (x=>y=>X x y) (x=>Y x) (x=>y=>t + (c (b a (c x x)) + (c (Y y) + (c (b' (c x x) a) + (c (b' y y) + (c (b' (c x x) (b y y)) + (b' x y))))))) --> A. -[X,Y] a1 X (x => Y x) (x => y => - t (c (Y x) - (c y - (c (b x x) - (c (b a y) - (c (b x y) - (b a a))))))) --> A. +[X,Y] a1 (x=>y=>X x y) (x=>Y x) (x=>y=>t + (c (X x y) + (c (b (c y y) (c x x)) + (c x + (c y + (c y + (c (Y x) a))))))) --> A. (; Terms that *must* contain x and *must* contain y are convertible with diff --git a/tests/OK/SR_sat_eq2.dk b/tests/OK/SR_sat_eq2.dk index cfc3a7ed..d87d24d9 100644 --- a/tests/OK/SR_sat_eq2.dk +++ b/tests/OK/SR_sat_eq2.dk @@ -8,16 +8,25 @@ T : A -> Type. t : x : A -> T x. def f : A -> A. +def g : A -> A. +def test0 : x : A -> T (f x) -> T (f (f x)). +[X,Y] test0 X (t Y ) --> t (f Y ). -def test1 : x : A -> T (c (f x) a) -> T (f (f x)). -[X,Y] test1 X (t (c Y a)) --> t (f Y ). +def test0': x : A -> T (c (f x) a) -> T (f (f x)). +[X,Y] test0' X (t (c Y a)) --> t (f Y ). -def test2 : x : A -> T (c (f x) a) -> T (f (f x)). -[X,Y] test2 X (t (c (f Y) a)) --> t (f (f Y)). +def test1 : x : A -> T (c (g x) a) -> T (f (g x)). +[X,Y] test1 X (t (c (f Y) a)) --> t (f (f Y)). -def test3 : x : A -> T (f (c (f x) (f (f x)))) -> T (f (c (f x) (f (f x)))). -[X,Y] test3 X (t (f Y) ) --> t (f Y). +def test2 : x : A -> T (g (c (f x) (f (f x)))) -> T (g (c (f x) (f (f x)))). +[X,Y] test2 X (t (f Y) ) --> t (f Y). -def test4 : x : A -> T (c a (f (c (f x) (f (f x))))) -> T (f (c (f x) (f (f x)))). -[X,Y] test4 X (t (c a (f Y) )) --> t (f Y). +def test3 : x : A -> T (c a (g (c (f x) (f (f x))))) -> T (g (g (c (f x) (f (f x))))). +[X,Y] test3 X (t (c a (f Y) )) --> t (g (f Y)). + +def h : A -> A. +[X] h (g X) --> X. + +def test4 : x : A -> T (c a (g (c (f x) (f (f x))))) -> T (g (c (f x) (f (f x)))). +[X,Y] test4 X (t (c a (f Y) )) --> t (h (g (f Y))). From b13bc2b1926a4ed6abab73c1e1d2c1e254faf095 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 11 Dec 2019 14:05:19 +0100 Subject: [PATCH 19/35] Fixed buggy test. Implemented conversion under exsubst. --- kernel/typing.ml | 83 ++++++++++++++++++---------------- tests/OK/higher_order_cstr3.dk | 24 +++++----- 2 files changed, 56 insertions(+), 51 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index dc9ff778..e4aafa16 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -81,7 +81,7 @@ struct (term_eq t1' t2' && term_eq u1' u2') || (term_eq t1' u2' && term_eq u1' t2') - let csq_of_eq (sg:Signature.t) (ty_inf:typ) (ty_exp:typ) (addi_eq:cstr list) : bool = + let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (addi_eq:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = let rec bis n ty1 ty2 = List.exists (is_same_cstr (n,ty1,ty2)) addi_eq || match ty1,ty2 with @@ -90,14 +90,16 @@ struct | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> bis n a1 a2 && bis (n+1) b1 b2 | _ -> term_eq ty1 ty2 in - R.are_convertible sg ty_inf ty_exp || - (addi_eq <> [] && bis 0 (R.snf sg ty_inf) (R.snf sg ty_exp)) + let subst_ty_inf = SS.apply sub depth ty_inf in + let subst_ty_exp = SS.apply sub depth ty_exp in + R.are_convertible sg subst_ty_inf subst_ty_exp || + (addi_eq <> [] && bis 0 (R.snf sg subst_ty_inf) (R.snf sg subst_ty_exp)) (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) (* The functions [check'] and [infer'] have an additional argument compared to [check] and [infer] which is a list of additional equalities, which are useful when checking subject reduction *) - let rec infer' sg (ctx:typed_context) (te:term) (addi_eq:cstr list) : typ = + let rec infer' sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (te:term) : typ = Debug.(debug D_typeChecking "Inferring: %a" pp_term te); match te with | Kind -> raise (TypingError KindIsNotTypable) @@ -105,60 +107,62 @@ struct | DB (l,x,n) -> get_type ctx l x n | Const (l,cst) -> Signature.get_type sg l cst | App (f,a,args) -> - snd (List.fold_left (check_app sg ctx addi_eq) (f,infer' sg ctx f addi_eq) (a::args)) + snd (List.fold_left (check_app sg sub addi_eq d ctx) + (f,infer' sg sub addi_eq d ctx f) (a::args)) | Pi (l,x,a,b) -> - let ty_a = infer' sg ctx a addi_eq in + let ty_a = infer' sg sub addi_eq d ctx a in let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer' sg ctx2 b addi_eq in + let ty_b = infer' sg sub addi_eq (d+1) ctx2 b in ( match ty_b with | Kind | Type _ -> ty_b | _ -> raise (TypingError (SortExpected (b, ctx2, ty_b))) ) | Lam (l,x,Some a,b) -> - let ty_a = infer' sg ctx a addi_eq in + let ty_a = infer' sg sub addi_eq d ctx a in let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer' sg ctx2 b addi_eq in + let ty_b = infer' sg sub addi_eq (d+1) ctx2 b in ( match ty_b with | Kind -> raise (TypingError (InexpectedKind (b, ctx2))) | _ -> mk_Pi l x a ty_b ) | Lam (l,_,None,_) -> raise (TypingError (DomainFreeLambda l)) - and check' sg (ctx:typed_context) (te:term) (ty_exp:typ) (addi_eq:cstr list) : unit = + and check' sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (te:term) (ty_exp:typ) : unit = Debug.(debug D_typeChecking "Checking (%a): %a : %a" pp_loc (get_loc te) pp_term te pp_term ty_exp); match te with | Lam (l,x,None,b) -> begin match R.whnf sg ty_exp with - | Pi (_,_,a,ty_b) -> check' sg ((l,x,a)::ctx) b ty_b addi_eq + | Pi (_,_,a,ty_b) -> check' sg sub addi_eq (d+1) ((l,x,a)::ctx) b ty_b | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) end | Lam (l,x,Some a,b) -> begin match R.whnf sg ty_exp with | Pi (_,_,a',ty_b) -> - ignore(infer' sg ctx a addi_eq); - if not (csq_of_eq sg a a' addi_eq) - then raise (TypingError (ConvertibilityError ((mk_DB l x 0),ctx,a',a))) - else check' sg ((l,x,a)::ctx) b ty_b addi_eq + ignore(infer' sg sub addi_eq d ctx a); + if not (convertible_under_cstr sg sub addi_eq d a a') + then raise (TypingError (ConvertibilityError ((mk_DB l x 0),ctx,a',a))) + else check' sg sub addi_eq (d+1) ((l,x,a)::ctx) b ty_b | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) end | _ -> - let ty_inf = infer' sg ctx te addi_eq in - Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" - pp_term ty_inf pp_term ty_exp); - if not (csq_of_eq sg ty_inf ty_exp addi_eq) - then - let ty_exp' = rename_vars_with_typed_context ctx ty_exp in - raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) - - and check_app sg (ctx:typed_context) (addi_eq:cstr list) (f,ty_f:term*typ) (arg:term) : term*typ = + let ty_inf = infer' sg sub addi_eq d ctx te in + Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" + pp_term ty_inf pp_term ty_exp); + if not (convertible_under_cstr sg sub addi_eq d ty_inf ty_exp) + then + let ty_exp' = rename_vars_with_typed_context ctx ty_exp in + raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) + + and check_app sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = match R.whnf sg ty_f with | Pi (_,_,a,b) -> - let _ = check' sg ctx arg a addi_eq in (mk_App f arg [], Subst.subst b arg ) + let _ = check' sg sub addi_eq d ctx arg a in + (mk_App f arg [], Subst.subst b arg ) | _ -> raise (TypingError ( ProductExpected (f,ctx,ty_f))) - let check sg ctx te ty = check' sg ctx te ty [] - let infer sg ctx te = infer' sg ctx te [] + let check sg = check' sg SS.identity [] 0 + let infer sg = infer' sg SS.identity [] 0 let inference sg (te:term) : typ = infer sg [] te @@ -255,7 +259,9 @@ struct type solver = { subst : SS.t; + (* ho_subst : (int*int*term) list; +*) unsolved : cstr list; unsatisf : cstr list } @@ -396,7 +402,7 @@ struct | false, s -> s | true, sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} in - process_solver {subst=SS.identity;ho_subst=[];unsolved=cstr;unsatisf=[]} + process_solver {subst=SS.identity;unsolved=cstr;unsatisf=[]} @@ -604,29 +610,28 @@ struct (if q > 0 then Format.sprintf " (under %i abstractions)" q else "") ); let sub = sol.subst in + (* let ty_le2 = SS.apply sub 0 ty_le in + *) let ctx = LList.lst delta.pctx in let ctx2 = try subst_context sub ctx with Subst.UnshiftExn -> (* TODO make Dedukti handle this case *) - Debug.( - debug D_rule "Failed to infer a typing context for the rule:\n%a" + begin + Debug.(debug D_rule) "Failed to infer a typing context for the rule:\n%a" pp_part_typed_rule rule; let ctx_name n = let _,name,_ = List.nth ctx n in name in - debug D_rule "Tried inferred typing substitution: %a" (SS.pp ctx_name) sub); - raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) ) ) + Debug.(debug D_rule) "Tried inferred typing substitution: %a" + (SS.pp ctx_name) sub; + raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) )) + end in - (* FIXME: Why is the RHS substituted ?! - Instead we should keep the original RHS and perform a check *modulo a substitution* - This simply means extend the check function to apply the substitution to all infered - types. *) - let ri2 = SS.apply sub 0 rule.rhs in Debug.(debug D_rule "Typechecking rule"); let cstr_nf = List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) sol.unsolved in - check' sg ctx2 ri2 ty_le2 cstr_nf; + check' sg sub cstr_nf 0 ctx2 rule.rhs ty_le; check_type_annotations sg sub ctx2 rule.ctx; Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" - pp_context_inline ctx2 pp_pattern rule.pat pp_term ri2); + pp_context_inline ctx pp_pattern rule.pat pp_term rule.rhs); sub, { name = rule.name; ctx = ctx2; diff --git a/tests/OK/higher_order_cstr3.dk b/tests/OK/higher_order_cstr3.dk index 1832f810..c1626e26 100644 --- a/tests/OK/higher_order_cstr3.dk +++ b/tests/OK/higher_order_cstr3.dk @@ -29,26 +29,26 @@ def g1 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z [x,y] g1 x y (z => t a) (z => t a) --> z => t a. def g2 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). -[x,y] g2 x y (z => t a) (z => t a) --> z => t a. +[x,y] g2 x y (z => t a) (z => t a) --> t a. def g3 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> z:A -> T (y z). [x,y] g3 x y (z => t z) (z => t a) --> z => t z. def g4 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T (x z)) -> T (y b). -[x,y] g4 x y (z => t z) (z => t a) --> z => t b. +[x,y] g4 x y (z => t z) (z => t a) --> t b. def h1 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). -[x,y] h1 x y (z => t a) (z => t (x z)) --> z => t a. +[x,y] h1 (z => x z) y (z => t a) (z => t (x z)) --> z => t a. def h2 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). -[x,y] h2 x y (z => t a) (z => t (x z)) --> z => t a. +[x,y] h2 (z => x z) y (z => t a) (z => t (x z)) --> t a. def h3 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> z:A -> T (y z). -[x,y] h3 x y (z => t z) (z => t (x z)) --> z => t z. +[x,y] h3 (z => x z) y (z => t z) (z => t (x z)) --> z => t z. def h4 : x:(A->A) -> y:(A->A) -> (z:A -> R (x z) (y z)) -> (z:A -> T a) -> T (y b). -[x,y] h4 x y (z => t z) (z => t (x z)) --> z => t b. +[x,y] h4 (z=>x z) y (z => t z) (z => t (x z)) --> t b. @@ -57,23 +57,23 @@ def g'1 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> [x,y] g'1 x y (z => t a) (z => t a) --> z => t a. def g'2 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). -[x,y] g'2 x y (z => t a) (z => t a) --> z => t a. +[x,y] g'2 x y (z => t a) (z => t a) --> t a. def g'3 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). [x,y] g'3 x y (z => t a) (z => t z) --> z => t z. def g'4 : x:(A->A) -> y:(A->A) -> (z:A -> T (x z)) -> (z:A -> R (x z) (y z)) -> T (y b). -[x,y] g'4 x y (z => t a) (z => t z) --> z => t b. +[x,y] g'4 x y (z => t a) (z => t z) --> t b. def h'1 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). -[x,y] h'1 x y (z => t (x z)) (z => t a) --> z => t a. +[x,y] h'1 (z=>x z) y (z => t (x z)) (z => t a) --> z => t a. def h'2 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). -[x,y] h'2 x y (z => t (x z)) (z => t a) --> z => t a. +[x,y] h'2 (z=>x z) y (z => t (x z)) (z => t a) --> t a. def h'3 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> z:A -> T (y z). -[x,y] h'3 x y (z => t (x z)) (z => t z) --> z => t z. +[x,y] h'3 (z=>x z) y (z => t (x z)) (z => t z) --> z => t z. def h'4 : x:(A->A) -> y:(A->A) -> (z:A -> T a) -> (z:A -> R (x z) (y z)) -> T (y b). -[x,y] h'4 x y (z => t (x z)) (z => t z) --> z => t b. +[x,y] h'4 (z=>x z) y (z => t (x z)) (z => t z) --> t b. From 4f2db0e1ee4b316e24981c9bdc454cd8f6d49c2f Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 11 Dec 2019 14:47:12 +0100 Subject: [PATCH 20/35] Fixed extended substitution application. --- kernel/exsubst.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index 052e2e8d..e52d295f 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -11,13 +11,16 @@ let apply_exsubst (subst:ex_substitution) : int -> term -> term = let rec aux k t = match t with (* k counts the number of local lambda abstractions *) | DB (l,x,n) when n >= k -> (* a free variable *) ( try let res = subst l x n 0 k in incr ct; res with Not_found -> t) - | App (DB (l,x,n),a,args) when n >= k -> (* an applied free variable *) - ( try + | App (DB (l,x,n) as db,a,args) when n >= k -> (* an applied free variable *) + let ct' = !ct in + let f' = + try let res = subst l x n (1+(List.length args)) k in incr ct; - let a', args' = aux k a, List.map (aux k) args in - mk_App res a' args' - with Not_found -> t) + res + with Not_found -> db in + let a', args' = aux k a, List.map (aux k) args in + if !ct = ct' then t else mk_App f' a' args' | App (f,a,args) -> let ct' = !ct in let f', a', args' = aux k f, aux k a, List.map (aux k) args in From 39fb14359487840f93464b45a98be33ccd9ef0ae Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 13 Dec 2019 09:15:48 +0100 Subject: [PATCH 21/35] Added comments and removed unused Subst module. --- kernel/exsubst.ml | 7 ++++--- kernel/exsubst.mli | 14 ++++++++++++-- kernel/subst.ml | 37 +------------------------------------ kernel/subst.mli | 36 ------------------------------------ 4 files changed, 17 insertions(+), 77 deletions(-) diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index e52d295f..d4232084 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -45,14 +45,15 @@ module IntMap = Map.Make( module ExSubst = struct type t = (int*term) IntMap.t + (* Maps a DB index to an arity and a lambda-lifted substitute *) let identity = IntMap.empty - let is_identity = IntMap.is_empty let subst (sigma:t) = fun _ _ n nargs k -> - let (argmin,t) = IntMap.find (n-k) sigma in - if nargs >= argmin then Subst.shift k t else raise Not_found + let (arity,t) = IntMap.find (n-k) sigma in + if nargs >= arity then Subst.shift k t else raise Not_found + let subst2 (sigma:t) (i:int) = fun _ _ n nargs k -> let (argmin,t) = IntMap.find (n+i+1-k) sigma in diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli index 4317d219..2445f3f8 100644 --- a/kernel/exsubst.mli +++ b/kernel/exsubst.mli @@ -33,10 +33,20 @@ sig (** [add sigma n t] returns the substitution [sigma] with the extra mapping [n] -> [t]. *) val subst : t -> ex_substitution - (** Provides substitution from Subst instance. *) + (** Substitution function corresponding to given ExSubst.t instance [sigma]. + We lookup the table at index: (DB index) [n] - (nb of local binders) [k] + When the variable is under applied it is simply not substituted. + Otherwise we return the reduct is shifted up by (nb of local binders) [k] *) val subst2 : t -> int -> ex_substitution - (** Provides special substitution from Subst instance. *) + (** Special substitution function corresponding to given ExSubst.t instance [sigma] + "in a smaller context": + Assume [sigma] a substitution in a context Gamma = Gamma' ; Delta with |Delta|=[i]. + Then this function represents the substitution [sigma] in the context Gamma'. + All variables of Delta are ignored and substitutes of the variables of Gamma' + are unshifted. This may therefore raise UnshiftExn in case substitutes of + variables of Gamma' refers to variables of Delta. + *) val apply : t -> int -> term -> term (** [apply sigma n t] applies the subsitution [sigma] to [t] considered diff --git a/kernel/subst.ml b/kernel/subst.ml index b9d2016d..0df86444 100644 --- a/kernel/subst.ml +++ b/kernel/subst.ml @@ -1,5 +1,4 @@ open Basic -open Format open Term exception UnshiftExn @@ -60,8 +59,8 @@ let subst (te:term) (u:term) = let subst_n m y = apply_subst (fun l x n k -> if n = m+k then mk_DB l y k else mk_DB l x (n+1)) 0 -exception Occurs let occurs (n:int) (te:term) : bool = + let exception Occurs in let rec aux depth = function | Kind | Type _ | Const _ -> () | DB (_,_,k) -> if k = n + depth then raise Occurs else () @@ -71,37 +70,3 @@ let occurs (n:int) (te:term) : bool = | Pi (_,_,a,b) -> aux depth a; aux (depth+1) b in try aux 0 te; false with Occurs -> true - -module IntMap = Map.Make( - struct - type t = int - let compare = compare - end) - -module Subst = -struct - type t = term IntMap.t - let identity = IntMap.empty - - let is_identity = IntMap.is_empty - - let subst (sigma:t) = fun _ _ n k -> shift k (IntMap.find (n-k) sigma) - let subst2 (sigma:t) (i:int) = fun _ _ n k -> shift k (unshift (i+1) (IntMap.find (n+i+1-k) sigma)) - - let apply (sigma:t) : int -> term -> term = - if is_identity sigma then (fun _ t -> t) else apply_subst (subst sigma) - - let add (sigma:t) (n:int) (t:term) : t = - assert ( not (IntMap.mem n sigma) ); - IntMap.add n t sigma - - let rec mk_idempotent (sigma:t) : t = - let sigma2:t = IntMap.map (apply sigma 0) sigma in - if IntMap.equal term_eq sigma sigma2 then sigma - else mk_idempotent sigma2 - - let pp (name:(int->ident)) (fmt:formatter) (sigma:t) : unit = - let pp_aux i t = fprintf fmt " %a[%i] -> %a\n" pp_ident (name i) i pp_term t in - IntMap.iter pp_aux sigma - -end diff --git a/kernel/subst.mli b/kernel/subst.mli index 3efb1ae2..eb5b35ce 100644 --- a/kernel/subst.mli +++ b/kernel/subst.mli @@ -37,39 +37,3 @@ val subst_n : int -> Basic.ident -> term -> term (** [occurs n t] returns true if [t] contains the variable [n]. *) val occurs : int -> term -> bool - -(** This modules implements substitution of DB variables in a term. - This is typically used to: - 1) infer a "most general" typing substitution from constraints gathered while - inferring the type of the LHS of a rule. - 2) apply the substitution to the RHS of the rule before typechecking it. -*) -module Subst : -sig - type t - - val identity : t - (** Empty substitution *) - - val is_identity : t -> bool - (** Checks emptyness *) - - val add : t -> int -> term -> t - (** [add sigma n t] returns the substitution [sigma] with the extra mapping [n] -> [t]. *) - - val subst : t -> substitution - (** Provides substitution from Subst instance. *) - - val subst2 : t -> int -> substitution - (** Provides special substitution from Subst instance. *) - - val apply : t -> int -> term -> term - (** [apply sigma n t] applies the subsitution [sigma] to [t] considered under [n] lambda abstractions. *) - - val mk_idempotent : t -> t - (** [mk_idempotent sigma] successively applies sigma to its mapped terms until this operation - has no effect anymore. *) - - val pp : (int->Basic.ident) -> t Basic.printer - (** Prints the substitution using given naming function *) -end From 0b701553d2f300c6e371dae3110957504c4490ae Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 13 Dec 2019 10:59:10 +0100 Subject: [PATCH 22/35] Some style. Fixed a test. Made convertible_under_cstr tail rec. --- kernel/typing.ml | 338 +++++++++++++++++++++--------------------- tests/KO/self_dep2.dk | 2 +- 2 files changed, 166 insertions(+), 174 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 83f88e04..60065703 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -70,30 +70,30 @@ struct type cstr = int*term*term (* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) - (* - let pp_cstr fmt (n,t1,t2) = - fprintf fmt "[%i] %a ~ %a" n pp_term t1 pp_term t2 - *) - - let is_same_cstr ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = + let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in (term_eq t1' t2' && term_eq u1' u2') || - (term_eq t1' u2' && term_eq u1' t2') - - let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (addi_eq:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = - let rec bis n ty1 ty2 = - List.exists (is_same_cstr (n,ty1,ty2)) addi_eq || - match ty1,ty2 with - | App(h1,a1,l1), App(h2,a2,l2) -> List.for_all2 (bis n) (h1::a1::l1) (h2::a2::l2) - | Lam(_,_,_,t1), Lam(_,_,_,t2) -> bis (n+1) t1 t2 - | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> bis n a1 a2 && bis (n+1) b1 b2 - | _ -> term_eq ty1 ty2 - in + (term_eq t1' u2' && term_eq u1' t2') + + let term_eq_under_cstr (eq_cstr:cstr list) : typ -> typ -> bool = + let rec aux = function + | [] -> true + | (n,t1,t2)::tl -> + List.exists (cstr_eq (n,t1,t2)) eq_cstr || + match t1,t2 with + | App(h1,a1,l1), App(h2,a2,l2) -> + aux ((n,h1,h2)::(n,a1,a2)::(List.map2 (fun x y -> (n,x,y)) l1 l2)@tl) + | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) + | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) + | _ -> term_eq t1 t2 && aux tl + in fun t1 t2 -> eq_cstr <> [] && aux [(0,t1,t2)] + + let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (eq_cstr:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = let subst_ty_inf = SS.apply sub depth ty_inf in let subst_ty_exp = SS.apply sub depth ty_exp in R.are_convertible sg subst_ty_inf subst_ty_exp || - (addi_eq <> [] && bis 0 (R.snf sg subst_ty_inf) (R.snf sg subst_ty_exp)) + term_eq_under_cstr eq_cstr (R.snf sg subst_ty_inf) (R.snf sg subst_ty_exp) (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) @@ -117,7 +117,7 @@ struct | Kind | Type _ -> ty_b | _ -> raise (TypingError (SortExpected (b, ctx2, ty_b))) ) | Lam (l,x,Some a,b) -> - let ty_a = infer' sg sub addi_eq d ctx a in + let ty_a = infer' sg sub addi_eq d ctx a in let ctx2 = extend_ctx (l,x,a) ctx ty_a in let ty_b = infer' sg sub addi_eq (d+1) ctx2 b in ( match ty_b with @@ -146,7 +146,7 @@ struct | _ -> let ty_inf = infer' sg sub addi_eq d ctx te in Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" - pp_term ty_inf pp_term ty_exp); + pp_term ty_inf pp_term ty_exp); if not (convertible_under_cstr sg sub addi_eq d ty_inf ty_exp) then let ty_exp' = rename_vars_with_typed_context ctx ty_exp in @@ -184,7 +184,7 @@ struct try Some (Subst.unshift q t) with Subst.UnshiftExn -> ( try Some (Subst.unshift q (R.snf sg t)) - with Subst.UnshiftExn -> None ) + with Subst.UnshiftExn -> None ) (** Under [d] lambdas, checks whether term [te] *must* contain an occurence of any variable that satisfies the given predicate [p], @@ -201,23 +201,23 @@ struct let rec aux = function | [] -> () | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) - match t with - | Kind | Type _ | Const _ -> aux tl - | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) - | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) - | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) - | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl - | App (f,a,args) -> + match t with + | Kind | Type _ | Const _ -> aux tl + | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) + | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) + | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) + | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl + | App (f,a,args) -> begin match f with | DB (_,_,n) when n >= k + d -> (* a matching variable *) - if p (n-k) then raise VarSurelyOccurs else aux tl + if p (n-k) then raise VarSurelyOccurs else aux tl | DB (_,_,n) when n < k + d -> (* a locally bound variable *) - if n >= k && p (n-k) - then raise VarSurelyOccurs - else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) + if n >= k && p (n-k) + then raise VarSurelyOccurs + else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) | Const (l,cst) when Signature.is_static sg l cst -> - ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) + ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) | _ -> aux tl (* Default case encompasses: - Meta variables: DB(_,_,n) with n >= k + d @@ -245,21 +245,18 @@ struct let rec aux = function | [] -> () | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) - match t with - | DB (_,_,n) -> (if n >= k && n < k + d then vars.(n-k) <- true); aux tl - | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) - | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) - | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) - | App (f,a,args) -> aux ((k,f)::(k,a):: (List.map (fun t -> (k,t)) args) @ tl) - | _ -> aux tl + match t with + | DB (_,_,n) -> (if n >= k && n < k + d then vars.(n-k) <- true); aux tl + | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) + | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) + | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) + | App (f,a,args) -> aux ((k,f)::(k,a):: (List.map (fun t -> (k,t)) args) @ tl) + | _ -> aux tl in aux (List.map (fun t -> (0,t)) terms); vars type solver = { subst : SS.t; - (* - ho_subst : (int*int*term) list; -*) unsolved : cstr list; unsatisf : cstr list } @@ -272,124 +269,122 @@ struct let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function | [] -> (flag, s) - | (q,t1,t2)::lst -> - begin - let t1' = R.whnf sg (SS.apply s.subst q t1) in - let t2' = R.whnf sg (SS.apply s.subst q t2) in - let dropped () = pseudo_u sg flag s lst in - let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in - let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in - if term_eq t1' t2' then dropped () - else - match t1', t2' with - | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) - | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) - | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () - - | Pi (_,_,a,b), Pi (_,_,a',b') -> - pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) - | Lam (_,_,_,b), Lam (_,_,_,b') -> - pseudo_u sg true s ((q+1,b,b')::lst) - - (* Potentially eta-equivalent terms *) - | Lam (_,i,_,b), a when !Reduction.eta -> - let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg true s ((q+1,b,b')::lst) + | (q,t1,t2)::lst -> begin + let t1' = R.whnf sg (SS.apply s.subst q t1) in + let t2' = R.whnf sg (SS.apply s.subst q t2) in + let dropped () = pseudo_u sg flag s lst in + let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in + let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in + let subst db ar te = pseudo_u sg true { s with subst=SS.add s.subst db ar te } lst in + if term_eq t1' t2' then dropped () + else + match t1', t2' with + | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) + | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) + | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () + + | Pi (_,_,a,b), Pi (_,_,a',b') -> + pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) + | Lam (_,_,_,b), Lam (_,_,_,b') -> + pseudo_u sg true s ((q+1,b,b')::lst) + + (* Potentially eta-equivalent terms *) + | Lam (_,i,_,b), a when !Reduction.eta -> + let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in + pseudo_u sg true s ((q+1,b,b')::lst) | a, Lam (_,i,_,b) when !Reduction.eta -> - let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg true s ((q+1,b,b')::lst) + let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in + pseudo_u sg true s ((q+1,b,b')::lst) - (* A definable symbol is only be convertible with closed terms *) + (* A definable symbol is only be convertible with closed terms *) | Const (l,cst), t when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() | t, Const (l,cst) when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() - (* X = Y : map either X to Y or Y to X *) + (* X = Y : map either X to Y or Y to X *) | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> - let (n,t) = if n1=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then unsatisf() - else begin - match unshift_reduce sg q t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() - else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst - end + if sure_occur_check sg q (fun k -> k <= q || k = n) t + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + end | t, DB (_,_,n) when n>=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then unsatisf() - else begin - match unshift_reduce sg q t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() - else pseudo_u sg true {s with subst=SS.add s.subst n' 0 t'} lst - end - - (* f t1 ... tn / X t1 ... tn = u - 1) Gather all free variables in t1 ... tn - 2) Make sure u only relies on these variables - *) + if sure_occur_check sg q (fun k -> k <= q || k = n) t + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + end + + (* f t1 ... tn / X t1 ... tn = u + 1) Gather all free variables in t1 ... tn + 2) Make sure u only relies on these variables + *) | App (DB (_,_,n),a,args), t when n >= q -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() - else begin - match try_solve q (a::args) t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) - else pseudo_u sg true - {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsolved() + (* X = t[X] cannot be turned into a (extended-)substitution *) + else subst n' (1+(List.length args)) t' end | t, App (DB (_,_,n),a,args) when n >= q -> let occs = gather_free_vars q (a::args) in if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t then unsatisf() else begin - match try_solve q (a::args) t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsolved() (* X = t[X] cannot be turned into a (extended-)substitution *) - else pseudo_u sg true - {s with subst=SS.add s.subst n' (1+(List.length args)) t'} lst + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsolved() + (* X = t[X] cannot be turned into a (extended-)substitution *) + else subst n' (1+(List.length args)) t' end | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() | t, App (Const (l,cst),a,args) when not (Signature.is_static sg l cst) -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() | App (f,a,args), App (f',a',args') -> - (* f = Kind | Type | DB n when n unsatisf() (* Different number of arguments. *) - | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) - end + (* f = Kind | Type | DB n when n unsatisf() (* Different number of arguments. *) + | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) + end | _, _ -> unsatisf() end @@ -497,60 +492,60 @@ struct match pat with | Lambda (l,x,p) -> begin - match R.whnf sg exp_ty with - | Pi (_,_,a,b) -> check_pattern sg delta (LList.cons (l,x,a) sigma) b lst p - | _ -> raise (TypingError ( ProductExpected (pattern_to_term pat,ctx (),exp_ty))) + match R.whnf sg exp_ty with + | Pi (_,_,a,b) -> check_pattern sg delta (LList.cons (l,x,a) sigma) b lst p + | _ -> raise (TypingError ( ProductExpected (pattern_to_term pat,ctx (),exp_ty))) end | Brackets te -> let _ = - try Subst.unshift (LList.len sigma) te - with Subst.UnshiftExn -> raise (TypingError (BracketExprBoundVar (te,ctx()))) + try Subst.unshift (LList.len sigma) te + with Subst.UnshiftExn -> raise (TypingError (BracketExprBoundVar (te,ctx()))) in let exp_ty2 = - try unshift_n sg (LList.len sigma) exp_ty - with Subst.UnshiftExn -> + try unshift_n sg (LList.len sigma) exp_ty + with Subst.UnshiftExn -> raise (TypingError (BracketExpectedTypeBoundVar (te,ctx(),exp_ty))) in let _ = - try unshift_n sg delta.padding exp_ty2 - with Subst.UnshiftExn -> + try unshift_n sg delta.padding exp_ty2 + with Subst.UnshiftExn -> raise (TypingError (BracketExpectedTypeRightVar (te,ctx(),exp_ty))) in ( {delta with bracket = true}, lst) | Var (l,x,n,[]) when n >= LList.len sigma -> begin - let k = LList.len sigma in + let k = LList.len sigma in (* Bracket may introduce circularity (variable's expected type depending on itself *) - if delta.bracket && Subst.occurs (n-k) exp_ty - then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); - if pc_in delta (n-k) - then + if delta.bracket && Subst.occurs (n-k) exp_ty + then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); + if pc_in delta (n-k) + then let inf_ty = Subst.shift k (pc_get delta (n-k)) in ( delta, (k,inf_ty,exp_ty)::lst ) - else + else ( try ( pc_add delta (n-k) l x (unshift_n sg k exp_ty), lst ) with Subst.UnshiftExn -> raise (TypingError (FreeVariableDependsOnBoundVariable (l,x,n,ctx(),exp_ty))) ) end | Var (l,x,n,args) when n >= LList.len sigma -> begin - let k = LList.len sigma in + let k = LList.len sigma in (* Bracket may introduce circularity (variable's expected type depending on itself *) - if delta.bracket && Subst.occurs (n-k) exp_ty - then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); - let (args2, last) = get_last args in - match last with - | Var (l2,x2,n2,[]) -> + if delta.bracket && Subst.occurs (n-k) exp_ty + then raise (TypingError (TypingCircularity(l,x,n,ctx(),exp_ty))); + let (args2, last) = get_last args in + match last with + | Var (l2,x2,n2,[]) -> check_pattern sg delta sigma (mk_Pi l2 x2 (get_type (LList.lst sigma) l2 x2 n2) (Subst.subst_n n2 x2 exp_ty) ) lst (Var(l,x,n,args2)) - | _ -> raise (TypingError (CannotInferTypeOfPattern (pat,ctx ()))) (* not a pattern *) + | _ -> raise (TypingError (CannotInferTypeOfPattern (pat,ctx ()))) (* not a pattern *) end | _ -> begin - let (inf_ty,delta2,lst2) = infer_pattern sg delta sigma lst pat in - let q = LList.len sigma in - ( delta2 , (q,inf_ty,exp_ty)::lst2 ) + let (inf_ty,delta2,lst2) = infer_pattern sg delta sigma lst pat in + let q = LList.len sigma in + ( delta2 , (q,inf_ty,exp_ty)::lst2 ) end (* ************************************************************************** *) @@ -571,7 +566,7 @@ struct let rec aux ctx depth ctx1 ctx2 = match ctx1, ctx2 with | (l,x,ty)::ctx1' , (_,_,ty')::ctx2' -> - begin + begin match ty' with | None -> () | Some ty' -> @@ -583,8 +578,8 @@ struct let ty2' = SS.apply sub 0 (Subst.shift depth ty') in if not (R.are_convertible sg ty2 ty2') then raise (TypingError (AnnotConvertibilityError (l,x,ctx,ty',ty))) - end; - aux ((l,x,ty)::ctx) (depth+1) ctx1' ctx2' + end; + aux ((l,x,ty)::ctx) (depth+1) ctx1' ctx2' | [], [] -> () | _ -> assert false in aux [] 1 typed_ctx annot_ctx @@ -601,21 +596,18 @@ struct if !fail_on_unsatisfiable_constraints then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) else - Debug.(debug D_warn) - "At %a: unsatisfiable constraint: %a ~ %a%s" + Debug.(debug D_warn) + "At %a: unsatisfiable constraint: %a ~ %a%s" pp_loc (get_loc_rule rule) pp_term t1 pp_term t2 (if q > 0 then Format.sprintf " (under %i abstractions)" q else "") ); let sub = sol.subst in - (* - let ty_le2 = SS.apply sub 0 ty_le in - *) let ctx = LList.lst delta.pctx in let ctx2 = try subst_context sub ctx with Subst.UnshiftExn -> (* TODO make Dedukti handle this case *) - begin + begin Debug.(debug D_rule) "Failed to infer a typing context for the rule:\n%a" pp_part_typed_rule rule; let ctx_name n = let _,name,_ = List.nth ctx n in name in diff --git a/tests/KO/self_dep2.dk b/tests/KO/self_dep2.dk index 84d0f563..9eb0d731 100644 --- a/tests/KO/self_dep2.dk +++ b/tests/KO/self_dep2.dk @@ -1,7 +1,7 @@ (; KO 101 ;) def A : Type. -U : A -> Type. +def U : A -> Type. def a : A. def B : Type. From 7450167b1b4a1ab1c13ea02ee79d1bd47fbf9a9f Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 13 Dec 2019 16:01:26 +0100 Subject: [PATCH 23/35] Experimentations. --- kernel/exsubst.ml | 28 ++++++++++------ kernel/exsubst.mli | 9 ++--- kernel/typing.ml | 83 +++++++++++++++++++++++++++------------------- tests/OK/WIP.dk | 49 +++++++++++++++++++++++++++ 4 files changed, 121 insertions(+), 48 deletions(-) create mode 100644 tests/OK/WIP.dk diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index d4232084..c16b385c 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -4,7 +4,7 @@ open Term type ex_substitution = loc -> ident -> int -> int -> int -> term -let apply_exsubst (subst:ex_substitution) : int -> term -> term = +let apply_exsubst (subst:ex_substitution) (n:int) (te:term) : term*bool = let ct = ref 0 in (* aux increments this counter every time a substitution occurs. * Terms are reused when no substitution occurs in recursive calls. *) @@ -34,7 +34,7 @@ let apply_exsubst (subst:ex_substitution) : int -> term -> term = let a', b' = aux k a, aux (k+1) b in if !ct = ct' then t else mk_Pi l x a' b' | _ -> t - in aux + in (aux n te, !ct > 0) module IntMap = Map.Make( struct @@ -59,24 +59,32 @@ struct let (argmin,t) = IntMap.find (n+i+1-k) sigma in if nargs >= argmin then Subst.shift k (Subst.unshift (i+1) t) else raise Not_found - let apply (sigma:t) : int -> term -> term = - if is_identity sigma then (fun _ t -> t) else apply_exsubst (subst sigma) + let apply (sigma:t) : int -> term -> term*bool = + if is_identity sigma then (fun _ t -> t,false) else apply_exsubst (subst sigma) let add (sigma:t) (n:int) (nargs:int) (t:term) : t = -(* assert ( not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs ); -*) if not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs then IntMap.add n (nargs,t) sigma else sigma + let applys (sigma:t) : t -> t*bool = + if is_identity sigma then (fun t -> t,false) + else fun sigma' -> + let modified = ref false in + let applysigma (n,t) = + let res,flag = apply sigma 0 t in + if flag then modified := true; + (n,res) + in + IntMap.map applysigma sigma', !modified + let rec mk_idempotent (sigma:t) : t = - let sigma2:t = IntMap.map (fun (n,t) -> n,apply sigma 0 t) sigma in - if IntMap.equal (fun (n1,t1) (n2,t2) -> n1 = n2 && term_eq t1 t2) sigma sigma2 then sigma - else mk_idempotent sigma2 + let sigma', flag = applys sigma sigma in + if flag then mk_idempotent sigma' else sigma let pp (name:(int->ident)) (fmt:formatter) (sigma:t) : unit = let pp_aux i (n,t) = - fprintf fmt " %a[%i](...%i...) -> %a(...)\n" pp_ident (name i) i n pp_term t in + fprintf fmt " %a[%i](%i args) -> %a\n" pp_ident (name i) i n pp_term t in IntMap.iter pp_aux sigma end diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli index 2445f3f8..156639cb 100644 --- a/kernel/exsubst.mli +++ b/kernel/exsubst.mli @@ -8,10 +8,11 @@ open Term A substitution raises Not_found meaning that the variable is not subsituted. *) type ex_substitution = Basic.loc -> Basic.ident -> int -> int -> int -> term -(** [apply_subst subst n t] applies [subst] to [t] under [n] lambda abstractions. +(** [apply_exsubst subst n t] applies [subst] to [t] under [n] lambda abstractions. - Variables with DB index [k] < [n] are considered "locally bound" and are never substituted. - - Variables with DB index [k] >= [n] may be substituted if [k-n] is mapped in [sigma]. *) -val apply_exsubst : ex_substitution -> int -> term -> term + - Variables with DB index [k] >= [n] may be substituted if [k-n] is mapped in [sigma] + and if they occur applied to enough arguments (substitution's arity). *) +val apply_exsubst : ex_substitution -> int -> term -> term*bool (** This modules implements extended substitution of DB variables in a term. This is typically used to: @@ -48,7 +49,7 @@ sig variables of Gamma' refers to variables of Delta. *) - val apply : t -> int -> term -> term + val apply : t -> int -> term -> term*bool (** [apply sigma n t] applies the subsitution [sigma] to [t] considered under [n] lambda abstractions. *) diff --git a/kernel/typing.ml b/kernel/typing.ml index 60065703..aa695630 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -73,8 +73,7 @@ struct let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in - (term_eq t1' t2' && term_eq u1' u2') || - (term_eq t1' u2' && term_eq u1' t2') + (term_eq t1' t2' && term_eq u1' u2') || (term_eq t1' u2' && term_eq u1' t2') let term_eq_under_cstr (eq_cstr:cstr list) : typ -> typ -> bool = let rec aux = function @@ -83,17 +82,27 @@ struct List.exists (cstr_eq (n,t1,t2)) eq_cstr || match t1,t2 with | App(h1,a1,l1), App(h2,a2,l2) -> + List.length l1 = List.length l2 && aux ((n,h1,h2)::(n,a1,a2)::(List.map2 (fun x y -> (n,x,y)) l1 l2)@tl) | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) | _ -> term_eq t1 t2 && aux tl in fun t1 t2 -> eq_cstr <> [] && aux [(0,t1,t2)] + let rec full_snf sg subst d t = + let t1 = R.snf sg t in + let t2,flag = SS.apply subst d t1 in + if flag then full_snf sg subst d t2 else R.snf sg t2 + let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (eq_cstr:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = - let subst_ty_inf = SS.apply sub depth ty_inf in - let subst_ty_exp = SS.apply sub depth ty_exp in - R.are_convertible sg subst_ty_inf subst_ty_exp || - term_eq_under_cstr eq_cstr (R.snf sg subst_ty_inf) (R.snf sg subst_ty_exp) + let subst_ty_inf,_ = SS.apply sub depth ty_inf in + let subst_ty_exp,_ = SS.apply sub depth ty_exp in + if R.are_convertible sg subst_ty_inf subst_ty_exp then true + else + let snf_ty_inf = full_snf sg sub depth subst_ty_inf in + let snf_ty_exp = full_snf sg sub depth subst_ty_exp in + R.are_convertible sg snf_ty_inf snf_ty_exp || + term_eq_under_cstr eq_cstr snf_ty_inf snf_ty_exp (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) @@ -151,7 +160,6 @@ struct then let ty_exp' = rename_vars_with_typed_context ctx ty_exp in raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) - and check_app sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = match R.whnf sg ty_f with | Pi (_,_,a,b) -> @@ -208,23 +216,23 @@ struct | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl | App (f,a,args) -> - begin - match f with - | DB (_,_,n) when n >= k + d -> (* a matching variable *) - if p (n-k) then raise VarSurelyOccurs else aux tl - | DB (_,_,n) when n < k + d -> (* a locally bound variable *) - if n >= k && p (n-k) - then raise VarSurelyOccurs - else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) - | Const (l,cst) when Signature.is_static sg l cst -> - ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) - | _ -> aux tl - (* Default case encompasses: - - Meta variables: DB(_,_,n) with n >= k + d - - Definable symbols - - Lambdas (FIXME: when can this happen ?) - - Illegal applications *) - end + begin + match f with + | DB (_,_,n) -> + if n >= k && p (n-k) + then raise VarSurelyOccurs + else if n >= k + d (* a matching variable *) + then aux tl + else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) + | Const (l,cst) when Signature.is_static sg l cst -> + ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) + | _ -> aux tl + (* Default case encompasses: + - Meta variables: DB(_,_,n) with n >= k + d + - Definable symbols + - Lambdas (FIXME: when can this happen ?) + - Illegal applications *) + end in try aux [(0,te)]; false with VarSurelyOccurs -> true @@ -267,15 +275,22 @@ struct Some (Matching.solve q (LList.of_list dbs) t) with Matching.NotUnifiable -> None + let rec full_whnf sg subst d t = + let t1 = R.whnf sg t in + let t2,flag = SS.apply subst d t1 in + if flag then full_whnf sg subst d t2 else R.whnf sg t2 + let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function | [] -> (flag, s) | (q,t1,t2)::lst -> begin - let t1' = R.whnf sg (SS.apply s.subst q t1) in - let t2' = R.whnf sg (SS.apply s.subst q t2) in + let t1' = full_whnf sg s.subst q t1 in + let t2' = full_whnf sg s.subst q t2 in let dropped () = pseudo_u sg flag s lst in let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in - let subst db ar te = pseudo_u sg true { s with subst=SS.add s.subst db ar te } lst in + let subst db ar te = + let subst' = SS.add s.subst db ar te in + pseudo_u sg true { s with subst=subst' } lst in if term_eq t1' t2' then dropped () else match t1', t2' with @@ -392,8 +407,8 @@ struct let solve_cstr (sg : Signature.t) (cstr : cstr list) : solver = let rec process_solver sol = match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with - | false, s -> s - | true, sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} + | false, s -> s + | true , sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} in process_solver {subst=SS.identity;unsolved=cstr;unsatisf=[]} @@ -558,7 +573,7 @@ struct let subst_context (sub:SS.t) (ctx:typed_context) : typed_context = if SS.is_identity sub then ctx else - let apply_subst i (l,x,ty) = (l,x,Exsubst.apply_exsubst (SS.subst2 sub i) 0 ty) in + let apply_subst i (l,x,ty) = (l,x,fst (Exsubst.apply_exsubst (SS.subst2 sub i) 0 ty)) in List.mapi apply_subst ctx let check_type_annotations sg sub typed_ctx annot_ctx = @@ -574,8 +589,8 @@ struct pp_loc l pp_term ty pp_term ty'); if not (R.are_convertible sg ty ty') then - let ty2 = SS.apply sub 0 (Subst.shift depth ty ) in - let ty2' = SS.apply sub 0 (Subst.shift depth ty') in + let ty2 = fst (SS.apply sub 0 (Subst.shift depth ty )) in + let ty2' = fst (SS.apply sub 0 (Subst.shift depth ty')) in if not (R.are_convertible sg ty2 ty2') then raise (TypingError (AnnotConvertibilityError (l,x,ctx,ty',ty))) end; @@ -596,8 +611,8 @@ struct if !fail_on_unsatisfiable_constraints then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) else - Debug.(debug D_warn) - "At %a: unsatisfiable constraint: %a ~ %a%s" + Debug.(debug D_warn) + "At %a: unsatisfiable constraint: %a ~ %a%s" pp_loc (get_loc_rule rule) pp_term t1 pp_term t2 (if q > 0 then Format.sprintf " (under %i abstractions)" q else "") diff --git a/tests/OK/WIP.dk b/tests/OK/WIP.dk new file mode 100644 index 00000000..aeb6d214 --- /dev/null +++ b/tests/OK/WIP.dk @@ -0,0 +1,49 @@ +(; OK ;) + +A : Type. +a : A. a' : A. +c : A -> A -> A. + +T : A -> Type. +t : a : A -> T a. + +U : (A -> A) -> Type. +u : a : (A -> A) -> U a. + +V : (A -> A -> A) -> Type. +v : a : (A -> A -> A) -> V a. + +def flip : A -> A. +[X,Y] flip (c X Y) --> c Y X. + +def test1 : f : (A -> A -> A) -> + (x:A -> U (f x)) -> + (x:A -> y:A -> T (f x y)) -> + V (x => y => f y x). +(; Constraints: + x,y |- F x y = c x y + x |- G x = F x ;) +[F,G] + test1 F (x => u (G x)) (x => y => t (c x y)) + --> + v (x => y => flip (G x y)). + + +d : (A -> A -> A) -> (A -> A -> A). +def e : (A -> A -> A) -> (A -> A -> A). +[X] e (d X) --> X. + + +def test2 : f : (A -> A -> A) -> + (x:A -> U (e f x)) -> + (x:A -> y:A -> T (e f x y)) -> + V f -> + V (x => y => flip (e f y x)). +(; Constraints: + |- F = d H + x,y |- H x y = c x y + x |- G x = H x ;) +[F,G,H] + test2 F (x => u (G x)) (x => y => t (c x y)) (v (d H)) + --> + v (x => y => G x y). From b1de1b5e22189813d39c09cd67f1627e6bab6254 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Fri, 13 Dec 2019 19:31:42 +0100 Subject: [PATCH 24/35] WIP --- kernel/typing.ml | 18 +++++++++--------- tests/KO/church.dk | 2 +- 2 files changed, 10 insertions(+), 10 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index aa695630..98f3ffb2 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -95,12 +95,14 @@ struct if flag then full_snf sg subst d t2 else R.snf sg t2 let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (eq_cstr:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = - let subst_ty_inf,_ = SS.apply sub depth ty_inf in - let subst_ty_exp,_ = SS.apply sub depth ty_exp in - if R.are_convertible sg subst_ty_inf subst_ty_exp then true - else - let snf_ty_inf = full_snf sg sub depth subst_ty_inf in - let snf_ty_exp = full_snf sg sub depth subst_ty_exp in + R.are_convertible sg ty_inf ty_exp || + match SS.is_identity sub, eq_cstr with + | true, [] -> false + | true, _ -> term_eq_under_cstr eq_cstr (R.snf sg ty_inf) (R.snf sg ty_exp) + | false,_ -> + let snf_ty_inf = full_snf sg sub depth ty_inf in + let snf_ty_exp = full_snf sg sub depth ty_exp in + Debug.(debug D_warn) "Test %a ~ %a" pp_term snf_ty_inf pp_term snf_ty_exp; R.are_convertible sg snf_ty_inf snf_ty_exp || term_eq_under_cstr eq_cstr snf_ty_inf snf_ty_exp @@ -288,9 +290,7 @@ struct let dropped () = pseudo_u sg flag s lst in let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in - let subst db ar te = - let subst' = SS.add s.subst db ar te in - pseudo_u sg true { s with subst=subst' } lst in + let subst db ar te = pseudo_u sg true { s with subst =SS.add s.subst db ar te } lst in if term_eq t1' t2' then dropped () else match t1', t2' with diff --git a/tests/KO/church.dk b/tests/KO/church.dk index e792bf10..f9ba20ae 100644 --- a/tests/KO/church.dk +++ b/tests/KO/church.dk @@ -29,4 +29,4 @@ P : numeral -> Type. P2: n:numeral -> P n -> Type. y : P 2_13. -z: P2 2_17 y. +z : P2 2_17 y. From 377ce08487a06b2223f91aac3f4c0c5cc2e697bc Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Mon, 16 Dec 2019 15:42:18 +0100 Subject: [PATCH 25/35] Moved SR checking to a separate module. --- kernel/exsubst.ml | 13 ++ kernel/exsubst.mli | 4 + kernel/term.ml | 2 + kernel/term.mli | 3 + kernel/typing.ml | 333 +++++---------------------------------------- 5 files changed, 54 insertions(+), 301 deletions(-) diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index c16b385c..f718cfe1 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -36,6 +36,16 @@ let apply_exsubst (subst:ex_substitution) (n:int) (te:term) : term*bool = | _ -> t in (aux n te, !ct > 0) +let head_apply_exsubst (subst:ex_substitution) (k:int) (te:term) : term*bool = + match te with + | DB (l,x,n) when n >= k -> + ( try ( subst l x n 0 k, true) + with Not_found -> (te,false) ) + | App (DB (l,x,n),a,args) when n >= k -> + ( try ( mk_App (subst l x n (1+(List.length args)) k) a args, true) + with Not_found -> (te,false) ) + | _ -> (te, false) + module IntMap = Map.Make( struct type t = int @@ -62,6 +72,9 @@ struct let apply (sigma:t) : int -> term -> term*bool = if is_identity sigma then (fun _ t -> t,false) else apply_exsubst (subst sigma) + let head_apply (sigma:t) : int -> term -> term*bool = + if is_identity sigma then (fun _ t -> t,false) else head_apply_exsubst (subst sigma) + let add (sigma:t) (n:int) (nargs:int) (t:term) : t = assert ( not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs ); if not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli index 156639cb..2475b2b8 100644 --- a/kernel/exsubst.mli +++ b/kernel/exsubst.mli @@ -53,6 +53,10 @@ sig (** [apply sigma n t] applies the subsitution [sigma] to [t] considered under [n] lambda abstractions. *) + val head_apply : t -> int -> term -> term*bool + (** [head_apply sigma n t] applies the subsitution [sigma] *at the head* of [t] + considered under [n] lambda abstractions. *) + val mk_idempotent : t -> t (** [mk_idempotent sigma] successively applies sigma to its mapped terms until this operation has no effect anymore. *) diff --git a/kernel/term.ml b/kernel/term.ml index 0bc1c80c..6075442b 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -80,6 +80,8 @@ let subterm t i = match t with let subterm = List.fold_left subterm +type cstr = int*term*term + (*********** Contexts} ***********) diff --git a/kernel/term.mli b/kernel/term.mli index 1d725ea3..9490810a 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -40,6 +40,9 @@ val subterm : term -> position -> term (** [subterm t p] returns the subterm of [t] at position [p]. Raises InvalidSubterm in case of invalid position in given term. *) +type cstr = int*term*term +(** Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) + (** {2 Contexts} *) type 'a context = (loc * ident * 'a) list diff --git a/kernel/typing.ml b/kernel/typing.ml index 98f3ffb2..dfe4277c 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -55,6 +55,7 @@ end (* ********************** CONTEXT *) module Make(R:Reduction.S) = struct + module SR = Srcheck.SRChecker(R) let get_type ctx l x n = try let (_,_,ty) = List.nth ctx n in Subst.shift (n+1) ty @@ -67,50 +68,11 @@ struct let (_,_,te) = a in raise (TypingError (ConvertibilityError (te, ctx, mk_Type dloc, ty_a))) - type cstr = int*term*term - (* Constraints [(n,t,u)] are [t]=[u] under [n] lambdas *) - - let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = - let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in - let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in - (term_eq t1' t2' && term_eq u1' u2') || (term_eq t1' u2' && term_eq u1' t2') - - let term_eq_under_cstr (eq_cstr:cstr list) : typ -> typ -> bool = - let rec aux = function - | [] -> true - | (n,t1,t2)::tl -> - List.exists (cstr_eq (n,t1,t2)) eq_cstr || - match t1,t2 with - | App(h1,a1,l1), App(h2,a2,l2) -> - List.length l1 = List.length l2 && - aux ((n,h1,h2)::(n,a1,a2)::(List.map2 (fun x y -> (n,x,y)) l1 l2)@tl) - | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) - | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) - | _ -> term_eq t1 t2 && aux tl - in fun t1 t2 -> eq_cstr <> [] && aux [(0,t1,t2)] - - let rec full_snf sg subst d t = - let t1 = R.snf sg t in - let t2,flag = SS.apply subst d t1 in - if flag then full_snf sg subst d t2 else R.snf sg t2 - - let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (eq_cstr:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = - R.are_convertible sg ty_inf ty_exp || - match SS.is_identity sub, eq_cstr with - | true, [] -> false - | true, _ -> term_eq_under_cstr eq_cstr (R.snf sg ty_inf) (R.snf sg ty_exp) - | false,_ -> - let snf_ty_inf = full_snf sg sub depth ty_inf in - let snf_ty_exp = full_snf sg sub depth ty_exp in - Debug.(debug D_warn) "Test %a ~ %a" pp_term snf_ty_inf pp_term snf_ty_exp; - R.are_convertible sg snf_ty_inf snf_ty_exp || - term_eq_under_cstr eq_cstr snf_ty_inf snf_ty_exp - (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) (* The functions [check'] and [infer'] have an additional argument compared to [check] and [infer] which is a list of additional equalities, which are useful when checking subject reduction *) - let rec infer' sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (te:term) : typ = + let rec infer' sg (c:SR.t) (d:int) (ctx:typed_context) (te:term) : typ = Debug.(debug D_typeChecking "Inferring: %a" pp_term te); match te with | Kind -> raise (TypingError KindIsNotTypable) @@ -118,25 +80,25 @@ struct | DB (l,x,n) -> get_type ctx l x n | Const (l,cst) -> Signature.get_type sg l cst | App (f,a,args) -> - snd (List.fold_left (check_app sg sub addi_eq d ctx) - (f,infer' sg sub addi_eq d ctx f) (a::args)) + snd (List.fold_left (check_app sg c d ctx) + (f,infer' sg c d ctx f) (a::args)) | Pi (l,x,a,b) -> - let ty_a = infer' sg sub addi_eq d ctx a in + let ty_a = infer' sg c d ctx a in let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer' sg sub addi_eq (d+1) ctx2 b in + let ty_b = infer' sg c (d+1) ctx2 b in ( match ty_b with | Kind | Type _ -> ty_b | _ -> raise (TypingError (SortExpected (b, ctx2, ty_b))) ) | Lam (l,x,Some a,b) -> - let ty_a = infer' sg sub addi_eq d ctx a in + let ty_a = infer' sg c d ctx a in let ctx2 = extend_ctx (l,x,a) ctx ty_a in - let ty_b = infer' sg sub addi_eq (d+1) ctx2 b in + let ty_b = infer' sg c (d+1) ctx2 b in ( match ty_b with | Kind -> raise (TypingError (InexpectedKind (b, ctx2))) | _ -> mk_Pi l x a ty_b ) | Lam (l,_,None,_) -> raise (TypingError (DomainFreeLambda l)) - and check' sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (te:term) (ty_exp:typ) : unit = + and check' sg (c:SR.t) (d:int) (ctx:typed_context) (te:term) (ty_exp:typ) : unit = Debug.(debug D_typeChecking "Checking (%a): %a : %a" pp_loc (get_loc te) pp_term te pp_term ty_exp); match te with @@ -146,31 +108,32 @@ struct | Pi (_,_,a,ty_b) -> ( match op with | Some a' -> - ignore(infer' sg sub addi_eq d ctx a'); - if not (convertible_under_cstr sg sub addi_eq d a a') + ignore(infer' sg c d ctx a'); + if not (SR.convertible sg c d a a') then raise (TypingError (ConvertibilityError ((mk_DB l x 0),ctx,a,a'))) | _ -> () ); - check' sg sub addi_eq (d+1) ((l,x,a)::ctx) b ty_b + check' sg c (d+1) ((l,x,a)::ctx) b ty_b | _ -> raise (TypingError (ProductExpected (te,ctx,ty_exp))) end | _ -> - let ty_inf = infer' sg sub addi_eq d ctx te in + let ty_inf = infer' sg c d ctx te in Debug.(debug D_typeChecking "Checking convertibility: %a ~ %a" pp_term ty_inf pp_term ty_exp); - if not (convertible_under_cstr sg sub addi_eq d ty_inf ty_exp) + if not (SR.convertible sg c d ty_inf ty_exp) then let ty_exp' = rename_vars_with_typed_context ctx ty_exp in raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) - and check_app sg (sub:SS.t) (addi_eq:cstr list) (d:int) (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = + + and check_app sg (c:SR.t) (d:int) (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = match R.whnf sg ty_f with | Pi (_,_,a,b) -> - let _ = check' sg sub addi_eq d ctx arg a in + let _ = check' sg c d ctx arg a in (mk_App f arg [], Subst.subst b arg ) | _ -> raise (TypingError ( ProductExpected (f,ctx,ty_f))) - let check sg = check' sg SS.identity [] 0 - let infer sg = infer' sg SS.identity [] 0 + let check sg = check' sg SR.empty 0 + let infer sg = infer' sg SR.empty 0 let inference sg (te:term) : typ = infer sg [] te @@ -178,239 +141,6 @@ struct let _ = infer sg [] ty in check sg [] te ty - (* **** PSEUDO UNIFICATION ********************** *) - - let rec add_to_list q lst args1 args2 = - match args1,args2 with - | [], [] -> lst - | a1::args1, a2::args2 -> add_to_list q ((q,a1,a2)::lst) args1 args2 - | _, _ -> raise (Invalid_argument "add_to_list") - - let safe_add_to_list q lst args1 args2 = - try Some (add_to_list q lst args1 args2) - with Invalid_argument _ -> None - - let unshift_reduce sg q t = - try Some (Subst.unshift q t) - with Subst.UnshiftExn -> - ( try Some (Subst.unshift q (R.snf sg t)) - with Subst.UnshiftExn -> None ) - - (** Under [d] lambdas, checks whether term [te] *must* contain an occurence - of any variable that satisfies the given predicate [p], - *even when substituted or reduced*. - This check make no assumption on the rewrite system or possible substitution - - any definable symbol are "safe" as they may reduce to a term where no variable occur - - any applied meta variable (DB index > [d]) are "safe" as they may be - substituted and reduce to a term where no variable occur - Raises VarSurelyOccurs if the term [te] *surely* contains an occurence of one - of the [vars]. - *) - let sure_occur_check sg (d:int) (p:int -> bool) (te:term) : bool = - let exception VarSurelyOccurs in - let rec aux = function - | [] -> () - | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) - match t with - | Kind | Type _ | Const _ -> aux tl - | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) - | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) - | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) - | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl - | App (f,a,args) -> - begin - match f with - | DB (_,_,n) -> - if n >= k && p (n-k) - then raise VarSurelyOccurs - else if n >= k + d (* a matching variable *) - then aux tl - else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) - | Const (l,cst) when Signature.is_static sg l cst -> - ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) - | _ -> aux tl - (* Default case encompasses: - - Meta variables: DB(_,_,n) with n >= k + d - - Definable symbols - - Lambdas (FIXME: when can this happen ?) - - Illegal applications *) - end - in - try aux [(0,te)]; false - with VarSurelyOccurs -> true - -(** Under [d] lambdas, gather all free variables that are *surely* - contained in term [te]. That is to say term [te] will contain - an occurence of these variables *even when substituted or reduced*. - This check make no assumption on the rewrite system or possible substitutions - - applied definable symbols *surely* contain no variable as they may - reduce to terms where their arguments are erased - - applied meta variable (DB index > [d]) *surely* contain no variable as they - may be substituted and reduce to a term where their arguments are erased - Sets the indices of *surely* contained variables to [true] in the [vars] - boolean array which is expected to be of size (at least) [d]. -*) - let gather_free_vars (d:int) (terms:term list) : bool array = - let vars = Array.make d false in - let rec aux = function - | [] -> () - | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) - match t with - | DB (_,_,n) -> (if n >= k && n < k + d then vars.(n-k) <- true); aux tl - | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) - | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) - | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) - | App (f,a,args) -> aux ((k,f)::(k,a):: (List.map (fun t -> (k,t)) args) @ tl) - | _ -> aux tl - in aux (List.map (fun t -> (0,t)) terms); vars - - type solver = - { - subst : SS.t; - unsolved : cstr list; - unsatisf : cstr list - } - - let try_solve q args t = - try - let dbs = List.map (function DB(_,_,n) -> n | _ -> raise Matching.NotUnifiable) args in - Some (Matching.solve q (LList.of_list dbs) t) - with Matching.NotUnifiable -> None - - let rec full_whnf sg subst d t = - let t1 = R.whnf sg t in - let t2,flag = SS.apply subst d t1 in - if flag then full_whnf sg subst d t2 else R.whnf sg t2 - - let rec pseudo_u sg flag (s:solver) : cstr list -> bool*solver = function - | [] -> (flag, s) - | (q,t1,t2)::lst -> begin - let t1' = full_whnf sg s.subst q t1 in - let t2' = full_whnf sg s.subst q t2 in - let dropped () = pseudo_u sg flag s lst in - let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in - let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in - let subst db ar te = pseudo_u sg true { s with subst =SS.add s.subst db ar te } lst in - if term_eq t1' t2' then dropped () - else - match t1', t2' with - | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) - | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) - | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () - - | Pi (_,_,a,b), Pi (_,_,a',b') -> - pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) - | Lam (_,_,_,b), Lam (_,_,_,b') -> - pseudo_u sg true s ((q+1,b,b')::lst) - - (* Potentially eta-equivalent terms *) - | Lam (_,i,_,b), a when !Reduction.eta -> - let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg true s ((q+1,b,b')::lst) - | a, Lam (_,i,_,b) when !Reduction.eta -> - let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in - pseudo_u sg true s ((q+1,b,b')::lst) - - (* A definable symbol is only be convertible with closed terms *) - | Const (l,cst), t when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() - | t, Const (l,cst) when not (Signature.is_static sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() - - (* X = Y : map either X to Y or Y to X *) - | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> - let (n,t) = if n1=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then unsatisf() - else begin - match unshift_reduce sg q t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() else subst n' 0 t' - end - | t, DB (_,_,n) when n>=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then unsatisf() - else begin - match unshift_reduce sg q t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() else subst n' 0 t' - end - - (* f t1 ... tn / X t1 ... tn = u - 1) Gather all free variables in t1 ... tn - 2) Make sure u only relies on these variables - *) - | App (DB (_,_,n),a,args), t when n >= q -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() - else begin - match try_solve q (a::args) t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsolved() - (* X = t[X] cannot be turned into a (extended-)substitution *) - else subst n' (1+(List.length args)) t' - end - | t, App (DB (_,_,n),a,args) when n >= q -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() - else begin - match try_solve q (a::args) t with - | None -> unsolved() - | Some ut -> - let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsolved() - (* X = t[X] cannot be turned into a (extended-)substitution *) - else subst n' (1+(List.length args)) t' - end - | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() - | t, App (Const (l,cst),a,args) when not (Signature.is_static sg l cst) -> - let occs = gather_free_vars q (a::args) in - if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t - then unsatisf() else unsolved() - - | App (f,a,args), App (f',a',args') -> - (* f = Kind | Type | DB n when n unsatisf() (* Different number of arguments. *) - | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) - end - - | _, _ -> unsatisf() - end - - let solve_cstr (sg : Signature.t) (cstr : cstr list) : solver = - let rec process_solver sol = - match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with - | false, s -> s - | true , sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} - in - process_solver {subst=SS.identity;unsolved=cstr;unsatisf=[]} @@ -581,20 +311,20 @@ struct let rec aux ctx depth ctx1 ctx2 = match ctx1, ctx2 with | (l,x,ty)::ctx1' , (_,_,ty')::ctx2' -> - begin + begin match ty' with | None -> () | Some ty' -> - Debug.(debug D_typeChecking "Checking type annotation (%a): %a ~ %a" - pp_loc l pp_term ty pp_term ty'); + Debug.(debug D_typeChecking "Checking type annotation (%a): %a ~ %a" + pp_loc l pp_term ty pp_term ty'); if not (R.are_convertible sg ty ty') then let ty2 = fst (SS.apply sub 0 (Subst.shift depth ty )) in let ty2' = fst (SS.apply sub 0 (Subst.shift depth ty')) in if not (R.are_convertible sg ty2 ty2') then raise (TypingError (AnnotConvertibilityError (l,x,ctx,ty',ty))) - end; - aux ((l,x,ty)::ctx) (depth+1) ctx1' ctx2' + end; + aux ((l,x,ty)::ctx) (depth+1) ctx1' ctx2' | [], [] -> () | _ -> assert false in aux [] 1 typed_ctx annot_ctx @@ -604,10 +334,11 @@ struct let delta = pc_make rule.ctx in let (ty_le,delta,lst) = infer_pattern sg delta LList.nil [] rule.pat in assert ( delta.padding == 0 ); - let sol = solve_cstr sg lst in - ( match sol.unsatisf with - | [] -> () - | (q,t1,t2)::_ -> + (* Compile a unifier for the generated type checking constraints *) + let unif = SR.compile_cstr sg lst in + ( match SR.get_unsat unif with (* Fetch unsatisfiable conditions... *) + | None -> () + | Some (q,t1,t2)-> (* ...if any warn or fail *) if !fail_on_unsatisfiable_constraints then raise (TypingError (UnsatisfiableConstraints (rule,(q,t1,t2)))) else @@ -617,7 +348,7 @@ struct pp_term t1 pp_term t2 (if q > 0 then Format.sprintf " (under %i abstractions)" q else "") ); - let sub = sol.subst in + let sub = SR.get_subst unif in let ctx = LList.lst delta.pctx in let ctx2 = try subst_context sub ctx @@ -632,8 +363,8 @@ struct end in Debug.(debug D_rule "Typechecking rule"); - let cstr_nf = List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) sol.unsolved in - check' sg sub cstr_nf 0 ctx2 rule.rhs ty_le; + (* Optimize the unifier then use it to check the type of the RHS *) + check' sg (SR.optimize sg unif) 0 ctx2 rule.rhs ty_le; check_type_annotations sg sub ctx2 rule.ctx; Debug.(debug D_rule "Fully checked rule:@.[ %a ] %a --> %a" pp_context_inline ctx pp_pattern rule.pat pp_term rule.rhs); From 22fb8a8724267efa2edfb0484f94e221f3af2905 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Mon, 16 Dec 2019 15:42:24 +0100 Subject: [PATCH 26/35] Moved SR checking to a separate module. --- kernel/srcheck.ml | 300 +++++++++++++++++++++++++++++++++++++++++++++ kernel/srcheck.mli | 14 +++ 2 files changed, 314 insertions(+) create mode 100644 kernel/srcheck.ml create mode 100644 kernel/srcheck.mli diff --git a/kernel/srcheck.ml b/kernel/srcheck.ml new file mode 100644 index 00000000..48eb03b1 --- /dev/null +++ b/kernel/srcheck.ml @@ -0,0 +1,300 @@ +open Basic +open Term + +module SS = Exsubst.ExSubst + +let srfuel = ref 3 + +(* Check whether two pairs of terms are unifiable (one way or the other) *) +let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = + let t1',u1' = Subst.shift n2 t1, Subst.shift n2 u1 in + let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in + (term_eq t1' t2' && term_eq u1' u2') || (term_eq t1' u2' && term_eq u1' t2') + +module SRChecker(R:Reduction.S) : +sig + type t + val empty : t + val get_subst : t -> SS.t + val get_unsat : t -> cstr option + val convertible : Signature.t -> t -> int -> term -> term -> bool + val compile_cstr : Signature.t -> cstr list -> t + val optimize : Signature.t -> t -> t +end = struct + type t = + { + subst : SS.t; + unsolved : cstr list; + unsatisf : cstr list + } + + let empty : t = { subst = SS.identity; unsolved=[]; unsatisf=[] } + + let get_subst c = c.subst + let get_unsat c = match c.unsatisf with [] -> None | c::_ -> Some c + + let snf sg c d = + let rec aux fuel t = + let t1,flag = SS.apply c.subst d t in + let t2 = R.snf sg t1 in + if flag && fuel <> 0 then aux (fuel-1) t2 else t2 in + aux !srfuel + + let whnf sg c d = + let rec aux fuel t = + let t1,flag = SS.apply c.subst d t in + let t2 = R.whnf sg t1 in + if flag && fuel <> 0 then aux (fuel-1) t2 else t2 in + aux !srfuel + + (* Applies *) + let term_eq_under_cstr (eq_cstr:cstr list) : term -> term -> bool = + let rec aux = function + | [] -> true + | (n,t1,t2)::tl -> + List.exists (cstr_eq (n,t1,t2)) eq_cstr || + match t1,t2 with + | App(h1,a1,l1), App(h2,a2,l2) -> + List.length l1 = List.length l2 && + aux ((n,h1,h2)::(n,a1,a2)::(List.map2 (fun x y -> (n,x,y)) l1 l2)@tl) + | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) + | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) + | _ -> term_eq t1 t2 && aux tl + in fun t1 t2 -> eq_cstr <> [] && aux [(0,t1,t2)] + + let convertible (sg:Signature.t) (c:t) (depth:int) (ty_inf:term) (ty_exp:term) : bool = + R.are_convertible sg ty_inf ty_exp || + match SS.is_identity c.subst, c.unsolved with + | true, [] -> false + | true, _ -> term_eq_under_cstr c.unsolved (R.snf sg ty_inf) (R.snf sg ty_exp) + | false,_ -> + let snf_ty_inf = snf sg c depth ty_inf in + let snf_ty_exp = snf sg c depth ty_exp in + R.are_convertible sg snf_ty_inf snf_ty_exp || + term_eq_under_cstr c.unsolved snf_ty_inf snf_ty_exp + + (* **** PSEUDO UNIFICATION ********************** *) + + let rec add_to_list q lst args1 args2 = + match args1,args2 with + | [], [] -> lst + | a1::args1, a2::args2 -> add_to_list q ((q,a1,a2)::lst) args1 args2 + | _, _ -> raise (Invalid_argument "add_to_list") + + let safe_add_to_list q lst args1 args2 = + try Some (add_to_list q lst args1 args2) + with Invalid_argument _ -> None + + let unshift_reduce sg q t = + try Some (Subst.unshift q t) + with Subst.UnshiftExn -> + ( try Some (Subst.unshift q (R.snf sg t)) + with Subst.UnshiftExn -> None ) + + (** Under [d] lambdas, checks whether term [te] *must* contain an occurence + of any variable that satisfies the given predicate [p], + *even when substituted or reduced*. + This check make no assumption on the rewrite system or possible substitution + - any definable symbol are "safe" as they may reduce to a term where no variable occur + - any applied meta variable (DB index > [d]) are "safe" as they may be + substituted and reduce to a term where no variable occur + Raises VarSurelyOccurs if the term [te] *surely* contains an occurence of one + of the [vars]. + *) + let sure_occur_check sg (d:int) (p:int -> bool) (te:term) : bool = + let exception VarSurelyOccurs in + let rec aux = function + | [] -> () + | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) + match t with + | Kind | Type _ | Const _ -> aux tl + | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) + | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) + | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) + | DB (_,_,n) -> if n >= k && p (n-k) then raise VarSurelyOccurs else aux tl + | App (f,a,args) -> + begin + match f with + | DB (_,_,n) -> + if n >= k && p (n-k) + then raise VarSurelyOccurs + else if n >= k + d (* a matching variable *) + then aux tl + else aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) + | Const (l,cst) when Signature.is_static sg l cst -> + ( aux ( (k, a):: (List.map (fun t -> (k,t)) args) @ tl) ) + | _ -> aux tl + (* Default case encompasses: + - Meta variables: DB(_,_,n) with n >= k + d + - Definable symbols + - Lambdas (FIXME: when can this happen ?) + - Illegal applications *) + end + in + try aux [(0,te)]; false + with VarSurelyOccurs -> true + +(** Under [d] lambdas, gather all free variables that are *surely* + contained in term [te]. That is to say term [te] will contain + an occurence of these variables *even when substituted or reduced*. + This check make no assumption on the rewrite system or possible substitutions + - applied definable symbols *surely* contain no variable as they may + reduce to terms where their arguments are erased + - applied meta variable (DB index > [d]) *surely* contain no variable as they + may be substituted and reduce to a term where their arguments are erased + Sets the indices of *surely* contained variables to [true] in the [vars] + boolean array which is expected to be of size (at least) [d]. +*) + let gather_free_vars (d:int) (terms:term list) : bool array = + let vars = Array.make d false in + let rec aux = function + | [] -> () + | (k,t) :: tl -> (* k counts the number of local lambda abstractions *) + match t with + | DB (_,_,n) -> (if n >= k && n < k + d then vars.(n-k) <- true); aux tl + | Pi (_,_, a,b) -> aux ((k,a)::(k+1,b)::tl) + | Lam (_,_,None ,b) -> aux ( (k+1,b)::tl) + | Lam (_,_,Some a,b) -> aux ((k,a)::(k+1,b)::tl) + | App (f,a,args) -> aux ((k,f)::(k,a):: (List.map (fun t -> (k,t)) args) @ tl) + | _ -> aux tl + in aux (List.map (fun t -> (0,t)) terms); vars + + let try_solve q args t = + try + let dbs = List.map (function DB(_,_,n) -> n | _ -> raise Matching.NotUnifiable) args in + Some (Matching.solve q (LList.of_list dbs) t) + with Matching.NotUnifiable -> None + + let rec pseudo_u sg flag (s:t) : cstr list -> bool*t = function + | [] -> (flag, s) + | (q,t1,t2)::lst -> begin + let t1' = whnf sg s q t1 in + let t2' = whnf sg s q t2 in + let dropped () = pseudo_u sg flag s lst in + let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in + let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in + let subst db ar te = pseudo_u sg true { s with subst =SS.add s.subst db ar te } lst in + if term_eq t1' t2' then dropped () + else + match t1', t2' with + | Kind, Kind | Type _, Type _ -> assert false (* Equal terms *) + | DB (_,_,n), DB (_,_,n') when n=n' -> assert false (* Equal terms *) + | _, Kind | Kind, _ |_, Type _ | Type _, _ -> unsatisf () + + | Pi (_,_,a,b), Pi (_,_,a',b') -> + pseudo_u sg true s ((q,a,a')::(q+1,b,b')::lst) + | Lam (_,_,_,b), Lam (_,_,_,b') -> + pseudo_u sg true s ((q+1,b,b')::lst) + + (* Potentially eta-equivalent terms *) + | Lam (_,i,_,b), a when !Reduction.eta -> + let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in + pseudo_u sg true s ((q+1,b,b')::lst) + | a, Lam (_,i,_,b) when !Reduction.eta -> + let b' = mk_App (Subst.shift 1 a) (mk_DB dloc i 0) [] in + pseudo_u sg true s ((q+1,b,b')::lst) + + (* A definable symbol is only be convertible with closed terms *) + | Const (l,cst), t when not (Signature.is_static sg l cst) -> + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() + | t, Const (l,cst) when not (Signature.is_static sg l cst) -> + if sure_occur_check sg q (fun k -> k <= q) t then unsatisf() else unsolved() + + (* X = Y : map either X to Y or Y to X *) + | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> + let (n,t) = if n1=q -> + if sure_occur_check sg q (fun k -> k <= q || k = n) t + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + end + | t, DB (_,_,n) when n>=q -> + if sure_occur_check sg q (fun k -> k <= q || k = n) t + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + end + + (* f t1 ... tn / X t1 ... tn = u + 1) Gather all free variables in t1 ... tn + 2) Make sure u only relies on these variables + *) + | App (DB (_,_,n),a,args), t when n >= q -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsolved() + (* X = t[X] cannot be turned into a (extended-)substitution *) + else subst n' (1+(List.length args)) t' + end + | t, App (DB (_,_,n),a,args) when n >= q -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() + else begin + match try_solve q (a::args) t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + let t' = if Subst.occurs n' ut then ut else R.snf sg ut in + if Subst.occurs n' t' then unsolved() + (* X = t[X] cannot be turned into a (extended-)substitution *) + else subst n' (1+(List.length args)) t' + end + | App (Const (l,cst),a,args), t when not (Signature.is_static sg l cst) -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() + | t, App (Const (l,cst),a,args) when not (Signature.is_static sg l cst) -> + let occs = gather_free_vars q (a::args) in + if sure_occur_check sg q (fun k -> k < q && not occs.(k)) t + then unsatisf() else unsolved() + + | App (f,a,args), App (f',a',args') -> + (* f = Kind | Type | DB n when n unsatisf() (* Different number of arguments. *) + | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) + end + + | _, _ -> unsatisf() + end + + let compile_cstr (sg : Signature.t) (cstr : cstr list) : t = + let rec process_solver sol = + match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with + | false, s -> s + | true , sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} + in + process_solver {subst=SS.identity;unsolved=cstr;unsatisf=[]} + + let optimize sg c = + { c with unsolved=List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) c.unsolved } +end diff --git a/kernel/srcheck.mli b/kernel/srcheck.mli new file mode 100644 index 00000000..f6b36364 --- /dev/null +++ b/kernel/srcheck.mli @@ -0,0 +1,14 @@ +open Term + +val srfuel : int ref + +module SRChecker(R:Reduction.S) : +sig + type t + val empty : t + val get_subst : t -> Exsubst.ExSubst.t + val get_unsat : t -> cstr option + val convertible : Signature.t -> t -> int -> term -> term -> bool + val compile_cstr : Signature.t -> cstr list -> t + val optimize : Signature.t -> t -> t +end From 0635cdc54cbe6e7e5fc6f8c27d30358a54f2c385 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Mon, 16 Dec 2019 16:02:16 +0100 Subject: [PATCH 27/35] Fixed implementation. --- commands/dkcheck.ml | 5 +++++ kernel/srcheck.ml | 18 ++++++++++++------ tests/OK/WIP.dk | 10 ++++++++-- 3 files changed, 25 insertions(+), 8 deletions(-) diff --git a/commands/dkcheck.ml b/commands/dkcheck.ml index e19e62d2..2a4a3dd5 100644 --- a/commands/dkcheck.ml +++ b/commands/dkcheck.ml @@ -92,6 +92,11 @@ let _ = ; ( "--type-lhs" , Arg.Set Typing.fail_on_unsatisfiable_constraints , " Forbids rules with untypable left-hand side" ) + ; ( "--sr-check" + , Arg.Int (fun i -> Srcheck.srfuel := i) + , "LVL Sets the level of subject reduction checking to LVL. + Default value is 3. Values < 0 may not terminate on + rules that do not preserve typing. " ) ; ( "--snf" , Arg.Set Errors.errors_in_snf , " Normalizes all terms printed in error messages" ) diff --git a/kernel/srcheck.ml b/kernel/srcheck.ml index 48eb03b1..ce4baa04 100644 --- a/kernel/srcheck.ml +++ b/kernel/srcheck.ml @@ -212,26 +212,32 @@ end = struct 2) if by chance t already is so, then map X to t 3) otherwise drop the constraint *) | DB (_,_,n), t when n>=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t + if sure_occur_check sg q (fun k -> k < q || k = n) t then unsatisf() else begin match unshift_reduce sg q t with | None -> unsolved() | Some ut -> let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + if Subst.occurs n' ut + then + let t' = R.snf sg ut in + if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + else subst n' 0 ut end | t, DB (_,_,n) when n>=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t + if sure_occur_check sg q (fun k -> k < q || k = n) t then unsatisf() else begin match unshift_reduce sg q t with | None -> unsolved() | Some ut -> let n' = n-q in - let t' = if Subst.occurs n' ut then ut else R.snf sg ut in - if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + if Subst.occurs n' ut + then + let t' = R.snf sg ut in + if Subst.occurs n' t' then unsatisf() else subst n' 0 t' + else subst n' 0 ut end (* f t1 ... tn / X t1 ... tn = u diff --git a/tests/OK/WIP.dk b/tests/OK/WIP.dk index aeb6d214..813d9fc4 100644 --- a/tests/OK/WIP.dk +++ b/tests/OK/WIP.dk @@ -22,7 +22,10 @@ def test1 : f : (A -> A -> A) -> V (x => y => f y x). (; Constraints: x,y |- F x y = c x y - x |- G x = F x ;) + x |- G x = F x +------------------------- + x,y |- flip (G x y) = c y x +;) [F,G] test1 F (x => u (G x)) (x => y => t (c x y)) --> @@ -42,7 +45,10 @@ def test2 : f : (A -> A -> A) -> (; Constraints: |- F = d H x,y |- H x y = c x y - x |- G x = H x ;) + x |- G x = H x +----------------------------- + x,y |- +;) [F,G,H] test2 F (x => u (G x)) (x => y => t (c x y)) (v (d H)) --> From dc4552173bd74318faed468a6c99739fd1515682 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Mon, 16 Dec 2019 16:03:10 +0100 Subject: [PATCH 28/35] Added missing comment in test. --- tests/OK/WIP.dk | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/OK/WIP.dk b/tests/OK/WIP.dk index 813d9fc4..27104282 100644 --- a/tests/OK/WIP.dk +++ b/tests/OK/WIP.dk @@ -47,7 +47,7 @@ def test2 : f : (A -> A -> A) -> x,y |- H x y = c x y x |- G x = H x ----------------------------- - x,y |- + x,y |- flip (e F y x) = G x y ;) [F,G,H] test2 F (x => u (G x)) (x => y => t (c x y)) (v (d H)) From d33ed1a68d57b4a8b0fdddb49b852170b97a9392 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 17 Dec 2019 14:54:27 +0100 Subject: [PATCH 29/35] Added unit testing. --- kernel/exsubst.ml | 13 -------- kernel/exsubst.mli | 4 --- kernel/srcheck.ml | 62 ++++++++++++++++++------------------- kernel/srcheck.mli | 8 ++++- tests/OK/SR_OK_1.dk | 23 ++++++++++++++ tests/OK/SR_OK_2.dk | 59 +++++++++++++++++++++++++++++++++++ tests/OK/SR_OK_3.dk | 39 +++++++++++++++++++++++ tests/OK/SR_OK_4.dk | 75 +++++++++++++++++++++++++++++++++++++++++++++ 8 files changed, 232 insertions(+), 51 deletions(-) create mode 100644 tests/OK/SR_OK_1.dk create mode 100644 tests/OK/SR_OK_2.dk create mode 100644 tests/OK/SR_OK_3.dk create mode 100644 tests/OK/SR_OK_4.dk diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index f718cfe1..c16b385c 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -36,16 +36,6 @@ let apply_exsubst (subst:ex_substitution) (n:int) (te:term) : term*bool = | _ -> t in (aux n te, !ct > 0) -let head_apply_exsubst (subst:ex_substitution) (k:int) (te:term) : term*bool = - match te with - | DB (l,x,n) when n >= k -> - ( try ( subst l x n 0 k, true) - with Not_found -> (te,false) ) - | App (DB (l,x,n),a,args) when n >= k -> - ( try ( mk_App (subst l x n (1+(List.length args)) k) a args, true) - with Not_found -> (te,false) ) - | _ -> (te, false) - module IntMap = Map.Make( struct type t = int @@ -72,9 +62,6 @@ struct let apply (sigma:t) : int -> term -> term*bool = if is_identity sigma then (fun _ t -> t,false) else apply_exsubst (subst sigma) - let head_apply (sigma:t) : int -> term -> term*bool = - if is_identity sigma then (fun _ t -> t,false) else head_apply_exsubst (subst sigma) - let add (sigma:t) (n:int) (nargs:int) (t:term) : t = assert ( not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs ); if not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli index 2475b2b8..156639cb 100644 --- a/kernel/exsubst.mli +++ b/kernel/exsubst.mli @@ -53,10 +53,6 @@ sig (** [apply sigma n t] applies the subsitution [sigma] to [t] considered under [n] lambda abstractions. *) - val head_apply : t -> int -> term -> term*bool - (** [head_apply sigma n t] applies the subsitution [sigma] *at the head* of [t] - considered under [n] lambda abstractions. *) - val mk_idempotent : t -> t (** [mk_idempotent sigma] successively applies sigma to its mapped terms until this operation has no effect anymore. *) diff --git a/kernel/srcheck.ml b/kernel/srcheck.ml index ce4baa04..8ba97d24 100644 --- a/kernel/srcheck.ml +++ b/kernel/srcheck.ml @@ -3,7 +3,7 @@ open Term module SS = Exsubst.ExSubst -let srfuel = ref 3 +let srfuel = ref 1 (* Check whether two pairs of terms are unifiable (one way or the other) *) let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = @@ -11,16 +11,8 @@ let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = let t2',u2' = Subst.shift n1 t2, Subst.shift n1 u2 in (term_eq t1' t2' && term_eq u1' u2') || (term_eq t1' u2' && term_eq u1' t2') -module SRChecker(R:Reduction.S) : -sig - type t - val empty : t - val get_subst : t -> SS.t - val get_unsat : t -> cstr option - val convertible : Signature.t -> t -> int -> term -> term -> bool - val compile_cstr : Signature.t -> cstr list -> t - val optimize : Signature.t -> t -> t -end = struct +module SRChecker(R:Reduction.S) = +struct type t = { subst : SS.t; @@ -47,19 +39,19 @@ end = struct if flag && fuel <> 0 then aux (fuel-1) t2 else t2 in aux !srfuel - (* Applies *) + (* Syntactical match against all unsolved equations *) let term_eq_under_cstr (eq_cstr:cstr list) : term -> term -> bool = let rec aux = function | [] -> true | (n,t1,t2)::tl -> List.exists (cstr_eq (n,t1,t2)) eq_cstr || - match t1,t2 with - | App(h1,a1,l1), App(h2,a2,l2) -> - List.length l1 = List.length l2 && - aux ((n,h1,h2)::(n,a1,a2)::(List.map2 (fun x y -> (n,x,y)) l1 l2)@tl) - | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) - | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) - | _ -> term_eq t1 t2 && aux tl + match t1,t2 with + | App(h1,a1,l1), App(h2,a2,l2) -> + List.length l1 = List.length l2 && + aux ((n,h1,h2)::(n,a1,a2)::(List.map2 (fun x y -> (n,x,y)) l1 l2)@tl) + | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) + | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) + | _ -> term_eq t1 t2 && aux tl in fun t1 t2 -> eq_cstr <> [] && aux [(0,t1,t2)] let convertible (sg:Signature.t) (c:t) (depth:int) (ty_inf:term) (ty_exp:term) : bool = @@ -75,15 +67,11 @@ end = struct (* **** PSEUDO UNIFICATION ********************** *) - let rec add_to_list q lst args1 args2 = - match args1,args2 with - | [], [] -> lst - | a1::args1, a2::args2 -> add_to_list q ((q,a1,a2)::lst) args1 args2 - | _, _ -> raise (Invalid_argument "add_to_list") - let safe_add_to_list q lst args1 args2 = - try Some (add_to_list q lst args1 args2) - with Invalid_argument _ -> None + let rec add_to_list q acc l1 l2 = match l1, l2 with + | [], [] -> Some acc + | h1::t1, h2::t2 -> add_to_list q ((q,h1,h2)::acc) t1 t2 + | _, _ -> None let unshift_reduce sg q t = try Some (Subst.unshift q t) @@ -285,7 +273,7 @@ end = struct (* f = Kind | Type | DB n when n unsatisf() (* Different number of arguments. *) | Some lst2 -> pseudo_u sg true s ((q,f,f')::(q,a,a')::lst2) end @@ -294,13 +282,21 @@ end = struct end let compile_cstr (sg : Signature.t) (cstr : cstr list) : t = - let rec process_solver sol = + (* Successively runs pseudo_u to apply solved constraints to the remaining + unsolved constraints in the hope to deduce more constraints in solved form *) + let rec process_solver fuel sol = match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with - | false, s -> s - | true , sol' -> process_solver {sol' with subst=SS.mk_idempotent sol'.subst} + | false, s -> s (* When pseudo_u did nothing *) + | true , sol' -> + if fuel = 0 then sol' + else process_solver (fuel-1) {sol' with subst=SS.mk_idempotent sol'.subst} in - process_solver {subst=SS.identity;unsolved=cstr;unsatisf=[]} + (* TODO: this function is given some fuel. In practice 1 is enough for all tests. + We should write a test to force a second reentry in the loop. *) + let res = process_solver (!srfuel) {subst=SS.identity;unsolved=cstr;unsatisf=[]} in + res - let optimize sg c = + + let optimize sg c = (* Substitutes are put in SNF *) { c with unsolved=List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) c.unsolved } end diff --git a/kernel/srcheck.mli b/kernel/srcheck.mli index f6b36364..db25b14e 100644 --- a/kernel/srcheck.mli +++ b/kernel/srcheck.mli @@ -5,8 +5,14 @@ val srfuel : int ref module SRChecker(R:Reduction.S) : sig type t - val empty : t + (** Representation of LHS typing constraints *) + + val empty : t + (** No constraints *) + val get_subst : t -> Exsubst.ExSubst.t + (** Retrieve extended substitution *) + val get_unsat : t -> cstr option val convertible : Signature.t -> t -> int -> term -> term -> bool val compile_cstr : Signature.t -> cstr list -> t diff --git a/tests/OK/SR_OK_1.dk b/tests/OK/SR_OK_1.dk new file mode 100644 index 00000000..b4dceb5c --- /dev/null +++ b/tests/OK/SR_OK_1.dk @@ -0,0 +1,23 @@ +(; OK --sr-check 1 ;) + +A : Type. +a : A. + +f : A -> A. +def g : A -> A. +[X] g (g X) --> f X. + +T : A -> Type. +t : a : A -> T a. +k : a : A -> T a -> T (f a). + +(; + f Y = g X + X = g Z +--------------- + Z = Y +;) +def test : X : A -> T X -> T (g X) -> T (g X). +[X,Y,Z] + test X (t (g Z)) (t (f Y)) + --> k Z (t Y). diff --git a/tests/OK/SR_OK_2.dk b/tests/OK/SR_OK_2.dk new file mode 100644 index 00000000..fc8d843a --- /dev/null +++ b/tests/OK/SR_OK_2.dk @@ -0,0 +1,59 @@ +(; OK --sr-check 2 ;) + +A : Type. +a : A. + +def f : A -> A. +def g : A -> A. +[X] f (g X) --> X. + +T : A -> Type. +t : a : A -> T a. +k : a : A -> T a -> T (f a). + +(; + f (f X) = g U + f X = g Z + X = g Y +--------------- + X = g Y + Y = g Z + Z = g U +;) +def test : + X : A -> + T X -> + T (f X) -> + T (f (f X)) -> + T X. + +[X,Y,Z,U] + test X + (t (g Y)) + (t (g Z)) + (t (g U)) + --> t (g (g (g U))). + + +(; + f (f X) = g U + f X = g Z + X = g Y +--------------- + X = g Y + Y = g Z + Z = g U +;) +def test2 : + X : A -> + T X -> + T (f (f X)) -> + T (f X) -> + T X. + +[X,Y,Z,U] + test2 X + (t (g Y)) + (t (g U)) + (t (g Z)) + --> t (g (g (g U))). diff --git a/tests/OK/SR_OK_3.dk b/tests/OK/SR_OK_3.dk new file mode 100644 index 00000000..a919461e --- /dev/null +++ b/tests/OK/SR_OK_3.dk @@ -0,0 +1,39 @@ +(; OK --sr-check 3 ;) + +A : Type. +a : A. + +def f : A -> A. +def g : A -> A. +[X] f (g X) --> X. + +T : A -> Type. +t : a : A -> T a. +k : a : A -> T a -> T (f a). + +(; + f (f (f X)) = g V + f (f X) = g U + f X = g Z + X = g Y +--------------- + X = g Y + Y = g Z + Z = g U + U = g V +;) +def test : + X : A -> + T X -> + T (f (f X)) -> + T (f (f (f X))) -> + T (f X) -> + T X. + +[X,Y,Z,U,V] + test X + (t (g Y)) + (t (g U)) + (t (g V)) + (t (g Z)) + --> t (g (g (g (g V)))). diff --git a/tests/OK/SR_OK_4.dk b/tests/OK/SR_OK_4.dk new file mode 100644 index 00000000..f43ef2bb --- /dev/null +++ b/tests/OK/SR_OK_4.dk @@ -0,0 +1,75 @@ +(; OK --sr-check 4 ;) + +A : Type. +a : A. + +def f : A -> A. +def g : A -> A. +[X] f (g X) --> X. + +T : A -> Type. +t : a : A -> T a. +k : a : A -> T a -> T (f a). + +(; + f (f (f (f X)) = g W + f (f (f X)) = g V + f (f X) = g U + f X = g Z + X = g Y +------------------------- + X = g Y + Y = g Z + Z = g U + U = g V + V = g W +;) +def test : + X : A -> + T X -> + T (f (f X)) -> + T (f (f (f (f X)))) -> + T (f (f (f X))) -> + T (f X) -> + T X. + +[X,Y,Z,U,V,W] + test X + (t (g Y)) + (t (g U)) + (t (g W)) + (t (g V)) + (t (g Z)) + --> t (g (g (g (g (g W))))). + + +(; + f (f (f (f X)) = g W + f (f (f X)) = g V + f (f X) = g U + f X = g Z + X = g Y +------------------------- + X = g Y + Y = g Z + Z = g U + U = g V + V = g W +;) +def test2 : + X : A -> + T X -> + T (f (f (f (f X)))) -> + T (f (f X)) -> + T (f (f (f X))) -> + T (f X) -> + T X. + +[X,Y,Z,U,V,W] + test2 X + (t (g Y)) + (t (g W)) + (t (g U)) + (t (g V)) + (t (g Z)) + --> t (g (g (g (g (g W))))). From 0f55ecaca0e0b9292211f7d5058d0bb77d551375 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 17 Dec 2019 17:11:42 +0100 Subject: [PATCH 30/35] Added SR checking debug messages. --- api/env.ml | 1 + commands/dkcheck.ml | 3 ++- kernel/srcheck.ml | 8 +++++--- kernel/srcheck.mli | 3 +++ kernel/typing.ml | 2 +- 5 files changed, 12 insertions(+), 5 deletions(-) diff --git a/api/env.ml b/api/env.ml index 88084d8b..723b53f3 100644 --- a/api/env.ml +++ b/api/env.ml @@ -15,6 +15,7 @@ let set_debug_mode = | 'c' -> Debug.enable_flag Confluence.D_confluence | 'u' -> Debug.enable_flag Typing.D_rule | 't' -> Debug.enable_flag Typing.D_typeChecking + | 's' -> Debug.enable_flag Srcheck.D_SRChecking | 'r' -> Debug.enable_flag Reduction.D_reduce | 'm' -> Debug.enable_flag Dtree.D_matching | c -> raise (DebugFlagNotRecognized c) diff --git a/commands/dkcheck.ml b/commands/dkcheck.ml index 2a4a3dd5..a4c9d38e 100644 --- a/commands/dkcheck.ml +++ b/commands/dkcheck.ml @@ -60,7 +60,8 @@ let _ = c : (confluence) notifies about information provided to the confluence checker (when option --confluence used) u : (rule) provides information about type checking of rules - t : (typing) provides information about type-checking of terms + t : (typing) provides information about type checking of terms + s : (SR) provides information about subject reduction checking of terms r : (reduce) provides information about reduction performed in terms m : (matching) provides information about pattern matching" ) ; ( "-v" diff --git a/kernel/srcheck.ml b/kernel/srcheck.ml index 8ba97d24..af008c57 100644 --- a/kernel/srcheck.ml +++ b/kernel/srcheck.ml @@ -3,6 +3,9 @@ open Term module SS = Exsubst.ExSubst +type Debug.flag += D_SRChecking +let _ = Debug.register_flag D_SRChecking "SRChecking" + let srfuel = ref 1 (* Check whether two pairs of terms are unifiable (one way or the other) *) @@ -158,6 +161,7 @@ struct | (q,t1,t2)::lst -> begin let t1' = whnf sg s q t1 in let t2' = whnf sg s q t2 in + Debug.(debug D_SRChecking) "Processing: %a = %a" pp_term t1' pp_term t2'; let dropped () = pseudo_u sg flag s lst in let unsolved () = pseudo_u sg flag { s with unsolved=(q,t1',t2')::s.unsolved } lst in let unsatisf () = pseudo_u sg true { s with unsatisf=(q,t1',t2')::s.unsolved } lst in @@ -293,9 +297,7 @@ struct in (* TODO: this function is given some fuel. In practice 1 is enough for all tests. We should write a test to force a second reentry in the loop. *) - let res = process_solver (!srfuel) {subst=SS.identity;unsolved=cstr;unsatisf=[]} in - res - + process_solver (!srfuel) {subst=SS.identity;unsolved=cstr;unsatisf=[]} let optimize sg c = (* Substitutes are put in SNF *) { c with unsolved=List.map (fun (n,t,u) -> (n,R.snf sg t,R.snf sg u)) c.unsolved } diff --git a/kernel/srcheck.mli b/kernel/srcheck.mli index db25b14e..64aa1ebb 100644 --- a/kernel/srcheck.mli +++ b/kernel/srcheck.mli @@ -1,4 +1,7 @@ open Term +open Basic + +type Debug.flag += D_SRChecking val srfuel : int ref diff --git a/kernel/typing.ml b/kernel/typing.ml index dfe4277c..d90cb429 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -362,7 +362,7 @@ struct raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) )) end in - Debug.(debug D_rule "Typechecking rule"); + Debug.(debug D_rule "Typechecking rule %a" pp_rule_name rule.name); (* Optimize the unifier then use it to check the type of the RHS *) check' sg (SR.optimize sg unif) 0 ctx2 rule.rhs ty_le; check_type_annotations sg sub ctx2 rule.ctx; From a95f05ab867d90bed7ca16da658a969093729ae2 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Tue, 17 Dec 2019 17:24:36 +0100 Subject: [PATCH 31/35] Rule-loggin LHS constraint substitution --- kernel/typing.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index d90cb429..c3a6ddc3 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -350,15 +350,15 @@ struct ); let sub = SR.get_subst unif in let ctx = LList.lst delta.pctx in + let ctx_name n = let _,name,_ = List.nth ctx n in name in + Debug.(debug D_rule) "Inferred typing substitution:@.%a" + (SS.pp ctx_name) sub; let ctx2 = try subst_context sub ctx with Subst.UnshiftExn -> (* TODO make Dedukti handle this case *) begin Debug.(debug D_rule) "Failed to infer a typing context for the rule:\n%a" pp_part_typed_rule rule; - let ctx_name n = let _,name,_ = List.nth ctx n in name in - Debug.(debug D_rule) "Tried inferred typing substitution: %a" - (SS.pp ctx_name) sub; raise (TypingError (NotImplementedFeature (get_loc_pat rule.pat) )) end in From 8ab2bb93c45a7d0cfce97edd89405c093db17609 Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Tue, 17 Dec 2019 19:38:41 +0100 Subject: [PATCH 32/35] Do not compute snf if no constraint remains --- kernel/typing.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/kernel/typing.ml b/kernel/typing.ml index 60065703..afa95643 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -87,13 +87,14 @@ struct | Lam(_,_,_,t1), Lam(_,_,_,t2) -> aux ((n+1,t1,t2)::tl) | Pi(_,_,a1,b1), Pi(_,_,a2,b2) -> aux ((n,a1,a2)::(n+1,b1,b2)::tl) | _ -> term_eq t1 t2 && aux tl - in fun t1 t2 -> eq_cstr <> [] && aux [(0,t1,t2)] + in fun t1 t2 -> aux [(0,t1,t2)] let convertible_under_cstr (sg:Signature.t) (sub:SS.t) (eq_cstr:cstr list) (depth:int) (ty_inf:typ) (ty_exp:typ) : bool = let subst_ty_inf = SS.apply sub depth ty_inf in let subst_ty_exp = SS.apply sub depth ty_exp in R.are_convertible sg subst_ty_inf subst_ty_exp || - term_eq_under_cstr eq_cstr (R.snf sg subst_ty_inf) (R.snf sg subst_ty_exp) + eq_cstr <> [] && + term_eq_under_cstr eq_cstr (R.snf sg subst_ty_inf) (R.snf sg subst_ty_exp) (* ********************** TYPE CHECKING/INFERENCE FOR TERMS *) From 3dc8024d637ce4bae585841903a744f502d16736 Mon Sep 17 00:00:00 2001 From: Gaspard Ferey Date: Wed, 18 Dec 2019 08:03:48 +0100 Subject: [PATCH 33/35] Fixed evaluation order bug. --- kernel/exsubst.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index c16b385c..7abd2e02 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -34,7 +34,7 @@ let apply_exsubst (subst:ex_substitution) (n:int) (te:term) : term*bool = let a', b' = aux k a, aux (k+1) b in if !ct = ct' then t else mk_Pi l x a' b' | _ -> t - in (aux n te, !ct > 0) + in let res = aux n te in (res, !ct > 0) module IntMap = Map.Make( struct From b94ba1328d7edc4802e9f958fe67f79b1b2f525c Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Fri, 14 Feb 2020 16:20:24 +0100 Subject: [PATCH 34/35] A few cleaning to improve readibility --- commands/dkcheck.ml | 2 +- kernel/exsubst.ml | 33 +++++++++++++++++++++++++++++++-- kernel/exsubst.mli | 32 ++++++++------------------------ kernel/srcheck.ml | 18 +++++++++--------- kernel/srcheck.mli | 14 +++++++------- kernel/typing.ml | 12 ++++++------ 6 files changed, 62 insertions(+), 49 deletions(-) diff --git a/commands/dkcheck.ml b/commands/dkcheck.ml index a4c9d38e..b7d7cf73 100644 --- a/commands/dkcheck.ml +++ b/commands/dkcheck.ml @@ -96,7 +96,7 @@ let _ = ; ( "--sr-check" , Arg.Int (fun i -> Srcheck.srfuel := i) , "LVL Sets the level of subject reduction checking to LVL. - Default value is 3. Values < 0 may not terminate on + Default value is 1. Values < 0 may not terminate on rules that do not preserve typing. " ) ; ( "--snf" , Arg.Set Errors.errors_in_snf diff --git a/kernel/exsubst.ml b/kernel/exsubst.ml index 7abd2e02..af56c010 100644 --- a/kernel/exsubst.ml +++ b/kernel/exsubst.ml @@ -2,8 +2,18 @@ open Basic open Format open Term +(** An extended substitution is a function mapping + - a variable (location, identifier and DB index) + - applied to a given number of arguments + - under a given number of lambda abstractions + to a term. + A substitution raises Not_found meaning that the variable is not subsituted. *) type ex_substitution = loc -> ident -> int -> int -> int -> term +(** [apply_exsubst subst n t] applies [subst] to [t] under [n] lambda abstractions. + - Variables with DB index [k] < [n] are considered "locally bound" and are never substituted. + - Variables with DB index [k] >= [n] may be substituted if [k-n] is mapped in [sigma] + and if they occur applied to enough arguments (substitution's arity). *) let apply_exsubst (subst:ex_substitution) (n:int) (te:term) : term*bool = let ct = ref 0 in (* aux increments this counter every time a substitution occurs. @@ -49,19 +59,38 @@ struct let identity = IntMap.empty let is_identity = IntMap.is_empty + (** Substitution function corresponding to given ExSubst.t instance [sigma]. + We lookup the table at index: (DB index) [n] - (nb of local binders) [k] + When the variable is under applied it is simply not substituted. + Otherwise we return the reduct is shifted up by (nb of local binders) [k] *) let subst (sigma:t) = fun _ _ n nargs k -> let (arity,t) = IntMap.find (n-k) sigma in if nargs >= arity then Subst.shift k t else raise Not_found + (** Special substitution function corresponding to given ExSubst.t instance [sigma] + "in a smaller context": + Assume [sigma] a substitution in a context Gamma = Gamma' ; Delta with |Delta|=[i]. + Then this function represents the substitution [sigma] in the context Gamma'. + All variables of Delta are ignored and substitutes of the variables of Gamma' + are unshifted. This may therefore raise UnshiftExn in case substitutes of + variables of Gamma' refers to variables of Delta. + *) let subst2 (sigma:t) (i:int) = fun _ _ n nargs k -> let (argmin,t) = IntMap.find (n+i+1-k) sigma in if nargs >= argmin then Subst.shift k (Subst.unshift (i+1) t) else raise Not_found - let apply (sigma:t) : int -> term -> term*bool = + let apply' (sigma:t) : int -> term -> term*bool = if is_identity sigma then (fun _ t -> t,false) else apply_exsubst (subst sigma) + let apply2' (sigma:t) (i:int) : int -> term -> term*bool = + if is_identity sigma then (fun _ t -> t,false) else apply_exsubst (subst2 sigma i) + + let apply = fun sigma i t -> fst (apply' sigma i t) + + let apply2 = fun sigma n i t -> fst (apply2' sigma n i t) + let add (sigma:t) (n:int) (nargs:int) (t:term) : t = assert ( not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs ); if not (IntMap.mem n sigma) || fst (IntMap.find n sigma) > nargs @@ -72,7 +101,7 @@ struct else fun sigma' -> let modified = ref false in let applysigma (n,t) = - let res,flag = apply sigma 0 t in + let res,flag = apply' sigma 0 t in if flag then modified := true; (n,res) in diff --git a/kernel/exsubst.mli b/kernel/exsubst.mli index 156639cb..ac3aa0e4 100644 --- a/kernel/exsubst.mli +++ b/kernel/exsubst.mli @@ -1,19 +1,5 @@ open Term -(** An extended substitution is a function mapping - - a variable (location, identifier and DB index) - - applied to a given number of arguments - - under a given number of lambda abstractions - to a term. - A substitution raises Not_found meaning that the variable is not subsituted. *) -type ex_substitution = Basic.loc -> Basic.ident -> int -> int -> int -> term - -(** [apply_exsubst subst n t] applies [subst] to [t] under [n] lambda abstractions. - - Variables with DB index [k] < [n] are considered "locally bound" and are never substituted. - - Variables with DB index [k] >= [n] may be substituted if [k-n] is mapped in [sigma] - and if they occur applied to enough arguments (substitution's arity). *) -val apply_exsubst : ex_substitution -> int -> term -> term*bool - (** This modules implements extended substitution of DB variables in a term. This is typically used to: 1) infer a "most general" typing substitution from constraints gathered while @@ -33,13 +19,15 @@ sig val add : t -> int -> int -> term -> t (** [add sigma n t] returns the substitution [sigma] with the extra mapping [n] -> [t]. *) - val subst : t -> ex_substitution - (** Substitution function corresponding to given ExSubst.t instance [sigma]. - We lookup the table at index: (DB index) [n] - (nb of local binders) [k] - When the variable is under applied it is simply not substituted. - Otherwise we return the reduct is shifted up by (nb of local binders) [k] *) + val apply : t -> int -> term -> term + (** [apply sigma n t] applies the subsitution [sigma] to [t] considered + under [n] lambda abstractions. *) + + val apply' : t -> int -> term -> term*bool + (** Same as apply, but outputting a boolean [true] if the term is modified + by the substitution. *) - val subst2 : t -> int -> ex_substitution + val apply2 : t -> int -> int -> term -> term (** Special substitution function corresponding to given ExSubst.t instance [sigma] "in a smaller context": Assume [sigma] a substitution in a context Gamma = Gamma' ; Delta with |Delta|=[i]. @@ -49,10 +37,6 @@ sig variables of Gamma' refers to variables of Delta. *) - val apply : t -> int -> term -> term*bool - (** [apply sigma n t] applies the subsitution [sigma] to [t] considered - under [n] lambda abstractions. *) - val mk_idempotent : t -> t (** [mk_idempotent sigma] successively applies sigma to its mapped terms until this operation has no effect anymore. *) diff --git a/kernel/srcheck.ml b/kernel/srcheck.ml index ee4822ce..a7257a77 100644 --- a/kernel/srcheck.ml +++ b/kernel/srcheck.ml @@ -16,28 +16,28 @@ let cstr_eq ((n1,t1,u1):cstr) ((n2,t2,u2):cstr) = module SRChecker(R:Reduction.S) = struct - type t = + type lhs_typing_cstr = { subst : SS.t; unsolved : cstr list; unsatisf : cstr list } - let empty : t = { subst = SS.identity; unsolved=[]; unsatisf=[] } + let empty : lhs_typing_cstr = { subst = SS.identity; unsolved=[]; unsatisf=[] } let get_subst c = c.subst let get_unsat c = match c.unsatisf with [] -> None | c::_ -> Some c - let snf sg c d = + let snf sg c depth = let rec aux fuel t = - let t1,flag = SS.apply c.subst d t in + let t1,flag = SS.apply' c.subst depth t in let t2 = R.snf sg t1 in if flag && fuel <> 0 then aux (fuel-1) t2 else t2 in aux !srfuel - let whnf sg c d = + let whnf sg c depth = let rec aux fuel t = - let t1,flag = SS.apply c.subst d t in + let t1,flag = SS.apply' c.subst depth t in let t2 = R.whnf sg t1 in if flag && fuel <> 0 then aux (fuel-1) t2 else t2 in aux !srfuel @@ -57,7 +57,7 @@ struct | _ -> term_eq t1 t2 && aux tl in fun t1 t2 -> aux [(0,t1,t2)] - let convertible (sg:Signature.t) (c:t) (depth:int) (ty_inf:term) (ty_exp:term) : bool = + let convertible (sg:Signature.t) (c:lhs_typing_cstr) (depth:int) (ty_inf:term) (ty_exp:term) : bool = R.are_convertible sg ty_inf ty_exp || match SS.is_identity c.subst, c.unsolved with | true, [] -> false @@ -156,7 +156,7 @@ struct Some (Matching.solve q (LList.of_list dbs) t) with Matching.NotUnifiable -> None - let rec pseudo_u sg flag (s:t) : cstr list -> bool*t = function + let rec pseudo_u sg flag (s:lhs_typing_cstr) : cstr list -> bool*lhs_typing_cstr = function | [] -> (flag, s) | (q,t1,t2)::lst -> begin let t1' = whnf sg s q t1 in @@ -285,7 +285,7 @@ struct | _, _ -> unsatisf() end - let compile_cstr (sg : Signature.t) (cstr : cstr list) : t = + let compile_cstr (sg : Signature.t) (cstr : cstr list) : lhs_typing_cstr = (* Successively runs pseudo_u to apply solved constraints to the remaining unsolved constraints in the hope to deduce more constraints in solved form *) let rec process_solver fuel sol = diff --git a/kernel/srcheck.mli b/kernel/srcheck.mli index 64aa1ebb..0f01deea 100644 --- a/kernel/srcheck.mli +++ b/kernel/srcheck.mli @@ -7,17 +7,17 @@ val srfuel : int ref module SRChecker(R:Reduction.S) : sig - type t + type lhs_typing_cstr (** Representation of LHS typing constraints *) - val empty : t + val empty : lhs_typing_cstr (** No constraints *) - val get_subst : t -> Exsubst.ExSubst.t + val get_subst : lhs_typing_cstr -> Exsubst.ExSubst.t (** Retrieve extended substitution *) - val get_unsat : t -> cstr option - val convertible : Signature.t -> t -> int -> term -> term -> bool - val compile_cstr : Signature.t -> cstr list -> t - val optimize : Signature.t -> t -> t + val get_unsat : lhs_typing_cstr -> cstr option + val convertible : Signature.t -> lhs_typing_cstr -> int -> term -> term -> bool + val compile_cstr : Signature.t -> cstr list -> lhs_typing_cstr + val optimize : Signature.t -> lhs_typing_cstr -> lhs_typing_cstr end diff --git a/kernel/typing.ml b/kernel/typing.ml index c3a6ddc3..6456b570 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -72,7 +72,7 @@ struct (* The functions [check'] and [infer'] have an additional argument compared to [check] and [infer] which is a list of additional equalities, which are useful when checking subject reduction *) - let rec infer' sg (c:SR.t) (d:int) (ctx:typed_context) (te:term) : typ = + let rec infer' sg (c:SR.lhs_typing_cstr) (d:int) (ctx:typed_context) (te:term) : typ = Debug.(debug D_typeChecking "Inferring: %a" pp_term te); match te with | Kind -> raise (TypingError KindIsNotTypable) @@ -98,7 +98,7 @@ struct | _ -> mk_Pi l x a ty_b ) | Lam (l,_,None,_) -> raise (TypingError (DomainFreeLambda l)) - and check' sg (c:SR.t) (d:int) (ctx:typed_context) (te:term) (ty_exp:typ) : unit = + and check' sg (c:SR.lhs_typing_cstr) (d:int) (ctx:typed_context) (te:term) (ty_exp:typ) : unit = Debug.(debug D_typeChecking "Checking (%a): %a : %a" pp_loc (get_loc te) pp_term te pp_term ty_exp); match te with @@ -125,7 +125,7 @@ struct let ty_exp' = rename_vars_with_typed_context ctx ty_exp in raise (TypingError (ConvertibilityError (te,ctx,ty_exp',ty_inf))) - and check_app sg (c:SR.t) (d:int) (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = + and check_app sg (c:SR.lhs_typing_cstr) (d:int) (ctx:typed_context) (f,ty_f:term*typ) (arg:term) : term*typ = match R.whnf sg ty_f with | Pi (_,_,a,b) -> let _ = check' sg c d ctx arg a in @@ -303,7 +303,7 @@ struct let subst_context (sub:SS.t) (ctx:typed_context) : typed_context = if SS.is_identity sub then ctx else - let apply_subst i (l,x,ty) = (l,x,fst (Exsubst.apply_exsubst (SS.subst2 sub i) 0 ty)) in + let apply_subst i (l,x,ty) = (l,x,SS.apply2 sub i 0 ty) in List.mapi apply_subst ctx let check_type_annotations sg sub typed_ctx annot_ctx = @@ -319,8 +319,8 @@ struct pp_loc l pp_term ty pp_term ty'); if not (R.are_convertible sg ty ty') then - let ty2 = fst (SS.apply sub 0 (Subst.shift depth ty )) in - let ty2' = fst (SS.apply sub 0 (Subst.shift depth ty')) in + let ty2 = SS.apply sub 0 (Subst.shift depth ty ) in + let ty2' = SS.apply sub 0 (Subst.shift depth ty') in if not (R.are_convertible sg ty2 ty2') then raise (TypingError (AnnotConvertibilityError (l,x,ctx,ty',ty))) end; From 5cf335194fc4f1f810d8fed5e5775cfbd14d8025 Mon Sep 17 00:00:00 2001 From: Guillaume GENESTIER Date: Fri, 14 Feb 2020 17:19:24 +0100 Subject: [PATCH 35/35] Doc --- kernel/srcheck.mli | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/kernel/srcheck.mli b/kernel/srcheck.mli index 8f27e24f..8f20dd76 100644 --- a/kernel/srcheck.mli +++ b/kernel/srcheck.mli @@ -4,6 +4,9 @@ open Basic val d_SR : Debug.flag val srfuel : int ref +(** This parameters indicates how much time, substitution followed by reduction + is applied on the type of the rhs of a rule to check that the rule preserves + typing. *) module SRChecker(R:Reduction.S) : sig @@ -17,7 +20,18 @@ sig (** Retrieve extended substitution *) val get_unsat : lhs_typing_cstr -> cstr option + (** If no instance of the LHS is typable, + output a witness that the rule cannot be triggered *) + val convertible : Signature.t -> lhs_typing_cstr -> int -> term -> term -> bool + (** [convertible sg c depth t u] is true if the constraints [c] ensures that + [t] and [u], considered both under [depth] abstractions, are convertible *) + val compile_cstr : Signature.t -> cstr list -> lhs_typing_cstr + (** Transforms a list of constraints (ie equality between terms under abstractions), + to a [lhs_typing_cstr]. *) + val optimize : Signature.t -> lhs_typing_cstr -> lhs_typing_cstr + (** Equality inferred while assuming that the LHS is well-typed are put + in normal form. *) end