generalize Scheme to support custom schemes

Author: felixL-K

clib/option.ml

@@ -181,5 +181,14 @@ module List =
       | Some y -> y :: aux f l
     in
     try Some (aux f l) with Exit -> None
-
+      
+  let fold_left f init lst =
+    let rec aux acc = function
+      | [] -> Some acc
+      | x :: xs ->
+        match f acc x with
+        | None -> None
+        | Some acc' -> aux acc' xs
+    in
+    aux init lst
 end

clib/option.mli

@@ -126,4 +126,9 @@ module List : sig
       [None] if, for at least one i, [f ai] is [None]. *)
   val map : ('a -> 'b option) -> 'a list -> 'b list option
 
+  (** [List.fold_left f acc [a1;...;an]] is [Some f (...(f (f init a1) a2)...)an] if
+      for all i, there is a [bi] such that [f acc ai] is [Some bi]; it is
+      [None] if, for at least one i, [f acc ai] is [None]. *)
+  val fold_left : ('acc -> 'b -> 'acc option) -> 'acc -> 'b list -> 'acc option
+
 end

engine/evd.ml

@@ -440,9 +440,11 @@ type evar_flags =
     rewrite_rule_evars : Evar.Set.t;
   }
 
+(* inductive * (scheme_name * sort * is_mutual *)
 type side_effect_role =
-| Schema of inductive * string
+| Schema of inductive * (string list * UnivGen.QualityOrSet.t option * bool)
 
+(* Schemes already defined but not yet in the global env *)
 type side_effects = {
   seff_safeenv : Safe_typing.safe_environment option;
   (* If seff_safeenv = Some senv, then senv = Global.safe_env + seff_private *)

engine/evd.mli

@@ -386,8 +386,9 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t
 
 (** {5 Side-effects} *)
 
+(* inductive * (scheme_name * sort * is_mutual *)
 type side_effect_role =
-| Schema of inductive * string
+| Schema of inductive * (string list * UnivGen.QualityOrSet.t option * bool)
 
 type side_effects
 

engine/univGen.ml

@@ -234,3 +234,12 @@ let fresh_sort_context_instance ((qs,us),csts) =
       (QVar.Map.empty, QVar.Set.empty)
   in
   (qsubst, usubst), ((qs, us), csts)
+
+let family_to_str = function
+  | QualityOrSet.Set -> "InSet"
+  | Qual a -> begin match a with
+      | Quality.QConstant Quality.QSProp -> "InSProp"
+      | Quality.QConstant Quality.QProp -> "InProp"
+      | Quality.QConstant Quality.QType -> "InType"
+      | Quality.QVar _ -> "InQSort"
+    end

engine/univGen.mli

@@ -111,3 +111,5 @@ val fresh_sort_context_instance : sort_context_set ->
     See Evd.fresh_global, Evarutil.new_global, and pf_constr_of_global for
     the proper way to get a fresh copy of a polymorphic global reference. *)
 val constr_of_monomorphic_global : env -> GlobRef.t -> constr
+
+val family_to_str : QualityOrSet.t -> string 

tactics/declareScheme.ml

@@ -10,12 +10,39 @@
 
 open Names
 
+module Key = struct
+
+  type is_mutual = bool
+
+  type t = (string list * UnivGen.QualityOrSet.t option * is_mutual)
+
+  let compare (a : t) (b : t) =
+    let a1, a2, a3 = a and b1, b2, b3 = b in
+    let c = CList.compare String.compare a1 b1 in
+    if c <> 0 then c
+    else
+      let c = Option.compare UnivGen.QualityOrSet.compare a2 b2 in
+      if c <> 0 then c
+      else Bool.compare a3 b3
+
+  module Self = struct
+    type nonrec t = t
+    let compare = compare
+  end
+
+  let equal a b = compare a b = 0
+
+  module Set = CSet.Make(Self)
+  module Map = CMap.Make(Self)
+
+end
+
 let scheme_map = Summary.ref Indmap_env.empty ~name:"Schemes"
 
 let cache_one_scheme kind (ind,const) =
   scheme_map := Indmap_env.update ind (function
-      | None -> Some (CString.Map.singleton kind const)
-      | Some map -> Some (CString.Map.add kind const map))
+      | None -> Some (Key.Map.singleton kind const)
+      | Some map -> Some (Key.Map.add kind const map))
       !scheme_map
 
 let cache_scheme (kind,l) =
@@ -28,7 +55,7 @@ let subst_one_scheme subst (ind,const) =
 let subst_scheme (subst,(kind,l)) =
   (kind, subst_one_scheme subst l)
 
-let inScheme : Libobject.locality * (string * (inductive * Constant.t)) -> Libobject.obj =
+let inScheme : Libobject.locality * (Key.t * (inductive * Constant.t)) -> Libobject.obj =
   let open Libobject in
   declare_object @@ object_with_locality "SCHEME"
     ~cache:cache_scheme
@@ -38,6 +65,6 @@ let inScheme : Libobject.locality * (string * (inductive * Constant.t)) -> Libob
 let declare_scheme local kind indcl =
   Lib.add_leaf (inScheme (local,(kind,indcl)))
 
-let lookup_scheme kind ind = CString.Map.find kind (Indmap_env.find ind !scheme_map)
+let lookup_scheme kind ind = Key.Map.find kind (Indmap_env.find ind !scheme_map)
 
 let all_schemes () = !scheme_map

tactics/declareScheme.mli

@@ -10,6 +10,17 @@
 
 open Names
 
-val declare_scheme : Libobject.locality -> string -> (inductive * Constant.t) -> unit
-val lookup_scheme : string -> inductive -> Constant.t
-val all_schemes : unit -> Constant.t CString.Map.t Indmap_env.t
+module Key : sig
+
+  type t = (string list * UnivGen.QualityOrSet.t option * bool)
+
+  val equal : t -> t -> bool
+
+  module Set : CSet.ExtS with type elt = t
+  module Map : CMap.ExtS with type key = t and module Set := Set
+end
+
+
+val declare_scheme : Libobject.locality -> Key.t -> (inductive * Constant.t) -> unit
+val lookup_scheme : (string list * UnivGen.QualityOrSet.t option * bool) -> inductive -> Constant.t
+val all_schemes : unit -> Constant.t Key.Map.t Indmap_env.t

tactics/elimschemes.ml

@@ -27,39 +27,134 @@ let build_induction_scheme_in_type env dep sort ind =
   let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
   let sigma, sort = Evd.fresh_sort_in_quality ~rigid:UnivRigid sigma sort in
   let sigma, c = build_induction_scheme env sigma pind dep sort in
-  EConstr.to_constr sigma c, Evd.ustate sigma
+  Some (EConstr.to_constr sigma c, Evd.ustate sigma)
+
+let build_mutual_induction_scheme_in_type env dep sort isrec l =
+  let ind,_ = match l with | x::_ -> x | [] -> assert false in
+  let sigma, inst =
+    let _, ctx = Typeops.type_of_global_in_context env (Names.GlobRef.IndRef (ind,0)) in
+    let u, ctx = UnivGen.fresh_instance_from ctx None in
+    let u = EConstr.EInstance.make u in
+    let sigma = Evd.from_ctx (UState.of_context_set ctx) in
+    sigma, u
+  in
+  let n = List.length l in
+  let sigma, lrecspec =
+    let rec loop i n sigma ll =
+      if i>=n then (sigma,ll)
+      else
+        let new_sigma, new_sort = Evd.fresh_sort_in_quality ~rigid:UnivRigid sigma sort in
+        let (indd,ii) = List.nth l i in
+        let new_l = List.append ll [(((indd,ii),inst),dep,new_sort)] in
+        loop (i + 1) n new_sigma new_l
+    in
+    loop 0 n sigma []
+  in
+  let sigma, listdecl =
+    if isrec then Indrec.build_mutual_induction_scheme env sigma ~force_mutual:false lrecspec
+    else
+      List.fold_left_map (fun sigma (ind,dep,sort) ->
+          let sigma, c = Indrec.build_case_analysis_scheme env sigma ind dep sort in
+          let c, _ = Indrec.eval_case_analysis c in
+          sigma, c)
+        sigma lrecspec
+  in
+  let array = Array.of_list listdecl in
+  let l = Array.map (fun x -> EConstr.to_constr sigma x) array in
+  Some (l, Evd.ustate sigma)
+
+let make_suff_sort one_ind suff dep =
+  match one_ind with
+  | None -> suff
+  | Some i ->
+    let sort = i.mind_sort
+    in
+    match sort with
+    | Prop -> if dep then (Names.Id.to_string i.mind_typename) ^ "_" ^ suff ^ "_dep"
+      else (Names.Id.to_string i.mind_typename) ^ "_" ^ suff
+    | Type _ | SProp | Set -> if dep then (Names.Id.to_string i.mind_typename) ^ "_" ^ suff
+      else (Names.Id.to_string i.mind_typename) ^ "_" ^ suff ^ "_nodep"
+    | QSort _ -> (Names.Id.to_string i.mind_typename) ^ "_" ^ suff
 
 let rect_dep =
-  declare_individual_scheme_object "rect_dep"
-    (fun env _ x -> build_induction_scheme_in_type env true QualityOrSet.qtype x)
+  declare_individual_scheme_object (["Induction"], Some QualityOrSet.qtype)
+    (fun id -> make_suff_sort id "rect" true)
+    (fun env _ x _ -> build_induction_scheme_in_type env true QualityOrSet.qtype x)
+
+let mutual_rect_dep =
+  declare_mutual_scheme_object (["Induction"], Some QualityOrSet.qtype)
+    (fun id -> make_suff_sort id "rect" true)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env true QualityOrSet.qtype true x)
 
 let rec_dep =
