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: mlutil.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
14 open OcamlExtractionTable
23 (*S Names operations. *)
25 let anonymous_name = "x"
28 let anonymous = Id anonymous_name
30 let id_of_name = function
31 | "_" -> anonymous_name
34 let id_of_mlid = function
43 let is_tmp = function Tmp _ -> true | _ -> false
45 (*S Operations upon ML types (with meta). *)
47 let meta_count = ref 0
49 let reset_meta_count () = meta_count := 0
53 Tmeta {id = !meta_count; contents = None}
55 (*s Sustitution of [Tvar i] by [t] in a ML type. *)
57 let type_subst i t0 t =
58 let rec subst t = match t with
59 | Tvar j when i = j -> t0
60 | Tmeta {contents=None} -> t
61 | Tmeta {contents=Some u} -> subst u
62 | Tarr (a,b) -> Tarr (subst a, subst b)
63 | Tglob (r, l) -> Tglob (r, List.map subst l)
67 (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *)
69 let type_subst_list l t =
70 let rec subst t = match t with
71 | Tvar j -> List.nth l (j-1)
72 | Tmeta {contents=None} -> t
73 | Tmeta {contents=Some u} -> subst u
74 | Tarr (a,b) -> Tarr (subst a, subst b)
75 | Tglob (r, l) -> Tglob (r, List.map subst l)
79 (* Simultaneous substitution of [[|Tvar 1; ... ; Tvar n|]] by [v] in a ML type. *)
81 let type_subst_vect v t =
82 let rec subst t = match t with
84 | Tmeta {contents=None} -> t
85 | Tmeta {contents=Some u} -> subst u
86 | Tarr (a,b) -> Tarr (subst a, subst b)
87 | Tglob (r, l) -> Tglob (r, List.map subst l)
91 (*s From a type schema to a type. All [Tvar] become fresh [Tmeta]. *)
93 let instantiation (nb,t) = type_subst_vect (Array.init nb new_meta) t
95 (*s Occur-check of a free meta in a type *)
97 let rec type_occurs alpha t =
99 | Tmeta {id=beta; contents=None} -> alpha = beta
100 | Tmeta {contents=Some u} -> type_occurs alpha u
101 | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2
102 | Tglob (_r,l) -> List.exists (type_occurs alpha) l
105 (*s Most General Unificator *)
107 let rec mgu = function
108 | Tmeta m, Tmeta m' when m.id = m'.id -> ()
109 | Tmeta m, t | t, Tmeta m ->
110 (match m.contents with
111 | Some u -> mgu (u, t)
112 | None when type_occurs m.id t -> raise Impossible
113 | None -> m.contents <- Some t)
114 | Tarr(a, b), Tarr(a', b') ->
115 mgu (a, a'); mgu (b, b')
116 | Tglob (r,l), Tglob (r',l') when r = r' ->
117 List.iter mgu (List.combine l l')
118 | Tdummy _, Tdummy _ -> ()
119 | t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
120 | _ -> raise Impossible
122 let needs_magic p = try mgu p; false with Impossible -> true
124 let put_magic_if b a = if b then MLmagic a else a
126 let put_magic p a = if needs_magic p then MLmagic a else a
128 let generalizable a =
131 | _ -> true (* TODO, this is just an approximation for the moment *)
135 module Mlenv = struct
137 let meta_cmp m m' = compare m.id m'.id
138 module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end)
140 (* Main MLenv type. [env] is the real environment, whereas [free]
141 (tries to) record the free meta variables occurring in [env]. *)
143 type t = { env : ml_schema list; mutable free : Metaset.t}
145 (* Empty environment. *)
147 let empty = { env = []; free = Metaset.empty }
149 (* [get] returns a instantiated copy of the n-th most recently added
150 type in the environment. *)
153 assert (List.length mle.env >= n);
154 instantiation (List.nth mle.env (n-1))
156 (* [find_free] finds the free meta in a type. *)
158 let rec find_free set = function
159 | Tmeta m when m.contents = None -> Metaset.add m set
160 | Tmeta {contents = Some t} -> find_free set t
161 | Tarr (a,b) -> find_free (find_free set a) b
162 | Tglob (_,l) -> List.fold_left find_free set l
165 (* The [free] set of an environment can be outdate after
166 some unifications. [clean_free] takes care of that. *)
169 let rem = ref Metaset.empty
170 and add = ref Metaset.empty in
171 let clean m = match m.contents with
173 | Some u -> rem := Metaset.add m !rem; add := find_free !add u
175 Metaset.iter clean mle.free;
176 mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add
178 (* From a type to a type schema. If a [Tmeta] is still uninstantiated
179 and does appears in the [mle], then it becomes a [Tvar]. *)
181 let generalization mle t =
183 let map = ref (Intmap.empty : int Intmap.t) in
184 let add_new i = incr c; map := Intmap.add i !c !map; !c in
185 let rec meta2var t = match t with
186 | Tmeta {contents=Some u} -> meta2var u
187 | Tmeta ({id=i} as m) ->
188 (try Tvar (Intmap.find i !map)
190 if Metaset.mem m mle.free then t
191 else Tvar (add_new i))
192 | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2)
193 | Tglob (r,l) -> Tglob (r, List.map meta2var l)
197 (* Adding a type in an environment, after generalizing. *)
201 { env = generalization mle t :: mle.env; free = mle.free }
203 (* Adding a type with no [Tvar], hence no generalization needed. *)
205 let push_type {env=e;free=f} t =
206 { env = (0,t) :: e; free = find_free f t}
208 (* Adding a type with no [Tvar] nor [Tmeta]. *)
210 let push_std_type {env=e;free=f} t =
211 { env = (0,t) :: e; free = f}
215 (*S Operations upon ML types (without meta). *)
217 (*s Does a section path occur in a ML type ? *)
219 let rec type_mem_kn uri =
221 | Tmeta {contents = Some t} -> type_mem_kn uri t
223 let NReference.Ref (uri',_) = r in
224 NUri.eq uri uri' || List.exists (type_mem_kn uri) l
225 | Tarr (a,b) -> (type_mem_kn uri a) || (type_mem_kn uri b)
228 (*s Greatest variable occurring in [t]. *)
231 let rec parse n = function
232 | Tmeta {contents = Some t} -> parse n t
234 | Tarr (a,b) -> parse (parse n a) b
235 | Tglob (_,l) -> List.fold_left parse n l
239 (*s What are the type variables occurring in [t]. *)
241 let intset_union_map_list f l =
242 List.fold_left (fun s t -> Intset.union s (f t)) Intset.empty l
244 let intset_union_map_array f a =
245 Array.fold_left (fun s t -> Intset.union s (f t)) Intset.empty a
247 let rec type_listvar = function
248 | Tmeta {contents = Some t} -> type_listvar t
249 | Tvar i | Tvar' i -> Intset.singleton i
250 | Tarr (a,b) -> Intset.union (type_listvar a) (type_listvar b)
251 | Tglob (_,l) -> intset_union_map_list type_listvar l
254 (*s From [a -> b -> c] to [[a;b],c]. *)
256 let rec type_decomp = function
257 | Tmeta {contents = Some t} -> type_decomp t
258 | Tarr (a,b) -> let l,h = type_decomp b in a::l, h
261 (*s The converse: From [[a;b],c] to [a -> b -> c]. *)
263 let rec type_recomp (l,t) = match l with
265 | a::l -> Tarr (a, type_recomp (l,t))
267 (*s Translating [Tvar] to [Tvar'] to avoid clash. *)
269 let rec var2var' = function
270 | Tmeta {contents = Some t} -> var2var' t
272 | Tarr (a,b) -> Tarr (var2var' a, var2var' b)
273 | Tglob (r,l) -> Tglob (r, List.map var2var' l)
276 type 'status abbrev_map =
277 'status -> NReference.reference -> ('status * ml_type) option
279 (*s Delta-reduction of type constants everywhere in a ML type [t].
280 [env] is a function of type [ml_type_env]. *)
282 let type_expand status env t =
283 let rec expand status = function
284 | Tmeta {contents = Some t} -> expand status t
286 (match env status r with
287 | Some (status,mlt) -> expand status (type_subst_list l mlt)
291 (fun t (status,res) ->
292 let status,res' = expand status t in
298 let status,a = expand status a in
299 let status,b = expand status b in
302 if OcamlExtractionTable.type_expand () then
307 let type_simpl status = type_expand status (fun _ _ -> None)
309 (*s Generating a signature from a ML type. *)
311 let type_to_sign status env t =
312 let status,res = type_expand status env t in
318 let type_to_signature status env t =
320 | Tmeta {contents = Some t} -> f t
321 | Tarr (Tdummy d, b) -> Kill d :: f b
322 | Tarr (_, b) -> Keep :: f b
325 let status,res = type_expand status env t in
328 let isKill = function Kill _ -> true | _ -> false
330 let isDummy = function Tdummy _ -> true | _ -> false
332 let sign_of_id = function
333 | Dummy -> Kill Kother
336 (* Classification of signatures *)
340 | NonLogicalSig (* at least a [Keep] *)
341 | UnsafeLogicalSig (* No [Keep], at least a [Kill Kother] *)
342 | SafeLogicalSig (* only [Kill Ktype] *)
344 let rec sign_kind = function
346 | Keep :: _ -> NonLogicalSig
348 match sign_kind s with
349 | NonLogicalSig -> NonLogicalSig
350 | UnsafeLogicalSig -> UnsafeLogicalSig
351 | SafeLogicalSig | EmptySig ->
352 if k = Kother then UnsafeLogicalSig else SafeLogicalSig
354 (* Removing the final [Keep] in a signature *)
356 let rec sign_no_final_keeps = function
359 let s' = k :: sign_no_final_keeps s in
360 if s' = [Keep] then [] else s'
362 (*s Removing [Tdummy] from the top level of a ML type. *)
364 let type_expunge_from_sign status env s t =
365 let rec expunge status s t =
366 if s = [] then status,t else match t with
367 | Tmeta {contents = Some t} -> expunge status s t
369 let status,t = expunge status (List.tl s) b in
370 status, if List.hd s = Keep then Tarr (a, t) else t
372 (match env status r with
373 | Some (status,mlt) -> expunge status s (type_subst_list l mlt)
374 | None -> assert false)
377 let status,t = expunge status (sign_no_final_keeps s) t in
379 if sign_kind s = UnsafeLogicalSig then
380 Tarr (Tdummy Kother, t)
383 let type_expunge status env t =
384 let status,res = type_to_signature status env t in
385 type_expunge_from_sign status env res t
387 (*S Generic functions over ML ast terms. *)
389 let mlapp f a = if a = [] then f else MLapp (f,a)
391 (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care
392 of the number of bingings crossed before reaching the [MLrel]. *)
395 let rec iter n = function
397 | MLlam (_,a) -> iter (n+1) a
398 | MLletin (_,a,b) -> iter n a; iter (n+1) b
400 iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
401 | MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
402 | MLapp (a,l) -> iter n a; List.iter (iter n) l
403 | MLcons (_,_,l) -> List.iter (iter n) l
404 | MLmagic a -> iter n a
405 | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
408 (*s Map over asts. *)
410 let ast_map_case f (c,ids,a) = (c,ids,f a)
412 let ast_map f = function
413 | MLlam (i,a) -> MLlam (i, f a)
414 | MLletin (i,a,b) -> MLletin (i, f a, f b)
415 | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
416 | MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
417 | MLapp (a,l) -> MLapp (f a, List.map f l)
418 | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
419 | MLmagic a -> MLmagic (f a)
420 | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
422 (*s Map over asts, with binding depth as parameter. *)
424 let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
426 let ast_map_lift f n = function
427 | MLlam (i,a) -> MLlam (i, f (n+1) a)
428 | MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
429 | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
431 let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
432 | MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
433 | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
434 | MLmagic a -> MLmagic (f n a)
435 | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
437 (*s Iter over asts. *)
439 let ast_iter_case f (_c,_ids,a) = f a
441 let ast_iter f = function
442 | MLlam (_i,a) -> f a
443 | MLletin (_i,a,b) -> f a; f b
444 | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
445 | MLfix (_i,_ids,v) -> Array.iter f v
446 | MLapp (a,l) -> f a; List.iter f l
447 | MLcons (_,_c,l) -> List.iter f l
449 | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
451 (*S Operations concerning De Bruijn indices. *)
453 (*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *)
457 ast_iter_rel (fun i -> if i = k then raise Found) t; false
460 (*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)]
461 in [t] with [k<=i<=k'] *)
463 let ast_occurs_itvl k k' t =
465 ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false
468 (*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *)
472 ast_iter_rel (fun i -> if i = k then incr cpt) t;
475 let nb_occur t = nb_occur_k 1 t
477 (* Number of occurences of [Rel 1] in [t], with special treatment of match:
478 occurences in different branches aren't added, but we rather use max. *)
481 let rec nb k = function
482 | MLrel i -> if i = k then 1 else 0
486 (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
487 | MLletin (_,a,b) -> (nb k a) + (nb (k+1) b)
488 | MLfix (_,ids,v) -> let k = k+(Array.length ids) in
489 Array.fold_left (fun r a -> r+(nb k a)) 0 v
490 | MLlam (_,a) -> nb (k+1) a
491 | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
492 | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
493 | MLmagic a -> nb k a
494 | MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
497 (*s Lifting on terms.
498 [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *)
501 let rec liftrec n = function
502 | MLrel i as a -> if i-n < 1 then a else MLrel (i+k)
503 | a -> ast_map_lift liftrec n a
504 in if k = 0 then t else liftrec 0 t
506 let ast_pop t = ast_lift (-1) t
508 (*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ...
509 Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *)
511 let permut_rels k k' =
512 let rec permut n = function
515 if i'<1 || i'>k+k' then a
516 else if i'<=k then MLrel (i+k')
518 | a -> ast_map_lift permut n a
521 (*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t].
522 Lifting (of one binder) is done at the same time. *)
525 let rec subst n = function
528 if i'=1 then ast_lift n e
531 | a -> ast_map_lift subst n a
534 (*s Generalized substitution.
535 [gen_subst v d t] applies to [t] the substitution coded in the
536 [v] array: [(Rel i)] becomes [v.(i-1)]. [d] is the correction applies
537 to [Rel] greater than [Array.length v]. *)
539 let gen_subst v d t =
540 let rec subst n = function
544 else if i' <= Array.length v then
546 | None -> MLexn ("UNBOUND " ^ string_of_int i')
547 | Some u -> ast_lift n u
549 | a -> ast_map_lift subst n a
552 (*S Operations concerning lambdas. *)
554 (*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns
555 [[idn;...;id1]] and the term [t]. *)
558 let rec collect acc = function
559 | MLlam(id,t) -> collect (id::acc) t
563 (*s [collect_n_lams] does the same for a precise number of [MLlam]. *)
566 let rec collect acc n t =
569 | MLlam(id,t) -> collect (id::acc) (n-1) t
573 (*s [remove_n_lams] just removes some [MLlam]. *)
575 let rec remove_n_lams n t =
578 | MLlam(_,t) -> remove_n_lams (n-1) t
581 (*s [nb_lams] gives the number of head [MLlam]. *)
583 let rec nb_lams = function
584 | MLlam(_,t) -> succ (nb_lams t)
587 (*s [named_lams] does the converse of [collect_lams]. *)
589 let rec named_lams ids a = match ids with
591 | id :: ids -> named_lams ids (MLlam (id,a))
593 (*s The same for a specific identifier (resp. anonymous, dummy) *)
595 let rec many_lams id a = function
597 | n -> many_lams id (MLlam (id,a)) (pred n)
599 let anonym_lams a n = many_lams anonymous a n
600 let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n
601 let dummy_lams a n = many_lams Dummy a n
603 (*s mixed according to a signature. *)
605 let rec anonym_or_dummy_lams a = function
607 | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s)
608 | Kill _ :: s -> MLlam(Dummy, anonym_or_dummy_lams a s)
610 (*S Operations concerning eta. *)
612 (*s The following function creates [MLrel n;...;MLrel 1] *)
615 if n = 0 then [] else (MLrel n)::(eta_args (pred n))
617 (*s Same, but filtered by a signature. *)
619 let rec eta_args_sign n = function
621 | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s)
622 | Kill _ :: s -> eta_args_sign (n-1) s
624 (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *)
626 let rec test_eta_args_lift k n = function
628 | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q)
630 (*s Computes an eta-reduction. *)
633 let ids,t = collect_lams e in
634 let n = List.length ids in
638 let m = List.length a in
643 list_skipn m ids, f, a
645 let a1,a2 = list_chop (m-n) a in
648 let p = List.length args in
649 if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body)
650 then named_lams ids (ast_lift (-p) body)
654 (*s Computes all head linear beta-reductions possible in [(t a)].
655 Non-linear head beta-redex become let-in. *)
657 let rec linear_beta_red a t = match a,t with
659 | a0::a, MLlam (id,t) ->
660 (match nb_occur_match t with
661 | 0 -> linear_beta_red a (ast_pop t)
662 | 1 -> linear_beta_red a (ast_subst a0 t)
664 let a = List.map (ast_lift 1) a in
665 MLletin (id, a0, linear_beta_red a t))
668 let rec tmp_head_lams = function
669 | MLlam (id, t) -> MLlam (tmp_id id, tmp_head_lams t)
672 (*s Applies a substitution [s] of constants by their body, plus
673 linear beta reductions at modified positions.
674 Moreover, we mark some lambdas as suitable for later linear
675 reduction (this helps the inlining of recursors).
678 let rec ast_glob_subst _s _t = assert false (*CSC: reimplement match t with
679 | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) ->
680 let a = List.map (fun e -> tmp_head_lams (ast_glob_subst s e)) a in
681 (try linear_beta_red a (Refmap'.find refe s)
682 with Not_found -> MLapp (f, a))
683 | MLglob ((ConstRef kn) as refe) ->
684 (try Refmap'.find refe s with Not_found -> t)
685 | _ -> ast_map (ast_glob_subst s) t *)
688 (*S Auxiliary functions used in simplification of ML cases. *)
690 (* Factorisation of some match branches into a common "x -> f x"
691 branch may break types sometimes. Example: [type 'x a = A].
692 Then [let id = function A -> A] has type ['x a -> 'y a],
693 which is incompatible with the type of [let id x = x].
694 We now check that the type arguments of the inductive are
695 preserved by our transformation.
697 TODO: this verification should be done someday modulo
698 expansion of type definitions.
701 (*s [branch_as_function b typs (r,l,c)] tries to see branch [c]
702 as a function [f] applied to [MLcons(r,l)]. For that it transforms
703 any [MLcons(r,l)] in [MLrel 1] and raises [Impossible]
704 if any variable in [l] occurs outside such a [MLcons] *)
706 let branch_as_fun typs (r,l,c) =
707 let nargs = List.length l in
708 let rec genrec n = function
712 else if i'>nargs then MLrel (i-nargs+1)
713 else raise Impossible
714 | MLcons(i,r',args) when
715 r=r' && (test_eta_args_lift n nargs args) && typs = i.c_typs ->
717 | a -> ast_map_lift genrec n a
720 (*s [branch_as_cst (r,l,c)] tries to see branch [c] as a constant
721 independent from the pattern [MLcons(r,l)]. For that is raises [Impossible]
722 if any variable in [l] occurs in [c], and otherwise returns [c] lifted to
723 appear like a function with one arg (for uniformity with [branch_as_fun]).
724 NB: [MLcons(r,l)] might occur nonetheless in [c], but only when [l] is
725 empty, i.e. when [r] is a constant constructor
728 let branch_as_cst (_,l,c) =
729 let n = List.length l in
730 if ast_occurs_itvl 1 n c then raise Impossible;
733 (* A branch [MLcons(r,l)->c] can be seen at the same time as a function
734 branch and a constant branch, either because:
735 - [MLcons(r,l)] doesn't occur in [c]. For example : "A -> B"
736 - this constructor is constant (i.e. [l] is empty). For example "A -> A"
737 When searching for the best factorisation below, we'll try both.
740 (* The following structure allows to record which element occurred
741 at what position, and then finally return the most frequent
742 element and its positions. *)
744 let census_add, census_max, census_clean =
745 let h = Hashtbl.create 13 in
746 let clear () = Hashtbl.clear h in
748 let s = try Hashtbl.find h e with Not_found -> Intset.empty in
749 Hashtbl.replace h e (Intset.add i s)
752 let len = ref 0 and lst = ref Intset.empty and elm = ref e0 in
755 let n = Intset.cardinal s in
756 if n > !len then begin len := n; lst := s; elm := e end)
762 (* [factor_branches] return the longest possible list of branches
763 that have the same factorization, either as a function or as a
767 let factor_branches o typs br =
769 for i = 0 to Array.length br - 1 do
770 if o.opt_case_idr then
771 (try census_add (branch_as_fun typs br.(i)) i with Impossible -> ());
772 if o.opt_case_cst then
773 (try census_add (branch_as_cst br.(i)) i with Impossible -> ());
775 let br_factor, br_set = census_max MLdummy in
777 let n = Intset.cardinal br_set in
779 else if Array.length br >= 2 && n < 2 then None
780 else Some (br_factor, br_set)
782 (*s If all branches are functions, try to permut the case and the functions. *)
784 let rec merge_ids ids ids' = match ids,ids' with
787 | i::ids, i'::ids' ->
788 (if i = Dummy then i' else i) :: (merge_ids ids ids')
790 let is_exn = function MLexn _ -> true | _ -> false
792 let rec permut_case_fun br _acc =
793 let nb = ref max_int in
794 Array.iter (fun (_,_,t) ->
795 let ids, c = collect_lams t in
796 let n = List.length ids in
797 if (n < !nb) && (not (is_exn c)) then nb := n) br;
798 if !nb = max_int || !nb = 0 then ([],br)
800 let br = Array.copy br in
802 for i = 0 to Array.length br - 1 do
803 let (r,l,t) = br.(i) in
804 let local_nb = nb_lams t in
805 if local_nb < !nb then (* t = MLexn ... *)
806 br.(i) <- (r,l,remove_n_lams local_nb t)
808 let local_ids,t = collect_n_lams !nb t in
809 ids := merge_ids !ids local_ids;
810 br.(i) <- (r,l,permut_rels !nb (List.length l) t)
816 (*S Generalized iota-reduction. *)
818 (* Definition of a generalized iota-redex: it's a [MLcase(e,_)]
819 with [(is_iota_gen e)=true]. Any generalized iota-redex is
820 transformed into beta-redexes. *)
822 let rec is_iota_gen = function
824 | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
827 let constructor_index _ = assert false (*CSC: function
828 | ConstructRef (_,j) -> pred j
829 | _ -> assert false*)
832 let rec iota k = function
834 let (_,ids,c) = br.(constructor_index r) in
835 let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
836 let c = ast_lift k c in
840 Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
841 in MLcase(i,e, new_br)
845 let is_atomic = function
846 | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true
849 let is_imm_apply = function MLapp (MLrel 1, _) -> true | _ -> false
851 (** Program creates a let-in named "program_branch_NN" for each branch of match.
852 Unfolding them leads to more natural code (and more dummy removal) *)
854 let is_program_branch = function
857 let br = "program_branch_" in
858 let n = String.length br in
860 ignore (int_of_string (String.sub s n (String.length s - n)));
861 String.sub s 0 n = br
863 | Tmp _ | Dummy -> false
865 let expand_linear_let o id e =
866 o.opt_lin_let || is_tmp id || is_program_branch id || is_imm_apply e
868 (*S The main simplification function. *)
870 (* Some beta-iota reductions + simplifications. *)
872 let rec simpl o = function
873 | MLapp (f, []) -> simpl o f
874 | MLapp (f, a) -> simpl_app o (List.map (simpl o) a) (simpl o f)
876 let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
877 simpl_case o i br (simpl o e)
878 | MLletin(Dummy,_,e) -> simpl o (ast_pop e)
882 (is_atomic c) || (is_atomic e) ||
883 (let n = nb_occur_match e in
884 (n = 0 || (n=1 && expand_linear_let o id e)))
886 simpl o (ast_subst c e)
888 MLletin(id, simpl o c, e)
890 let n = Array.length ids in
891 if ast_occurs_itvl 1 n c.(i) then
892 MLfix (i, ids, Array.map (simpl o) c)
893 else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *)
894 | a -> ast_map (simpl o) a
896 (* invariant : list [a] of arguments is non-empty *)
898 and simpl_app o a = function
899 | MLapp (f',a') -> simpl_app o (a'@a) f'
901 simpl o (MLapp (ast_pop t, List.tl a))
902 | MLlam (id,t) -> (* Beta redex *)
903 (match nb_occur_match t with
904 | 0 -> simpl o (MLapp (ast_pop t, List.tl a))
905 | 1 when (is_tmp id || o.opt_lin_beta) ->
906 simpl o (MLapp (ast_subst (List.hd a) t, List.tl a))
908 let a' = List.map (ast_lift 1) (List.tl a) in
909 simpl o (MLletin (id, List.hd a, MLapp (t, a'))))
910 | MLletin (id,e1,e2) when o.opt_let_app ->
911 (* Application of a letin: we push arguments inside *)
912 MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
913 | MLcase (i,e,br) when o.opt_case_app ->
914 (* Application of a case: we push arguments inside *)
918 let k = List.length l in
919 let a' = List.map (ast_lift k) a in
920 (n, l, simpl o (MLapp (t,a')))) br
921 in simpl o (MLcase (i,e,br'))
922 | (MLdummy | MLexn _) as e -> e
923 (* We just discard arguments in those cases. *)
926 (* Invariant : all empty matches should now be [MLexn] *)
928 and simpl_case o i br e =
929 if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
930 simpl o (iota_gen br e)
932 (* Swap the case and the lam if possible *)
933 let ids,br = if o.opt_case_fun then permut_case_fun br [] else [],br in
934 let n = List.length ids in
936 simpl o (named_lams ids (MLcase (i,ast_lift n e, br)))
938 (* Can we merge several branches as the same constant or function ? *)
939 match factor_branches o i.m_typs br with
940 | Some (f,ints) when Intset.cardinal ints = Array.length br ->
941 (* If all branches have been factorized, we remove the match *)
942 simpl o (MLletin (Tmp anonymous_name, e, f))
944 let same = if ast_occurs 1 f then BranchFun ints else BranchCst ints
945 in MLcase ({i with m_same=same}, e, br)
946 | None -> MLcase (i, e, br)
948 (*S Local prop elimination. *)
949 (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *)
951 (*s In a list, it selects only the elements corresponding to a [Keep]
952 in the boolean list [l]. *)
954 let rec select_via_bl l args = match l,args with
956 | Keep::l,a::args -> a :: (select_via_bl l args)
957 | Kill _::l,_a::args -> select_via_bl l args
960 (*s [kill_some_lams] removes some head lambdas according to the signature [bl].
961 This list is build on the identifier list model: outermost lambda
963 [Rels] corresponding to removed lambdas are supposed not to occur, and
964 the other [Rels] are made correct via a [gen_subst].
965 Output is not directly a [ml_ast], compose with [named_lams] if needed. *)
967 let kill_some_lams bl (ids,c) =
968 let n = List.length bl in
969 let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in
971 else if n' = 0 then [],ast_lift (-n) c
973 let v = Array.make n None in
974 let rec parse_ids i j = function
976 | Keep :: l -> v.(i) <- Some (MLrel j); parse_ids (i+1) (j+1) l
977 | Kill _ :: l -> parse_ids (i+1) j l
979 select_via_bl bl ids, gen_subst v (n'-n) c
982 (*s [kill_dummy_lams] uses the last function to kill the lambdas corresponding
983 to a [dummy_name]. It can raise [Impossible] if there is nothing to do, or
984 if there is no lambda left at all. *)
986 let kill_dummy_lams c =
987 let ids,c = collect_lams c in
988 let bl = List.map sign_of_id ids in
989 if not (List.mem Keep bl) then raise Impossible;
990 let rec fst_kill n = function
991 | [] -> raise Impossible
993 | Keep :: bl -> fst_kill (n+1) bl
995 let skip = max 0 ((fst_kill 0 bl) - 1) in
996 let ids_skip, ids = list_chop skip ids in
997 let _, bl = list_chop skip bl in
998 let c = named_lams ids_skip c in
999 let ids',c = kill_some_lams bl (ids,c) in
1000 ids, named_lams ids' c
1002 (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
1003 and a signature [s] and builds a eta-long version. *)
1005 (* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is :
1006 [fun idn ... id1 x x _ x -> (c' 4 3 __ 1)] with [c' = lift 4 c] *)
1008 let eta_expansion_sign s (ids,c) =
1009 let rec abs ids rels i = function
1011 let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels
1012 in ids, MLapp (ast_lift (i-1) c, a)
1013 | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l
1014 | Kill _ :: l -> abs (Dummy :: ids) (MLdummy :: rels) (i+1) l
1017 (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e]
1018 in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas
1019 corresponding to [Del] in [s]. *)
1021 let case_expunge s e =
1022 let m = List.length s in
1023 let n = nb_lams e in
1024 let p = if m <= n then collect_n_lams m e
1025 else eta_expansion_sign (list_skipn n s) (collect_lams e) in
1026 kill_some_lams (List.rev s) p
1028 (*s [term_expunge] takes a function [fun idn ... id1 -> c]
1029 and a signature [s] and remove dummy lams. The difference
1030 with [case_expunge] is that we here leave one dummy lambda
1031 if all lambdas are logical dummy and the target language is strict. *)
1033 let term_expunge s (ids,c) =
1036 let ids,c = kill_some_lams (List.rev s) (ids,c) in
1037 if ids = [] && List.mem (Kill Kother) s then
1038 MLlam (Dummy, ast_lift 1 c)
1039 else named_lams ids c
1041 (*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
1042 purge the args of [MLrel r] corresponding to a [dummy_name].
1043 It makes eta-expansion if needed. *)
1045 let kill_dummy_args ids r t =
1046 let m = List.length ids in
1047 let bl = List.rev_map sign_of_id ids in
1048 let rec found n = function
1049 | MLrel r' when r' = r + n -> true
1050 | MLmagic e -> found n e
1053 let rec killrec n = function
1054 | MLapp(e, a) when found n e ->
1055 let k = max 0 (m - (List.length a)) in
1056 let a = List.map (killrec n) a in
1057 let a = List.map (ast_lift k) a in
1058 let a = select_via_bl bl (a @ (eta_args k)) in
1059 named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
1060 | e when found n e ->
1061 let a = select_via_bl bl (eta_args m) in
1062 named_lams ids (MLapp (ast_lift m e, a))
1063 | e -> ast_map_lift killrec n e
1066 (*s The main function for local [dummy] elimination. *)
1068 let rec kill_dummy = function
1071 let ids,c = kill_dummy_fix i c in
1072 ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1))
1073 with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
1074 | MLapp (MLfix (i,fi,c),a) ->
1075 let a = List.map kill_dummy a in
1077 let ids,c = kill_dummy_fix i c in
1078 let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
1079 let fake' = kill_dummy_args ids 1 fake in
1080 ast_subst (MLfix (i,fi,c)) fake'
1081 with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
1082 | MLletin(id, MLfix (i,fi,c),e) ->
1084 let ids,c = kill_dummy_fix i c in
1085 let e = kill_dummy (kill_dummy_args ids 1 e) in
1086 MLletin(id, MLfix(i,fi,c),e)
1088 MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
1089 | MLletin(id,c,e) ->
1091 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
1092 let e = kill_dummy (kill_dummy_args ids 1 e) in
1093 let c = kill_dummy c in
1094 if is_atomic c then ast_subst c e else MLletin (id, c, e)
1095 with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
1096 | a -> ast_map kill_dummy a
1098 (* Similar function, but acting only on head lambdas and let-ins *)
1100 and kill_dummy_hd = function
1101 | MLlam(id,e) -> MLlam(id, kill_dummy_hd e)
1102 | MLletin(id,c,e) ->
1104 let ids,c = kill_dummy_lams (kill_dummy_hd c) in
1105 let e = kill_dummy_hd (kill_dummy_args ids 1 e) in
1106 let c = kill_dummy c in
1107 if is_atomic c then ast_subst c e else MLletin (id, c, e)
1108 with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
1111 and kill_dummy_fix i c =
1112 let n = Array.length c in
1113 let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in
1114 let c = Array.copy c in c.(i) <- ci;
1115 for j = 0 to (n-1) do
1116 c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j))
1120 (*s Putting things together. *)
1123 let o = optims () in
1125 let a' = if o.opt_kill_dum then kill_dummy (simpl o a) else simpl o a in
1126 if a = a' then a else norm a'
1129 (*S Special treatment of fixpoint for pretty-printing purpose. *)
1131 let general_optimize_fix f ids n args m c =
1132 let v = Array.make n 0 in
1133 for i=0 to (n-1) do v.(i)<-i done;
1134 let aux i = function
1135 | MLrel j when v.(j-1)>=0 ->
1136 if ast_occurs (j+1) c then raise Impossible else v.(j-1)<-(-i-1)
1137 | _ -> raise Impossible
1138 in list_iter_i aux args;
1139 let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in
1140 let new_f = anonym_tmp_lams (MLapp (MLrel (n+m+1),args_f)) m in
1141 let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in
1142 MLfix(0,[|f|],[|new_c|])
1144 let optimize_fix a =
1145 if not (optims()).opt_fix_fun then a
1147 let ids,a' = collect_lams a in
1148 let n = List.length ids in
1151 | MLfix(_,[|f|],[|c|]) ->
1152 let new_f = MLapp (MLrel (n+1),eta_args n) in
1153 let new_c = named_lams ids (normalize (ast_subst new_f c))
1154 in MLfix(0,[|f|],[|new_c|])
1156 let m = List.length args in
1159 (test_eta_args_lift 0 n args) && not (ast_occurs_itvl 1 m a')
1161 | MLfix(_,[|f|],[|c|]) ->
1162 (try general_optimize_fix f ids n args m c
1163 with Impossible -> a)
1169 (* Utility functions used in the decision of inlining. *)
1171 let rec ml_size = function
1172 | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
1173 | MLlam(_,t) -> 1 + ml_size t
1174 | MLcons(_,_,l) -> ml_size_list l
1176 1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
1177 | MLfix(_,_,f) -> ml_size_array f
1178 | MLletin (_,_,t) -> ml_size t
1179 | MLmagic t -> ml_size t
1182 and ml_size_list l = List.fold_left (fun a t -> a + ml_size t) 0 l
1184 and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l
1186 let is_fix = function MLfix _ -> true | _ -> false
1188 let rec is_constr = function
1190 | MLlam(_,t) -> is_constr t
1195 (* A variable is strict if the evaluation of the whole term implies
1196 the evaluation of this variable. Non-strict variables can be found
1197 behind Match, for example. Expanding a term [t] is a good idea when
1198 it begins by at least one non-strict lambda, since the corresponding
1199 argument to [t] might be unevaluated in the expanded code. *)
1203 let lift n l = List.map ((+) n) l
1205 let pop n l = List.map (fun x -> if x<=n then raise Toplevel else x-n) l
1207 (* This function returns a list of de Bruijn indices of non-strict variables,
1208 or raises [Toplevel] if it has an internal non-strict variable.
1209 In fact, not all variables are checked for strictness, only the ones which
1210 de Bruijn index is in the candidates list [cand]. The flag [add] controls
1211 the behaviour when going through a lambda: should we add the corresponding
1212 variable to the candidates? We use this flag to check only the external
1213 lambdas, those that will correspond to arguments. *)
1215 let rec non_stricts add cand = function
1217 let cand = lift 1 cand in
1218 let cand = if add then 1::cand else cand in
1219 pop 1 (non_stricts add cand t)
1221 List.filter ((<>) n) cand
1223 let cand = non_stricts false cand t in
1224 List.fold_left (non_stricts false) cand l
1226 List.fold_left (non_stricts false) cand l
1227 | MLletin (_,t1,t2) ->
1228 let cand = non_stricts false cand t1 in
1229 pop 1 (non_stricts add (lift 1 cand) t2)
1231 let n = Array.length i in
1232 let cand = lift n cand in
1233 let cand = Array.fold_left (non_stricts false) cand f in
1236 (* The only interesting case: for a variable to be non-strict, *)
1237 (* it is sufficient that it appears non-strict in at least one branch, *)
1238 (* so we make an union (in fact a merge). *)
1239 let cand = non_stricts false cand t in
1242 let n = List.length i in
1243 let cand = lift n cand in
1244 let cand = pop n (non_stricts add cand t) in
1245 Sort.merge (<=) cand c) [] v
1246 (* [merge] may duplicates some indices, but I don't mind. *)
1248 non_stricts add cand t
1252 (* The real test: we are looking for internal non-strict variables, so we start
1253 with no candidates, and the only positive answer is via the [Toplevel]
1256 let is_not_strict t =
1257 try let _ = non_stricts true [] t in false
1258 with Toplevel -> true
1260 (*s Inlining decision *)
1262 (* [inline_test] answers the following question:
1263 If we could inline [t] (the user said nothing special),
1266 We expand small terms with at least one non-strict
1267 variable (i.e. a variable that may not be evaluated).
1269 Futhermore we don't expand fixpoints.
1271 Moreover, as mentionned by X. Leroy (bug #2241),
1272 inling a constant from inside an opaque module might
1273 break types. To avoid that, we require below that
1274 both [r] and its body are globally visible. This isn't
1275 fully satisfactory, since [r] might not be visible (functor),
1276 and anyway it might be interesting to inline [r] at least
1277 inside its own structure. But to be safe, we adopt this
1278 restriction for the moment.
1281 let inline_test _r _t =
1282 (*CSC:if not (auto_inline ()) then*) false
1285 let c = match r with ConstRef c -> c | _ -> assert false in
1286 let body = try (Global.lookup_constant c).const_body with _ -> None in
1287 if body = None then false
1289 let t1 = eta_red t in
1290 let t2 = snd (collect_lams t1) in
1291 not (is_fix t2) && ml_size t < 12 && is_not_strict t
1294 (*CSC: (not) reimplemented
1295 let con_of_string s =
1296 let null = empty_dirpath in
1297 match repr_dirpath (dirpath_of_string s) with
1298 | id :: d -> make_con (MPfile (make_dirpath d)) null (label_of_id id)
1299 | [] -> assert false
1301 let manual_inline_set =
1302 List.fold_right (fun x -> Cset_env.add (con_of_string x))
1303 [ "Coq.Init.Wf.well_founded_induction_type";
1304 "Coq.Init.Wf.well_founded_induction";
1305 "Coq.Init.Wf.Acc_iter";
1306 "Coq.Init.Wf.Fix_F";
1308 "Coq.Init.Datatypes.andb";
1309 "Coq.Init.Datatypes.orb";
1310 "Coq.Init.Logic.eq_rec_r";
1311 "Coq.Init.Logic.eq_rect_r";
1312 "Coq.Init.Specif.proj1_sig";
1316 let manual_inline = function (*CSC:
1317 | ConstRef c -> Cset_env.mem c manual_inline_set
1320 (* If the user doesn't say he wants to keep [t], we inline in two cases:
1322 \item the user explicitly requests it
1323 \item [expansion_test] answers that the inlining is a good idea, and
1324 we are free to act (AutoInline is set)
1327 let inline _r _t = false (*CSC: we never inline atm
1328 (*CSC:not (to_keep r) (* The user DOES want to keep it *)
1329 && not (is_inline_custom r)
1330 &&*) (false(*to_inline r*) (* The user DOES want to inline it *)
1331 || (not (is_projection r) &&
1332 (is_recursor r || manual_inline r || inline_test r t)))