fix checking of uninstantiated metavariables in rules #301

src/basics.ml

@@ -178,44 +178,44 @@ let iter : (term -> unit) -> term -> unit = fun action ->
     | Appl(t,u)  -> iter t; iter u
   in iter
 
-(** [iter_meta f t] applies the function [f] to every metavariable of
-   [t], as well as to every metavariable occurring in the type of an
-   uninstantiated metavariable occurring in [t], and so on. *)
-let rec iter_meta : (meta -> unit) -> term -> unit = fun f t ->
-  match unfold t with
-  | Patt(_,_,_)
-  | TEnv(_,_)
-  | Wild
-  | TRef(_)
-  | Vari(_)
-  | Type
-  | Kind
-  | Symb(_)    -> ()
-  | Prod(a,b)
-  | Abst(a,b)  -> iter_meta f a; iter_meta f (Bindlib.subst b Kind)
-  | Appl(t,u)  -> iter_meta f t; iter_meta f u
-  | Meta(v,ts) -> f v; iter_meta f !(v.meta_type); Array.iter (iter_meta f) ts
-
-(** {b NOTE} that {!val:iter_meta} is not implemented using {!val:iter} due to
-    the fact this it is performance-critical. *)
+(** [iter_meta b f t] applies the function [f] to every metavariable of [t],
+   and to the type of every metavariable recursively if [b] is true. *)
+let iter_meta : bool -> (meta -> unit) -> term -> unit = fun b f ->
+  let rec iter t =
+    match unfold t with
+    | Patt(_,_,_)
+    | TEnv(_,_)
+    | Wild
+    | TRef(_)
+    | Vari(_)
+    | Type
+    | Kind
+    | Symb(_)    -> ()
+    | Prod(a,b)
+    | Abst(a,b)  -> iter a; iter (Bindlib.subst b Kind)
+    | Appl(t,u)  -> iter t; iter u
+    | Meta(v,ts) -> f v; Array.iter iter ts; if b then iter !(v.meta_type)
+  in iter
 
 (** [occurs m t] tests whether the metavariable [m] occurs in the term [t]. *)
 let occurs : meta -> term -> bool =
   let exception Found in fun m t ->
   let fn p = if m == p then raise Found in
-  try iter_meta fn t; false with Found -> true
+  try iter_meta false fn t; false with Found -> true
 
