1 (************************************************************************)
2 (* v * The Coq Proof Assistant / The Coq Development Team *)
3 (* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
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 14786 2011-12-10 12:55:19Z letouzey $ i*)
13 open OcamlExtractionTable
17 (* A set of all fixpoint functions currently being extracted *)
18 (*CSC: very imperative, fix/check?*)
19 let current_fixpoints = ref (None : NUri.uri option)
21 let whd_betadeltaiota status context t =
22 NCicReduction.whd status ~subst:[] context t
24 let whd_betaiotazeta status context t =
25 NCicReduction.whd status ~delta:max_int ~subst:[] context t
27 let isRel = function NCic.Rel _ -> true | _ -> false
29 let rec split_all_prods status ~subst context te =
30 match NCicReduction.whd status ~subst context te with
31 | NCic.Prod (name,so,ta) ->
32 split_all_prods status ~subst ((name,(NCic.Decl so))::context) ta
36 (* (nb_lam [na1:T1]...[nan:Tan]c) where c is not an abstraction
41 | NCic.Lambda (_,_,c) -> nbrec (n+1) c
46 (* Given a positive integer n, transforms a lambda term [x1:T1]..[xn:Tn]T
47 into the pair ([(xn,Tn);...;(x1,T1)],T) *)
48 let decompose_lam_n n =
49 if n < 0 then assert false else
50 let rec lamdec_rec l n c =
53 | NCic.Lambda (x,t,c) -> lamdec_rec ((x,NCic.Decl t)::l) (n-1) c
59 let rec lamdec_rec l =
61 | NCic.Lambda (x,t,c) -> lamdec_rec ((x,t)::l) c
66 let splay_prod_n status context n =
67 let rec decrec context m ln c = if m = 0 then (ln,c) else
68 match whd_betadeltaiota status context c with
69 | NCic.Prod (n,a,c0) ->
70 decrec ((n,NCic.Decl a)::context)
71 (m-1) ((n,NCic.Decl a)::ln) c0
72 | _ -> invalid_arg "splay_prod_n"
76 let splay_prod status context =
77 let rec decrec context m c =
78 let t = whd_betadeltaiota status context c in
80 | NCic.Prod (n,a,c0) ->
81 decrec ((n,NCic.Decl a)::context) ((n,NCic.Decl a)::m) c0
86 let type_of status context t =
87 NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context t
89 type sorts_family = InProp | InType
95 match NCicEnvironment.family_of u with
99 let sort_of status context t =
101 NCicTypeChecker.typeof status ~subst:[] ~metasenv:[] context t
103 NCic.Sort s -> classify_sort s
106 (*S Generation of flags and signatures. *)
108 (* The type [flag] gives us information about any Coq term:
110 \item [TypeScheme] denotes a type scheme, that is
111 something that will become a type after enough applications.
112 More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
113 [s = Set], [Prop] or [Type]
114 \item [Default] denotes the other cases. It may be inexact after
115 instanciation. For example [(X:Type)X] is [Default] and may give [Set]
116 after instanciation, which is rather [TypeScheme]
117 \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
118 \item [Info] is the opposite. The same example [(X:Type)X] shows
119 that an [Info] term might in fact be [Logic] later on.
122 type info = Logic | Info
124 type scheme = TypeScheme | Default
126 type flag = info * scheme
128 (*s [flag_of_type] transforms a type [t] into a [flag].
129 Really important function. *)
131 let rec flag_of_type status context t =
132 let t = whd_betadeltaiota status context t in
134 | NCic.Prod (x,t,c) -> flag_of_type status ((x,NCic.Decl t)::context) c
136 (match classify_sort s with
137 InProp -> (Logic,TypeScheme)
138 | InType -> (Info,TypeScheme))
140 if (sort_of status context t) = InProp then (Logic,Default)
143 (*s Two particular cases of [flag_of_type]. *)
145 let is_default status context t=(flag_of_type status context t= (Info, Default))
147 exception NotDefault of kill_reason
149 let check_default status context t =
150 match flag_of_type status context t with
151 | _,TypeScheme -> raise (NotDefault Ktype)
152 | Logic,_ -> raise (NotDefault Kother)
155 let is_info_scheme status context t =
156 (flag_of_type status context t = (Info, TypeScheme))
158 (*s [type_sign] generates a signature aimed at treating a type application. *)
160 let rec type_sign status context c =
161 match whd_betadeltaiota status context c with
162 | NCic.Prod (n,t,d) ->
163 (if is_info_scheme status context t then Keep else Kill Kother)
164 :: (type_sign status ((n,NCic.Decl t)::context) d)
167 let rec type_scheme_nb_args status context c =
168 match whd_betadeltaiota status context c with
169 | NCic.Prod (n,t,d) ->
170 let n = type_scheme_nb_args status ((n,NCic.Decl t)::context) d in
171 if is_info_scheme status context t then n+1 else n
174 (*CSC: only useful for inline extraction
175 let _ = register_type_scheme_nb_args type_scheme_nb_args
178 (*s [type_sign_vl] does the same, plus a type var list. *)
180 let rec type_sign_vl status context c =
181 match whd_betadeltaiota status context c with
182 | NCic.Prod (n,t,d) ->
183 let s,vl = type_sign_vl status ((n,NCic.Decl t)::context) d in
184 if not (is_info_scheme status context t) then Kill Kother::s, vl
185 else Keep::s, (next_ident_away (id_of_name n) vl) :: vl
188 let rec nb_default_params status context c =
189 match whd_betadeltaiota status context c with
190 | NCic.Prod (n,t,d) ->
191 let n = nb_default_params status ((n,NCic.Decl t)::context) d in
192 if is_default status context t then n+1 else n
195 (* Enriching a signature with implicit information *)
197 let sign_with_implicits _r s =
198 let implicits = [](*CSC: implicits_of_global r*) in
199 let rec add_impl i = function
203 if sign = Keep && List.mem i implicits then Kill Kother else sign
204 in sign' :: add_impl (succ i) s
208 (* Enriching a exception message *)
210 let rec handle_exn _r _n _fn_name = function x -> x
211 (*CSC: only for pretty printing
213 (try Scanf.sscanf s "UNBOUND %d"
215 assert ((0 < i) && (i <= n));
216 MLexn ("IMPLICIT "^ msg_non_implicit r (n+1-i) (fn_name i)))
218 | a -> ast_map (handle_exn r n fn_name) a*)
220 (*S Management of type variable contexts. *)
222 (* A De Bruijn variable context (db) is a context for translating Coq [Rel]
223 into ML type [Tvar]. *)
225 (*s From a type signature toward a type variable context (db). *)
228 let rec make i acc = function
230 | Keep :: l -> make (i+1) (i::acc) l
231 | Kill _ :: l -> make i (0::acc) l
234 (*s Create a type variable context from indications taken from
235 an inductive type (see just below). *)
237 let rec db_from_ind dbmap i =
239 else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1))
241 (*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument
242 of a constructor corresponds to the j-th type var of the ML inductive. *)
245 \item [si] : signature of the inductive
246 \item [i] : counter of Coq args for [(I args)]
247 \item [j] : counter of ML type vars
248 \item [relmax] : total args number of the constructor
251 let parse_ind_args si args relmax =
252 let rec parse i j = function
254 | Kill _ :: s -> parse (i+1) j s
256 (match args.(i-1) with
257 | NCic.Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s)
258 | _ -> parse (i+1) (j+1) s)
261 (*S Extraction of a type. *)
263 (* [extract_type env db c args] is used to produce an ML type from the
264 coq term [(c args)], which is supposed to be a Coq type. *)
266 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
268 (* [j] stands for the next ML type var. [j=0] means we do not
269 generate ML type var anymore (in subterms for example). *)
272 let rec extract_type status context db j c args =
273 match whd_betaiotazeta status context c with
274 | NCic.Appl (d::args') ->
275 (* We just accumulate the arguments. *)
276 extract_type status context db j d (args' @ args)
277 | NCic.Lambda (_,_,d) ->
279 | [] -> assert false (* otherwise the lambda would be reductible. *)
280 | a :: args -> extract_type status context db j (NCicSubstitution.subst status a d) args)
281 | NCic.Prod (n,t,d) ->
283 let context' = (n,NCic.Decl t)::context in
284 (match flag_of_type status context t with
286 (* Standard case: two [extract_type] ... *)
287 let status,mld = extract_type status context' (0::db) j d [] in
288 let status,res = expand status mld in
290 | Tdummy d -> status,Tdummy d
292 let status,res=extract_type status context db 0 t [] in
293 status,Tarr (res, mld))
294 | (Info, TypeScheme) when j > 0 ->
295 (* A new type var. *)
296 let status,mld=extract_type status context' (j::db) (j+1) d [] in
297 let status,res = expand status mld in
300 | Tdummy d -> Tdummy d
301 | _ -> Tarr (Tdummy Ktype, mld))
303 let status,mld = extract_type status context' (0::db) j d [] in
304 let status,res = expand status mld in
307 | Tdummy d -> Tdummy d
309 let reason = if lvl=TypeScheme then Ktype else Kother in
310 Tarr (Tdummy reason, mld)))
311 | NCic.Sort _ -> status,Tdummy Ktype (* The two logical cases. *)
312 | _ when sort_of status context (NCicUntrusted.mk_appl c args) = InProp ->
315 (match List.nth context (n-1) with
316 | (_,NCic.Def (t,_)) -> extract_type status context db j (NCicSubstitution.lift status n t) args
318 (* Asks [db] a translation for [n]. *)
319 if n > List.length db then status,Tunknown
320 else let n' = List.nth db (n-1) in
321 status,if n' = 0 then Tunknown else Tvar n')
322 | NCic.Const (NReference.Ref (uri,spec) as r) ->
325 let _,_,typ,_,_ = NCicEnvironment.get_checked_decl status r in
326 (match flag_of_type status [] typ with
327 | (Info, TypeScheme) ->
328 extract_type_app status context db
329 (r, type_sign status [] typ) args
330 | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
331 status,Tunknown (* Brutal approximation ... *))
332 | NReference.Def _ ->
333 let _,_,bo,typ,_,_ = NCicEnvironment.get_checked_def status r in
334 (match flag_of_type status [] typ with
335 | (Info, TypeScheme) ->
337 extract_type_app status context db
338 (r, type_sign status [] typ) args in
339 (*CSC: if is_custom r then mlt else*)
340 let newc = NCicUntrusted.mk_appl bo args in
341 let status,mlt' = extract_type status context db j newc [] in
342 (* ML type abbreviations interact badly with Coq *)
343 (* reduction, so [mlt] and [mlt'] might be different: *)
344 (* The more precise is [mlt'], extracted after reduction *)
345 (* The shortest is [mlt], which use abbreviations *)
346 (* If possible, we take [mlt], otherwise [mlt']. *)
347 let status,res1 = expand status mlt in
348 let status,res2 = expand status mlt' in
349 if res1=res2 then status,mlt else status,mlt'
350 | _ -> (* only other case here: Info, Default, i.e. not an ML type *)
351 (* We try to reduce. *)
352 let newc = NCicUntrusted.mk_appl bo args in
353 extract_type status context db j newc [])
354 | NReference.Fix _ -> status,Tunknown
356 | NReference.CoFix _ -> assert false
357 | NReference.Ind (_,i,_) ->
358 let status,ind = extract_ind status uri in
359 let s = ind.ind_packets.(i).ip_sign in
360 extract_type_app status context db (r,s) args)
361 | NCic.Match _ -> status,Tunknown
364 (*s Auxiliary function dealing with type application.
365 Precondition: [r] is a type scheme represented by the signature [s],
366 and is completely applied: [List.length args = List.length s]. *)
368 and extract_type_app status context db (r,s) args =
371 (fun (b,c) (status,a) ->
375 (fst (splay_prod status context (type_of status context c))) in
376 let db = iterate (fun l -> 0 :: l) p db in
377 let status,res = extract_type_scheme status context db c p in
380 (List.combine s args) (status,[])
381 in status, Tglob (r, ml_args)
383 (*S Extraction of a type scheme. *)
385 (* [extract_type_scheme env db c p] works on a Coq term [c] which is
386 an informative type scheme. It means that [c] is not a Coq type, but will
387 be when applied to sufficiently many arguments ([p] in fact).
388 This function decomposes p lambdas, with eta-expansion if needed. *)
390 (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *)
392 and extract_type_scheme status context db c p =
393 if p=0 then extract_type status context db 0 c []
395 let c = whd_betaiotazeta status context c in
397 | NCic.Lambda (n,t,d) ->
398 extract_type_scheme status((n,NCic.Decl t)::context) db d (p-1)
400 let rels=fst (splay_prod status context (type_of status context c)) in
401 let context = rels@context in
402 let eta_args = List.rev_map (fun x -> NCic.Rel x) (interval 1 p) in
403 extract_type status context db 0 (NCicSubstitution.lift status p c)
407 (*S Extraction of an inductive type. *)
409 and extract_ind status uri =
411 status,lookup_ind status uri
413 let _,_,_,_,obj = NCicEnvironment.get_checked_obj status uri in
415 NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
416 extract_ind0 status uri inductive ind_pragma leftno types
419 and extract_ind0 status uri inductive ind_pragma leftno types =
420 (* First, if this inductive is aliased via a Module, *)
421 (* we process the original inductive. *)
422 (* Everything concerning parameters. *)
423 (* We do that first, since they are common to all the [mib]. *)
424 let _,_,mipty0,_ = List.hd types in
425 let mipcontext,_=NCicReduction.split_prods status ~subst:[] [] ~-1 mipty0 in
426 let epar_rev,_= HExtlib.split_nth leftno (List.rev mipcontext) in
427 let epar = List.rev epar_rev in
428 (* First pass: we store inductive signatures together with *)
429 (* their type var list. *)
432 (fun tyno (_,name,arity,kl) ->
433 let _,sort=NCicReduction.split_prods status ~subst:[] [] ~-1 arity in
434 let sort=match sort with NCic.Sort sort -> sort | _ ->assert false in
435 let b = classify_sort sort <> InProp in
436 let s,v = if b then type_sign_vl status [] arity else [],[] in
437 let t = Array.make (List.length kl) [] in
438 let kl = Array.of_list kl in
439 let spec = NReference.Ind (inductive,tyno,leftno) in
440 let ref = NReference.reference_of_spec uri spec in
441 { ip_reference = ref;
445 NReference.reference_of_spec uri
446 (NReference.Con (tyno,i+1,leftno))
449 ip_consnames= Array.map (fun (_,name,_) -> name) kl;
450 ip_logical = (not b);
455 (Array.of_list types)
457 let status = add_ind ~dummy:true status uri
458 {ind_kind = Standard;
459 ind_nparams = leftno;
460 ind_packets = packets
462 (* Second pass: we extract constructors *)
463 let rec aux1 i status =
464 if i = List.length types then status
466 let p = packets.(i) in
467 let _,_,_,cl = List.nth types i in
468 if not p.ip_logical then
469 let ktypes = Array.of_list (List.map (fun (_,_,arity) -> arity) cl) in
470 let rec aux2 j status =
471 if j = Array.length ktypes then status
474 NCicReduction.split_prods status ~subst:[] [] leftno ktypes.(j) in
475 let prods,head = split_all_prods status ~subst:[] tctx t in
476 let nprods = List.length prods in
477 let args = match head with
478 | NCic.Appl (_f::args) -> Array.of_list args (* [f = Ind ip] *)
481 let dbmap = parse_ind_args p.ip_sign args nprods in
482 let db = db_from_ind dbmap leftno in
483 let status,res = extract_type_cons status epar db dbmap t (leftno+1)in
484 p.ip_types.(j) <- res;
488 let status = aux2 0 status in
494 let status = aux1 0 status in
495 (* Third pass: we determine special cases. *)
496 let status,ind_info =
497 (*CSC: let ip = (kn, 0) in
499 if is_custom r then raise_I status Standard;*)
500 if not inductive then status,Coinductive else
501 if List.length types <> 1 then status,Standard else
502 let p = packets.(0) in
503 if p.ip_logical then status,Standard else
504 if Array.length p.ip_types <> 1 then status,Standard else
505 let typ = p.ip_types.(0) in
508 (fun x (status,res) ->
509 let status,y = expand status x in
512 let l = List.filter (fun t -> not (isDummy t)) l in
513 if List.length l = 1 && not (type_mem_kn uri (List.hd l))
514 then status,Singleton else
515 if l = [] then status,Standard else
516 (match ind_pragma with
517 `Regular -> status,Standard
519 let baseuri = NUri.baseuri_of_uri uri in
520 let field_names = List.map (fun (n,_,_) -> n) fields in
521 assert (List.length field_names = List.length typ);
522 let rec select_fields status l typs = match l,typs with
524 | id::l, typ::typs ->
525 let status,res = expand status typ in
527 select_fields status l typs
529 (* Is it safe to use [id] for projections [foo.id] ? *)
530 let status,res = type2signature status typ in
532 NUri.uri_of_string (baseuri ^ "/" ^ id ^ ".con") in
534 NReference.reference_of_spec fielduri fake_spec in
539 let (_,height,_,_,obj) =
540 NCicEnvironment.get_checked_obj status fielduri
543 NCic.Fixpoint (_,fs,(_,_,`Projection)) ->
544 let _,_,recparamno,_,_ = List.nth fs 0 in
545 NReference.Fix (0,recparamno,height)
548 NReference.reference_of_spec fielduri fieldspec
549 with NCicEnvironment.ObjectNotFound _ ->
553 if List.for_all ((=) Keep) res
555 let n = nb_default_params status [] mipty0 in
556 guess_projection status fielduri n
558 let status,res = select_fields status l typs in
559 status, fieldfakeref::res
562 let status,field_glob = select_fields status field_names typ in
563 (* Is this record officially declared with its projections ? *)
564 (* If so, we use this information. *)
565 status, Record field_glob)
567 let i = {ind_kind = ind_info;
568 ind_nparams = leftno;
569 ind_packets = packets
571 let status = add_ind status uri i in
574 (*s [extract_type_cons] extracts the type of an inductive
575 constructor toward the corresponding list of ML types.
577 - [db] is a context for translating Coq [Rel] into ML type [Tvar]
578 - [dbmap] is a translation map (produced by a call to [parse_in_args])
579 - [i] is the rank of the current product (initially [params_nb+1])
582 and extract_type_cons status context db dbmap c i =
583 match whd_betadeltaiota status context c with
584 | NCic.Prod (n,t,d) ->
585 let context' = (n,NCic.Decl t)::context in
586 let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in
587 let status,l = extract_type_cons status context' db' dbmap d (i+1) in
588 let status, res = extract_type status context db 0 t [] in
592 (*s Recording the ML type abbreviation of a Coq type scheme constant. *)
594 and mlt_env status r =
596 if false (*CSC:XXX not (visible_con kn)*) then raise Not_found;
597 match lookup_term status r with
598 | Dtype (_,_vl,mlt) -> Some (status,mlt)
602 NReference.Ref (_,NReference.Def _) ->
603 let _,_,body,typ,_,_ = NCicEnvironment.get_checked_def status r in
604 (match flag_of_type status [] typ with
606 let s,vl = type_sign_vl status [] typ in
607 let db = db_from_sign s in
609 extract_type_scheme status [] db body (List.length s) in
610 let status = add_term status r (Dtype (r, vl, t)) in
613 | NReference.Ref (_,NReference.Decl) -> None
614 | NReference.Ref (_,NReference.Fix _)
615 | NReference.Ref (_,NReference.CoFix _) -> assert false
616 | NReference.Ref (_,NReference.Ind _)
617 | NReference.Ref (_,NReference.Con _) -> None
619 and expand status = type_expand status mlt_env
620 and type2signature status = type_to_signature status mlt_env
621 let type2sign status = type_to_sign status mlt_env
622 let type_expunge status = type_expunge status mlt_env
623 let type_expunge_from_sign status = type_expunge_from_sign status mlt_env
625 (*s Extraction of the type of a constant. *)
627 let type_of_constant status (NReference.Ref (uri,spec)) =
628 let (_,_,_,_,obj) = NCicEnvironment.get_checked_obj status uri in
630 NCic.Constant (_,_,_,typ,_),_ -> typ
631 | NCic.Fixpoint (_,fs,_), (NReference.Fix (n,_,_) | NReference.CoFix n) ->
632 let _,_,_,typ,_ = List.nth fs n in
636 let record_constant_type status r opt_typ =
638 (*CSC:XXX to be implemented? if not (visible_con kn) then raise Not_found;*)
639 status,lookup_type status r
641 let typ = match opt_typ with
642 | None -> type_of_constant status r
644 let status,mlt = extract_type status [] [] 1 typ [] in
645 let schema = (type_maxvar mlt, mlt) in
646 let status = add_type status r schema in
649 (*S Extraction of a term. *)
651 (* Precondition: [(c args)] is not a type scheme, and is informative. *)
653 (* [mle] is a ML environment [Mlenv.t]. *)
654 (* [mlt] is the ML type we want our extraction of [(c args)] to have. *)
656 let rec extract_term status context mle mlt c args =
658 NCic.Appl [] -> assert false
659 | NCic.Appl (f::a) ->
660 extract_term status context mle mlt f (a@args)
661 | NCic.Lambda (n, t, d) ->
665 (* We make as many [LetIn] as possible. *)
666 let d' = NCic.LetIn (id,t,a,NCic.Appl (d::(List.map (NCicSubstitution.lift status 1) l)))
667 in extract_term status context mle mlt d' []
669 let context' = (id, NCic.Decl t)::context in
671 try check_default status context t; Id id, new_meta()
672 with NotDefault d -> Dummy, Tdummy d
674 let b = new_meta () in
675 (* If [mlt] cannot be unified with an arrow type, then magic! *)
676 let magic = needs_magic (mlt, Tarr (a, b)) in
678 extract_term status context' (Mlenv.push_type mle a) b d [] in
679 status,put_magic_if magic (MLlam (id, d')))
680 | NCic.LetIn (n, t1, c1, c2) ->
682 let context' = (id, NCic.Def (c1, t1))::context in
683 let args' = List.map (NCicSubstitution.lift status 1) args in
685 check_default status context t1;
686 let a = new_meta () in
687 let status,c1' = extract_term status context mle a c1 [] in
688 (* The type of [c1'] is generalized and stored in [mle]. *)
691 then Mlenv.push_gen mle a
692 else Mlenv.push_type mle a
694 let status,res = extract_term status context' mle' mlt c2 args' in
695 status,MLletin (Id id, c1', res)
697 let mle' = Mlenv.push_std_type mle (Tdummy d) in
698 let status,res = extract_term status context' mle' mlt c2 args' in
700 | NCic.Const ((NReference.Ref (uri,
704 | NReference.CoFix _ ))) as ref) ->
705 extract_cst_app status context mle mlt uri ref args
706 | NCic.Const ((NReference.Ref (_,(NReference.Con _))) as ref) ->
707 extract_cons_app status context mle mlt ref args
709 (* As soon as the expected [mlt] for the head is known, *)
710 (* we unify it with an fresh copy of the stored type of [Rel n]. *)
711 let extract_rel status mlt =
712 status,put_magic (mlt, Mlenv.get mle n) (MLrel n)
713 in extract_app status context mle mlt extract_rel args
714 | NCic.Match (ref,_,c0,br) ->
715 extract_app status context mle mlt
716 (extract_case context mle (ref,c0,Array.of_list br)) args
717 | NCic.Const (NReference.Ref (_,NReference.Ind _))
721 | NCic.Meta _ -> assert false
723 (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *)
725 and extract_maybe_term status context mle mlt c =
726 try check_default status context (type_of status context c);
727 extract_term status context mle mlt c []
729 status,put_magic (mlt, Tdummy d) MLdummy
731 (*s Generic way to deal with an application. *)
733 (* We first type all arguments starting with unknown meta types.
734 This gives us the expected type of the head. Then we use the
735 [mk_head] to produce the ML head from this type. *)
737 and extract_app status context mle mlt mk_head args =
738 let metas = List.map new_meta args in
739 let type_head = type_recomp (metas, mlt) in
742 (fun x y (status,res) ->
743 let status,z = extract_maybe_term status context mle x y in
745 ) metas args (status,[]) in
746 let status,res = mk_head status type_head in
747 status,mlapp res mlargs
749 (*s Auxiliary function used to extract arguments of constant or constructor. *)
751 and make_mlargs status context e s args typs =
752 let rec f status = function
753 | [], [], _ -> status,[]
754 | a::la, t::lt, [] ->
755 let status,res = extract_maybe_term status context e t a in
756 let status,res2 = f status (la,lt,[]) in
758 | a::la, t::lt, Keep::s ->
759 let status,res = extract_maybe_term status context e t a in
760 let status,res2 = f status (la,lt,s) in
762 | _::la, _::lt, _::s -> f status (la,lt,s)
764 in f status (args,typs,s)
766 (*s Extraction of a constant applied to arguments. *)
768 and extract_cst_app status context mle mlt uri ref args =
769 (* First, the [ml_schema] of the constant, in expanded version. *)
770 let status,(nb,t) = record_constant_type status ref None in
771 let status,res = expand status t in
772 let schema = nb, res in
773 (* Can we instantiate types variables for this constant ? *)
774 (* In Ocaml, inside the definition of this constant, the answer is no. *)
777 match !current_fixpoints with None -> false | Some uri' -> NUri.eq uri uri'
778 then var2var' (snd schema)
779 else instantiation schema
781 (* Then the expected type of this constant. *)
782 let a = new_meta () in
783 (* We compare stored and expected types in two steps. *)
784 (* First, can [kn] be applied to all args ? *)
785 let metas = List.map new_meta args in
786 let magic1 = needs_magic (type_recomp (metas, a), instantiated) in
787 (* Second, is the resulting type compatible with the expected type [mlt] ? *)
788 let magic2 = needs_magic (a, mlt) in
789 (* The internal head receives a magic if [magic1] *)
790 let head = put_magic_if magic1 (MLglob ref) in
791 (* Now, the extraction of the arguments. *)
792 let status,s_full = type2signature status (snd schema) in
793 let s_full = sign_with_implicits ref s_full in
794 let s = sign_no_final_keeps s_full in
795 let ls = List.length s in
796 let la = List.length args in
797 (* The ml arguments, already expunged from known logical ones *)
798 let status,mla = make_mlargs status context mle s args metas in
802 let l,l' = list_chop (projection_arity status ref) mla in
803 if l' <> [] then (List.map (fun _ -> MLexn "Proj Args") l) @ l'
808 (* For strict languages, purely logical signatures with at least
809 one [Kill Kother] lead to a dummy lam. So a [MLdummy] is left
811 let optdummy = match sign_kind s_full with
812 | UnsafeLogicalSig -> [MLdummy]
815 (* Different situations depending of the number of arguments: *)
818 (* Enough args, cleanup already done in [mla], we only add the
819 additionnal dummy if needed. *)
820 status,put_magic_if (magic2 && not magic1) (mlapp head (optdummy @ mla))
822 (* Partially applied function with some logical arg missing.
823 We complete via eta and expunge logical args. *)
825 let s' = list_skipn la s in
826 let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
827 let e = anonym_or_dummy_lams (mlapp head mla) s' in
828 status,put_magic_if magic2 (remove_n_lams (List.length optdummy) e)
830 (*s Extraction of an inductive constructor applied to arguments. *)
833 \item In ML, contructor arguments are uncurryfied.
834 \item We managed to suppress logical parts inside inductive definitions,
835 but they must appears outside (for partial applications for instance)
836 \item We also suppressed all Coq parameters to the inductives, since
837 they are fixed, and thus are not used for the computation.
840 and extract_cons_app status context mle mlt ref (*(((kn,i) as ip,j) as cp)*) args =
843 NReference.Ref (uri,NReference.Con(i,j,_)) -> uri,i,j
844 | _ -> assert false in
845 let b,_,_,_,_ = NCicEnvironment.get_checked_indtys status ref in
846 let tyref = NReference.mk_indty b ref in
847 (* First, we build the type of the constructor, stored in small pieces. *)
848 let status,mi = extract_ind status uri in
849 let params_nb = mi.ind_nparams in
850 let oi = mi.ind_packets.(i) in
851 let nb_tvars = List.length oi.ip_vars in
854 (fun x (status,res) ->
855 let status,y = expand status x in
857 ) oi.ip_types.(j-1) (status,[]) in
858 let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in
859 let type_cons = type_recomp (types, Tglob (tyref, list_tvar)) in
860 let type_cons = instantiation (nb_tvars, type_cons) in
861 (* Then, the usual variables [s], [ls], [la], ... *)
864 (fun x (status,res) ->
865 let status,y = type2sign status x in
868 let s = sign_with_implicits ref s in
869 let ls = List.length s in
870 let la = List.length args in
871 assert (la <= ls + params_nb);
872 let la' = max 0 (la - params_nb) in
873 let args' = list_lastn la' args in
874 (* Now, we build the expected type of the constructor *)
875 let metas = List.map new_meta args' in
876 (* If stored and expected types differ, then magic! *)
877 let a = new_meta () in
878 let magic1 = needs_magic (type_cons, type_recomp (metas, a)) in
879 let magic2 = needs_magic (a, mlt) in
880 let head status mla =
881 if mi.ind_kind = Singleton then
882 status, put_magic_if magic1 (List.hd mla)
884 let status,typeargs = match snd (type_decomp type_cons) with
887 (fun x (status,res) ->
888 let status,y = type_simpl status x in
893 let info = {c_kind = mi.ind_kind; c_typs = typeargs} in
894 status, put_magic_if magic1 (MLcons (info, ref, mla))
896 (* Different situations depending of the number of arguments: *)
897 if la < params_nb then
898 let status,head' = head status (eta_args_sign ls s) in
901 (dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la))
903 let status,mla = make_mlargs status context mle s args' metas in
904 if la = ls + params_nb
906 let status,res = head status mla in
907 status,put_magic_if (magic2 && not magic1) res
908 else (* [ params_nb <= la <= ls + params_nb ] *)
909 let ls' = params_nb + ls - la in
910 let s' = list_lastn ls' s in
911 let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in
912 let status,res = head status mla in
913 status,put_magic_if magic2 (anonym_or_dummy_lams res s')
915 (*S Extraction of a case. *)
917 and extract_case context mle (ip,c,br) status mlt =
918 (* [br]: bodies of each branch (in functional form) *)
919 (* [ni]: number of arguments without parameters in each branch *)
922 NReference.Ref (uri,NReference.Ind (_,i,_)) -> uri,i
925 let br_size = Array.length br in
926 if br_size = 0 then begin
927 (*CSC: to be implemented only if we allow inlining of recursors add_recursors env kn; (* May have passed unseen if logical ... *)*)
928 status,MLexn "absurd case"
930 (* [c] has an inductive type, and is not a type scheme type. *)
931 let t = type_of status context c in
932 (* The only non-informative case: [c] is of sort [Prop] *)
933 if (sort_of status context t) = InProp then
935 (*CSC: to be implemented only if we allow inlining of recursors add_recursors env kn; (* May have passed unseen if logical ... *)*)
936 (* Logical singleton case: *)
937 (* [match c with C i j k -> t] becomes [t'] *)
938 assert (br_size = 1);
940 let _,leftno,tys,_,_ = NCicEnvironment.get_checked_indtys status ip in
941 let _,_,_,cl = List.hd tys in
942 let _,_,cty = List.hd cl in
943 let prods,_ = split_all_prods status ~subst:[] [] cty in
944 List.length prods - leftno
946 let s = iterate (fun l -> Kill Kother :: l) ni [] in
947 let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni mlt in
948 let status,e = extract_maybe_term status context mle mlt br.(0) in
949 status, snd (case_expunge s e)
952 let status,mi = extract_ind status uri in
953 let oi = mi.ind_packets.(i) in
954 let metas = Array.init (List.length oi.ip_vars) new_meta in
955 (* The extraction of the head. *)
956 let type_head = Tglob (ip, Array.to_list metas) in
957 let status,a = extract_term status context mle type_head c [] in
958 (* The extraction of each branch. *)
959 let extract_branch status i =
960 let r = NReference.mk_constructor (i+1) ip in
961 (* The types of the arguments of the corresponding constructor. *)
963 let status,res = expand status t in
964 status,type_subst_vect metas res in
967 (fun x (status,res) ->
968 let status,y = f status x in
970 oi.ip_types.(i) (status,[]) in
971 (* the corresponding signature *)
974 (fun x (status,res) ->
975 let status,y = type2sign status x in
977 oi.ip_types.(i) (status,[]) in
978 let s = sign_with_implicits r s in
979 (* Extraction of the branch (in functional form). *)
981 extract_maybe_term status context mle (type_recomp (l,mlt)) br.(i) in
982 (* We suppress dummy arguments according to signature. *)
983 let ids,e = case_expunge s e in
984 let e' = handle_exn r (List.length s) (fun _ -> "_") e in
985 status,(r, List.rev ids, e')
987 if mi.ind_kind = Singleton then
989 (* Informative singleton case: *)
990 (* [match c with C i -> t] becomes [let i = c' in t'] *)
991 assert (br_size = 1);
992 let status,(_,ids,e') = extract_branch status 0 in
993 assert (List.length ids = 1);
994 status,MLletin (tmp_id (List.hd ids),a,e')
997 (* Standard case: we apply [extract_branch]. *)
998 let status,typs = List.fold_right
999 (fun x (status,res) ->
1000 let status,y = type_simpl status x in
1002 (Array.to_list metas) (status,[]) in
1003 let info={ m_kind = mi.ind_kind; m_typs = typs; m_same = BranchNone } in
1006 (fun i _ (status,res) ->
1007 let status,y = extract_branch status i in
1008 status,y::res) br (status,[])
1010 status,MLcase (info, a, Array.of_list res)
1012 (*S ML declarations. *)
1014 (* [decomp_lams_eta env c t] finds the number [n] of products in the type [t],
1015 and decompose the term [c] in [n] lambdas, with eta-expansion if needed. *)
1017 let rec decomp_lams_eta_n n m status context c t =
1018 let rels = fst (splay_prod_n status context n t) in
1019 let rels',c = decompose_lam c in
1021 (* we'd better keep rels' as long as possible. *)
1022 let rels=(list_firstn d rels)@(List.map (fun (n,t) -> n, NCic.Decl t) rels')in
1023 let eta_args = List.rev_map (fun n -> NCic.Rel n) (interval 1 d) in
1024 rels, NCic.Appl ((NCicSubstitution.lift status d c)::eta_args)
1026 (* Let's try to identify some situation where extracted code
1027 will allow generalisation of type variables *)
1029 let rec gentypvar_ok c =
1031 | NCic.Lambda _ -> true
1032 | NCic.Const (NReference.Ref (_,
1036 |NReference.CoFix _))) -> true
1037 | NCic.Appl (c::v) ->
1038 (* if all arguments are variables, these variables will
1039 disappear after extraction (see [empty_s] below) *)
1040 List.for_all isRel v && gentypvar_ok c
1043 (*s From a constant to a ML declaration. *)
1045 let extract_std_constant status uri body typ =
1046 reset_meta_count ();
1047 (* The short type [t] (i.e. possibly with abbreviations). *)
1048 let status,res = record_constant_type status uri (Some typ) in
1050 (* The real type [t']: without head products, expanded, *)
1051 (* and with [Tvar] translated to [Tvar'] (not instantiable). *)
1052 let status,res = expand status (var2var' t) in
1053 let l,t' = type_decomp res in
1056 (fun x (status,res) ->
1057 let status,y = type2sign status x in
1060 (* Check for user-declared implicit information *)
1061 let s = sign_with_implicits uri(*CSC: (ConstRef uri)*) s in
1062 (* Decomposing the top level lambdas of [body].
1063 If there isn't enough, it's ok, as long as remaining args
1064 aren't to be pruned (and initial lambdas aren't to be all
1065 removed if the target language is strict). In other situations,
1066 eta-expansions create artificially enough lams (but that may
1067 break user's clever let-ins and partial applications). *)
1069 let n = List.length s
1070 and m = nb_lam body in
1071 if n <= m then decompose_lam_n n body
1073 let s,s' = list_split_at m s in
1074 if List.for_all ((=) Keep) s' && sign_kind s <> UnsafeLogicalSig
1075 then decompose_lam_n m body
1076 else decomp_lams_eta_n n m status [] body typ
1078 (* Should we do one eta-expansion to avoid non-generalizable '_a ? *)
1080 let n = List.length rels in
1081 let s,s' = list_split_at n s in
1082 let k = sign_kind s in
1083 let empty_s = (k = EmptySig || k = SafeLogicalSig) in
1084 if empty_s && not (gentypvar_ok c) && s' <> [] && type_maxvar t <> 0
1085 then decomp_lams_eta_n (n+1) n status [] body typ
1088 let n = List.length rels in
1089 let s = list_firstn n s in
1090 let l,l' = list_split_at n l in
1091 let t' = type_recomp (l',t') in
1092 (* The initial ML environment. *)
1093 let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
1094 (* The lambdas names. *)
1095 let ids = List.map (fun (n,_) -> Id (id_of_name n)) rels in
1096 (* The according Coq environment. *)
1097 let context = rels in
1098 (* The real extraction: *)
1099 let status,e = extract_term status context mle t' c [] in
1100 (* Expunging term and type from dummy lambdas. *)
1101 let trm = term_expunge s (ids,e) in
1102 let trm = handle_exn uri n (fun i -> fst (List.nth rels (i-1))) trm in
1103 let status,res = type_expunge_from_sign status s t in
1106 let extract_constant_spec status r bo typ =
1107 match flag_of_type status [] typ with
1108 | (Logic, TypeScheme) ->
1109 status,Stype (r, [], Some (Tdummy Ktype))
1110 | (Logic, Default) -> status,Sval (r, Tdummy Kother)
1111 | (Info, TypeScheme) ->
1112 let s,vl = type_sign_vl status [] typ in
1114 | None -> status,Stype (r, vl, None)
1116 let db = db_from_sign s in
1118 extract_type_scheme status [] db body (List.length s) in
1119 status,Stype (r, vl, Some t))
1120 | (Info, Default) ->
1121 let status,(_,t) = record_constant_type status r (Some typ) in
1122 let status,res = type_expunge status t in
1126 let extract_fixpoint_common uri height fix_or_cofix ifl =
1127 let recparamnoi,ti,ci =
1129 (fun (_,_,recparamno,ty,bo) (recparamnos,tys,bos) ->
1130 recparamno::recparamnos,ty::tys,bo::bos) ifl ([],[],[]) in
1131 let recparamnoi = Array.of_list recparamnoi in
1132 let ti = Array.of_list ti in
1133 let ci = Array.of_list ci in
1134 let n = Array.length ti in
1138 if fix_or_cofix then
1139 NReference.reference_of_spec uri
1140 (NReference.Fix (i,recparamnoi.(i),height))
1142 NReference.reference_of_spec uri (NReference.CoFix i)) in
1145 (*s Is a [ml_spec] logical ? *)
1146 let logical_spec = function
1147 | Stype (_, [], Some (Tdummy _)) -> true
1148 | Sval (_,Tdummy _) -> true
1149 | Sind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
1152 let extract_fixpoint status uri height fix_or_cofix is_projection ifl =
1154 if is_projection then
1155 let _,_,recparamno,_,_ = List.nth ifl 0 in
1156 let fieldspec = NReference.Fix (0,recparamno,height) in
1157 let ref = NReference.reference_of_spec uri fieldspec in
1158 confirm_projection status ref
1161 let ti,ci,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
1162 current_fixpoints := Some uri;
1163 let status,res = array_mapi_status status
1165 let _,head = split_all_prods status ~subst:[] [] ti.(i) in
1167 NCic.Sort s when classify_sort s = InProp -> status,`None
1169 let n = type_scheme_nb_args status [] ti.(i) in
1170 let ids = iterate (fun l -> anonymous_name::l) n [] in
1171 status,`Type (Dtype (vkn.(i), ids, Tunknown))
1173 if sort_of status [] ti.(i) <> InProp then
1174 let status,e,t = extract_std_constant status vkn.(i) ci.(i) ti.(i) in
1179 let axioms,terms,types =
1181 (fun x ((axioms,terms,types) as res) ->
1184 | `Some (t,ty) -> axioms,t::terms,ty::types
1185 | `Type decl -> decl::axioms,terms,types
1187 current_fixpoints := None;
1188 status,axioms @ [Dfix (vkn, Array.of_list terms, Array.of_list types)]
1190 let extract_fixpoint_spec status uri height fix_or_cofix ifl =
1191 let ti,_,_,vkn= extract_fixpoint_common uri height fix_or_cofix ifl in
1193 array_mapi_status status
1194 (fun status i vkn ->
1195 if sort_of status [] ti.(i) <> InProp then begin
1196 let status,spec = extract_constant_spec status vkn None ti.(i) in
1197 status, if logical_spec spec then None else Some spec
1201 status,HExtlib.filter_map (fun x -> x) (Array.to_list specs)
1203 let extract_constant status r bo typ =
1205 | None -> (* A logical axiom is risky, an informative one is fatal. *)
1206 (match flag_of_type status [] typ with
1207 | (Info,TypeScheme) ->
1208 if true (*CSC: not (is_custom r)*) then () (*CSC: only for warnings add_info_axiom r*);
1209 let n = type_scheme_nb_args status [] typ in
1210 let ids = iterate (fun l -> anonymous_name::l) n [] in
1211 status,Dtype (r, ids, Taxiom)
1213 if true (*CSC: not (is_custom r)*) then () (*CSC: only for warnings add_info_axiom r*);
1214 let status,(_,t) = record_constant_type status r (Some typ) in
1215 let status,res = type_expunge status t in
1216 status, Dterm (r, MLaxiom, res)
1217 | (Logic,TypeScheme) ->
1218 (*CSC: only for warnings add_log_axiom r;*)
1219 status,Dtype (r, [], Tdummy Ktype)
1220 | (Logic,Default) ->
1221 (*CSC: only for warnings add_log_axiom r;*)
1222 status,Dterm (r, MLdummy, Tdummy Kother))
1224 (match flag_of_type status [] typ with
1225 | (Logic, Default) ->
1226 status,Dterm (r, MLdummy, Tdummy Kother)
1227 | (Logic, TypeScheme) ->
1228 status,Dtype (r, [], Tdummy Ktype)
1229 | (Info, Default) ->
1230 let status,e,t = extract_std_constant status r body typ in
1231 status,Dterm (r,e,t)
1232 | (Info, TypeScheme) ->
1233 let s,vl = type_sign_vl status [] typ in
1234 let db = db_from_sign s in
1236 extract_type_scheme status [] db body (List.length s)
1237 in status,Dtype (r, vl, t))
1239 let extract_inductive status uri inductive ind_pragma leftno types =
1240 let status,ind = extract_ind0 status uri inductive ind_pragma leftno types in
1241 (*CSC: add_recursors status kn;*)
1242 let f status _i _j l =
1243 let implicits = [] (*CSC:implicits_of_global (ConstructRef ((kn,i),j+1))*) in
1244 let rec filter status i = function
1247 let status,l' = filter status (succ i) l in
1248 let status,res = expand status t in
1249 if isDummy res || List.mem i implicits then status,l'
1251 in filter status 1 l
1253 let status,packets =
1255 (fun i p (status,res) ->
1258 (fun j x (status,res) ->
1259 let status,y = f status i j x in
1261 ) p.ip_types (status,[])
1263 status, { p with ip_types = Array.of_list types }::res
1264 ) ind.ind_packets (status,[])
1265 in status,{ ind with ind_packets = Array.of_list packets }
1267 (*s Is a [ml_decl] logical ? *)
1269 let logical_decl = function
1270 | Dterm (_,MLdummy,Tdummy _) -> true
1271 | Dtype (_,[],Tdummy _) -> true
1273 (array_for_all ((=) MLdummy) av) &&
1274 (array_for_all isDummy tv)
1275 | Dind i -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
1278 let extract_impl status (uri,height,metasenv,subst,obj_kind) =
1279 assert (metasenv=[]);
1283 NCic.Constant (_,_,bo,typ,_) ->
1287 None -> NReference.Decl
1288 | Some _ -> NReference.Def height
1289 in NReference.reference_of_spec uri spec
1291 let status,res = extract_constant status r bo typ in
1293 | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
1295 extract_inductive status uri inductive ind_pragma leftno types
1298 | NCic.Fixpoint (fix_or_cofix,ifl,(_,_,def_pragma)) ->
1299 extract_fixpoint status uri height fix_or_cofix
1300 (def_pragma = `Projection) ifl
1302 status, List.filter (fun decl -> not (logical_decl decl)) decl
1305 let extract_spec status (uri,height,metasenv,subst,obj_kind) =
1306 assert (metasenv=[]);
1309 NCic.Constant (_,_,bo,typ,_) ->
1313 None -> NReference.Decl
1314 | Some _ -> NReference.Def height
1315 in NReference.reference_of_spec uri spec
1317 let status,spec = extract_constant_spec status r bo typ in
1318 status,if logical_spec spec then [] else [spec]
1319 | NCic.Inductive (inductive,leftno,types,(_,ind_pragma)) ->
1321 extract_inductive status uri inductive ind_pragma leftno types in
1322 let spec = Sind res in
1323 status,if logical_spec spec then [] else [spec]
1324 | NCic.Fixpoint (fix_or_cofix,ifl,_) ->
1325 extract_fixpoint_spec status uri height fix_or_cofix ifl
1327 let extract status obj =
1328 let status,res = extract_impl status obj in
1329 let status,resl = extract_spec status obj in