Source file scope.ml

(** Scoping. Convert parsed terms in core terms by finding out which
   identifiers are bound variables or function symbol declared in open
   modules. *)

open Lplib
open Common open Error open Pos open Debug
open Syntax
open Core open Term open Env open Sig_state open Print

(** Logging function for term scoping. *)
let log_scop = Logger.make 'o' "scop" "term scoping"
let log_scop = log_scop.pp

(** [find_qid ~find_sym prt prv ss env qid] returns a boxed term corresponding
    to a variable of the environment [env] or a symbol which name corresponds
    to [qid]. In case of a qualified identifier, we search in symbols using
    [find_sym]. In case of an unqualified identifier, we first search in [env]
    and the in symbols using [find_sym]. The exception [Fatal] is raised if an
    error occurs (e.g. when the name cannot be found). If [prt] is true,
    protected symbols from external modules are allowed (protected symbols
    from current modules are always allowed). If [prv] is true, private
    symbols are allowed. *)
let find_qid :
      ?find_sym:find_sym -> bool -> bool -> sig_state -> env -> p_qident
      -> tbox =
  fun ?(find_sym = find_sym) prt prv ss env qid ->
  if Logger.log_enabled () then log_scop "find_qid %a" Pretty.qident qid;
  let (mp, s) = qid.elt in
  (* Check for variables in the environment first. *)
  try
    if mp <> [] then raise Not_found; (* Variables cannot be qualified. *)
    _Vari (Env.find s env)
  with Not_found ->
    (* Check for symbols. *)
    _Symb (find_sym ~prt ~prv ss qid)

(** Representation of the different scoping modes.  Note that the constructors
    hold specific information for the given mode. *)
type lhs_data =
  { m_lhs_prv              : bool
  (** True if private symbols are allowed. *)
  ; m_lhs_indices          : (string, int   ) Hashtbl.t
  (** Stores index reserved for a pattern variable of the given name. *)
  ; m_lhs_arities          : (int   , int   ) Hashtbl.t
  (** Stores the arity of the pattern variable at the given index. *)
  ; m_lhs_names            : (int   , string) Hashtbl.t
  (** Stores the name of the pattern variable at given index (if any). *)
  ; mutable m_lhs_size     : int
  (** Stores the current known size of the environment of the RHS. *)
  ; m_lhs_in_env           : string list
  (** Pattern variables definitely needed in the RHS environment. *) }

type mode =
  | M_Term of
      { m_term_meta_of_key : int -> meta option
      (** Allows to retrieve generated metas by their key. *)
      ; m_term_prv : bool
      (** Indicate if private symbols are allowed. *) }
  (** Standard scoping mode for terms, holding a map for metavariables
     introduced by the user, a map for metavariables generated by the system,
     and a boolean indicating whether private symbols are allowed. *)
  | M_Patt
  (** Scoping mode for patterns in the rewrite tactic. *)
  | M_LHS of lhs_data
  (** Scoping mode for rewriting rule left-hand sides. *)
  | M_SearchPatt of (int -> meta option) * lhs_data
  (** Scoping mode for search queries *)
  | M_RHS of
      { m_rhs_prv  : bool
      (** True if private symbols are allowed. *)
      ; m_rhs_data : (string, tevar) Hashtbl.t
      (** Environment for variables that we know to be bound in the RHS. *)
      ; mutable m_rhs_new_metas : problem
      (** Metavariables generated during scoping. *) }
  (** Scoping mode for rewriting rule right-hand sides. *)
  | M_URHS of
      { mutable m_urhs_vars_nb : int
      (** Number  of  distinct  variables  in  the rewriting  rule,  including
          variables  only in  the  RHS. It  is initialised  to  the number  of
          (distinct) variables in the LHS and incremented each time a variable
          of the RHS that was not in the LHS is scoped. *)
      ; mutable m_urhs_xvars : (string * tevar) list
      (** Variables scoped that  were not in the LHS. This  field is only used
          in  unification  rules and  is  updated  imperatively for  each  new
          variable scoped. A couple [(n, v)]  is the name of the variable with
          the variable itself. The name is needed to ensure that two variables
          with the same name are scoped as the same variable. *)
      ; m_urhs_data : (string, tevar) Hashtbl.t }
  (** Scoping mode for unification rule right-hand sides. During  scoping, we
      always have [m_urhs_vars_nb = m_lhs_size + length m_urhs_xvars]. *)

