Work on inference, unification and subject-reduction

src/core/basics.ml

@@ -4,15 +4,11 @@ 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)
+(** [fresh_vars n] creates an array of [n] fresh variables. The names of these
+    variables is ["_var_i"], where [i] is a number introduced by the [Bindlib]
+    library to avoid name clashes (minimal renaming is done). *)
+let fresh_vars : int -> tvar array = fun n ->
+  Bindlib.new_mvar mkfree (Array.make n "_var_")
 
 (** [to_tvar t] returns [x] if [t] is of the form [Vari x] and fails
     otherwise. *)
@@ -71,48 +67,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 +132,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 +168,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
@@ -240,7 +176,8 @@ let nl_distinct_vars : ctxt -> term array -> tvar array option = fun ctx ts ->
     LHS counterparts. This is a more convenient way of representing terms when
     analysing confluence or termination. *)
 let term_of_rhs : rule -> term = fun r ->
-  let fn i (name, arity) =
+  let fn i x =
+    let (name, arity) = (Bindlib.name_of x, r.arities.(i)) in
     let make_var i = Bindlib.new_var mkfree (Printf.sprintf "x%i" i) in
     let vars = Array.init arity make_var in
     let p = _Patt (Some(i)) name (Array.map Bindlib.box_var vars) in

src/core/env.ml

@@ -27,17 +27,21 @@ let add : tvar -> tbox -> tbox option -> env -> env = fun v a t env ->
 let find : string -> env -> tvar = fun n env ->
   let (x,_,_) = List.assoc n env in x
 
-(** [to_prod env t] builds a sequence of products or let-bindings whose
-    domains are the variables of the environment [env] (from left to right),
-    and which body is the term [t]:
-    [to_prod [(xn,an,None);..;(x1,a1,None)] t = ∀x1:a1,..,∀xn:an,t]. *)
-let to_prod : env -> tbox -> term = fun env t ->
+(** [to_prod env t] builds a sequence of products / let-bindings whose domains
+    are the variables of the environment [env] (from left to right), and whose
+    body is the term [t]. By calling [to_prod [(xn,an,None);⋯;(x1,a1,None)] t]
+    you obtain a term of the form [∀x1:a1,..,∀xn:an,t]. *)
+let to_prod_box : env -> tbox -> tbox = fun env t ->
   let fn t (_,(x,a,u)) =
     match u with
     | Some(u) -> _LLet a u (Bindlib.bind_var x t)
     | None    -> _Prod a (Bindlib.bind_var x t)
   in
-  Bindlib.unbox (List.fold_left fn t env)
+  List.fold_left fn t env
+
+(** [to_prod] is an “unboxed” version of [to_prod_box]. *)
+let to_prod : env -> tbox -> term = fun env t ->
+  Bindlib.unbox (to_prod_box env t)
 
 (** [to_abst env t] builds a sequence of abstractions or let bindings,
     depending on the definition of the elements in the environment whose

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

@@ -112,12 +112,13 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option =
       ({ss with in_scope = StrMap.add x.elt (s, x.pos) ss.in_scope}, None)
   | P_rules(rs)                ->
       (* Scoping and checking each rule in turn. *)
-      let handle_rule pr =
-        let (s,_,_) as r = scope_rule ss pr in
-        if !(s.sym_def) <> None then
+      let handle_rule r =
+        let pr = scope_rule ss r in
+        let (sym, hint) = pr.elt.pr_sym in
+        if !(sym.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
+                        symbol [%s]." sym.sym_name;
+        (sym, hint, Pos.make r.pos (Sr.check_rule ss.builtins pr))
       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/pretty.ml

@@ -235,6 +235,9 @@ let rec pp_ast : ast pp = fun oc cs ->
   | [c]   -> Format.fprintf oc "%a@." pp_command c
   | c::cs -> Format.fprintf oc "%a\n@.%a" pp_command c pp_ast cs
 
+(** Short synonym of [pp_p_term]. *)
+let pp : p_term pp = pp_p_term
+
 (** [beautify cmds] pretty-prints the commands [cmds] to standard output. *)
 let beautify : ast -> unit =
   pp_ast Format.std_formatter

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