ecScope.ml

(* -------------------------------------------------------------------- *)
open EcUtils
open EcMaps
open EcSymbols
open EcLocation
open EcPath
open EcParsetree
open EcAst
open EcTypes
open EcDecl
open EcModules
open EcFol
open EcTyping
open EcHiInductive
open EcBigInt.Notations

module Sid  = EcIdent.Sid
module Mid  = EcIdent.Mid
module MSym = EcSymbols.Msym
module BI   = EcBigInt

(* -------------------------------------------------------------------- *)
exception HiScopeError of EcLocation.t option * string

let pp_hi_scope_error fmt exn =
  match exn with
  | HiScopeError (None, s) ->
      Format.fprintf fmt "%s" s

  | HiScopeError (Some loc, s) ->
      Format.fprintf fmt "%s: %s" (EcLocation.tostring loc) s

  | _ -> raise exn

let _ = EcPException.register pp_hi_scope_error

let hierror ?loc fmt =
  let buf  = Buffer.create 127 in
  let bfmt = Format.formatter_of_buffer buf in

    Format.kfprintf
      (fun _ ->
         Format.pp_print_flush bfmt ();
         raise (HiScopeError (loc, Buffer.contents buf)))
      bfmt fmt

(* -------------------------------------------------------------------- *)
exception ImportError of EcLocation.t option * symbol * exn

let is_import_error = function ImportError _ -> true | _ -> false

let pp_import_error fmt exn =
  match exn with
  | ImportError (None, name, e) ->
      Format.fprintf fmt "In external theory %s [<unknown> location]:@\n%a"
        name EcPException.exn_printer e

  | ImportError (Some l, name, e) when is_import_error e ->
      Format.fprintf fmt "In external theory %s [%s]:@\n%a"
        name (EcLocation.tostring l)
        EcPException.exn_printer e

  | ImportError (Some l, name, e) ->
      Format.fprintf fmt "In external theory %s [%s]:@\n@\n%a"
        name (EcLocation.tostring l)
        EcPException.exn_printer e

  | _ -> raise exn

let _ = EcPException.register pp_import_error

(* -------------------------------------------------------------------- *)
exception TopError of EcLocation.t * exn

let rec toperror_of_exn_r ?gloc exn =
  match exn with
  | TyError    (loc, _, _) -> Some (loc, exn)
  | RcError    (loc, _, _) -> Some (loc, exn)
  | DtError    (loc, _, _) -> Some (loc, exn)
  | ParseError (loc, _)    -> Some (loc, exn)

  | EcHiPredicates.TransPredError (loc, _, _) -> Some (loc, exn)
  | EcHiNotations .NotationError  (loc, _, _) -> Some (loc, exn)

  | EcLexer.LexicalError (loc, _) ->
      Some (odfl (odfl _dummy gloc) loc, exn)

  | EcCoreGoal.TcError { EcCoreGoal.tc_location = None } ->
      Some (odfl _dummy gloc, exn)

  | EcCoreGoal.TcError
      { EcCoreGoal.tc_location = Some { EcCoreGoal.plc_loc = loc } } ->
      let gloc = if EcLocation.isdummy loc then gloc else Some loc in
      Some (odfl _dummy gloc, exn)

  | LocError (loc, e)    -> begin
      let gloc = if EcLocation.isdummy loc then gloc else Some loc in
      match toperror_of_exn_r ?gloc e with
      | None -> Some (loc, e)
      | Some (loc, e) -> Some (loc, e)
    end

  | ImportError _ ->
      Some (odfl _dummy gloc, exn)

  | TopError (loc, e) ->
      let gloc = if EcLocation.isdummy loc then gloc else Some loc in
      toperror_of_exn_r ?gloc e
  | EcSection.SectionError _ ->
    Some (odfl _dummy gloc, exn)
  | HiScopeError (loc, msg) ->
      let gloc =
        match loc with
        | None     -> gloc
        | Some loc -> if EcLocation.isdummy loc then gloc else Some loc
      in
        Some (odfl _dummy gloc, HiScopeError (None, msg))

  | Sys.Break ->
      Some (odfl _dummy gloc, HiScopeError (None, "interrupted"))

  | _ -> None

let toperror_of_exn ?gloc exn =
  match toperror_of_exn_r ?gloc exn with
  | Some (loc, exn) -> TopError (loc, exn)
  | None            -> exn

let pp_toperror fmt loc exn =
  Format.fprintf fmt "%s: %a"
    (EcLocation.tostring loc)
    EcPException.exn_printer exn

let () =
  let pp fmt exn =
    match exn with
    | TopError (loc, exn) -> pp_toperror fmt loc exn
    | _ -> raise exn
  in
    EcPException.register pp

(* -------------------------------------------------------------------- *)
type goption = ..

module type IOptions = sig
  type oid
  type options

  type action = { for_loading : goption -> goption; }

  val register     : ?action:action -> goption -> oid
  val freeze       : unit -> options
  val get          : options -> oid -> goption
  val set          : options -> oid -> goption -> options
  val for_loading  : options -> options
  val for_subscope : options -> options
end

(* -------------------------------------------------------------------- *)
module GenOptions : IOptions = struct
  type action  = { for_loading : goption -> goption; }
  type oid     = EcUid.uid
  type options = (action * goption) EcUid.Muid.t

  let options : options ref =
    ref EcUid.Muid.empty

  let identity = { for_loading = (fun x -> x); }

  let register ?(action = identity) goption =
    let oid = EcUid.unique () in
    options := EcUid.Muid.add oid (action, goption) !options; oid

  let freeze () =
    !options

  let get (options : options) (oid : oid) =
    snd (oget (EcUid.Muid.find_opt oid options))

  let set (options : options) (oid : oid) (goption : goption) =
    EcUid.Muid.change (fun k -> Some (fst (oget k), goption)) oid options

  let for_loading options =
    EcUid.Muid.map (fun (act, exn) -> act, act.for_loading exn) options

  let for_subscope options =
    options
end

(* -------------------------------------------------------------------- *)
module Check_mode = struct
  type mode = [`Off | `On | `Forced]

  type goption += Check of mode

  let oid =
    let for_loading = function
      | Check `Off    -> Check `Off
      | Check `On     -> Check `Off
      | Check `Forced -> Check `Forced
      | exn           -> exn
    in GenOptions.register ~action:({ GenOptions.for_loading }) (Check `On)

  let check options =
    match GenOptions.get options oid with
    | Check `On     -> true
    | Check `Forced -> true
    | Check `Off    -> false
    | _ -> true

  let set_checkproof options b =
    match GenOptions.get options oid with
    | Check `On  when not b -> GenOptions.set options oid (Check `Off)
    | Check `Off when     b -> GenOptions.set options oid (Check `On )
    | _ -> options

  let set_fullcheck options =
    GenOptions.set options oid (Check `Forced)
end

(* -------------------------------------------------------------------- *)
module Prover_info = struct
  type goption += PI of EcProvers.prover_infos

  let oid = GenOptions.register (PI EcProvers.dft_prover_infos)

  let set options pi =
    GenOptions.set options oid (PI pi)

  let get options =
    match GenOptions.get options oid with
    | PI pi -> pi
    | _     -> assert false
end

(* -------------------------------------------------------------------- *)
module KnownFlags = struct
  let implicits = "implicits"
  let oldip     = "oldip"
  let redlogic  = "redlogic"
  let und_delta = "und_delta"

  let flags = [
    (implicits, false);
    (oldip    , false);
    (redlogic , true );
    (und_delta, false);
  ]
end

exception UnknownFlag of string

module Flags : sig
  open GenOptions

  val get : options -> string -> bool
  val set : options -> string -> bool -> options
end = struct
  type flags    = bool Mstr.t
  type goption += Flags of flags

  let asflags = function Flags m -> m | _ -> assert false

  let oid =
    let default = Mstr.of_list KnownFlags.flags in
    let for_loading = function
      | Flags _ -> Flags default
      | exn -> exn
    in GenOptions.register ~action:{ GenOptions.for_loading } (Flags default)

  let get options name =
    let flags = asflags (GenOptions.get options oid) in
    oget ~exn:(UnknownFlag name) (Mstr.find_opt name flags)

  let set options name value =
    let flags = asflags (GenOptions.get options oid) in
    let flags =
      Mstr.change (fun x ->
        ignore (oget ~exn:(UnknownFlag name) x : bool);
        Some value)
      name flags in

    GenOptions.set options oid (Flags flags)
end

(* -------------------------------------------------------------------- *)
type proof_uc = {
  puc_active : (proof_auc * (proof_ctxt option)) option;
  puc_cont   : proof_ctxt list * (EcSection.scenv option);
  puc_init   : EcSection.scenv;
}

and proof_auc = {
  puc_name    : symbol option;
  puc_started : bool;
  puc_jdg     : proof_state;
  puc_flags   : pucflags;
  puc_crt     : EcDecl.axiom;
}

and proof_ctxt =
  (symbol option * EcDecl.axiom) * EcPath.path * EcSection.scenv

and proof_state =
  PSNoCheck | PSCheck of EcCoreGoal.proof

and pucflags = {
  puc_smt   : bool;
  puc_local : bool;
}

(* -------------------------------------------------------------------- *)
type required_info = {
  rqd_name      : symbol;
  rqd_namespace : EcLoader.namespace option;
  rqd_kind      : EcLoader.kind;
  rqd_digest    : Digest.t;
  rqd_direct    : bool;
}

type required = required_info list

type prelude = {
  pr_env      : EcEnv.env;
  pr_required : required;
}

type thloaded = EcEnv.Theory.compiled_theory

type scope = {
  sc_name     : (symbol * EcTheory.thmode);
  sc_env      : EcSection.scenv;
  sc_top      : scope option;
  sc_prelude  : ([`Frozen | `InPrelude] * prelude);
  sc_loaded   : (thloaded * required) Msym.t;
  sc_required : required;
  sc_clears   : path list;
  sc_pr_uc    : proof_uc option;
  sc_options  : GenOptions.options;
  sc_globdoc  : string list;
  sc_locdoc   : docstate;
}

and docstate = {
  docentities  : docentity list;
  subdocentbl  : docentity list;
  docstringbl  : string list;
  srcstringbl  : string list;
  currentname  : string option;
  currentkind  : itemkind option;
  currentmode  : mode option;
  currentproc  : bool;
}

and docentity =
  | ItemDoc   of string list * docitem
  | SubDoc    of (string list * docitem) * docentity list

and docitem =
  mode * itemkind * string * string list (* dec/reg, kind, name, src *)

and itemkind = [`Type | `Operator | `Axiom | `Lemma | `ModuleType | `Module | `Theory]

and mode = [`Abstract | `Specific]

(* -------------------------------------------------------------------- *)
let get_gdocstrings (sc : scope) : string list =
  sc.sc_globdoc

let get_ldocentities (sc : scope) : docentity list =
  sc.sc_locdoc.docentities

module DocState = struct
  let empty : docstate =
    { docentities = [];
      subdocentbl = [];
      docstringbl = [];
      srcstringbl = [];
      currentname = None;
      currentkind = None;
      currentmode = None;
      currentproc = false; }

  let start_process (state : docstate) (name : string) (kind : itemkind) (md : mode): docstate =
    { state with
        currentname = Some name;
        currentkind = Some kind;
        currentmode = Some md;
        currentproc = true }

  let prevent_process (state : docstate) : docstate =
    { state with
        currentname = None;
        currentkind = None;
        currentmode = None;
        currentproc = false }

  let reinitialize_process (state : docstate) : docstate =
    { state with
        docstringbl = [];
        srcstringbl = [];
        currentname = None;
        currentkind = None;
        currentmode = None;
        currentproc = false }

  let push_docbl (state : docstate) (docc : string) : docstate =
    { state with docstringbl = state.docstringbl @ [docc] }

  let push_srcbl (state : docstate) (srcs : string) : docstate =
    { state with srcstringbl = state.srcstringbl @ [srcs] }

  let add_entity (state : docstate) (docent : docentity) : docstate =
    { state with docentities = state.docentities @ [docent] }

  let add_item (state : docstate) : docstate =
    let state =
      if state.currentproc
      then
        add_entity state (ItemDoc (state.docstringbl, (oget state.currentmode, oget state.currentkind, oget state.currentname, state.srcstringbl)))
      else
        state
    in
    reinitialize_process state

  let add_sub (state : docstate) (substate : docstate) : docstate =
    let state =
      if state.currentproc
      then
        add_entity state (SubDoc ((state.docstringbl, (oget state.currentmode, oget state.currentkind, oget state.currentname, state.srcstringbl)),
                                 (substate.docentities)))
      else
        state
    in
    reinitialize_process state

  end

(* -------------------------------------------------------------------- *)
let empty (gstate : EcGState.gstate) =
  let env = EcEnv.initial gstate in
  { sc_name       = (EcPath.basename (EcEnv.root env), `Concrete);
    sc_env        = EcSection.initial env;
    sc_top        = None;
    sc_prelude    = (`InPrelude, { pr_env = env; pr_required = []; });
    sc_loaded     = Msym.empty;
    sc_required   = [];
    sc_clears     = [];
    sc_pr_uc      = None;
    sc_options    = GenOptions.freeze ();
    sc_globdoc    = [];
    sc_locdoc     = DocState.empty; }

(* -------------------------------------------------------------------- *)
let env (scope : scope) =
  EcSection.env scope.sc_env

(* -------------------------------------------------------------------- *)
let gstate (scope : scope) =
  EcEnv.gstate (env scope)

(* -------------------------------------------------------------------- *)
let name (scope : scope) =
  scope.sc_name

(* -------------------------------------------------------------------- *)
let path (scope : scope) =
  EcEnv.root (env scope)

(* -------------------------------------------------------------------- *)
let attop (scope : scope) =
  scope.sc_top = None

(* -------------------------------------------------------------------- *)
let freeze (scope : scope) =
  match scope.sc_prelude with
  | `Frozen   , _  -> assert false
  | `InPrelude, pr -> { scope with sc_prelude = (`Frozen, pr) }