(** [scope_iden ~find_sym md ss env qid] calls [find_qid] with the [prt] and
    [prv] flags set according to [md]. *)
let scope_iden : ?find_sym:find_sym ->
  mode -> sig_state -> env -> p_qident -> tbox =
  fun ?find_sym md ss env qid ->
  let prt = match md with M_LHS _ | M_SearchPatt _ -> true | _ -> false
  and prv =
    match md with
    | M_SearchPatt _ -> true
    | M_LHS(d) -> d.m_lhs_prv
    | M_Term(d) -> d.m_term_prv
    | M_RHS(d) -> d.m_rhs_prv
    | _ -> false
  in
  find_qid ?find_sym prt prv ss env qid

(** [fresh_patt name ts] creates a unique pattern variable applied to
   [ts]. [name] is used as suffix if distinct from [None]. *)
let fresh_patt : lhs_data -> string option -> tbox array -> tbox =
  fun data nopt ts ->
  let fresh_index () =
    let i = data.m_lhs_size in
    data.m_lhs_size <- i + 1;
    let arity = Array.length ts in
    Hashtbl.add data.m_lhs_arities i arity; i
  in
  match nopt with
  | Some name ->
      let i =
        try Hashtbl.find data.m_lhs_indices name with Not_found ->
          let i = fresh_index () in
          Hashtbl.add data.m_lhs_indices name i;
          Hashtbl.add data.m_lhs_names i name; i
      in
      _Patt (Some i) (string_of_int i) ts
  | None ->
      let i = fresh_index () in
      _Patt (Some i) (string_of_int i) ts

(** [is_invalid_bindlib_id s] says whether [s] can be safely used as variable
   name in Bindlib. Indeed, because Bindlib converts any suffix consisting of
   a sequence of digits into an integer, and increment it, we cannot use as
   bound variable names escaped identifiers or regular identifiers ending with
   a non-negative integer with leading zeros. *)
let is_invalid_bindlib_id : string -> bool =
  let rec last_digit s k =
    let l = k-1 in
    if l < 0 then 0 else
      match s.[l] with
      | '0' .. '9' -> last_digit s l
      | _ -> k
  in
  fun s ->
    let n = String.length s - 1 in
    n >= 0 &&
    match s.[n] with
    | '0' .. '9' -> let k = last_digit s n in s.[k] = '0' && k < n
    | '}' -> true
    | _ -> false

(* unit tests *)
let _ =
  let invalid = is_invalid_bindlib_id in
  let valid s = not (invalid s) in
  assert (invalid "00");
  assert (invalid "01");
  assert (invalid "a01");
  assert (invalid "{|:|}");
  assert (valid "_x_100");
  assert (valid "_z1002");
  assert (valid "case_ex2_intro");
  assert (valid "case_ex02_intro");
  assert (valid "case_ex02_intro0");
  assert (valid "case_ex02_intro1");
  assert (valid "case_ex02_intro10")

(* used in desugaring decimal notations *)
let strint = Array.init 11 string_of_int

(** [scope ~find_sym ~typ k md ss env t] turns a parser-level term [t] into an
    actual term. *)
let rec scope : ?find_sym:find_sym ->
  ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> tbox =
  fun ?find_sym ?(typ=false) k md ss env t ->
  if Logger.log_enabled () then
    log_scop "%a before Pratt: %a" D.depth k Pretty.term t;
  let u = Pratt.parse ?find_sym ss env t in
  if Logger.log_enabled () then
    log_scop "%a after Pratt: %a" D.depth k Pretty.term u;
  scope_parsed ?find_sym ~typ k md ss env u

(** [scope_parsed ~find_sym ~typ k md ss env t] turns a parser-level
    Pratt-parsed term [t] into an actual term. *)