-  declare_individual_scheme_object "rec_dep"
-    (fun env _ x -> build_induction_scheme_in_type env true QualityOrSet.set x)
+  declare_individual_scheme_object (["Induction"], Some QualityOrSet.set)
+    (fun id -> make_suff_sort id "rec" true)
+    (fun env _ x _ -> build_induction_scheme_in_type env true QualityOrSet.set x)
+
+let mutual_rec_dep =
+  declare_mutual_scheme_object (["Induction"], Some QualityOrSet.set)
+    (fun id -> make_suff_sort id "rec" true)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env true QualityOrSet.set true x)
 
 let ind_dep =
-  declare_individual_scheme_object "ind_dep"
-    (fun env _ x -> build_induction_scheme_in_type env true QualityOrSet.prop x)
+  declare_individual_scheme_object (["Induction"], Some QualityOrSet.prop)
+    (fun id -> make_suff_sort id "ind" true)
+    (fun env _ x _ -> build_induction_scheme_in_type env true QualityOrSet.prop x)
+
+let mutual_ind_dep =
+  declare_mutual_scheme_object (["Induction"], Some QualityOrSet.prop)
+    (fun id -> make_suff_sort id "ind" true)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env true QualityOrSet.prop true x)
 
 let sind_dep =
-  declare_individual_scheme_object "sind_dep"
-    (fun env _ x -> build_induction_scheme_in_type env true QualityOrSet.sprop x)
+  declare_individual_scheme_object (["Induction"], Some QualityOrSet.sprop)
+    (fun id -> make_suff_sort id "inds" true)
+    (fun env _ x _ -> build_induction_scheme_in_type env true QualityOrSet.sprop x)
+
+let mutual_sind_dep =
+  declare_mutual_scheme_object (["Induction"], Some QualityOrSet.sprop)
+    (fun id -> make_suff_sort id "inds" true)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env true QualityOrSet.sprop true x)
 
 let rect_nodep =
