Source file `elimschemes.ml`

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *         Copyright INRIA, CNRS and contributors             *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(* 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 builds schemes related to case analysis and recursion schemes *)

open Sorts
open Constr
open Indrec
open Declarations
open Typeops
open Ind_tables

(* Induction/recursion schemes *)

let optimize_non_type_induction_scheme kind dep sort env _handle ind =
  let sigma = Evd.from_env env in
  (* This non-local call to [lookup_scheme] is fine since we do not use it on a
     dependency generated on the fly. *)
  match lookup_scheme kind ind with
  | Some cte ->
    (* in case the inductive has a type elimination, generates only one
       induction scheme, the other ones share the same code with the
       appropriate type *)
    let sigma, cte = Evd.fresh_constant_instance env sigma cte in
    let c = mkConstU cte in
    let t = type_of_constant_in env cte in
    let (mib,mip) = Inductive.lookup_mind_specif env ind in
    let npars =
      (* if a constructor of [ind] contains a recursive call, the scheme
         is generalized only wrt recursively uniform parameters *)
      if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs)
      then
        mib.mind_nparams_rec
      else
        mib.mind_nparams in
    let sigma, sort = Evd.fresh_sort_in_family sigma sort in
    let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in
    let sigma = Evd.minimize_universes sigma in
    (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma)
  | None ->
    let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
    let sigma, c = build_induction_scheme env sigma pind dep sort in
      (c, Evd.evar_universe_context sigma)

let build_induction_scheme_in_type env dep sort ind =
  let sigma = Evd.from_env env in
  let sigma, pind = Evd.fresh_inductive_instance ~rigid:UState.univ_rigid env sigma ind in
  let sigma, c = build_induction_scheme env sigma pind dep sort in
    c, Evd.evar_universe_context sigma

let rect_scheme_kind_from_type =
  declare_individual_scheme_object "_rect_nodep"
    (fun env _ x -> build_induction_scheme_in_type env false InType x)

let rect_scheme_kind_from_prop =
  declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop"
    (fun env _ x -> build_induction_scheme_in_type env false InType x)

let rect_dep_scheme_kind_from_type =
  declare_individual_scheme_object "_rect" ~aux:"_rect_from_type"
    (fun env _ x -> build_induction_scheme_in_type env true InType x)

let rec_scheme_kind_from_type =
  declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type"
  (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet)

let rec_scheme_kind_from_prop =
  declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop"
  (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet)

let rec_dep_scheme_kind_from_type =
  declare_individual_scheme_object "_rec" ~aux:"_rec_from_type"
  (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet)

let ind_scheme_kind_from_type =
  declare_individual_scheme_object "_ind_nodep"
  (optimize_non_type_induction_scheme rec_scheme_kind_from_type false InProp)

let sind_scheme_kind_from_type =
  declare_individual_scheme_object "_sind_nodep"
  (fun env _ x -> build_induction_scheme_in_type env false InSProp x)

let ind_dep_scheme_kind_from_type =
  declare_individual_scheme_object "_ind" ~aux:"_ind_from_type"
  (optimize_non_type_induction_scheme rec_dep_scheme_kind_from_type true InProp)

let sind_dep_scheme_kind_from_type =
  declare_individual_scheme_object "_sind" ~aux:"_sind_from_type"
  (fun env _ x -> build_induction_scheme_in_type env true InSProp x)

let ind_scheme_kind_from_prop =
  declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop"
  (optimize_non_type_induction_scheme rec_scheme_kind_from_prop false InProp)

let sind_scheme_kind_from_prop =
  declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop"
  (fun env _ x -> build_induction_scheme_in_type env false InSProp x)

let nondep_elim_scheme from_kind to_kind =
  match from_kind, to_kind with
  | InProp, InProp  -> ind_scheme_kind_from_prop
  | InProp, InSProp -> sind_scheme_kind_from_prop
  | InProp, InSet   -> rec_scheme_kind_from_prop
  | InProp, (InType | InQSort) -> rect_scheme_kind_from_prop
  | _     , InProp  -> ind_scheme_kind_from_type
  | _     , InSProp -> sind_scheme_kind_from_type
  | _     , InSet   -> rec_scheme_kind_from_type
  | _     , (InType | InQSort) -> rect_scheme_kind_from_type

(* Case analysis *)

let build_case_analysis_scheme_in_type env dep sort ind =
  let sigma = Evd.from_env env in
  let (sigma, indu) = Evd.fresh_inductive_instance env sigma ind 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.evar_universe_context sigma

let case_scheme_kind_from_type =
  declare_individual_scheme_object "_case_nodep"
  (fun env _ x -> build_case_analysis_scheme_in_type env false InType x)

let case_scheme_kind_from_prop =
  declare_individual_scheme_object "_case" ~aux:"_case_from_prop"
  (fun env _ x -> build_case_analysis_scheme_in_type env false InType x)

let case_dep_scheme_kind_from_type =
  declare_individual_scheme_object "_case" ~aux:"_case_from_type"
  (fun env _ x -> build_case_analysis_scheme_in_type env true InType x)

let case_dep_scheme_kind_from_type_in_prop =
  declare_individual_scheme_object "_casep_dep"
  (fun env _ x -> build_case_analysis_scheme_in_type env true InProp x)

let case_dep_scheme_kind_from_prop =
  declare_individual_scheme_object "_case_dep"
  (fun env _ x -> build_case_analysis_scheme_in_type env true InType x)

let case_dep_scheme_kind_from_prop_in_prop =
  declare_individual_scheme_object "_casep"
  (fun env _ x -> build_case_analysis_scheme_in_type env true InProp x)