[stm] Break stm/toplevel dependency loop.

Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.

This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.

As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.

Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.

1 files changed, 530 insertions, 0 deletions

diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml
new file mode 100644
index 000000000..f7e3f0d95
--- /dev/null
+++ b/vernac/indschemes.ml
@@ -0,0 +1,530 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* Created by Hugo Herbelin from contents related to inductive schemes
+   initially developed by Christine Paulin (induction schemes), Vincent
+   Siles (decidable equality and boolean equality) and Matthieu Sozeau
+   (combined scheme) in file command.ml, Sep 2009 *)
+
+(* This file provides entry points for manually or automatically
+   declaring new schemes *)
+
+open Pp
+open CErrors
+open Util
+open Names
+open Declarations
+open Entries
+open Term
+open Inductive
+open Decl_kinds
+open Indrec
+open Declare
+open Libnames
+open Globnames
+open Goptions
+open Nameops
+open Termops
+open Pretyping
+open Nametab
+open Smartlocate
+open Vernacexpr
+open Ind_tables
+open Auto_ind_decl
+open Eqschemes
+open Elimschemes
+open Context.Rel.Declaration
+
+(* Flags governing automatic synthesis of schemes *)
+
+let elim_flag = ref true
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "automatic declaration of induction schemes";
+      optkey   = ["Elimination";"Schemes"];
+      optread  = (fun () -> !elim_flag) ;
+      optwrite = (fun b -> elim_flag := b) }
+
+let bifinite_elim_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "automatic declaration of induction schemes for non-recursive types";
+      optkey   = ["Nonrecursive";"Elimination";"Schemes"];
+      optread  = (fun () -> !bifinite_elim_flag) ;
+      optwrite = (fun b -> bifinite_elim_flag := b) }
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = true; (* compatibility 2014-09-03*)
+      optname  = "automatic declaration of induction schemes for non-recursive types";
+      optkey   = ["Record";"Elimination";"Schemes"];
+      optread  = (fun () -> !bifinite_elim_flag) ;
+      optwrite = (fun b -> bifinite_elim_flag := b) }
+
+let case_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "automatic declaration of case analysis schemes";
+      optkey   = ["Case";"Analysis";"Schemes"];
+      optread  = (fun () -> !case_flag) ;
+      optwrite = (fun b -> case_flag := b) }
+
+let eq_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "automatic declaration of boolean equality";
+      optkey   = ["Boolean";"Equality";"Schemes"];
+      optread  = (fun () -> !eq_flag) ;
+      optwrite = (fun b -> eq_flag := b) }
+let _ = (* compatibility *)
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = true;
+      optname  = "automatic declaration of boolean equality";
+      optkey   = ["Equality";"Scheme"];
+      optread  = (fun () -> !eq_flag) ;
+      optwrite = (fun b -> eq_flag := b) }
+
+let is_eq_flag () = !eq_flag && Flags.version_strictly_greater Flags.V8_2
+
+let eq_dec_flag = ref false 
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "automatic declaration of decidable equality";
+      optkey   = ["Decidable";"Equality";"Schemes"];
+      optread  = (fun () -> !eq_dec_flag) ;
+      optwrite = (fun b -> eq_dec_flag := b) }
+
+let rewriting_flag = ref false
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  ="automatic declaration of rewriting schemes for equality types";
+      optkey   = ["Rewriting";"Schemes"];
+      optread  = (fun () -> !rewriting_flag) ;
+      optwrite = (fun b -> rewriting_flag := b) }
+
+(* Util *)
+
+let define id internal ctx c t =
+  let f = declare_constant ~internal in
+  let kn = f id
+    (DefinitionEntry
+      { const_entry_body = c;
+        const_entry_secctx = None;
+        const_entry_type = t;
+	const_entry_polymorphic = Flags.is_universe_polymorphism ();
+	const_entry_universes = snd (Evd.universe_context ctx);
+        const_entry_opaque = false;
+        const_entry_inline_code = false;
+        const_entry_feedback = None;
+      },
+      Decl_kinds.IsDefinition Scheme) in
+  definition_message id;
+  kn
+
+(* Boolean equality *)
+
+let declare_beq_scheme_gen internal names kn =
+  ignore (define_mutual_scheme beq_scheme_kind internal names kn)
+
+let alarm what internal msg =
+  let debug = false in
+  match internal with
+  | UserAutomaticRequest
+  | InternalTacticRequest ->
+    (if debug then
+      Feedback.msg_debug
+	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
+  | _ -> Some msg
+
+let try_declare_scheme what f internal names kn =
+  try f internal names kn
+  with e ->
+  let e = CErrors.push e in
+  let msg = match fst e with
+    | ParameterWithoutEquality cst ->
+	alarm what internal
+	  (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++
+	   str".")
+    | InductiveWithProduct ->
+	alarm what internal
+	  (str "Unable to decide equality of functional arguments.")
+    | InductiveWithSort ->
+	alarm what internal
+	  (str "Unable to decide equality of type arguments.")
+    | NonSingletonProp ind ->
+	alarm what internal
+	  (str "Cannot extract computational content from proposition " ++
+	   quote (Printer.pr_inductive (Global.env()) ind) ++ str ".")
+    | EqNotFound (ind',ind) ->
+	alarm what internal
+	  (str "Boolean equality on " ++
+	   quote (Printer.pr_inductive (Global.env()) ind') ++
+	   strbrk " is missing.")
+    | UndefinedCst s ->
+	alarm what internal
+	  (strbrk "Required constant " ++ str s ++ str " undefined.")
+    | AlreadyDeclared msg ->
+        alarm what internal (msg ++ str ".")
+    | DecidabilityMutualNotSupported ->
+        alarm what internal
+          (str "Decidability lemma for mutual inductive types not supported.")
+    | EqUnknown s ->
+         alarm what internal
+           (str "Found unsupported " ++ str s ++ str " while building Boolean equality.")
+    | NoDecidabilityCoInductive ->
+         alarm what internal
+           (str "Scheme Equality is only for inductive types.")
+    | e when CErrors.noncritical e ->
+        alarm what internal
+	  (str "Unexpected error during scheme creation: " ++ CErrors.print e)
+    | _ -> iraise e
+  in
+  match msg with
+  | None -> ()
+  | Some msg -> iraise (UserError (None, msg), snd e)
+
+let beq_scheme_msg mind =
+  let mib = Global.lookup_mind mind in
+  (* TODO: mutual inductive case *)
+  str "Boolean equality on " ++
+    pr_enum (fun ind -> quote (Printer.pr_inductive (Global.env()) ind))
+    (List.init (Array.length mib.mind_packets) (fun i -> (mind,i)))
+
+let declare_beq_scheme_with l kn =
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserIndividualRequest l kn
+
+let try_declare_beq_scheme kn =
+  (* TODO: handle Fix, eventually handle
+      proof-irrelevance; improve decidability by depending on decidability
+      for the parameters rather than on the bl and lb properties *)
+  try_declare_scheme (beq_scheme_msg kn) declare_beq_scheme_gen UserAutomaticRequest [] kn
+
+let declare_beq_scheme = declare_beq_scheme_with []
+
+(* Case analysis schemes *)
+let declare_one_case_analysis_scheme ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let kind = inductive_sort_family mip in
+  let dep =
+    if kind == InProp then case_scheme_kind_from_prop
+    else if not (Inductiveops.has_dependent_elim mib) then
+      case_scheme_kind_from_type
+    else case_dep_scheme_kind_from_type in
+  let kelim = elim_sorts (mib,mip) in
+    (* in case the inductive has a type elimination, generates only one
+       induction scheme, the other ones share the same code with the
+       apropriate type *)
+  if Sorts.List.mem InType kelim then
+    ignore (define_individual_scheme dep UserAutomaticRequest None ind)
+
+(* Induction/recursion schemes *)
+
+let kinds_from_prop =
+  [InType,rect_scheme_kind_from_prop;
+   InProp,ind_scheme_kind_from_prop;
+   InSet,rec_scheme_kind_from_prop]
+
+let kinds_from_type =
+  [InType,rect_dep_scheme_kind_from_type;
+   InProp,ind_dep_scheme_kind_from_type;
+   InSet,rec_dep_scheme_kind_from_type]
+
+let nondep_kinds_from_type =
+  [InType,rect_scheme_kind_from_type;
+   InProp,ind_scheme_kind_from_type;
+   InSet,rec_scheme_kind_from_type]
+
+let declare_one_induction_scheme ind =
+  let (mib,mip) = Global.lookup_inductive ind in
+  let kind = inductive_sort_family mip in
+  let from_prop = kind == InProp in
+  let depelim = Inductiveops.has_dependent_elim mib in
+  let kelim = elim_sorts (mib,mip) in
+  let elims =
+    List.map_filter (fun (sort,kind) ->
+      if Sorts.List.mem sort kelim then Some kind else None)
+      (if from_prop then kinds_from_prop
+       else if depelim then kinds_from_type
+       else nondep_kinds_from_type) in
+  List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind))
+    elims
+
+let declare_induction_schemes kn =
+  let mib = Global.lookup_mind kn in
+  if mib.mind_finite <> Decl_kinds.CoFinite then begin
+    for i = 0 to Array.length mib.mind_packets - 1 do
+      declare_one_induction_scheme (kn,i);
+    done;
+  end
+
+(* Decidable equality *)
+
+let declare_eq_decidability_gen internal names kn =
+  let mib = Global.lookup_mind kn in
+  if mib.mind_finite <> Decl_kinds.CoFinite then
+    ignore (define_mutual_scheme eq_dec_scheme_kind internal names kn)
+
+let eq_dec_scheme_msg ind = (* TODO: mutual inductive case *)
+  str "Decidable equality on " ++ quote (Printer.pr_inductive (Global.env()) ind)
+
+let declare_eq_decidability_scheme_with l kn =
+  try_declare_scheme (eq_dec_scheme_msg (kn,0))
+    declare_eq_decidability_gen UserIndividualRequest l kn
+
+let try_declare_eq_decidability kn =
+  try_declare_scheme (eq_dec_scheme_msg (kn,0))
+    declare_eq_decidability_gen UserAutomaticRequest [] kn
+
+let declare_eq_decidability = declare_eq_decidability_scheme_with []
+
+let ignore_error f x =
+  try ignore (f x) with e when CErrors.noncritical e -> ()
+
+let declare_rewriting_schemes ind =
+  if Hipattern.is_inductive_equality ind then begin
+    ignore (define_individual_scheme rew_r2l_scheme_kind UserAutomaticRequest None ind);
+    ignore (define_individual_scheme rew_r2l_dep_scheme_kind UserAutomaticRequest None ind);
+    ignore (define_individual_scheme rew_r2l_forward_dep_scheme_kind
+      UserAutomaticRequest None ind);
+    (* These ones expect the equality to be symmetric; the first one also *)
+    (* needs eq *)
+    ignore_error (define_individual_scheme rew_l2r_scheme_kind UserAutomaticRequest None) ind;
+    ignore_error
+      (define_individual_scheme rew_l2r_dep_scheme_kind UserAutomaticRequest None) ind;
+    ignore_error
+      (define_individual_scheme rew_l2r_forward_dep_scheme_kind UserAutomaticRequest None) ind
+  end
+
+let warn_cannot_build_congruence =
+  CWarnings.create ~name:"cannot-build-congruence" ~category:"schemes"
+         (fun () ->
+          strbrk "Cannot build congruence scheme because eq is not found")
+
+let declare_congr_scheme ind =
+  if Hipattern.is_equality_type (mkInd ind) then begin
+    if
+      try Coqlib.check_required_library Coqlib.logic_module_name; true
+      with e when CErrors.noncritical e -> false
+    then
+      ignore (define_individual_scheme congr_scheme_kind UserAutomaticRequest None ind)
+    else
+      warn_cannot_build_congruence ()
+  end
+
+let declare_sym_scheme ind =
+  if Hipattern.is_inductive_equality ind then
+    (* Expect the equality to be symmetric *)
+    ignore_error (define_individual_scheme sym_scheme_kind UserAutomaticRequest None) ind
+
+(* Scheme command *)
+
+let smart_global_inductive y = smart_global_inductive y
+let rec split_scheme l =
+ let env = Global.env() in
+ match l with
+  | [] -> [],[]
+  | (Some id,t)::q -> let l1,l2 = split_scheme q in
+    ( match t with
+      | InductionScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
+      | CaseScheme (x,y,z) -> ((id,x,smart_global_inductive y,z)::l1),l2
+      | EqualityScheme  x -> l1,((Some id,smart_global_inductive x)::l2)
+    )
+(*
+ if no name has been provided, we build one from the types of the ind
+requested
+*)
+  | (None,t)::q ->
+      let l1,l2 = split_scheme q in
+      let names inds recs isdep y z =
+        let ind = smart_global_inductive y in
+        let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
+        let z' = interp_elimination_sort z in
+        let suffix = (
+          match sort_of_ind with
+          | InProp ->
+              if isdep then (match z' with
+              | InProp -> inds ^ "_dep"
+              | InSet  -> recs ^ "_dep"
+              | InType -> recs ^ "t_dep")
+              else ( match z' with
+              | InProp -> inds
+              | InSet -> recs
+              | InType -> recs ^ "t" )
+          | _ ->
+              if isdep then (match z' with
+              | InProp -> inds
+              | InSet -> recs
+              | InType -> recs ^ "t" )
+              else (match z' with
+              | InProp -> inds ^ "_nodep"
+              | InSet -> recs ^ "_nodep"
+              | InType -> recs ^ "t_nodep")
+        ) in
+        let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
+        let newref = (Loc.ghost,newid) in
+          ((newref,isdep,ind,z)::l1),l2
+      in
+	match t with
+	| CaseScheme (x,y,z) -> names "_case" "_case" x y z
+	| InductionScheme (x,y,z) -> names "_ind" "_rec" x y z
+	| EqualityScheme  x -> l1,((None,smart_global_inductive x)::l2)
+	    
+
+let do_mutual_induction_scheme lnamedepindsort =
+  let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
+  and env0 = Global.env() in
+  let sigma, lrecspec, _ =
+    List.fold_right
+      (fun (_,dep,ind,sort) (evd, l, inst) -> 
+       let evd, indu, inst =
+	 match inst with
+	 | None ->
+	    let _, ctx = Global.type_of_global_in_context env0 (IndRef ind) in
+	    let ctxs = Univ.ContextSet.of_context ctx in
+	    let evd = Evd.from_ctx (Evd.evar_universe_context_of ctxs) in
+	    let u = Univ.UContext.instance ctx in
+	      evd, (ind,u), Some u
+	 | Some ui -> evd, (ind, ui), inst
+       in
+          (evd, (indu,dep,interp_elimination_sort sort) :: l, inst))
+    lnamedepindsort (Evd.from_env env0,[],None)
+  in
+  let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in
+  let declare decl fi lrecref =
+    let decltype = Retyping.get_type_of env0 sigma decl in
+    let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+    let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in
+    ConstRef cst :: lrecref
+  in
+  let _ = List.fold_right2 declare listdecl lrecnames [] in
+  fixpoint_message None lrecnames
+
+let get_common_underlying_mutual_inductive = function
+  | [] -> assert false
+  | (id,(mind,i as ind))::l as all ->
+      match List.filter (fun (_,(mind',_)) -> not (eq_mind mind mind')) l with
+      | (_,ind')::_ ->
+	  raise (RecursionSchemeError (NotMutualInScheme (ind,ind')))
+      | [] ->
+	  if not (List.distinct_f Int.compare (List.map snd (List.map snd all)))
+          then error "A type occurs twice";
+	  mind,
+	  List.map_filter
+	    (function (Some id,(_,i)) -> Some (i,snd id) | (None,_) -> None) all
+
+let do_scheme l =
+  let ischeme,escheme = split_scheme l in
+(* we want 1 kind of scheme at a time so we check if the user
+tried to declare different schemes at once *)
+    if not (List.is_empty ischeme) && not (List.is_empty escheme)
+    then
+      error "Do not declare equality and induction scheme at the same time."
+    else (
+      if not (List.is_empty ischeme) then do_mutual_induction_scheme ischeme
+      else
+	let mind,l = get_common_underlying_mutual_inductive escheme in
+	declare_beq_scheme_with l mind;
+	declare_eq_decidability_scheme_with l mind
+    )
+
+(**********************************************************************)
+(* Combined scheme *)
+(* Matthieu Sozeau, Dec 2006 *)
+
+let list_split_rev_at index l =
+  let rec aux i acc = function
+      hd :: tl when Int.equal i index -> acc, tl
+    | hd :: tl -> aux (succ i) (hd :: acc) tl
+    | [] -> failwith "List.split_when: Invalid argument"
+  in aux 0 [] l
+
+let fold_left' f = function
+    [] -> invalid_arg "fold_left'"
+  | hd :: tl -> List.fold_left f hd tl
+
+let build_combined_scheme env schemes =
+  let defs = List.map (fun cst -> (* FIXME *)
+    let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in
+      (c, Typeops.type_of_constant_in env c)) schemes in
+(*   let nschemes = List.length schemes in *)
+  let find_inductive ty =
+    let (ctx, arity) = decompose_prod ty in
+    let (_, last) = List.hd ctx in
+      match kind_of_term last with
+	| App (ind, args) ->
+	    let ind = destInd ind in
+	    let (_,spec) = Inductive.lookup_mind_specif env (fst ind) in
+	      ctx, ind, spec.mind_nrealargs
+	| _ -> ctx, destInd last, 0
+  in
+  let (c, t) = List.hd defs in
+  let ctx, ind, nargs = find_inductive t in
+  (* Number of clauses, including the predicates quantification *)
+  let prods = nb_prod t - (nargs + 1) in
+  let coqand = Coqlib.build_coq_and () and coqconj = Coqlib.build_coq_conj () in
+  let relargs = rel_vect 0 prods in
+  let concls = List.rev_map
+    (fun (cst, t) -> (* FIXME *)
+      mkApp(mkConstU cst, relargs),
+      snd (decompose_prod_n prods t)) defs in
+  let concl_bod, concl_typ =
+    fold_left'
+      (fun (accb, acct) (cst, x) ->
+	mkApp (coqconj, [| x; acct; cst; accb |]),
+	mkApp (coqand, [| x; acct |])) concls
+  in
+  let ctx, _ =
+    list_split_rev_at prods
+      (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in
+  let typ = it_mkProd_wo_LetIn concl_typ ctx in
+  let body = it_mkLambda_or_LetIn concl_bod ctx in
+  (body, typ)
+
+let do_combined_scheme name schemes =
+  let csts =
+    List.map (fun x ->
+		let refe = Ident x in
+		let qualid = qualid_of_reference refe in
+		try Nametab.locate_constant (snd qualid)
+                with Not_found -> error ((string_of_qualid (snd qualid))^" is not declared."))
+      schemes
+  in
+  let body,typ = build_combined_scheme (Global.env ()) csts in
+  let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in
+  ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ));
+  fixpoint_message None [snd name]
+
+(**********************************************************************)
+
+let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done
+
+let declare_default_schemes kn =
+  let mib = Global.lookup_mind kn in
+  let n = Array.length mib.mind_packets in
+  if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag)
+     && mib.mind_typing_flags.check_guarded then
+    declare_induction_schemes kn;
+  if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n;
+  if is_eq_flag() then try_declare_beq_scheme kn;
+  if !eq_dec_flag then try_declare_eq_decidability kn;
+  if !rewriting_flag then map_inductive_block declare_congr_scheme kn n;
+  if !rewriting_flag then map_inductive_block declare_sym_scheme kn n;
+  if !rewriting_flag then map_inductive_block declare_rewriting_schemes kn n