-  declare_individual_scheme_object "rect_nodep"
-    (fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.qtype x)
+  declare_individual_scheme_object (["Minimality"], Some QualityOrSet.qtype)
+    (fun id -> make_suff_sort id "rect" false)
+    (fun env _ x _ -> build_induction_scheme_in_type env false QualityOrSet.qtype x)
+
+let mutual_rect_nodep =
+  declare_mutual_scheme_object (["Minimality"], Some QualityOrSet.qtype)
+    (fun id -> make_suff_sort id "rect" false)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env false QualityOrSet.qtype true x)
 
 let rec_nodep =
-  declare_individual_scheme_object "rec_nodep"
-    (fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.set x)
+  declare_individual_scheme_object (["Minimality"], Some QualityOrSet.set)
+    (fun id -> make_suff_sort id "rec" false)
+    (fun env _ x _ -> build_induction_scheme_in_type env false QualityOrSet.set x)
+
+let mutual_rec_nodep =
+  declare_mutual_scheme_object (["Minimality"], Some QualityOrSet.set)
+    (fun id -> make_suff_sort id "rec" false)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env false QualityOrSet.set true x)
 
 let ind_nodep =
-  declare_individual_scheme_object "ind_nodep"
-    (fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.prop x)
+  declare_individual_scheme_object (["Minimality"], Some QualityOrSet.prop)
+    (fun id -> make_suff_sort id "ind" false)
+    (fun env _ x _ -> build_induction_scheme_in_type env false QualityOrSet.prop x)
+
+let mutual_ind_nodep =
+  declare_mutual_scheme_object (["Minimality"], Some QualityOrSet.prop)
+    (fun id -> make_suff_sort id "ind" false)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env false QualityOrSet.prop true x)
 
 let sind_nodep =
-  declare_individual_scheme_object "sind_nodep"
-    (fun env _ x -> build_induction_scheme_in_type env false QualityOrSet.sprop x)
+  declare_individual_scheme_object (["Minimality"], Some QualityOrSet.sprop)
+    (fun id -> make_suff_sort id "inds" false)
+    (fun env _ x _ -> build_induction_scheme_in_type env false QualityOrSet.sprop x)
+
+let mutual_sind_nodep =
+  declare_mutual_scheme_object (["Minimality"], Some QualityOrSet.sprop)
+    (fun id -> make_suff_sort id "inds" false)
+    (fun env _ x _ -> build_mutual_induction_scheme_in_type env false QualityOrSet.sprop true x)
 
 let elim_scheme ~dep ~to_kind =
   let open QualityOrSet in
