diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
| -rw-r--r-- | plugins/extraction/modutil.ml | 44 |
1 files changed, 12 insertions, 32 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 15145344..b4334750 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: modutil.ml 13420 2010-09-16 15:47:08Z letouzey $ i*) open Names open Declarations @@ -217,45 +217,25 @@ let get_decl_in_structure r struc = let dfix_to_mlfix rv av i = let rec make_subst n s = if n < 0 then s - else make_subst (n-1) (Refmap.add rv.(n) (n+1) s) + else make_subst (n-1) (Refmap'.add rv.(n) (n+1) s) in - let s = make_subst (Array.length rv - 1) Refmap.empty + let s = make_subst (Array.length rv - 1) Refmap'.empty in let rec subst n t = match t with | MLglob ((ConstRef kn) as refe) -> - (try MLrel (n + (Refmap.find refe s)) with Not_found -> t) + (try MLrel (n + (Refmap'.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) -let rec optim to_appear s = function - | [] -> [] - | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l -> - if List.mem r to_appear - then d :: (optim to_appear s l) - else optim to_appear s l - | Dterm (r,t,typ) :: l -> - let t = normalize (ast_glob_subst !s t) in - let i = inline r t in - if i then s := Refmap.add r t !s; - if not i || modular () || List.mem r to_appear - then - let d = match optimize_fix t with - | MLfix (0, _, [|c|]) -> - Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|]) - | t -> Dterm (r, t, typ) - in d :: (optim to_appear s l) - else optim to_appear s l - | d :: l -> d :: (optim to_appear s l) - let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> let a = normalize (ast_glob_subst !s a) in let i = inline r a in - if i then s := Refmap.add r a !s; + if i then s := Refmap'.add r a !s; if top && i && not (modular ()) && not (List.mem r to_appear) then optim_se top to_appear s lse else @@ -271,7 +251,7 @@ let rec optim_se top to_appear s = function let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body - then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s + then s := Refmap'.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; if !all && top && not (modular ()) @@ -302,11 +282,11 @@ let base_r = function | _ -> assert false let reset_needed, add_needed, found_needed, is_needed = - let needed = ref Refset.empty in - ((fun l -> needed := Refset.empty), - (fun r -> needed := Refset.add (base_r r) !needed), - (fun r -> needed := Refset.remove (base_r r) !needed), - (fun r -> Refset.mem (base_r r) !needed)) + let needed = ref Refset'.empty in + ((fun l -> needed := Refset'.empty), + (fun r -> needed := Refset'.add (base_r r) !needed), + (fun r -> needed := Refset'.remove (base_r r) !needed), + (fun r -> Refset'.mem (base_r r) !needed)) let declared_refs = function | Dind (kn,_) -> [|IndRef (mind_of_kn kn,0)|] @@ -361,7 +341,7 @@ let check_implicits = function | _ -> false let optimize_struct to_appear struc = - let subst = ref (Refmap.empty : ml_ast Refmap.t) in + let subst = ref (Refmap'.empty : ml_ast Refmap'.t) in let opt_struc = List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc in |