Work on inference, unification and subject-reduction

src/core/basics.ml

@@ -4,15 +4,9 @@ open Extra
 open Timed
 open Terms
 
-(** Sets and maps of variables. *)
-module Var =
-  struct
-    type t = term Bindlib.var
-    let compare = Bindlib.compare_vars
-  end
-
-module VarSet = Set.Make(Var)
-module VarMap = Map.Make(Var)
+(** Create an array of fresh variables [|x1;..;xn|]. *)
+let fresh_vars : int -> tvar array = fun n ->
+  Bindlib.new_mvar mkfree (Array.init n (Printf.sprintf "x%i"))
 
 (** [to_tvar t] returns [x] if [t] is of the form [Vari x] and fails
     otherwise. *)
@@ -71,48 +65,6 @@ let add_args : term -> term list -> term = fun t args ->
     | u::args -> add_args (Appl(t,u)) args
   in add_args t args
 
-(** [eq ctx t u] tests the equality of [t] and [u] (up to α-equivalence). It
-    fails if [t] or [u] contain terms of the form [Patt(i,s,e)] or
-    [TEnv(te,env)].  In the process, subterms of the form [TRef(r)] in [t] and
-    [u] may be set with the corresponding value to enforce equality, and
-    variables appearing in [ctx] can be unfolded. In other words, [eq t u] can
-    be used to implement non-linear matching (see {!module:Rewrite}). When the
-    matching feature is used, one should make sure that [TRef] constructors do
-    not appear both in [t] and in [u] at the same time. Indeed, the references
-    are set naively, without checking occurrence. *)
-let eq : ctxt -> term -> term -> bool = fun ctx a b -> a == b ||
-  let exception Not_equal in
-  let rec eq l =
-    match l with
-    | []       -> ()
-    | (a,b)::l ->
-    match (Ctxt.unfold ctx a, Ctxt.unfold ctx b) with
-    | (a          , b          ) when a == b -> eq l
-    | (Vari(x1)   , Vari(x2)   ) when Bindlib.eq_vars x1 x2 -> eq l
-    | (Type       , Type       )
-    | (Kind       , Kind       ) -> eq l
-    | (Symb(s1,_) , Symb(s2,_) ) when s1 == s2 -> eq l
-    | (Prod(a1,b1), Prod(a2,b2))
-    | (Abst(a1,b1), Abst(a2,b2)) -> let (_, b1, b2) = Bindlib.unbind2 b1 b2 in
-                                    eq ((a1,a2)::(b1,b2)::l)
-    | (LLet(a1,t1,u1), LLet(a2,t2,u2)) ->
-        let (_, u1, u2) = Bindlib.unbind2 u1 u2 in
-        eq ((a1,a2)::(t1,t2)::(u1,u2)::l)
-    | (Appl(t1,u1), Appl(t2,u2)) -> eq ((t1,t2)::(u1,u2)::l)
-    | (Meta(m1,e1), Meta(m2,e2)) when m1 == m2 ->
-        eq (if e1 == e2 then l else List.add_array2 e1 e2 l)
-    | (Wild       , _          )
-    | (_          , Wild       ) -> eq l
-    | (TRef(r)    , b          ) -> r := Some(b); eq l
-    | (a          , TRef(r)    ) -> r := Some(a); eq l
-    | (Patt(_,_,_), _          )
-    | (_          , Patt(_,_,_))
-    | (TEnv(_,_)  , _          )
-    | (_          , TEnv(_,_)  ) -> assert false
-    | (_          , _          ) -> raise Not_equal
-  in
-  try eq [(a,b)]; true with Not_equal -> false
-
 (** [is_symb s t] tests whether [t] is of the form [Symb(s)]. *)
 let is_symb : sym -> term -> bool = fun s t ->
   match unfold t with
@@ -178,13 +130,18 @@ let occurs : meta -> term -> bool =
   let fn p = if m == p then raise Found in
   try iter_meta false fn t; false with Found -> true
 
