Work on inference, unification and subject-reduction

src/core/basics.ml

@@ -178,13 +178,13 @@ 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 ->
+(** [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 ->
   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 MetaSet.empty in
+  iter_meta b (fun m -> ms := MetaSet.add m !ms) t;
+  !ms
 
 (** [has_metas b t] checks whether there are metavariables in [t], and in the
     types of metavariables recursively if [b] is true. *)
@@ -246,4 +246,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/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/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/scope.ml

@@ -282,13 +282,14 @@ let scope : mode -> sig_state -> env -> p_term -> tbox = fun md ss env t ->
     | (P_Wild          , M_LHS(_)         ) -> fresh_patt env
     | (P_Wild          , M_Patt           ) -> _Wild
     | (P_Wild          , _                ) ->
-        (* We create a metavariable [m] of type [m_ty], which is itself also a
-           metavariable (of type [Type]).  Note that this case applies both to
-           regular terms, and to the RHS of rewriting rules. *)
+        (* We create a metavariable [m] of type [tm], which itself is also a
+           metavariable [x] of type [Type].  Note that this case applies both
+           to regular terms, and to the RHS of rewriting rules. *)
         let vs = Env.to_tbox env in
-        let m_ty = fresh_meta (Env.to_prod env _Type) (Array.length vs) in
-        let a = Env.to_prod env (_Meta m_ty vs) in
-        let m = fresh_meta a (Array.length vs) in
+        let n = Array.length vs in
+        let x = fresh_meta (Env.to_prod env _Type) n in
+        let tm = Env.to_prod env (_Meta x vs) in
+        let m = fresh_meta tm n in
         _Meta m vs
     | (P_Meta(id,ts)   , M_Term(m,_)      ) ->
         let m2 =
@@ -480,7 +481,7 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r ->
   let (pvs_lhs, nl) = patt_vars p_lhs in
   let (pvs_rhs, _ ) = patt_vars p_rhs in
   (* NOTE to reject non-left-linear rules, we can check [nl = []] here. *)
-  (* Check that the meta-variables of the RHS exist in the LHS. *)
+  (* Check that the pattern variables of the RHS exist in the LHS. *)
   let check_in_lhs (m,i) =
     let j =
       try List.assoc m pvs_lhs with Not_found ->
@@ -491,11 +492,11 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r ->
   List.iter check_in_lhs pvs_rhs;
   (* Get the non-linear variables not in the RHS. *)
   let nl = List.filter (fun m -> not (List.mem_assoc m pvs_rhs)) nl in
-  (* Reserve space for meta-variables that appear non-linearly in the LHS. *)
+  (* Reserve space for pattern variables that appear non-linearly in the LHS. *)
   let pvs = List.map (fun m -> (m, List.assoc m pvs_lhs)) nl @ pvs_rhs in
   let map = List.mapi (fun i (m,_) -> (m,i)) pvs in
-  (* NOTE [map] maps meta-variables to their position in the environment. *)
-  (* NOTE meta-variables not in [map] can be considered as wildcards. *)
+  (* NOTE [map] maps pattern variables to their position in the environment. *)
+  (* NOTE pattern variables not in [map] can be considered as wildcards. *)
   (* Get privacy of the head of the rule, and scope the rest with this
      privacy. *)
   let prv = is_private (fst (get_root p_lhs ss)) in
@@ -515,7 +516,7 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r ->
         fatal p_lhs.pos "No head symbol in LHS."
   in
   if lhs = [] then wrn p_lhs.pos "LHS head symbol with no argument.";
-  (* We scope the RHS and bind the meta-variables. *)
+  (* We scope the RHS and bind the pattern variables. *)
   let names = Array.of_list (List.map fst map) in
   let vars = Bindlib.new_mvar te_mkfree names in
   let rhs =
@@ -524,9 +525,9 @@ let scope_rule : sig_state -> p_rule -> sym * pp_hint * rule loc = fun ss r ->
     Bindlib.unbox (Bindlib.bind_mvar vars (scope mode ss Env.empty p_rhs))
   in
   (* We also store [pvs] to facilitate confluence / termination checking. *)
-  let vars = Array.of_list pvs in
+  let pvs = Array.of_list pvs in
   (* We put everything together to build the rule. *)
-  (sym, hint, Pos.make r.pos {lhs; rhs; arity = List.length lhs; vars})
+  (sym, hint, Pos.make r.pos {lhs; rhs; arity = List.length lhs; pvs; vars})
 
 (** [scope_pattern ss env t] turns a parser-level term [t] into an actual term
     that will correspond to selection pattern (rewrite tactic). *)

src/core/sr.ml

@@ -66,8 +66,11 @@ let build_meta_type : int -> term = fun k ->
 let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit =
     fun builtins (s,h,r) ->
   if !log_enabled then log_subj "check_rule [%a]" pp_rule (s, h, r.elt);
-  (* We process the LHS to replace pattern variables by metavariables. *)
   let binder_arity = Bindlib.mbinder_arity r.elt.rhs in
+  (* Compute the metavariables of the RHS. *)
+  let rhs = Bindlib.msubst r.elt.rhs (Array.make binder_arity TE_None) in
+  let rhs_metas = Basics.get_metas true rhs in
+  (* We process the LHS to replace pattern variables by metavariables. *)
   let metas = Array.make binder_arity None in
   let rec to_m : int -> term -> tbox = fun k t ->
     (* [k] is the number of arguments to which [m] is applied. *)
@@ -102,8 +105,8 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit =
     | Wild        -> assert false (* Cannot appear in LHS. *)
     | TRef(_)     -> assert false (* Cannot appear in LHS. *)
   in
-  let lhs = List.map (fun p -> Bindlib.unbox (to_m 0 p)) r.elt.lhs in
-  let lhs = Basics.add_args (Symb(s,h)) lhs in
+  let lhs_args = List.map (fun p -> Bindlib.unbox (to_m 0 p)) r.elt.lhs in
+  let lhs = Basics.add_args (Symb(s,h)) lhs_args in
   let metas = Array.map (function Some m -> m | None -> assert false) metas in
   (* We substitute the RHS with the corresponding metavariables. *)
   let fn m =
@@ -113,7 +116,14 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit =
     TE_Some(Bindlib.unbox (Bindlib.bind_mvar xs (_Meta m e)))
   in
   let te_envs = Array.map fn metas in
-  let rhs = Bindlib.msubst r.elt.rhs te_envs in
+  let subst t = Bindlib.msubst t te_envs in
+  let rhs = subst r.elt.rhs in
+  (* We substitute the metavariables of the RHS as well. *)
+  let fn m =
+    let bt = lift !(m.meta_type) in
+    m.meta_type := subst (Bindlib.unbox (Bindlib.bind_mvar r.elt.vars bt))
+  in
+  MetaSet.iter fn rhs_metas;
   (* Infer the type of the LHS and the constraints. *)
   match Typing.infer_constr builtins [] lhs with
   | None                      -> wrn r.pos "Untypable LHS."
@@ -160,7 +170,7 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit =
   (* Check that there is no uninstanciated metas left. *)
   let lhs_metas = Basics.get_metas false lhs in
   let f m =
-    if not (List.in_sorted cmp_meta m lhs_metas) then
+    if not (MetaSet.mem m lhs_metas) then
       fatal r.pos "Cannot instantiate all metavariables in rule [%a]."
         pp_rule (s,h,r.elt)
   in

src/core/tactics.ml

@@ -56,9 +56,12 @@ let handle_tactic : sig_state -> Proof.t -> p_tactic -> Proof.t =
     set_meta m (Bindlib.unbox (Bindlib.bind_mvar (Env.vars env) (lift t)));
     (* New subgoals and focus. *)
     let metas = Basics.get_metas true t in
-    let new_goals = List.map Proof.Goal.of_meta metas in
+    let add_goal m = List.insert Proof.Goal.compare (Proof.Goal.of_meta m) in
+    let new_goals = MetaSet.fold add_goal metas [] in
+    (* New goals must appear first. *)
     Proof.({ps with proof_goals = new_goals @ gs})
   in
+
   match tac.elt with
   | P_tac_print
   | P_tac_proofterm

src/core/terms.ml

@@ -143,8 +143,10 @@ type term =
   (** Right hand side (or RHS). *)
   ; arity : int
   (** Required number of arguments to be applicable. *)
-  ; vars  : (string * int) array
-  (** Name and arity of the pattern variables bound in the RHS. *) }
+  ; pvs   : (string * int) array
+  (** Name and arity of the pattern variables bound in the RHS. *)
+  ; vars  : term_env Bindlib.var array
+  (** Bindlib variables used to build [rhs]. *) }
 
 (** The LHS (or pattern) of a rewriting rule is always formed of a head symbol
     (on which the rule is defined) applied to a list of pattern arguments. The
@@ -242,11 +244,12 @@ type term =
   ; meta_value : (term, term) Bindlib.mbinder option ref
   (** Definition of the metavariable, if known. *) }
 