@@ -118,7 +213,7 @@ let lookup_eliminator_by_name env ind_sp s =
 let deprecated_lookup_by_name =
   CWarnings.create ~name:"deprecated-lookup-elim-by-name" ~category:Deprecation.Version.v9_1
     Pp.(fun (env,ind,to_kind,r) ->
-        let pp_scheme () s = str (scheme_kind_name s) in
+        let pp_scheme () s = str (match scheme_kind_name s with (ss,_,_) -> String.concat " " ss) in
         fmt "Found unregistered eliminator %t for %t by name.@ \
              Use \"Register Scheme\" with it instead@ \
              (\"as %a\" if dependent or \"as %a\" if non dependent)."
@@ -156,20 +251,44 @@ let build_case_analysis_scheme_in_type env dep sort ind =
   let sigma, sort = Evd.fresh_sort_in_quality ~rigid:UnivRigid sigma sort in
   let (sigma, c) = build_case_analysis_scheme env sigma indu dep sort in
   let (c, _) = Indrec.eval_case_analysis c in
-  EConstr.Unsafe.to_constr c, Evd.ustate sigma
+  Some (EConstr.Unsafe.to_constr c, Evd.ustate sigma)
 
 let case_dep =
-  declare_individual_scheme_object "case_dep"
-    (fun env _ x -> build_case_analysis_scheme_in_type env true QualityOrSet.qtype x)
-
-let case_nodep =
-  declare_individual_scheme_object "case_nodep"
-    (fun env _ x -> build_case_analysis_scheme_in_type env false QualityOrSet.qtype x)
+    declare_individual_scheme_object (["Elimination"], Some QualityOrSet.qtype)
+      (fun id -> make_suff_sort id "caset" true)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env true QualityOrSet.qtype x)
 
 let casep_dep =
-  declare_individual_scheme_object "casep_dep"
-    (fun env _ x -> build_case_analysis_scheme_in_type env true QualityOrSet.prop x)
+    declare_individual_scheme_object (["Elimination"], Some QualityOrSet.prop)
+      (fun id -> make_suff_sort id "case" true)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env true QualityOrSet.prop x)
+
+let cases_dep =
+    declare_individual_scheme_object (["Elimination"], Some QualityOrSet.sprop)
+      (fun id -> make_suff_sort id "cases" true)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env true QualityOrSet.sprop x)
+
+let casep_dep_set =
+    declare_individual_scheme_object (["Elimination"], Some QualityOrSet.set)
+      (fun id -> make_suff_sort id "case" true)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env true QualityOrSet.set x)
+
+let case_nodep =
+    declare_individual_scheme_object (["Case"], Some QualityOrSet.qtype)
+      (fun id -> make_suff_sort id "caset" false)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env false QualityOrSet.qtype x)
 
 let casep_nodep =
-  declare_individual_scheme_object "casep_nodep"
-    (fun env _ x -> build_case_analysis_scheme_in_type env false QualityOrSet.prop x)
+    declare_individual_scheme_object (["Case"], Some QualityOrSet.prop)
+      (fun id -> make_suff_sort id "case" false)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env false QualityOrSet.prop x)
+
+let cases_nodep =
+    declare_individual_scheme_object (["Case"], Some QualityOrSet.sprop)
+      (fun id -> make_suff_sort id "cases" false)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env false QualityOrSet.sprop x)
+
+let case_nodep_set =
+    declare_individual_scheme_object (["Case"], Some QualityOrSet.set)
+      (fun id -> make_suff_sort id "case" false)
+      (fun env _ x _ -> build_case_analysis_scheme_in_type env false QualityOrSet.set x)      

tactics/elimschemes.mli

@@ -14,13 +14,27 @@ open Ind_tables
 
 val elim_scheme : dep:bool -> to_kind:UnivGen.QualityOrSet.t -> individual scheme_kind
 
+val mutual_rect_dep : mutual scheme_kind
+val mutual_rec_dep : mutual scheme_kind
+val mutual_ind_dep : mutual scheme_kind
+val mutual_sind_dep : mutual scheme_kind
+val mutual_rect_nodep : mutual scheme_kind
+val mutual_rec_nodep : mutual scheme_kind
+val mutual_ind_nodep : mutual scheme_kind
+val mutual_sind_nodep : mutual scheme_kind
+
 (** Case analysis schemes *)
 
 val case_dep : individual scheme_kind
 val case_nodep : individual scheme_kind
 val casep_dep : individual scheme_kind
 val casep_nodep : individual scheme_kind
 
+val cases_dep : individual scheme_kind
+val cases_nodep : individual scheme_kind
+val casep_dep_set : individual scheme_kind
+val case_nodep_set : individual scheme_kind
+
 (** Recursor names utilities *)
 
 val lookup_eliminator : Environ.env -> Names.inductive -> UnivGen.QualityOrSet.t -> Names.GlobRef.t