Source file command.ml

(** Handling of commands. *)

open Lplib open Base open Extra
open Timed
open Common open Error open Pos
open Core open Term open Sign open Sig_state open Print
open Parsing open Syntax open Scope
open Proof

(** Type alias for a function that compiles a Lambdapi module. *)
type compiler = Path.t -> Sign.t

(** Register a check for the type of the builtin symbols "0" and "+1". *)
let _ =
  (* [eq_noexn t u] tries to unify the terms [t] and [u]. *)
  let eq_noexn : term -> term -> bool = fun t u ->
    let p = new_problem() in p := {!p with to_solve = [[], t, u]};
    Unif.solve_noexn p && !p.unsolved = [] && !p.metas = MetaSet.empty
  in
  let register = Builtin.register_expected_type eq_noexn term in
  let expected_zero_type ss _pos =
    try
      match !((StrMap.find "+1" ss.builtins).sym_type) with
      | Prod(a,_) -> a
      | _ -> assert false
    with Not_found -> mk_Meta (LibMeta.fresh (new_problem()) mk_Type 0, [||])
  in
  register "0" expected_zero_type;
  let expected_succ_type ss _pos =
    let typ_0 =
      try lift !((StrMap.find "0" ss.builtins).sym_type)
      with Not_found -> _Meta (LibMeta.fresh (new_problem()) mk_Type 0) [||]
    in
    Bindlib.unbox (_Impl typ_0 typ_0)
  in
  register "+1" expected_succ_type

(** [handle_open ss p] handles the command [open p] with [ss] as the
   signature state. On success, an updated signature state is returned. *)
let handle_open : sig_state -> p_path -> sig_state =
  fun ss {elt=p;pos} ->
  (* Check that [p] is not an alias. *)
  match p with
  | [a] when StrMap.mem a ss.alias_path ->
    fatal pos "Module aliases cannot be open."
  | _ ->
  (* Check that [p] has been required. *)
  if not (Path.Map.mem p !(ss.signature.sign_deps)) then
    fatal pos "Module %a needs to be required first." path p;
  (* Obtain the signature corresponding to [p]. *)
  open_sign ss (Path.Map.find p !(Sign.loaded))

(** [handle_require b ss p] handles the command [require p] (or [require
   open p] if b is true) with [ss] as the signature state and [compile] the
   main compile function (passed as argument to avoid cyclic dependencies).
   On success, an updated signature state is returned. *)
let handle_require : compiler -> bool -> sig_state -> p_path -> sig_state =
  fun compile b ss {elt=p;pos} ->
  (* Check that the module has not already been required. *)
  if Path.Map.mem p !(ss.signature.sign_deps) then
    fatal pos "Module %a is already required." path p;
  (* Compile required path (adds it to [Sign.loaded] among other things) *)
  ignore (compile p);
  (* Add the dependency (it was compiled already while parsing). *)
  ss.signature.sign_deps
    := Path.Map.add p StrMap.empty !(ss.signature.sign_deps);
  if b then open_sign ss (Path.Map.find p !(Sign.loaded)) else ss

(** [handle_require_as compile ss p id] handles the command
    [require p as id] with [ss] as the signature state and [compile] the main
    compilation function passed as argument to avoid cyclic dependencies. On
    success, an updated signature state is returned. *)
let handle_require_as : compiler -> sig_state -> p_path -> p_ident ->
  sig_state =
  fun compile ss ({elt=p;_} as mp) {elt=id;_} ->
  let ss = handle_require compile false ss mp in
  let alias_path = StrMap.add id p ss.alias_path in
  let path_alias = Path.Map.add p id ss.path_alias in
  {ss with alias_path; path_alias}

(** [handle_modifiers ms] verifies that the modifiers in [ms] are compatible.
    If so, they are returned as a tuple. Otherwise, it fails. *)