-(** [get_metas t] returns the list of all the metavariables in [t]. *)
-let get_metas : term -> meta list = fun t ->
+(** [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 ->
   let open Pervasives in
   let l = ref [] in
-  iter_meta (fun m -> l := m :: !l) t;
-  List.sort_uniq (fun m1 m2 -> m1.meta_key - m2.meta_key) !l
+  iter_meta b (fun m -> l := m :: !l) t;
+  List.sort_uniq cmp_meta !l
 
-(** [has_metas t] checks that there are metavariables in [t]. *)
-let has_metas : term -> bool =
-  let exception Found in fun t ->
-  try iter_meta (fun _ -> raise Found) t; false with Found -> true
+(** [has_metas b t] checks whether there are metavariables in [t], and in the
+   types of metavariables recursively if [b] is true. *)
+let has_metas : bool -> term -> bool =
+  let exception Found in fun b t ->
+  try iter_meta b (fun _ -> raise Found) t; false with Found -> true
 
 (** [distinct_vars_opt ts] checks that [ts] is made of distinct
    variables and returns these variables. *)

src/extra.ml

@@ -6,6 +6,9 @@ type 'a pp = Format.formatter -> 'a -> unit
 (** Short name for the type of an equality function. *)
 type 'a eq = 'a -> 'a -> bool
 
+(** Short name for the type of a comparison function. *)
+type 'a cmp = 'a -> 'a -> int
+
 module Int =
   struct
     type t = int
@@ -61,7 +64,7 @@ module Option =
       | None    -> ()
       | Some(e) -> f e
 
-    let get : 'a option -> 'a -> 'a = fun o d ->
+    let get : 'a -> 'a option -> 'a = fun d o ->
       match o with
       | None    -> d
       | Some(e) -> e
@@ -204,6 +207,20 @@ module List =
     let init : int -> (int -> 'a) -> 'a list = fun n f ->
       if n < 0 then invalid_arg "Extra.List.init" else
       let rec loop k = if k > n then [] else f k :: loop (k + 1) in loop 0
+
+    (** [in_sorted cmp x l] tells whether [x] is in [l] assuming that [l] is
+       sorted wrt [cmp]. *)
+    let in_sorted : 'a cmp -> 'a -> 'a list -> bool = fun cmp x ->
+      let rec in_sorted l =
+        match l with
+        | [] -> false
+        | y :: l ->
+            match cmp x y with
+            | 0 -> true
+            | n when n > 0 -> in_sorted l
+            | _ -> false
+      in in_sorted
+
   end
 
 module Array =

src/handle.ml

@@ -109,7 +109,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option =
       (* We check that [a] is typable by a sort. *)
       Typing.sort_type ss.builtins Ctxt.empty a;
       (* We check that no metavariable remains. *)
-      if Basics.has_metas a then
+      if Basics.has_metas true a then
         begin
           fatal_msg "The type of [%s] has unsolved metavariables.\n" x.elt;
           fatal x.pos "We have %s : %a." x.elt pp a
@@ -179,7 +179,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option =
             | None    -> fatal cmd.pos "Cannot infer the type of [%a]." pp t
       in
       (* We check that no metavariable remains. *)
-      if Basics.has_metas t || Basics.has_metas a then
+      if Basics.has_metas true t || Basics.has_metas true a then
         begin
           fatal_msg "The definition of [%s] or its type \
                      have unsolved metavariables.\n" x.elt;
@@ -205,7 +205,7 @@ let handle_cmd : sig_state -> p_command -> sig_state * proof_data option =
       (* Check that [a] is typable and that its type is a sort. *)
       Typing.sort_type ss.builtins Ctxt.empty a;
       (* We check that no metavariable remains in [a]. *)
-      if Basics.has_metas a then
+      if Basics.has_metas true a then
         begin
           fatal_msg "The type of [%s] has unsolved metavariables.\n" x.elt;
           fatal x.pos "We have %s : %a." x.elt pp a

src/parser.ml

@@ -576,13 +576,14 @@ let parser cmd =
       -> List.iter (get_ops _loc) ps;
          P_open(ps)
   | e:exposition? p:property? _symbol_ s:ident al:arg* ":" a:term
-      -> P_symbol(Option.get e Terms.Public,Option.get p Terms.Defin,s,al,a)
+      -> P_symbol(Option.get Terms.Public e,
+                  Option.get Terms.Defin p,s,al,a)
   | _rule_ r:rule rs:{_:_and_ rule}*
       -> P_rules(r::rs)
   | e:exposition? _definition_ s:ident al:arg* ao:{":" term}? "≔" t:term
-      -> P_definition(Option.get e Terms.Public,false,s,al,ao,t)
+      -> P_definition(Option.get Terms.Public e,false,s,al,ao,t)
   | e:exposition? st:statement (ts,pe):proof
-      -> P_theorem(Option.get e Terms.Public,st,ts,pe)
+      -> P_theorem(Option.get Terms.Public e,st,ts,pe)
   | _set_ c:config
       -> P_set(c)
   | q:query

src/sign.ml

@@ -185,7 +185,7 @@ let unlink : t -> unit = fun sign ->
 let add_symbol : t -> expo -> prop -> strloc -> term -> bool list -> sym =
     fun sign sym_expo sym_prop s a impl ->
   (* Check for metavariables in the symbol type. *)
-  if Basics.has_metas a then
+  if Basics.has_metas true a then
     fatal s.pos "The type of [%s] contains metavariables" s.elt;
   (* We minimize [impl] to enforce our invariant (see {!type:Terms.sym}). *)
   let rec rem_false l = match l with false::l -> rem_false l | _ -> l in

src/sr.ml

@@ -103,9 +103,9 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit =
   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
-  (* We substitute the RHS with the corresponding metavariables.*)
+  let metas = Array.map (function Some m -> m | None -> assert false) metas in
+  (* We substitute the RHS with the corresponding metavariables. *)
   let fn 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 e = Array.map _Vari xs in
@@ -154,7 +154,10 @@ let check_rule : sym StrMap.t -> sym * pp_hint * rule Pos.loc -> unit =
       fatal r.pos "Unable to prove SR for rule [%a]." pp_rule (s,h,r.elt)
     end;
   (* Check that there is no uninstanciated metas left. *)
-  let rhs = Bindlib.msubst r.elt.rhs (Array.make binder_arity TE_None) in
-  if Basics.has_metas rhs then
-    fatal r.pos "Cannot instantiate all metavariables in rule [%a]."
-      pp_rule (s,h,r.elt)
+  let lhs_metas = Basics.get_metas false lhs in
+  let f m =
+    if not (List.in_sorted cmp_meta m lhs_metas) then
+      fatal r.pos "Cannot instantiate all metavariables in rule [%a]."
+        pp_rule (s,h,r.elt)
+  in
+  Basics.iter_meta false f rhs

src/tactics.ml

@@ -55,7 +55,7 @@ let handle_tactic : sig_state -> Proof.t -> p_tactic -> Proof.t =
     (* Instantiation. *)
     set_meta m (Bindlib.unbox (Bindlib.bind_mvar (Env.vars env) (lift t)));
     (* New subgoals and focus. *)
-    let metas = Basics.get_metas t in
+    let metas = Basics.get_metas true t in
     let new_goals = List.map Proof.Goal.of_meta metas in
     Proof.({ps with proof_goals = new_goals @ gs})
   in

src/terms.ml

@@ -240,8 +240,14 @@ 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
+
+(** Equality on metavariables. *)
+let eq_meta : meta -> meta -> bool = fun m1 m2 -> m1.meta_key = m2.meta_key
+
 (** [symb s] returns the term [Symb (s, Nothing)]. *)
-let symb s = Symb (s, Nothing)
+let symb : sym -> term = fun s -> Symb (s, Nothing)
 
 (** [is_injective s] tells whether the symbol is injective. *)
 let is_injective : sym -> bool = fun s -> s.sym_prop = Injec

src/why3_tactic.ml

@@ -168,7 +168,7 @@ let handle : Pos.popt -> Proof.proof_state -> sig_state -> string option ->
   (* Get the goal to prove. *)
   let (hyps, trm) = Proof.Goal.get_type g in
   (* Get the default or the indicated name of the prover. *)
-  let prover_name = Option.get prover_name !default_prover in
+  let prover_name = Option.get !default_prover prover_name in
   if !log_enabled then log_why3 "running with configuration [%s]" prover_name;
   (* Encode the goal in Why3. *)
   let tsk = encode pos ps.Proof.proof_builtins hyps trm in

tests/OK/301.lp

@@ -0,0 +1,7 @@
+constant symbol U : TYPE
+constant symbol u : U
+symbol Ux : U ⇒ TYPE
+rule Ux _ → U
+constant symbol hx : ∀ (x : U), (Ux x ⇒ U) ⇒ U
+symbol g : U ⇒ U
+rule g &i → hx &i (λ_, u)