and scope_parsed : ?find_sym:find_sym ->
  ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> tbox =
  fun ?find_sym ?(typ=false) k md ss env t ->
  if Logger.log_enabled () then log_scop "%a%a" D.depth k Pretty.term t;
  (* Extract the spine. *)
  let p_head, args = Syntax.p_get_args t in
  (* Check that LHS pattern variables are applied to no argument. *)
  begin
    match p_head.elt, md with
    | P_Patt _, M_LHS _ when args <> [] ->
      begin match args with
        | [{elt=P_Expl _;_}] ->
          fatal t.pos "Explicit terms are forbidden in rule LHS. \
                       You perhaps forgot to write a dot before?"
        | _ -> fatal t.pos "Pattern variables cannot be applied."
      end
    | _ -> ()
  end;
  (* Scope the head and obtain the implicitness of arguments. *)
  let h = scope_head ?find_sym ~typ k md ss env p_head in
  (* Find out whether [h] has implicit arguments. *)
  let rec get_impl p_head =
    match p_head.elt with
    | P_Wrap e -> get_impl e
    | P_Iden (_, false) ->
        (* We avoid unboxing if [h] is not closed (and hence not a symbol). *)
        if Bindlib.is_closed h then
          match Bindlib.unbox h with
          | Symb s -> s.sym_impl
          | _ -> []
        else []
    | P_Abst (params_list, t) ->
      Syntax.get_impl_params_list params_list @ get_impl t
    | _ -> []
  in
  let impl =
    match p_head.elt, args with
    | P_Abst _, [] -> []
    | _ -> minimize_impl (get_impl p_head)
  in
  (* Scope and insert the (implicit) arguments. *)
  add_impl ?find_sym k md ss env t.pos h impl args
  |> D.log_and_return
    (fun e -> log_scop "%agot %a" D.depth k Raw.term (Bindlib.unbox e))

(** [add_impl ~find_sym k md ss env loc h impl args] scopes [args] and returns
    the application of [h] to the scoped arguments. [impl] is a boolean list
    described the implicit arguments. Implicit arguments are added as
    underscores before scoping. *)
and add_impl : ?find_sym:find_sym -> int -> mode -> sig_state ->
               Env.t -> popt -> tbox -> bool list -> p_term list -> tbox =
  fun ?find_sym k md ss env loc h impl args ->
  let appl =
   match md with
      M_LHS _ | M_SearchPatt _ -> _Appl_not_canonical
    | _ -> _Appl in
  let appl_p_term t u = appl t (scope_parsed ?find_sym (k+1) md ss env u) in
  let appl_meta t = appl t (scope_head ?find_sym (k+1) md ss env P.wild) in
  match impl, args with
  (* The remaining arguments are all explicit. *)
  | [], _ -> List.fold_left appl_p_term h args
  (* Only implicit arguments remain. *)
  | true::impl, [] -> add_impl ?find_sym k md ss env loc (appl_meta h) impl []
  (* The first argument is implicit (could be [a] if made explicit). *)
  | true::impl, a::args ->
      begin match a.elt with
      | P_Expl b ->
          add_impl ?find_sym k md ss env loc
            (appl_p_term h {a with elt = P_Wrap b}) impl args
      | _ -> add_impl ?find_sym k md ss env loc (appl_meta h) impl (a::args)
      end
  (* The first argument [a] is explicit. *)
  | false::impl, a::args ->
      begin match a.elt with
      | P_Expl _ -> fatal a.pos "Unexpected explicit argument."
      | _ -> add_impl ?find_sym k md ss env loc (appl_p_term h a) impl args
      end
  (* The application is too "partial" to insert all implicit arguments. *)
  | false::_, [] ->
      (* NOTE this could be improved with more general implicits. *)
      fatal loc "More arguments are required to instantiate implicits."

(** [scope_domain ~find_sym k md ss env t] scopes [t] as the domain of an
    abstraction or product. *)
and scope_domain : ?find_sym:find_sym ->
  int -> mode -> sig_state -> env -> p_term option -> tbox =
  fun ?find_sym k md ss env a ->
  match a, md with
  | (Some {elt=P_Wild;_}|None), (M_LHS data | M_SearchPatt (_,data)) ->
      fresh_patt data None (Env.to_tbox env)
  | (Some {elt=P_Wild;_}|None), _ -> _Plac true
  | Some a, _ -> scope ?find_sym ~typ:true k md ss env a

(** [scope_binder ~find_sym ~typ k md ss cons env params_list t] scopes [t],
    abstract [params_list] and returns a tbox using [cons] (either [_Abst] or
    [_Prod]). *)
