Extending the type preservation check

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;

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. *)
 

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 "%[email protected] 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

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" )

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

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