(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Compat
open Util
open Names
open Tacexpr
open Extend
open Genarg
open Topconstr
open Decl_kinds
open Ppextend
open Declaremods

(* Toplevel control exceptions *)
exception Drop
exception Quit

open Libnames
open Nametab

type lident = identifier located
type lname = name located
type lstring = string located
type lreference = reference

type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation

type goal_identifier = string

type goal_reference =
  | OpenSubgoals
  | NthGoal of int
  | GoalId of goal_identifier

type printable =
  | PrintTables
  | PrintFullContext
  | PrintSectionContext of reference
  | PrintInspect of int
  | PrintGrammar of string
  | PrintLoadPath of dir_path option
  | PrintModules
  | PrintModule of reference
  | PrintModuleType of reference
  | PrintMLLoadPath
  | PrintMLModules
  | PrintName of reference or_by_notation
  | PrintGraph
  | PrintClasses
  | PrintTypeClasses
  | PrintInstances of reference or_by_notation
  | PrintLtac of reference
  | PrintCoercions
  | PrintCoercionPaths of class_rawexpr * class_rawexpr
  | PrintCanonicalConversions
  | PrintUniverses of bool * string option
  | PrintHint of reference or_by_notation
  | PrintHintGoal
  | PrintHintDbName of string
  | PrintRewriteHintDbName of string
  | PrintHintDb
  | PrintScopes
  | PrintScope of string
  | PrintVisibility of string option
  | PrintAbout of reference or_by_notation
  | PrintImplicit of reference or_by_notation
  | PrintAssumptions of bool * reference or_by_notation

type search_about_item =
  | SearchSubPattern of constr_pattern_expr
  | SearchString of string * scope_name option

type searchable =
  | SearchPattern of constr_pattern_expr
  | SearchRewrite of constr_pattern_expr
  | SearchHead of constr_pattern_expr
  | SearchAbout of (bool * search_about_item) list

type locatable =
  | LocateTerm of reference or_by_notation
  | LocateLibrary of reference
  | LocateModule of reference
  | LocateTactic of reference
  | LocateFile of string

type showable =
  | ShowGoal of goal_reference
  | ShowGoalImplicitly of int option
  | ShowProof
  | ShowNode
  | ShowScript
  | ShowExistentials
  | ShowTree
  | ShowProofNames
  | ShowIntros of bool
  | ShowMatch of lident
  | ShowThesis

type comment =
  | CommentConstr of constr_expr
  | CommentString of string
  | CommentInt of int

type hints_expr =
  | HintsResolve of (int option * bool * constr_expr) list
  | HintsImmediate of constr_expr list
  | HintsUnfold of reference list
  | HintsTransparency of reference list * bool
  | HintsConstructors of reference list
  | HintsExtern of int * constr_expr option * raw_tactic_expr

type search_restriction =
  | SearchInside of reference list
  | SearchOutside of reference list

type rec_flag       = bool (* true = Rec;           false = NoRec          *)
type verbose_flag   = bool (* true = Verbose;       false = Silent         *)
type opacity_flag   = bool (* true = Opaque;        false = Transparent    *)
type locality_flag  = bool (* true = Local;         false = Global         *)
type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
type instance_flag  = bool option (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
type export_flag    = bool (* true = Export;        false = Import         *)
type specif_flag    = bool (* true = Specification; false = Implementation *)
type inductive_flag = Decl_kinds.recursivity_kind
type infer_flag     = bool (* true = try to Infer record; false = nothing  *)
type full_locality_flag = bool option (* true = Local; false = Global      *)
type onlyparsing_flag = Flags.compat_version option
 (* Some v = Parse only;  None = Print also.
    If v<>Current, it contains the name of the coq version
    which this notation is trying to be compatible with *)

type option_value = Goptionstyp.option_value =
  | BoolValue of bool
  | IntValue of int option
  | StringValue of string

type option_ref_value =
  | StringRefValue of string
  | QualidRefValue of reference

type sort_expr = Glob_term.glob_sort

type definition_expr =
  | ProveBody of local_binder list * constr_expr
  | DefineBody of local_binder list * raw_red_expr option * constr_expr
      * constr_expr option

type fixpoint_expr =
    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr option

type cofixpoint_expr =
    identifier located * local_binder list * constr_expr * constr_expr option

type local_decl_expr =
  | AssumExpr of lname * constr_expr
  | DefExpr of lname * constr_expr * constr_expr option

type inductive_kind = Inductive_kw | CoInductive | Record | Structure | Class of bool (* true = definitional, false = inductive *)
type decl_notation = lstring * constr_expr * scope_name option
type simple_binder = lident list  * constr_expr
type class_binder = lident * constr_expr list
type 'a with_coercion = coercion_flag * 'a
type 'a with_instance = instance_flag * 'a
type 'a with_notation = 'a * decl_notation list
type 'a with_priority = 'a * int option
type constructor_expr = (lident * constr_expr) with_coercion
type constructor_list_or_record_decl_expr =
  | Constructors of constructor_expr list
  | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list
type inductive_expr =
  lident with_coercion * local_binder list * constr_expr option * inductive_kind *
    constructor_list_or_record_decl_expr

type one_inductive_expr =
  lident * local_binder list * constr_expr option * constructor_expr list

type module_ast_inl = module_ast annotated
type module_binder = bool option * lident list * module_ast_inl

type grammar_tactic_prod_item_expr =
  | TacTerm of string
  | TacNonTerm of loc * string * (Names.identifier * string) option

type syntax_modifier =
  | SetItemLevel of string list * production_level
  | SetLevel of int
  | SetAssoc of gram_assoc
  | SetEntryType of string * simple_constr_prod_entry_key
  | SetOnlyParsing of Flags.compat_version
  | SetFormat of string located

type proof_end =
  | Admitted
  | Proved of opacity_flag * (lident * theorem_kind option) option

type scheme =
  | InductionScheme of bool * reference or_by_notation * sort_expr
  | CaseScheme of bool * reference or_by_notation * sort_expr
  | EqualityScheme of reference or_by_notation

type inline = int option (* inlining level, none for no inlining *)

type bullet =
    | Dash
    | Star
    | Plus

type vernac_expr =
  (* Control *)
  | VernacList of located_vernac_expr list
  | VernacLoad of verbose_flag * string
  | VernacTime of vernac_expr
  | VernacTimeout of int * vernac_expr
  | VernacFail of vernac_expr

  (* Syntax *)
  | VernacTacticNotation of int * grammar_tactic_prod_item_expr list * raw_tactic_expr
  | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
  | VernacOpenCloseScope of (locality_flag * bool * scope_name)
  | VernacDelimiters of scope_name * string
  | VernacBindScope of scope_name * class_rawexpr list
  | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
      constr_expr * scope_name option
  | VernacNotation of
      locality_flag * constr_expr * (lstring * syntax_modifier list) *
      scope_name option

  (* Gallina *)
  | VernacDefinition of definition_kind * lident * definition_expr *
      declaration_hook
  | VernacStartTheoremProof of theorem_kind *
      (lident option * (local_binder list * constr_expr * (lident option * recursion_order_expr) option)) list *
        bool * declaration_hook
  | VernacEndProof of proof_end
  | VernacExactProof of constr_expr
  | VernacAssumption of assumption_kind * inline * simple_binder with_coercion list
  | VernacInductive of inductive_flag * infer_flag * (inductive_expr * decl_notation list) list
  | VernacFixpoint of (fixpoint_expr * decl_notation list) list
  | VernacCoFixpoint of (cofixpoint_expr * decl_notation list) list
  | VernacScheme of (lident option * scheme) list
  | VernacCombinedScheme of lident * lident list

  (* Gallina extensions *)
  | VernacBeginSection of lident
  | VernacEndSegment of lident
  | VernacRequire of
      export_flag option * specif_flag option * lreference list
  | VernacImport of export_flag * lreference list
  | VernacCanonical of reference or_by_notation
  | VernacCoercion of locality * reference or_by_notation *
      class_rawexpr * class_rawexpr
  | VernacIdentityCoercion of locality * lident *
      class_rawexpr * class_rawexpr

  (* Type classes *)
  | VernacInstance of
      bool * (* abstract instance *)
      bool * (* global *)
      local_binder list * (* super *)
	typeclass_constraint * (* instance name, class name, params *)
	constr_expr option * (* props *)
	int option (* Priority *)

  | VernacContext of local_binder list

  | VernacDeclareInstances of
      bool (* global *) * reference list (* instance names *)

  | VernacDeclareClass of reference (* inductive or definition name *)

  (* Modules and Module Types *)
  | VernacDeclareModule of bool option * lident *
      module_binder list * module_ast_inl
  | VernacDefineModule of bool option * lident *
      module_binder list * module_ast_inl module_signature * module_ast_inl list
  | VernacDeclareModuleType of lident *
      module_binder list * module_ast_inl list * module_ast_inl list
  | VernacInclude of module_ast_inl list

  (* Solving *)

  | VernacSolve of int * raw_tactic_expr * bool
  | VernacSolveExistential of int * constr_expr

  (* Auxiliary file and library management *)
  | VernacRequireFrom of export_flag option * specif_flag option * string
  | VernacAddLoadPath of rec_flag * string * dir_path option
  | VernacRemoveLoadPath of string
  | VernacAddMLPath of rec_flag * string
  | VernacDeclareMLModule of locality_flag * string list
  | VernacChdir of string option

  (* State management *)
  | VernacWriteState of string
  | VernacRestoreState of string

  (* Resetting *)
  | VernacResetName of lident
  | VernacResetInitial
  | VernacBack of int
  | VernacBackTo of int

  (* Commands *)
  | VernacDeclareTacticDefinition of
      (locality_flag * rec_flag * (reference * bool * raw_tactic_expr) list)
  | VernacCreateHintDb of locality_flag * string * bool
  | VernacRemoveHints of locality_flag * string list * reference list
  | VernacHints of locality_flag * string list * hints_expr
  | VernacSyntacticDefinition of identifier located * (identifier list * constr_expr) *
      locality_flag * onlyparsing_flag
  | VernacDeclareImplicits of locality_flag * reference or_by_notation *
      (explicitation * bool * bool) list list
  | VernacArguments of locality_flag * reference or_by_notation * 
      ((name * bool * (loc * string) option * bool * bool) list) list *
      int * [ `SimplDontExposeCase | `SimplNeverUnfold | `Rename | `ExtraScopes
            | `ClearImplicits | `ClearScopes | `DefaultImplicits ] list
  | VernacArgumentsScope of locality_flag * reference or_by_notation *
      scope_name option list
  | VernacReserve of simple_binder list
  | VernacGeneralizable of locality_flag * (lident list) option
  | VernacSetOpacity of
      locality_flag * (Conv_oracle.level * reference or_by_notation list) list
  | VernacUnsetOption of full_locality_flag * Goptions.option_name
  | VernacSetOption of full_locality_flag * Goptions.option_name * option_value
  | VernacAddOption of Goptions.option_name * option_ref_value list
  | VernacRemoveOption of Goptions.option_name * option_ref_value list
  | VernacMemOption of Goptions.option_name * option_ref_value list
  | VernacPrintOption of Goptions.option_name
  | VernacCheckMayEval of raw_red_expr option * int option * constr_expr
  | VernacGlobalCheck of constr_expr
  | VernacDeclareReduction of locality_flag * string * raw_red_expr
  | VernacPrint of printable
  | VernacSearch of searchable * search_restriction
  | VernacLocate of locatable
  | VernacComments of comment list
  | VernacNop

  (* Proof management *)
  | VernacGoal of constr_expr
  | VernacAbort of lident option
  | VernacAbortAll
  | VernacRestart
  | VernacUndo of int
  | VernacUndoTo of int
  | VernacBacktrack of int*int*int
  | VernacFocus of int option
  | VernacUnfocus
  | VernacUnfocused
  | VernacBullet of bullet
  | VernacSubproof of int option
  | VernacEndSubproof
  | VernacShow of showable
  | VernacCheckGuard
  | VernacProof of raw_tactic_expr option * lident list option
  | VernacProofMode of string
  (* Toplevel control *)
  | VernacToplevelControl of exn

  (* For extension *)
  | VernacExtend of string * raw_generic_argument list

and located_vernac_expr = loc * vernac_expr


(** Categories of [vernac_expr] *)

let rec strip_vernac = function
  | VernacTime c | VernacTimeout(_,c) | VernacFail c -> strip_vernac c
  | c -> c (* TODO: what about VernacList ? *)

let rec is_navigation_vernac = function
  | VernacResetInitial
  | VernacResetName _
  | VernacBacktrack _
  | VernacBackTo _
  | VernacBack _ -> true
  | VernacTime c -> is_navigation_vernac c (* Time Back* is harmless *)
  | c -> is_deep_navigation_vernac c

and is_deep_navigation_vernac = function
  | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
  | VernacList l -> List.exists (fun (_,c) -> is_navigation_vernac c) l
  | _ -> false

(* NB: Reset is now allowed again as asked by A. Chlipala *)

let is_reset = function
  | VernacResetInitial | VernacResetName _ -> true
  | _ -> false

(* Locating errors raised just after the dot is parsed but before the
   interpretation phase *)

let syntax_checking_error loc s = user_err_loc (loc,"",Pp.str s)

(**********************************************************************)
(* Managing locality *)

let locality_flag = ref None

let local_of_bool = function true -> Local | false -> Global

let check_locality () =
  match !locality_flag with
  | Some (loc,true) -> 
      syntax_checking_error loc
	"This command does not support the \"Local\" prefix.";
  | Some (loc,false) -> 
      syntax_checking_error loc
	"This command does not support the \"Global\" prefix."
  | None -> ()

(** Extracting the locality flag *)

(* Commands which supported an inlined Local flag *)

let enforce_locality_full local =
  let local =
    match !locality_flag with
    | Some (_,false) when local ->
	error "Cannot be simultaneously Local and Global."
    | Some (_,true) when local ->
	error "Use only prefix \"Local\"."
    | None ->
	if local then begin
	  Flags.if_warn
	   Pp.msg_warning (Pp.str"Obsolete syntax: use \"Local\" as a prefix.");
	  Some true
	end else
	None
    | Some (_,b) -> Some b in
  locality_flag := None;
  local

(* Commands which did not supported an inlined Local flag (synonym of
   [enforce_locality_full false]) *)

let use_locality_full () =
  let r = Option.map snd !locality_flag in
  locality_flag := None;
   r

(** Positioning locality for commands supporting discharging and export
     outside of modules *)

(* For commands whose default is to discharge and export:
   Global is the default and is neutral;
   Local in a section deactivates discharge, 
   Local not in a section deactivates export *)

let make_locality = function Some true -> true | _ -> false

let use_locality () = make_locality (use_locality_full ())

let use_locality_exp () = local_of_bool (use_locality ())

let enforce_locality local = make_locality (enforce_locality_full local)

let enforce_locality_exp local = local_of_bool (enforce_locality local)

(* For commands whose default is not to discharge and not to export:
   Global forces discharge and export;
   Local is the default and is neutral *)

let use_non_locality () =
  match use_locality_full () with Some false -> false | _ -> true

(* For commands whose default is to not discharge but to export:
   Global in sections forces discharge, Global not in section is the default;
   Local in sections is the default, Local not in section forces non-export *)

let make_section_locality =
  function Some b -> b | None -> Lib.sections_are_opened ()

let use_section_locality () =
  make_section_locality (use_locality_full ())

let enforce_section_locality local =
  make_section_locality (enforce_locality_full local)

(** Positioning locality for commands supporting export but not discharge *)

(* For commands whose default is to export (if not in section):
   Global in sections is forbidden, Global not in section is neutral;
   Local in sections is the default, Local not in section forces non-export *)

let make_module_locality = function
  | Some false ->
      if Lib.sections_are_opened () then
	error "This command does not support the Global option in sections.";
      false
  | Some true -> true
  | None -> false

let use_module_locality () =
  make_module_locality (use_locality_full ())

let enforce_module_locality local =
  make_module_locality (enforce_locality_full local)

(**********************************************************************)