(* -------------------------------------------------------------------- *)
let goal (scope : scope) =
  scope.sc_pr_uc |> obind (fun x -> omap fst x.puc_active)

(* -------------------------------------------------------------------- *)
let xgoal (scope : scope) =
  scope.sc_pr_uc

(* -------------------------------------------------------------------- *)
let dump_why3 (scope : scope) (filename : string) =
  try  EcSmt.dump_why3 (env scope) filename
  with
  | Sys_error msg ->
      hierror "cannot dump to `%s`: system error: %s"
        filename msg
  | Unix.Unix_error (e, _, _) ->
      hierror "cannot dump to `%s`: system error: %s"
        filename (Unix.error_message e)

(* -------------------------------------------------------------------- *)
type topmode = [`InProof | `InActiveProof | `InTop]

let check_state (mode : topmode) action (scope : scope) =
  match mode with
  | `InProof when scope.sc_pr_uc = None ->
      hierror "cannot process [%s] outside a proof script" action

  | `InActiveProof when scope.sc_pr_uc = None ->
      hierror "cannot process [%s] outside a proof script" action

  | `InTop when scope.sc_pr_uc <> None ->
      hierror "cannot process [%s] inside a proof script" action

  | _ -> ()

(* -------------------------------------------------------------------- *)
let notify (scope : scope) (lvl : EcGState.loglevel) =
  EcEnv.notify (env scope) lvl

(* -------------------------------------------------------------------- *)
module Options = struct
  let get scope name =
    Flags.get scope.sc_options name

  let set scope name value =
    { scope with sc_options =
        Flags.set scope.sc_options name value }

  let get_implicits scope =
    get scope KnownFlags.implicits

  let set_implicits scope value =
    set scope KnownFlags.implicits value

  let get_oldip scope =
    get scope KnownFlags.oldip

  let set_oldip scope value =
    set scope KnownFlags.oldip value

  let get_redlogic scope =
    get scope KnownFlags.redlogic

  let set_redlogic scope value =
    set scope KnownFlags.redlogic value

  let get_und_delta scope =
    get scope KnownFlags.und_delta

  let set_und_delta scope value =
    set scope KnownFlags.und_delta value
end

(* -------------------------------------------------------------------- *)
let for_loading (scope : scope) =
  let pr  = snd (scope.sc_prelude) in
  let env = EcEnv.copy pr.pr_env in
  let lg  = EcGState.loglevel (EcEnv.gstate env) in

  EcGState.set_loglevel
    (EcGState.max_loglevel `Warning lg)
    (EcEnv.gstate env);

  { sc_name       = (EcPath.basename (EcEnv.root pr.pr_env), `Concrete);
    sc_env        = EcSection.initial env;
    sc_top        = None;
    sc_prelude    = scope.sc_prelude;
    sc_loaded     = scope.sc_loaded;
    sc_required   = pr.pr_required;
    sc_clears     = [];
    sc_pr_uc      = None;
    sc_options    = GenOptions.for_loading scope.sc_options;
    sc_globdoc    = [];
    sc_locdoc     = DocState.empty; }

(* -------------------------------------------------------------------- *)
let subscope (scope : scope) (mode : EcTheory.thmode) (name : symbol) lc =
  let env = EcSection.enter_theory name lc mode scope.sc_env in

  { sc_name       = (name, mode);
    sc_env        = env;
    sc_top        = Some scope;
    sc_prelude    = scope.sc_prelude;
    sc_loaded     = scope.sc_loaded;
    sc_required   = scope.sc_required;
    sc_clears     = [];
    sc_pr_uc      = None;
    sc_options    = GenOptions.for_subscope scope.sc_options;
    sc_globdoc    = [];
    sc_locdoc     = DocState.empty;
  }

(* -------------------------------------------------------------------- *)
module Prover = struct
  let all_provers () =
    List.map
      (fun p -> p.EcProvers.pr_name)
      (EcProvers.known ~evicted:false)

  let check_prover_name { pl_desc = name; pl_loc = loc } =
    if not (EcProvers.is_prover_known name) then
      hierror ~loc "Unknown prover %s" name;
    name

  (* -------------------------------------------------------------------- *)
  let process_dbhint env db =
    let add hints x =
      let nf kind p =
        hierror
          ~loc:p.pl_loc "cannot find %s `%s'"
          (match kind with `Lemma -> "lemma" | `Theory -> "theory")
          (string_of_qsymbol (unloc p))
      in

      let addm hints hflag p =
        match EcEnv.Theory.lookup_opt (unloc p) env with
        | None -> nf `Theory p
        | Some (p, _) -> EcProvers.Hints.addm p hflag hints

      and add1 hints hflag p =
        match EcEnv.Ax.lookup_opt (unloc p) env with
        | None -> nf `Lemma p
        | Some (p, _) -> EcProvers.Hints.add1 p hflag hints
      in

      match x.pht_kind with
      | `Theory -> addm hints x.pht_flag x.pht_name
      | `Lemma  -> add1 hints x.pht_flag x.pht_name

    in
    let hints = EcProvers.Hints.empty in
    let hints = List.fold_left add hints db in
    hints

  (* -------------------------------------------------------------------- *)
  type smt_options = {
    po_timeout    : int option;
    po_cpufactor  : int option;
    po_nprovers   : int option;
    po_provers    : string list option * (include_exclude * string) list;
    po_quorum     : int option;
    po_verbose    : int option;
    pl_all        : bool option;
    pl_max        : int option;
    pl_wanted     : EcProvers.hints option;
    pl_unwanted   : EcProvers.hints option;
    pl_dumpin     : string located option;
    pl_selected   : bool option;
    gn_debug      : bool option;
  }

  (* -------------------------------------------------------------------- *)
  let empty_options = {
    po_timeout   = None;
    po_cpufactor = None;
    po_nprovers  = None;
    po_provers   = (None, []);
    po_quorum    = None;
    po_verbose   = None;
    pl_all       = None;
    pl_max       = None;
    pl_wanted    = None;
    pl_unwanted  = None;
    pl_dumpin    = None;
    pl_selected  = None;
    gn_debug     = None;
  }

  (* -------------------------------------------------------------------- *)
  let process_prover_option env ppr =
    let provers =
      match ppr.pprov_names with
      | None -> None, []
      | Some pl ->
        let do_uo uo s =
          match s.pl_desc with
          | "!" -> all_provers ()
          | ""  -> []
          | _   ->
            let x = check_prover_name s in
            if List.exists ((=) x) uo then uo else x :: uo in
        let uo =
          if pl.pp_use_only = [] then None
          else Some (List.fold_left do_uo [] pl.pp_use_only) in
        let do_ar (k,s) = k, check_prover_name s in
        uo, List.map do_ar pl.pp_add_rm in
    let verbose = omap (odfl 1) ppr.pprov_verbose in
    {
      po_timeout   = ppr.pprov_timeout;
      po_cpufactor = ppr.pprov_cpufactor;
      po_nprovers  = ppr.pprov_max;
      po_provers   = provers;
      po_quorum    = ppr.pprov_quorum;
      po_verbose   = verbose;
      pl_all       = ppr.plem_all;
      pl_max       =
        begin match ppr.plem_max, ppr.plem_wanted with
        | Some i, _      -> Some (odfl max_int i)
        | None  , None   -> None
        | None  , Some _ -> Some 0
        end;
      pl_wanted    = omap (process_dbhint env) ppr.plem_wanted;
      pl_unwanted  = omap (process_dbhint env) ppr.plem_unwanted;
      pl_dumpin    = ppr.plem_dumpin;
      pl_selected  = ppr.plem_selected;
      gn_debug     = ppr.psmt_debug;
    }

  (* -------------------------------------------------------------------- *)
  let mk_prover_info_from_dft (dft : EcProvers.prover_infos)
      (options : smt_options) : EcProvers.prover_infos =
    let open EcProvers in

    let gn_debug     = odfl dft.gn_debug options.gn_debug in
    let pr_maxprocs  = odfl dft.pr_maxprocs options.po_nprovers in
    let pr_timelimit = max 0 (odfl dft.pr_timelimit options.po_timeout) in
    let pr_cpufactor = max 0 (odfl dft.pr_cpufactor options.po_cpufactor) in
    let pr_verbose   = max 0 (odfl dft.pr_verbose options.po_verbose) in
    let pr_all       = odfl dft.pr_all options.pl_all in
    let pr_max       = odfl dft.pr_max options.pl_max in
    let pr_wanted    = odfl dft.pr_wanted options.pl_wanted in
    let pr_unwanted  = odfl dft.pr_unwanted options.pl_unwanted in
    let pr_selected  = odfl dft.pr_selected options.pl_selected in
    let pr_quorum    = max 1 (odfl dft.pr_quorum options.po_quorum) in
    let pr_dumpin    = options.pl_dumpin in
    let pr_provers   =
      let l = odfl dft.pr_provers (fst options.po_provers) in
      let do_ar l (k, p) =
        match k with
        | `Exclude -> List.remove_all l p
        | `Include -> if List.exists ((=) p) l then l else p::l
      in List.fold_left do_ar l (snd options.po_provers) in

    { pr_maxprocs; pr_provers ; pr_timelimit; pr_cpufactor;
      pr_verbose ; pr_all     ; pr_max      ;
      pr_wanted  ; pr_unwanted; pr_selected ; pr_quorum   ;
      pr_dumpin  ;
      gn_debug   ; }

  (* -------------------------------------------------------------------- *)
  let mk_prover_info scope (options : smt_options) =
    let dft = Prover_info.get scope.sc_options in
    mk_prover_info_from_dft dft options

  (* -------------------------------------------------------------------- *)
  let do_prover_info scope ?(default = empty_options) ppr =
    let options = Option.map (process_prover_option (env scope)) ppr in
    let options = Option.value ~default options in
    mk_prover_info scope options

  (* -------------------------------------------------------------------- *)
  let pprover_infos_to_prover_infos
      (env : EcEnv.env) (dft : EcProvers.prover_infos)
      (ppr : pprover_infos) : EcProvers.prover_infos =
    let options = process_prover_option env ppr in
    mk_prover_info_from_dft dft options

  (* -------------------------------------------------------------------- *)
  let process scope ppr =
    let pi = do_prover_info scope (Some ppr) in
    { scope with sc_options = Prover_info.set scope.sc_options pi }

  (* -------------------------------------------------------------------- *)
  let set_default scope options =
    let provers = match fst options.po_provers with
      | None   ->
        let provers = EcProvers.dft_prover_names in
        List.filter EcProvers.is_prover_known provers

      | Some l ->
        List.iter
          (fun name -> if not (EcProvers.is_prover_known name) then
              hierror "unknown prover %s" name) l; l in
    let options =
      { options with po_provers = (Some provers, snd options.po_provers) } in
    let pi = mk_prover_info scope options in
    { scope with sc_options = Prover_info.set scope.sc_options pi }

  (* -------------------------------------------------------------------- *)
  let full_check scope =
    { scope with sc_options = Check_mode.set_fullcheck scope.sc_options }

  (* -------------------------------------------------------------------- *)
  let check_proof scope b =
    { scope with sc_options = Check_mode.set_checkproof scope.sc_options b }
