diff options
Diffstat (limited to 'plugins/extraction/modutil.ml')
-rw-r--r-- | plugins/extraction/modutil.ml | 61 |
1 files changed, 35 insertions, 26 deletions
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 2c923241..8158ac64 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -1,27 +1,25 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) open Names -open Declarations -open Environ -open Libnames +open Globnames +open Errors open Util open Miniml open Table open Mlutil -open Mod_subst (*S Functions upon ML modules. *) let rec msid_of_mt = function | MTident mp -> mp | MTwith(mt,_)-> msid_of_mt mt - | _ -> anomaly "Extraction:the With operator isn't applied to a name" + | _ -> anomaly ~label:"extraction" (Pp.str "the With operator isn't applied to a name") (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -32,16 +30,16 @@ let se_iter do_decl do_spec do_mp = | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' | MTwith (mt,ML_With_type(idl,l,t))-> let mp_mt = msid_of_mt mt in - let l',idl' = list_sep_last idl in + let l',idl' = List.sep_last idl in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl' + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl' in - let r = ConstRef (make_con mp_w empty_dirpath (label_of_id l')) in + let r = ConstRef (Constant.make2 mp_w (Label.of_id l')) in mt_iter mt; do_decl (Dtype(r,l,t)) | MTwith (mt,ML_With_module(idl,mp))-> let mp_mt = msid_of_mt mt in let mp_w = - List.fold_left (fun mp l -> MPdot(mp,label_of_id l)) mp_mt idl + List.fold_left (fun mp l -> MPdot(mp,Label.of_id l)) mp_mt idl in mt_iter mt; do_mp mp_w; do_mp mp | MTsig (_, sign) -> List.iter spec_iter sign @@ -110,13 +108,13 @@ let ind_iter_references do_term do_cons do_type kn ind = let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in let packet_iter ip p = do_type (IndRef ip); - if lang () = Ocaml then + if lang () == Ocaml then (match ind.ind_equiv with | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip)); | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in - if lang () = Ocaml then record_iter_references do_term ind.ind_kind; + if lang () == Ocaml then record_iter_references do_term ind.ind_kind; Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets let decl_iter_references do_term do_cons do_type = @@ -199,6 +197,11 @@ let rec msig_of_ms = function let signature_of_structure s = List.map (fun (mp,ms) -> mp,msig_of_ms ms) s +let rec mtyp_of_mexpr = function + | MEfunctor (id,ty,e) -> MTfunsig (id,ty, mtyp_of_mexpr e) + | MEstruct (mp,str) -> MTsig (mp, msig_of_ms str) + | _ -> assert false + (*s Searching one [ml_decl] in a [ml_structure] by its [global_reference] *) @@ -208,18 +211,18 @@ let is_modular = function let rec search_structure l m = function | [] -> raise Not_found - | (lab,d)::_ when lab=l && is_modular d = m -> d + | (lab,d)::_ when Label.equal lab l && (is_modular d : bool) == m -> d | _::fields -> search_structure l m fields let get_decl_in_structure r struc = try let base_mp,ll = labels_of_ref r in if not (at_toplevel base_mp) then error_not_visible r; - let sel = List.assoc base_mp struc in + let sel = List.assoc_f ModPath.equal base_mp struc in let rec go ll sel = match ll with | [] -> assert false | l :: ll -> - match search_structure l (ll<>[]) sel with + match search_structure l (not (List.is_empty ll)) sel with | SEdecl d -> d | SEmodtype m -> assert false | SEmodule m -> @@ -228,7 +231,7 @@ let get_decl_in_structure r struc = | _ -> error_not_visible r in go ll sel with Not_found -> - anomaly "reference not found in extracted structure" + anomaly (Pp.str "reference not found in extracted structure") (*s Optimization of a [ml_structure]. *) @@ -251,7 +254,7 @@ let dfix_to_mlfix rv av i = (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 ids = Array.map (fun r -> Label.to_id (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) @@ -297,8 +300,6 @@ and optim_me to_appear s = function For non-library extraction, we recompute a minimal set of dependencies for first-level definitions (no module pruning yet). *) -exception NoDepCheck - let base_r = function | ConstRef c as r -> r | IndRef (kn,_) -> IndRef (kn,0) @@ -353,7 +354,7 @@ let rec depcheck_se = function let se' = depcheck_se se in let refs = declared_refs d in let refs' = List.filter is_needed refs in - if refs' = [] then + if List.is_empty refs' then (List.iter remove_info_axiom refs; List.iter remove_opaque refs; se') @@ -362,7 +363,7 @@ let rec depcheck_se = function (* Hack to avoid extracting unused part of a Dfix *) match d with | Dfix (rv,trms,tys) when (List.for_all is_custom refs') -> - let trms' = Array.create (Array.length rv) (MLexn "UNUSED") in + let trms' = Array.make (Array.length rv) (MLexn "UNUSED") in ((l,SEdecl (Dfix (rv,trms',tys))) :: se') | _ -> (compute_deps_decl d; t::se') end @@ -376,14 +377,22 @@ let rec depcheck_struct = function | (mp,lse)::struc -> let struc' = depcheck_struct struc in let lse' = depcheck_se lse in - if lse' = [] then struc' else (mp,lse')::struc' + if List.is_empty lse' then struc' else (mp,lse')::struc' + +let is_prefix pre s = + let len = String.length pre in + let rec is_prefix_aux i = + if Int.equal i len then true + else pre.[i] == s.[i] && is_prefix_aux (succ i) + in + is_prefix_aux 0 let check_implicits = function | MLexn s -> - if String.length s > 8 && (s.[0] = 'U' || s.[0] = 'I') then + if String.length s > 8 && (s.[0] == 'U' || s.[0] == 'I') then begin - if String.sub s 0 7 = "UNBOUND" then assert false; - if String.sub s 0 8 = "IMPLICIT" then + if is_prefix "UNBOUND" s then assert false; + if is_prefix "IMPLICIT" s then error_non_implicit (String.sub s 9 (String.length s - 9)); end; false @@ -397,7 +406,7 @@ let optimize_struct to_appear struc = in ignore (struct_ast_search check_implicits opt_struc); if library () then - List.filter (fun (_,lse) -> lse<>[]) opt_struc + List.filter (fun (_,lse) -> not (List.is_empty lse)) opt_struc else begin reset_needed (); List.iter add_needed (fst to_appear); |