-(** Comparison function on metavariables. *)
-let cmp_meta : meta -> meta -> int = fun m1 m2 -> m1.meta_key - m2.meta_key
+module Meta = struct
+  type t = meta
+  let compare m1 m2 = m1.meta_key - m2.meta_key
+end
 
-(** Equality on metavariables. *)
-let eq_meta : meta -> meta -> bool = fun m1 m2 -> m1.meta_key = m2.meta_key
+module MetaSet = Set.Make(Meta)
 
 (** [symb s] returns the term [Symb (s, Nothing)]. *)
 let symb : sym -> term = fun s -> Symb (s, Nothing)

src/core/xtc.ml

@@ -118,7 +118,7 @@ let print_tl_rule : Format.formatter -> int -> sym -> rule -> unit =
     in the form of a pair containing the name of the variable and its type,
     inferred by the solver. *)
 let get_vars : sym -> rule -> (string * Terms.term) list = fun s r ->
-  let rule_ctx : tvar option array = Array.make (Array.length r.vars) None in
+  let rule_ctx : tvar option array = Array.make (Array.length r.pvs) None in
   let var_list : tvar list ref = ref [] in
   let rec subst_patt v t =
     match t with

tests/OK/303.lp

@@ -0,0 +1,11 @@
+constant symbol U : TYPE
+
+constant symbol u : U
+
+constant symbol f : (U ⇒ U) ⇒ TYPE
+
+symbol G : U ⇒ TYPE
+
+constant symbol H : U ⇒ TYPE
+
+rule G &v → ∀ (a : H &v), f (λ _, u)

tests/OK/logic.lp

@@ -111,4 +111,4 @@ set builtin "top"   ≔ top
 set builtin "imp"   ≔ imp
 set builtin "and"   ≔ {|and|}
 set builtin "or"    ≔ or
-set builtin "not"   ≔ not
+set builtin "not"   ≔ not