Implementation of an algorithm for checking subject reduction

src/basics.ml

@@ -112,6 +112,13 @@ let is_symb : sym -> term -> bool = fun s t ->
   | Symb(r,_) -> r == s
   | _         -> false
 
+(** [get_symb t] returns [Some s] if [t] is of the form [Symb (s , _)].
+    Otherwise, it returns [None]. *)
+let get_symb : term -> sym option = fun t ->
+  match unfold t with
+  | Symb (s, _) -> Some s
+  | _           -> None
+
 (** [iter_ctxt f t] applies the function [f] to every node of the term [t].
    At each call, the function is given the list of the free variables in the
    term, in the reverse order they were given. Free variables that were
@@ -201,6 +208,103 @@ let has_metas : term -> bool =
   let exception Found in fun t ->
   try iter_meta (fun _ -> raise Found) t; false with Found -> true
 
+(** [build_meta_type k] builds the type “∀(x₁:A₁) (x₂:A₂) ⋯ (xk:Ak), B” where
+    “x₁” through “xk” are fresh variables, “Ai = Mi[x₁,⋯,x(i-1)]”, “Mi” is a
+    new metavar of arity “i-1” and type “∀(x₁:A₂) ⋯ (x(i-1):A(i-1), TYPE”. *)
+let build_meta_type : int -> term = fun k ->
+  assert (k>=0);
+  let vs = Bindlib.new_mvar mkfree (Array.make k "x") in
+  let rec build_prod k p =
+    if k = 0 then p
+    else
+      let k = k-1 in
+      let mk_typ = Bindlib.unbox (build_prod k _Type) in
+      let mk = fresh_meta mk_typ k in
+      let tk = _Meta mk (Array.map _Vari (Array.sub vs 0 k)) in
+      let b = Bindlib.bind_var vs.(k) p in
+      let p = Bindlib.box_apply2 (fun a b -> Prod(a,b)) tk b in
+      build_prod k p
+  in
+  let mk_typ = Bindlib.unbox (build_prod k _Type) (*FIXME?*) in
+  let mk = fresh_meta mk_typ k in
+  let tk = _Meta mk (Array.map _Vari vs) in
+  Bindlib.unbox (build_prod k tk)
+
+(** [new_symb name t] returns a new function symbol of name [name] and of
+    type [t]. *)
+let new_symb name t =
+  { sym_name = name ; sym_type = ref t ; sym_path = [] ; sym_def = ref None
+  ; sym_impl = [] ; sym_rules = ref [] ; sym_mode = Const }
+
+(** [to_m k metas t] computes a new (boxed) term by replacing every pattern
+    variable in [t] by a fresh metavariable and store the latter in [metas],
+    where [k] indicates the order of the term obtained *)
+let rec to_m : int -> (meta option) array -> term -> tbox = fun k metas t ->
+  match unfold t with
+  | Vari x         -> _Vari x
+  | Symb (s, h)    -> _Symb s h
+  | Abst (a, t)    ->
+      let (x, t) = Bindlib.unbind t in
+      _Abst (to_m 0 metas a) (Bindlib.bind_var x (to_m 0 metas t))
+  | Appl (t, u)    -> _Appl (to_m (k + 1) metas t) (to_m 0 metas u)
+  | Patt (i, n, a) ->
+      begin
+        let a = Array.map (to_m 0 metas) a in
+        let l = Array.length a in
+        match i with
+        | None   ->
+            let m = fresh_meta ~name:n (build_meta_type (l + k)) l in
+            _Meta m a
+        | Some i ->
+            match metas.(i) with
+            | Some m -> _Meta m a
+            | None   ->
+                let m = fresh_meta ~name:n (build_meta_type (l + k)) l in
+                metas.(i) <- Some m;
+                _Meta m a
+      end
+  | _              -> assert false
+
+exception Not_FO
+
+(** [to_closed symbs t] computes a new (boxed) term by replacing every
+    pattern variable in [t] by a fresh symbol [c_n] of type [t_n] ([t_n] is
+    another fresh symbol of type [Kind]) and store [c_n] the latter in
+    [symbs]. *)
+let rec to_closed : (sym option) array -> term -> tbox
+  = fun symbs t ->
+  match unfold t with
+  | Vari x            -> _Vari x
+  | Symb (s, h)       -> _Symb s h
+  | Abst (a, t)       ->
+      let (x, t) = Bindlib.unbind t in
+      _Abst (to_closed symbs a) (Bindlib.bind_var x (to_closed symbs t))
+  | Appl (t, u)       -> _Appl (to_closed symbs t) (to_closed symbs u)
+  | Patt (i, n, [||]) ->
+      begin
+        match i with
+        | None   ->
+            let t_n = new_symb ("{t_" ^ n) Kind in
+            let term_t_n = symb t_n in
+            let c_n = new_symb ("{c_" ^ n) term_t_n in
+            _Symb c_n Nothing
+        | Some i ->
+            match symbs.(i) with
+            | Some s -> _Symb s Nothing
+            | None   ->
+                let t_n = new_symb ("{t_" ^ n) Kind in
+                let term_t_n = symb t_n in
+                let c_n = new_symb ("{c_" ^ n) term_t_n in
+                symbs.(i) <- Some c_n;
+                _Symb c_n Nothing
+      end
+  | Patt _            -> raise Not_FO
+  | _                 -> assert false
+
+(** [is_new_symb s] checks if [s] is a function symbol created for checking
+    SR. *)
+let is_new_symb s = s.sym_name.[0] = '{'
+
 (** [distinct_vars_opt ts] checks that [ts] is made of distinct
    variables and returns these variables. *)
 let distinct_vars_opt : term array -> tvar array option =
@@ -239,3 +343,52 @@ let term_of_rhs : rule -> term = fun r ->
     TE_Some(Bindlib.unbox (Bindlib.bind_mvar vars p))
   in
   Bindlib.msubst r.rhs (Array.mapi fn r.vars)
+
+(** [to_terms r] translates the rule [r] into a pair of terms. The pattern
+    variables in the LHS are replaced by metavariables and the terms with
+    environment in the RHS are replaced by their corresponding metavariables.
+    *)
+let to_terms : sym * rule -> term * term = fun (s, r) ->
+  let arity = Bindlib.mbinder_arity r.rhs in
+  let metas = Array.init arity (fun _ -> None) in
+  let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 metas p)) r.lhs in
+  let lhs = add_args (symb s) lhs in
+  (* [to_term_env m] computes the term with environment corresponding to the
+     metavariable [m]. *)
+  let to_term_env : meta option -> term_env = fun m ->
+    let m = match m with Some m -> m | None -> assert false in
+    let xs = Array.init m.meta_arity (Printf.sprintf "x%i") in
+    let xs = Bindlib.new_mvar mkfree xs in
+    let ar = Array.map _Vari xs in
+    TE_Some (Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m ar))) in
+  let terms_env = Array.map to_term_env metas in
+  let rhs = Bindlib.msubst r.rhs terms_env in
+  (lhs, rhs)
+
+(** [to_closed_terms r] translates the rule [r] into a pair of terms. The
+    pattern variables in the LHS are replaced by fresh symbols as in the
+    function [to_closed] and the terms with environment in the RHS are
+    replaced by their corresponding symbols. *)
+let to_closed_terms : sym * rule -> term * term = fun (s, r) ->
+  let arity = Bindlib.mbinder_arity r.rhs in
+  let symbs = Array.init arity (fun _ -> None) in
+  let lhs = List.map (fun p -> Bindlib.unbox (to_closed symbs p)) r.lhs in
+  let lhs = add_args (symb s) lhs in
+  let to_term_env : sym option -> term_env = fun s ->
+    let s = match s with Some s -> s | None -> assert false in
+    TE_Some (Bindlib.unbox (Bindlib.bind_mvar [||] (_Symb s Nothing))) in
+  let terms_env = Array.map to_term_env symbs in
+  let rhs = Bindlib.msubst r.rhs terms_env in
+  (lhs, rhs)
+
+(** [check_fo t] checks that [t] is a first-order term. *)
+let rec check_fo : term -> unit = fun t ->
+  match t with
+  | Type
+  | Kind
+  | Symb _
+  | Wild
+  | Patt _                      -> ()
+  | Meta (_, ar) when ar = [||] -> ()
+  | Appl (u, v)                 -> check_fo u; check_fo v
+  | _                           -> raise Not_FO

