diff options
| author | filliatr | 2001-03-30 09:37:34 +0000 |
|---|---|---|
| committer | filliatr | 2001-03-30 09:37:34 +0000 |
| commit | 6c54cdf3dd31796c658e6854d50bcaa4bc6a140d (patch) | |
| tree | e5ef00d2412079a38802e523cd59646f820e01af | |
| parent | 02d7ec75988e2cd13ebf233b364e400309c605a3 (diff) | |
beta-reduction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1502 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/extract_env.ml | 4 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 72 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.mli | 6 |
3 files changed, 79 insertions, 3 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 3cfee3a9bb..fa0ed72705 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -134,8 +134,8 @@ end module Pp = Ocaml.Make(ToplevelParams) -let pp_ast a = Pp.pp_ast (uncurrify_ast a) -let pp_decl d = Pp.pp_decl (uncurrify_decl d) +let pp_ast a = Pp.pp_ast (betared_ast (uncurrify_ast a)) +let pp_decl d = Pp.pp_decl (betared_decl (uncurrify_decl d)) open Vernacinterp diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 09683eb77e..06625a302a 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -44,7 +44,7 @@ let ml_liftn k n c = | MLrel i as c -> if i < n then c else MLrel (i+k) | MLlam (id,t) -> MLlam (id, liftrec (n+1) t) | MLletin (id,a,b) -> MLletin (id, liftrec n a, liftrec (n+1) b) - | MLcase(t,pl) -> + | MLcase (t,pl) -> MLcase (liftrec n t, Array.map (fun (id,idl,p) -> let k = List.length idl in @@ -60,6 +60,76 @@ let ml_lift k c = ml_liftn k 1 c let pop c = ml_lift (-1) c +(*s substitution *) + +let rec ml_subst v = + let rec subst n m = function + | MLrel i -> + if i = n then + m + else + if i < n then MLrel i else MLrel (i-1) + | MLlam (id,t) -> + MLlam (id, subst (n+1) (ml_lift 1 m) t) + | MLletin (id,a,b) -> + MLletin (id, subst n m a, subst (n+1) (ml_lift 1 m) b) + | MLcase (t,pv) -> + MLcase (subst n m t, + Array.map (fun (id,ids,t) -> + let k = List.length ids in + (id,ids,subst (n+k) (ml_lift k m) t)) + pv) + | MLfix (i,ids,cl) -> + MLfix (i,ids, + let k = List.length ids in + List.map (subst (n+k) (ml_lift k m)) cl) + | a -> ast_map (subst n m) a + in + subst 1 v + +(*s Number of occurences of [Rel 1] in [a] *) + +let nb_occur a = + let cpt = ref 0 in + let rec count n = function + | MLrel i -> if i = n then incr cpt + | MLlam (id,t) -> count (n+1) t + | MLletin (id,a,b) -> count n a; count (n+1) b + | MLcase (t,pv) -> + count n t; + Array.iter (fun (_,l,t) -> let k = List.length l in count (n+k) t) pv + | MLfix (_,ids,cl) -> + let k = List.length ids in List.iter (count (n+k)) cl + | MLapp (a,l) -> count n a; List.iter (count n) l + | MLcons (_,_,l) -> List.iter (count n) l + | MLmagic a -> count n a + | MLcast (a,_) -> count n a + | MLprop | MLexn _ | MLglob _ | MLarity -> () + in + count 1 a; !cpt + +(*s Beta-reduction *) + +let rec betared_ast = function + | MLapp (f, []) -> + betared_ast f + | MLapp (f, a) -> + let f' = betared_ast f + and a' = List.map betared_ast a in + (match f' with + | MLlam (id,t) -> + (match nb_occur t with + | 0 -> betared_ast (MLapp (ml_lift 1 t, List.tl a')) + | 1 -> betared_ast (MLapp (ml_subst (List.hd a') t,List.tl a')) + | _ -> MLapp (f',a')) + | _ -> + MLapp (f',a')) + | a -> ast_map betared_ast a + +let betared_decl = function + | Dglob (id, a) -> Dglob (id, betared_ast a) + | d -> d + (*s [uncurrify] uncurrifies the applications of constructors *) let rec is_constructor_app = function diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index a8a3f470b3..3bbe8f8a3c 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -7,5 +7,11 @@ val occurs : int -> ml_ast -> bool val ml_lift : int -> ml_ast -> ml_ast +(* [ml_subst e t] substitutes [e] for [Rel 1] in [t] *) +val ml_subst : ml_ast -> ml_ast -> ml_ast + +val betared_ast : ml_ast -> ml_ast +val betared_decl : ml_decl -> ml_decl + val uncurrify_ast : ml_ast -> ml_ast val uncurrify_decl : ml_decl -> ml_decl |
