diff --git a/api/env.ml b/api/env.ml index 0e7fa4c3..8e287675 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_SR | 'r' -> Debug.enable_flag Reduction.d_reduce | 'm' -> Debug.enable_flag Matching.d_matching | c -> raise (DebugFlagNotRecognized c) @@ -65,7 +66,7 @@ sig val define : loc -> ident -> Signature.scope -> bool -> term -> term option -> unit val add_rules : Rule.partially_typed_rule list -> - (Subst.Subst.t * Rule.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 @@ -193,7 +194,7 @@ struct try _define lc id scope 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 34a2909e..875f5c9d 100644 --- a/api/env.mli +++ b/api/env.mli @@ -88,7 +88,7 @@ sig val define : loc -> ident -> Signature.scope -> bool -> term -> term option -> unit (** [define l id scope body ty] defines 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 58c5c434..7b6ae3d6 100644 --- a/api/processor.ml +++ b/api/processor.ml @@ -34,7 +34,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/commands/dkcheck.ml b/commands/dkcheck.ml index 4b91bc77..fdf9e057 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" @@ -92,6 +93,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 1. 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/exsubst.ml b/kernel/exsubst.ml new file mode 100644 index 00000000..af56c010 --- /dev/null +++ b/kernel/exsubst.ml @@ -0,0 +1,119 @@ +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. + * 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) 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; + 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 + 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 let res = aux n te in (res, !ct > 0) + +module IntMap = Map.Make( + struct + type t = int + let compare = compare + end) + +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 + + (** 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 = + 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 + 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 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 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 new file mode 100644 index 00000000..ac3aa0e4 --- /dev/null +++ b/kernel/exsubst.mli @@ -0,0 +1,46 @@ +open 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 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 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]. + 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 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 diff --git a/kernel/srcheck.ml b/kernel/srcheck.ml new file mode 100644 index 00000000..ee6be16e --- /dev/null +++ b/kernel/srcheck.ml @@ -0,0 +1,303 @@ +open Basic +open Term + +module SS = Exsubst.ExSubst + +let d_SR = Debug.register_flag "SR Checking" + +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) = + 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) = +struct + type lhs_typing_cstr = + { + subst : SS.t; + unsolved : cstr list; + unsatisf : cstr list + } + + 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 depth = + let rec aux fuel t = + 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 depth = + let rec aux fuel t = + 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 + + (* 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 + in fun t1 t2 -> aux [(0,t1,t2)] + + 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 + | 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 || + (c.unsolved <> [] && term_eq_under_cstr c.unsolved snf_ty_inf snf_ty_exp) + + (* **** PSEUDO UNIFICATION ********************** *) + + + 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) + 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_injective 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: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 + let t2' = whnf sg s q t2 in + Debug.(debug d_SR) "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 + 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_injective 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_injective 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 + 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 + then unsatisf() + else begin + match unshift_reduce sg q t with + | None -> unsolved() + | Some ut -> + let n' = n-q in + 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 + 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_injective 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_injective 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) : 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 = + match pseudo_u sg false { sol with unsolved = [] } sol.unsolved with + | 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 + (* 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. *) + 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 } +end diff --git a/kernel/srcheck.mli b/kernel/srcheck.mli new file mode 100644 index 00000000..8f20dd76 --- /dev/null +++ b/kernel/srcheck.mli @@ -0,0 +1,37 @@ +open Term +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 + type lhs_typing_cstr + (** Representation of LHS typing constraints *) + + val empty : lhs_typing_cstr + (** No constraints *) + + val get_subst : lhs_typing_cstr -> Exsubst.ExSubst.t + (** 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 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 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 a1e31bc0..0c47962a 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 let d_typeChecking = Debug.register_flag "TypeChecking" let d_rule = Debug.register_flag "Rule" @@ -54,6 +54,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 @@ -63,12 +64,14 @@ struct | Type _ -> a::ctx | Kind when !coc -> a::ctx | ty_a -> - let (_,_,te) = a in - raise (Typing_error (ConvertibilityError (te, ctx, mk_Type dloc, ty_a))) + let (_,_,te) = a in + raise (Typing_error (ConvertibilityError (te, ctx, mk_Type dloc, ty_a))) (* ********************** 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 to [check] and [infer] + which is a list of additional equalities, which are useful when checking subject reduction *) + 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 (Typing_error KindIsNotTypable) @@ -76,24 +79,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 ctx) (f,infer sg 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 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 (Typing_error (SortExpected (b, ctx2, ty_b))) ) + 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 c (d+1) ctx2 b in + ( match ty_b with + | Kind | Type _ -> ty_b + | _ -> raise (Typing_error (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 (Typing_error (InexpectedKind (b, ctx2))) - | _ -> mk_Pi l x a ty_b ) + 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 c (d+1) ctx2 b in + ( match ty_b with + | Kind -> raise (Typing_error (InexpectedKind (b, ctx2))) + | _ -> mk_Pi l x a ty_b ) | Lam (l,_,None,_) -> raise (Typing_error (DomainFreeLambda l)) - and check sg (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 @@ -103,257 +107,77 @@ struct | Pi (_,_,a,ty_b) -> ( match op with | Some a' -> - ignore(infer sg ctx a'); - if not (R.are_convertible sg a a') + ignore (infer' sg c d ctx a'); + if not (SR.convertible sg c d a a') then raise (Typing_error (ConvertibilityError ((mk_DB l x 0),ctx,a,a'))) | _ -> () ); - check sg ((l,x,a)::ctx) b ty_b + check' sg c (d+1) ((l,x,a)::ctx) b ty_b | _ -> raise (Typing_error (ProductExpected (te,ctx,ty_exp))) end | _ -> - let ty_inf = infer sg 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 (R.are_convertible sg ty_inf ty_exp) then + 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 (Typing_error (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 (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 ctx arg a in (mk_App f arg [], Subst.subst b arg ) + let _ = check' sg c d ctx arg a in + (mk_App f arg [], Subst.subst b arg ) | _ -> raise (Typing_error ( ProductExpected (f,ctx,ty_f))) + 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 let checking sg (te:term) (ty:term) : unit = 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) 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_injective 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 rec pseudo_u sg (fail: int*term*term-> unit) (sigma:SS.t) : (int*term*term) list -> SS.t = function - | [] -> sigma - | (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 () - 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 () - - | Pi (_,_,a,b), Pi (_,_,a',b') -> - pseudo_u sg fail sigma ((q,a,a')::(q+1,b,b')::lst) - | Lam (_,_,_,b), Lam (_,_,_,b') -> - pseudo_u sg fail sigma ((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) - | 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) - - (* A definable symbol is only be convertible with closed terms *) - | Const (l,cst), t when not (Signature.is_injective sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then warn() else keepon() - | t, Const (l,cst) when not (Signature.is_injective sg l cst) -> - if sure_occur_check sg q (fun k -> k <= q) t then warn() else keepon() - - (* 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 warn() - else begin - match unshift_reduce sg q t with - | None -> keepon() - | 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 - end - | t, DB (_,_,n) when n>=q -> - if sure_occur_check sg q (fun k -> k <= q || k = n) t - then warn() - else begin - match unshift_reduce sg q t with - | None -> keepon() - | 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 - 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 warn() else keepon() - | 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() - | App (Const (l,cst),a,args), t when not (Signature.is_injective 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() - | t, App (Const (l,cst),a,args) when not (Signature.is_injective 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() - - | 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) - end - - | _, _ -> warn () - end - (* **** 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 @@ -364,181 +188,188 @@ 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 (Typing_error (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 (Typing_error (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 (Typing_error ( ProductExpected (pattern_to_term pat,ctx (),exp_ty))) - end - | Brackets te -> - let _ = - try Subst.unshift (LList.len sigma) te - with Subst.UnshiftExn -> raise (Typing_error (BracketExprBoundVar (te,ctx()))) - in - let exp_ty2 = - try unshift_n sg (LList.len sigma) exp_ty - with Subst.UnshiftExn -> - raise (Typing_error (BracketExpectedTypeBoundVar (te,ctx(),exp_ty))) - in - let _ = - try unshift_n sg delta.padding exp_ty2 - with Subst.UnshiftExn -> - raise (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error ( ProductExpected (pattern_to_term pat,ctx (),exp_ty))) + end + | Brackets te -> + let _ = + try Subst.unshift (LList.len sigma) te + with Subst.UnshiftExn -> raise (Typing_error (BracketExprBoundVar (te,ctx()))) + in + let exp_ty2 = + try unshift_n sg (LList.len sigma) exp_ty + with Subst.UnshiftExn -> + raise (Typing_error (BracketExpectedTypeBoundVar (te,ctx(),exp_ty))) + in + let _ = + try unshift_n sg delta.padding exp_ty2 + with Subst.UnshiftExn -> + raise (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error (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 (Typing_error (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,Subst.apply_subst (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 (Typing_error (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 fail = if !fail_on_unsatisfiable_constraints - then (fun x -> raise (Typing_error (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 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 - 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 (Typing_error (NotImplementedFeature (get_loc_pat rule.pat) ) ) - 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 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,SS.apply2 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 (Typing_error (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 ); + (* 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 (Typing_error (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 = 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; + raise (Typing_error (NotImplementedFeature (get_loc_pat rule.pat) )) + end + in + 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; + Debug.(debug d_rule "Fully checked rule:@.[ %a ] %a --> %a" + pp_context_inline ctx pp_pattern rule.pat pp_term rule.rhs); + sub, + { name = rule.name; + ctx = ctx2; + pat = rule.pat; + rhs = rule.rhs + } end diff --git a/kernel/typing.mli b/kernel/typing.mli index 1e9cf38d..eabcd1d6 100644 --- a/kernel/typing.mli +++ b/kernel/typing.mli @@ -55,7 +55,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 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/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. 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. 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))))). diff --git a/tests/OK/SR_sat.dk b/tests/OK/SR_sat_bv1.dk similarity index 99% rename from tests/OK/SR_sat.dk rename to tests/OK/SR_sat_bv1.dk index 976659cd..f637ec9b 100644 --- a/tests/OK/SR_sat.dk +++ b/tests/OK/SR_sat_bv1.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. diff --git a/tests/OK/SR_sat_bv2.dk b/tests/OK/SR_sat_bv2.dk new file mode 100644 index 00000000..9b40984d --- /dev/null +++ b/tests/OK/SR_sat_bv2.dk @@ -0,0 +1,77 @@ +(; OK --type-lhs ;) + +A : Type. +T : A -> Type. +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 + 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 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 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=>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 + 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..d87d24d9 --- /dev/null +++ b/tests/OK/SR_sat_eq2.dk @@ -0,0 +1,32 @@ +(; OK --type-lhs ;) + +A : Type. +a : A. +c : A -> A -> A. + +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 test0': x : A -> T (c (f x) a) -> T (f (f x)). +[X,Y] test0' X (t (c Y a)) --> t (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 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 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))). diff --git a/tests/OK/WIP.dk b/tests/OK/WIP.dk new file mode 100644 index 00000000..27104282 --- /dev/null +++ b/tests/OK/WIP.dk @@ -0,0 +1,55 @@ +(; 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 +------------------------- + x,y |- flip (G x y) = c y 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 +----------------------------- + 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)) + --> + v (x => y => G x y). diff --git a/tests/OK/first_order_cstr1.dk b/tests/OK/first_order_cstr1.dk new file mode 100644 index 00000000..c89c6556 --- /dev/null +++ b/tests/OK/first_order_cstr1.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. diff --git a/tests/OK/higher_order_cstr1.dk b/tests/OK/higher_order_cstr1.dk new file mode 100644 index 00000000..bfd06b24 --- /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:N => 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: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). 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/higher_order_cstr3.dk b/tests/OK/higher_order_cstr3.dk new file mode 100644 index 00000000..c1626e26 --- /dev/null +++ b/tests/OK/higher_order_cstr3.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) --> 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) --> 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 (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 (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 (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 (z=>x z) y (z => t z) (z => t (x 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) --> 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) --> 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 (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 (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 (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 (z=>x z) y (z => t (x z)) (z => t z) --> t b.