1
(************************************************************************)
2
(* v * The Coq Proof Assistant / The Coq Development Team *)
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
4
(* \VV/ **************************************************************)
5
(* // * This file is distributed under the terms of the *)
6
(* * GNU Lesser General Public License Version 2.1 *)
7
(************************************************************************)
9
(*i $Id: extraction.ml 11897 2009-02-09 19:28:02Z barras $ i*)
32
exception I of inductive_info
34
(* A set of all fixpoint functions currently being extracted *)
35
let current_fixpoints = ref ([] : constant list)
39
let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
41
let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
43
let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
45
(*S Generation of flags and signatures. *)
47
(* The type [flag] gives us information about any Coq term:
49
\item [TypeScheme] denotes a type scheme, that is
50
something that will become a type after enough applications.
51
More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
52
[s = Set], [Prop] or [Type]
53
\item [Default] denotes the other cases. It may be inexact after
54
instanciation. For example [(X:Type)X] is [Default] and may give [Set]
55
after instanciation, which is rather [TypeScheme]
56
\item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
57
\item [Info] is the opposite. The same example [(X:Type)X] shows
58
that an [Info] term might in fact be [Logic] later on.
61
type info = Logic | Info
63
type scheme = TypeScheme | Default
65
type flag = info * scheme
67
(*s [flag_of_type] transforms a type [t] into a [flag].
68
Really important function. *)
70
let rec flag_of_type env t =
71
let t = whd_betadeltaiota env none t in
72
match kind_of_term t with
73
| Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c
74
| Sort (Prop Null) -> (Logic,TypeScheme)
75
| Sort _ -> (Info,TypeScheme)
76
| _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default)
78
(*s Two particular cases of [flag_of_type]. *)
80
let is_default env t = (flag_of_type env t = (Info, Default))
82
exception NotDefault of kill_reason
84
let check_default env t =
85
match flag_of_type env t with
86
| _,TypeScheme -> raise (NotDefault Ktype)
87
| Logic,_ -> raise (NotDefault Kother)
90
let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme))
92
(*s [type_sign] gernerates a signature aimed at treating a type application. *)
94
let rec type_sign env c =
95
match kind_of_term (whd_betadeltaiota env none c) with
97
(if is_info_scheme env t then Keep else Kill Kother)
98
:: (type_sign (push_rel_assum (n,t) env) d)
101
let rec type_scheme_nb_args env c =
102
match kind_of_term (whd_betadeltaiota env none c) with
104
let n = type_scheme_nb_args (push_rel_assum (n,t) env) d in
105
if is_info_scheme env t then n+1 else n
108
let _ = register_type_scheme_nb_args type_scheme_nb_args
110
(*s [type_sign_vl] does the same, plus a type var list. *)
112
let rec type_sign_vl env c =
113
match kind_of_term (whd_betadeltaiota env none c) with
115
let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in
116
if not (is_info_scheme env t) then Kill Kother::s, vl
117
else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
120
let rec nb_default_params env c =
121
match kind_of_term (whd_betadeltaiota env none c) with
123
let n = nb_default_params (push_rel_assum (n,t) env) d in
124
if is_default env t then n+1 else n
127
(*S Management of type variable contexts. *)
129
(* A De Bruijn variable context (db) is a context for translating Coq [Rel]
130
into ML type [Tvar]. *)
132
(*s From a type signature toward a type variable context (db). *)
135
let rec make i acc = function
137
| Keep :: l -> make (i+1) (i::acc) l
138
| Kill _ :: l -> make i (0::acc) l
141
(*s Create a type variable context from indications taken from
142
an inductive type (see just below). *)
144
let rec db_from_ind dbmap i =
146
else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
148
(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
149
of a constructor corresponds to the j-th type var of the ML inductive. *)
152
\item [si] : signature of the inductive
153
\item [i] : counter of Coq args for [(I args)]
154
\item [j] : counter of ML type vars
155
\item [relmax] : total args number of the constructor
158
let parse_ind_args si args relmax =
159
let rec parse i j = function
161
| Kill _ :: s -> parse (i+1) j s
163
(match kind_of_term args.(i-1) with
164
| Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
165
| _ -> parse (i+1) (j+1) s)
168
(*S Extraction of a type. *)
170
(* [extract_type env db c args] is used to produce an ML type from the
171
coq term [(c args)], which is supposed to be a Coq type. *)
173
(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
175
(* [j] stands for the next ML type var. [j=0] means we do not
176
generate ML type var anymore (in subterms for example). *)
179
let rec extract_type env db j c args =
180
match kind_of_term (whd_betaiotazeta Evd.empty c) with
182
(* We just accumulate the arguments. *)
183
extract_type env db j d (Array.to_list args' @ args)
186
| [] -> assert false (* otherwise the lambda would be reductible. *)
187
| a :: args -> extract_type env db j (subst1 a d) args)
190
let env' = push_rel_assum (n,t) env in
191
(match flag_of_type env t with
193
(* Standard case: two [extract_type] ... *)
194
let mld = extract_type env' (0::db) j d [] in
195
(match expand env mld with
196
| Tdummy d -> Tdummy d
197
| _ -> Tarr (extract_type env db 0 t [], mld))
198
| (Info, TypeScheme) when j > 0 ->
199
(* A new type var. *)
200
let mld = extract_type env' (j::db) (j+1) d [] in
201
(match expand env mld with
202
| Tdummy d -> Tdummy d
203
| _ -> Tarr (Tdummy Ktype, mld))
205
let mld = extract_type env' (0::db) j d [] in
206
(match expand env mld with
207
| Tdummy d -> Tdummy d
209
let reason = if lvl=TypeScheme then Ktype else Kother in
210
Tarr (Tdummy reason, mld)))
211
| Sort _ -> Tdummy Ktype (* The two logical cases. *)
212
| _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother
214
(match lookup_rel n env with
215
| (_,Some t,_) -> extract_type env db j (lift n t) args
217
(* Asks [db] a translation for [n]. *)
218
if n > List.length db then Tunknown
219
else let n' = List.nth db (n-1) in
220
if n' = 0 then Tunknown else Tvar n')
222
let r = ConstRef kn in
223
let cb = lookup_constant kn env in
224
let typ = Typeops.type_of_constant_type env cb.const_type in
225
(match flag_of_type env typ with
226
| (Info, TypeScheme) ->
227
let mlt = extract_type_app env db (r, type_sign env typ) args in
228
(match cb.const_body with
230
| Some _ when is_custom r -> mlt
232
let newc = applist (Declarations.force lbody, args) in
233
let mlt' = extract_type env db j newc [] in
234
(* ML type abbreviations interact badly with Coq *)
235
(* reduction, so [mlt] and [mlt'] might be different: *)
236
(* The more precise is [mlt'], extracted after reduction *)
237
(* The shortest is [mlt], which use abbreviations *)
238
(* If possible, we take [mlt], otherwise [mlt']. *)
239
if expand env mlt = expand env mlt' then mlt else mlt')
240
| _ -> (* only other case here: Info, Default, i.e. not an ML type *)
241
(match cb.const_body with
242
| None -> Tunknown (* Brutal approximation ... *)
244
(* We try to reduce. *)
245
let newc = applist (Declarations.force lbody, args) in
246
extract_type env db j newc []))
248
let s = (extract_ind env kn).ind_packets.(i).ip_sign in
249
extract_type_app env db (IndRef (kn,i),s) args
250
| Case _ | Fix _ | CoFix _ -> Tunknown
253
(* [extract_maybe_type] calls [extract_type] when used on a Coq type,
254
and otherwise returns [Tdummy] or [Tunknown] *)
256
and extract_maybe_type env db c =
257
let t = whd_betadeltaiota env none (type_of env c) in
258
if isSort t then extract_type env db 0 c []
259
else if sort_of env t = InProp then Tdummy Kother else Tunknown
261
(*s Auxiliary function dealing with type application.
262
Precondition: [r] is a type scheme represented by the signature [s],
263
and is completely applied: [List.length args = List.length s]. *)
265
and extract_type_app env db (r,s) args =
268
(fun (b,c) a -> if b=Keep then
269
let p = List.length (fst (splay_prod env none (type_of env c))) in
270
let db = iterate (fun l -> 0 :: l) p db in
271
(extract_type_scheme env db c p) :: a
273
(List.combine s args) []
274
in Tglob (r, ml_args)
276
(*S Extraction of a type scheme. *)
278
(* [extract_type_scheme env db c p] works on a Coq term [c] which is
279
an informative type scheme. It means that [c] is not a Coq type, but will
280
be when applied to sufficiently many arguments ([p] in fact).
281
This function decomposes p lambdas, with eta-expansion if needed. *)
283
(* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
285
and extract_type_scheme env db c p =
286
if p=0 then extract_type env db 0 c []
288
let c = whd_betaiotazeta Evd.empty c in
289
match kind_of_term c with
291
extract_type_scheme (push_rel_assum (n,t) env) db d (p-1)
293
let rels = fst (splay_prod env none (type_of env c)) in
294
let env = push_rels_assum rels env in
295
let eta_args = List.rev_map mkRel (interval 1 p) in
296
extract_type env db 0 (lift p c) eta_args
299
(*S Extraction of an inductive type. *)
301
and extract_ind env kn = (* kn is supposed to be in long form *)
302
let mib = Environ.lookup_mind kn env in
304
(* For a same kn, we can get various bodies due to module substitutions.
305
We hence check that the mib has not changed from recording
306
time to retrieving time. Ideally we should also check the env. *)
307
let (mib0,ml_ind) = lookup_ind kn in
308
if not (mib = mib0) then raise Not_found;
311
(* First, if this inductive is aliased via a Module, *)
312
(* we process the original inductive. *)
313
Option.iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv;
314
(* Everything concerning parameters. *)
315
(* We do that first, since they are common to all the [mib]. *)
316
let mip0 = mib.mind_packets.(0) in
317
let npar = mib.mind_nparams in
318
let epar = push_rel_context mib.mind_params_ctxt env in
319
(* First pass: we store inductive signatures together with *)
320
(* their type var list. *)
324
let b = snd (mind_arity mip) <> InProp in
325
let ar = Inductive.type_of_inductive env (mib,mip) in
326
let s,v = if b then type_sign_vl env ar else [],[] in
327
let t = Array.make (Array.length mip.mind_nf_lc) [] in
328
{ ip_typename = mip.mind_typename;
329
ip_consnames = mip.mind_consnames;
330
ip_logical = (not b);
337
{ind_info = Standard;
339
ind_packets = packets;
340
ind_equiv = match mib.mind_equiv with
342
| Some kn -> Equiv kn
344
(* Second pass: we extract constructors *)
345
for i = 0 to mib.mind_ntypes - 1 do
346
let p = packets.(i) in
347
if not p.ip_logical then
348
let types = arities_of_constructors env (kn,i) in
349
for j = 0 to Array.length types - 1 do
350
let t = snd (decompose_prod_n npar types.(j)) in
351
let prods,head = dest_prod epar t in
352
let nprods = List.length prods in
353
let args = match kind_of_term head with
354
| App (f,args) -> args (* [kind_of_term f = Ind ip] *)
357
let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
358
let db = db_from_ind dbmap npar in
359
p.ip_types.(j) <- extract_type_cons epar db dbmap t (npar+1)
362
(* Third pass: we determine special cases. *)
365
if not mib.mind_finite then raise (I Coinductive);
366
if mib.mind_ntypes <> 1 then raise (I Standard);
367
let p = packets.(0) in
368
if p.ip_logical then raise (I Standard);
369
if Array.length p.ip_types <> 1 then raise (I Standard);
370
let typ = p.ip_types.(0) in
371
let l = List.filter (fun t -> not (isDummy (expand env t))) typ in
372
if List.length l = 1 && not (type_mem_kn kn (List.hd l))
373
then raise (I Singleton);
374
if l = [] then raise (I Standard);
375
if not mib.mind_record then raise (I Standard);
378
if is_custom r then raise (I Standard);
379
(* Now we're sure it's a record. *)
380
(* First, we find its field names. *)
381
let rec names_prod t = match kind_of_term t with
382
| Prod(n,_,t) -> n::(names_prod t)
383
| LetIn(_,_,_,t) -> names_prod t
384
| Cast(t,_,_) -> names_prod t
388
list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in
389
assert (List.length field_names = List.length typ);
390
let projs = ref Cset.empty in
391
let mp,d,_ = repr_kn kn in
392
let rec select_fields l typs = match l,typs with
394
| (Name id)::l, typ::typs ->
395
if isDummy (expand env typ) then select_fields l typs
397
let knp = make_con mp d (label_of_id id) in
398
if not (List.exists isKill (type2signature env typ))
400
projs := Cset.add knp !projs;
401
(ConstRef knp) :: (select_fields l typs)
402
| Anonymous::l, typ::typs ->
403
if isDummy (expand env typ) then select_fields l typs
407
let field_glob = select_fields field_names typ
409
(* Is this record officially declared with its projections ? *)
410
(* If so, we use this information. *)
412
let n = nb_default_params env
413
(Inductive.type_of_inductive env (mib,mip0))
417
(fun kn -> if Cset.mem kn !projs then add_projection n kn))
418
(lookup_projections ip)
422
with (I info) -> info
424
let i = {ind_info = ind_info;
426
ind_packets = packets;
427
ind_equiv = match mib.mind_equiv with
429
| Some kn -> Equiv kn }
434
(*s [extract_type_cons] extracts the type of an inductive
435
constructor toward the corresponding list of ML types. *)
438
\item [db] is a context for translating Coq [Rel] into ML type [Tvar]
439
\item [dbmap] is a translation map (produced by a call to [parse_in_args])
440
\item [i] is the rank of the current product (initially [params_nb+1])
443
and extract_type_cons env db dbmap c i =
444
match kind_of_term (whd_betadeltaiota env none c) with
446
let env' = push_rel_assum (n,t) env in
447
let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
448
let l = extract_type_cons env' db' dbmap d (i+1) in
449
(extract_type env db 0 t []) :: l
452
(*s Recording the ML type abbreviation of a Coq type scheme constant. *)
454
and mlt_env env r = match r with
457
if not (visible_con kn) then raise Not_found;
458
match lookup_term kn with
459
| Dtype (_,vl,mlt) -> Some mlt
462
let cb = Environ.lookup_constant kn env in
463
let typ = Typeops.type_of_constant_type env cb.const_type in
464
match cb.const_body with
467
(match flag_of_type env typ with
469
let body = Declarations.force l_body in
470
let s,vl = type_sign_vl env typ in
471
let db = db_from_sign s in
472
let t = extract_type_scheme env db body (List.length s)
473
in add_term kn (Dtype (r, vl, t)); Some t
477
and expand env = type_expand (mlt_env env)
478
and type2signature env = type_to_signature (mlt_env env)
479
let type2sign env = type_to_sign (mlt_env env)
480
let type_expunge env = type_expunge (mlt_env env)
482
(*s Extraction of the type of a constant. *)
484
let record_constant_type env kn opt_typ =
486
if not (visible_con kn) then raise Not_found;
489
let typ = match opt_typ with
490
| None -> Typeops.type_of_constant env kn
492
in let mlt = extract_type env [] 1 typ []
493
in let schema = (type_maxvar mlt, mlt)
494
in add_type kn schema; schema
496
(*S Extraction of a term. *)
498
(* Precondition: [(c args)] is not a type scheme, and is informative. *)
500
(* [mle] is a ML environment [Mlenv.t]. *)
501
(* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
503
let rec extract_term env mle mlt c args =
504
match kind_of_term c with
506
extract_term env mle mlt f (Array.to_list a @ args)
507
| Lambda (n, t, d) ->
508
let id = id_of_name n in
511
(* We make as many [LetIn] as possible. *)
512
let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l))
513
in extract_term env mle mlt d' []
515
let env' = push_rel_assum (Name id, t) env in
516
let id, a = try check_default env t; id, new_meta()
517
with NotDefault d -> dummy_name, Tdummy d
519
let b = new_meta () in
520
(* If [mlt] cannot be unified with an arrow type, then magic! *)
521
let magic = needs_magic (mlt, Tarr (a, b)) in
522
let d' = extract_term env' (Mlenv.push_type mle a) b d [] in
523
put_magic_if magic (MLlam (id, d')))
524
| LetIn (n, c1, t1, c2) ->
525
let id = id_of_name n in
526
let env' = push_rel (Name id, Some c1, t1) env in
527
let args' = List.map (lift 1) args in
529
check_default env t1;
530
let a = new_meta () in
531
let c1' = extract_term env mle a c1 [] in
532
(* The type of [c1'] is generalized and stored in [mle]. *)
533
let mle' = Mlenv.push_gen mle a in
534
MLletin (id, c1', extract_term env' mle' mlt c2 args')
536
let mle' = Mlenv.push_std_type mle (Tdummy d) in
537
ast_pop (extract_term env' mle' mlt c2 args'))
539
extract_cst_app env mle mlt kn args
541
extract_cons_app env mle mlt cp args
543
(* As soon as the expected [mlt] for the head is known, *)
544
(* we unify it with an fresh copy of the stored type of [Rel n]. *)
545
let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n)
546
in extract_app env mle mlt extract_rel args
547
| Case ({ci_ind=ip},_,c0,br) ->
548
extract_app env mle mlt (extract_case env mle (ip,c0,br)) args
549
| Fix ((_,i),recd) ->
550
extract_app env mle mlt (extract_fix env mle i recd) args
552
extract_app env mle mlt (extract_fix env mle i recd) args
553
| Cast (c,_,_) -> extract_term env mle mlt c args
554
| Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false
556
(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
558
and extract_maybe_term env mle mlt c =
559
try check_default env (type_of env c);
560
extract_term env mle mlt c []
562
put_magic (mlt, Tdummy d) MLdummy
564
(*s Generic way to deal with an application. *)
566
(* We first type all arguments starting with unknown meta types.
567
This gives us the expected type of the head. Then we use the
568
[mk_head] to produce the ML head from this type. *)
570
and extract_app env mle mlt mk_head args =
571
let metas = List.map new_meta args in
572
let type_head = type_recomp (metas, mlt) in
573
let mlargs = List.map2 (extract_maybe_term env mle) metas args in
574
if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs)
576
(*s Auxiliary function used to extract arguments of constant or constructor. *)
578
and make_mlargs env e s args typs =
580
let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in
583
| a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt))
584
| _::la, _::lt -> f (la,lt)
588
(*s Extraction of a constant applied to arguments. *)
590
and extract_cst_app env mle mlt kn args =
591
(* First, the [ml_schema] of the constant, in expanded version. *)
592
let nb,t = record_constant_type env kn None in
593
let schema = nb, expand env t in
594
(* Can we instantiate types variables for this constant ? *)
595
(* In Ocaml, inside the definition of this constant, the answer is no. *)
597
if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema)
598
else instantiation schema
600
(* Then the expected type of this constant. *)
601
let a = new_meta () in
602
(* We compare stored and expected types in two steps. *)
603
(* First, can [kn] be applied to all args ? *)
604
let metas = List.map new_meta args in
605
let magic1 = needs_magic (type_recomp (metas, a), instantiated) in
606
(* Second, is the resulting type compatible with the expected type [mlt] ? *)
607
let magic2 = needs_magic (a, mlt) in
608
(* The internal head receives a magic if [magic1] *)
609
let head = put_magic_if magic1 (MLglob (ConstRef kn)) in
610
(* Now, the extraction of the arguments. *)
611
let s = type2signature env (snd schema) in
612
let ls = List.length s in
613
let la = List.length args in
614
let mla = make_mlargs env mle s args metas in
618
let l,l' = list_chop (projection_arity (ConstRef kn)) mla in
619
if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
624
(* Different situations depending of the number of arguments: *)
625
if ls = 0 then put_magic_if magic2 head
626
else if List.mem Keep s then
627
if la >= ls || not (List.exists isKill s)
629
put_magic_if (magic2 && not magic1) (MLapp (head, mla))
631
(* Not enough arguments. We complete via eta-expansion. *)
633
let s' = list_lastn ls' s in
634
let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
635
put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s')
636
else if List.mem (Kill Kother) s then
637
(* In the special case of always false signature, one dummy lam is left. *)
638
(* So a [MLdummy] is left accordingly. *)
640
then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla))
641
else put_magic_if magic2 (dummy_lams head (ls-la-1))
642
else (* s is made only of [Kill Ktype] *)
644
then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
645
else put_magic_if magic2 (dummy_lams head (ls-la))
648
(*s Extraction of an inductive constructor applied to arguments. *)
651
\item In ML, contructor arguments are uncurryfied.
652
\item We managed to suppress logical parts inside inductive definitions,
653
but they must appears outside (for partial applications for instance)
654
\item We also suppressed all Coq parameters to the inductives, since
655
they are fixed, and thus are not used for the computation.
658
and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
659
(* First, we build the type of the constructor, stored in small pieces. *)
660
let mi = extract_ind env kn in
661
let params_nb = mi.ind_nparams in
662
let oi = mi.ind_packets.(i) in
663
let nb_tvars = List.length oi.ip_vars
664
and types = List.map (expand env) oi.ip_types.(j-1) in
665
let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
666
let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
667
let type_cons = instantiation (nb_tvars, type_cons) in
668
(* Then, the usual variables [s], [ls], [la], ... *)
669
let s = List.map (type2sign env) types in
670
let ls = List.length s in
671
let la = List.length args in
672
assert (la <= ls + params_nb);
673
let la' = max 0 (la - params_nb) in
674
let args' = list_lastn la' args in
675
(* Now, we build the expected type of the constructor *)
676
let metas = List.map new_meta args' in
677
(* If stored and expected types differ, then magic! *)
678
let a = new_meta () in
679
let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
680
let magic2 = needs_magic (a, mlt) in
682
if mi.ind_info = Singleton then
683
put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
684
else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
686
(* Different situations depending of the number of arguments: *)
687
if la < params_nb then
688
let head' = head (eta_args_sign ls s) in
690
(dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
692
let mla = make_mlargs env mle s args' metas in
693
if la = ls + params_nb
694
then put_magic_if (magic2 && not magic1) (head mla)
695
else (* [ params_nb <= la <= ls + params_nb ] *)
696
let ls' = params_nb + ls - la in
697
let s' = list_lastn ls' s in
698
let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
699
put_magic_if magic2 (anonym_or_dummy_lams (head mla) s')
701
(*S Extraction of a case. *)
703
and extract_case env mle ((kn,i) as ip,c,br) mlt =
704
(* [br]: bodies of each branch (in functional form) *)
705
(* [ni]: number of arguments without parameters in each branch *)
706
let ni = mis_constr_nargs_env env ip in
707
let br_size = Array.length br in
708
assert (Array.length ni = br_size);
709
if br_size = 0 then begin
710
add_recursors env kn; (* May have passed unseen if logical ... *)
713
(* [c] has an inductive type, and is not a type scheme type. *)
714
let t = type_of env c in
715
(* The only non-informative case: [c] is of sort [Prop] *)
716
if (sort_of env t) = InProp then
718
add_recursors env kn; (* May have passed unseen if logical ... *)
719
(* Logical singleton case: *)
720
(* [match c with C i j k -> t] becomes [t'] *)
721
assert (br_size = 1);
722
let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in
723
let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in
724
let e = extract_maybe_term env mle mlt br.(0) in
725
snd (case_expunge s e)
728
let mi = extract_ind env kn in
729
let oi = mi.ind_packets.(i) in
730
let metas = Array.init (List.length oi.ip_vars) new_meta in
731
(* The extraction of the head. *)
732
let type_head = Tglob (IndRef ip, Array.to_list metas) in
733
let a = extract_term env mle type_head c [] in
734
(* The extraction of each branch. *)
735
let extract_branch i =
736
(* The types of the arguments of the corresponding constructor. *)
737
let f t = type_subst_vect metas (expand env t) in
738
let l = List.map f oi.ip_types.(i) in
739
(* the corresponding signature *)
740
let s = List.map (type2sign env) oi.ip_types.(i) in
741
(* Extraction of the branch (in functional form). *)
742
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
743
(* We suppress dummy arguments according to signature. *)
744
let ids,e = case_expunge s e in
745
(ConstructRef (ip,i+1), List.rev ids, e)
747
if mi.ind_info = Singleton then
749
(* Informative singleton case: *)
750
(* [match c with C i -> t] becomes [let i = c' in t'] *)
751
assert (br_size = 1);
752
let (_,ids,e') = extract_branch 0 in
753
assert (List.length ids = 1);
754
MLletin (List.hd ids,a,e')
757
(* Standard case: we apply [extract_branch]. *)
758
MLcase ((mi.ind_info,[]), a, Array.init br_size extract_branch)
760
(*s Extraction of a (co)-fixpoint. *)
762
and extract_fix env mle i (fi,ti,ci as recd) mlt =
763
let env = push_rec_types recd env in
764
let metas = Array.map new_meta fi in
766
let mle = Array.fold_left Mlenv.push_type mle metas in
767
let ei = array_map2 (extract_maybe_term env mle) metas ci in
768
MLfix (i, Array.map id_of_name fi, ei)
770
(*S ML declarations. *)
772
(* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
773
and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
775
let rec decomp_lams_eta_n n env c t =
776
let rels = fst (decomp_n_prod env none n t) in
777
let rels = List.map (fun (id,_,c) -> (id,c)) rels in
779
if m >= n then decompose_lam_n n c
781
let rels',c = decompose_lam c in
783
(* we'd better keep rels' as long as possible. *)
784
let rels = (list_firstn d rels) @ rels' in
785
let eta_args = List.rev_map mkRel (interval 1 d) in
786
rels, applist (lift d c,eta_args)
788
(*s From a constant to a ML declaration. *)
790
let extract_std_constant env kn body typ =
792
(* The short type [t] (i.e. possibly with abbreviations). *)
793
let t = snd (record_constant_type env kn (Some typ)) in
794
(* The real type [t']: without head lambdas, expanded, *)
795
(* and with [Tvar] translated to [Tvar'] (not instantiable). *)
796
let l,t' = type_decomp (expand env (var2var' t)) in
797
let s = List.map (type2sign env) l in
798
(* The initial ML environment. *)
799
let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
800
(* Decomposing the top level lambdas of [body]. *)
801
let rels,c = decomp_lams_eta_n (List.length s) env body typ in
802
(* The lambdas names. *)
803
let ids = List.map (fun (n,_) -> id_of_name n) rels in
804
(* The according Coq environment. *)
805
let env = push_rels_assum rels env in
806
(* The real extraction: *)
807
let e = extract_term env mle t' c [] in
808
(* Expunging term and type from dummy lambdas. *)
809
term_expunge s (ids,e), type_expunge env t
811
let extract_fixpoint env vkn (fi,ti,ci) =
812
let n = Array.length vkn in
813
let types = Array.make n (Tdummy Kother)
814
and terms = Array.make n MLdummy in
815
let kns = Array.to_list vkn in
816
current_fixpoints := kns;
817
(* for replacing recursive calls [Rel ..] by the corresponding [Const]: *)
818
let sub = List.rev_map mkConst kns in
820
if sort_of env ti.(i) <> InProp then begin
821
let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in
826
current_fixpoints := [];
827
Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types)
829
let extract_constant env kn cb =
830
let r = ConstRef kn in
831
let typ = Typeops.type_of_constant_type env cb.const_type in
832
match cb.const_body with
833
| None -> (* A logical axiom is risky, an informative one is fatal. *)
834
(match flag_of_type env typ with
835
| (Info,TypeScheme) ->
836
if not (is_custom r) then add_info_axiom r;
837
let n = type_scheme_nb_args env typ in
838
let ids = iterate (fun l -> anonymous::l) n [] in
839
Dtype (r, ids, Taxiom)
841
if not (is_custom r) then add_info_axiom r;
842
let t = snd (record_constant_type env kn (Some typ)) in
843
Dterm (r, MLaxiom, type_expunge env t)
844
| (Logic,TypeScheme) ->
845
add_log_axiom r; Dtype (r, [], Tdummy Ktype)
847
add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother))
849
(match flag_of_type env typ with
850
| (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother)
851
| (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype)
853
let e,t = extract_std_constant env kn (force body) typ in
855
| (Info, TypeScheme) ->
856
let s,vl = type_sign_vl env typ in
857
let db = db_from_sign s in
858
let t = extract_type_scheme env db (force body) (List.length s)
861
let extract_constant_spec env kn cb =
862
let r = ConstRef kn in
863
let typ = Typeops.type_of_constant_type env cb.const_type in
864
match flag_of_type env typ with
865
| (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype))
866
| (Logic, Default) -> Sval (r, Tdummy Kother)
867
| (Info, TypeScheme) ->
868
let s,vl = type_sign_vl env typ in
869
(match cb.const_body with
870
| None -> Stype (r, vl, None)
872
let db = db_from_sign s in
873
let t = extract_type_scheme env db (force body) (List.length s)
874
in Stype (r, vl, Some t))
876
let t = snd (record_constant_type env kn (Some typ)) in
877
Sval (r, type_expunge env t)
879
let extract_with_type env cb =
880
let typ = Typeops.type_of_constant_type env cb.const_type in
881
match flag_of_type env typ with
882
| (Info, TypeScheme) ->
883
let s,vl = type_sign_vl env typ in
884
let body = Option.get cb.const_body in
885
let db = db_from_sign s in
886
let t = extract_type_scheme env db (force body) (List.length s) in
891
let extract_inductive env kn =
892
let ind = extract_ind env kn in
893
add_recursors env kn;
894
let f l = List.filter (fun t -> not (isDummy (expand env t))) l in
896
Array.map (fun p -> { p with ip_types = Array.map f p.ip_types })
898
in { ind with ind_packets = packets }
900
(*s Is a [ml_decl] logical ? *)
902
let logical_decl = function
903
| Dterm (_,MLdummy,Tdummy _) -> true
904
| Dtype (_,[],Tdummy _) -> true
906
(array_for_all ((=) MLdummy) av) &&
907
(array_for_all isDummy tv)
908
| Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
911
(*s Is a [ml_spec] logical ? *)
913
let logical_spec = function
914
| Stype (_, [], Some (Tdummy _)) -> true
915
| Sval (_,Tdummy _) -> true
916
| Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
added
removed
contrib/extraction/extraction.ml