end

(* -------------------------------------------------------------------- *)
module Tactics = struct
  type prinfos =
    EcCoreGoal.proofenv * (EcCoreGoal.handle * EcCoreGoal.handle list)

  type proofmode = [`WeakCheck | `Check | `Report]

  let pi scope pi = Prover.do_prover_info scope pi

  let proof ?(src : string option) (scope : scope) =
    check_state `InActiveProof "proof script" scope;

    match (oget scope.sc_pr_uc).puc_active with
    | None -> hierror "no active lemmas"
    | Some (pac, pct) ->
      let pac =
        if pac.puc_started then
          hierror "[proof] can only be used at beginning of a proof script";
        { pac with puc_started = true }
      in
        { scope with
            sc_pr_uc = Some { (oget scope.sc_pr_uc) with puc_active = Some (pac, pct) };
            sc_locdoc =
            match src with
            | Some src -> DocState.push_srcbl scope.sc_locdoc src
            | None -> scope.sc_locdoc; }

  let process_r ?(src : string option) ?reloc mark (mode : proofmode) (scope : scope) (tac : ptactic list) =
    check_state `InProof "proof script" scope;

    let scope =
      match (oget scope.sc_pr_uc).puc_active with
      | None -> hierror "no active lemma"
      | Some (pac, _) ->
          if   mark && not pac.puc_started
          then proof scope
          else scope
    in

    let scope = { scope with
                  sc_locdoc =
                    match src with
                    | Some src -> DocState.push_srcbl scope.sc_locdoc src
                    | None -> scope.sc_locdoc; }
    in

    let puc = oget (scope.sc_pr_uc) in
    let pac, pct = oget (puc).puc_active in

    match pac.puc_jdg with
    | PSNoCheck ->
        None, scope

    | PSCheck juc ->
        let module TTC = EcHiTacticals in

        let htmode =
          match mode with
          | `WeakCheck -> `Admit
          | `Check     -> `Strict
          | `Report    -> `Report
        in

        let ttenv = {
          EcHiGoal.tt_provers    = pi scope;
          EcHiGoal.tt_smtmode    = htmode;
          EcHiGoal.tt_implicits  = Options.get_implicits scope;
          EcHiGoal.tt_oldip      = Options.get_oldip scope;
          EcHiGoal.tt_redlogic   = Options.get_redlogic scope;
          EcHiGoal.tt_und_delta  = Options.get_und_delta scope; } in

        let (hds, juc) =
          try  TTC.process ttenv tac juc
          with EcCoreGoal.TcError tcerror ->
            let tcerror =
              ofold
                (fun reloc error ->
                  { error with EcCoreGoal.tc_reloced = Some (reloc, true) })
                tcerror reloc
            in raise (EcCoreGoal.TcError tcerror)
        in

        let penv = EcCoreGoal.proofenv_of_proof juc in

        let pac = { pac with puc_jdg = PSCheck juc } in
        let puc = { puc with puc_active = Some (pac, pct); } in
        let scope = { scope with sc_pr_uc = Some puc; } in
        Some (penv, hds), scope

  let process1_r mark mode scope t =
    process_r mark mode scope [t]

  let process_core mark mode (scope : scope) (ts : ptactic_core list) =
    let ts = List.map (fun t -> { pt_core = t; pt_intros = []; }) ts in
    snd (process_r mark mode scope ts)

  let process ?(src : string option) scope mode tac =
    process_r ?src true mode scope tac
end

(* -------------------------------------------------------------------- *)
module Auto = struct
  let add_rw scope ~local ~base l =
    let scope, base =
      match EcEnv.BaseRw.lookup_opt base.pl_desc (env scope) with
      | None ->
        let pre, ibase = unloc base in
        if not (List.is_empty pre) then
          hierror ~loc:base.pl_loc
            "cannot create rewrite hints out of its enclosing theory";
        let scope =
          let item = EcTheory.mkitem ~import:true (EcTheory.Th_baserw (ibase, local)) in
          { scope with sc_env = EcSection.add_item item scope.sc_env; } in
        (scope, fst (EcEnv.BaseRw.lookup base.pl_desc (env scope)))

      | Some (base, _) -> (scope, base) in

    let env = env scope in
    let l = List.map (fun l -> EcEnv.Ax.lookup_path (unloc l) env) l in
    let item = EcTheory.mkitem ~import:true (Th_addrw (base, l, local)) in
    { scope with sc_env =  EcSection.add_item item scope.sc_env }

  let bind_hint scope ~local ~level ?base axioms =
    let item = EcTheory.mkitem ~import:true (Th_auto { level; base; axioms; locality=local} ) in
    { scope with sc_env = EcSection.add_item item scope.sc_env }

  let add_hint scope hint =
    let base = omap unloc hint.ht_base in
    let env = env scope in
    let names = List.map
      (fun l -> EcEnv.Ax.lookup_path (unloc l) env)
      hint.ht_names in
    let mode = if List.mem `Rigid hint.ht_options then `Rigid else `Default in
    let names = List.map (fun p -> (p, mode)) names in

    bind_hint scope ~local:hint.ht_local ~level:hint.ht_prio ?base names
end

(* -------------------------------------------------------------------- *)
module Ax = struct
  open EcParsetree
  open EcDecl

  module TT = EcTyping

  type proofmode = Tactics.proofmode

  (* ------------------------------------------------------------------ *)
  let bind ?(import = true) (scope : scope) ((x, ax) : _ * axiom) =
    assert (scope.sc_pr_uc = None);
    let item = EcTheory.mkitem ~import (EcTheory.Th_axiom (x, ax)) in
    { scope with sc_env =
        EcSection.add_item item scope.sc_env;
        sc_locdoc = DocState.add_item scope.sc_locdoc; }

  (* ------------------------------------------------------------------ *)
  let start_lemma scope (cont, axflags) check ?name (axd, ctxt) =
    let puc =
      match check with
      | false -> PSNoCheck
      | true  ->
          let hyps  = EcEnv.LDecl.init (env scope) axd.ax_tparams in
          let proof = EcCoreGoal.start hyps axd.ax_spec in
          PSCheck proof
    in
    let puc =
      let active =
        { puc_name    = name
        ; puc_started = false
        ; puc_jdg     = puc
        ; puc_flags   = axflags
        ; puc_crt     = axd }
      in
        { puc_active    = Some (active, ctxt);
          puc_cont      = cont;
          puc_init      = scope.sc_env; }
    in
      { scope with sc_pr_uc = Some puc }

  (* ------------------------------------------------------------------ *)
  let rec add_r (scope : scope) (mode : proofmode) (ax : paxiom located) =
    assert (scope.sc_pr_uc = None);

    let env = env scope in
    let loc = ax.pl_loc and ax = ax.pl_desc in
    let ue  = TT.transtyvars env (loc, ax.pa_tyvars) in

    let (pconcl, tintro) =
      match ax.pa_vars with
      | None ->
          (ax.pa_formula, [])
      | Some vs ->
          let pconcl = mk_loc loc (PFforall (vs, ax.pa_formula)) in
          (pconcl, List.flatten (List.map fst vs))
    in

    let ip =
      let ip x = x |> omap (fun x -> `Named (unloc x)) |> odfl `Clear in
      List.map (lmap (fun x -> IPCore (ip x))) tintro in
    let tintro = mk_loc loc (Plogic (Pmove prevertv0)) in
    let tintro = { pt_core = tintro; pt_intros = [`Ip ip]; } in

    let concl = TT.trans_prop env ue pconcl in

    if not (EcUnify.UniEnv.closed ue) then
      hierror "the formula contains free type variables";

    let uidmap = EcUnify.UniEnv.close ue in
    let fs = Tuni.subst uidmap in
    let concl   = Fsubst.f_subst fs concl in
    let tparams = EcUnify.UniEnv.tparams ue in

    let axd  =
      let kind =
        match ax.pa_kind with
        | PAxiom tags -> `Axiom (Ssym.of_list (List.map unloc tags), false)
        | _ -> `Lemma

      in { ax_tparams = tparams;
           ax_spec    = concl;
           ax_kind    = kind;
           ax_loca    = ax.pa_locality;
           ax_smt     = true; }
    in

    match ax.pa_kind with
    | PLemma tc -> begin
        let local =
          match ax.pa_locality with
          | `Declare -> hierror ~loc "cannot mark with `declare` a lemma"
          | `Local   -> true
          | `Global  -> false in

        let check    = Check_mode.check scope.sc_options in
        let pucflags = { puc_smt = axd.ax_smt; puc_local = local; } in
        let pucflags = (([], None), pucflags) in

        match tc with
        | None ->
            let scope =
              start_lemma scope ~name:(unloc ax.pa_name)
                pucflags check (axd, None) in
            let scope = snd (Tactics.process1_r false `Check scope tintro) in
            None, scope

        | Some tc ->
            start_lemma_with_proof scope
              (Some tintro) pucflags (mode, mk_loc loc tc) check
              ~name:(unloc ax.pa_name) axd
      end

    | PAxiom _ ->
        (Some (unloc ax.pa_name), bind scope (unloc ax.pa_name, axd))

  (* ------------------------------------------------------------------ *)
  and add_defer (scope : scope) proofs =
    match proofs with
    | [] -> scope
    | _  ->
        assert (scope.sc_pr_uc = None);
        let puc = { puc_active = None;
                    puc_cont   = (proofs, Some scope.sc_env);
                    puc_init   = scope.sc_env; }
        in { scope with sc_pr_uc = Some puc; }

  (* ------------------------------------------------------------------ *)
  and save_r ?(mode = `Save) scope =
    let puc = oget scope.sc_pr_uc in
    let pac, pct =
      match puc.puc_active with
      | None -> hierror "no active lemma"
      | Some (pac, pct) -> begin
          match pac.puc_jdg with
          | PSNoCheck -> ()
          | PSCheck _ when mode <> `Save -> ()
          | PSCheck pf -> begin
              if not (EcCoreGoal.closed pf) then
                hierror "cannot save an incomplete proof"
          end
      end; (pac, pct)
    in

    let scope = { scope with
      sc_pr_uc = Some { puc with puc_active = None; } }
    in

    let puc =
      if mode = `Abort then pct
        |> omap (fun pct ->
          { puc with puc_cont =
              fst_map (fun x -> pct :: x) puc.puc_cont })
        |> odfl puc
      else puc in

    let puc   = { puc with puc_active = None; } in
    let scope = { scope with sc_pr_uc = Some puc } in

    let scope =
      match fst puc.puc_cont with
      | [] -> { scope with sc_pr_uc = None; }
      | _  -> scope
    in

    match mode with
    | `Save | `Admit ->
      let scope =
        match snd puc.puc_cont with
        | Some e ->
            { scope with sc_env = e }

        | None ->
            let bind name scope = bind scope (name, pac.puc_crt) in
            pac.puc_name |> ofold bind scope

      in (pac.puc_name, scope)

    | `Abort ->
         (None, { scope with sc_env = puc.puc_init })

  (* ------------------------------------------------------------------ *)
  and start_lemma_with_proof scope tintro pucflags (mode, tc) check ?name axd =
    let { pl_loc = loc; pl_desc = tc } = tc in

    let scope = start_lemma scope pucflags check ?name (axd, None) in
    let scope =
      tintro |> ofold
        (fun t sc -> snd (Tactics.process1_r false `Check sc t))
        scope in
    let scope = Tactics.proof scope in

    let tc =
      match tc with
      | Some tc -> tc
      | None    ->
          let dtc = { pl_loc = loc; pl_desc = Pby None; } in
          [{ pt_core = dtc; pt_intros = []; }]
    in

    let tc = { pl_loc = loc; pl_desc = Pby (Some tc) } in
    let tc = { pt_core = tc; pt_intros = []; } in

    let _, scope = Tactics.process_r false mode scope [tc] in
    save_r scope

  (* ------------------------------------------------------------------ *)
  let save ?(src : string option) scope =
    check_state `InProof "save" scope;

    let scope =
      { scope with
          sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc; }
    in
    save_r ~mode:`Save scope

  (* ------------------------------------------------------------------ *)
  let admit ?(src : string option) scope =
    check_state `InProof "admitted" scope;

    let scope =
      { scope with
          sc_locdoc =
            match src with
            | Some src -> DocState.push_srcbl scope.sc_locdoc src
            | None -> scope.sc_locdoc; }
    in

    save_r ~mode:`Admit scope

  (* ------------------------------------------------------------------ *)
  let abort ?(src : string option) scope =
    check_state `InProof "abort" scope;

    let scope =
      { scope with
          sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc; }
    in

    snd (save_r ~mode:`Abort scope)

  (* ------------------------------------------------------------------ *)
  let add ?(src : string option) (scope : scope) (mode : proofmode) (ax : paxiom located) =
    let uax = unloc ax in
    let kind =
      match uax.pa_kind with
      | PLemma _ -> `Lemma
      | _ -> `Axiom
    in
    let scope =
      { scope with
          sc_locdoc =
          match uax.pa_locality with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc (unloc uax.pa_name) kind `Specific
          | `Declare -> DocState.start_process scope.sc_locdoc (unloc uax.pa_name) kind `Abstract}
    in
    let scope =
      { scope with
          sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc; }
    in
    add_r scope mode ax

  (* ------------------------------------------------------------------ *)
  let realize (scope : scope) (mode : proofmode) (rl : prealize located) =
    check_state `InProof "activate" scope;

    let loc = rl.pl_loc and rl = rl.pl_desc in
    let qn  = EcPath.fromqsymbol (unloc rl.pr_name) in

    let puc = oget scope.sc_pr_uc in
    let _ =
      match puc.puc_active with
      | Some _ -> hierror "a lemma is already active"
      | None -> ()
    in

    let (((axname, ax), _, axenv) as st, proofs) =
      let rec doit past proofs =
        match proofs with
        | [] -> hierror "no such lemma: `%s'" (EcPath.tostring qn)
        | (((_, _), p, _) as st) :: proofs ->
            match EcPath.p_equal p qn with
            | false -> doit (st :: past) proofs
            | true  -> (st, List.rev_append past proofs)
      in
        doit [] (fst puc.puc_cont)
    in
    let pucflags = { puc_smt = ax.ax_smt; puc_local = false; } in
    let pucflags = ((proofs, snd puc.puc_cont), pucflags) in
    let check    = Check_mode.check scope.sc_options in

    let scope = { scope with sc_env = axenv } in

    match rl.pr_proof with
    | None ->
        None, start_lemma scope pucflags check ?name:axname (ax, Some st)

    | Some tc ->
        start_lemma_with_proof scope
          None pucflags (mode, mk_loc loc tc) check
          ?name:axname ax
end

(* -------------------------------------------------------------------- *)
module Op = struct
  open EcTypes
  open EcDecl
  open EcFol

  module TT  = EcTyping
  module EHI = EcHiInductive

  let bind ?(import = true) (scope : scope) ((x, op) : _ * operator) =
    assert (scope.sc_pr_uc = None);
    let item = EcTheory.mkitem ~import (EcTheory.Th_operator (x, op)) in
    { scope with sc_env =
        EcSection.add_item item scope.sc_env;
        sc_locdoc = DocState.add_item scope.sc_locdoc; }

  let add ?(src : string option) (scope : scope) (op : poperator located) =
    assert (scope.sc_pr_uc = None);

    let uop = unloc op in
    let scope =
      { scope with
          sc_locdoc =
          match uop.po_locality with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Specific
          | `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.po_name) `Operator `Abstract }
    in
    let scope =
      { scope with
        sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc; }
    in

    let op = op.pl_desc and loc = op.pl_loc in
    let eenv = env scope in
    let ue = TT.transtyvars eenv (loc, op.po_tyvars) in
    let lc = op.po_locality in
    let args = fst op.po_args @ odfl [] (snd op.po_args) in
    let (ty, body, refts) =
      match op.po_def with
      | PO_abstr pty ->
          let codom = TT.transty TT.tp_relax eenv ue pty in
          let xs    = snd (TT.trans_binding eenv ue args) in
          (EcTypes.toarrow (List.map snd xs) codom, `Abstract, [])

      | PO_concr (pty, pf) ->
          let codom   = TT.transty TT.tp_relax eenv ue pty in
          let env, xs = TT.trans_binding eenv ue args in
          let body    = TT.trans_form env ue pf codom in
          let lam     = f_lambda (List.map (fun (x, ty) -> (x, GTty ty)) xs) body in
          (lam.f_ty, `Plain lam, [])

      | PO_case (pty, pbs) -> begin
          let name = { pl_loc = loc; pl_desc = unloc op.po_name } in
          match EHI.trans_matchfix eenv ue name (args, pty, pbs) with
          | (ty, opinfo) -> (ty, `Fix opinfo, [])
        end

      | PO_reft (pty, (rname, reft)) ->
          let env      = env scope in
          let codom    = TT.transty TT.tp_relax eenv ue pty in
          let _env, xs = TT.trans_binding eenv ue args in
          let opty     = EcTypes.toarrow (List.map snd xs) codom in
          let opabs    = EcDecl.mk_op ~opaque:optransparent [] codom None lc in
          let openv    = EcEnv.Op.bind (unloc op.po_name) opabs env in
          let openv    = EcEnv.Var.bind_locals xs openv in
          let reft     = TT.trans_prop openv ue reft in
          (opty, `Abstract, [(rname, xs, reft, codom)])
    in

    if not (EcUnify.UniEnv.closed ue) then
      hierror ~loc "this operator type contains free type variables";

    let uidmap  = EcUnify.UniEnv.close ue in
    let ts      = Tuni.subst uidmap in
    let fs      = Fsubst.f_subst ts in
    let ty      = ty_subst ts ty in
    let tparams = EcUnify.UniEnv.tparams ue in
    let body    =
      match body with
      | `Abstract -> None
      | `Plain e  -> Some (OP_Plain (fs e))
      | `Fix opfx ->
          Some (OP_Fix {
            opf_recp     = EcPath.pqname (EcEnv.root eenv) (EcIdent.name opfx.EHI.mf_name);
            opf_args     = opfx.EHI.mf_args;
            opf_resty    = opfx.EHI.mf_codom;
            opf_struct   = (opfx.EHI.mf_recs, List.length opfx.EHI.mf_args);
            opf_branches = opfx.EHI.mf_branches;
          })

    in

    let tags   = Sstr.of_list (List.map unloc op.po_tags) in
    let opaque = {
      smt       = Sstr.mem "smt_opaque" tags;
      reduction = Sstr.mem "opaque" tags
    } in
    let unfold =
      match op.po_args with
      | (a, Some _) -> Some (List.length a)
      | (_, None) -> None in

    let tyop   = EcDecl.mk_op ~opaque ?unfold tparams ty body lc in
    let opname = EcPath.pqname (EcEnv.root eenv) (unloc op.po_name) in

    if op.po_kind = `Const then begin
      let tue   = EcUnify.UniEnv.copy ue in
      let ty, _ = EcUnify.UniEnv.openty tue tparams None ty in
      let tdom  = EcUnify.UniEnv.fresh tue in
      let tcom  = EcUnify.UniEnv.fresh tue in
      let tfun  = EcTypes.tfun tdom tcom in

        try
          EcUnify.unify eenv tue ty tfun;
          let msg = "this operator type is (unifiable) to a function type" in
            hierror ~loc "%s" msg
        with EcUnify.UnificationFailure _ -> ()
    end;

    let scope =
      match op.po_ax with
      | None    -> bind scope (unloc op.po_name, tyop)
      | Some ax -> begin
          match tyop.op_kind with
          | OB_oper (Some (OP_Plain bd)) ->
              let path  = EcPath.pqname (path scope) (unloc op.po_name) in
              let axop  =
                let nargs = List.sum (List.map (List.length -| fst) args) in
                  EcDecl.axiomatized_op ~nargs path (tyop.op_tparams, bd) lc in
              let tyop  = { tyop with op_opaque = { reduction = true; smt = false; }} in
              let scope = bind scope (unloc op.po_name, tyop) in
              Ax.bind scope (unloc ax, axop)

          | _ -> hierror ~loc "cannot axiomatize non-plain operators"
      end
    in

    let scope =
      List.fold_left (fun scope (rname, xs, ax, codom) ->
          let ax =
            let opargs  = List.map (fun (x, xty) -> e_local x xty) xs in
            let opapp   = List.map tvar tparams in
            let opapp   = e_app (e_op opname opapp ty) opargs codom in

            let subst   = EcSubst.add_opdef EcSubst.empty opname ([], opapp) in
            let ax      = EcSubst.subst_form subst ax in
            let ax      = f_forall (List.map (snd_map gtty) xs) ax in

            let uidmap  = EcUnify.UniEnv.close ue in
            let subst   = Tuni.subst uidmap in
            let ax      = Fsubst.f_subst subst ax in

            ax
          in

          let ax, axpm =
            let bdpm = tparams in
            let axpm = List.map EcIdent.fresh bdpm in
              (Tvar.f_subst ~freshen:true bdpm (List.map EcTypes.tvar axpm) ax,
               axpm) in
          let ax =
            { ax_tparams = axpm;
              ax_spec    = ax;
              ax_kind    = `Axiom (Ssym.empty, false);
              ax_loca    = lc;
              ax_smt     = true; }
          in Ax.bind scope (unloc rname, ax))
        scope refts
    in

    let scope =
      if not (List.is_empty op.po_aliases) then begin
        if not (EcUtils.is_none body) || not (List.is_empty refts) then
          hierror ~loc
            "multiple names are only allowed for non-refined abstract operators";
        let addnew scope name =
          let nparams = List.map EcIdent.fresh tparams in
          let subst = Tvar.init
            tparams
            (List.map tvar nparams) in
          let rop = EcDecl.mk_op ~opaque:optransparent nparams (Tvar.subst subst ty) None lc in
          bind scope (unloc name, rop)
        in List.fold_left addnew scope op.po_aliases

      end else scope
    in

    let axs = ref [] in

    let add_distr_tag
        (pred : path) (bases : string list) (tag : string) (suffix : string) scope
    =
      if not (EcAlgTactic.is_module_loaded (env scope)) then
        hierror "for tag %s, load Distr first" tag;

      let oppath   = EcPath.pqname (path scope) (unloc op.po_name) in
      let nparams  = List.map EcIdent.fresh tyop.op_tparams in
      let subst    = Tvar.init tyop.op_tparams (List.map tvar nparams) in
      let ty       = Tvar.subst subst tyop.op_ty in
      let aty, rty = EcTypes.tyfun_flat ty in

      let dty =
        match EcTypes.as_tdistr (EcEnv.ty_hnorm rty (env scope)) with
        | None -> hierror ~loc "[%s] can only be applied to distributions" tag
        | Some dty -> dty
      in

      let bds = List.combine (List.map EcTypes.fresh_id_of_ty aty) aty in
      let ax  = EcFol.f_op oppath (List.map tvar nparams) ty in
      let ax  = EcFol.f_app ax (List.map (curry f_local) bds) rty in
      let ax  = EcFol.f_app (EcFol.f_op pred [dty] (tfun rty tbool)) [ax] tbool in
      let ax  = EcFol.f_forall (List.map (snd_map gtty) bds) ax in

      let ax =
        { ax_tparams = nparams;
          ax_spec    = ax;
          ax_kind    = `Axiom (Ssym.empty, false);
          ax_loca    = lc;
          ax_smt     = true; } in

      let scope, axname =
        let axname = Printf.sprintf "%s_%s" (unloc op.po_name) suffix in
        (Ax.bind scope (axname, ax), axname) in

      axs := axname :: !axs;

      let axpath = EcPath.pqname (path scope) axname in

      List.fold_left
        (fun scope base ->
            Auto.bind_hint
              ~local:(local_of_locality lc) ~level:0 ~base scope
              [(axpath, `Default)])
        scope bases

    in

    let scope =
      if   Sstr.mem "lossless" tags
      then add_distr_tag EcCoreLib.CI_Distr.p_lossless
             [EcCoreLib.base_ll; EcCoreLib.base_rnd] "lossless" "ll" scope
      else scope in

    let scope =
      if   Sstr.mem "uniform" tags
      then add_distr_tag EcCoreLib.CI_Distr.p_uniform
             [EcCoreLib.base_rnd] "uniform" "uni" scope
      else scope in

    let scope =
      if   Sstr.mem "full" tags
      then add_distr_tag EcCoreLib.CI_Distr.p_full
             [EcCoreLib.base_rnd] "full" "fu" scope
      else scope in

    tyop, List.rev !axs, scope


  let add_opsem ?(src : string option) (scope : scope) (op : pprocop located) =
    let module Sem = EcProcSem in

    let uop = unloc op in
    let scope =
      { scope with
          sc_locdoc =
          match uop.ppo_locality with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Specific
          | `Declare -> DocState.start_process scope.sc_locdoc (unloc uop.ppo_name) `Operator `Abstract }
    in
    let scope =
      { scope with
        sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc; }
    in

    let op = unloc op in
    let f  = EcTyping.trans_gamepath (env scope) op.ppo_target  in
    let sig_, body =
      let f = EcEnv.Fun.by_xpath f (env scope) in
      let body =
        match f.f_def with
        | FBdef body -> body
        | _ -> raise Sem.SemNotSupported in

        (f.f_sig, body) in

    let ret = oget ~exn:Sem.SemNotSupported body.f_ret in

    let params =
      let for1 (v : ovariable) =
        (oget ~exn:Sem.SemNotSupported v.ov_name, v.ov_type) in
      List.map for1 sig_.fs_anames in

    let env = Sem.Env.empty (env scope) in
    let env, ids = List.fold_left_map Sem.Env.fresh env (List.fst params) in

    let cont (env : Sem.senv) =
      (`Det, Sem.translate_e env ret) in

    let mode, aout = Sem.translate_s env cont body.f_body in
    let aout = form_of_expr aout in (* FIXME: translate to forms directly? *)
    let aout = f_lambda (List.map2 (fun (_, ty) x -> (x, GTty ty)) params ids) aout in

    let opdecl = EcDecl.{
      op_tparams  = [];
      op_ty       = aout.f_ty;
      op_kind     = OB_oper (Some (OP_Plain aout));
      op_loca     = op.ppo_locality;
      op_opaque   = optransparent;
      op_clinline = false;
      op_unfold   = None;
    } in

    let oppath = EcPath.pqname (path scope) (unloc op.ppo_name) in

    let scope = bind scope (unloc op.ppo_name, opdecl) in

    let scope =
      let prax =
        let locs  = List.map (fun (x, ty) -> (EcIdent.create x, ty)) params in
        let prmem = EcIdent.create "&m" in
        let res   = f_pvar pv_res sig_.fs_ret prmem in
        let resx  = EcIdent.create "v" in
        let resv  = f_local resx sig_.fs_ret in

        let mu =
          let sem =
            f_app
              (f_op oppath [] opdecl.op_ty)
              (List.map (fun (x, ty) -> f_local x ty) locs)
              (match mode with `Det -> sig_.fs_ret | `Distr -> tdistr sig_.fs_ret) in

          match mode with
          | `Det ->
             f_if (f_eq sem resv) f_r1 f_r0

          | `Distr ->
             f_mu_x sem resv
        in

        f_forall
          [(prmem, GTmem EcMemory.abstract_mt)]
          (f_forall
             (List.map (fun (x, ty) -> (x, GTty ty)) ((resx, sig_.fs_ret) :: locs))
             (f_eq
                (f_pr prmem
                   f
                   (f_tuple (List.map (fun (x, ty) -> f_local x ty) locs))
                   (map_ss_inv1 (fun r -> f_eq r resv) res))
                mu))
      in

      let prax = EcDecl.{
        ax_tparams = [];
        ax_spec    = prax;
        ax_kind    = `Lemma;
        ax_loca    = op.ppo_locality;
        ax_smt     = true;
      } in

      Ax.bind scope (unloc op.ppo_name ^ "_opsem", prax) in

    let scope =
      match mode with
      | `Det ->
         let hax =
           let locs  = List.map (fun (x, ty) -> (EcIdent.create x, ty)) params in
           let m = EcIdent.create "&hr" in
           let res   = f_pvar pv_res sig_.fs_ret m in
           let args  = f_pvar pv_arg sig_.fs_arg m in

           let post =
             f_eq
               res.inv
               (f_app
                  (f_op oppath [] opdecl.op_ty)
                  (List.map (fun (x, ty) -> f_local x ty) locs)
                  sig_.fs_ret)
           in
           f_forall
             (List.map (fun (x, ty) -> (x, GTty ty)) locs)
             (f_hoareF
                {m;inv=(f_eq
                   args.inv
                   (f_tuple (List.map (fun (x, ty) -> f_local x ty) locs)))}
                f
                {hsi_m=m;hsi_inv= POE.empty post})
         in

         let prax = EcDecl.{
           ax_tparams = [];
           ax_spec    = hax;
           ax_kind    = `Lemma;
           ax_loca    = op.ppo_locality;
           ax_smt     = true;
         } in

         Ax.bind scope (unloc op.ppo_name ^ "_opsem_det", prax)

      | `Distr ->
         scope
    in

    scope
end

(* -------------------------------------------------------------------- *)
module Exception = struct
  module TT = EcTyping

  let bind ?(import = true) (scope : scope) (x, e) =
    assert (scope.sc_pr_uc = None);
    let op = operator_of_exception e in
    Op.bind ~import scope (x, op)

  let add (scope : scope) (pe : pexception_decl located) =
    assert (scope.sc_pr_uc = None);
    let loc = loc pe in
    let pe = pe.pl_desc in
    let lc = pe.pe_locality in
    let eenv = env scope in
    let ue = TT.transtyvars eenv (loc, Some []) in
    let e_dom = transtys tp_nothing eenv ue pe.pe_dom in
    let tparams = EcUnify.UniEnv.tparams ue in
    if tparams <> [] then
      hierror ~loc "Polymorphic expression are not allowed";
    let e   = EcDecl.mk_exception lc e_dom in
    let scope = bind scope (unloc pe.pe_name, e) in
    e, scope
end

(* -------------------------------------------------------------------- *)
module Pred = struct
  module TT = EcTyping

  let add ?(src : string option) (scope : scope) (pr : ppredicate located) =
    assert (scope.sc_pr_uc = None);

    let upr = unloc pr in
    let scope =
      { scope with
          sc_locdoc =
          match upr.pp_locality with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Specific
          | `Declare -> DocState.start_process scope.sc_locdoc (unloc upr.pp_name) `Operator `Abstract }
    in
    let scope =
      { scope with
        sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc;  }
    in

    let typr  = EcHiPredicates.trans_preddecl (env scope) pr in
    let scope = Op.bind scope (unloc (unloc pr).pp_name, typr) in
    typr, scope
end

(* -------------------------------------------------------------------- *)
module Notations = struct
  module TT  = EcTyping

  let add (scope : scope) (nt : pnotation located) =
    EcHiNotations.trans_notation (env scope) nt; scope

  let add_abbrev (scope : scope) (ab : pabbrev located) =
    let op = EcHiNotations.trans_abbrev (env scope) ab in
    Op.bind scope op
end

(* -------------------------------------------------------------------- *)
module Mod = struct
  module TT = EcTyping

  let bind ?(import = true) (scope : scope) (m : top_module_expr) =
    assert (scope.sc_pr_uc = None);
    let item = EcTheory.mkitem ~import (EcTheory.Th_module m) in
    { scope with
        sc_env = EcSection.add_item item scope.sc_env;
        sc_locdoc = DocState.add_item scope.sc_locdoc; }

  let add_concrete ?(src : string option) (scope : scope) lc (ptm : pmodule_def) =
    assert (scope.sc_pr_uc = None);

    if lc = `Declare then
      hierror "cannot use [declare] for concrete modules";

    let nm = unloc (EcParsetree.pcmhd_ident ptm.ptm_header) in

    let scope =
      { scope with
          sc_locdoc =
          match lc with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc nm `Module `Specific
          | `Declare -> DocState.start_process scope.sc_locdoc nm `Module `Abstract }
    in
    let scope =
      { scope with
        sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc;  }
    in

    let m = TT.transmod (env scope) ~attop:true ptm in
    let ur = EcModules.get_uninit_read_of_module (path scope) m in

    if not (List.is_empty ur) then begin
      let ppe = EcPrinting.PPEnv.ofenv (env scope) in
      let pp fmt (xp, names) =
        Format.fprintf fmt "  - %a -> [%a]"
          (EcPrinting.pp_funname ppe) (xastrip xp)
          (EcPrinting.pp_list ", " pp_symbol)
          (Ssym.elements names)
      in

      notify scope `Warning
        "these procedures may use uninitialized local variables:@\n@[<v>%a@]"
        (EcPrinting.pp_list "@," pp) ur
    end;

    bind scope {tme_expr = m; tme_loca = lc}

  let declare (scope : scope) (m : pmodule_decl) =
    let modty = m.ptm_modty in
    let name  = EcIdent.create (unloc m.ptm_name) in
    let tysig = fst (TT.transmodtype (env scope) modty.pmty_pq) in
    (* We modify tysig restrictions according if necessary. *)
    let tysig = trans_restr_for_modty (env scope) tysig modty.pmty_mem in

    { scope with
        sc_env = EcSection.add_decl_mod name tysig scope.sc_env }

  let add ?(src : string option) (scope : scope) (m : pmodule_def_or_decl) =
    match m with
    | { ptm_locality = lc; ptm_def = `Concrete def } ->
      add_concrete ?src scope lc def

    | { ptm_locality = lc; ptm_def = `Abstract decl } ->
      if lc <> `Declare then
        hierror "use declare for abstract module";
      declare scope decl

  let import (scope : scope) (m : pmsymbol located) : scope =
    let m, _ = EcTyping.trans_msymbol (env scope) m in
    { scope with sc_env = EcSection.import_vars m scope.sc_env }

end

(* -------------------------------------------------------------------- *)
module ModType = struct
  let bind
        ?(import = true) (scope : scope)
        ((x, tysig) : _ * top_module_sig)
  =
    assert (scope.sc_pr_uc = None);
    let item = EcTheory.mkitem ~import (EcTheory.Th_modtype (x, tysig)) in
    { scope with
        sc_env = EcSection.add_item item scope.sc_env;
        sc_locdoc = DocState.add_item scope.sc_locdoc; }

  let add ?(src : string option) (scope : scope) (intf : pinterface) =
    assert (scope.sc_pr_uc = None);

    let scope =
      { scope with
          sc_locdoc =
          match intf.pi_locality with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc (unloc intf.pi_name) `ModuleType `Specific }
    in
    let scope =
      { scope with
        sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc;  }
    in
    let tysig = EcTyping.transmodsig (env scope) intf in
    bind scope (unloc intf.pi_name, tysig)
end

(* -------------------------------------------------------------------- *)
module Theory = struct
  open EcTheory

  exception TopScope

  (* ------------------------------------------------------------------ *)
  let bind ?(import = true) (scope : scope) (cth : thloaded) =
    assert (scope.sc_pr_uc = None);
    { scope with
        sc_env = EcSection.add_th ~import cth scope.sc_env }

  (* ------------------------------------------------------------------ *)
  let required (scope : scope) (rqd : required_info) =
    assert (scope.sc_pr_uc = None);
    List.exists (fun x ->
        if x.rqd_name = rqd.rqd_name then (
          if (x.rqd_digest <> rqd.rqd_digest) then begin
            let fullname (ri : required_info) =
              let namespace =
                ri.rqd_namespace
                |> Option.map EcLoader.string_of_namespace
                |> Option.map (fun s -> s ^ ":")
                |> Option.value ~default:"" in
              namespace ^ ri.rqd_name in
            hierror
              "Digest mismatch, file %s differs from %s"
              (fullname x) (fullname rqd)
          end;
          true)
        else false)
      scope.sc_required

  (* ------------------------------------------------------------------ *)
  let mark_as_direct (scope : scope) (name : symbol) =
    let for1 rq =
      if   rq.rqd_name = name
      then { rq with rqd_direct = true }
      else rq
    in { scope with sc_required = List.map for1 scope.sc_required }

  (* ------------------------------------------------------------------ *)
  let enter ?(src : string option) (scope : scope) (mode : thmode) (name : symbol) =
    assert (scope.sc_pr_uc = None);
    let sc_locdoc = scope.sc_locdoc in
    let sc_locdoc =
      match src with
      | None -> DocState.prevent_process scope.sc_locdoc
      | Some src ->
         let sc_locdoc =
           DocState.start_process sc_locdoc name `Theory
             (match mode with `Concrete -> `Specific | `Abstract -> `Abstract)
         in
         DocState.push_srcbl sc_locdoc src
    in
    let
      scope = { scope with sc_locdoc }
    in

    subscope scope mode name

  (* ------------------------------------------------------------------ *)
  let rec require_loaded (id : required_info) scope =
    if required scope id then
      scope
    else
      match Msym.find_opt id.rqd_name scope.sc_loaded with
      | Some (rth, ids) ->
          let scope = List.fold_right require_loaded ids scope in
          let env   = EcSection.require rth scope.sc_env in
            { scope with
                sc_env      = env;
                sc_required = id :: scope.sc_required; }

      | None -> assert false

  (* ------------------------------------------------------------------ *)
  let update_with_required ~(dst : scope) ~(src : scope) =
    let dst =
      let sc_loaded =
        Msym.union
          (fun _ x y -> assert (x ==(*phy*) y); Some x)
          dst.sc_loaded src.sc_loaded
      in { dst with sc_loaded }
    in List.fold_right require_loaded src.sc_required dst

  (* ------------------------------------------------------------------ *)
  let add_clears clears scope =
    let clears =
      let for1 = function
        | None -> EcEnv.root (env scope)
        | Some { pl_loc = loc; pl_desc = (xs, x) as q } ->
          let xp = EcEnv.root (env scope) in
          let xp = EcPath.pqname (EcPath.extend xp xs) x in
          if is_none (EcEnv.Theory.by_path_opt xp (env scope)) then
            hierror ~loc "unknown theory: `%s`" (string_of_qsymbol q);
          xp
      in List.map for1 clears
    in { scope with sc_clears = scope.sc_clears @ clears }

  (* -------------------------------------------------------------------- *)
  let exit_r ?pempty (scope : scope) =
    match scope.sc_top with
    | None     -> raise TopScope
    | Some sup ->
      let clears   = scope.sc_clears in
      let _, cth, _ = EcSection.exit_theory ?pempty ~clears scope.sc_env in
      let loaded   = scope.sc_loaded in
      let required = scope.sc_required in
      let sup = {
        sup with
          sc_loaded = loaded;
          sc_locdoc = DocState.add_sub sup.sc_locdoc scope.sc_locdoc} in
      ((cth, required), scope.sc_name, sup)

  (* ------------------------------------------------------------------ *)
  let exit ?import ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
    assert (scope.sc_pr_uc = None);

    let cth = exit_r ~pempty (add_clears clears scope) in
    let ((cth, required), (name, _), scope) = cth in
    let scope = List.fold_right require_loaded required scope in
    let scope = ofold (fun cth scope -> bind ?import scope cth) scope cth in
    (name, scope)

  (* ------------------------------------------------------------------ *)
  let bump_prelude (scope : scope) =
    match scope.sc_prelude with
    | `InPrelude, _ ->
         { scope with sc_prelude = (`InPrelude,
             { pr_env      = env scope;
               pr_required = scope.sc_required; }) }
    | _ -> scope

  (* ------------------------------------------------------------------ *)
  let import (scope : scope) (name : qsymbol) =
    assert (scope.sc_pr_uc = None);

    match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with
    | None ->
        hierror
          "cannot import the non-existent theory `%s'"
          (string_of_qsymbol name)

    | Some (path, cth) ->
      if cth.cth_mode = `Abstract then
        hierror "cannot import an abstract theory";
      bump_prelude
        { scope with
          sc_env = EcSection.import path scope.sc_env }

  (* ------------------------------------------------------------------ *)
  let export_p scope (p, lc) =
    let item = mkitem ~import:true (EcTheory.Th_export (p, lc)) in
    { scope with sc_env = EcSection.add_item item scope.sc_env }

  let export (scope : scope) (name : qsymbol) =
    assert (scope.sc_pr_uc = None);

    match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with
    | None ->
        hierror
          "cannot export the non-existent theory `%s'"
          (string_of_qsymbol name)

    | Some (path, cth) ->
      if cth.cth_mode = `Abstract then
        hierror "cannot export an abstract theory";
      (* The section will fix the locality *)
      bump_prelude (export_p scope (path, `Global))

  (* ------------------------------------------------------------------ *)
  let check_end_required scope thname =
    if fst scope.sc_name <> thname then
      hierror "end-of-file while processing external theory %s %s"
        (fst scope.sc_name) thname;
    if scope.sc_pr_uc <> None then
      hierror
        "end-of-file while processing proof %s" (fst scope.sc_name)

  (* -------------------------------------------------------------------- *)
  let require_start (scope : scope) (thname : symbol) (mode : thmode)
        : scope =
    let new_ = enter (for_loading scope) mode thname `Global in
    { new_ with sc_env = EcSection.astop new_.sc_env }

  let require_finish ?(old : scope option = None) ~(new_ : scope)
      (ri : required_info) : scope =
    let (cth, rqs), (name1, _), new_ = exit_r ~pempty:`No new_ in
    assert (ri.rqd_name = name1);
    let scope =
      { (odfl new_ old) with sc_loaded =
          Msym.add ri.rqd_name (oget cth, rqs) new_.sc_loaded; } in
    bump_prelude (require_loaded ri scope)

  let require (scope : scope) ((name, mode) : required_info * thmode) loader =
    assert (scope.sc_pr_uc = None);

    if required scope name then begin
      if   name.rqd_direct
      then mark_as_direct scope name.rqd_name
      else scope
    end else
      match Msym.find_opt name.rqd_name scope.sc_loaded with
      | Some _ -> require_loaded name scope
      | None ->
        try
          let imported = require_start scope name.rqd_name mode in
          let thname   = fst imported.sc_name in
          let imported = loader imported in
          check_end_required imported thname;
          require_finish ~old:(Some scope) ~new_:imported name
        with e -> begin
          match toperror_of_exn_r e with
          | Some (l, e) when not (EcLocation.isdummy l) ->
              raise (ImportError (Some l, name.rqd_name, e))
          | _ ->
              raise (ImportError (None, name.rqd_name, e))
        end

  (* -------------------------------------------------------------------- *)
  let required scope = scope.sc_required

  (* -------------------------------------------------------------------- *)
  let alias (scope : scope) ((name, target) : psymbol * pqsymbol) =
    let thpath = EcEnv.Theory.lookup_opt (unloc target) (env scope) in
    let thpath, _ = ofdfl (fun () ->
      hierror ~loc:(loc target) "unknown theory: %a" pp_qsymbol (unloc target)
    ) thpath in
    let item = EcTheory.mkitem ~import:true (Th_alias (unloc name, thpath)) in

    { scope with sc_env = EcSection.add_item item scope.sc_env }
