diff --git a/kernel/typing.ml b/kernel/typing.ml index 111c2b47..f3c49817 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -1,3 +1,4 @@ + open Basic open Format open Rule @@ -150,45 +151,52 @@ let unshift_reduce sg q t = ( try Some (Subst.unshift q (R.snf sg t)) with Subst.UnshiftExn -> None ) -let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) list -> SS.t = function - | [] -> sigma +type unif = (int*term*term) list + +let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) + (acc:unif) : unif -> SS.t * unif = function + | [] -> sigma, acc | (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 keepon_with acc = pseudo_u sg fail sigma lst acc in + let keepon () = keepon_with acc in + if term_eq t1' t2' then keepon_with acc else - let warn () = fail (q,t1,t2); keepon () in + let register () = keepon_with ((q,t1',t2')::acc) in + let warn () = fail (q,t1,t2); register() 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 () | Pi (_,_,a,b), Pi (_,_,a',b') -> - pseudo_u sg fail sigma ((q,a,a')::(q+1,b,b')::lst) + pseudo_u sg fail sigma ((q,a,a')::(q+1,b,b')::lst) acc | Lam (_,_,_,b), Lam (_,_,_,b') -> - pseudo_u sg fail sigma ((q+1,b,b')::lst) + pseudo_u sg fail sigma ((q+1,b,b')::lst) acc (* 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 fail sigma ((q+1,b,b')::lst) acc | 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 fail sigma ((q+1,b,b')::lst) acc | Const (_,c), Const (_,c') when name_eq c c' -> keepon () | Const (l,cst), t when not (Signature.is_static sg l cst) -> - ( match unshift_reduce sg q t with None -> warn () | Some _ -> keepon ()) + ( match unshift_reduce sg q t with None -> warn () + | Some t -> keepon_with ((0,t1',t)::acc)) | t, Const (l,cst) when not (Signature.is_static sg l cst) -> - ( match unshift_reduce sg q t with None -> warn () | Some _ -> keepon ()) + ( match unshift_reduce sg q t with None -> warn () + | Some t -> keepon_with ((0,t,t2')::acc)) | DB (l1,x1,n1), DB (l2,x2,n2) when n1>=q && n2>=q -> let (n,t) = if n1=q -> begin let n' = n-q in @@ -197,7 +205,7 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) | 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 + else pseudo_u sg fail (SS.add sigma n' t') lst acc end | t, DB (_,_,n) when n>=q -> begin @@ -207,7 +215,7 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) | 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 + else pseudo_u sg fail (SS.add sigma n' t') lst acc end | App (DB (_,_,n),_,_), _ when n >= q -> @@ -215,8 +223,8 @@ let rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) | _ , App (DB (_,_,n),_,_) when n >= q -> if R.are_convertible sg t1' t2' then keepon () else warn () - | 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 () + | App (Const (l,cst),_,_), _ when not (Signature.is_static sg l cst) -> register () + | _, App (Const (l,cst),_,_) when not (Signature.is_static sg l cst) -> register () | App (f,a,args), App (f',a',args') -> (* f = Kind | Type | DB n when n unit) (sigma:SS.t) : (int*term*term) begin match safe_add_to_list q lst args args' with | None -> warn () (* Different number of arguments. *) - | Some lst2 -> pseudo_u sg fail sigma ((q,f,f')::(q,a,a')::lst2) + | Some lst2 -> pseudo_u sg fail sigma ((q,f,f')::(q,a,a')::lst2) acc end | _, _ -> warn () 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).