-(** [get_metas b t] returns the list of all the metavariables in [t], and in
-    the types of metavariables recursively if [b], sorted wrt [cmp_meta]. *)
-let get_metas : bool -> term -> meta list = fun b t ->
+(** [add_metas b t ms] extends [ms] with all the metavariables of [t], and
+   those in the types of these metavariables recursively if [b]. *)
+let add_metas : bool -> term -> MetaSet.t -> MetaSet.t = fun b t ms ->
   let open Stdlib in
-  let l = ref [] in
-  iter_meta b (fun m -> l := m :: !l) t;
-  List.sort_uniq cmp_meta !l
+  let ms = ref ms in
+  iter_meta b (fun m -> ms := MetaSet.add m !ms) t;
+  !ms
+
+(** [get_metas b t] returns the set of all the metavariables in [t], and in
+    the types of metavariables recursively if [b]. *)
+let get_metas : bool -> term -> MetaSet.t = fun b t ->
+  add_metas b t MetaSet.empty
 
 (** [has_metas b t] checks whether there are metavariables in [t], and in the
     types of metavariables recursively if [b] is true. *)
@@ -209,29 +166,6 @@ let distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts ->
   in
   try Some (Array.map to_var ts) with Not_unique_var -> None
 
-(** [nl_distinct_vars ctx ts] checks that [ts] is made of variables  [vs] only
-    and returns some copy of [vs] where variables occurring more than once are
-    replaced by fresh variables.  Variables defined in  [ctx] are unfolded. It
-    returns [None] otherwise. *)
-let nl_distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts ->
-  let exception Not_a_var in
-  let open Stdlib in
-  let vars = ref VarSet.empty
-  and nl_vars = ref VarSet.empty in
-  let to_var t =
-    match Ctxt.unfold ctx t with
-    | Vari(x) ->
-        if VarSet.mem x !vars then nl_vars := VarSet.add x !nl_vars else
-        vars := VarSet.add x !vars;
-        x
-    | _       -> raise Not_a_var
-  in
-  let replace_nl_var x =
-    if VarSet.mem x !nl_vars then Bindlib.new_var mkfree "_" else x
-  in
-  try Some (Array.map replace_nl_var (Array.map to_var ts))
-  with Not_a_var -> None
-
 (** {3 Conversion of a rule into a "pair" of terms} *)
 
 (** [terms_of_rule r] converts the RHS (right hand side) of the rewriting rule
@@ -246,4 +180,4 @@ let term_of_rhs : rule -> term = fun r ->
     let p = _Patt (Some(i)) name (Array.map Bindlib.box_var vars) in
     TE_Some(Bindlib.unbox (Bindlib.bind_mvar vars p))
   in
-  Bindlib.msubst r.rhs (Array.mapi fn r.vars)
+  Bindlib.msubst r.rhs (Array.mapi fn r.pvs)

src/core/eval.ml

@@ -49,7 +49,7 @@ type stack = term list
 
 (** [whnf_beta t] computes a weak head beta normal form of the term [t]. *)
 let rec whnf_beta : term -> term = fun t ->
-  if !log_enabled then log_eval "evaluating [%a]" pp t;
+  if !log_enabled then log_eval "evaluating %a" pp t;
   let s = Stdlib.(!steps) in
   let (u, stk) = whnf_beta_stk t [] in
   if Stdlib.(!steps) <> s then add_args u stk else unfold t

src/core/extra.ml

@@ -239,6 +239,15 @@ module List =
             | _ -> false
       in in_sorted
 
+    (** [insert cmp x l] inserts [x] in the list [l] assuming that [l] is
+       sorted wrt [cmp]. *)
+    let insert : 'a cmp -> 'a -> 'a list -> 'a list = fun cmp x ->
+      let rec insert acc l =
+        match l with
+        | y :: m when cmp x y > 0 -> insert (y::acc) m
+        | _ -> List.rev_append acc (x::l)
+      in insert []
+
   end
 
 module Array =

src/core/handle.ml

@@ -117,7 +117,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option =
         if !(s.sym_def) <> None then
           fatal pr.pos "Rewriting rules cannot be given for defined \
                         symbol [%s]." s.sym_name;
-        Sr.check_rule ss.builtins r; r
+        Sr.check_rule ss.builtins r
       in
       let rs = List.map handle_rule rs in
       (* Adding the rules all at once. *)

src/core/infer.ml

@@ -14,7 +14,7 @@ let constraints = Stdlib.ref []
 
 (** Function adding a constraint. *)
 let conv ctx a b =
-  if not (Basics.eq ctx a b) then
+  if not (Eval.eq_modulo ctx a b) then
     begin
       if !log_enabled then log_infr (yel "add %a") pp_constr (ctx,a,b);
       let open Stdlib in constraints := (ctx,a,b) :: !constraints
@@ -37,7 +37,7 @@ let make_meta_codomain : ctxt -> term -> tbinder = fun ctx a ->
    constraints are satisfied. [ctx] must be well-formed. This function
    never fails (but constraints may be unsatisfiable). *)
 let rec infer : ctxt -> term -> term = fun ctx t ->
