diff options
author | 2001-11-02 23:51:55 +0000 | |
---|---|---|
committer | 2001-11-02 23:51:55 +0000 | |
commit | c3ff17ba405beb26b1c865719d86e7e364a45cae (patch) | |
tree | 1833b324fdd55912da3f215286c57a39be24f977 /contrib/extraction | |
parent | 86188a92fb1e3db08ede1a17bcdb1d0b9c3a0c57 (diff) |
suite des modifs concernant les optimisations divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2151 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/extraction.ml | 6 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 4 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 172 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 13 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 44 |
5 files changed, 124 insertions, 115 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 23264fb07..974a47a59 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -244,10 +244,6 @@ let decompose_lam_eta n env c = let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in (rb, e) -let rec abstract_n n a = - if n = 0 then a else MLlam (anonymous, ml_lift 1 (abstract_n (n-1) a)) - - (*s Error message when extraction ends on an axiom. *) @@ -573,7 +569,7 @@ and abstract_constructor cp = | (_,Arity) :: l -> abstract rels i l in - abstract_n n (abstract [] 1 s) + anonym_lams (ml_lift n (abstract [] 1 s)) n (* Extraction of a case *) diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 28c0612c9..f3d64fcee 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -103,7 +103,7 @@ let rec pp_expr par env args = let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f | MLlam _ as a -> - let fl,a' = collect_lambda a in + let fl,a' = collect_lams a in let fl,env' = push_vars fl env in let st = [< pp_abst (List.rev fl); pp_expr false env' [] a' >] in if args = [] then @@ -194,7 +194,7 @@ and pp_fix par env in_p (ids,bl) args = close_par par >] and pp_function env f t = - let bl,t' = collect_lambda t in + let bl,t' = collect_lams t in let bl,env' = push_vars bl env in [< f; pr_binding (List.rev bl); 'sTR " ="; 'fNL; 'sTR " "; diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index b047b1003..27c971c65 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -81,8 +81,8 @@ let rec occurs_itvl k k' = function | MLcase(t,pv) -> (occurs_itvl k k' t) || (array_exists - (fun (_,l,t') -> - let n = List.length l in occurs_itvl (k + n) (k' + n) t') pv) + (fun (_,l,t') -> + let n = List.length l in occurs_itvl (k + n) (k' + n) t') pv) | MLfix(_,l,cl) -> let n = Array.length l in occurs_itvl_vect (k + n) (k' + n) cl | MLcast(t,_) -> occurs_itvl k k' t @@ -119,14 +119,14 @@ 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,pv) -> MLcase (liftrec n t, Array.map (fun (id,idl,p) -> let k = List.length idl in - (id, idl, liftrec (n+k) p)) pl) - | MLfix (n0,idl,pl) -> + (id, idl, liftrec (k+n) p)) pv) + | MLfix (n0,idl,pv) -> MLfix (n0,idl, - let k = Array.length idl in Array.map (liftrec (n+k)) pl) + let k = Array.length idl in Array.map (liftrec (k+n)) pv) | a -> ast_map (liftrec n) a in if k = 0 then c else liftrec n c @@ -196,6 +196,48 @@ let nb_occur a = in count 1 a; !cpt +(*s The two following functions test and create [MLrel n;...;MLrel 1] *) + +let rec test_eta_args n = function + | [] -> n=0 + | a :: q -> (a = (MLrel n)) && (test_eta_args (pred n) q) + +let rec make_eta_args n = + if n = 0 then [] else (MLrel n)::(make_eta_args (pred n)) + +(*s [generalize_check k k' i] return true if there is a [(Rel j)] + in [t] with [k<=i<=k'] *) + +exception Impossible + +let check_and_generalize (r0,l,c) = + let nargs = List.length l in + let rec genrec k k' = function + | MLrel i as c -> + if i<k then c + else if i>k' then MLrel (i-nargs+1) + else raise Impossible + | MLcons(r,args) when r=r0 -> + if (test_eta_args nargs args) then MLrel k + else raise Impossible + | MLlam(id,t) -> MLlam(id,genrec (k + 1) (k' + 1) t) + | MLletin(id,t,t') -> MLletin(id,(genrec k k' t),(genrec (k+1) (k'+1) t')) + | MLcase(t,pv) -> + MLcase(genrec k k' t, + Array.map (fun (id,idl,t') -> + let n = List.length idl in + (id,idl,genrec (k+n) (k'+n) t')) pv) + | MLfix(n0,idl,pv) -> + MLfix(n0,idl, + let n = Array.length idl in Array.map (genrec (k+n) (k'+n)) pv) + | a -> ast_map (genrec k k') a + in genrec 1 nargs c + +let check_case br = + let f = check_and_generalize br.(0) in + for i = 1 to Array.length br - 1 do + if check_and_generalize br.(i) <> f then raise Impossible + done; f (*s Some Beta-iota reductions + simplifications*) @@ -207,38 +249,6 @@ let is_atomic = function | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity -> true | _ -> false -exception Impossible - -let check_identity_case br = - let rec check_list k = function - | [] -> () - | t :: q -> - if t <> MLrel k then raise Impossible; - check_list (k-1) q - in - let check_one_branch (r,l,t) = - match t with - | MLcons (r',l') -> - if r<>r' then raise Impossible; - check_list (List.length l) l' - | _ -> raise Impossible - in - Array.iter check_one_branch br - - -let check_constant_case br = - let (_,l,t) = br.(0) in - let n = List.length l in - if occurs_itvl 1 n t then raise Impossible; - let cst = ml_lift (-n) t in - for i = 1 to Array.length br - 1 do - let (_,l,t) = br.(i) in - let n = List.length l in - if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) - then raise Impossible - done; cst - - let all_constr br = try Array.iter @@ -250,7 +260,6 @@ let all_constr br = true with Impossible -> false - let normalize a = let o = optim() in let rec simplify = function @@ -308,10 +317,10 @@ let normalize a = | e' -> let br' = Array.map (fun (n,l,t) -> (n,l,simplify t)) br in if o then - try check_identity_case br'; e' - with Impossible -> - try check_constant_case br' - with Impossible -> MLcase (e', br') + try + let f = check_case br' in + simplify (MLapp (MLlam (anonymous,f),[e'])) + with Impossible -> MLcase (e', br') else MLcase (e', br')) | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> (* expansion of a letin in special cases *) @@ -325,72 +334,65 @@ let normalize a = ast_map simplify a in simplify (merge_app a) -(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns +let normalize_decl = function + | Dglob (id, a) -> Dglob (id, normalize a) + | d -> d + +(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns the list [idn;...;id1] and the term [t]. *) -let collect_lambda = +let collect_lams = let rec collect acc = function | MLlam(id,t) -> collect (id::acc) t | x -> acc,x in collect [] -let rec pass_n_lambda n = function - | MLlam(_,t)-> pass_n_lambda (n-1) t - | _ -> raise Impossible +(* [named_abstract] does the converse of [collect_lambda] *) -let rec test_eta n = function - | [] -> n=0 - | a :: q -> (a = (MLrel n)) && (test_eta (pred n) q) - -let rec make_args n = - if n = 0 then [] else (MLrel n)::(make_args (pred n)) - -(* this abstract is written without lift on purpose *) -let rec abstract ids a = match ids with +let rec named_lams a = function | [] -> a - | id :: l -> abstract l (MLlam(id,a)) + | id :: ids -> named_lams (MLlam(id,a)) ids + +let rec anonym_lams a = function + | 0 -> a + | n -> anonym_lams (MLlam(anonymous,a)) (pred n) + +(*s special treatment of non-mutual fixpoint for pretty-printing purpose *) let optimize_fix a = if not (optim()) then a else - let lams,b = collect_lambda a in - let n = List.length lams in + let ids,a' = collect_lams a in + let n = List.length ids in if n = 0 then a else - (match b with + (match a' with | MLfix(_,[|f|],[|c|]) -> - let new_f = MLapp (MLrel (n+1),make_args n) in - let new_c = abstract lams (ml_subst new_f c) + let new_f = MLapp (MLrel (n+1),make_eta_args n) in + let new_c = named_lams (ml_subst new_f c) ids in MLfix(0,[|f|],[|new_c|]) - | MLapp(b,ids) -> - (match b with - | MLfix(_,[|_|],[|_|]) when (test_eta n ids)-> b - | MLfix(_,[|f|],[|c|]) -> a -(* TODO: tenir compte des occurrences des ids + | MLapp(a',args) -> + (match a' with + | MLfix(_,[|_|],[|_|]) when (test_eta_args n args)-> a' + | MLfix(_,[|f|],[|c|]) -> (try + let m = List.length args in let v = Array.make n 0 in - let m = List.length ids in - list_iter_i (fun i t -> - (match t with - MLrel j when v.(j-1)=0 -> v.(j-1)<-(succ i) - | _ -> raise Impossible)) ids; - let args = array_fold_left_i - (fun i accum j -> - let r = if j=0 then (succ i)+m else j - in (MLrel r) :: accum) [] v in - let new_f = - abstract (List.map (fun _ ->anonymous) ids) - (MLapp (MLrel (m+n+1),args)) in - let new_c = abstract lams (normalize (ml_subst new_f c)) + for i=0 to (n-1) do v.(i)<-i done; + let aux i = function + MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1) + | _ -> raise Impossible + in + list_iter_i aux args; + let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in + let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in + let new_c = named_lams (normalize (MLapp ((ml_subst new_f c),args))) ids in MLfix(0,[|f|],[|new_c|]) with Impossible -> a) -*) | _ -> a) + | _ -> a) | _ -> a) -let normalize_decl = function - | Dglob (id, a) -> Dglob (id, normalize a) - | d -> d (*s Utility functions used for the decision of expansion *) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index 2c5a586ac..3771151b4 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -42,15 +42,22 @@ val ml_subst : ml_ast -> ml_ast -> ml_ast val subst_glob_ast : global_reference -> ml_ast -> ml_ast -> ml_ast (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns - the list [id1;...;idn] and the term [t]. *) + the list [idn;...;id1] and the term [t]. *) + +val collect_lams : ml_ast -> identifier list * ml_ast + +(* [named_abstract] is the converse of [collect_lambda]. *) + +val named_lams : ml_ast -> identifier list -> ml_ast + +val anonym_lams : ml_ast -> int -> ml_ast -val collect_lambda : ml_ast -> identifier list * ml_ast (*s Some transformations of ML terms. [normalize] and [normalize_decl] reduce all beta redexes (when the argument does not occur, it is just thrown away; when it occurs exactly once it is substituted; otherwise a let in redex is created for clarity) and iota redexes, plus some other - optimizations. *) + optimizations. *) (* TO UPDATE *) val normalize : ml_ast -> ml_ast val normalize_decl : ml_decl -> ml_decl diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 1a7d151fb..4470e00ac 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -158,6 +158,7 @@ let expr_needs_par = function | _ -> false let rec pp_expr par env args = + let par' = args <> [] || par in let apply st = match args with | [] -> st | _ -> hOV 2 [< open_par par; st; 'sPC; @@ -171,16 +172,12 @@ let rec pp_expr par env args = let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f | MLlam _ as a -> - let fl,a' = collect_lambda a in + let fl,a' = collect_lams a in let fl,env' = push_vars fl env in let st = [< pp_abst (List.rev fl); pp_expr false env' [] a' >] in - if args = [] then - [< open_par par; st; close_par par >] - else - apply [< 'sTR "("; st; 'sTR ")" >] + [< open_par par'; st; close_par par' >] | MLletin (id,a1,a2) -> let id',env' = push_vars [id] env in - let par' = par || args <> [] in let par2 = not par' && expr_needs_par a2 in apply (hOV 0 [< open_par par'; @@ -199,12 +196,20 @@ let rec pp_expr par env args = | MLcons (r,args') -> [< open_par par; pp_global r; 'sPC; pp_tuple (pp_expr true env []) args'; close_par par >] + | MLcase (t,[|x|])-> + apply + (hOV 0 [< open_par par'; 'sTR "let "; + pp_one_pat + [< 'sTR " ="; 'sPC; + pp_expr false env [] t; 'sPC; 'sTR "in" >] + env x; + close_par par' >]) | MLcase (t, pv) -> apply - [< if args <> [] then [< 'sTR "(" >] else open_par par; + [< open_par par'; v 0 [< 'sTR "match "; pp_expr false env [] t; 'sTR " with"; 'fNL; 'sTR " "; pp_pat env pv >]; - if args <> [] then [< 'sTR ")" >] else close_par par >] + close_par par' >] | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args @@ -222,18 +227,17 @@ let rec pp_expr par env args = [< open_par true; 'sTR "Obj.magic"; 'sPC; pp_expr false env args a; close_par true >] +and pp_one_pat s env (r,ids,t) = + let ids,env' = push_vars (List.rev ids) env in + let par = expr_needs_par t in + [< pp_global r; + if ids = [] then [< >] + else [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >]; + s; 'sPC; pp_expr par env' [] t >] + and pp_pat env pv = - let pp_one_pat (name,ids,t) = - let ids,env' = push_vars (List.rev ids) env in - let par = expr_needs_par t in - hOV 2 [< pp_global name; - begin match ids with - | [] -> [< >] - | _ -> [< 'sTR " "; pp_boxed_tuple pr_id (List.rev ids) >] - end; - 'sTR " ->"; 'sPC; pp_expr par env' [] t >] - in - [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) pp_one_pat pv >] + [< prvect_with_sep (fun () -> [< 'fNL; 'sTR "| " >]) + (fun x -> hOV 2 (pp_one_pat (string " ->") env x)) pv >] (*s names of the functions ([ids]) are already pushed in [env], and passed here just for convenience. *) @@ -260,7 +264,7 @@ and pp_fix par env in_p (ids,bl) args = close_par par >] and pp_function env f t = - let bl,t' = collect_lambda t in + let bl,t' = collect_lams t in let bl,env' = push_vars bl env in let is_function pv = let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in |