aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac/comProgramFixpoint.ml
blob: af34f8b299a685fd29acce535db766c530f9d3d4 (plain)
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
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
open Pp
open CErrors
open Util
open Constr
open Entries
open Vars
open Declare
open Names
open Libnames
open Globnames
open Nameops
open Constrexpr
open Constrexpr_ops
open Constrintern
open Decl_kinds
open Evarutil
open Context.Rel.Declaration
open ComFixpoint

module RelDecl = Context.Rel.Declaration

(* Wellfounded definition *)

open Coqlib

let contrib_name = "Program"
let subtac_dir = [contrib_name]
let fixsub_module = subtac_dir @ ["Wf"]
(* let tactics_module = subtac_dir @ ["Tactics"] *)

let init_reference dir s () = Coqlib.coq_reference "Command" dir s
let init_constant dir s sigma =
  Evarutil.new_global sigma (Coqlib.coq_reference "Command" dir s)

let make_ref l s = init_reference l s
(* let fix_proto = init_constant tactics_module "fix_proto" *)
let fix_sub_ref = make_ref fixsub_module "Fix_sub"
let measure_on_R_ref = make_ref fixsub_module "MR"
let well_founded = init_constant ["Init"; "Wf"] "well_founded"
let mkSubset sigma name typ prop =
  let open EConstr in
  let sigma, app_h = Evarutil.new_global sigma (delayed_force build_sigma).typ in
  sigma, mkApp (app_h, [| typ; mkLambda (name, typ, prop) |])

let sigT = Lazy.from_fun build_sigma_type

let make_qref s = Qualid (Loc.tag @@ qualid_of_string s)
let lt_ref = make_qref "Init.Peano.lt"

let rec telescope sigma l =
  let open EConstr in
  let open Vars in
  match l with
  | [] -> assert false
  | [LocalAssum (n, t)] ->
    sigma, t, [LocalDef (n, mkRel 1, t)], mkRel 1
  | LocalAssum (n, t) :: tl ->
      let sigma, ty, tys, (k, constr) =
        List.fold_left
          (fun (sigma, ty, tys, (k, constr)) decl ->
            let t = RelDecl.get_type decl in
            let pred = mkLambda (RelDecl.get_name decl, t, ty) in
            let sigma, ty = Evarutil.new_global sigma (Lazy.force sigT).typ in
            let sigma, intro = Evarutil.new_global sigma (Lazy.force sigT).intro in
            let sigty = mkApp (ty, [|t; pred|]) in
            let intro = mkApp (intro, [|lift k t; lift k pred; mkRel k; constr|]) in
              (sigma, sigty, pred :: tys, (succ k, intro)))
          (sigma, t, [], (2, mkRel 1)) tl
      in
      let sigma, last, subst = List.fold_right2
        (fun pred decl (sigma, prev, subst) ->
          let t = RelDecl.get_type decl in
          let sigma, p1 = Evarutil.new_global sigma (Lazy.force sigT).proj1 in
          let sigma, p2 = Evarutil.new_global sigma (Lazy.force sigT).proj2 in
          let proj1 = applist (p1, [t; pred; prev]) in
          let proj2 = applist (p2, [t; pred; prev]) in
            (sigma, lift 1 proj2, LocalDef (get_name decl, proj1, t) :: subst))
        (List.rev tys) tl (sigma, mkRel 1, [])
      in sigma, ty, (LocalDef (n, last, t) :: subst), constr

  | LocalDef (n, b, t) :: tl ->
    let sigma, ty, subst, term = telescope sigma tl in
    sigma, ty, (LocalDef (n, b, t) :: subst), lift 1 term

let nf_evar_context sigma ctx =
  List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx

let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
  let open EConstr in
  let open Vars in
  let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
  Coqlib.check_required_library ["Coq";"Program";"Wf"];
  let env = Global.env() in
  let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
  let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in
  let len = List.length binders_rel in
  let top_env = push_rel_context binders_rel env in
  let sigma, top_arity = interp_type_evars top_env sigma arityc in
  let full_arity = it_mkProd_or_LetIn top_arity binders_rel in
  let sigma, argtyp, letbinders, make = telescope sigma binders_rel in
  let argname = Id.of_string "recarg" in
  let arg = LocalAssum (Name argname, argtyp) in
  let binders = letbinders @ [arg] in
  let binders_env = push_rel_context binders_rel env in
  let sigma, (rel, _) = interp_constr_evars_impls env sigma r in
  let relty = Typing.unsafe_type_of env sigma rel in
  let relargty =
    let error () =
      user_err ?loc:(constr_loc r)
               ~hdr:"Command.build_wellfounded"
                    (Printer.pr_econstr_env env sigma rel ++ str " is not an homogeneous binary relation.")
    in
      try
        let ctx, ar = Reductionops.splay_prod_n env sigma 2 relty in
          match ctx, EConstr.kind sigma ar with
          | [LocalAssum (_,t); LocalAssum (_,u)], Sort s
              when Sorts.is_prop (ESorts.kind sigma s) && Reductionops.is_conv env sigma t u -> t
          | _, _ -> error ()
      with e when CErrors.noncritical e -> error ()
  in
  let sigma, measure = interp_casted_constr_evars binders_env sigma measure relargty in
  let sigma, wf_rel, wf_rel_fun, measure_fn =
    let measure_body, measure =
      it_mkLambda_or_LetIn measure letbinders,
      it_mkLambda_or_LetIn measure binders
    in
    let sigma, comb = Evarutil.new_global sigma (delayed_force measure_on_R_ref) in
    let wf_rel = mkApp (comb, [| argtyp; relargty; rel; measure |]) in
    let wf_rel_fun x y =
      mkApp (rel, [| subst1 x measure_body;
                     subst1 y measure_body |])
    in sigma, wf_rel, wf_rel_fun, measure
  in
  let sigma, wf_term = well_founded sigma in
  let wf_proof = mkApp (wf_term, [| argtyp ; wf_rel |]) in
  let argid' = Id.of_string (Id.to_string argname ^ "'") in
  let wfarg sigma len =
    let sigma, ss_term = mkSubset sigma (Name argid') argtyp (wf_rel_fun (mkRel 1) (mkRel (len + 1))) in
    sigma, LocalAssum (Name argid', ss_term)
  in
  let sigma, intern_bl =
    let sigma, wfa = wfarg sigma 1 in
    sigma, wfa :: [arg]
  in
  let _intern_env = push_rel_context intern_bl env in
  let sigma, proj = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.proj1 in
  let wfargpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel 3)) in
  let projection = (* in wfarg :: arg :: before *)
    mkApp (proj, [| argtyp ; wfargpred ; mkRel 1 |])
  in
  let top_arity_let = it_mkLambda_or_LetIn top_arity letbinders in
  let intern_arity = substl [projection] top_arity_let in
  (* substitute the projection of wfarg for something,
     now intern_arity is in wfarg :: arg *)
  let sigma, wfa = wfarg sigma 1 in
  let intern_fun_arity_prod = it_mkProd_or_LetIn intern_arity [wfa] in
  let intern_fun_binder = LocalAssum (Name (add_suffix recname "'"), intern_fun_arity_prod) in
  let sigma, curry_fun =
    let wfpred = mkLambda (Name argid', argtyp, wf_rel_fun (mkRel 1) (mkRel (2 * len + 4))) in
    let sigma, intro = Evarutil.new_global sigma (delayed_force build_sigma).Coqlib.intro in
    let arg = mkApp (intro, [| argtyp; wfpred; lift 1 make; mkRel 1 |]) in
    let app = mkApp (mkRel (2 * len + 2 (* recproof + orig binders + current binders *)), [| arg |]) in
    let rcurry = mkApp (rel, [| measure; lift len measure |]) in
    let lam = LocalAssum (Name (Id.of_string "recproof"), rcurry) in
    let body = it_mkLambda_or_LetIn app (lam :: binders_rel) in
    let ty = it_mkProd_or_LetIn (lift 1 top_arity) (lam :: binders_rel) in
    sigma, LocalDef (Name recname, body, ty)
  in
  let fun_bl = intern_fun_binder :: [arg] in
  let lift_lets = lift_rel_context 1 letbinders in
  let sigma, intern_body =
    let ctx = LocalAssum (Name recname, get_type curry_fun) :: binders_rel in
    let (r, l, impls, scopes) =
      Constrintern.compute_internalization_data env
        Constrintern.Recursive (EConstr.Unsafe.to_constr full_arity) impls
    in
    let newimpls = Id.Map.singleton recname
        (r, l, impls @ [(Some (Id.of_string "recproof", Impargs.Manual, (true, false)))],
         scopes @ [None]) in
    interp_casted_constr_evars (push_rel_context ctx env) sigma
      ~impls:newimpls body (lift 1 top_arity)
  in
  let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in
  let prop = mkLambda (Name argname, argtyp, top_arity_let) in
  (* XXX: Previous code did parallel evdref update, so possible old
     weak ordering semantics may bite here. *)
  let sigma, def =
    let sigma, h_a_term = Evarutil.new_global sigma (delayed_force fix_sub_ref) in
    let sigma, h_e_term = Evarutil.new_evar env sigma
        ~src:(Loc.tag @@ Evar_kinds.QuestionMark (Evar_kinds.Define false,Anonymous)) wf_proof in
    sigma, mkApp (h_a_term, [| argtyp ; wf_rel ; h_e_term; prop |])
  in
  let _evd = ref sigma in
  let def = Typing.e_solve_evars env _evd def in
  let sigma = !_evd in
  let sigma = Evarutil.nf_evar_map sigma in
  let def = mkApp (def, [|intern_body_lam|]) in
  let binders_rel = nf_evar_context sigma binders_rel in
  let binders = nf_evar_context sigma binders in
  let top_arity = Evarutil.nf_evar sigma top_arity in
  let hook, recname, typ =
    if List.length binders_rel > 1 then
      let name = add_suffix recname "_func" in
      (* XXX: Mutating the evar_map in the hook! *)
      (* XXX: Likely the sigma is out of date when the hook is called .... *)
      let hook sigma l gr _ =
        let sigma, h_body = Evarutil.new_global sigma gr in
        let body = it_mkLambda_or_LetIn (mkApp (h_body, [|make|])) binders_rel in
        let ty = it_mkProd_or_LetIn top_arity binders_rel in
        let ty = EConstr.Unsafe.to_constr ty in
        let univs = Evd.check_univ_decl ~poly sigma decl in
        (*FIXME poly? *)
        let ce = definition_entry ~types:ty ~univs (EConstr.to_constr sigma body) in
        (** FIXME: include locality *)
        let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
        let gr = ConstRef c in
        let () = Universes.register_universe_binders gr (Evd.universe_binders sigma) in
        if Impargs.is_implicit_args () || not (List.is_empty impls) then
          Impargs.declare_manual_implicits false gr [impls]
      in
      let typ = it_mkProd_or_LetIn top_arity binders in
      hook, name, typ
    else
      let typ = it_mkProd_or_LetIn top_arity binders_rel in
      let hook sigma l gr _ =
        if Impargs.is_implicit_args () || not (List.is_empty impls) then
          Impargs.declare_manual_implicits false gr [impls]
      in hook, recname, typ
  in
  (* XXX: Capturing sigma here... bad bad *)
  let hook = Lemmas.mk_hook (hook sigma) in
  let fullcoqc = EConstr.to_constr sigma def in
  let fullctyp = EConstr.to_constr sigma typ in
  Obligations.check_evars env sigma;
  let evars, _, evars_def, evars_typ =
    Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp
  in
  let ctx = Evd.evar_universe_context sigma in
    ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl
             evars_typ ctx evars ~hook)