let handle_modifiers : p_modifier list -> prop * expo * match_strat =
  fun ms ->
  let rec get_modifiers ((props, expos, strats) as acc) = function
    | [] -> acc
    | {elt=P_prop _;_} as p::ms -> get_modifiers (p::props, expos, strats) ms
    | {elt=P_expo _;_} as e::ms -> get_modifiers (props, e::expos, strats) ms
    | {elt=P_mstrat _;_} as s::ms ->
        get_modifiers (props, expos, s::strats) ms
    | {elt=P_opaq;_}::ms -> get_modifiers acc ms
  in
  let props, expos, strats = get_modifiers ([],[],[]) ms in
  let prop =
    match props with
    | [{elt=P_prop (Assoc b);_};{elt=P_prop Commu;_}]
    | [{elt=P_prop Commu;_};{elt=P_prop (Assoc b);_}] -> AC b
    | _::{pos;_}::_ -> fatal pos "Incompatible or duplicated properties."
    | [{elt=P_prop (Assoc _);pos}] ->
        fatal pos "Associativity alone is not allowed as \
                   you can use a rewriting rule instead."
    | [{elt=P_prop p;_}] -> p
    | [] -> Defin
    | _ -> assert false
  in
  let expo =
    match expos with
    | _::{pos;_}::_ ->
        fatal pos "Incompatible or duplicated exposition markers."
    | [{elt=P_expo e;_}] -> e
    | [] -> Public
    | _ -> assert false
  in
  let strat =
    match strats with
    | _::{pos;_}::_ ->
        fatal pos "Incompatible or duplicated matching strategies."
    | [{elt=P_mstrat s;_}] -> s
    | [] -> Eager
    | _ -> assert false
  in
  (prop, expo, strat)

(** [sr_check] indicates whether subject-reduction should be checked. *)
let sr_check = Stdlib.ref true

(** [check_rule ss syms r] checks rule [r] and returns the head symbol of the
   lhs and the rule itself. *)
let check_rule : sig_state -> p_rule -> sym_rule = fun ss r ->
  Console.out 3 (Color.cya "%a") Pos.pp r.pos;
  Console.out 4 "%a" (Pretty.rule "rule") r;
  let pr = scope_rule false ss r in
  let s = pr.elt.pr_sym in
  if !(s.sym_def) <> None then
    fatal pr.pos "No rewriting rule can be given on a defined symbol.";
  let r =
    if Stdlib.(!sr_check) then Tool.Sr.check_rule pr
    else Scope.rule_of_pre_rule pr
  in
  s, r

(** [add_rule ss syms r] checks rule [r], adds it in [ss] and returns the
   head symbol of the lhs and the rule itself. *)
let add_rule : sig_state -> sym_rule -> unit = fun ss ((s,r) as x) ->
  Sign.add_rule ss.signature s r;
  Console.out 2 (Color.red "rule %a") sym_rule x

(** [handle_inductive_symbol ss e p strat x declpos xs a] handles the command
    [e p strat symbol x xs : a] with [ss] as the signature state.
    The command is at position [pos].
    On success, an updated signature state and the new symbol are returned. *)
let handle_inductive_symbol : sig_state -> expo -> prop -> match_strat
    -> p_ident -> popt -> p_params list -> p_term -> sig_state * sym =
  fun ss expo prop mstrat ({elt=name;pos} as id) declpos xs typ ->
  (* We check that [id] is not already used. *)
  if Sign.mem ss.signature name then
    fatal pos "Symbol %a already exists." uid name;
  (* Desugaring of arguments of [typ]. *)
  let typ = if xs = [] then typ else Pos.none (P_Prod(xs, typ)) in
  (* Obtaining the implicitness of arguments. *)
  let impl = Syntax.get_impl_term typ in
  (* We scope the type of the declaration. *)
  let p = new_problem() in
  let typ = scope_term ~typ:true (expo = Privat) ss Env.empty typ in
  (* We check that [typ] is typable by a sort. *)
  let (typ,  _) = Query.check_sort pos p [] typ in
  (* We check that no metavariable remains. *)
  if !p.metas <> MetaSet.empty then begin
    fatal_msg "The type of %a has unsolved metavariables.@." uid name;
    fatal pos "We have %a : %a." uid name term typ
  end;
  (* Actually add the symbol to the signature and the state. *)
  Console.out 2 (Color.red "symbol %a : %a") uid name term typ;
  let r =
   Sig_state.add_symbol ss expo prop mstrat false id declpos typ impl None in
  sig_state := fst r; r

