aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs/goal.ml
blob: e7a6bce6cd9e801af13c2a2caa398b3f015f31ed (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
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
(************************************************************************)
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
(*   \VV/  **************************************************************)
(*    //   *      This file is distributed under the terms of the       *)
(*         *       GNU Lesser General Public License Version 2.1        *)
(************************************************************************)

open Pp
open Term

(* This module implements the abstract interface to goals *)
(* A general invariant of the module, is that a goal whose associated
   evar is defined in the current evar_map, should not be accessed. *)

(* type of the goals *)
type goal = {
  content : Evd.evar;      (* Corresponding evar. Allows to retrieve
			      logical information once put together
			      with an evar_map. *)
  tags : string list       (* Heriditary? tags to be displayed *)
}
(* spiwack: I don't deal with the tags, yet. It is a worthy discussion
   whether we do want some tags displayed besides the goal or not. *)


let pr_goal {content = e} = str "GOAL:" ++ Pp.int e

(* access primitive *)
(* invariant : [e] must exist in [em] *)
let content evars { content = e } = Evd.find evars e


(* Builds a new (empty) goal with evar [e] *)
let build e =
  { content = e ;
    tags = []
  }


let uid {content = e} = string_of_int e
let get_by_uid u =
  (* this necessarily forget about tags.
     when tags are to be implemented, they
     should be done another way.
     We could use the store in evar_extra,
     for instance. *)
  build (int_of_string u)

(* Builds a new goal with content evar [e] and
   inheriting from goal [gl]*)
let descendent gl e =
  { gl with content = e}

(* [advance sigma g] returns [Some g'] if [g'] is undefined and
    is the current avatar of [g] (for instance [g] was changed by [clear]
    into [g']). It returns [None] if [g] has been (partially) solved. *)
open Store.Field
let rec advance sigma g =
  let evi = Evd.find sigma g.content in
  if Option.default false (Evarutil.cleared.get evi.Evd.evar_extra) then
    let v =
      match evi.Evd.evar_body with
      | Evd.Evar_defined c -> c
      | _ -> Errors.anomaly "Some goal is marked as 'cleared' but is uninstantiated"
    in
    let (e,_) = Term.destEvar v in
    let g' = { g with content = e } in
    advance sigma g'
  else
    match evi.Evd.evar_body with
    | Evd.Evar_defined _ -> None
    | _ -> Some g

(*** Goal tactics ***)


(* Goal tactics are [subgoal sensitive]-s *)
type subgoals = { subgoals: goal list }

(* type of the base elements of the goal API.*)
(* it has an extra evar_info with respect to what would be expected,
   it is supposed to be the evar_info of the goal in the evar_map.
   The idea is that it is computed by the [run] function as an
   optimisation, since it will generaly not change during the
   evaluation. *)
type 'a sensitive =
    Environ.env -> Evd.evar_map ref -> goal -> Evd.evar_info -> 'a

(* evaluates a goal sensitive value in a given goal (knowing the current evar_map). *)
(* the evar_info corresponding to the goal is computed at once
   as an optimisation (it shouldn't change during the evaluation). *)
let eval t env defs gl =
  let info = content defs gl in
  let env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
  let rdefs = ref defs in
  let r = t env rdefs gl info in
  ( r , !rdefs )

(* monadic bind on sensitive expressions *)
let bind e f env rdefs goal info =
  f (e env rdefs goal info) env rdefs goal info

(* monadic return on sensitive expressions *)
let return v _ _ _ _ = v

(* interpretation of "open" constr *)
(* spiwack: it is a wrapper around [Constrintern.interp_open_constr].
    In an ideal world, this could/should be the other way round.
    As of now, though, it seems at least quite useful to build tactics. *)
let interp_constr cexpr env rdefs _ _ =
  let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in
  rdefs := defs ;
  c

(* Type of constr with holes used by refine. *)
(* The list of evars doesn't necessarily contain all the evars in the constr,
    only those the constr has introduced. *)
(* The variables in [myevars] are supposed to be stored
   in decreasing order. Breaking this invariant might cause
   many things to go wrong. *)
type refinable = {
  me: constr;
  my_evars: Evd.evar list
}

module Refinable = struct
  type t = refinable

  type handle = Evd.evar list ref

  let make t env rdefs gl info =
    let r = ref [] in
    let me = t r env rdefs gl info in
    { me = me;
       my_evars = !r }
  let make_with t env rdefs gl info =
    let r = ref [] in
    let (me,side) = t r env rdefs gl info in
    { me = me ; my_evars = !r } , side

  let mkEvar handle env typ _ rdefs _ _ =
    let ev = Evarutil.e_new_evar rdefs env typ in
    let (e,_) = Term.destEvar ev in
    handle := e::!handle;
    ev

  (* [with_type c typ] constrains term [c] to have type [typ].  *)
  let with_type t typ env rdefs _ _ =
    (* spiwack: this function assumes that no evars can be created during
        this sort of coercion.
        If it is not the case it could produce bugs. We would need to add a handle
        and add the new evars to it. *)
    let my_type = Retyping.get_type_of env !rdefs t in
    let j = Environ.make_judge t my_type in
    let (new_defs,j') =
      Coercion.inh_conv_coerce_to (Loc.ghost) env !rdefs j typ
    in
    rdefs := new_defs;
    j'.Environ.uj_val

  (* spiwack: it is not very fine grain since it solves all typeclasses holes,
      not only those containing the current goal, or a given term. But it
      seems to fit our needs so far. *)
  let resolve_typeclasses ?filter ?split ?(fail=false) () env rdefs _ _ =
    rdefs:=Typeclasses.resolve_typeclasses ?filter ?split ~fail env !rdefs;
    ()



  (* a pessimistic (i.e : there won't be many positive answers) filter
     over evar_maps, acting only on undefined evars *)
  let evar_map_filter_undefined f evm =
    Evd.fold_undefined
      (fun ev evi r -> if f ev evi then Evd.add r ev evi else r)
      evm
      Evd.empty

  (* Union, sorted in decreasing order, of two lists of evars in decreasing order. *)
  let rec fusion l1 l2 = match l1 , l2 with
    | [] , _ -> l2
    | _ , [] -> l1
    | a::l1 , b::_ when a>b -> a::(fusion l1 l2)
    | a::l1 , b::l2 when a=b -> a::(fusion l1 l2)
    | _ , b::l2 -> b::(fusion l1 l2)

  let update_handle handle init_defs post_defs =
    (* [delta_evars] holds the evars that have been introduced by this
       refinement (but not immediatly solved) *)
    (* spiwack: this is the hackish part, don't know how to do any better though. *)
    let delta_evars = evar_map_filter_undefined
      (fun ev _ -> not (Evd.mem init_defs ev))
      post_defs
    in
    (* [delta_evars] in the shape of a list of [evar]-s*)
    let delta_list = List.map fst (Evd.to_list delta_evars) in
    (* The variables in [myevars] are supposed to be stored
       in decreasing order. Breaking this invariant might cause
       many things to go wrong. *)
    handle := fusion delta_list !handle;
    delta_evars

  (* [constr_of_raw] is a pretyping function. The [check_type] argument
      asks whether the term should have the same type as the conclusion.
      [resolve_classes] is a flag on pretyping functions which, if set to true,
      calls the typeclass resolver.
      The principal argument is a [glob_constr] which is then pretyped in the
      context of a term, the remaining evars are registered to the handle.
      It is the main component of the toplevel refine tactic.*)
  (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
      a bit hackish. However it does not seem possible to move it out until
      pretyping is defined as some proof procedure. *)
  let constr_of_raw handle check_type resolve_classes rawc env rdefs gl info =
    (* We need to keep trace of what [rdefs] was originally*)
    let init_defs = !rdefs in
    (* if [check_type] is true, then creates a type constraint for the
       proof-to-be *)
    let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in
    (* call to [understand_tcc_evars] returns a constr with undefined evars
       these evars will be our new goals *)
    let open_constr =
      Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc
    in
      ignore(update_handle handle init_defs !rdefs);
      open_constr

  let constr_of_open_constr handle check_type (evars, c) env rdefs gl info =
    let delta = update_handle handle !rdefs evars in
      rdefs := Evd.fold (fun ev evi evd -> Evd.add evd ev evi) delta !rdefs;
      if check_type then with_type c (Evd.evar_concl (content !rdefs gl)) env rdefs gl info
      else c

end

(* [refine t] takes a refinable term and use it as a partial proof for current
    goal. *)
let refine step env rdefs gl info =
  (* subgoals to return *)
  (* The evars in [my_evars] are stored in reverse order.
     It is expectingly better however to display the goal
     in increasing order. *)
  rdefs := Evarconv.consider_remaining_unif_problems env !rdefs ;
  let subgoals = List.map (descendent gl) (List.rev step.my_evars) in
  (* creates the new [evar_map] by defining the evar of the current goal
     as being [refine_step]. *)
  let new_defs = Evd.define gl.content (step.me) !rdefs in
  rdefs := new_defs;
  (* Filtering the [subgoals] for uninstanciated (=unsolved) goals. *)
  let subgoals =
    Option.List.flatten (List.map (advance !rdefs) subgoals)
  in
  { subgoals = subgoals }


(*** Cleaning  goals ***)

let clear ids env rdefs gl info =
  let hyps = Evd.evar_hyps info in
  let concl = Evd.evar_concl info in
  let (hyps,concl) = Evarutil.clear_hyps_in_evi rdefs hyps concl ids in
  let cleared_env = Environ.reset_with_named_context hyps env in
  let cleared_concl = Evarutil.e_new_evar rdefs cleared_env concl in
  let (cleared_evar,_) = Term.destEvar cleared_concl in
  let cleared_goal = descendent gl cleared_evar in
  rdefs := Evd.define gl.content cleared_concl !rdefs;
  { subgoals = [cleared_goal] }

let wrap_apply_to_hyp_and_dependent_on sign id f g =
  try Environ.apply_to_hyp_and_dependent_on sign id f g
  with Environ.Hyp_not_found ->
    Errors.error "No such assumption"

let check_typability env sigma c =
  let _ = Typing.type_of env sigma c in ()

let recheck_typability (what,id) env sigma t =
  try check_typability env sigma t
  with _ ->
    let s = match what with
      | None -> "the conclusion"
      | Some id -> "hypothesis "^(Names.string_of_id id) in
    Errors.error
      ("The correctness of "^s^" relies on the body of "^(Names.string_of_id id))

let remove_hyp_body env sigma id =
  let sign =
    wrap_apply_to_hyp_and_dependent_on (Environ.named_context_val env) id
      (fun (_,c,t) _ ->
	match c with
	| None -> Errors.error ((Names.string_of_id id)^" is not a local definition")
	| Some c ->(id,None,t))
      (fun (id',c,t as d) sign ->
	(
	  begin
	    let env = Environ.reset_with_named_context sign env in
	    match c with
	    | None ->  recheck_typability (Some id',id) env sigma t
	    | Some b ->
		let b' = mkCast (b,DEFAULTcast, t) in
		recheck_typability (Some id',id) env sigma b'
	  end;d))
  in
  Environ.reset_with_named_context sign env


let clear_body idents env rdefs gl info =
  let info = content !rdefs gl in
  let full_env = Environ.reset_with_named_context (Evd.evar_hyps info) env in
  let aux env id =
     let env' = remove_hyp_body env !rdefs id in
       recheck_typability (None,id) env' !rdefs (Evd.evar_concl info);
       env'
  in
  let new_env =
    List.fold_left aux full_env idents
  in
  let concl = Evd.evar_concl info in
  let (defs',new_constr) = Evarutil.new_evar !rdefs new_env concl in
  let (new_evar,_) = destEvar new_constr in
  let new_goal = descendent gl new_evar in
  rdefs := Evd.define gl.content new_constr defs';
  { subgoals = [new_goal] }


(*** Sensitive primitives ***)

(* [concl] is the conclusion of the current goal *)
let concl _ _ _ info =
  Evd.evar_concl info

(* [hyps] is the [named_context_val] representing the hypotheses
   of the current goal *)
let hyps _ _ _ info =
  Evd.evar_hyps info

(* [env] is the current [Environ.env] containing both the
   environment in which the proof is ran, and the goal hypotheses *)
let env env _ _ _ = env

(* [defs] is the [Evd.evar_map] at the current evaluation point *)
let defs _ rdefs _ _ =
  !rdefs

(* Cf mli for more detailed comment.
    [null], [plus], [here] and [here_list] use internal exception [UndefinedHere]
    to communicate whether or not the value is defined in the particular context. *)
exception UndefinedHere
(* no handler: this should never be allowed to reach toplevel *)
let null _ _ _ _ = raise UndefinedHere

let plus s1 s2 env rdefs goal info =
  try s1 env rdefs goal info
  with UndefinedHere -> s2 env rdefs goal info

(* Equality of two goals *)
let equal { content = e1 } { content = e2 } = e1 = e2

let here goal value _ _ goal' _ =
  if equal goal goal' then
    value
  else
    raise UndefinedHere

(* arnaud: voir à la passer dans Util ? *)
let rec list_mem_with eq x = function
  | y::_ when eq x y -> true
  | _::l -> list_mem_with eq x l
  | [] -> false

let here_list goals value _ _ goal' _ =
  if list_mem_with equal goal' goals then
    value
  else
    raise UndefinedHere


(*** Conversion in goals ***)

let convert_hyp check (id,b,bt as d) env rdefs gl info =
  let sigma = !rdefs in
  (* This function substitutes the new type and body definitions
     in the appropriate variable when used with {!Environ.apply_hyps}. *)
  let replace_function =
    (fun _ (_,c,ct) _ ->
       if check && not (Reductionops.is_conv env sigma bt ct) then
	 Errors.error ("Incorrect change of the type of "^(Names.string_of_id id));
       if check && not (Option.Misc.compare (Reductionops.is_conv env sigma) b c) then
	 Errors.error ("Incorrect change of the body of "^(Names.string_of_id id));
       d)
  in
  (* Modified named context. *)
  let new_hyps =
    Environ.apply_to_hyp (hyps env rdefs gl info) id replace_function
  in
  let new_env = Environ.reset_with_named_context new_hyps env in
  let new_constr =
    Evarutil.e_new_evar rdefs new_env (concl env rdefs gl info)
  in
  let (new_evar,_) = Term.destEvar new_constr in
  let new_goal = descendent gl new_evar in
  rdefs := Evd.define gl.content new_constr !rdefs;
  { subgoals = [new_goal] }

let convert_concl check cl' env rdefs gl info =
  let sigma = !rdefs in
  let cl = concl env rdefs gl info in
  check_typability env sigma cl';
  if (not check) || Reductionops.is_conv_leq env sigma cl' cl then
    let new_constr =
      Evarutil.e_new_evar rdefs env cl'
    in
    let (new_evar,_) = Term.destEvar new_constr in
    let new_goal = descendent gl new_evar in
    rdefs := Evd.define gl.content new_constr !rdefs;
    { subgoals = [new_goal] }
  else
    Errors.error "convert-concl rule passed non-converting term"


(*** Bureaucracy in hypotheses ***)

(* Renames a hypothesis. *)
let rename_hyp_sign id1 id2 sign =
  Environ.apply_to_hyp_and_dependent_on sign id1
    (fun (_,b,t) _ -> (id2,b,t))
    (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
let rename_hyp id1 id2 env rdefs gl info =
  let hyps = hyps env rdefs gl info in
  if id1 <> id2 &&
    List.mem id2 (Termops.ids_of_named_context (Environ.named_context_of_val hyps)) then
       Errors.error ((Names.string_of_id id2)^" is already used.");
  let new_hyps = rename_hyp_sign id1 id2 hyps in
  let new_env = Environ.reset_with_named_context new_hyps env in
  let new_concl = Term.replace_vars [id1,mkVar id2] (concl env rdefs gl info) in
  let new_subproof = Evarutil.e_new_evar rdefs new_env new_concl in
  let new_subproof = Term.replace_vars [id2,mkVar id1] new_subproof in
  let (new_evar,_) = Term.destEvar new_subproof in
  let new_goal = descendent gl new_evar in
  rdefs := Evd.define gl.content new_subproof !rdefs;
  { subgoals = [new_goal] }

(*** Additional functions ***)

(* emulates List.map for functions of type
   [Evd.evar_map -> 'a -> 'b * Evd.evar_map] on lists of type 'a, by propagating
   new evar_map to next definition. *)
(*This sort of construction actually works with any monad (here the State monade
   in Haskell). There is a generic construction in Haskell called mapM.
*)
let rec list_map f l s =
  match l with
  | [] -> ([],s)
  | a::l -> let (a,s) = f s a in
               let (l,s) = list_map f l s in
	       (a::l,s)


(* Layer to implement v8.2 tactic engine ontop of the new architecture.
   Types are different from what they used to be due to a change of the
   internal types. *)
module V82 = struct

  (* Old style env primitive *)
  let env evars gl =
    let evi = content evars gl in
    Evd.evar_env evi

  (* For printing *)
  let unfiltered_env evars gl =
    let evi = content evars gl in
    Evd.evar_unfiltered_env evi

  (* Old style hyps primitive *)
  let hyps evars gl =
    let evi = content evars gl in
    evi.Evd.evar_hyps

  (* Access to ".evar_concl" *)
  let concl evars gl =
    let evi = content evars gl in
    evi.Evd.evar_concl

  (* Access to ".evar_extra" *)
  let extra evars gl =
    let evi = content evars gl in
    evi.Evd.evar_extra

  (* Old style filtered_context primitive *)
  let filtered_context evars gl =
    let evi = content evars gl in
    Evd.evar_filtered_context evi

  (* Old style mk_goal primitive *)
  let mk_goal evars hyps concl extra =
    let evk = Evarutil.new_untyped_evar () in
    let evi = { Evd.evar_hyps = hyps;
		Evd.evar_concl = concl;
		Evd.evar_filter = List.map (fun _ -> true)
	(Environ.named_context_of_val hyps);
		Evd.evar_body = Evd.Evar_empty;
		Evd.evar_source = (Loc.ghost,Evar_kinds.GoalEvar);
		Evd.evar_candidates = None;
		Evd.evar_extra = extra }
    in
    let evi = Typeclasses.mark_unresolvable evi in
    let evars = Evd.add evars evk evi in
    let ids = List.map Util.pi1 (Environ.named_context_of_val hyps) in
    let inst = Array.of_list (List.map mkVar ids) in
    let ev = Term.mkEvar (evk,inst) in
    (build evk, ev, evars)

  (* Equality function on goals *)
  let equal evars gl1 gl2 =
    let evi1 = content evars gl1 in
    let evi2 = content evars gl2 in
    Evd.eq_evar_info evi1 evi2

  (* Creates a dummy [goal sigma] for use in auto *)
  let dummy_goal =
    (* This goal seems to be marshalled somewhere. Therefore it cannot be
       marked unresolvable for typeclasses, as non-empty Store.t-s happen
       to have functional content. *)
    let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
    let evk = Evarutil.new_untyped_evar () in
    let sigma = Evd.add Evd.empty evk evi in
    { Evd.it = build evk ; Evd.sigma = sigma }

  (* Makes a goal out of an evar *)
  let build = build

  (* Instantiates a goal with an open term *)
  let partial_solution sigma { content=evk } c =
    Evd.define evk c sigma

  (* Parts of the progress tactical *)
  let same_goal evars1 gl1 evars2 gl2 =
    let evi1 = content evars1 gl1 in
    let evi2 = content evars2 gl2 in
    Term.eq_constr evi1.Evd.evar_concl evi2.Evd.evar_concl &&
    Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps

  let weak_progress glss gls =
    match glss.Evd.it with
    | [ g ] -> not (same_goal glss.Evd.sigma g gls.Evd.sigma gls.Evd.it)
    | _ -> true

  let progress glss gls =
    weak_progress glss gls
    (* spiwack: progress normally goes like this:
    (Evd.progress_evar_map gls.Evd.sigma glss.Evd.sigma) || (weak_progress glss gls)
       This is immensly slow in the current implementation. Maybe we could
       reimplement progress_evar_map with restricted folds like "fold_undefined",
       with a good implementation of them.
    *)

  (* Used for congruence closure *)
  let new_goal_with sigma gl new_hyps =
    let evi = content sigma gl in
    let new_evi = { evi with Evd.evar_hyps = new_hyps } in
    let new_evi = Typeclasses.mark_unresolvable new_evi in
    let evk = Evarutil.new_untyped_evar () in
    let new_sigma = Evd.add Evd.empty evk new_evi in
    { Evd.it = build evk ; sigma = new_sigma }

  (* Used by the compatibility layer and typeclasses *)
  let nf_evar sigma gl =
    let evi = content sigma gl in
    let evi = Evarutil.nf_evar_info sigma evi in
    let sigma = Evd.add sigma gl.content evi in
    (gl,sigma)

  (* Goal represented as a type, doesn't take into account section variables *)
  let abstract_type sigma gl =
    let (gl,sigma) = nf_evar sigma gl in
    let env = env sigma gl in
    let genv = Global.env () in
    let is_proof_var decl =
      try ignore (Environ.lookup_named (Util.pi1 decl) genv); false
      with Not_found -> true in
    Environ.fold_named_context_reverse (fun t decl ->
					  if is_proof_var decl then
					    mkNamedProd_or_LetIn decl t
					  else
					    t
				       ) ~init:(concl sigma gl) env

end