let out_def = function
  | Some def -> def
  | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.")

let collect_evars_of_term evd c ty =
  let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in
  Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev))
  evars (Evd.from_ctx (Evd.evar_universe_context evd))

let do_program_recursive local poly fixkind fixl ntns =
  let cofix = fixkind = Obligations.IsCoFixpoint in
  let (env, rec_sign, pl, evd), fix, info =
    interp_recursive ~cofix ~program_mode:true fixl ntns
  in
    (* Program-specific code *)
    (* Get the interesting evars, those that were not instanciated *)
  let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in
    (* Solve remaining evars *)
  let evd = nf_evar_map_undefined evd in
  let collect_evars id def typ imps =
    (* Generalize by the recursive prototypes  *)
    let def =
      EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
    and typ =
      EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
    in
    let evm = collect_evars_of_term evd def typ in
    let evars, _, def, typ =
      Obligations.eterm_obligations env id evm
        (List.length rec_sign) def typ
    in (id, def, typ, imps, evars)
  in
  let (fixnames,fixdefs,fixtypes) = fix in
  let fiximps = List.map pi2 info in
  let fixdefs = List.map out_def fixdefs in
  let defs = List.map4 collect_evars fixnames fixdefs fixtypes fiximps in
  let () = if not cofix then begin
      let possible_indexes = List.map ComFixpoint.compute_possible_guardness_evidences info in
      let fixdecls = Array.of_list (List.map (fun x -> Name x) fixnames),
        Array.of_list fixtypes,
        Array.of_list (List.map (subst_vars (List.rev fixnames)) fixdefs)
      in
      let indexes =
        Pretyping.search_guard (Global.env ()) possible_indexes fixdecls in
      List.iteri (fun i _ ->
          Inductive.check_fix env
                              ((indexes,i),fixdecls))
        fixl
  end in
  let ctx = Evd.evar_universe_context evd in
  let kind = match fixkind with
  | Obligations.IsFixpoint _ -> (local, poly, Fixpoint)
  | Obligations.IsCoFixpoint -> (local, poly, CoFixpoint)
  in
  Obligations.add_mutual_definitions defs ~kind ~univdecl:pl ctx ntns fixkind