src/completion.ml

@@ -0,0 +1,228 @@
+(** Completion procedure for closed equations *)
+
+open Terms
+open Basics
+open Extra
+open Timed
+
+(** [lpo ord] computes the lexicographic path ordering corresponding to
+    the strict total order [ord] on the set of all function symbols. *)
+let rec lpo : sym Ord.cmp -> term Ord.cmp = fun ord t1 t2 ->
+  let f, args = get_args t1 in
+  let f = get_symb f in
+  match f with
+  | None   -> if t1 == t2 then 0 else -1
+  | Some f ->
+      if List.exists (fun x -> lpo ord x t2 >= 0) args then 1
+      else
+        let g, args' = get_args t2 in
+        let g = get_symb g in
+        match g with
+        | None   -> 1
+        | Some g ->
+            match ord f g with
+            | k when k > 0 ->
+                if List.for_all (fun x -> lpo ord t1 x > 0) args' then 1
+                else -1
+            | 0            ->
+                if List.for_all (fun x -> lpo ord t1 x > 0) args' then
+                  Ord.ord_lex (lpo ord) args args'
+                else -1
+            | _            -> -1
+
+(** [to_rule (lhs, rhs)] tranlates the pair [(lhs, rhs)] of closed terms into
+    a rule. *)
+let to_rule : term * term -> sym * rule = fun (lhs, rhs) ->
+  let (s, args) = get_args lhs in
+  let s = get_symb s in
+  match s with
+  | None   -> assert false
+  | Some s ->
+      let vs = Bindlib.new_mvar te_mkfree [||] in
+      let rhs = Bindlib.unbox (Bindlib.bind_mvar vs (lift rhs)) in
+      s, { lhs = args ; rhs = rhs ; arity = List.length args ; vars = [||] }
+
+(** [find_deps eqs] returns a pair [(symbs, deps)], where [symbs] is a list of
+    (names of) new symbols and [deps] is a list of pairs of symbols. (s, t)
+    is added into [deps] iff there is a equation (l, r) in [eqs] such that
+    (l = s and t is a proper subterm of r) or (r = s and t is a proper subterm
+    of l). In this case, we also add s and t into [symbs]. *)
+let find_deps : (term * term) list -> string list * (string * string) list
+  = fun eqs ->
+  let deps = ref [] in
+  let symbs = ref [] in
+  let add_symb name =
+    if not (List.mem name !symbs) then symbs := name :: !symbs in
+  let add_dep dep =
+    if not (List.mem dep !deps) then deps := dep :: !deps in
+  let find_dep_aux (t1, t2) =
+    match get_symb t1 with
+    | Some sym ->
+        if is_new_symb sym then
+          let check_root t =
+            let g, _ = get_args t in
+            match get_symb g with
+            | Some sym' when is_new_symb sym' ->
+                add_dep (sym.sym_name, sym'.sym_name);
+                add_symb sym.sym_name;
+                add_symb sym'.sym_name;
+            | _                           -> () in
+          let _, args = get_args t2 in
+          List.iter (Basics.iter check_root) args
+    | None     -> () in
+  List.iter
+    (fun (t1, t2) -> find_dep_aux (t1, t2); find_dep_aux (t2, t1)) eqs;
+  (!symbs, !deps)
+
+module StrMap = Map.Make(struct
+  type t = string
+  let compare = compare
+end)
+
+exception Not_DAG
+
+(** [topo_sort symbs edges] computes a topological sort on the directed graph
+    [(symbs, edges)]. *)
+let topo_sort : string list -> (string * string) list -> int StrMap.t
+  = fun symbs edges ->
+  let n = List.length symbs in
+  let i = ref (-1) in
+  let name_map =
+    List.fold_left
+      (fun map s -> incr i; StrMap.add s !i map) StrMap.empty symbs in
+  let adj = Array.make_matrix n n 0 in
+  let incoming = Array.make n 0 in
+  List.iter
+    (fun (s1, s2) ->
+      let i1 = StrMap.find s1 name_map in
+      let i2 = StrMap.find s2 name_map in
+      adj.(i1).(i2) <- 1 + adj.(i1).(i2);
+      incoming.(i2) <- 1 + incoming.(i2)) edges;
+  let no_incoming = ref [] in
+  let remove_edge (i, j) =
+    if adj.(i).(j) <> 0 then begin
+      adj.(i).(j) <- 0;
+      incoming.(j) <- incoming.(j) - 1;
+      if incoming.(j) = 0 then no_incoming := j :: !no_incoming
+    end
+  in
+  Array.iteri
+    (fun i incoming ->
+      if incoming = 0 then no_incoming := i :: !no_incoming) incoming;
+  let ord = ref 0 in
+  let ord_array = Array.make n (-1) in
+  while !no_incoming <> [] do
+    let s = List.hd !no_incoming in
+    ord_array.(s) <- !ord;
+    incr ord;
+    no_incoming := List.tl !no_incoming;
+    for i = 0 to n-1 do
+      remove_edge (s, i)
+    done;
+  done;
+  if Array.exists (fun x -> x > 0) incoming then raise Not_DAG
+  else
+    List.fold_left
+      (fun map s ->
+        let i = StrMap.find s name_map in
+        StrMap.add s (ord_array.(i)) map) StrMap.empty symbs
+
+(** [ord_from_eqs eqs s1 s2] computes the order induced by the equations
+    [eqs]. We first use [find_deps] to find the dependency between the new
+    symbols (symbols introduced for checking SR) and compute its corresponding
+    DAG. The order obtained satisfies the following property:
+    1. New symbols are always larger than the orginal ones.
+    2. If [s1] and [s2] are not new symbols, then we use the usual
+       lexicographic order.
+    3. If [s1] and [s2] are new symbols, then if the topological order is well
+       defined then we compare their positions in this latter one. Otherwise,
+       we use the usual lexicographic order. *)
+let ord_from_eqs : (term * term) list -> sym Ord.cmp = fun eqs ->
+  let symbs, deps = find_deps eqs in
+  try
+    let ord = topo_sort symbs deps in
+    fun s1 s2 ->
+      match (is_new_symb s1, is_new_symb s2) with
+      | true, true   ->
+          if s1 == s2 then 0
+          else begin
+            try
+              StrMap.find s2.sym_name ord - StrMap.find s1.sym_name ord
+            with _ -> Pervasives.compare s1.sym_name s2.sym_name
+          end
+      | true, false  -> 1
+      | false, true  -> -1
+      | false, false -> Pervasives.compare s1.sym_name s2.sym_name
+  with Not_DAG ->
+    fun s1 s2 -> Pervasives.compare s1.sym_name s2.sym_name
+
+(** [completion eqs ord] returns the convergent rewrite system obtained from
+    the completion procedure on the set of equations [eqs] using the LPO
+    [lpo ord]. *)
+let completion : (term * term) list -> sym Ord.cmp -> (sym * rule list) list
+  = fun eqs ord ->
+  let lpo = lpo ord in
+  (* [symbs] is used to store all the symbols appearing in the equations. *)
+  let symbs = ref [] in
+  (* [reset_sym t] erases all the rules defined for all the symbols in
+     [symbs]. Note that these rules can be retrieved using [t1]. *)
+  let reset_sym t =
+    match t with
+    | Symb (s, _) when not (List.mem s !symbs) ->
+        s.sym_rules := [];
+        symbs := s :: !symbs
+    | _                                        -> () in
+  List.iter
+    (fun (t1, t2) -> Basics.iter reset_sym t1; Basics.iter reset_sym t2) eqs;
+  let add_rule (s, r) = s.sym_rules := r :: !(s.sym_rules) in
+  (* [orient (t1, t2)] orients the equation [t1 = t2] using LPO. *)
+  let orient (t1, t2) =
+    match lpo t1 t2 with
+    | 0            -> ()
+    | k when k > 0 -> add_rule (to_rule (t1, t2))
+    | _            -> add_rule (to_rule (t2, t1)) in
+  List.iter orient eqs;
+  let completion_aux : unit -> bool = fun () ->
+    let b = ref false in
+    (* [to_add] is used to store the new rules that need to be added. *)
+    let to_add = ref [] in
+    (* [find_cp s] applies the following procedure to all the rules of head
+       symbol [s]. *)
+    let find_cp s =
+      (* Intuitively, [f acc rs' r] corresponds to a sequence of Deduce,
+         Simplify, and Orient (or Delete) steps in the Knuth-Bendix
+         completion algorithm. Here, we attempts to deal with the critical
+         pairs between [r] and the other rules. Since only closed equations
+         are considered here, a critical pair between the rules (l1, r1) and
+         (l2, r2) is of the form (r1, r2') or (r1', r2) where ri' is a reduct
+         of ri. Note that [acc @ rs'] is the list of rules of head symbol [s]
+         other than [r]. *)
+      let f acc rs' r =
+        s.sym_rules := acc @ rs';
+        let (lhs, rhs) = to_terms (s, r) in
+        let lhs' = Eval.snf lhs in
+        let rhs' = Eval.snf rhs in
+        s.sym_rules := r :: !(s.sym_rules);
+        if eq lhs lhs' then ()
+        else begin
+          match lpo lhs' rhs' with
+          | 0            -> ()
+          | k when k > 0 ->
+              to_add := to_rule (lhs', rhs') :: !to_add;
+              b := true;
+          | _            ->
+              to_add := to_rule (rhs', lhs') :: !to_add;
+              b := true;
+        end
+      in
+      let rec aux acc f rs =
+        match rs with
+        | []       -> ()
+        | r :: rs' -> f acc rs' r; aux (r :: acc) f rs' in
+      aux [] f !(s.sym_rules) in
+    List.iter find_cp !symbs;
+    List.iter add_rule !to_add;
+    !b in
+  let b = ref true in
+  while !b do b := completion_aux () done;
+  List.map (fun s -> (s, !(s.sym_rules))) !symbs