and scope_binder :
      ?find_sym:find_sym -> ?typ:bool -> int -> mode -> sig_state ->
      (tbox -> tbinder Bindlib.box -> tbox) -> Env.t -> p_params list ->
      p_term option -> tbox =
  fun ?find_sym ?(typ=false) k md ss cons env params_list t ->
  (* [n] is used to give different names to parameters of the form "_" *)
  let rec scope_params_list n env params_list =
    match params_list with
    | [] ->
        begin
          match t with
          | Some t -> scope ?find_sym ~typ (k+1) md ss env t
          | None -> _Plac true
        end
    | (idopts,typopt,_implicit)::params_list ->
      let dom = scope_domain ?find_sym (k+1) md ss env typopt in
      scope_params n env idopts dom params_list
  and scope_params n env idopts a params_list =
    let rec aux n env idopts =
      match idopts with
      | [] -> scope_params_list n env params_list
      | None::idopts ->
          let v = if n = 0 then new_tvar "_" else new_tvar_ind "_" n in
          let t = aux (n+1) env idopts in
          cons a (Bindlib.bind_var v t)
      | Some {elt=id;pos}::idopts ->
          if is_invalid_bindlib_id id then
            fatal pos "\"%s\": Escaped identifiers or regular identifiers \
                       having an integer suffix with leading zeros \
                       are not allowed for bound variable names." id;
          let v = new_tvar id in
          let env = Env.add v a None env in
          let t = aux n env idopts in
          cons a (Bindlib.bind_var v t)
    in aux n env idopts
  in
  scope_params_list 0 env params_list