let do_program_fixpoint local poly l =
  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
    match g, l with
    | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
        let recarg =
          match n with
          | Some n -> mkIdentC n.CAst.v
          | None ->
              user_err ~hdr:"do_program_fixpoint"
                (str "Recursive argument required for well-founded fixpoints")
        in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn

    | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] ->
        build_wellfounded (id, pl, n, bl, typ, out_def def) poly
          (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn

    | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
        let fixl,ntns = extract_fixpoint_components true l in
        let fixkind = Obligations.IsFixpoint g in
          do_program_recursive local poly fixkind fixl ntns

    | _, _ ->
        user_err ~hdr:"do_program_fixpoint"
          (str "Well-founded fixpoints not allowed in mutually recursive blocks")

let extract_cofixpoint_components l =
  let fixl, ntnl = List.split l in
  List.map (fun (({CAst.v=id},pl),bl,typ,def) ->
            {fix_name = id; fix_annot = None; fix_univs = pl;
             fix_binders = bl; fix_body = def; fix_type = typ}) fixl,
  List.flatten ntnl

let check_safe () =
  let open Declarations in
  let flags = Environ.typing_flags (Global.env ()) in
  flags.check_universes && flags.check_guarded

let do_fixpoint local poly l =
  do_program_fixpoint local poly l;
  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()

let do_cofixpoint local poly l =
  let fixl,ntns = extract_cofixpoint_components l in
  do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns;
  if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else ()