(** Representation of a yet unchecked proof. The structure is initialized when
    the proof mode is entered, and its finalizer is called when the proof mode
    is exited (i.e., when a terminator like “end” is used).  Note that tactics
    do not work on this structure directly,  although they act on the contents
    of its [pdata_state] field. *)
type proof_data =
  { pdata_sym_pos  : Pos.popt (** Position of the declared symbol. *)
  ; pdata_state    : proof_state (** Proof state. *)
  ; pdata_proof    : p_proof (** Proof. *)
  ; pdata_finalize : sig_state -> proof_state -> sig_state (** Finalizer. *)
  ; pdata_end_pos  : Pos.popt (** Position of the proof's terminator. *)
  ; pdata_prv      : bool (** [true] iff private symbols are allowed. *) }

(** Representation of a command output. *)
type cmd_output = sig_state * proof_data option * Query.result

(** [get_proof_data compile ss cmd] tries to handle the command [cmd] with
    [ss] as the signature state and [compile] as the main compilation function
    processing lambdapi modules (it is passed as argument to avoid cyclic
    dependencies). On success, an updated signature state is returned.  When
    [cmd] leads to entering the proof mode,  a [proof_data] is also  returned.
    This structure contains the list of the tactics to be executed, as well as
    the initial state of the proof.  The checking of the proof is then handled
    separately. Note that [Fatal] is raised in case of an error. *)
let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
  fun compile ss ({elt; pos} as cmd) ->
  Console.out 3 (Color.cya "%a") Pos.pp pos;
  Console.out 4 "%a" Pretty.command cmd;
  match elt with
  | P_opaque qid ->
    let s = Sig_state.find_sym ~prt:true ~prv:true ss qid in
    if !(s.sym_opaq) then fatal pos "Symbol already opaque.";
    s.sym_opaq := true;
    (ss, None, None)
  | P_query(q) -> (ss, None, Query.handle ss None q)
  | P_require(b,ps) ->
      (List.fold_left (handle_require compile b) ss ps, None, None)
  | P_require_as(p,id) -> (handle_require_as compile ss p id, None, None)
  | P_open(ps) -> (List.fold_left handle_open ss ps, None, None)
  | P_rules(rs) ->
    (* Scope rules, and check that they preserve typing. Return the list of
       rules [srs] and also a map [map] mapping every symbol defined by a rule
       of [srs] to its defining rules. *)
      let handle_rule r (srs, map) =
        let (s,r) as sr = check_rule ss r in
        let h = function Some rs -> Some(r::rs) | None -> Some[r] in
        sr::srs, SymMap.update s h map
      in
      (* The order of rules must be kept between [rs] and [srs].
         That is, the following assertion should hold
         [assert (srs = List.map (check_rule ss) rs);] if we could compare
         functional values. Failure to keep that invariant breaks some
         evaluation strategies. *)
      let srs, map = List.fold_right handle_rule rs ([], SymMap.empty) in
      (* /!\ Update decision trees without adding the rules themselves. It is
         important for local confluence checking. *)
      SymMap.iter Tree.update_dtree map;
      let sign = ss.signature in
      (* Local confluence checking. *)
      Tool.Lcr.check_cps pos sign srs map;
      (* Add rules in the signature. *)
      SymMap.iter (Sign.add_rules ss.signature) map;
      if !Console.verbose >= 2 then
        List.iter (Console.out 2 (Color.red "rule %a") sym_rule)
          (List.rev srs);
      (* Update critical pair positions. *)
      sign.Sign.sign_cp_pos :=
        Tool.Lcr.update_cp_pos pos !(sign.Sign.sign_cp_pos) map;
      (ss, None, None)
  | P_builtin(n,qid) ->
      let s = find_sym ~prt:true ~prv:true ss qid in
      begin
        match StrMap.find_opt n ss.builtins with
        | Some s' when s' == s ->
          fatal pos "Builtin \"%s\" already mapped to %a" n sym s
        | _ ->
          Builtin.check ss pos n s;
          Console.out 2 "builtin \"%s\" ≔ %a" n sym s;
          (Sig_state.add_builtin ss n s, None, None)
      end
  | P_notation(qid,n) ->
      let s = find_sym ~prt:true ~prv:true ss qid in
      (* Check arity. *)
      let expected =
        match n with
        | Prefix _ | Postfix _ -> 1
        | Infix _ -> 2
        | Zero -> 0
        | Succ _ -> 1
        | Quant -> 1
        | PosOne -> 0
        | PosDouble -> 1
        | PosSuccDouble -> 1
        | IntZero -> 0
        | IntPos -> 1
        | IntNeg -> 1
      and real = Tactic.count_products [] !(s.sym_type) in
      if real < expected then
        fatal pos "Notation incompatible with the type of %a" sym s;
      (* Convert strings into floats. *)
      let float_priority_from_string_priority s =
        try
          if String.contains s '.' then float_of_string s
          else float_of_int (int_of_string s)
        with Failure _ -> fatal pos "Too big number (max is %d)" max_int
      in
      let rec float_notation_from_string_notation n =
        match n with
        | Prefix s -> Prefix (float_priority_from_string_priority s)
        | Postfix s -> Postfix (float_priority_from_string_priority s)
        | Infix(a,s) -> Infix(a, float_priority_from_string_priority s)
        | Succ x -> Succ (Option.map float_notation_from_string_notation x)
        | Zero -> Zero
        | Quant -> Quant
        | PosOne -> PosOne
        | PosDouble -> PosDouble
        | PosSuccDouble -> PosSuccDouble
        | IntZero -> IntZero
        | IntPos -> IntPos
        | IntNeg -> IntNeg
      in
      let n = float_notation_from_string_notation n in
      Console.out 2 "notation %a %a" sym s (notation float) n;
      (Sig_state.add_notation ss s n, None, None)
  | P_unif_rule(h) ->
      (* Approximately same processing as rules without SR checking. *)
      let pur = scope_rule true ss h in
      let urule = Scope.rule_of_pre_rule pur in
      Sign.add_rule ss.signature Unif_rule.equiv urule;
      Tree.update_dtree Unif_rule.equiv [];
      Console.out 2 "unif_rule %a" unif_rule urule;
      (ss, None, None)
  | P_coercion c ->
      let pc = scope_rule false ss c in
      let r = Scope.rule_of_pre_rule pc in
      Sign.add_rule ss.signature Coercion.coerce r;
      Tree.update_dtree Coercion.coerce [];
      Console.out 2 "coercion %a" (rule_of Coercion.coerce) r;
      (ss, None, None)

  | P_inductive(ms, params, p_ind_list) ->
      (* Check modifiers. *)
      let (prop, expo, mstrat) = handle_modifiers ms in
      if prop <> Defin then
        fatal pos "Property modifiers cannot be used on inductive types.";
      if mstrat <> Eager then
        fatal pos "Pattern matching strategy modifiers cannot be used on \
                       inductive types.";
      (* Add inductive types in the signature. *)
      let add_ind_sym (ss, ind_sym_list) {elt=(id,pt,_); _} =
        let (ss, ind_sym) =
          (* All inductive types are declared at position [pos]
             so that constructors are declared afterwards. *)
          let id = {id with pos} in
          handle_inductive_symbol ss expo Const Eager id pos
           params pt in
        (ss, ind_sym::ind_sym_list)
      in
      let (ss, ind_sym_list_rev) =
        List.fold_left add_ind_sym (ss, []) p_ind_list in
      (* Set parameters as implicit in the type of constructors. *)
      let params =
        List.map (fun (idopts,typopt,_) -> (idopts,typopt,true)) params in
      (* Add constructors in the signature. *)
      let add_constructors
            (ss, cons_sym_list_list) {elt=(_,_,p_cons_list); _} =
        let add_cons_sym (ss, cons_sym_list) (id, pt) =
          let (ss, cons_sym) =
            handle_inductive_symbol ss expo Const Eager id pos
            params pt in
          (ss, cons_sym::cons_sym_list)
        in
        let (ss, cons_sym_list_rev) =
          List.fold_left add_cons_sym (ss, []) p_cons_list in
        (* Reverse the list of constructors previously computed to preserve
           the initial order. *)
        let cons_sym_list = List.rev cons_sym_list_rev in
        (ss, cons_sym_list::cons_sym_list_list)
      in
      let (ss, cons_sym_list_list_rev) =
        List.fold_left add_constructors (ss, []) p_ind_list
      in
      let ind_list =
        List.fold_left2
          (fun acc ind_sym cons_sym_list -> (ind_sym,cons_sym_list)::acc)
          []
          ind_sym_list_rev cons_sym_list_list_rev
      in
      (* Compute data useful for generating the induction principles. *)
      let cfg = Inductive.get_config ss pos in
      let a_str, p_str, x_str = Inductive.gen_safe_prefixes ind_list in
      let ind_nb_params = List.length params in
      let vs, env, ind_pred_map =
        Inductive.create_ind_pred_map pos cfg ind_nb_params ind_list
          a_str p_str x_str
      in
      (* Compute the induction principles. *)
      let rec_typ_list_rev =
        Inductive.gen_rec_types cfg pos ind_list vs env ind_pred_map x_str
      in
      (* Add the induction principles in the signature. *)
      let add_recursor (ss, rec_sym_list) ind_sym rec_typ =
        let rec_name = Inductive.rec_name ind_sym in
        if Sign.mem ss.signature rec_name then
          fatal pos "Symbol %a already exists." uid rec_name;
        let (ss, rec_sym) =
          Console.out 2 (Color.red "symbol %a : %a")
            uid rec_name term rec_typ;
          (* Recursors are declared after the types and constructors. *)
          let pos = after (end_pos pos) in
          let id = Pos.make pos rec_name in
          let r =
            Sig_state.add_symbol ss expo Defin Eager false id
             None rec_typ [] None
          in sig_state := fst r; r
        in
        (ss, rec_sym::rec_sym_list)
      in
      let (ss, rec_sym_list) =
        List.fold_left2 add_recursor (ss, [])
          ind_sym_list_rev rec_typ_list_rev
      in
      (* Add recursor rules in the signature. *)
      with_no_wrn
        (Inductive.iter_rec_rules pos ind_list vs ind_pred_map)
        (fun r -> add_rule ss (check_rule ss r));
      List.iter (fun s -> Tree.update_dtree s []) rec_sym_list;
      (* Store the inductive structure in the signature *)
      let ind_nb_types = List.length ind_list in
      List.iter2
        (fun (ind_sym, cons_sym_list) rec_sym ->
          Sign.add_inductive ss.signature ind_sym cons_sym_list rec_sym
            ind_nb_params ind_nb_types)
        ind_list
        rec_sym_list;
      (ss, None, None)

  | P_symbol {p_sym_mod;p_sym_nam;p_sym_arg;p_sym_typ;p_sym_trm;p_sym_prf;
              p_sym_def} ->
    (* We check that the identifier is not already used. *)
    let {elt=id; _} = p_sym_nam in
    if Sign.mem ss.signature id then
      fatal p_sym_nam.pos "Symbol %a already exists." uid id;
    (* Check that this is a syntactically valid symbol declaration. *)
    begin
      match p_sym_typ, p_sym_def, p_sym_trm, p_sym_prf with
      | None, true, None, Some _ -> fatal pos "missing type"
      |    _, true, None, None   -> fatal pos "missing definition"
      | _ -> ()
    end;
    (* Verify modifiers. *)
    let prop, expo, mstrat = handle_modifiers p_sym_mod in
    let opaq = List.exists Syntax.is_opaq p_sym_mod in
    let pdata_prv = opaq || expo = Privat in
    (match p_sym_def, opaq, prop, mstrat with
     | false, true, _, _ -> fatal pos "Symbol declarations cannot be opaque."
     | true, _, Const, _ -> fatal pos "Definitions cannot be constant."
     | true, _, _, Sequen ->
         fatal pos "Definitions cannot have matching strategies."
     | _ -> ());
    (* Scoping the definition and the type. *)
    let scope ?(typ=false) = scope_term ~typ pdata_prv ss Env.empty in
    (* Scoping function keeping track of the position. *)
    let scope ?(typ=false) t = Pos.make t.pos (scope ~typ t) in
    (* Desugaring of parameters and scoping of [p_sym_trm]. *)
    let pt, t =
      match p_sym_trm with
      | Some pt ->
          let pt =
            if p_sym_arg = [] then pt
            else let pos = Pos.(cat (end_pos p_sym_nam.pos) pt.pos) in
                 Pos.make pos (P_Abst(p_sym_arg, pt))
          in Some pt, Some (scope pt)
      | None -> None, None
    in
    (* Desugaring of parameters, scoping of [p_sym_typ], and computation
       of implicit arguments. *)
    let a, impl =
      match p_sym_typ with
      | None ->
        let impl =
          match pt with
          | None -> assert false
          | Some pt -> Syntax.get_impl_term pt
        in None, impl
      | Some a ->
          let a =
            if p_sym_arg = [] then a
            else let pos = Pos.(cat (end_pos p_sym_nam.pos) a.pos) in
                 Pos.make pos (P_Prod(p_sym_arg, a))
          in Some (scope ~typ:true a), Syntax.get_impl_term a
    in
    (* Problem recording metavariables and constraints. *)
    let p = new_problem() in
    (* Build proof data. *)
    let pdata =
      (* Type of the symbol. *)
      let t, a =
        match a with
        | Some {elt=a;pos} -> (* Check that the given type is well sorted. *)
          begin match Infer.check_sort_noexn p [] a with
            | None -> fatal pos "%a@ cannot be typed by a sort" term a
            | Some (a,_) ->
              let t =
                match t with
                | None -> None
                | Some {elt=t;pos} ->
                  match Infer.check_noexn p [] t a with
                  | None ->
                    fatal pos "%a@ cannot be of type@ %a" term t term a
                  | Some t -> Some (Pos.make pos t)
              in
              (t, a)
          end
        | None -> (* If no type is given, infer it from the definition. *)
          match t with
          | None -> assert false
          | Some {elt=t;pos} ->
            match Infer.infer_noexn p [] t with
            | None -> fatal pos "%a@ is not typable" term t
            | Some (t,a) -> Some (Pos.make pos t), a
      in
      (* Get tactics and proof end. *)
      let pdata_proof, pe =
        match p_sym_prf with
        | None -> [], Pos.make (Pos.end_pos pos) P_proof_end
        | Some (ts, pe) -> ts, pe
      in
      (* Build finalizer. *)
      let declpos = Pos.cat pos (Option.bind p_sym_typ (fun x -> x.pos)) in
      let pdata_finalize ss ps =
        match pe.elt with
        | P_proof_abort -> wrn pe.pos "Proof aborted."; ss
        | P_proof_admitted ->
            if finished ps then
              fatal pe.pos "The proof is finished. Use 'end' instead.";
            (* Admit all the remaining typing goals. *)
            let admit_goal g =
              match g with
              | Unif _ -> fatal pos "Cannot admit unification goals."
              | Typ gt ->
                let m = gt.goal_meta in
                match !(m.meta_value) with
                | None -> Tactic.admit_meta ss p_sym_nam.pos m
                | Some _ -> ()
            in
            List.iter admit_goal ps.proof_goals;
            (* Add the symbol in the signature with a warning. *)
            Console.out 2 (Color.red "symbol %a : %a") uid id term a;
            wrn pe.pos "Proof admitted.";
            (* Keep the definition only if the symbol is not opaque. *)
            let d =
              if opaq then None else
                Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
            in
            (* Add the symbol in the signature. *)
            fst (Sig_state.add_symbol
                   ss expo prop mstrat opaq p_sym_nam declpos a impl d)
        | P_proof_end ->
            (* Check that the proof is indeed finished. *)
            if not (finished ps) then
              fatal pe.pos "The proof is not finished:@.%a" goals ps;
            (* Keep the definition only if the symbol is not opaque. *)
            let d =
              if opaq then None else
                Option.map (fun m -> unfold (mk_Meta(m,[||]))) ps.proof_term
            in
            (* Add the symbol in the signature. *)
            Console.out 2 (Color.red "symbol %a : %a") uid id term a;
            fst (Sig_state.add_symbol
                   ss expo prop mstrat opaq p_sym_nam declpos a impl d)
      in
      (* Create the proof state. *)
      let pdata_state =
        let proof_goals = Proof.add_goals_of_problem p [] in
        if p_sym_def then
          (* Add a new focused goal and refine on it. *)
          let m = LibMeta.fresh p a 0 in
          let g = Goal.of_meta m in
          let ps = {proof_name = p_sym_nam; proof_term = Some m;
                    proof_goals = g :: proof_goals} in
          match pt, t with
          | Some pt, Some t ->
              let gt = match g with Typ gt -> gt | _ -> assert false in
              Tactic.tac_refine ~check:false pt.pos ps gt proof_goals p t.elt
          | _, _ -> Tactic.tac_solve pos ps
        else
          let ps = {proof_name = p_sym_nam; proof_term = None; proof_goals} in
          Tactic.tac_solve pos ps
      in
      if p_sym_prf = None && not (finished pdata_state) then wrn pos
        "Some metavariables could not be solved: a proof must be given";
      { pdata_sym_pos=p_sym_nam.pos; pdata_state; pdata_proof
      ; pdata_finalize; pdata_end_pos=pe.pos; pdata_prv }
    in
      (ss, Some pdata, None)

(** [too_long] indicates the duration after which a warning should be given to
    indicate commands that take too long to execute. *)
let too_long = Stdlib.ref infinity

(** [get_proof_data compile ss cmd] adds to the previous [command] some
    exception handling. In particular, the position of [cmd] is used on errors
    that lack a specific position. All exceptions except [Timeout] and [Fatal]
    are captured, although they should not occur. *)
let get_proof_data : compiler -> sig_state -> p_command -> cmd_output =
  fun compile ss ({pos;_} as cmd) ->
  sig_state := ss;
  try
    let (tm, ss) = Extra.time (get_proof_data compile ss) cmd in
    if Stdlib.(tm >= !too_long) then
      wrn pos "It took %.2f seconds to handle the command." tm;
    ss
  with
  | Timeout                as e -> raise e
  | Fatal(Some(Some(_)),_) as e -> raise e
  | Fatal(None         ,m)      -> fatal pos "Error on command.@.%s" m
  | Fatal(Some(None)   ,m)      -> fatal pos "Error on command.@.%s" m
  | e                           ->
      fatal pos "Uncaught exception: %s." (Printexc.to_string e)

(** [handle compile_mod ss cmd] retrieves proof data from [cmd] (with
    {!val:get_proof_data}) and handles proofs using functions from
    {!module:Tactic} The function [compile_mod] is used to compile required
    modules recursively. *)
let handle : compiler -> Sig_state.t -> Syntax.p_command -> Sig_state.t =
  fun compile_mod ss cmd ->
  LibMeta.reset_meta_counter ();
  (* We provide the compilation function to the handle commands, so that
     "require" is able to compile files. *)
  let (ss, p, _) = get_proof_data compile_mod ss cmd in
  match p with
  | None -> ss
  | Some d ->
    let ps, _ =
      fold_proof (Tactic.handle ss d.pdata_sym_pos d.pdata_prv)
        (d.pdata_state, None) d.pdata_proof
    in d.pdata_finalize ss ps