(** [scope_head ~find_sym ~typ k md ss env t] scopes [t] as term head. *)
and scope_head : ?find_sym:find_sym ->
  ?typ:bool -> int -> mode -> sig_state -> env -> p_term -> tbox =
  fun ?find_sym ?(typ=false) k md ss env t ->
  match (t.elt, md) with
  | (P_Type, _) -> _Type

  | (P_Iden(qid,_), _) -> scope_iden ?find_sym md ss env qid

  | (P_NLit(s), _) ->
      let neg, s =
        let neg = s.[0] = '-' in
        let s = if neg then String.sub s 1 (String.length s - 1) else s in
        neg, s
      in
      let sym_of s = _Symb (Builtin.get ss t.pos s) in
      let sym = Array.map sym_of strint in
      let digit = function
        | '0' -> sym.(0) | '1' -> sym.(1) | '2' -> sym.(2) | '3' -> sym.(3)
        | '4' -> sym.(4) | '5' -> sym.(5) | '6' -> sym.(6) | '7' -> sym.(7)
        | '8' -> sym.(8) | '9' -> sym.(9) | _ -> assert false
      in
      let sym_add = sym_of "+" in
      let add x y = _Appl (_Appl sym_add x) y in
      let sym_mul = sym_of "*" in
      let mul x y = _Appl (_Appl sym_mul x) y in
      let rec unsugar i =
        if i <= 0 then digit s.[0]
        else add (digit s.[i]) (mul sym.(10) (unsugar (i-1)))
      in
      let n = unsugar (String.length s - 1) in
      if neg then _Appl (sym_of "-") n else n

  | (P_Wild, M_URHS(data)) ->
    let x =
      let name = string_of_int data.m_urhs_vars_nb in
      let x = new_tevar name in
      data.m_urhs_vars_nb <- data.m_urhs_vars_nb + 1;
      data.m_urhs_xvars <- (name, x) :: data.m_urhs_xvars;
      x
    in
    _TEnv (_TE_Vari x) (Env.to_tbox env)
  | (P_Wild, (M_LHS data | M_SearchPatt (_,data))) ->
      fresh_patt data None (Env.to_tbox env)
  | (P_Wild, M_Patt) -> _Wild
  | (P_Wild, (M_RHS _|M_Term _)) -> _Plac typ

  | (P_Meta({elt;pos} as mk,ts),
    (M_Term {m_term_meta_of_key;_} | M_SearchPatt(m_term_meta_of_key,_))) -> (
      match m_term_meta_of_key elt with
      | None ->
          fatal pos "Metavariable %a not found among generated variables: \
                     metavariables can only be created by the system."
            Pretty.meta_ident mk
      | Some m -> _Meta m (Array.map (scope ?find_sym (k + 1) md ss env) ts))
  | (P_Meta(_), _) -> fatal t.pos "Metavariables are not allowed here."

  | (P_Patt(id,ts), (M_LHS(d) | M_SearchPatt(_,d))) ->
      (* Check that [ts] are variables. *)
      let scope_var t =
        match unfold (Bindlib.unbox (scope ?find_sym (k+1) md ss env t)) with
        | Vari(x) -> x
        | _       -> fatal t.pos "Only bound variables are allowed in the \
                                  environment of pattern variables."
      in
      let ts =
        match ts with
        | None ->
            if env = [] then [||] (* $M stands for $M[] *)
            else fatal t.pos "Missing square brackets under binder."
        | Some ts ->
            let vs = Array.map scope_var ts in
            (* Check that [vs] are distinct variables. *)
            for i = 0 to Array.length vs - 2 do
              for j = i + 1 to Array.length vs - 1 do
                if Bindlib.eq_vars vs.(i) vs.(j) then
                  fatal ts.(j).pos
                    "Variable %a appears more than once \
                     in the environment of a pattern variable."
                    var vs.(j)
              done
            done;
            Array.map _Vari vs
      in
      begin
        match id with
        | None when List.length env = Array.length ts ->
            wrn t.pos
              "Pattern [%a] could be replaced by [_]." Pretty.term t;
        | Some {elt=id;pos} when not (List.mem id d.m_lhs_in_env) ->
            if List.length env = Array.length ts then
              wrn pos "Pattern variable %s can be replaced by a '_'." id
            else wrn pos "Pattern variable %s doesn't need to be named." id
        | _ -> ()
      end;
      fresh_patt d (Option.map (fun id -> id.elt) id) ts
  | (P_Patt(id,ts), M_URHS(r)) ->
      let x =
        match id with
        | None ->
            fatal t.pos "Wildcard pattern not allowed in the right \
                         hand-side of a unification rule."
        | Some {elt=id;_} ->
            (* Search in variables declared in LHS. *)
            try Hashtbl.find r.m_urhs_data id
            with Not_found ->
              (* Search in variables already declared in RHS. *)
              try List.assoc id r.m_urhs_xvars
              with Not_found ->
                let name = string_of_int r.m_urhs_vars_nb in
                let x = new_tevar name in
                r.m_urhs_vars_nb <- r.m_urhs_vars_nb + 1;
                r.m_urhs_xvars   <- (id, x) :: r.m_urhs_xvars;
                x
      in
      let ts =
        match ts with
        | None -> [||] (* $M stands for $M[] *)
        | Some ts -> Array.map (scope ?find_sym (k+1) md ss env) ts
      in
      _TEnv (_TE_Vari x) ts
  | (P_Patt(id,ts), M_RHS(r)) ->
      let x =
        match id with
        | None     -> fatal t.pos "Wildcard pattern not allowed in a RHS."
        | Some(id) ->
            (* Search in variables declared in LHS. *)
            try Hashtbl.find r.m_rhs_data id.elt
            with Not_found -> fatal t.pos "Variable must be in LHS."
      in
      let ts =
        match ts with
        | None -> [||] (* $M stands for $M[] *)
        | Some ts -> Array.map (scope ?find_sym (k+1) md ss env) ts
      in
      _TEnv (_TE_Vari x) ts
  | (P_Patt(_,_), _) ->
      fatal t.pos "Pattern variables are only allowed in rewriting rules."

  | (P_Appl(_,_), _) ->  assert false (* Unreachable. *)

  | (P_Arro(_,_), M_Patt) ->
      fatal t.pos "Arrows are not allowed in patterns."
  | (P_Arro(a,b), _) ->
    _Impl (scope ?find_sym ~typ:true (k+1) md ss env a)
          (scope ?find_sym ~typ:true (k+1) md ss env b)

  | (P_Abst(_,_), M_Patt) ->
      fatal t.pos "Abstractions are not allowed in patterns."
  | (P_Abst(xs,t), _) -> scope_binder ?find_sym k md ss _Abst env xs (Some(t))

  | (P_Prod(_,_), M_Patt) ->
      fatal t.pos "Dependent products are not allowed in patterns."
  | (P_Prod(xs,b), _) ->
      scope_binder ?find_sym ~typ:true k md ss _Prod env xs (Some b)

  | (P_LLet(x,xs,a,t,u), (M_Term _|M_URHS _|M_RHS _|M_SearchPatt _)) ->
      let a = scope_binder ?find_sym ~typ:true (k+1) md ss _Prod env xs a in
      let t = scope_binder ?find_sym (k+1) md ss _Abst env xs (Some(t)) in
      let v = new_tvar x.elt in
      let u = scope ?find_sym ~typ (k+1) md ss (Env.add v a (Some t) env) u in
      if not (Bindlib.occur v u) then
        wrn x.pos "Useless let-binding (%s is not bound)." x.elt;
      _LLet a t (Bindlib.bind_var v u)
  | (P_LLet(_), M_LHS(_)) ->
      fatal t.pos "Let-bindings are not allowed in a LHS."
  | (P_LLet(_), M_Patt) ->
      fatal t.pos "Let-bindings are not allowed in patterns."

  (* Evade the addition of implicit arguments inside the wrap *)
  | (P_Wrap ({ elt = (P_Iden _ | P_Abst _); _ } as id), _) ->
    scope_head ?find_sym ~typ (k+1) md ss env id
  | (P_Wrap t, _) -> scope ?find_sym ~typ (k+1) md ss env t

  | (P_Expl(_), _) -> fatal t.pos "Explicit argument not allowed here."

