aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorfilliatr2001-03-30 09:37:34 +0000
committerfilliatr2001-03-30 09:37:34 +0000
commit6c54cdf3dd31796c658e6854d50bcaa4bc6a140d (patch)
treee5ef00d2412079a38802e523cd59646f820e01af
parent02d7ec75988e2cd13ebf233b364e400309c605a3 (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.ml4
-rw-r--r--contrib/extraction/mlutil.ml72
-rw-r--r--contrib/extraction/mlutil.mli6
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