diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-28 15:27:19 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-05-28 15:27:19 +0000 |
commit | 8fb775da36bd321428a0a6f9c73cc07dea6295f8 (patch) | |
tree | ab3b427a48b10a38197e1a1aec31fcecbd21b2e4 | |
parent | 283bed9d858ccce2db4dc5cdb946fb8e12619fe7 (diff) |
gestion plus fine des beta-redex lineaires (cf nb_occur_match)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4085 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | contrib/extraction/mlutil.ml | 24 |
1 files changed, 22 insertions, 2 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index b0278b372..fd521a211 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -409,6 +409,26 @@ let nb_occur_k k t = let nb_occur t = nb_occur_k 1 t +(* Number of occurences of [Rel 1] in [t], with special treatment of match: + occurences in different branches aren't added, but we rather use max. *) + +let nb_occur_match = + let rec nb k = function + | MLrel i -> if i = k then 1 else 0 + | MLcase(a,v) -> + Array.fold_left + (fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) (nb k a) v + | MLletin (_,a,b) -> (nb k a) + (nb (k+1) a) + | MLfix (_,ids,v) -> let k = k+(Array.length ids) in + Array.fold_left (fun r a -> r+(nb k a)) 0 v + | MLlam (_,a) -> nb (k+1) a + | MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l + | MLcons (_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l + | MLcast (a,_) -> nb k a + | MLmagic a -> nb k a + | MLglob _ | MLexn _ | MLdummy -> 0 + in nb 1 + (*s Lifting on terms. [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *) @@ -673,7 +693,7 @@ let rec simpl o = function let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in simpl_case o br (simpl o e) | MLletin(id,c,e) when - (id = dummy_name) || (is_atomic c) || (nb_occur e <= 1) -> + (id = dummy_name) || (is_atomic c) || (nb_occur_match e <= 1) -> simpl o (ast_subst c e) | MLfix(i,ids,c) as t when o -> let n = Array.length ids in @@ -687,7 +707,7 @@ and simpl_app o a = function | MLlam (id,t) when id = dummy_name -> simpl o (MLapp (ast_pop t, List.tl a)) | MLlam (id,t) -> (* Beta redex *) - (match nb_occur t with + (match nb_occur_match t with | 0 -> simpl o (MLapp (ast_pop t, List.tl a)) | 1 when o -> simpl o (MLapp (ast_subst (List.hd a) t, List.tl a)) |