-  if !log_enabled then log_infr "infer [%a]" pp t;
+  if !log_enabled then log_infr "infer %a%a" pp_ctxt ctx pp t;
   match unfold t with
   | Patt(_,_,_) -> assert false (* Forbidden case. *)
   | TEnv(_,_)   -> assert false (* Forbidden case. *)
@@ -51,11 +51,19 @@ let rec infer : ctxt -> term -> term = fun ctx t ->
 
   (* ---------------------------------
       ctx ⊢ Vari(x) ⇒ Ctxt.find x ctx  *)
-  | Vari(x)     -> (try Ctxt.type_of x ctx with Not_found -> assert false)
+  | Vari(x)     ->
+      let a = try Ctxt.type_of x ctx with Not_found -> assert false in
+      if !log_enabled then
+        log_infr (blu "%a : %a") pp_term t pp_term a;
+      a
 
   (* -------------------------------
       ctx ⊢ Symb(s) ⇒ !(s.sym_type)  *)
-  | Symb(s,_)   -> !(s.sym_type)
+  | Symb(s,_)   ->
+      let a = !(s.sym_type) in
+      if !log_enabled then
+        log_infr (blu "%a : %a") pp_term t pp_term a;
+      a
 
   (*  ctx ⊢ a ⇐ Type    ctx, x : a ⊢ b<x> ⇒ s
      -----------------------------------------
@@ -127,54 +135,16 @@ let rec infer : ctxt -> term -> term = fun ctx t ->
   (*  ctx ⊢ term_of_meta m e ⇒ a
      ----------------------------
          ctx ⊢ Meta(m,e) ⇒ a      *)
-  | Meta(m,e)   ->
-      if !log_enabled then
-        log_infr (yel "%s is of type [%a]") (meta_name m) pp !(m.meta_type);
-      infer ctx (term_of_meta m e)
+  | Meta(m,ts)   ->
+      infer ctx (term_of_meta m ts)
 
 (** [check ctx t c] checks that the term [t] has type [c] in context
    [ctx], possibly under some constraints recorded in [constraints]
    using [conv]. [ctx] must be well-formed and [c] well-sorted. This
    function never fails (but constraints may be unsatisfiable). *)
-
-(* [check ctx t c] could be reduced to the default case [conv
-   (infer ctx t) c]. We however provide some more efficient
-   code when [t] is an abstraction, as witnessed by 'make holide':
-
-   Finished in 3:56.61 at 99% with 3180096Kb of RAM
-
-   Finished in 3:46.13 at 99% with 2724844Kb of RAM
-
-   This avoids to build a product to destructure it just after. *)
 and check : ctxt -> term -> term -> unit = fun ctx t c ->
-  if !log_enabled then log_infr "check [%a] [%a]" pp t pp c;
-  match unfold t with
-  (*  c → Prod(d,b)    a ~ d    ctx, x : A ⊢ t<x> ⇐ b<x>
-      ----------------------------------------------------
-                         ctx ⊢ Abst(a,t) ⇐ c                   *)
-  | Abst(a,t)   ->
-      (* We ensure that [a] is of type [Type]. *)
-      check ctx a Type;
-      (* We (hopefully) evaluate [c] to a product, and get its body. *)
-      let b =
-        let c = Eval.whnf ctx c in
-        match c with
-        | Prod(d,b)  -> conv ctx d a; b (* Domains must be convertible. *)
-        | Meta(m,ts) ->
-            let mxs, p, _bp1, bp2 = Env.extend_meta_type m in
-            conv ctx mxs p; Bindlib.msubst bp2 ts
-        | _         ->
-           let b = make_meta_codomain ctx a in
-           conv ctx c (Prod(a,b)); b
-      in
-      (* We type-check the body with the codomain. *)
-      let (x,t,ctx') = Ctxt.unbind ctx a None t in
-      check ctx' t (Bindlib.subst b (Vari(x)))
-  | t           ->
-      (*  ctx ⊢ t ⇒ a
-         -------------
-          ctx ⊢ t ⇐ a  *)
-      conv ctx (infer ctx t) c
+  if !log_enabled then log_infr "check %a : %a" pp t pp c;
+  conv ctx (infer ctx t) c
 
 (** [infer ctx t] returns a pair [(a,cs)] where [a] is a type for the
    term [t] in the context [ctx], under unification constraints [cs].
@@ -187,8 +157,8 @@ let infer : ctxt -> term -> term * unif_constrs = fun ctx t ->
   let constrs = Stdlib.(!constraints) in
   if !log_enabled then
     begin
-      log_infr (gre "infer [%a] yields [%a]") pp t pp a;
-      List.iter (log_infr "  assuming %a" pp_constr) constrs;
+      log_infr (gre "infer %a : %a") pp t pp a;
+      List.iter (log_infr "  if %a" pp_constr) constrs;
     end;
   Stdlib.(constraints := []);
   (a, constrs)
@@ -204,8 +174,8 @@ let check : ctxt -> term -> term -> unif_constrs = fun ctx t c ->
   let constrs = Stdlib.(!constraints) in
   if !log_enabled then
     begin
-      log_infr (gre "check [%a] [%a]") pp t pp c;
-      List.iter (log_infr "  assuming %a" pp_constr) constrs;
+      log_infr (gre "check %a : %a") pp t pp c;
+      List.iter (log_infr "  if %a" pp_constr) constrs;
     end;
   Stdlib.(constraints := []);
   constrs

src/core/proof.ml

@@ -22,6 +22,9 @@ module Goal :
 
     (** [simpl g] simplifies the given goal, evaluating its type to SNF. *)
     val simpl : t -> t
+
+    (** Comparison function. *)
+    val compare : t -> t -> int
   end =
   struct
     type t =
@@ -42,6 +45,9 @@ module Goal :
 
     let simpl : t -> t = fun g ->
       {g with goal_type = Eval.snf (Env.to_ctxt g.goal_hyps) g.goal_type}
+
+    let compare : t -> t -> int = fun g1 g2 ->
+      Meta.compare g1.goal_meta g2.goal_meta
   end
 
 (** Representation of the proof state of a theorem. *)

src/core/queries.ml

@@ -31,7 +31,7 @@ let handle_query : sig_state -> Proof.t option -> p_query -> unit =
           | (Some(a), Some(b)) ->
               let pb = { no_problems with to_solve = [[], a, b] } in
               begin
-                match solve ss.builtins true pb with
+                match solve ss.builtins pb with
                 | None -> fatal q.pos "Infered types are not convertible."
                 | Some [] -> Eval.eq_modulo [] t u
                 | Some cs ->

src/core/rewrite.ml

@@ -13,6 +13,51 @@ open Print
 let log_rewr = new_logger 'r' "rewr" "the rewrite tactic"
 let log_rewr = log_rewr.logger
 
+(** [eq ctx t u] tests the equality of [t] and [u] (up to α-equivalence). It
+    fails if [t] or [u] contain terms of the form [Patt(i,s,e)] or
+    [TEnv(te,env)].  In the process, subterms of the form [TRef(r)] in [t] and
+    [u] may be set with the corresponding value to enforce equality, and
+    variables appearing in [ctx] can be unfolded. In other words, [eq t u] can
+    be used to implement non-linear matching. When the
+    matching feature is used, one should make sure that [TRef] constructors do
+    not appear both in [t] and in [u] at the same time. Indeed, the references
+    are set naively, without occurrence checking. *)
+let eq : ctxt -> term -> term -> bool = fun ctx a b -> a == b ||
+  let exception Not_equal in
+  let rec eq l =
+    match l with
+    | []       -> ()
+    | (a,b)::l ->
+    begin
+    if !log_enabled then log_rewr "eq [%a] [%a]" pp_term a pp_term b;
+    match (Ctxt.unfold ctx a, Ctxt.unfold ctx b) with
+    | (a          , b          ) when a == b -> eq l
+    | (Vari(x1)   , Vari(x2)   ) when Bindlib.eq_vars x1 x2 -> eq l
+    | (Type       , Type       )
+    | (Kind       , Kind       ) -> eq l
+    | (Symb(s1,_) , Symb(s2,_) ) when s1 == s2 -> eq l
+    | (Prod(a1,b1), Prod(a2,b2))
+    | (Abst(a1,b1), Abst(a2,b2)) -> let (_, b1, b2) = Bindlib.unbind2 b1 b2 in
+                                    eq ((a1,a2)::(b1,b2)::l)
+    | (LLet(a1,t1,u1), LLet(a2,t2,u2)) ->
+        let (_, u1, u2) = Bindlib.unbind2 u1 u2 in
+        eq ((a1,a2)::(t1,t2)::(u1,u2)::l)
+    | (Appl(t1,u1), Appl(t2,u2)) -> eq ((t1,t2)::(u1,u2)::l)
+    | (Meta(m1,e1), Meta(m2,e2)) when m1 == m2 ->
+        eq (if e1 == e2 then l else List.add_array2 e1 e2 l)
+    | (Wild       , _          )
+    | (_          , Wild       ) -> eq l
+    | (TRef(r)    , b          ) -> r := Some(b); eq l
+    | (a          , TRef(r)    ) -> r := Some(a); eq l
+    | (Patt(_,_,_), _          )
+    | (_          , Patt(_,_,_))
+    | (TEnv(_,_)  , _          )
+    | (_          , TEnv(_,_)  ) -> assert false
+    | (_          , _          ) -> raise Not_equal
+    end
+  in
+  try eq [(a,b)]; true with Not_equal -> false
+
 (** Rewrite patterns as in Coq/SSReflect. See "A Small Scale
     Reflection Extension for the Coq system", by Georges Gonthier,
     Assia Mahboubi and Enrico Tassi, INRIA Research Report 6455, 2016,
@@ -165,7 +210,7 @@ let break_prod : term -> term * tvar array = fun a ->
 let match_pattern : to_subst -> term -> term array option = fun (xs,p) t ->
   let ts = Array.map (fun _ -> TRef(ref None)) xs in
   let p = Bindlib.msubst (Bindlib.unbox (Bindlib.bind_mvar xs (lift p))) ts in
-  if Basics.eq [] p t then Some(Array.map unfold ts) else None
+  if eq [] p t then Some(Array.map unfold ts) else None
 
 (** [find_subst t (xs,p)] is given a term [t] and a pattern [p] (with “pattern
     variables” of [xs]),  and it finds the first instance of (a term matching)
@@ -198,7 +243,7 @@ let find_subst : term -> to_subst -> term array option = fun t (xs,p) ->
 let make_pat : term -> term -> bool = fun t p ->
   let time = Time.save () in
   let rec make_pat_aux : term -> bool = fun t ->
-    if Basics.eq [] t p then true else
+    if eq [] t p then true else
       begin
         Time.restore time;
         match unfold t with
@@ -218,7 +263,7 @@ let make_pat : term -> term -> bool = fun t p ->
 let bind_match : term -> term -> tbinder =  fun p t ->
   let x = Bindlib.new_var mkfree "X" in
   let rec lift_subst : term -> tbox = fun t ->
-    if Basics.eq [] p t then _Vari x else
+    if eq [] p t then _Vari x else
     match unfold t with
     | Vari(y)     -> _Vari y
     | Type        -> _Type