let scope =
  let open Stdlib in
  let r = ref _Kind in
  fun ?find_sym ?(typ=false) k md ss env t ->
  Debug.(record_time Scoping
           (fun () -> r := scope ?find_sym ~typ k md ss env t)); !r

(** [scope_term ~find_sym ~typ ~mok prv ss env t] scopes [t] in mode [M_Term]
    with [m_term_prv] set to [prv], and [m_term_meta_of_key] set to [mok]
    (which defaults to the constant function equal to [None]). *)
let scope_term :
      ?find_sym:find_sym -> ?typ:bool -> ?mok:(int -> meta option)
      -> bool -> sig_state -> env -> p_term -> term =
  fun ?find_sym ?(typ=false) ?(mok=fun _ -> None) m_term_prv ss env t ->
  let md = M_Term {m_term_meta_of_key=mok; m_term_prv} in
  Bindlib.unbox (scope ?find_sym ~typ 0 md ss env t)

(** [scope_search_pattern ~find_sym ~typ prv ss env t] scopes [t] in mode
    [M_SearchPatt] with [m_term_meta_of_key] set to [mok] (which defaults to
    the constant function equal to [None]). *)
let scope_search_pattern : ?find_sym:find_sym -> ?typ:bool ->
  ?mok:(int -> meta option) -> sig_state -> env -> p_term -> term =
  fun ?find_sym ?(typ=false) ?(mok=fun _ -> None) ss env t ->
  let md =
   M_SearchPatt(mok,{m_lhs_prv = true
    ; m_lhs_indices = Hashtbl.create 7
    ; m_lhs_arities = Hashtbl.create 7
    ; m_lhs_names   = Hashtbl.create 7
    ; m_lhs_size    = 0
    ; m_lhs_in_env  = [] }) in
  Bindlib.unbox (scope ?find_sym ~typ 0 md ss env t)

(** [patt_vars t] returns a couple [(pvs,nl)]. The first compoment [pvs] is an
    association list giving the arity of all the “pattern variables” appearing
    in the parser-level term [t]. The second component [nl] contains the names
    of the “pattern variables” that appear non-linearly.  If a given  “pattern
    variable” occurs with different arities the program fails gracefully. *)
let patt_vars : p_term -> (string * int) list * string list =
  let rec patt_vars acc t =
    match t.elt with
    | P_Type             -> acc
    | P_Iden(_)          -> acc
    | P_Wild             -> acc
    | P_Meta(_,ts)       -> Array.fold_left patt_vars acc ts
    | P_Patt(id,ts)      -> add_patt acc id ts
    | P_Appl(t,u)        -> patt_vars (patt_vars acc t) u
    | P_Arro(a,b)        -> patt_vars (patt_vars acc a) b
    | P_Abst(args,t)     -> patt_vars (patt_vars_args acc args) t
    | P_Prod(args,b)     -> patt_vars (patt_vars_args acc args) b
    | P_LLet(_,args,a,t,u) ->
        let pvs = patt_vars (patt_vars (patt_vars_args acc args) t) u in
        begin
          match a with
          | None    -> pvs
          | Some(a) -> patt_vars pvs a
        end
    | P_NLit(_)          -> acc
    | P_Wrap(t)          -> patt_vars acc t
    | P_Expl(t)          -> patt_vars acc t
  and add_patt ((pvs, nl) as acc) id ts =
    let acc, arity =
      match ts with
      | None     -> (acc, 0)
      | Some(ts) -> (Array.fold_left patt_vars acc ts, Array.length ts)
    in
    match id with
    | None     -> acc
    | Some {elt=id;pos} ->
        begin
          try
            if List.assoc id pvs <> arity then
              fatal pos "Arity mismatch for pattern variable %s." id;
            if List.mem id nl then acc else (pvs, id::nl)
          with Not_found -> ((id, arity)::pvs, nl)
        end
  and patt_vars_args acc args =
    match args with
    | []            -> acc
    | (_,a,_)::args ->
        let acc = match a with None -> acc | Some a -> patt_vars acc a in
        patt_vars_args acc args
  in
  patt_vars ([],[])