end

(* -------------------------------------------------------------------- *)
module Section = struct
  module T = EcTheory

  let enter (scope : scope) (name : psymbol option) =
    assert (scope.sc_pr_uc = None);
    { scope with
      sc_env = EcSection.enter_section (omap unloc name) scope.sc_env }

  let exit (scope : scope) (name : psymbol option) =
    let sc_env = EcSection.exit_section (omap unloc name) scope.sc_env in
    { scope with sc_env }
end

(* -------------------------------------------------------------------- *)
module Reduction = struct
  (* FIXME: section -> allow "local" flag *)
  let add_reduction scope (opts, reds) =
    check_state `InTop "hint simplify" scope;

    let rules =
      let for1 idx name =
        let idx  = odfl 0 idx in
        let ax_p = EcEnv.Ax.lookup_path (unloc name) (env scope) in
        let opts = EcTheory.{
          ur_delta  = List.mem `Delta  opts;
          ur_eqtrue = List.mem `EqTrue opts;
        } in

        let red_info =
          EcReduction.User.compile ~opts ~prio:idx (env scope) ax_p in
        (ax_p, opts, Some red_info) in

      let rules = List.map (fun (xs, idx) -> List.map (for1 idx) xs) reds in
      List.flatten rules

    in

    let item = EcTheory.mkitem ~import:true (EcTheory.Th_reduction rules) in
    { scope with sc_env = EcSection.add_item item scope.sc_env }
end

(* -------------------------------------------------------------------- *)
module Cloning = struct
  (* ------------------------------------------------------------------ *)
  open EcTheory
  open EcThCloning

  module C = EcThCloning
  module R = EcTheoryReplay

  (* ------------------------------------------------------------------ *)
  let hooks ~(override_locality: is_local option) : scope R.ovrhooks =
    let thexit sc ~import pempty =
      snd (Theory.exit ~import ?clears:None ~pempty sc) in
    let add_item scope ~import item =
      let item = EcTheory.mkitem ~import item in
      { scope with sc_env = EcSection.add_item ~override_locality item scope.sc_env } in
    { R.henv      = (fun scope -> scope.sc_env);
      R.hadd_item = add_item;
      R.hthenter  = Theory.enter;
      R.hthexit   = thexit;
      R.herr      = (fun ?loc -> hierror ?loc "%s"); }

  (* ------------------------------------------------------------------ *)
  module Options = struct
    open EcTheoryReplay

    let default = { clo_abstract = false; }

    let merge1 opts (b, (x : theory_cloning_option)) =
      match x with
      | `Abstract -> { opts with clo_abstract = b; }

    let merge opts (specs : theory_cloning_options) =
      List.fold_left merge1 opts specs
  end

  (* ------------------------------------------------------------------ *)
  let replay_proofs (scope : scope) (mode : Tactics.proofmode) (proofs : _) =
    proofs |> List.pmap (fun axc ->
      match axc.C.axc_tac with
      | None ->
          Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env)

      | Some pt ->
          let t = { pt_core = pt; pt_intros = []; } in
          let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in
          let t = { pt_core = t; pt_intros = []; } in
          let (x, ax) = axc.C.axc_axiom in

          let pucflags = { puc_smt = true; puc_local = false; } in
          let pucflags = (([], None), pucflags) in
          let check    = Check_mode.check scope.sc_options in

          let escope = { scope with sc_env = axc.C.axc_env; } in
          let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
          let escope = Tactics.proof escope in
          let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
          ignore (Ax.save_r escope); None
    )

  (* ------------------------------------------------------------------ *)
  let clone (scope : scope) mode (thcl : theory_cloning) =
    assert (scope.sc_pr_uc = None);

    let { cl_name   = name;
          cl_theory = (opath, oth);
          cl_clone  = ovrds;
          cl_rename = rnms;
          cl_ntclr  = ntclr; }

        = C.clone scope.sc_env thcl in

    let incl  = thcl.pthc_import = Some `Include in
    let opts  = Options.merge Options.default thcl.pthc_opts in

    if thcl.pthc_import = Some `Include && opts.R.clo_abstract then
      hierror "cannot include an abstract theory";
    if thcl.pthc_import = Some `Include && EcUtils.is_some thcl.pthc_name then
      hierror "cannot give an alias to an included clone";

    let cpath = EcEnv.root (env scope) in
    let npath = if incl then cpath else EcPath.pqname cpath name in

    let (proofs, scope) =
      EcTheoryReplay.replay (hooks ~override_locality:thcl.pthc_local)
        ~abstract:opts.R.clo_abstract ~override_locality:thcl.pthc_local ~incl
        ~clears:ntclr ~renames:rnms ~opath ~npath ovrds
        scope (name, false, oth.cth_items, oth.cth_loca)
    in

    let proofs = replay_proofs scope mode proofs in

    let scope =
      thcl.pthc_import |> ofold (fun flag scope ->
        match flag with
        | `Import  ->
          { scope with sc_env = EcSection.import npath scope.sc_env; }
        | `Export  ->
          let item = EcTheory.mkitem ~import:true (Th_export (npath, `Global)) in
          { scope with sc_env = EcSection.add_item item scope.sc_env; }
        | `Include -> scope)
        scope
    in

    if is_none thcl.pthc_local && oth.cth_loca = `Local then
      notify scope `Info
        "Theory `%s` has inherited `local` visibility. \
         Use the `global` keyword if this is not wanted."
        name;

    Ax.add_defer scope proofs

end

(* -------------------------------------------------------------------- *)
module Ty = struct
  open EcDecl
  open EcTyping

  module TT  = EcTyping
  module ELI = EcInductive
  module EHI = EcHiInductive

  (* ------------------------------------------------------------------ *)
  let check_name_available scope x =
    let pname = EcPath.pqname (EcEnv.root (env scope)) x.pl_desc in

    if    EcEnv.Ty       .by_path_opt pname (env scope) <> None
       || EcEnv.TypeClass.by_path_opt pname (env scope) <> None then
      hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc

  (* ------------------------------------------------------------------ *)
  let bind ?(import = true) (scope : scope) ((x, tydecl) : (_ * tydecl)) =
    assert (scope.sc_pr_uc = None);
    let item = EcTheory.mkitem ~import (EcTheory.Th_type (x, tydecl)) in
    { scope with
        sc_env = EcSection.add_item item scope.sc_env;
        sc_locdoc = DocState.add_item scope.sc_locdoc; }

  (* ------------------------------------------------------------------ *)
  let add ?(src : string option) scope (tyd : ptydecl located) =
    let utyd = unloc tyd in
    let scope =
      { scope with
          sc_locdoc =
          match utyd.pty_locality with
          | `Local -> DocState.prevent_process scope.sc_locdoc
          | `Global -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Specific
          | `Declare -> DocState.start_process scope.sc_locdoc (unloc utyd.pty_name) `Type `Abstract }
    in
    let scope =
      { scope with
        sc_locdoc =
          match src with
          | Some src -> DocState.push_srcbl scope.sc_locdoc src
          | None -> scope.sc_locdoc;  }
    in

    let loc = loc tyd in

    let { pty_name = name; pty_tyvars = args;
          pty_body = body; pty_locality = tyd_loca } = unloc tyd in

    check_name_available scope name;
    let env = env scope in
    let tyd_params, tyd_type =
      match body with
      | PTYD_Abstract ->
        let ue = TT.transtyvars env (loc, Some args) in
        EcUnify.UniEnv.tparams ue, Abstract

      | PTYD_Alias    bd ->
        let ue     = TT.transtyvars env (loc, Some args) in
        let body   = transty tp_tydecl env ue bd in
        EcUnify.UniEnv.tparams ue, Concrete body

      | PTYD_Datatype dt -> (
          let datatype = EHI.trans_datatype env (mk_loc loc (args, name)) dt in
          let ty_from_ctor ctor = EcEnv.Ty.by_path ctor env in
          try
            ELI.check_positivity ty_from_ctor datatype;
            let tparams, tydt = ELI.datatype_as_ty_dtype datatype in
            (tparams, Datatype tydt)
          with ELI.NonPositive ctx ->
            let symbol = basename datatype.dt_path in
            EHI.dterror loc env (EHI.DTE_NonPositive (symbol, ctx)))

      | PTYD_Record rt ->
        let record  = EHI.trans_record env (mk_loc loc (args,name)) rt in
        let scheme  = ELI.indsc_of_record record in
        record.ELI.rc_tparams, Record (scheme, record.ELI.rc_fields)
    in

    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; })

  (* ------------------------------------------------------------------ *)
  let add_subtype (scope : scope) ({ pl_desc = subtype } : psubtype located) =
    let loced x = mk_loc _dummy x in
    let env = env scope in

    let scope =
      let decl = EcDecl.{
        tyd_params  = [];
        tyd_type    = Abstract;
        tyd_loca    = `Global; (* FIXME:SUBTYPE *)
      } in bind scope (unloc subtype.pst_name, decl) in

    let carrier =
      let ue = EcUnify.UniEnv.create None in
      transty tp_tydecl env ue subtype.pst_carrier in

    let pred =
      let x = EcIdent.create (fst subtype.pst_pred).pl_desc in
      let env = EcEnv.Var.bind_local x carrier env in
      let ue = EcUnify.UniEnv.create None in
      let pred = EcTyping.trans_prop env ue (snd subtype.pst_pred) in
      if not (EcUnify.UniEnv.closed ue) then
        hierror ~loc:(snd subtype.pst_pred).pl_loc
          "the predicate contains free type variables";
      let uidmap = EcUnify.UniEnv.close ue in
      let fs = Tuni.subst uidmap in
      f_lambda [(x, GTty carrier)] (Fsubst.f_subst fs pred) in

    let evclone =
      { EcThCloning.evc_empty with
          evc_types = Msym.of_list [
            "T", loced (`Direct carrier, `Inline `Clear);
            "sT", loced (
              `ByPath (EcPath.pqname (EcEnv.root env) (unloc subtype.pst_name)),
              `Inline `Clear
            );
          ];
          evc_ops = Msym.of_list [
            "P", loced (`Direct pred, `Inline `Clear)
          ];
          evc_lemmas = {
            ev_bynames = Msym.empty;
            ev_global  =  [ (None, Some [`Include, "prove"]) ]
          } } in

    let cname = Option.map unloc subtype.pst_cname in
    let npath = ofold ((^~) EcPath.pqname) (EcEnv.root env) cname in
    let cpath = EcPath.fromqsymbol ([EcCoreLib.i_top], "Subtype") in
    let theory = EcEnv.Theory.by_path ~mode:`Abstract cpath env in

    let renames =
      match subtype.pst_rename with
      | None -> []

      | Some (insub, val_) -> [
        (`All, (EcRegexp.regexp "val", EcRegexp.subst val_));
        (`All, (EcRegexp.regexp "insub", EcRegexp.subst insub));
      ] in

    let (proofs, scope) =
      EcTheoryReplay.replay (Cloning.hooks ~override_locality:None)
        ~abstract:false ~override_locality:None ~incl:(Option.is_none cname)
        ~clears:Sp.empty ~renames ~opath:cpath ~npath
        evclone scope
        (
          Option.value ~default:(EcPath.basename cpath) cname,
          false,
          theory.cth_items,
          theory.cth_loca
        ) in

    let proofs = Cloning.replay_proofs scope `Check proofs in

    Ax.add_defer scope proofs

  (* ------------------------------------------------------------------ *)
  let check_tci_operators env tcty ops reqs =
    let ue   = EcUnify.UniEnv.create (Some (fst tcty)) in
    let rmap = Mstr.of_list reqs in

    let ops =
      let tt1 m (x, (tvi, op)) =
        if not (Mstr.mem (unloc x) rmap) then
          hierror ~loc:x.pl_loc "invalid operator name: `%s'" (unloc x);

        let tvi = List.map (TT.transty tp_tydecl env ue) tvi in
        let selected =
          EcUnify.select_op ~filter:(fun _ -> EcDecl.is_oper)
            (Some (EcUnify.TVIunamed tvi)) env (unloc op) ue ([], None)
        in
        let op =
          match selected with
          | [] -> hierror ~loc:op.pl_loc "unknown operator"
          | op1::op2::_ ->
              hierror ~loc:op.pl_loc
                "ambiguous operator (%s / %s)"
                (EcPath.tostring (fst (proj4_1 op1)))
                (EcPath.tostring (fst (proj4_1 op2)))
          | [((p, _), _, _, _)] ->
              let op   = EcEnv.Op.by_path p env in
              let opty =
                Tvar.subst
                  (Tvar.init op.op_tparams tvi)
                  op.op_ty
              in
                (p, opty)

        in
          Mstr.change
            (function
            | None   -> Some (x.pl_loc, op)
            | Some _ -> hierror ~loc:(x.pl_loc)
              "duplicated operator name: `%s'" (unloc x))
            (unloc x) m
      in
        List.fold_left tt1 Mstr.empty ops
    in
      List.iter
        (fun (x, (req, _)) ->
           if req && not (Mstr.mem x ops) then
             hierror "no definition for operator `%s'" x)
        reqs;
      List.fold_left
        (fun m (x, (_, ty)) ->
           match Mstr.find_opt x ops with
           | None -> m
           | Some (loc, (p, opty)) ->
               if not (EcReduction.EqTest.for_type env ty opty) then
                 hierror ~loc "invalid type for operator `%s'" x;
               Mstr.add x p m)
        Mstr.empty reqs

  (* ------------------------------------------------------------------ *)
  let check_tci_axioms scope mode axs reqs lc =
    let rmap = Mstr.of_list reqs in
    let symbs, axs =
      List.map_fold
        (fun m (x, t) ->
          if not (Mstr.mem (unloc x) rmap) then
            hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x);
          if Sstr.mem (unloc x) m then
            hierror ~loc:(x.pl_loc) "duplicated axiom name: `%s'" (unloc x);
          (Sstr.add (unloc x) m, (unloc x, t, Mstr.find (unloc x) rmap)))
        Sstr.empty axs in

    let interactive =
      List.pmap
        (fun (x, req) ->
           if not (Mstr.mem x symbs) then
             let ax = {
               ax_tparams = [];
               ax_spec    = req;
               ax_kind    = `Lemma;
               ax_loca    = lc;
               ax_smt     = false;
             } in Some ((None, ax), EcPath.psymbol x, scope.sc_env)
           else None)
        reqs in
      List.iter
        (fun (x, pt, f) ->
          let x  = "$" ^ x in
          let t  = { pt_core = pt; pt_intros = []; } in
          let t  = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in
          let t  = { pt_core = t; pt_intros = []; } in
          let ax = {
              ax_tparams = [];
              ax_spec    = f;
              ax_kind    = `Lemma;
              ax_smt     = false;
              ax_loca    = lc;
          } in

          let pucflags = { puc_smt = true; puc_local = false; } in
          let pucflags = (([], None), pucflags) in
          let check    = Check_mode.check scope.sc_options in

          let escope = scope in
          let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
          let escope = Tactics.proof escope in
          let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
            ignore (Ax.save_r escope))
        axs;
      interactive

  (* ------------------------------------------------------------------ *)
  (* FIXME section: those path does not exists ...
     futhermode Ring.ZModule is an abstract theory *)
  let p_zmod    = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ZModule"], "zmodule")
  let p_ring    = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ComRing"], "ring"   )
  let p_idomain = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "IDomain"], "idomain")
  let p_field   = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field"  ], "field"  )

  (* ------------------------------------------------------------------ *)
  let ring_of_symmap env ty kind symbols =
    { r_type  = ty;
      r_zero  = oget (Mstr.find_opt "rzero" symbols);
      r_one   = oget (Mstr.find_opt "rone"  symbols);
      r_add   = oget (Mstr.find_opt "add"   symbols);
      r_opp   =      (Mstr.find_opt "opp"   symbols);
      r_mul   = oget (Mstr.find_opt "mul"   symbols);
      r_exp   =      (Mstr.find_opt "expr"  symbols);
      r_sub   =      (Mstr.find_opt "sub"   symbols);
      r_kind  = kind;
      r_embed =
        (match Mstr.find_opt "ofint" symbols with
         | None when EcReduction.EqTest.for_type env ty tint -> `Direct
         | None -> `Default | Some p -> `Embed p); }

  let addring ~import (scope : scope) mode (kind, { pl_desc = tci; pl_loc = loc }) =
    let env = env scope in
    if not (EcAlgTactic.is_module_loaded env) then
      hierror "load AlgTactic/Ring first";

    let ty =
      let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in
      let ty = transty tp_tydecl env ue (snd tci.pti_type) in
      assert (EcUnify.UniEnv.closed ue);
      let uidmap = EcUnify.UniEnv.close ue in
        (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty)
    in
    if not (List.is_empty (fst ty)) then
      hierror "ring instances cannot be polymorphic";

    let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in
    let symbols = check_tci_operators env ty tci.pti_ops symbols in
    let cr      = ring_of_symmap env (snd ty) kind symbols in
    let axioms  = EcAlgTactic.ring_axioms env cr in
    let lc      = (tci.pti_loca :> locality) in
    let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc in
    let add env p =
      let item = EcTheory.Th_instance (ty,`General p, tci.pti_loca) in
      let item = EcTheory.mkitem ~import item in
      EcSection.add_item item env in

    let scope   =
      { scope with sc_env =
          List.fold_left add
            (let item =
               EcTheory.Th_instance (([], snd ty), `Ring cr, tci.pti_loca) in
             let item = EcTheory.mkitem ~import item in
             EcSection.add_item item scope.sc_env)
            [p_zmod; p_ring; p_idomain] }

    in Ax.add_defer scope inter

  (* ------------------------------------------------------------------ *)
  let field_of_symmap env ty symbols =
    { f_ring = ring_of_symmap env ty `Integer symbols;
      f_inv  = oget (Mstr.find_opt "inv" symbols);
      f_div  = Mstr.find_opt "div" symbols; }

  let addfield ~import (scope : scope) mode { pl_desc = tci; pl_loc = loc; } =
    let env = env scope in
    if not (EcAlgTactic.is_module_loaded env) then
      hierror "load AlgTactic/Ring first";

    let ty =
      let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in
      let ty = transty tp_tydecl env ue (snd tci.pti_type) in
      assert (EcUnify.UniEnv.closed ue);
      let uidmap = EcUnify.UniEnv.close ue in
        (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty)
    in
    if not (List.is_empty (fst ty)) then
      hierror "field instances cannot be polymorphic";
    let symbols = EcAlgTactic.field_symbols env (snd ty) in
    let symbols = check_tci_operators env ty tci.pti_ops symbols in
    let cr      = field_of_symmap env (snd ty) symbols in
    let axioms  = EcAlgTactic.field_axioms env cr in
    let lc      = (tci.pti_loca :> locality) in
    let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc; in
    let add env p =
      let item = EcTheory.Th_instance(ty,`General p, tci.pti_loca) in
      let item = EcTheory.mkitem ~import item in
      EcSection.add_item item env in
    let scope   =
      { scope with
        sc_env =
          List.fold_left add
            (let item =
               EcTheory.Th_instance (([], snd ty), `Field cr, tci.pti_loca) in
             let item = EcTheory.mkitem ~import item in
              EcSection.add_item item scope.sc_env)
            [p_zmod; p_ring; p_idomain; p_field] }

    in Ax.add_defer scope inter

  (* ------------------------------------------------------------------ *)
  let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) =
    let subst = EcSubst.add_tydef EcSubst.empty tcp ([], ty) in
      List.map (fun (x, opty) ->
        (EcIdent.name x, (true, EcSubst.subst_ty subst opty)))
        tc.tc_ops

(*
  (* ------------------------------------------------------------------ *)
  let add_generic_tc (scope : scope) _mode { pl_desc = tci; pl_loc = loc; } =
    let ty =
      let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
      let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
        assert (EcUnify.UniEnv.closed ue);
        (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
    in

    let (tcp, tc) =
      match EcEnv.TypeClass.lookup_opt (unloc tci.pti_name) (env scope) with
      | None ->
          hierror ~loc:tci.pti_name.pl_loc
            "unknown type-class: %s" (string_of_qsymbol (unloc tci.pti_name))
      | Some tc -> tc
    in

    let  symbols = symbols_of_tc scope.sc_env (snd ty) (tcp, tc) in
    let _symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in

    { scope with
        sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env }

(*
          let ue = EcUnify.UniEnv.create (Some []) in
          let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in
            try  EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc
            with EcUnify.UnificationFailure _ ->
              hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc))
*)
*)

  (* ------------------------------------------------------------------ *)
  let add_instance (scope : scope) mode ({ pl_desc = tci } as toptci) =
    match unloc tci.pti_name with
    | ([], "bring") -> begin
        if EcUtils.is_some tci.pti_args then
          hierror "unsupported-option";
        addring ~import:true scope mode (`Boolean, toptci)
    end

    | ([], "ring") -> begin
      let kind =
        match tci.pti_args with
        | None -> `Integer
        | Some (`Ring (c, p)) ->
            if odfl false (c |> omap (fun c -> c <^ BI.of_int 2)) then
              hierror "invalid coefficient modulus";
            if odfl false (p |> omap (fun p -> p <^ BI.of_int 2)) then
              hierror "invalid power modulus";
            if      opt_equal BI.equal c (Some (BI.of_int 2))
                 && opt_equal BI.equal p (Some (BI.of_int 2))
            then `Boolean
            else `Modulus (c, p)
      in addring ~import:true scope mode (kind, toptci)
    end

    | ([], "field") -> addfield ~import:true scope mode toptci

    | _ ->
        if EcUtils.is_some tci.pti_args then
          hierror "unsupported-option";
        failwith "unsupported"          (* FIXME *)
end

(* -------------------------------------------------------------------- *)module Search = struct
  let search (scope : scope) qs =
    let env = env scope in
    let paths =
      let do1 fp =
        match unloc fp with
        | PFident (q, None) -> begin
            match EcEnv.Op.all ~name:q.pl_desc env with
            | [] ->
                hierror ~loc:q.pl_loc "unknown operator: `%s'"
                  (EcSymbols.string_of_qsymbol q.pl_desc)
            | paths -> begin
                let for1 (paths, pts) (p, decl) =
                  match decl.op_kind with
                  | OB_nott nt -> begin
                    let ps  = ref Mid.empty in
                    let ue  = EcUnify.UniEnv.create None in
                    let tip = EcUnify.UniEnv.opentvi ue decl.op_tparams None in
                    let tip = f_subst_init ~tv:tip () in
                    let es = e_subst tip in
                    let xs  = List.map (snd_map (ty_subst tip)) nt.ont_args in
                    let bd  = EcFol.form_of_expr (es nt.ont_body) in
                    List.iter (fun (id, ty) -> ps := Mid.add id ty !ps) xs;

                    match bd.f_node with
                    | Fop (pf, _) -> (pf :: paths, pts)
                    | _ -> (paths, (ps, ue, bd) ::pts)
                  end

                  | _ -> (p :: paths, pts) in

                let paths, pts = List.fold_left for1 ([], []) paths in
                let pts = List.map (fun (ps, ue, fp) -> `ByPattern ((ps, ue), fp)) pts in

                `ByOr (`ByPath (Sp.of_list paths) :: pts)
              end
        end

        | _ ->
          let ps = ref Mid.empty in
          let ue = EcUnify.UniEnv.create None in
          let fp = EcTyping.trans_pattern env ps ue fp in
          `ByPattern ((ps, ue), fp)
      in List.map do1 qs in

    let relevant =
      let get_path r = function `ByPath s -> Sp.union r s | _ -> r in
      List.fold_left get_path Sp.empty paths in

    let search_res = EcSearch.search env paths in
    let search_res = EcSearch.sort relevant search_res in

    let buffer = Buffer.create 0 in
    let fmt    = Format.formatter_of_buffer buffer in
    let ppe    = EcPrinting.PPEnv.ofenv env in

    List.iter (fun (p, ax) ->
      Format.fprintf fmt "%a@." (EcPrinting.pp_axiom ~long:true ppe) (p,ax)
    ) search_res;
    notify scope `Info "%s" (Buffer.contents buffer)

  let locate (scope : scope) ({ pl_desc = name } : pqsymbol) =
    let ppe = EcPrinting.PPEnv.ofenv (env scope) in

    let shorten lk p =
      let lk (p : path) (qs : qsymbol) =
        match lk qs (env scope) with
        | Some (p', _) -> p_equal p p'
        | _ -> false in
      EcPrinting.shorten_path ppe lk p
    in

    let buffer = Buffer.create 0 in
    let fmt    = Format.formatter_of_buffer buffer in

    let for_kind section getall shorten =
      let objs = getall ?check:None ?name:(Some name) (env scope) in
      let objs = List.map shorten (List.fst objs) in

      if not (List.is_empty objs) then begin
        Format.fprintf fmt "In section [%s]@\n@\n" section;

        List.iter (fun (long, short) ->
            match short with
            | None ->
                Format.fprintf fmt " - %a@\n"
                  EcSymbols.pp_qsymbol long
            | Some short ->
                Format.fprintf fmt " - %a (shorten name: %a)@\n"
                  EcSymbols.pp_qsymbol long
                  EcSymbols.pp_qsymbol short
          )  objs
      end in

    for_kind "operators" EcEnv.Op.all (shorten EcEnv.Op.lookup_opt);
    for_kind "types"     EcEnv.Ty.all (shorten EcEnv.Ty.lookup_opt);
    for_kind "lemmas"    EcEnv.Ax.all (shorten EcEnv.Ax.lookup_opt);

    Format.pp_print_flush fmt ();

    if Buffer.length buffer = 0 then begin
      Format.fprintf fmt
        "no objects found for `%a'"
        EcSymbols.pp_qsymbol name
    end;

    notify scope `Info "%s" (Buffer.contents buffer)
end

(* -------------------------------------------------------------------- *)
module DocComment = struct
  let add (scope : scope) ((kind, docc) : [`Global | `Item] * string) : scope =
    match kind with
    | `Global ->
       { scope with sc_globdoc = scope.sc_globdoc @ [docc] }

    | `Item ->
       { scope with sc_locdoc = DocState.push_docbl scope.sc_locdoc docc }
end