diff options
-rw-r--r-- | plugins/extraction/common.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/common.mli | 1 | ||||
-rw-r--r-- | plugins/extraction/extraction.ml | 10 | ||||
-rw-r--r-- | plugins/extraction/haskell.ml | 2 | ||||
-rw-r--r-- | plugins/extraction/mlutil.ml | 27 | ||||
-rw-r--r-- | plugins/extraction/mlutil.mli | 1 | ||||
-rw-r--r-- | plugins/extraction/table.ml | 15 | ||||
-rw-r--r-- | plugins/extraction/table.mli | 2 |
8 files changed, 0 insertions, 60 deletions
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 35d7ba3d5..61e2f8c28 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -45,8 +45,6 @@ let fnl2 () = fnl () ++ fnl () let space_if = function true -> str " " | false -> mt () -let sec_space_if = function true -> spc () | false -> mt () - let is_digit = function | '0'..'9' -> true | _ -> false diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index e85201982..0abb47c22 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -14,7 +14,6 @@ open Pp val fnl2 : unit -> std_ppcmds val space_if : bool -> std_ppcmds -val sec_space_if : bool -> std_ppcmds val pp_par : bool -> std_ppcmds -> std_ppcmds val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index ba7fc272a..1e2793aa5 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -38,8 +38,6 @@ let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) -let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None - (*S Generation of flags and signatures. *) (* The type [flag] gives us information about any Coq term: @@ -272,14 +270,6 @@ let rec extract_type env db j c args = | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false -(* [extract_maybe_type] calls [extract_type] when used on a Coq type, - and otherwise returns [Tdummy] or [Tunknown] *) - -and extract_maybe_type env db c = - let t = whd_betadeltaiota env none (type_of env c) in - if isSort t then extract_type env db 0 c [] - else if sort_of env t = InProp then Tdummy Kother else Tunknown - (*s Auxiliary function dealing with type application. Precondition: [r] is a type scheme represented by the signature [s], and is completely applied: [List.length args = List.length s]. *) diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 3048db4b7..3d18431aa 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -281,8 +281,6 @@ let rec pp_ind first kn i ind = (*s Pretty-printing of a declaration. *) -let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") - let pp_decl = function | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton (mind_of_kn kn) i.ind_packets.(0) ++ fnl () diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index e8f852266..29f9a817d 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -54,18 +54,6 @@ let new_meta _ = incr meta_count; Tmeta {id = !meta_count; contents = None} -(*s Sustitution of [Tvar i] by [t] in a ML type. *) - -let type_subst i t0 t = - let rec subst t = match t with - | Tvar j when i = j -> t0 - | Tmeta {contents=None} -> t - | Tmeta {contents=Some u} -> subst u - | Tarr (a,b) -> Tarr (subst a, subst b) - | Tglob (r, l) -> Tglob (r, List.map subst l) - | a -> a - in subst t - (* Simultaneous substitution of [[Tvar 1; ... ; Tvar n]] by [l] in a ML type. *) let type_subst_list l t = @@ -441,15 +429,6 @@ let ast_occurs_itvl k k' t = ast_iter_rel (fun i -> if (k <= i) && (i <= k') then raise Found) t; false with Found -> true -(*s Number of occurences of [Rel k] (resp. [Rel 1]) in [t]. *) - -let nb_occur_k k t = - let cpt = ref 0 in - ast_iter_rel (fun i -> if i = k then incr cpt) t; - !cpt - -let nb_occur t = nb_occur_k 1 t - (* Number of occurences of [Rel 1] in [t], with special treatment of match: occurences in different branches aren't added, but we rather use max. *) @@ -572,7 +551,6 @@ let rec many_lams id a = function | 0 -> a | n -> many_lams id (MLlam (id,a)) (pred n) -let anonym_lams a n = many_lams anonymous a n let anonym_tmp_lams a n = many_lams (Tmp anonymous_name) a n let dummy_lams a n = many_lams Dummy a n @@ -1144,11 +1122,6 @@ and ml_size_array l = Array.fold_left (fun a t -> a + ml_size t) 0 l let is_fix = function MLfix _ -> true | _ -> false -let rec is_constr = function - | MLcons _ -> true - | MLlam(_,t) -> is_constr t - | _ -> false - (*s Strictness *) (* A variable is strict if the evaluation of the whole term implies diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 022e42fdd..b4f3c4c18 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -18,7 +18,6 @@ open Table val reset_meta_count : unit -> unit val new_meta : 'a -> ml_type -val type_subst : int -> ml_type -> ml_type -> ml_type val type_subst_list : ml_type list -> ml_type -> ml_type val type_subst_vect : ml_type array -> ml_type -> ml_type diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index a292dec2f..c1b488f35 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -58,11 +58,6 @@ let raw_string_of_modfile = function | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) | _ -> assert false -let rec modfile_of_mp = function - | (MPfile _) as mp -> mp - | MPdot (mp,_) -> modfile_of_mp mp - | _ -> raise Not_found - let current_toplevel () = fst (Lib.current_prefix ()) let is_toplevel mp = @@ -96,12 +91,6 @@ let common_prefix_from_list mp0 mpl = | mp :: l -> if MPset.mem mp prefixes then Some mp else f l in f mpl -let rec parse_labels ll = function - | MPdot (mp,l) -> parse_labels (l::ll) mp - | mp -> mp,ll - -let labels_of_mp mp = parse_labels [] mp - let rec parse_labels2 ll mp1 = function | mp when mp1=mp -> mp,ll | MPdot (mp,l) -> parse_labels2 (l::ll) mp1 mp @@ -112,10 +101,6 @@ let labels_of_ref r = let mp,_,l = repr_of_r r in parse_labels2 [l] mp_top mp -let rec add_labels_mp mp = function - | [] -> mp - | l :: ll -> add_labels_mp (MPdot (mp,l)) ll - (*S The main tables: constants, inductives, records, ... *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index a0cffa596..f55ae53d8 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -56,10 +56,8 @@ val at_toplevel : module_path -> bool val visible_con : constant -> bool val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t -val modfile_of_mp : module_path -> module_path val common_prefix_from_list : module_path -> module_path list -> module_path option -val add_labels_mp : module_path -> label list -> module_path val get_nth_label_mp : int -> module_path -> label val labels_of_ref : global_reference -> module_path * label list |