diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-05 17:20:10 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-11-05 17:20:10 +0000 |
commit | 2e6751cdfb0c25274cf789078438df8579b46f7e (patch) | |
tree | 9274f1d2a966e64b7ae75dbe0b418602bb9314bc /contrib/extraction | |
parent | 5638b67d02ddc1fb963646d8229c93f3bba196ee (diff) |
optimisation consistant a parfois permuter case et fun
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2161 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/mlutil.ml | 112 |
1 files changed, 89 insertions, 23 deletions
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 00da8e84b..c4517cd60 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -197,6 +197,45 @@ let nb_occur a = in count 1 a; !cpt +(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns + the list [idn;...;id1] and the term [t]. *) + +let collect_lams = + let rec collect acc = function + | MLlam(id,t) -> collect (id::acc) t + | x -> acc,x + in + collect [] + +let collect_n_lams = + let rec collect acc n t = + if n = 0 then acc,t + else match t with + | MLlam(id,t) -> collect (id::acc) (n-1) t + | _ -> assert false + in + collect [] + +let rec remove_n_lams n t = + if n = 0 then t + else match t with + | MLlam(id,t) -> remove_n_lams (n-1) t + | _ -> assert false + +let rec nb_lam = function + | MLlam(id,t) -> succ (nb_lam t) + | _ -> 0 + +(* [named_abstract] does the converse of [collect_lambda] *) + +let rec named_lams a = function + | [] -> 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 The two following functions test and create [MLrel n;...;MLrel 1] *) let rec test_eta_args n = function @@ -219,7 +258,7 @@ let check_and_generalize (r0,l,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 + 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')) @@ -253,6 +292,42 @@ let check_constant_case br = then raise Impossible done; cst +(* [permut_rels n n' c] translates [Rel 1 ... Rel n] to [Rel (n'+1) ... Rel (n'+n)] + and [Rel (n+1) ... Rel (n+n')] to [Rel 1 ... Rel n'] *) + +let permut_rels n n' = + let rec permut k = function + | MLrel i as c -> + if i<k || i>=k+n+n' then c + else if i<n+k then MLrel (i+n') + else MLrel (i-n) + | MLlam (id,t) -> MLlam (id, permut (k+1) t) + | MLletin (id,a,b) -> MLletin (id, permut k a, permut (k+1) b) + | MLcase (t,pv) -> + MLcase (permut k t, + Array.map (fun (id,idl,p) -> + let nl = List.length idl in + (id, idl, permut (k+nl) p)) pv) + | MLfix (n0,idl,pv) -> + MLfix (n0,idl, + let nl = Array.length idl in Array.map (permut (k+nl)) pv) + | a -> ast_map (permut k) a + in + permut 1 + +let rec permut_case_fun br acc = + let (_,_,t0) = br.(0) in + let nb = ref (nb_lam t0) in + Array.iter (fun (_,_,t) -> let n = nb_lam t in if n < !nb then nb:=n) br; + let ids,_ = collect_n_lams !nb t0 + in + for i = 0 to Array.length br - 1 do + let (r,l,t) = br.(i) in + let t = permut_rels !nb (List.length l) (remove_n_lams !nb t) + in br.(i) <- (r,l,t) + done; + ids + (*s Some Beta-iota reductions + simplifications*) let constructor_index = function @@ -336,7 +411,18 @@ let normalize a = simplify (MLapp (MLlam (anonymous,f),[e'])) with Impossible -> try check_constant_case br' - with Impossible -> MLcase (e', br') + with Impossible -> + (match e' with + | MLrel i -> + let ids = permut_case_fun br' [] in + let ids = List.map + (fun id -> + if id = prop_name then anonymous + else id) ids in + let n = List.length ids in + if n = 0 then MLcase (e', br') + else named_lams (MLcase (MLrel (i+n), br')) ids + | _ -> 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 *) @@ -354,26 +440,6 @@ 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_lams = - let rec collect acc = function - | MLlam(id,t) -> collect (id::acc) t - | x -> acc,x - in - collect [] - -(* [named_abstract] does the converse of [collect_lambda] *) - -let rec named_lams a = function - | [] -> 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 = @@ -597,7 +663,7 @@ let rec optimize prm = function end else l in if (prm.mod_name <> None) || List.mem r prm.to_appear || not b then - let t = optimize_fix t in + let t = optimize_fix t in Dglob (r,t) :: (optimize prm l) else optimize prm l |