(** Representation of a rewriting rule prior to SR-checking. *)
type pre_rule =
  { pr_sym      : sym
  (** Head symbol of the LHS. *)
  ; pr_lhs      : term list
  (** Arguments of the LHS. *)
  ; pr_vars     : term_env Bindlib.mvar
  (** Pattern variables that appear in the RHS. The last [pr_xvars_nb]
      variables do not appear in the LHS. *)
  ; pr_rhs      : tbox
  (** Body of the RHS, should only be unboxed once. *)
  ; pr_names    : (int, string) Hashtbl.t
  (** Gives the original name (if any) of pattern variable at given index. *)
  ; pr_arities  : int array
  (** Gives the arity of all the pattern variables in field [pr_vars]. *)
  ; pr_xvars_nb : int
  (** Number of variables that appear in the RHS but not in the LHS. *) }

(** [rule_of_pre_rule r] converts a pre-rewrite rule into a rewrite rule. *)
let rule_of_pre_rule : pre_rule loc -> rule =
  fun { elt = pr; pos = rule_pos } ->
  let {pr_lhs; pr_vars; pr_rhs; pr_arities; pr_xvars_nb; _} = pr in
  { lhs = pr_lhs
  ; rhs = Bindlib.(unbox (bind_mvar pr_vars pr_rhs))
  ; arity = List.length pr_lhs
  ; arities = pr_arities
  ; vars = pr_vars
  ; xvars_nb = pr_xvars_nb
  ; rule_pos }

(** [scope_rule ~find_sym ur ss r] turns a parser-level rewriting rule [r],
    or a unification rule if [ur] is true, into a pre-rewriting rule. *)
let scope_rule :
  ?find_sym:find_sym -> bool -> sig_state -> p_rule -> pre_rule loc =
  fun ?(find_sym=Sig_state.find_sym) ur ss { elt = (p_lhs, p_rhs); pos } ->
  (* Compute the set of pattern variables on both sides. *)
  let (pvs_lhs, nl) = patt_vars p_lhs in
  (* NOTE to reject non-left-linear rules check [nl = []] here. *)
  let (pvs_rhs, _ ) = patt_vars p_rhs in
  (* Check that pattern variables of RHS that are in the LHS have the right
     arity. *)
  let check_arity (m,i) =
    try
      let j = List.assoc m pvs_lhs in
      if i <> j then fatal p_lhs.pos "Arity mismatch for %s." m
    with Not_found -> ()
  in
  List.iter check_arity pvs_rhs;
  (* [get_root t] returns the symbol at the root of the p_term [t]. *)
  let rec get_root t = get_root_after_pratt (Pratt.parse ~find_sym ss [] t)
  and get_root_after_pratt t =
    match t.elt with
    | P_Iden(qid,_) -> find_sym ~prt:true ~prv:true ss qid
    | P_Appl(t, _) -> get_root_after_pratt t
    | P_Wrap(t) -> get_root t
    | _ ->
      fatal p_lhs.pos "Rule left hand-side not headed by a function symbol."
  in
  (* Check that the LHS is headed by a function symbol that is definable and
     not protected. *)
  let pr_sym = get_root p_lhs in
  if is_constant pr_sym then
    fatal p_lhs.pos
      "Symbol %s has been declared constant, it cannot be used as the \
       head of a rewrite rule LHS." pr_sym.sym_name;
  if Timed.(!(pr_sym.sym_opaq) || (!(pr_sym.sym_def) <> None)) then
    fatal p_lhs.pos "No rewriting rule can be added on an opaque symbol \
                     or a symbol already defined with ≔";
  if pr_sym.sym_expo = Protec
    && ss.signature.sign_path <> pr_sym.sym_path then
    fatal p_lhs.pos "Cannot define rules on foreign protected symbols.";
  (* Scope the LHS and get the reserved index for named pattern variables. *)
  let (pr_lhs, lhs_indices, lhs_arities, pr_names, lhs_size) =
    let mode =
      M_LHS{ m_lhs_prv     = is_private pr_sym
           ; m_lhs_indices = Hashtbl.create 7
           ; m_lhs_arities = Hashtbl.create 7
           ; m_lhs_names   = Hashtbl.create 7
           ; m_lhs_size    = 0
           ; m_lhs_in_env  = nl @ List.map fst pvs_rhs }
    in
    let pr_lhs = scope ~find_sym 0 mode ss Env.empty p_lhs in
    match mode with
    | M_LHS{ m_lhs_indices; m_lhs_names; m_lhs_size; m_lhs_arities; _} ->
      let pr_lhs = snd (get_args (Bindlib.unbox pr_lhs)) in
      (pr_lhs, m_lhs_indices, m_lhs_arities, m_lhs_names, m_lhs_size)
    | _ -> assert false
  in
  (* Create the pattern variables that can be bound in the RHS. *)
  let pr_vars =
    Array.init lhs_size (fun i -> new_tevar (string_of_int i)) in
  let mode =
    let htbl_vars = Hashtbl.create (Hashtbl.length lhs_indices) in
    let fn k i = Hashtbl.add htbl_vars k pr_vars.(i) in
    Hashtbl.iter fn lhs_indices;
    if ur then
      M_URHS{ m_urhs_data = htbl_vars ; m_urhs_vars_nb = Array.length pr_vars
            ; m_urhs_xvars = [] }
    else
      M_RHS{ m_rhs_prv = is_private pr_sym; m_rhs_data = htbl_vars;
             m_rhs_new_metas = new_problem() }
  in
  let pr_rhs = scope ~find_sym 0 mode ss Env.empty p_rhs in
  let prerule =
    (* We put everything together to build the pre-rule. *)
    let pr_arities =
      let f i =
        try Hashtbl.find lhs_arities i
        with Not_found -> assert false (* Unreachable. *)
      in
      Array.init lhs_size f
    in
    if ur then (* Unification rule. *)
      (* We scope the RHS and retrieve variables not occurring in the LHS. *)
      let xvars =
        match mode with
        | M_URHS{m_urhs_xvars;_} -> m_urhs_xvars
        | _ -> assert false (* Guarded by the [if ur] *)
      in
      (* Add RHS-only variables to [pr_vars] and get index of the first
         one. *)
      let (pr_vars, pr_xvars_nb) =
        (* If there is no variable introduced in RHS, do nothing (typically
           while scoping regular rewriting rules.) *)
        if Stdlib.(xvars = []) then (pr_vars, 0) else
        let xvars = Array.of_list (List.map snd xvars) in
        (Array.append pr_vars xvars, Array.length xvars)
      in
      (* We put everything together to build the pre-rule. *)
      { pr_sym ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities
      ; pr_names ; pr_xvars_nb }
    else (* Rewrite rule. *)
      { pr_sym ; pr_lhs ; pr_vars ; pr_rhs ; pr_arities
      ; pr_names ; pr_xvars_nb=0 }
  in
  Pos.make pos prerule

(** [scope_pattern ss env t] turns a parser-level term [t] into an actual term
    in mode [M_Patt], i.e. as a selection pattern in a rewrite tactic. *)
let scope_pattern : sig_state -> env -> p_term -> term = fun ss env t ->
  Bindlib.unbox (scope 0 M_Patt ss env t)

(** [scope_rw_patt ss env s] scopes the parser-level rewrite tactic
    specification [s] into an actual rewrite specification. *)
let scope_rw_patt : sig_state -> env -> p_rw_patt -> (term, tbinder) rw_patt =
  fun ss env s ->
  match s.elt with
  | Rw_Term(t) -> Rw_Term(scope_pattern ss env t)
  | Rw_InTerm(t) -> Rw_InTerm(scope_pattern ss env t)
  | Rw_InIdInTerm(x,t) ->
      let v = new_tvar x.elt in
      let t = scope_pattern ss ((x.elt,(v, _Kind, None))::env) t in
      Rw_InIdInTerm(bind v lift_not_canonical t)
  | Rw_IdInTerm(x,t) ->
      let v = new_tvar x.elt in
      let t = scope_pattern ss ((x.elt,(v, _Kind, None))::env) t in
      Rw_IdInTerm(bind v lift_not_canonical t)
  | Rw_TermInIdInTerm(u,(x,t)) ->
      let u = scope_pattern ss env u in
      let v = new_tvar x.elt in
      let t = scope_pattern ss ((x.elt,(v, _Kind, None))::env) t in
      Rw_TermInIdInTerm(u, bind v lift_not_canonical t)
  | Rw_TermAsIdInTerm(u,(x,t)) ->
      let u = scope_pattern ss env u in
      let v = new_tvar x.elt in
      let t = scope_pattern ss ((x.elt,(v, _Kind, None))::env) t in
      Rw_TermAsIdInTerm(u, bind v lift_not_canonical t)