diff options
Diffstat (limited to 'contrib/extraction')
28 files changed, 1553 insertions, 1529 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 8e441613..346201ec 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*) +(*i $Id: common.ml 8930 2006-06-09 02:14:34Z letouzey $ i*) open Pp open Util @@ -112,7 +112,8 @@ let contents_first_level mp = | Extraction.Term -> add false (id_of_label l)) | (_, SPBmind mib) -> Array.iter - (fun mip -> if mip.mind_sort <> (Prop Null) then begin + (fun mip -> if snd (Inductive.mind_arity mip) <> InProp + then begin add upper_type mip.mind_typename; Array.iter (add true) mip.mind_consnames end) @@ -143,7 +144,7 @@ let create_modular_renamings struc = in (* 1) creates renamings of objects *) let add upper r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let l = mp_create_modular_renamings mp in let s = modular_rename upper (id_of_global r) in global_ids := Idset.add (id_of_string s) !global_ids; @@ -184,7 +185,7 @@ let create_modular_renamings struc = List.iter contents_first_level used_modules; let used_modules' = List.rev used_modules in let needs_qualify r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in if (is_modfile mp) && mp <> current_module && (clash mp [] (List.hd (get_renamings r)) used_modules') then to_qualify := Refset.add r !to_qualify @@ -239,7 +240,7 @@ let rec mp_create_mono_renamings mp = let create_mono_renamings struc = let { up = u ; down = d } = struct_get_references_list struc in let add upper r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let l = mp_create_mono_renamings mp in let mycase = if upper then uppercase_id else lowercase_id in let id = @@ -267,8 +268,6 @@ module StdParams = struct let globals () = !global_ids - (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *) - let unquote s = if lang () <> Scheme then s else @@ -285,26 +284,34 @@ module StdParams = struct let pp_global mpl r = let ls = get_renamings r in let s = List.hd ls in - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let ls = if mp = List.hd mpl then [s] (* simpliest situation *) - else - try (* has [mp] something in common with one of those in [mpl] ? *) - let pref = common_prefix_from_list mp mpl in - (*i TODO: possibilité de clash i*) - list_firstn ((mp_length mp)-(mp_length pref)+1) ls - with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base = base_mp mp in - if !modular && - (at_toplevel mp) && - not (Refset.mem r !to_qualify) && - not (clash base [] s mpl) - then snd (list_sep_last ls) - else ls + else match lang () with + | Scheme -> [s] (* no modular Scheme extraction... *) + | Toplevel -> [s] (* idem *) + | Haskell -> + if !modular then + ls (* for the moment we always qualify in modular Haskell *) + else [s] + | Ocaml -> + try (* has [mp] something in common with one of those in [mpl] ? *) + let pref = common_prefix_from_list mp mpl in + (*i TODO: possibilité de clash i*) + list_firstn ((mp_length mp)-(mp_length pref)+1) ls + with Not_found -> (* [mp] is othogonal with every element of [mp]. *) + let base = base_mp mp in + if !modular && + (at_toplevel mp) && + not (Refset.mem r !to_qualify) && + not (clash base [] s mpl) + then snd (list_sep_last ls) + else ls in add_module_contents mp s; (* update the visible environment *) str (dottify ls) + (* The next function is used only in Ocaml extraction...*) let pp_module mpl mp = let ls = if !modular @@ -317,7 +324,6 @@ module StdParams = struct (*i TODO: clash possible i*) list_firstn ((mp_length mp)-(mp_length pref)) ls with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base = base_mp mp in if !modular && (at_toplevel mp) then snd (list_sep_last ls) else ls @@ -394,15 +400,15 @@ let print_structure_to_file f prm struc = in let print_dummys = (struct_ast_search ((=) MLdummy) struc, - struct_type_search Tdummy struc, - struct_type_search Tunknown struc) + struct_type_search Mlutil.isDummy struc, + struct_type_search ((=) Tunknown) struc) in let print_magic = if lang () <> Haskell then false else struct_ast_search (function MLmagic _ -> true | _ -> false) struc in (* print the implementation *) - let cout = option_app (fun (f,_) -> open_out f) f in + let cout = option_map (fun (f,_) -> open_out f) f in let ft = match cout with | None -> !Pp_control.std_ft | Some cout -> Pp_control.with_output_to cout in diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 3e5efa0c..2ba51e1c 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.mli,v 1.19.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: common.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) open Names open Miniml diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index d725a1d7..e31b701c 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml,v 1.74.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extract_env.ml 9486 2007-01-15 19:11:28Z letouzey $ i*) open Term open Declarations @@ -19,6 +19,7 @@ open Table open Extraction open Modutil open Common +open Mod_subst (*s Obtaining Coq environment. *) @@ -28,7 +29,7 @@ let toplevel_env () = | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in let seb = match Libobject.object_tag o with - | "CONSTANT" -> SEBconst (Global.lookup_constant kn) + | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn)) | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l))) | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn) @@ -52,19 +53,61 @@ let environment_until dir_opt = | _ -> assert false in parse (Library.loaded_libraries ()) -type visit = { mutable kn : KNset.t; mutable mp : MPset.t } -let in_kn v kn = KNset.mem kn v.kn -let in_mp v mp = MPset.mem mp v.mp - -let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp -let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn) -let visit_ref v r = visit_kn v (kn_of_r r) +(*s Visit: + a structure recording the needed dependencies for the current extraction *) + +module type VISIT = sig + (* Reset the dependencies by emptying the visit lists *) + val reset : unit -> unit + + (* Add the module_path and all its prefixes to the mp visit list *) + val add_mp : module_path -> unit + + (* Add kernel_name / constant / reference / ... in the visit lists. + These functions silently add the mp of their arg in the mp list *) + val add_kn : kernel_name -> unit + val add_con : constant -> unit + val add_ref : global_reference -> unit + val add_decl_deps : ml_decl -> unit + val add_spec_deps : ml_spec -> unit + + (* Test functions: + is a particular object a needed dependency for the current extraction ? *) + val needed_kn : kernel_name -> bool + val needed_con : constant -> bool + val needed_mp : module_path -> bool +end + +module Visit : VISIT = struct + (* Thanks to C.S.C, what used to be in a single KNset should now be split + into a KNset (for inductives and modules names) and a Cset for constants + (and still the remaining MPset) *) + type must_visit = + { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t } + (* the imperative internal visit lists *) + let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } + (* the accessor functions *) + let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty + let needed_kn kn = KNset.mem kn v.kn + let needed_con c = Cset.mem c v.con + let needed_mp mp = MPset.mem mp v.mp + let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) + let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) + let add_ref = function + | ConstRef c -> add_con c + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn + | VarRef _ -> assert false + let add_decl_deps = decl_iter_references add_ref add_ref add_ref + let add_spec_deps = spec_iter_references add_ref add_ref add_ref +end exception Impossible let check_arity env cb = - if Reduction.is_arity env cb.const_type then raise Impossible + let t = Typeops.type_of_constant_type env cb.const_type in + if Reduction.is_arity env t then raise Impossible let check_fix env cb i = match cb.const_body with @@ -93,115 +136,108 @@ let factor_fix env l cb msb = labels, recd, msb'' end -let get_decl_references v d = - let f = visit_ref v in decl_iter_references f f f d - -let get_spec_references v s = - let f = visit_ref v in spec_iter_references f f f s - -let rec extract_msig env v mp = function +let rec extract_msig env mp = function | [] -> [] | (l,SPBconst cb) :: msig -> - let kn = make_kn mp empty_dirpath l in + let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in - if logical_spec s then extract_msig env v mp msig + if logical_spec s then extract_msig env mp msig else begin - get_spec_references v s; - (l,Spec s) :: (extract_msig env v mp msig) + Visit.add_spec_deps s; + (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmind cb) :: msig -> let kn = make_kn mp empty_dirpath l in let s = Sind (kn, extract_inductive env kn) in - if logical_spec s then extract_msig env v mp msig + if logical_spec s then extract_msig env mp msig else begin - get_spec_references v s; - (l,Spec s) :: (extract_msig env v mp msig) + Visit.add_spec_deps s; + (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmodule {msb_modtype=mtb}) :: msig -> -(*i let mpo = Some (MPdot (mp,l)) in i*) - (l,Smodule (extract_mtb env v None (*i mpo i*) mtb)) :: (extract_msig env v mp msig) + (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig) | (l,SPBmodtype mtb) :: msig -> - (l,Smodtype (extract_mtb env v None mtb)) :: (extract_msig env v mp msig) + (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig) -and extract_mtb env v mpo = function - | MTBident kn -> visit_kn v kn; MTident kn +and extract_mtb env mpo = function + | MTBident kn -> Visit.add_kn kn; MTident kn | MTBfunsig (mbid, mtb, mtb') -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_mtb env v None mtb, - extract_mtb env' v None mtb') + MTfunsig (mbid, extract_mtb env None mtb, + extract_mtb env' None mtb') | MTBsig (msid, msig) -> let mp, msig = match mpo with | None -> MPself msid, msig | Some mp -> mp, Modops.subst_signature_msid msid mp msig in let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_msig env' v mp msig) + MTsig (msid, extract_msig env' mp msig) -let rec extract_msb env v mp all = function +let rec extract_msb env mp all = function | [] -> [] | (l,SEBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in - let ms = extract_msb env v mp all msb in - let b = array_exists (in_kn v) vkn in + let vc = Array.map (make_con mp empty_dirpath) vl in + let ms = extract_msb env mp all msb in + let b = array_exists Visit.needed_con vc in if all || b then - let d = extract_fixpoint env vkn recd in + let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_msb env v mp all msb in - let kn = make_kn mp empty_dirpath l in - let b = in_kn v kn in + let ms = extract_msb env mp all msb in + let c = make_con mp empty_dirpath l in + let b = Visit.needed_con c in if all || b then - let d = extract_constant env kn cb in + let d = extract_constant env c cb in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) | (l,SEBmind mib) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in - let b = in_kn v kn in + let b = Visit.needed_kn kn in if all || b then let d = Dind (kn, extract_inductive env kn) in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms | (l,SEBmodule mb) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let mp = MPdot (mp,l) in - if all || in_mp v mp then - (l,SEmodule (extract_module env v mp true mb)) :: ms + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true mb)) :: ms else ms | (l,SEBmodtype mtb) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in - if all || in_kn v kn then - (l,SEmodtype (extract_mtb env v None mtb)) :: ms + if all || Visit.needed_kn kn then + (l,SEmodtype (extract_mtb env None mtb)) :: ms else ms -and extract_meb env v mpo all = function +and extract_meb env mpo all = function | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *) - | MEBident mp -> visit_mp v mp; MEident mp + | MEBident mp -> Visit.add_mp mp; MEident mp | MEBapply (meb, meb',_) -> - MEapply (extract_meb env v None true meb, - extract_meb env v None true meb') + MEapply (extract_meb env None true meb, + extract_meb env None true meb') | MEBfunctor (mbid, mtb, meb) -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_mtb env v None mtb, - extract_meb env' v None true meb) + MEfunctor (mbid, extract_mtb env None mtb, + extract_meb env' None true meb) | MEBstruct (msid, msb) -> let mp,msb = match mpo with | None -> MPself msid, msb | Some mp -> mp, subst_msb (map_msid msid mp) msb in let env' = add_structure mp msb env in - MEstruct (msid, extract_msb env' v mp all msb) + MEstruct (msid, extract_msb env' mp all msb) -and extract_module env v mp all mb = +and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) let meb = out_some mb.mod_expr in @@ -209,25 +245,21 @@ and extract_module env v mp all mb = (* Because of the "with" construct, the module type can be [MTBsig] with *) (* a msid different from the one of the module. Here is the patch. *) let mtb = replicate_msid meb mtb in - { ml_mod_expr = extract_meb env v (Some mp) all meb; - ml_mod_type = extract_mtb env v None mtb } + { ml_mod_expr = extract_meb env (Some mp) all meb; + ml_mod_type = extract_mtb env None mtb } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = - let l = environment_until None in - let v = - let add_kn r = KNset.add (kn_of_r r) in - let kns = List.fold_right add_kn refs KNset.empty in - let add_mp mp = MPset.union (prefixes_mp mp) in - let mps = List.fold_right add_mp mpl MPset.empty in - let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in - { kn = kns; mp = mps } - in + Visit.reset (); + List.iter Visit.add_ref refs; + List.iter Visit.add_mp mpl; let env = Global.env () in - List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) - (List.rev l) + let l = List.rev (environment_until None) in + List.rev_map + (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l + (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] to get the saturated environment to extract. *) @@ -248,6 +280,7 @@ let mono_extraction (f,m) qualids = let prm = {modular=false; mod_name = m; to_appear= refs} in let struc = optimize_struct prm None (mono_environment refs mps) in print_structure_to_file f prm struc; + Visit.reset (); reset_tables () let extraction_rec = mono_extraction (None,id_of_string "Main") @@ -266,16 +299,15 @@ let extraction qid = let r = Nametab.global qid in if is_custom r then msgnl (str "User defined extraction:" ++ spc () ++ - str (find_custom r) ++ fnl ()) - else begin + str (find_custom r) ++ fnl ()) + else let prm = - { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let kn = kn_of_r r in + { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in let struc = optimize_struct prm None (mono_environment [r] []) in let d = get_decl_in_structure r struc in - print_one_decl struc (modpath kn) d; - reset_tables () - end + print_one_decl struc (modpath_of_r r) d; + Visit.reset (); + reset_tables () (*s Extraction to a file (necessarily recursive). The vernacular command is @@ -303,32 +335,33 @@ let extraction_file f vl = let extraction_module m = check_inside_section (); check_inside_module (); - match lang () with + begin match lang () with | Toplevel -> error_toplevel () | Scheme -> error_scheme () - | _ -> - let q = snd (qualid_of_reference m) in - let mp = - try Nametab.locate_module q - with Not_found -> error_unknown_module q - in - let b = is_modfile mp in - let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in - let l = environment_until None in - let v = { kn = KNset.empty ; mp = prefixes_mp mp } in - let env = Global.env () in - let struc = - List.rev_map - (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) b m)) - (List.rev l) - in - let struc = optimize_struct prm None struc in - let struc = - let bmp = base_mp mp in - try [bmp, List.assoc bmp struc] with Not_found -> assert false - in - print_structure_to_file None prm struc; - reset_tables () + | _ -> () + end; + let q = snd (qualid_of_reference m) in + let mp = + try Nametab.locate_module q with Not_found -> error_unknown_module q + in + let b = is_modfile mp in + let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in + Visit.reset (); + Visit.add_mp mp; + let env = Global.env () in + let l = List.rev (environment_until None) in + let struc = + List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l + in + let struc = optimize_struct prm None struc in + let struc = + let bmp = base_mp mp in + try [bmp, List.assoc bmp struc] with Not_found -> assert false + in + print_structure_to_file None prm struc; + Visit.reset (); + reset_tables () + (*s (Recursive) Extraction of a library. The vernacular command is \verb!(Recursive) Extraction Library! [M]. *) @@ -345,36 +378,38 @@ let dir_module_of_id m = let extraction_library is_rec m = check_inside_section (); check_inside_module (); - match lang () with + begin match lang () with | Toplevel -> error_toplevel () | Scheme -> error_scheme () - | _ -> - let dir_m = dir_module_of_id m in - let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in - let l = environment_until (Some dir_m) in - let struc = - let env = Global.env () in - let select l (mp,meb) = - if in_mp v mp (* [mp] est long -> [in_mp] peut etre sans [long_mp] *) - then (mp, unpack (extract_meb env v (Some mp) true meb)) :: l - else l - in - List.fold_left select [] (List.rev l) - in - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let struc = optimize_struct dummy_prm None struc in - let rec print = function - | [] -> () - | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l - | (MPfile dir, sel) as e :: l -> - let short_m = snd (split_dirpath dir) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - print_structure_to_file (Some f) prm [e]; - print l - | _ -> assert false - in print struc; - reset_tables () + | _ -> () + end; + let dir_m = dir_module_of_id m in + Visit.reset (); + Visit.add_mp (MPfile dir_m); + let env = Global.env () in + let l = List.rev (environment_until (Some dir_m)) in + let select l (mp,meb) = + if Visit.needed_mp mp + then (mp, unpack (extract_meb env (Some mp) true meb)) :: l + else l + in + let struc = List.fold_left select [] l in + let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in + let struc = optimize_struct dummy_prm None struc in + let rec print = function + | [] -> () + | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l + | (MPfile dir, sel) as e :: l -> + let short_m = snd (split_dirpath dir) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + print_structure_to_file (Some f) prm [e]; + print l + | _ -> assert false + in + print struc; + Visit.reset (); + reset_tables () diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 8ce64342..a09464a1 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.mli,v 1.13.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extract_env.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*s This module declares the extraction commands. *) diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6bfe861f..6fd4a3cc 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*) +(*i $Id: extraction.ml 9456 2006-12-17 20:08:38Z letouzey $ i*) (*i*) open Util @@ -35,6 +35,9 @@ exception I of inductive_info to avoid loops in [extract_inductive] *) let internal_call = ref KNset.empty +(* A set of all fixpoint functions currently being extracted *) +let current_fixpoints = ref ([] : constant list) + let none = Evd.empty let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) @@ -80,6 +83,14 @@ let rec flag_of_type env t = let is_default env t = (flag_of_type env t = (Info, Default)) +exception NotDefault of kill_reason + +let check_default env t = + match flag_of_type env t with + | _,TypeScheme -> raise (NotDefault Ktype) + | Logic,_ -> raise (NotDefault Kother) + | _ -> () + let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme)) (*s [type_sign] gernerates a signature aimed at treating a type application. *) @@ -87,7 +98,8 @@ let is_info_scheme env t = (flag_of_type env t = (Info, TypeScheme)) let rec type_sign env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> - (is_info_scheme env t)::(type_sign (push_rel_assum (n,t) env) d) + (if is_info_scheme env t then Keep else Kill Kother) + :: (type_sign (push_rel_assum (n,t) env) d) | _ -> [] let rec type_scheme_nb_args env c = @@ -105,8 +117,8 @@ let rec type_sign_vl env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_scheme env t) then false::s, vl - else true::s, (next_ident_away (id_of_name n) vl) :: vl + if not (is_info_scheme env t) then Kill Kother::s, vl + else Keep::s, (next_ident_away (id_of_name n) vl) :: vl | _ -> [],[] let rec nb_default_params env c = @@ -126,8 +138,8 @@ let rec nb_default_params env c = let db_from_sign s = let rec make i acc = function | [] -> acc - | true :: l -> make (i+1) (i::acc) l - | false :: l -> make i (0::acc) l + | Keep :: l -> make (i+1) (i::acc) l + | Kill _ :: l -> make i (0::acc) l in make 1 [] s (*s Create a type variable context from indications taken from @@ -150,8 +162,8 @@ let rec db_from_ind dbmap i = let parse_ind_args si args relmax = let rec parse i j = function | [] -> Intmap.empty - | false :: s -> parse (i+1) j s - | true :: s -> + | Kill _ :: s -> parse (i+1) j s + | Keep :: s -> (match kind_of_term args.(i-1) with | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s) | _ -> parse (i+1) (j+1) s) @@ -167,6 +179,7 @@ let parse_ind_args si args relmax = (* [j] stands for the next ML type var. [j=0] means we do not generate ML type var anymore (in subterms for example). *) + let rec extract_type env db j c args = match kind_of_term (whd_betaiotazeta c) with | App (d, args') -> @@ -183,19 +196,24 @@ let rec extract_type env db j c args = | (Info, Default) -> (* Standard case: two [extract_type] ... *) let mld = extract_type env' (0::db) j d [] in - if type_eq (mlt_env env) mld Tdummy then Tdummy - else Tarr (extract_type env db 0 t [], mld) + (match expand env mld with + | Tdummy d -> Tdummy d + | _ -> Tarr (extract_type env db 0 t [], mld)) | (Info, TypeScheme) when j > 0 -> (* A new type var. *) let mld = extract_type env' (j::db) (j+1) d [] in - if type_eq (mlt_env env) mld Tdummy then Tdummy - else Tarr (Tdummy, mld) - | _ -> + (match expand env mld with + | Tdummy d -> Tdummy d + | _ -> Tarr (Tdummy Ktype, mld)) + | _,lvl -> let mld = extract_type env' (0::db) j d [] in - if type_eq (mlt_env env) mld Tdummy then Tdummy - else Tarr (Tdummy, mld)) - | Sort _ -> Tdummy (* The two logical cases. *) - | _ when sort_of env (applist (c, args)) = InProp -> Tdummy + (match expand env mld with + | Tdummy d -> Tdummy d + | _ -> + let reason = if lvl=TypeScheme then Ktype else Kother in + Tarr (Tdummy reason, mld))) + | Sort _ -> Tdummy Ktype (* The two logical cases. *) + | _ when sort_of env (applist (c, args)) = InProp -> Tdummy Kother | Rel n -> (match lookup_rel n env with | (_,Some t,_) -> extract_type env db j (lift n t) args @@ -207,7 +225,7 @@ let rec extract_type env db j c args = | Const kn -> let r = ConstRef kn in let cb = lookup_constant kn env in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in (match flag_of_type env typ with | (Info, TypeScheme) -> let mlt = extract_type_app env db (r, type_sign env typ) args in @@ -222,7 +240,7 @@ let rec extract_type env db j c args = (* The more precise is [mlt'], extracted after reduction *) (* The shortest is [mlt], which use abbreviations *) (* If possible, we take [mlt], otherwise [mlt']. *) - if type_eq (mlt_env env) mlt mlt' then mlt else mlt') + if expand env mlt = expand env mlt' then mlt else mlt') | _ -> (* only other case here: Info, Default, i.e. not an ML type *) (match cb.const_body with | None -> Tunknown (* Brutal approximation ... *) @@ -230,7 +248,7 @@ let rec extract_type env db j c args = (* We try to reduce. *) let newc = applist (Declarations.force lbody, args) in extract_type env db j newc [])) - | Ind ((kn,i) as ip) -> + | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args | Case _ | Fix _ | CoFix _ -> Tunknown @@ -242,7 +260,7 @@ let rec extract_type env db j c args = 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 else Tunknown + 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], @@ -251,7 +269,7 @@ and extract_maybe_type env db c = and extract_type_app env db (r,s) args = let ml_args = List.fold_right - (fun (b,c) a -> if b then + (fun (b,c) a -> if b=Keep then let p = List.length (fst (splay_prod env none (type_of env c))) in let db = iterate (fun l -> 0 :: l) p db in (extract_type_scheme env db c p) :: a @@ -292,18 +310,22 @@ and extract_ind env kn = (* kn is supposed to be in long form *) with Not_found -> internal_call := KNset.add kn !internal_call; let mib = Environ.lookup_mind kn env in + (* First, if this inductive is aliased via a Module, *) + (* we process the original inductive. *) + option_iter (fun kn -> ignore (extract_ind env kn)) mib.mind_equiv; (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in - let npar = mip0.mind_nparams in - let epar = push_rel_context mip0.mind_params_ctxt env in + let npar = mib.mind_nparams in + let epar = push_rel_context mib.mind_params_ctxt env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = Array.map - (fun mip -> - let b = mip.mind_sort <> (Prop Null) in - let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in + (fun mip -> + let b = snd (mind_arity mip) <> InProp in + let ar = Inductive.type_of_inductive env (mib,mip) in + let s,v = if b then type_sign_vl env ar else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in { ip_typename = mip.mind_typename; ip_consnames = mip.mind_consnames; @@ -313,7 +335,11 @@ and extract_ind env kn = (* kn is supposed to be in long form *) ip_types = t }) mib.mind_packets in - add_ind kn {ind_info = Standard; ind_nparams = npar; ind_packets = packets}; + add_ind kn + {ind_info = Standard; + ind_nparams = npar; + ind_packets = packets; + ind_equiv = mib.mind_equiv }; (* Second pass: we extract constructors *) for i = 0 to mib.mind_ntypes - 1 do let p = packets.(i) in @@ -341,7 +367,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) if p.ip_logical then raise (I Standard); if Array.length p.ip_types <> 1 then raise (I Standard); let typ = p.ip_types.(0) in - let l = List.filter (type_neq (mlt_env env) Tdummy) typ in + let l = List.filter (fun t -> not (isDummy (expand env t))) typ in if List.length l = 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); if l = [] then raise (I Standard); @@ -354,25 +380,26 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let rec names_prod t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t - | Cast(t,_) -> names_prod t + | Cast(t,_,_) -> names_prod t | _ -> [] in let field_names = - list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); - let projs = ref KNset.empty in + let projs = ref Cset.empty in let mp,d,_ = repr_kn kn in let rec select_fields l typs = match l,typs with | [],[] -> [] | (Name id)::l, typ::typs -> - if type_eq (mlt_env env) Tdummy typ then select_fields l typs + if isDummy (expand env typ) then select_fields l typs else - let knp = make_kn mp d (label_of_id id) in - if not (List.mem false (type_to_sign (mlt_env env) typ)) then - projs := KNset.add knp !projs; + let knp = make_con mp d (label_of_id id) in + if not (List.exists isKill (type2signature env typ)) + then + projs := Cset.add knp !projs; (ConstRef knp) :: (select_fields l typs) | Anonymous::l, typ::typs -> - if type_eq (mlt_env env) Tdummy typ then select_fields l typs + if isDummy (expand env typ) then select_fields l typs else error_record r | _ -> assert false in @@ -381,17 +408,23 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Is this record officially declared with its projections ? *) (* If so, we use this information. *) begin try - let n = nb_default_params env mip0.mind_nf_arity in + let n = nb_default_params env + (Inductive.type_of_inductive env (mib,mip0)) + in List.iter (option_iter - (fun kn -> if KNset.mem kn !projs then add_projection n kn)) - (find_structure ip).s_PROJ + (fun kn -> if Cset.mem kn !projs then add_projection n kn)) + (lookup_projections ip) with Not_found -> () end; Record field_glob with (I info) -> info in - let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in + let i = {ind_info = ind_info; + ind_nparams = npar; + ind_packets = packets; + ind_equiv = mib.mind_equiv} + in add_ind kn i; internal_call := KNset.remove kn !internal_call; i @@ -419,13 +452,13 @@ and extract_type_cons env db dbmap c i = and mlt_env env r = match r with | ConstRef kn -> (try - if not (visible_kn kn) then raise Not_found; + if not (visible_con kn) then raise Not_found; match lookup_term kn with | Dtype (_,vl,mlt) -> Some mlt | _ -> None with Not_found -> let cb = Environ.lookup_constant kn env in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in match cb.const_body with | None -> None | Some l_body -> @@ -439,20 +472,20 @@ and mlt_env env r = match r with | _ -> None)) | _ -> None -let type_expand env = type_expand (mlt_env env) -let type_neq env = type_neq (mlt_env env) -let type_to_sign env = type_to_sign (mlt_env env) +and expand env = type_expand (mlt_env env) +and type2signature env = type_to_signature (mlt_env env) +let type2sign env = type_to_sign (mlt_env env) let type_expunge env = type_expunge (mlt_env env) (*s Extraction of the type of a constant. *) let record_constant_type env kn opt_typ = try - if not (visible_kn kn) then raise Not_found; + if not (visible_con kn) then raise Not_found; lookup_type kn with Not_found -> let typ = match opt_typ with - | None -> constant_type env kn + | None -> Typeops.type_of_constant env kn | Some typ -> typ in let mlt = extract_type env [] 1 typ [] in let schema = (type_maxvar mlt, mlt) @@ -478,10 +511,9 @@ let rec extract_term env mle mlt c args = in extract_term env mle mlt d' [] | [] -> let env' = push_rel_assum (Name id, t) env in - let id, a = - if is_default env t - then id, new_meta () - else dummy_name, Tdummy in + let id, a = try check_default env t; id, new_meta() + with NotDefault d -> dummy_name, Tdummy d + in let b = new_meta () in (* If [mlt] cannot be unified with an arrow type, then magic! *) let magic = needs_magic (mlt, Tarr (a, b)) in @@ -491,15 +523,16 @@ let rec extract_term env mle mlt c args = let id = id_of_name n in let env' = push_rel (Name id, Some c1, t1) env in let args' = List.map (lift 1) args in - if is_default env t1 then + (try + check_default env t1; let a = new_meta () in let c1' = extract_term env mle a c1 [] in (* The type of [c1'] is generalized and stored in [mle]. *) let mle' = Mlenv.push_gen mle a in MLletin (id, c1', extract_term env' mle' mlt c2 args') - else - let mle' = Mlenv.push_std_type mle Tdummy in - ast_pop (extract_term env' mle' mlt c2 args') + with NotDefault d -> + let mle' = Mlenv.push_std_type mle (Tdummy d) in + ast_pop (extract_term env' mle' mlt c2 args')) | Const kn -> extract_cst_app env mle mlt kn args | Construct cp -> @@ -515,14 +548,16 @@ let rec extract_term env mle mlt c args = extract_app env mle mlt (extract_fix env mle i recd) args | CoFix (i,recd) -> extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c, _) -> extract_term env mle mlt c args + | Cast (c,_,_) -> extract_term env mle mlt c args | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) and extract_maybe_term env mle mlt c = - if is_default env (type_of env c) then extract_term env mle mlt c [] - else put_magic (mlt, Tdummy) MLdummy + try check_default env (type_of env c); + extract_term env mle mlt c [] + with NotDefault d -> + put_magic (mlt, Tdummy d) MLdummy (*s Generic way to deal with an application. *) @@ -540,7 +575,7 @@ and extract_app env mle mlt mk_head args = and make_mlargs env e s args typs = let l = ref s in - let keep () = match !l with [] -> true | b :: s -> l:=s; b in + let keep () = match !l with [] -> true | b :: s -> l:=s; b=Keep in let rec f = function | [], [] -> [] | a::la, t::lt when keep() -> extract_maybe_term env e t a :: (f (la,lt)) @@ -553,19 +588,25 @@ and make_mlargs env e s args typs = and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in - let schema = nb, type_expand env t in + let schema = nb, expand env t in + (* Can we instantiate types variables for this constant ? *) + (* In Ocaml, inside the definition of this constant, the answer is no. *) + let instantiated = + if lang () = Ocaml && List.mem kn !current_fixpoints then var2var' (snd schema) + else instantiation schema + in (* Then the expected type of this constant. *) - let metas = List.map new_meta args in + let a = new_meta () in (* We compare stored and expected types in two steps. *) (* First, can [kn] be applied to all args ? *) - let a = new_meta () in - let magic1 = needs_magic (type_recomp (metas, a), instantiation schema) in + let metas = List.map new_meta args in + let magic1 = needs_magic (type_recomp (metas, a), instantiated) in (* Second, is the resulting type compatible with the expected type [mlt] ? *) let magic2 = needs_magic (a, mlt) in (* The internal head receives a magic if [magic1] *) let head = put_magic_if magic1 (MLglob (ConstRef kn)) in (* Now, the extraction of the arguments. *) - let s = type_to_sign env (snd schema) in + let s = type2signature env (snd schema) in let ls = List.length s in let la = List.length args in let mla = make_mlargs env mle s args metas in @@ -580,8 +621,8 @@ and extract_cst_app env mle mlt kn args = in (* Different situations depending of the number of arguments: *) if ls = 0 then put_magic_if magic2 head - else if List.mem true s then - if la >= ls || not (List.mem false s) + else if List.mem Keep s then + if la >= ls || not (List.exists isKill s) then put_magic_if (magic2 && not magic1) (MLapp (head, mla)) else @@ -590,12 +631,17 @@ and extract_cst_app env mle mlt kn args = let s' = list_lastn ls' s in let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in put_magic_if magic2 (anonym_or_dummy_lams (MLapp (head, mla)) s') - else + else if List.mem (Kill Kother) s then (* In the special case of always false signature, one dummy lam is left. *) (* So a [MLdummy] is left accordingly. *) if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, MLdummy :: mla)) else put_magic_if magic2 (dummy_lams head (ls-la-1)) + else (* s is made only of [Kill Ktype] *) + if la >= ls + then put_magic_if (magic2 && not magic1) (MLapp (head, mla)) + else put_magic_if magic2 (dummy_lams head (ls-la)) + (*s Extraction of an inductive constructor applied to arguments. *) @@ -613,12 +659,12 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = let params_nb = mi.ind_nparams in let oi = mi.ind_packets.(i) in let nb_tvars = List.length oi.ip_vars - and types = List.map (type_expand env) oi.ip_types.(j-1) in + and types = List.map (expand env) oi.ip_types.(j-1) in let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in let type_cons = instantiation (nb_tvars, type_cons) in (* Then, the usual variables [s], [ls], [la], ... *) - let s = List.map (type_neq env Tdummy) types in + let s = List.map (type2sign env) types in let ls = List.length s in let la = List.length args in assert (la <= ls + params_nb); @@ -671,14 +717,13 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* Logical singleton case: *) (* [match c with C i j k -> t] becomes [t'] *) assert (br_size = 1); - let s = iterate (fun l -> false :: l) ni.(0) [] in - let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni.(0) mlt in + let s = iterate (fun l -> Kill Kother :: l) ni.(0) [] in + let mlt = iterate (fun t -> Tarr (Tdummy Kother, t)) ni.(0) mlt in let e = extract_maybe_term env mle mlt br.(0) in snd (case_expunge s e) end else let mi = extract_ind env kn in - let params_nb = mi.ind_nparams in let oi = mi.ind_packets.(i) in let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) @@ -687,10 +732,10 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* The extraction of each branch. *) let extract_branch i = (* The types of the arguments of the corresponding constructor. *) - let f t = type_subst_vect metas (type_expand env t) in + let f t = type_subst_vect metas (expand env t) in let l = List.map f oi.ip_types.(i) in (* the corresponding signature *) - let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in + let s = List.map (type2sign env) oi.ip_types.(i) in (* Extraction of the branch (in functional form). *) let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in (* We suppress dummy arguments according to signature. *) @@ -746,8 +791,8 @@ let extract_std_constant env kn body typ = let t = snd (record_constant_type env kn (Some typ)) in (* The real type [t']: without head lambdas, expanded, *) (* and with [Tvar] translated to [Tvar'] (not instantiable). *) - let l,t' = type_decomp (type_expand env (var2var' t)) in - let s = List.map (type_neq env Tdummy) l in + let l,t' = type_decomp (expand env (var2var' t)) in + let s = List.map (type2sign env) l in (* The initial ML environment. *) let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in (* Decomposing the top level lambdas of [body]. *) @@ -763,10 +808,12 @@ let extract_std_constant env kn body typ = let extract_fixpoint env vkn (fi,ti,ci) = let n = Array.length vkn in - let types = Array.make n Tdummy + let types = Array.make n (Tdummy Kother) and terms = Array.make n MLdummy in + let kns = Array.to_list vkn in + current_fixpoints := kns; (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) - let sub = List.rev_map mkConst (Array.to_list vkn) in + let sub = List.rev_map mkConst kns in for i = 0 to n-1 do if sort_of env ti.(i) <> InProp then begin let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in @@ -774,11 +821,12 @@ let extract_fixpoint env vkn (fi,ti,ci) = types.(i) <- t; end done; + current_fixpoints := []; Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) let extract_constant env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in match cb.const_body with | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with @@ -791,12 +839,14 @@ let extract_constant env kn cb = if not (is_custom r) then warning_info_ax r; let t = snd (record_constant_type env kn (Some typ)) in Dterm (r, MLaxiom, type_expunge env t) - | (Logic,TypeScheme) -> warning_log_ax r; Dtype (r, [], Tdummy) - | (Logic,Default) -> warning_log_ax r; Dterm (r, MLdummy, Tdummy)) + | (Logic,TypeScheme) -> + warning_log_ax r; Dtype (r, [], Tdummy Ktype) + | (Logic,Default) -> + warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother)) | Some body -> (match flag_of_type env typ with - | (Logic, Default) -> Dterm (r, MLdummy, Tdummy) - | (Logic, TypeScheme) -> Dtype (r, [], Tdummy) + | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother) + | (Logic, TypeScheme) -> Dtype (r, [], Tdummy Ktype) | (Info, Default) -> let e,t = extract_std_constant env kn (force body) typ in Dterm (r,e,t) @@ -808,10 +858,10 @@ let extract_constant env kn cb = let extract_constant_spec env kn cb = let r = ConstRef kn in - let typ = cb.const_type in + let typ = Typeops.type_of_constant_type env cb.const_type in match flag_of_type env typ with - | (Logic, TypeScheme) -> Stype (r, [], Some Tdummy) - | (Logic, Default) -> Sval (r, Tdummy) + | (Logic, TypeScheme) -> Stype (r, [], Some (Tdummy Ktype)) + | (Logic, Default) -> Sval (r, Tdummy Kother) | (Info, TypeScheme) -> let s,vl = type_sign_vl env typ in (match cb.const_body with @@ -827,7 +877,7 @@ let extract_constant_spec env kn cb = let extract_inductive env kn = let ind = extract_ind env kn in add_recursors env kn; - let f l = List.filter (type_neq env Tdummy) l in + let f l = List.filter (fun t -> not (isDummy (expand env t))) l in let packets = Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) ind.ind_packets @@ -846,7 +896,7 @@ let extract_declaration env r = match r with type kind = Logical | Term | Type let constant_kind env cb = - match flag_of_type env cb.const_type with + match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with | (Logic,_) -> Logical | (Info,TypeScheme) -> Type | (Info,Default) -> Term @@ -854,19 +904,19 @@ let constant_kind env cb = (*s Is a [ml_decl] logical ? *) let logical_decl = function - | Dterm (_,MLdummy,Tdummy) -> true - | Dtype (_,[],Tdummy) -> true + | Dterm (_,MLdummy,Tdummy _) -> true + | Dtype (_,[],Tdummy _) -> true | Dfix (_,av,tv) -> (array_for_all ((=) MLdummy) av) && - (array_for_all ((=) Tdummy) tv) + (array_for_all isDummy tv) | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false (*s Is a [ml_spec] logical ? *) let logical_spec = function - | Stype (_, [], Some Tdummy) -> true - | Sval (_,Tdummy) -> true + | Stype (_, [], Some (Tdummy _)) -> true + | Sval (_,Tdummy _) -> true | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets | _ -> false diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index fc5782c9..1dfd7e1a 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.mli,v 1.27.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extraction.mli 6303 2004-11-16 12:37:40Z sacerdot $ i*) (*s Extraction from Coq terms to Miniml. *) @@ -17,12 +17,12 @@ open Environ open Libnames open Miniml -val extract_constant : env -> kernel_name -> constant_body -> ml_decl +val extract_constant : env -> constant -> constant_body -> ml_decl -val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec +val extract_constant_spec : env -> constant -> constant_body -> ml_spec val extract_fixpoint : - env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl + env -> constant array -> (constr, types) prec_declaration -> ml_decl val extract_inductive : env -> kernel_name -> ml_ind diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index 33a6117d..13b29c7b 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -15,10 +15,7 @@ open Pcoq open Genarg open Pp -let pr_mlname _ _ s = - spc () ++ - (if !Options.v7 && not (Options.do_translate()) then qs s - else Pptacticnew.qsnew s) +let pr_mlname _ _ _ s = spc () ++ qs s ARGUMENT EXTEND mlname TYPED AS string @@ -37,21 +34,6 @@ VERNAC ARGUMENT EXTEND language | [ "Toplevel" ] -> [ Toplevel ] END -(* Temporary for translator *) -if !Options.v7 then - let pr_language _ _ = function - | Ocaml -> str " Ocaml" - | Haskell -> str " Haskell" - | Scheme -> str " Scheme" - | Toplevel -> str " Toplevel" - in - let globwit_language = Obj.magic rawwit_language in - let wit_language = Obj.magic rawwit_language in - Pptactic.declare_extra_genarg_pprule true - (rawwit_language, pr_language) - (globwit_language, pr_language) - (wit_language, pr_language); - (* Extraction commands *) VERNAC COMMAND EXTEND Extraction diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 3834fe81..f924396c 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*) +(*i $Id: haskell.ml 8930 2006-06-09 02:14:34Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -106,7 +106,7 @@ let rec pp_type par vl t = | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) - | Tdummy -> str "()" + | Tdummy _ -> str "()" | Tunknown -> str "()" | Taxiom -> str "() -- AXIOM TO BE REALIZED\n" in @@ -210,7 +210,7 @@ and pp_function env f t = (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ hov 2 (pp_expr false env' [] t')) - + (*s Pretty-printing of inductive types declaration. *) let pp_comment s = str "-- " ++ s ++ fnl () @@ -240,11 +240,11 @@ let pp_one_ind ip pl cv = prlist_with_sep (fun () -> (str " ")) (pp_type true pl) l)) in - str (if cv = [||] then "type " else "data ") ++ + str (if Array.length cv = 0 then "type " else "data ") ++ pp_global (IndRef ip) ++ str " " ++ prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ (if pl = [] then mt () else str " ") ++ - if cv = [||] then str "= () -- empty inductive" + if Array.length cv = 0 then str "= () -- empty inductive" else (v 0 (str "= " ++ prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor @@ -289,12 +289,16 @@ let pp_decl mpl = else str "=" ++ spc () ++ pp_type false l t in hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl () - | Dfix (rv, defs,_) -> - let ppv = Array.map pp_global rv in - prlist_with_sep (fun () -> fnl () ++ fnl ()) - (fun (pi,ti) -> pp_function (empty_env ()) pi ti) - (List.combine (Array.to_list ppv) (Array.to_list defs)) - ++ fnl () ++ fnl () + | Dfix (rv, defs, typs) -> + let max = Array.length rv in + let rec iter i = + if i = max then mt () + else + let e = pp_global rv.(i) in + e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () + ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl () + ++ iter (i+1) + in iter 0 | Dterm (r, a, t) -> if is_inline_custom r then mt () else diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 822444bd..106f7868 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: haskell.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) open Pp open Names diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 7c18f9f5..3b4146f8 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*) +(*i $Id: miniml.mli 9456 2006-12-17 20:08:38Z letouzey $ i*) (*s Target language for extraction: a core ML called MiniML. *) @@ -18,11 +18,18 @@ open Libnames (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML object. *) + +(* We eliminate from terms: 1) types 2) logical parts. + [Kother] stands both for logical or unknown reason. *) + +type kill_reason = Ktype | Kother + +type sign = Keep | Kill of kill_reason + -(* Convention: outmost lambda/product gives the head of the list, - and [true] means that the argument is to be kept. *) +(* Convention: outmost lambda/product gives the head of the list. *) -type signature = bool list +type signature = sign list (*s ML type expressions. *) @@ -32,7 +39,7 @@ type ml_type = | Tvar of int | Tvar' of int (* same as Tvar, used to avoid clash *) | Tmeta of ml_meta (* used during ML type reconstruction *) - | Tdummy + | Tdummy of kill_reason | Tunknown | Taxiom @@ -72,7 +79,9 @@ type ml_ind_packet = { type ml_ind = { ind_info : inductive_info; ind_nparams : int; - ind_packets : ml_ind_packet array } + ind_packets : ml_ind_packet array; + ind_equiv : kernel_name option +} (*s ML terms. *) diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index c01766b0..6bfedce5 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*) +(*i $Id: mlutil.ml 8886 2006-06-01 13:53:45Z letouzey $ i*) (*i*) open Pp @@ -111,7 +111,7 @@ let rec mgu = function List.iter mgu (List.combine l l') | Tvar i, Tvar j when i = j -> () | Tvar' i, Tvar' j when i = j -> () - | Tdummy, Tdummy -> () + | Tdummy _, Tdummy _ -> () | Tunknown, Tunknown -> () | _ -> raise Impossible @@ -209,8 +209,8 @@ end (*s Does a section path occur in a ML type ? *) let rec type_mem_kn kn = function - | Tmeta _ -> assert false - | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l + | Tmeta {contents = Some t} -> type_mem_kn kn t + | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b) | _ -> false @@ -218,7 +218,7 @@ let rec type_mem_kn kn = function let type_maxvar t = let rec parse n = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> parse n t | Tvar i -> max i n | Tarr (a,b) -> parse (parse n a) b | Tglob (_,l) -> List.fold_left parse n l @@ -228,7 +228,7 @@ let type_maxvar t = (*s From [a -> b -> c] to [[a;b],c]. *) let rec type_decomp = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> type_decomp t | Tarr (a,b) -> let l,h = type_decomp b in a::l, h | a -> [],a @@ -241,7 +241,7 @@ let rec type_recomp (l,t) = match l with (*s Translating [Tvar] to [Tvar'] to avoid clash. *) let rec var2var' = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> var2var' t | Tvar i -> Tvar' i | Tarr (a,b) -> Tarr (var2var' a, var2var' b) | Tglob (r,l) -> Tglob (r, List.map var2var' l) @@ -254,14 +254,14 @@ type abbrev_map = global_reference -> ml_type option let type_expand env t = let rec expand = function - | Tmeta _ -> assert false - | Tglob (r,l) as t -> + | Tmeta {contents = Some t} -> expand t + | Tglob (r,l) -> (match env r with | Some mlt -> expand (type_subst_list l mlt) | None -> Tglob (r, List.map expand l)) | Tarr (a,b) -> Tarr (expand a, expand b) | a -> a - in expand t + in if Table.type_expand () then expand t else t (*s Idem, but only at the top level of implications. *) @@ -269,7 +269,7 @@ let is_arrow = function Tarr _ -> true | _ -> false let type_weak_expand env t = let rec expand = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> expand t | Tglob (r,l) as t -> (match env r with | Some mlt -> @@ -280,34 +280,39 @@ let type_weak_expand env t = | a -> a in expand t -(*s Equality over ML types modulo delta-reduction *) - -let type_eq env t t' = (type_expand env t = type_expand env t') - -let type_neq env t t' = (type_expand env t <> type_expand env t') - (*s Generating a signature from a ML type. *) -let type_to_sign env t = +let type_to_sign env t = match type_expand env t with + | Tdummy d -> Kill d + | _ -> Keep + +let type_to_signature env t = let rec f = function - | Tmeta _ -> assert false - | Tarr (a,b) -> (Tdummy <> a) :: (f b) + | Tmeta {contents = Some t} -> f t + | Tarr (Tdummy d, b) -> Kill d :: f b + | Tarr (_, b) -> Keep :: f b | _ -> [] in f (type_expand env t) +let isKill = function Kill _ -> true | _ -> false + +let isDummy = function Tdummy _ -> true | _ -> false + +let sign_of_id i = if i = dummy_name then Kill Kother else Keep + (*s Removing [Tdummy] from the top level of a ML type. *) let type_expunge env t = - let s = type_to_sign env t in + let s = type_to_signature env t in if s = [] then t - else if List.mem true s then + else if List.mem Keep s then let rec f t s = - if List.mem false s then + if List.exists isKill s then match t with - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> f t s | Tarr (a,b) -> let t = f b (List.tl s) in - if List.hd s then Tarr (a, t) else t + if List.hd s = Keep then Tarr (a, t) else t | Tglob (r,l) -> (match env r with | Some mlt -> f (type_subst_list l mlt) s @@ -315,7 +320,9 @@ let type_expunge env t = | _ -> assert false else t in f t s - else Tarr (Tdummy, snd (type_decomp (type_weak_expand env t))) + else if List.mem (Kill Kother) s then + Tarr (Tdummy Kother, snd (type_decomp (type_weak_expand env t))) + else snd (type_decomp (type_weak_expand env t)) (*S Generic functions over ML ast terms. *) @@ -377,7 +384,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,c,l) -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) @@ -535,8 +542,8 @@ let rec dummy_lams a = function let rec anonym_or_dummy_lams a = function | [] -> a - | true :: s -> MLlam(anonymous, anonym_or_dummy_lams a s) - | false :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s) + | Keep :: s -> MLlam(anonymous, anonym_or_dummy_lams a s) + | Kill _ :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s) (*S Operations concerning eta. *) @@ -549,8 +556,8 @@ let rec eta_args n = let rec eta_args_sign n = function | [] -> [] - | true :: s -> (MLrel n) :: (eta_args_sign (n-1) s) - | false :: s -> eta_args_sign (n-1) s + | Keep :: s -> (MLrel n) :: (eta_args_sign (n-1) s) + | Kill _ :: s -> eta_args_sign (n-1) s (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *) @@ -594,11 +601,12 @@ let rec linear_beta_red a t = match a,t with linear beta reductions at modified positions. *) let rec ast_glob_subst s t = match t with - | MLapp ((MLglob (ConstRef kn)) as f, a) -> + | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> let a = List.map (ast_glob_subst s) a in - (try linear_beta_red a (KNmap.find kn s) + (try linear_beta_red a (Refmap.find refe s) with Not_found -> MLapp (f, a)) - | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t) + | MLglob ((ConstRef kn) as refe) -> + (try Refmap.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -653,7 +661,7 @@ let check_generalizable_case unsafe br = (*s Do all branches correspond to the same thing? *) let check_constant_case br = - if br = [||] then raise Impossible; + if Array.length br = 0 then raise Impossible; let (r,l,t) = br.(0) in let n = List.length l in if ast_occurs_itvl 1 n t then raise Impossible; @@ -818,33 +826,33 @@ let rec post_simpl = function (*S Local prop elimination. *) (* We try to eliminate as many [prop] as possible inside an [ml_ast]. *) -(*s In a list, it selects only the elements corresponding to a [true] +(*s In a list, it selects only the elements corresponding to a [Keep] in the boolean list [l]. *) let rec select_via_bl l args = match l,args with | [],_ -> args - | true::l,a::args -> a :: (select_via_bl l args) - | false::l,a::args -> select_via_bl l args + | Keep::l,a::args -> a :: (select_via_bl l args) + | Kill _::l,a::args -> select_via_bl l args | _ -> assert false -(*s [kill_some_lams] removes some head lambdas according to the bool list [bl]. +(*s [kill_some_lams] removes some head lambdas according to the signature [bl]. This list is build on the identifier list model: outermost lambda - is on the right. [true] means "to keep" and [false] means "to eliminate". + is on the right. [Rels] corresponding to removed lambdas are supposed not to occur, and the other [Rels] are made correct via a [gen_subst]. Output is not directly a [ml_ast], compose with [named_lams] if needed. *) let kill_some_lams bl (ids,c) = let n = List.length bl in - let n' = List.fold_left (fun n b -> if b then (n+1) else n) 0 bl in + let n' = List.fold_left (fun n b -> if b=Keep then (n+1) else n) 0 bl in if n = n' then ids,c else if n' = 0 then [],ast_lift (-n) c else begin let v = Array.make n MLdummy in let rec parse_ids i j = function | [] -> () - | true :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l - | false :: l -> parse_ids (i+1) j l + | Keep :: l -> v.(i) <- MLrel j; parse_ids (i+1) (j+1) l + | Kill _ :: l -> parse_ids (i+1) j l in parse_ids 0 1 bl ; select_via_bl bl ids, gen_subst v (n'-n) c end @@ -855,8 +863,8 @@ let kill_some_lams bl (ids,c) = let kill_dummy_lams c = let ids,c = collect_lams c in - let bl = List.map ((<>) dummy_name) ids in - if (List.mem true bl) && (List.mem false bl) then + let bl = List.map sign_of_id ids in + if (List.mem Keep bl) && (List.exists isKill bl) then let ids',c = kill_some_lams bl (ids,c) in ids, named_lams ids' c else raise Impossible @@ -864,7 +872,7 @@ let kill_dummy_lams c = (*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c] and a signature [s] and builds a eta-long version. *) -(* For example, if [s = [true;true;false;true]] then the output is : +(* For example, if [s = [Keep;Keep;Kill Prop;Keep]] then the output is : [fun idn ... id1 x x _ x -> (c' 4 3 __ 1)] with [c' = lift 4 c] *) let eta_expansion_sign s (ids,c) = @@ -872,13 +880,13 @@ let eta_expansion_sign s (ids,c) = | [] -> let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels in ids, MLapp (ast_lift (i-1) c, a) - | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l - | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l + | Keep :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l + | Kill _ :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l in abs ids [] 1 s (*s If [s = [b1; ... ; bn]] then [case_expunge] decomposes [e] in [n] lambdas (with eta-expansion if needed) and removes all dummy lambdas - corresponding to [false] in [s]. *) + corresponding to [Del] in [s]. *) let case_expunge s e = let m = List.length s in @@ -890,13 +898,14 @@ let case_expunge s e = (*s [term_expunge] takes a function [fun idn ... id1 -> c] and a signature [s] and remove dummy lams. The difference with [case_expunge] is that we here leave one dummy lambda - if all lambdas are dummy. *) + if all lambdas are logical dummy. *) let term_expunge s (ids,c) = if s = [] then c else let ids,c = kill_some_lams (List.rev s) (ids,c) in - if ids = [] then MLlam (dummy_name, ast_lift 1 c) + if ids = [] && List.mem (Kill Kother) s then + MLlam (dummy_name, ast_lift 1 c) else named_lams ids c (*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and @@ -905,7 +914,7 @@ let term_expunge s (ids,c) = let kill_dummy_args ids t0 t = let m = List.length ids in - let bl = List.rev_map ((<>) dummy_name) ids in + let bl = List.rev_map sign_of_id ids in let rec killrec n = function | MLapp(e, a) when e = ast_lift n t0 -> let k = max 0 (m - (List.length a)) in @@ -972,7 +981,8 @@ let general_optimize_fix f ids n args m c = let v = Array.make n 0 in 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) + | MLrel j when v.(j-1)>=0 -> + if ast_occurs (j+1) c then raise Impossible else 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 @@ -999,8 +1009,7 @@ let optimize_fix a = -> a' | MLfix(_,[|f|],[|c|]) -> (try general_optimize_fix f ids n args m c - with Impossible -> - named_lams ids (MLapp (MLfix (0,[|f|],[|c|]),args))) + with Impossible -> a) | _ -> a) | _ -> a @@ -1117,7 +1126,7 @@ let inline_test t = let manual_inline_list = let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in - List.map (fun s -> (make_kn mp empty_dirpath (mk_label s))) + List.map (fun s -> (make_con mp empty_dirpath (mk_label s))) [ "well_founded_induction_type"; "well_founded_induction"; "Acc_rect"; "Acc_rec" ; "Acc_iter" ] diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index eaf38778..a55caaf2 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.mli,v 1.47.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: mlutil.mli 8724 2006-04-20 09:57:01Z letouzey $ i*) open Util open Names @@ -62,13 +62,15 @@ val var2var' : ml_type -> ml_type type abbrev_map = global_reference -> ml_type option val type_expand : abbrev_map -> ml_type -> ml_type -val type_eq : abbrev_map -> ml_type -> ml_type -> bool -val type_neq : abbrev_map -> ml_type -> ml_type -> bool -val type_to_sign : abbrev_map -> ml_type -> bool list +val type_to_sign : abbrev_map -> ml_type -> sign +val type_to_signature : abbrev_map -> ml_type -> signature val type_expunge : abbrev_map -> ml_type -> ml_type -val case_expunge : bool list -> ml_ast -> identifier list * ml_ast -val term_expunge : bool list -> identifier list * ml_ast -> ml_ast +val isDummy : ml_type -> bool +val isKill : sign -> bool + +val case_expunge : signature -> ml_ast -> identifier list * ml_ast +val term_expunge : signature -> identifier list * ml_ast -> ml_ast (*s Special identifiers. [dummy_name] is to be used for dead code @@ -86,9 +88,9 @@ val collect_n_lams : int -> ml_ast -> identifier list * ml_ast val nb_lams : ml_ast -> int val dummy_lams : ml_ast -> int -> ml_ast -val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast +val anonym_or_dummy_lams : ml_ast -> signature -> ml_ast -val eta_args_sign : int -> bool list -> ml_ast list +val eta_args_sign : int -> signature -> ml_ast list (*s Utility functions over ML terms. *) @@ -101,7 +103,7 @@ val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast val ast_subst : ml_ast -> ml_ast -> ml_ast -val ast_glob_subst : ml_ast KNmap.t -> ml_ast -> ml_ast +val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 54f0c992..c9d4e237 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: modutil.ml 9456 2006-12-17 20:08:38Z letouzey $ i*) open Names open Declarations @@ -16,6 +16,7 @@ open Util open Miniml open Table open Mlutil +open Mod_subst (*S Functions upon modules missing in [Modops]. *) @@ -25,8 +26,9 @@ open Mlutil let add_structure mp msb env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in match elem with - | SEBconst cb -> Environ.add_constant kn cb env + | SEBconst cb -> Environ.add_constant con cb env | SEBmind mib -> Environ.add_mind kn mib env | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env | SEBmodtype mtb -> Environ.add_modtype kn mtb env @@ -116,8 +118,15 @@ let rec parse_labels ll = function let labels_of_mp mp = parse_labels [] mp -let labels_of_kn kn = - let mp,_,l = repr_kn kn in parse_labels [l] mp +let labels_of_ref r = + let mp,_,l = + match r with + ConstRef con -> repr_con con + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_kn kn + | VarRef _ -> assert false + in + parse_labels [l] mp let rec add_labels_mp mp = function | [] -> mp @@ -176,7 +185,7 @@ let ast_iter_references do_term do_cons do_type a = | MLcons (i,r,_) -> if lang () = Ocaml then record_iter_references do_term i; do_cons r - | MLcase (i,_,v) as a -> + | MLcase (i,_,v) -> if lang () = Ocaml then record_iter_references do_term i; Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () @@ -186,7 +195,10 @@ let ind_iter_references do_term do_cons do_type kn ind = let type_iter = type_iter_references do_type in let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in let packet_iter ip p = - do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types + do_type (IndRef ip); + if lang () = Ocaml then + option_iter (fun kne -> do_type (IndRef (kne,snd ip))) ind.ind_equiv; + Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in if lang () = Ocaml then record_iter_references do_term ind.ind_info; Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets @@ -243,40 +255,40 @@ let struct_get_references_list struc = exception Found -let rec ast_search t a = - if t a then raise Found else ast_iter (ast_search t) a +let rec ast_search f a = + if f a then raise Found else ast_iter (ast_search f) a -let decl_ast_search t = function - | Dterm (_,a,_) -> ast_search t a - | Dfix (_,c,_) -> Array.iter (ast_search t) c +let decl_ast_search f = function + | Dterm (_,a,_) -> ast_search f a + | Dfix (_,c,_) -> Array.iter (ast_search f) c | _ -> () -let struct_ast_search t s = - try struct_iter (decl_ast_search t) (fun _ -> ()) s; false +let struct_ast_search f s = + try struct_iter (decl_ast_search f) (fun _ -> ()) s; false with Found -> true -let rec type_search t = function - | Tarr (a,b) -> type_search t a; type_search t b - | Tglob (r,l) -> List.iter (type_search t) l - | u -> if t = u then raise Found +let rec type_search f = function + | Tarr (a,b) -> type_search f a; type_search f b + | Tglob (r,l) -> List.iter (type_search f) l + | u -> if f u then raise Found -let decl_type_search t = function +let decl_type_search f = function | Dind (_,{ind_packets=p}) -> Array.iter - (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p - | Dterm (_,_,u) -> type_search t u - | Dfix (_,_,v) -> Array.iter (type_search t) v - | Dtype (_,_,u) -> type_search t u + (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p + | Dterm (_,_,u) -> type_search f u + | Dfix (_,_,v) -> Array.iter (type_search f) v + | Dtype (_,_,u) -> type_search f u -let spec_type_search t = function +let spec_type_search f = function | Sind (_,{ind_packets=p}) -> Array.iter - (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p - | Stype (_,_,ot) -> option_iter (type_search t) ot - | Sval (_,u) -> type_search t u + (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p + | Stype (_,_,ot) -> option_iter (type_search f) ot + | Sval (_,u) -> type_search f u -let struct_type_search t s = - try struct_iter (decl_type_search t) (spec_type_search t) s; false +let struct_type_search f s = + try struct_iter (decl_type_search f) (spec_type_search f) s; false with Found -> true @@ -307,8 +319,7 @@ let signature_of_structure s = let get_decl_in_structure r struc = try - let kn = kn_of_r r in - let base_mp,ll = labels_of_kn kn in + 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 rec go ll sel = match ll with @@ -336,27 +347,27 @@ 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) (KNmap.add (kn_of_r 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) KNmap.empty + let s = make_subst (Array.length rv - 1) Refmap.empty in let rec subst n t = match t with - | MLglob (ConstRef kn) -> - (try MLrel (n + (KNmap.find kn s)) with Not_found -> t) + | MLglob ((ConstRef kn) as refe) -> + (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 (kn_of_r r))) rv 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 prm s = function | [] -> [] - | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l -> + | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l -> if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm 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 := KNmap.add (kn_of_r r) t !s; + if i then s := Refmap.add r t !s; if not i || prm.modular || List.mem r prm.to_appear then let d = match optimize_fix t with @@ -370,10 +381,9 @@ let rec optim prm s = function let rec optim_se top prm s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> - let kn = kn_of_r r in let a = normalize (ast_glob_subst !s a) in let i = inline r a in - if i then s := KNmap.add kn a !s; + if i then s := Refmap.add r a !s; if top && i && not prm.modular && not (List.mem r prm.to_appear) then optim_se top prm s lse else @@ -389,7 +399,7 @@ let rec optim_se top prm 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 := KNmap.add (kn_of_r 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 prm.modular @@ -408,6 +418,6 @@ and optim_me prm s = function | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me) let optimize_struct prm before struc = - let subst = ref (KNmap.empty : ml_ast KNmap.t) in + let subst = ref (Refmap.empty : ml_ast Refmap.t) in option_iter (fun l -> ignore (optim prm subst l)) before; List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index 7f8c4113..115a42ca 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: modutil.mli 8724 2006-04-20 09:57:01Z letouzey $ i*) open Names open Declarations open Environ open Libnames open Miniml +open Mod_subst (*s Functions upon modules missing in [Modops]. *) @@ -43,7 +44,7 @@ val add_labels_mp : module_path -> label list -> module_path (*s Functions upon ML modules. *) val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool -val struct_type_search : ml_type -> ml_structure -> bool +val struct_type_search : (ml_type -> bool) -> ml_structure -> bool type do_ref = global_reference -> unit diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index ff9cfd21..35f9a83c 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: ocaml.ml 9472 2007-01-05 15:49:32Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -196,7 +196,7 @@ let rec pp_type par vl t = | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) - | Tdummy -> str "__" + | Tdummy _ -> str "__" | Tunknown -> str "__" in hov 0 (pp_rec par t) @@ -264,7 +264,6 @@ let rec pp_expr par env args = let tuple = pp_tuple (pp_expr true env []) args' in pp_par par (pp_global r ++ spc () ++ tuple) | MLcase (i, t, pv) -> - let r,_,_ = pv.(0) in let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else @@ -344,13 +343,9 @@ and pp_pat env i pv = and pp_function env f t = 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 - not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl) - in match t' with - | MLcase(i,MLrel 1,pv) when i=Standard -> - if is_function pv then + | MLcase(i,MLrel 1,pv) when i=Standard -> + if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then (f ++ pr_binding (List.rev (List.tl bl)) ++ str " = function" ++ fnl () ++ v 0 (str " | " ++ pp_pat env' i pv)) @@ -359,7 +354,6 @@ and pp_function env f t = str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ v 0 (str " | " ++ pp_pat env' i pv)) - | _ -> (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ hov 2 (pp_expr false env' [] t')) @@ -398,7 +392,14 @@ let rec pp_Dfix init i ((rv,c,t) as fix) = (*s Pretty-printing of inductive types declaration. *) -let pp_one_ind prefix ip pl cv = +let pp_equiv param_list = function + | None -> mt () + | Some ip_equiv -> + str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv) + +let pp_comment s = str "(* " ++ s ++ str " *)" + +let pp_one_ind prefix ip ip_equiv pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = hov 2 (str " | " ++ pp_global r ++ @@ -408,13 +409,12 @@ let pp_one_ind prefix ip pl cv = prlist_with_sep (fun () -> spc () ++ str "* ") (pp_type true pl) l)) in - pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ - if cv = [||] then str " unit (* empty inductive *)" + pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ + pp_equiv pl ip_equiv ++ str " =" ++ + if Array.length cv = 0 then str " unit (* empty inductive *)" else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor (Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv)) -let pp_comment s = str "(* " ++ s ++ str " *)" - let pp_logical_ind packet = pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ fnl () ++ pp_comment (str "with constructors : " ++ @@ -428,10 +428,11 @@ let pp_singleton kn packet = pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) -let pp_record kn projs packet = +let pp_record kn projs ip_equiv packet = let l = List.combine projs packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in - str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++ + str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ + pp_equiv pl ip_equiv ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) ++ str " }" @@ -440,17 +441,20 @@ let pp_coind ip pl = let r = IndRef ip in let pl = rename_tvars keywords pl in pp_parameters pl ++ pp_global r ++ str " = " ++ - pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" + pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" ++ + fnl() ++ str "and " let pp_ind co kn ind = + let prefix = if co then "__" else "" in let some = ref false in let init= ref (str "type ") in let rec pp i = if i >= Array.length ind.ind_packets then mt () else let ip = (kn,i) in + let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in let p = ind.ind_packets.(i) in - if is_custom (IndRef (kn,i)) then pp (i+1) + if is_custom (IndRef ip) then pp (i+1) else begin some := true; if p.ip_logical then pp_logical_ind p ++ pp (i+1) @@ -459,8 +463,8 @@ let pp_ind co kn ind = begin init := (fnl () ++ str "and "); s ++ - (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) - ++ pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++ + (if co then pp_coind ip p.ip_vars else mt ()) + ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++ pp (i+1) end end @@ -474,19 +478,21 @@ let pp_mind kn i = match i.ind_info with | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i - | Record projs -> pp_record kn projs i.ind_packets.(0) + | Record projs -> + let ip_equiv = option_map (fun kn -> (kn,0)) i.ind_equiv in + pp_record kn projs ip_equiv i.ind_packets.(0) | Standard -> pp_ind false kn i let pp_decl mpl = local_mpl := mpl; function - | Dind (kn,i) as d -> pp_mind kn i + | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> if is_inline_custom r then failwith "empty phrase" else - let pp_r = pp_global r in + let pp_r = pp_global r in let l = rename_tvars keywords l in - let ids, def = try + let ids, def = try let ids,s = find_type_custom r in pp_string_parameters ids, str "=" ++ spc () ++ str s with not_found -> @@ -580,7 +586,7 @@ let rec pp_structure_elem mpl = function | (l,SEmodule m) -> hov 1 (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - (* if you want signatures everywhere: *) + (*i if you want signatures everywhere: i*) (*i str " :" ++ fnl () ++ i*) (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*) str " = " ++ diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 5015a50d..8c521ccd 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: ocaml.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) (*s Some utility functions to be reused in module [Haskell]. *) diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 4a881da2..7004a202 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*) +(*i $Id: scheme.ml 7651 2005-12-16 03:19:20Z letouzey $ i*) (*s Production of Scheme syntax. *) diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index 2a828fb9..ef4a3a63 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: scheme.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) (*s Some utility functions to be reused in module [Haskell]. *) diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 9d73d13f..b1a3cb31 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) +(*i $Id: table.ml 9310 2006-10-28 19:35:09Z herbelin $ i*) open Names open Term @@ -22,10 +22,23 @@ open Miniml (*S Utilities concerning [module_path] and [kernel_names] *) -let kn_of_r r = match r with - | ConstRef kn -> kn - | IndRef (kn,_) -> kn - | ConstructRef ((kn,_),_) -> kn +let occur_kn_in_ref kn = + function + | IndRef (kn',_) + | ConstructRef ((kn',_),_) -> kn = kn' + | ConstRef _ -> false + | VarRef _ -> assert false + +let modpath_of_r r = match r with + | ConstRef kn -> con_modpath kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> modpath kn + | VarRef _ -> assert false + +let label_of_r r = match r with + | ConstRef kn -> con_label kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> label kn | VarRef _ -> assert false let current_toplevel () = fst (Lib.current_prefix ()) @@ -45,21 +58,22 @@ let at_toplevel mp = is_modfile mp || is_toplevel mp let visible_kn kn = at_toplevel (base_mp (modpath kn)) +let visible_con kn = at_toplevel (base_mp (con_modpath kn)) (*S The main tables: constants, inductives, records, ... *) (*s Constants tables. *) -let terms = ref (KNmap.empty : ml_decl KNmap.t) -let init_terms () = terms := KNmap.empty -let add_term kn d = terms := KNmap.add kn d !terms -let lookup_term kn = KNmap.find kn !terms +let terms = ref (Cmap.empty : ml_decl Cmap.t) +let init_terms () = terms := Cmap.empty +let add_term kn d = terms := Cmap.add kn d !terms +let lookup_term kn = Cmap.find kn !terms -let types = ref (KNmap.empty : ml_schema KNmap.t) -let init_types () = types := KNmap.empty -let add_type kn s = types := KNmap.add kn s !types -let lookup_type kn = KNmap.find kn !types +let types = ref (Cmap.empty : ml_schema Cmap.t) +let init_types () = types := Cmap.empty +let add_type kn s = types := Cmap.add kn s !types +let lookup_type kn = Cmap.find kn !types (*s Inductives table. *) @@ -70,22 +84,22 @@ let lookup_ind kn = KNmap.find kn !inductives (*s Recursors table. *) -let recursors = ref KNset.empty -let init_recursors () = recursors := KNset.empty +let recursors = ref Cset.empty +let init_recursors () = recursors := Cset.empty let add_recursors env kn = - let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in + let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in let mib = Environ.lookup_mind kn env in Array.iter (fun mip -> let id = mip.mind_typename in let kn_rec = make_kn (Nameops.add_suffix id "_rec") and kn_rect = make_kn (Nameops.add_suffix id "_rect") in - recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) + recursors := Cset.add kn_rec (Cset.add kn_rect !recursors)) mib.mind_packets let is_recursor = function - | ConstRef kn -> KNset.mem kn !recursors + | ConstRef kn -> Cset.mem kn !recursors | _ -> false (*s Record tables. *) @@ -109,7 +123,7 @@ let reset_tables () = done before. *) let id_of_global = function - | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) | _ -> assert false @@ -126,16 +140,14 @@ let error_axiom_scheme r i = str " type variable(s).") let warning_info_ax r = - Options.if_verbose msg_warning - (str "You must realize axiom " ++ - pr_global r ++ str " in the extracted code.") + msg_warning (str "You must realize axiom " ++ + pr_global r ++ str " in the extracted code.") let warning_log_ax r = - Options.if_verbose msg_warning - (str "This extraction depends on logical axiom" ++ spc () ++ - pr_global r ++ str "." ++ spc() ++ - str "Having false logical axiom in the environment when extracting" ++ - spc () ++ str "may lead to incorrect or non-terminating ML terms.") + msg_warning (str "This extraction depends on logical axiom" ++ spc () ++ + pr_global r ++ str "." ++ spc() ++ + str "Having false logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms.") let check_inside_module () = try @@ -207,6 +219,18 @@ let _ = declare_bool_option optread = auto_inline; optwrite = (:=) auto_inline_ref} +(*s Extraction TypeExpand *) + +let type_expand_ref = ref true + +let type_expand () = !type_expand_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction TypeExpand"; + optkey = SecondaryTable ("Extraction", "TypeExpand"); + optread = type_expand; + optwrite = (:=) type_expand_ref} (*s Extraction Optimize *) @@ -311,14 +335,22 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let (inline_extraction,_) = +let (inline_extraction,_) = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); export_function = (fun x -> Some x); classify_function = (fun (_,o) -> Substitute o); - subst_function = (fun (_,s,(b,l)) -> (b,(List.map (subst_global s) l))) } + (*CSC: The following substitution may istantiate a realized parameter. + The right solution would be to make the substitution erase the + realizer from the table. However, this is not allowed by Coq. + In this particular case, though, keeping the realizer is place seems + to be harmless since the current code looks for a realizer only + when the constant is a parameter. However, if this behaviour changes + subtle bugs can happear in the future. *) + subst_function = + (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))} let _ = declare_summary "Extraction Inline" { freeze_function = (fun () -> !inline_table); @@ -409,7 +441,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Environ.constant_type env kn in + let typ = Typeops.type_of_constant env kn in let typ = Reduction.whd_betadeltaiota env typ in if Reduction.is_arity env typ then begin diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 6160452a..66662138 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) +(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*) open Names open Libnames @@ -35,7 +35,9 @@ val check_inside_section : unit -> unit (*s utilities concerning [module_path]. *) -val kn_of_r : global_reference -> kernel_name +val occur_kn_in_ref : kernel_name -> global_reference -> bool +val modpath_of_r : global_reference -> module_path +val label_of_r : global_reference -> label val current_toplevel : unit -> module_path val base_mp : module_path -> module_path @@ -43,14 +45,15 @@ val is_modfile : module_path -> bool val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool +val visible_con : constant -> bool (*s Some table-related operations *) -val add_term : kernel_name -> ml_decl -> unit -val lookup_term : kernel_name -> ml_decl +val add_term : constant -> ml_decl -> unit +val lookup_term : constant -> ml_decl -val add_type : kernel_name -> ml_schema -> unit -val lookup_type : kernel_name -> ml_schema +val add_type : constant -> ml_schema -> unit +val lookup_type : constant -> ml_schema val add_ind : kernel_name -> ml_ind -> unit val lookup_ind : kernel_name -> ml_ind @@ -58,7 +61,7 @@ val lookup_ind : kernel_name -> ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool -val add_projection : int -> kernel_name -> unit +val add_projection : int -> constant -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int @@ -68,6 +71,10 @@ val reset_tables : unit -> unit val auto_inline : unit -> bool +(*s TypeExpand parameter *) + +val type_expand : unit -> bool + (*s Optimize parameter *) type opt_flag = diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index 641b50a7..31d46eeb 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -2,110 +2,318 @@ theories/Arith/arith.cmo: theories/Arith/arith.cmi theories/Arith/arith.cmx: theories/Arith/arith.cmi theories/Arith/between.cmo: theories/Arith/between.cmi theories/Arith/between.cmx: theories/Arith/between.cmi -theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmi \ - theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi \ +theories/Arith/bool_nat.cmo: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Arith/peano_dec.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \ theories/Arith/bool_nat.cmi -theories/Arith/bool_nat.cmx: theories/Arith/compare_dec.cmx \ - theories/Init/datatypes.cmx theories/Arith/peano_dec.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx \ +theories/Arith/bool_nat.cmx: theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/Arith/peano_dec.cmx \ + theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \ theories/Arith/bool_nat.cmi -theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Arith/compare_dec.cmi -theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Arith/compare_dec.cmi -theories/Arith/compare.cmo: theories/Arith/compare_dec.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Arith/compare_dec.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi +theories/Arith/compare_dec.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Arith/compare_dec.cmi +theories/Arith/compare.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \ theories/Arith/compare.cmi -theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \ - theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Arith/compare.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \ theories/Arith/compare.cmi -theories/Arith/div2.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi \ - theories/Init/specif.cmi theories/Arith/div2.cmi -theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx \ - theories/Init/specif.cmx theories/Arith/div2.cmi -theories/Arith/eqNat.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Arith/eqNat.cmi -theories/Arith/eqNat.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Arith/eqNat.cmi -theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Arith/div2.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Arith/div2.cmi +theories/Arith/div2.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/Arith/div2.cmi +theories/Arith/eqNat.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Arith/eqNat.cmi +theories/Arith/eqNat.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Arith/eqNat.cmi +theories/Arith/euclid.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \ theories/Arith/euclid.cmi -theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \ - theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Arith/euclid.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \ theories/Arith/euclid.cmi -theories/Arith/even.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Arith/even.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ theories/Arith/even.cmi -theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Arith/even.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ theories/Arith/even.cmi -theories/Arith/factorial.cmo: theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Arith/factorial.cmi -theories/Arith/factorial.cmx: theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Arith/factorial.cmi +theories/Arith/factorial.cmo: theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Arith/factorial.cmi +theories/Arith/factorial.cmx: theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/Arith/factorial.cmi theories/Arith/gt.cmo: theories/Arith/gt.cmi theories/Arith/gt.cmx: theories/Arith/gt.cmi theories/Arith/le.cmo: theories/Arith/le.cmi theories/Arith/le.cmx: theories/Arith/le.cmi theories/Arith/lt.cmo: theories/Arith/lt.cmi theories/Arith/lt.cmx: theories/Arith/lt.cmi -theories/Arith/max.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Arith/max.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ theories/Arith/max.cmi -theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Arith/max.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ theories/Arith/max.cmi -theories/Arith/min.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Arith/min.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ theories/Arith/min.cmi -theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Arith/min.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ theories/Arith/min.cmi theories/Arith/minus.cmo: theories/Arith/minus.cmi theories/Arith/minus.cmx: theories/Arith/minus.cmi -theories/Arith/mult.cmo: theories/Init/datatypes.cmi theories/Arith/plus.cmi \ +theories/Arith/mult.cmo: theories/Arith/plus.cmi theories/Init/datatypes.cmi \ theories/Arith/mult.cmi -theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx \ +theories/Arith/mult.cmx: theories/Arith/plus.cmx theories/Init/datatypes.cmx \ theories/Arith/mult.cmi -theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Arith/peano_dec.cmi -theories/Arith/peano_dec.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Arith/peano_dec.cmi -theories/Arith/plus.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Arith/peano_dec.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi +theories/Arith/peano_dec.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Arith/peano_dec.cmi +theories/Arith/plus.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ theories/Arith/plus.cmi -theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Arith/plus.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ theories/Arith/plus.cmi theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmi \ theories/Arith/wf_nat.cmi theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx \ theories/Arith/wf_nat.cmi -theories/Bool/boolEq.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Bool/boolEq.cmi -theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Bool/boolEq.cmi -theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Bool/boolEq.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Bool/boolEq.cmi +theories/Bool/boolEq.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Bool/boolEq.cmi +theories/Bool/bool.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ theories/Bool/bool.cmi -theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Bool/bool.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ theories/Bool/bool.cmi -theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Bool/bvector.cmi -theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Bool/bvector.cmi +theories/Bool/bvector.cmo: theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Bool/bool.cmi \ + theories/Bool/bvector.cmi +theories/Bool/bvector.cmx: theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/Bool/bool.cmx \ + theories/Bool/bvector.cmi theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi -theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Bool/ifProp.cmi -theories/Bool/ifProp.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Bool/ifProp.cmi -theories/Bool/sumbool.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi -theories/Bool/sumbool.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmi +theories/Bool/ifProp.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Bool/ifProp.cmi +theories/Bool/ifProp.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Bool/ifProp.cmi +theories/Bool/sumbool.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Bool/sumbool.cmi +theories/Bool/sumbool.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Bool/sumbool.cmi theories/Bool/zerob.cmo: theories/Init/datatypes.cmi theories/Bool/zerob.cmi theories/Bool/zerob.cmx: theories/Init/datatypes.cmx theories/Bool/zerob.cmi +theories/FSets/decidableTypeEx.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedTypeEx.cmi theories/FSets/orderedType.cmi \ + theories/Init/datatypes.cmi theories/FSets/decidableTypeEx.cmi +theories/FSets/decidableTypeEx.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedTypeEx.cmx theories/FSets/orderedType.cmx \ + theories/Init/datatypes.cmx theories/FSets/decidableTypeEx.cmi +theories/FSets/decidableType.cmo: theories/Init/specif.cmi \ + theories/FSets/decidableType.cmi +theories/FSets/decidableType.cmx: theories/Init/specif.cmx \ + theories/FSets/decidableType.cmi +theories/FSets/fMapAVL.cmo: theories/Init/wf.cmi theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/FSets/int.cmi theories/FSets/fMapList.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/FSets/fMapAVL.cmi +theories/FSets/fMapAVL.cmx: theories/Init/wf.cmx theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/FSets/int.cmx theories/FSets/fMapList.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/FSets/fMapAVL.cmi +theories/FSets/fMapFacts.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/FSets/fMapInterface.cmi \ + theories/Init/datatypes.cmi theories/FSets/fMapFacts.cmi +theories/FSets/fMapFacts.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/FSets/fMapInterface.cmx \ + theories/Init/datatypes.cmx theories/FSets/fMapFacts.cmi +theories/FSets/fMapInterface.cmo: theories/FSets/orderedType.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi \ + theories/FSets/fMapInterface.cmi +theories/FSets/fMapInterface.cmx: theories/FSets/orderedType.cmx \ + theories/Lists/list.cmx theories/Init/datatypes.cmx \ + theories/FSets/fMapInterface.cmi +theories/FSets/fMapIntMap.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/NArith/ndigits.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/mapcanon.cmi \ + theories/IntMap/map.cmi theories/Lists/list.cmi \ + theories/FSets/fMapList.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi theories/FSets/fMapIntMap.cmi +theories/FSets/fMapIntMap.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/NArith/ndigits.cmx \ + theories/IntMap/mapiter.cmx theories/IntMap/mapcanon.cmx \ + theories/IntMap/map.cmx theories/Lists/list.cmx \ + theories/FSets/fMapList.cmx theories/Init/datatypes.cmx \ + theories/NArith/binNat.cmx theories/FSets/fMapIntMap.cmi +theories/FSets/fMapList.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/FSets/fMapList.cmi +theories/FSets/fMapList.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/FSets/fMapList.cmi +theories/FSets/fMapPositive.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/FSets/fMapPositive.cmi +theories/FSets/fMapPositive.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/FSets/fMapPositive.cmi +theories/FSets/fMaps.cmo: theories/FSets/fMaps.cmi +theories/FSets/fMaps.cmx: theories/FSets/fMaps.cmi +theories/FSets/fMapWeakFacts.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/FSets/fMapWeakInterface.cmi \ + theories/Init/datatypes.cmi theories/FSets/fMapWeakFacts.cmi +theories/FSets/fMapWeakFacts.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/FSets/fMapWeakInterface.cmx \ + theories/Init/datatypes.cmx theories/FSets/fMapWeakFacts.cmi +theories/FSets/fMapWeakInterface.cmo: theories/Lists/list.cmi \ + theories/FSets/decidableType.cmi theories/Init/datatypes.cmi \ + theories/FSets/fMapWeakInterface.cmi +theories/FSets/fMapWeakInterface.cmx: theories/Lists/list.cmx \ + theories/FSets/decidableType.cmx theories/Init/datatypes.cmx \ + theories/FSets/fMapWeakInterface.cmi +theories/FSets/fMapWeakList.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/FSets/decidableType.cmi \ + theories/Init/datatypes.cmi theories/FSets/fMapWeakList.cmi +theories/FSets/fMapWeakList.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/FSets/decidableType.cmx \ + theories/Init/datatypes.cmx theories/FSets/fMapWeakList.cmi +theories/FSets/fMapWeak.cmo: theories/FSets/fMapWeak.cmi +theories/FSets/fMapWeak.cmx: theories/FSets/fMapWeak.cmi +theories/FSets/fSetAVL.cmo: theories/Init/wf.cmi theories/Init/specif.cmi \ + theories/Init/peano.cmi theories/FSets/orderedType.cmi \ + theories/Lists/list.cmi theories/FSets/int.cmi \ + theories/FSets/fSetList.cmi theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \ + theories/FSets/fSetAVL.cmi +theories/FSets/fSetAVL.cmx: theories/Init/wf.cmx theories/Init/specif.cmx \ + theories/Init/peano.cmx theories/FSets/orderedType.cmx \ + theories/Lists/list.cmx theories/FSets/int.cmx \ + theories/FSets/fSetList.cmx theories/Init/datatypes.cmx \ + theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \ + theories/FSets/fSetAVL.cmi +theories/FSets/fSetBridge.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \ + theories/FSets/fSetBridge.cmi +theories/FSets/fSetBridge.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/FSets/fSetInterface.cmx theories/Init/datatypes.cmx \ + theories/FSets/fSetBridge.cmi +theories/FSets/fSetEqProperties.cmo: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/Init/peano.cmi \ + theories/FSets/orderedType.cmi theories/FSets/fSetProperties.cmi \ + theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \ + theories/Bool/bool.cmi theories/FSets/fSetEqProperties.cmi +theories/FSets/fSetEqProperties.cmx: theories/Init/specif.cmx \ + theories/Setoids/setoid.cmx theories/Init/peano.cmx \ + theories/FSets/orderedType.cmx theories/FSets/fSetProperties.cmx \ + theories/FSets/fSetInterface.cmx theories/Init/datatypes.cmx \ + theories/Bool/bool.cmx theories/FSets/fSetEqProperties.cmi +theories/FSets/fSetFacts.cmo: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/orderedType.cmi \ + theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \ + theories/FSets/fSetFacts.cmi +theories/FSets/fSetFacts.cmx: theories/Init/specif.cmx \ + theories/Setoids/setoid.cmx theories/FSets/orderedType.cmx \ + theories/FSets/fSetInterface.cmx theories/Init/datatypes.cmx \ + theories/FSets/fSetFacts.cmi +theories/FSets/fSetInterface.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/FSets/fSetInterface.cmi +theories/FSets/fSetInterface.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/FSets/fSetInterface.cmi +theories/FSets/fSetList.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/FSets/fSetList.cmi +theories/FSets/fSetList.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/FSets/fSetList.cmi +theories/FSets/fSetProperties.cmo: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/orderedType.cmi \ + theories/Lists/list.cmi theories/FSets/fSetInterface.cmi \ + theories/FSets/fSetFacts.cmi theories/Init/datatypes.cmi \ + theories/FSets/fSetProperties.cmi +theories/FSets/fSetProperties.cmx: theories/Init/specif.cmx \ + theories/Setoids/setoid.cmx theories/FSets/orderedType.cmx \ + theories/Lists/list.cmx theories/FSets/fSetInterface.cmx \ + theories/FSets/fSetFacts.cmx theories/Init/datatypes.cmx \ + theories/FSets/fSetProperties.cmi +theories/FSets/fSets.cmo: theories/FSets/fSets.cmi +theories/FSets/fSets.cmx: theories/FSets/fSets.cmi +theories/FSets/fSetToFiniteSet.cmo: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/orderedTypeEx.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/FSets/fSetProperties.cmi theories/Init/datatypes.cmi \ + theories/FSets/fSetToFiniteSet.cmi +theories/FSets/fSetToFiniteSet.cmx: theories/Init/specif.cmx \ + theories/Setoids/setoid.cmx theories/FSets/orderedTypeEx.cmx \ + theories/FSets/orderedType.cmx theories/Lists/list.cmx \ + theories/FSets/fSetProperties.cmx theories/Init/datatypes.cmx \ + theories/FSets/fSetToFiniteSet.cmi +theories/FSets/fSetWeakFacts.cmo: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/fSetWeakInterface.cmi \ + theories/Init/datatypes.cmi theories/FSets/fSetWeakFacts.cmi +theories/FSets/fSetWeakFacts.cmx: theories/Init/specif.cmx \ + theories/Setoids/setoid.cmx theories/FSets/fSetWeakInterface.cmx \ + theories/Init/datatypes.cmx theories/FSets/fSetWeakFacts.cmi +theories/FSets/fSetWeakInterface.cmo: theories/Lists/list.cmi \ + theories/FSets/decidableType.cmi theories/Init/datatypes.cmi \ + theories/FSets/fSetWeakInterface.cmi +theories/FSets/fSetWeakInterface.cmx: theories/Lists/list.cmx \ + theories/FSets/decidableType.cmx theories/Init/datatypes.cmx \ + theories/FSets/fSetWeakInterface.cmi +theories/FSets/fSetWeakList.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/FSets/decidableType.cmi \ + theories/Init/datatypes.cmi theories/FSets/fSetWeakList.cmi +theories/FSets/fSetWeakList.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/FSets/decidableType.cmx \ + theories/Init/datatypes.cmx theories/FSets/fSetWeakList.cmi +theories/FSets/fSetWeak.cmo: theories/FSets/fSetWeak.cmi +theories/FSets/fSetWeak.cmx: theories/FSets/fSetWeak.cmi +theories/FSets/fSetWeakProperties.cmo: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/Lists/list.cmi \ + theories/FSets/fSetWeakInterface.cmi theories/FSets/fSetWeakFacts.cmi \ + theories/Init/datatypes.cmi theories/FSets/fSetWeakProperties.cmi +theories/FSets/fSetWeakProperties.cmx: theories/Init/specif.cmx \ + theories/Setoids/setoid.cmx theories/Lists/list.cmx \ + theories/FSets/fSetWeakInterface.cmx theories/FSets/fSetWeakFacts.cmx \ + theories/Init/datatypes.cmx theories/FSets/fSetWeakProperties.cmi +theories/FSets/int.cmo: theories/ZArith/zmax.cmi \ + theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \ + theories/FSets/int.cmi +theories/FSets/int.cmx: theories/ZArith/zmax.cmx \ + theories/ZArith/zArith_dec.cmx theories/Init/specif.cmx \ + theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \ + theories/FSets/int.cmi +theories/FSets/orderedTypeAlt.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Init/datatypes.cmi \ + theories/FSets/orderedTypeAlt.cmi +theories/FSets/orderedTypeAlt.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Init/datatypes.cmx \ + theories/FSets/orderedTypeAlt.cmi +theories/FSets/orderedTypeEx.cmo: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Init/datatypes.cmi \ + theories/Arith/compare_dec.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi theories/ZArith/binInt.cmi \ + theories/FSets/orderedTypeEx.cmi +theories/FSets/orderedTypeEx.cmx: theories/Init/specif.cmx \ + theories/FSets/orderedType.cmx theories/Init/datatypes.cmx \ + theories/Arith/compare_dec.cmx theories/NArith/binPos.cmx \ + theories/NArith/binNat.cmx theories/ZArith/binInt.cmx \ + theories/FSets/orderedTypeEx.cmi +theories/FSets/orderedType.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/FSets/orderedType.cmi +theories/FSets/orderedType.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/FSets/orderedType.cmi theories/Init/datatypes.cmo: theories/Init/datatypes.cmi theories/Init/datatypes.cmx: theories/Init/datatypes.cmi theories/Init/logic.cmo: theories/Init/logic.cmi theories/Init/logic.cmx: theories/Init/logic.cmi -theories/Init/logic_Type.cmo: theories/Init/datatypes.cmi \ - theories/Init/logic_Type.cmi -theories/Init/logic_Type.cmx: theories/Init/datatypes.cmx \ - theories/Init/logic_Type.cmi +theories/Init/logic_Type.cmo: theories/Init/logic_Type.cmi +theories/Init/logic_Type.cmx: theories/Init/logic_Type.cmi theories/Init/notations.cmo: theories/Init/notations.cmi theories/Init/notations.cmx: theories/Init/notations.cmi theories/Init/peano.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi @@ -116,152 +324,146 @@ theories/Init/specif.cmo: theories/Init/datatypes.cmi \ theories/Init/specif.cmi theories/Init/specif.cmx: theories/Init/datatypes.cmx \ theories/Init/specif.cmi +theories/Init/tactics.cmo: theories/Init/tactics.cmi +theories/Init/tactics.cmx: theories/Init/tactics.cmi theories/Init/wf.cmo: theories/Init/wf.cmi theories/Init/wf.cmx: theories/Init/wf.cmi -theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/NArith/binPos.cmi \ - theories/Init/datatypes.cmi theories/IntMap/map.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi \ - theories/IntMap/adalloc.cmi -theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \ - theories/IntMap/addr.cmx theories/NArith/binPos.cmx \ - theories/Init/datatypes.cmx theories/IntMap/map.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx \ - theories/IntMap/adalloc.cmi -theories/IntMap/addec.cmo: theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi \ - theories/IntMap/addec.cmi -theories/IntMap/addec.cmx: theories/IntMap/addr.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx \ - theories/IntMap/addec.cmi -theories/IntMap/addr.cmo: theories/NArith/binPos.cmi theories/Bool/bool.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ - theories/IntMap/addr.cmi -theories/IntMap/addr.cmx: theories/NArith/binPos.cmx theories/Bool/bool.cmx \ - theories/Init/datatypes.cmx theories/Init/specif.cmx \ - theories/IntMap/addr.cmi -theories/IntMap/adist.cmo: theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/IntMap/adist.cmi -theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/IntMap/adist.cmi +theories/IntMap/adalloc.cmo: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/NArith/ndec.cmi theories/IntMap/map.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi theories/IntMap/adalloc.cmi +theories/IntMap/adalloc.cmx: theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/NArith/ndec.cmx theories/IntMap/map.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/NArith/binNat.cmx theories/IntMap/adalloc.cmi theories/IntMap/allmaps.cmo: theories/IntMap/allmaps.cmi theories/IntMap/allmaps.cmx: theories/IntMap/allmaps.cmi -theories/IntMap/fset.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ - theories/Init/datatypes.cmi theories/IntMap/map.cmi \ - theories/Init/specif.cmi theories/IntMap/fset.cmi -theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ - theories/Init/datatypes.cmx theories/IntMap/map.cmx \ - theories/Init/specif.cmx theories/IntMap/fset.cmi -theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Bool/bool.cmi \ - theories/Init/datatypes.cmi theories/Lists/list.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi \ - theories/IntMap/lsort.cmi -theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ - theories/NArith/binPos.cmx theories/Bool/bool.cmx \ - theories/Init/datatypes.cmx theories/Lists/list.cmx \ - theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx \ - theories/IntMap/lsort.cmi +theories/IntMap/fset.cmo: theories/Init/specif.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/IntMap/map.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi theories/IntMap/fset.cmi +theories/IntMap/fset.cmx: theories/Init/specif.cmx \ + theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \ + theories/IntMap/map.cmx theories/Init/datatypes.cmx \ + theories/NArith/binNat.cmx theories/IntMap/fset.cmi +theories/IntMap/lsort.cmo: theories/Bool/sumbool.cmi theories/Init/specif.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi theories/IntMap/lsort.cmi +theories/IntMap/lsort.cmx: theories/Bool/sumbool.cmx theories/Init/specif.cmx \ + theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \ + theories/IntMap/mapiter.cmx theories/IntMap/map.cmx \ + theories/Lists/list.cmx theories/Init/datatypes.cmx \ + theories/NArith/binNat.cmx theories/IntMap/lsort.cmi theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi -theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \ - theories/Init/specif.cmi theories/IntMap/mapcanon.cmi -theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \ - theories/Init/specif.cmx theories/IntMap/mapcanon.cmi -theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/IntMap/map.cmi theories/Init/peano.cmi \ - theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi \ - theories/IntMap/mapcard.cmi -theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \ - theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ - theories/IntMap/map.cmx theories/Init/peano.cmx \ - theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx \ - theories/IntMap/mapcard.cmi +theories/IntMap/mapcanon.cmo: theories/Init/specif.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapcanon.cmi +theories/IntMap/mapcanon.cmx: theories/Init/specif.cmx \ + theories/IntMap/map.cmx theories/IntMap/mapcanon.cmi +theories/IntMap/mapcard.cmo: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Arith/plus.cmi \ + theories/Arith/peano_dec.cmi theories/Init/peano.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/IntMap/map.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi theories/IntMap/mapcard.cmi +theories/IntMap/mapcard.cmx: theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/Arith/plus.cmx \ + theories/Arith/peano_dec.cmx theories/Init/peano.cmx \ + theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \ + theories/IntMap/map.cmx theories/Init/datatypes.cmx \ + theories/NArith/binNat.cmx theories/IntMap/mapcard.cmi theories/IntMap/mapc.cmo: theories/IntMap/mapc.cmi theories/IntMap/mapc.cmx: theories/IntMap/mapc.cmi -theories/IntMap/mapfold.cmo: theories/IntMap/addr.cmi \ - theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ - theories/Init/specif.cmi theories/IntMap/mapfold.cmi -theories/IntMap/mapfold.cmx: theories/IntMap/addr.cmx \ - theories/Init/datatypes.cmx theories/IntMap/fset.cmx \ - theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ - theories/Init/specif.cmx theories/IntMap/mapfold.cmi -theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/IntMap/map.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/IntMap/mapiter.cmi -theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \ - theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ - theories/Lists/list.cmx theories/IntMap/map.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx theories/IntMap/mapiter.cmi -theories/IntMap/maplists.cmo: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/IntMap/fset.cmi theories/Lists/list.cmi theories/IntMap/map.cmi \ - theories/IntMap/mapiter.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/IntMap/maplists.cmi -theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \ - theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ - theories/IntMap/fset.cmx theories/Lists/list.cmx theories/IntMap/map.cmx \ - theories/IntMap/mapiter.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx theories/IntMap/maplists.cmi -theories/IntMap/map.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi theories/IntMap/map.cmi -theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Init/specif.cmx theories/IntMap/map.cmi -theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmi \ - theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ +theories/IntMap/mapfold.cmo: theories/Init/specif.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \ + theories/IntMap/fset.cmi theories/Init/datatypes.cmi \ + theories/IntMap/mapfold.cmi +theories/IntMap/mapfold.cmx: theories/Init/specif.cmx \ + theories/IntMap/mapiter.cmx theories/IntMap/map.cmx \ + theories/IntMap/fset.cmx theories/Init/datatypes.cmx \ + theories/IntMap/mapfold.cmi +theories/IntMap/mapiter.cmo: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/NArith/ndigits.cmi \ + theories/NArith/ndec.cmi theories/IntMap/map.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binNat.cmi \ + theories/IntMap/mapiter.cmi +theories/IntMap/mapiter.cmx: theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/NArith/ndigits.cmx \ + theories/NArith/ndec.cmx theories/IntMap/map.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/NArith/binNat.cmx \ + theories/IntMap/mapiter.cmi +theories/IntMap/maplists.cmo: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/NArith/ndec.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \ + theories/Lists/list.cmi theories/IntMap/fset.cmi \ + theories/Init/datatypes.cmi theories/IntMap/maplists.cmi +theories/IntMap/maplists.cmx: theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/NArith/ndec.cmx \ + theories/IntMap/mapiter.cmx theories/IntMap/map.cmx \ + theories/Lists/list.cmx theories/IntMap/fset.cmx \ + theories/Init/datatypes.cmx theories/IntMap/maplists.cmi +theories/IntMap/map.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi theories/IntMap/map.cmi +theories/IntMap/map.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/NArith/ndigits.cmx theories/NArith/ndec.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/NArith/binNat.cmx theories/IntMap/map.cmi +theories/IntMap/mapsubset.cmo: theories/IntMap/mapiter.cmi \ + theories/IntMap/map.cmi theories/IntMap/fset.cmi \ + theories/Init/datatypes.cmi theories/Bool/bool.cmi \ theories/IntMap/mapsubset.cmi -theories/IntMap/mapsubset.cmx: theories/Bool/bool.cmx \ - theories/Init/datatypes.cmx theories/IntMap/fset.cmx \ - theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ +theories/IntMap/mapsubset.cmx: theories/IntMap/mapiter.cmx \ + theories/IntMap/map.cmx theories/IntMap/fset.cmx \ + theories/Init/datatypes.cmx theories/Bool/bool.cmx \ theories/IntMap/mapsubset.cmi -theories/Lists/list.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/Lists/list.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ theories/Lists/list.cmi -theories/Lists/list.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/Lists/list.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ theories/Lists/list.cmi -theories/Lists/listSet.cmo: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Init/specif.cmi \ - theories/Lists/listSet.cmi -theories/Lists/listSet.cmx: theories/Init/datatypes.cmx \ - theories/Lists/list.cmx theories/Init/specif.cmx \ - theories/Lists/listSet.cmi +theories/Lists/listSet.cmo: theories/Init/specif.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/Lists/listSet.cmi +theories/Lists/listSet.cmx: theories/Init/specif.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/Lists/listSet.cmi theories/Lists/monoList.cmo: theories/Init/datatypes.cmi \ theories/Lists/monoList.cmi theories/Lists/monoList.cmx: theories/Init/datatypes.cmx \ theories/Lists/monoList.cmi +theories/Lists/setoidList.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi \ + theories/Lists/setoidList.cmi +theories/Lists/setoidList.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/Init/datatypes.cmx \ + theories/Lists/setoidList.cmi theories/Lists/streams.cmo: theories/Init/datatypes.cmi \ theories/Lists/streams.cmi theories/Lists/streams.cmx: theories/Init/datatypes.cmx \ theories/Lists/streams.cmi -theories/Lists/theoryList.cmo: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Init/specif.cmi \ +theories/Lists/theoryList.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi \ theories/Lists/theoryList.cmi -theories/Lists/theoryList.cmx: theories/Init/datatypes.cmx \ - theories/Lists/list.cmx theories/Init/specif.cmx \ +theories/Lists/theoryList.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/Init/datatypes.cmx \ theories/Lists/theoryList.cmi theories/Logic/berardi.cmo: theories/Logic/berardi.cmi theories/Logic/berardi.cmx: theories/Logic/berardi.cmi -theories/Logic/choiceFacts.cmo: theories/Logic/choiceFacts.cmi -theories/Logic/choiceFacts.cmx: theories/Logic/choiceFacts.cmi +theories/Logic/choiceFacts.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Logic/choiceFacts.cmi +theories/Logic/choiceFacts.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Logic/choiceFacts.cmi theories/Logic/classicalChoice.cmo: theories/Logic/classicalChoice.cmi theories/Logic/classicalChoice.cmx: theories/Logic/classicalChoice.cmi -theories/Logic/classicalDescription.cmo: \ - theories/Logic/classicalDescription.cmi -theories/Logic/classicalDescription.cmx: \ - theories/Logic/classicalDescription.cmi +theories/Logic/classicalDescription.cmo: theories/Init/specif.cmi \ + theories/Logic/choiceFacts.cmi theories/Logic/classicalDescription.cmi +theories/Logic/classicalDescription.cmx: theories/Init/specif.cmx \ + theories/Logic/choiceFacts.cmx theories/Logic/classicalDescription.cmi +theories/Logic/classicalEpsilon.cmo: theories/Init/specif.cmi \ + theories/Logic/choiceFacts.cmi theories/Logic/classicalEpsilon.cmi +theories/Logic/classicalEpsilon.cmx: theories/Init/specif.cmx \ + theories/Logic/choiceFacts.cmx theories/Logic/classicalEpsilon.cmi theories/Logic/classicalFacts.cmo: theories/Logic/classicalFacts.cmi theories/Logic/classicalFacts.cmx: theories/Logic/classicalFacts.cmi theories/Logic/classical.cmo: theories/Logic/classical.cmi @@ -272,38 +474,118 @@ theories/Logic/classical_Pred_Type.cmo: \ theories/Logic/classical_Pred_Type.cmi theories/Logic/classical_Pred_Type.cmx: \ theories/Logic/classical_Pred_Type.cmi -theories/Logic/classical_Prop.cmo: theories/Logic/classical_Prop.cmi -theories/Logic/classical_Prop.cmx: theories/Logic/classical_Prop.cmi +theories/Logic/classical_Prop.cmo: theories/Logic/eqdepFacts.cmi \ + theories/Logic/classical_Prop.cmi +theories/Logic/classical_Prop.cmx: theories/Logic/eqdepFacts.cmx \ + theories/Logic/classical_Prop.cmi theories/Logic/classical_Type.cmo: theories/Logic/classical_Type.cmi theories/Logic/classical_Type.cmx: theories/Logic/classical_Type.cmi +theories/Logic/classicalUniqueChoice.cmo: \ + theories/Logic/classicalUniqueChoice.cmi +theories/Logic/classicalUniqueChoice.cmx: \ + theories/Logic/classicalUniqueChoice.cmi theories/Logic/decidable.cmo: theories/Logic/decidable.cmi theories/Logic/decidable.cmx: theories/Logic/decidable.cmi -theories/Logic/diaconescu.cmo: theories/Logic/diaconescu.cmi -theories/Logic/diaconescu.cmx: theories/Logic/diaconescu.cmi -theories/Logic/eqdep_dec.cmo: theories/Logic/eqdep_dec.cmi -theories/Logic/eqdep_dec.cmx: theories/Logic/eqdep_dec.cmi -theories/Logic/eqdep.cmo: theories/Logic/eqdep.cmi -theories/Logic/eqdep.cmx: theories/Logic/eqdep.cmi +theories/Logic/diaconescu.cmo: theories/Init/specif.cmi \ + theories/Logic/diaconescu.cmi +theories/Logic/diaconescu.cmx: theories/Init/specif.cmx \ + theories/Logic/diaconescu.cmi +theories/Logic/eqdep_dec.cmo: theories/Init/specif.cmi \ + theories/Logic/eqdep_dec.cmi +theories/Logic/eqdep_dec.cmx: theories/Init/specif.cmx \ + theories/Logic/eqdep_dec.cmi +theories/Logic/eqdepFacts.cmo: theories/Logic/eqdepFacts.cmi +theories/Logic/eqdepFacts.cmx: theories/Logic/eqdepFacts.cmi +theories/Logic/eqdep.cmo: theories/Logic/eqdepFacts.cmi \ + theories/Logic/eqdep.cmi +theories/Logic/eqdep.cmx: theories/Logic/eqdepFacts.cmx \ + theories/Logic/eqdep.cmi theories/Logic/hurkens.cmo: theories/Logic/hurkens.cmi theories/Logic/hurkens.cmx: theories/Logic/hurkens.cmi theories/Logic/jMeq.cmo: theories/Logic/jMeq.cmi theories/Logic/jMeq.cmx: theories/Logic/jMeq.cmi -theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevance.cmi -theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevance.cmi +theories/Logic/proofIrrelevanceFacts.cmo: theories/Logic/eqdepFacts.cmi \ + theories/Logic/proofIrrelevanceFacts.cmi +theories/Logic/proofIrrelevanceFacts.cmx: theories/Logic/eqdepFacts.cmx \ + theories/Logic/proofIrrelevanceFacts.cmi +theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevanceFacts.cmi \ + theories/Logic/proofIrrelevance.cmi +theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevanceFacts.cmx \ + theories/Logic/proofIrrelevance.cmi theories/Logic/relationalChoice.cmo: theories/Logic/relationalChoice.cmi theories/Logic/relationalChoice.cmx: theories/Logic/relationalChoice.cmi -theories/NArith/binNat.cmo: theories/NArith/binPos.cmi \ - theories/Init/datatypes.cmi theories/NArith/binNat.cmi -theories/NArith/binNat.cmx: theories/NArith/binPos.cmx \ - theories/Init/datatypes.cmx theories/NArith/binNat.cmi -theories/NArith/binPos.cmo: theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/NArith/binPos.cmi -theories/NArith/binPos.cmx: theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/NArith/binPos.cmi +theories/NArith/binNat.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi +theories/NArith/binNat.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/NArith/binNat.cmi +theories/NArith/binPos.cmo: theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi +theories/NArith/binPos.cmx: theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmi theories/NArith/nArith.cmo: theories/NArith/nArith.cmi theories/NArith/nArith.cmx: theories/NArith/nArith.cmi +theories/NArith/ndec.cmo: theories/Bool/sumbool.cmi theories/Init/specif.cmi \ + theories/NArith/nnat.cmi theories/NArith/ndigits.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \ + theories/NArith/binPos.cmi theories/NArith/binNat.cmi \ + theories/NArith/ndec.cmi +theories/NArith/ndec.cmx: theories/Bool/sumbool.cmx theories/Init/specif.cmx \ + theories/NArith/nnat.cmx theories/NArith/ndigits.cmx \ + theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \ + theories/NArith/binPos.cmx theories/NArith/binNat.cmx \ + theories/NArith/ndec.cmi +theories/NArith/ndigits.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Bool/bvector.cmi \ + theories/Bool/bool.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi theories/NArith/ndigits.cmi +theories/NArith/ndigits.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Bool/bvector.cmx \ + theories/Bool/bool.cmx theories/NArith/binPos.cmx \ + theories/NArith/binNat.cmx theories/NArith/ndigits.cmi +theories/NArith/ndist.cmo: theories/NArith/ndigits.cmi theories/Arith/min.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi theories/NArith/ndist.cmi +theories/NArith/ndist.cmx: theories/NArith/ndigits.cmx theories/Arith/min.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/NArith/binNat.cmx theories/NArith/ndist.cmi +theories/NArith/nnat.cmo: theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/NArith/binNat.cmi \ + theories/NArith/nnat.cmi +theories/NArith/nnat.cmx: theories/Init/datatypes.cmx \ + theories/NArith/binPos.cmx theories/NArith/binNat.cmx \ + theories/NArith/nnat.cmi theories/NArith/pnat.cmo: theories/NArith/pnat.cmi theories/NArith/pnat.cmx: theories/NArith/pnat.cmi +theories/QArith/qArith_base.cmo: theories/ZArith/zArith_dec.cmi \ + theories/Init/specif.cmi theories/Setoids/setoid.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/QArith/qArith_base.cmi +theories/QArith/qArith_base.cmx: theories/ZArith/zArith_dec.cmx \ + theories/Init/specif.cmx theories/Setoids/setoid.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/QArith/qArith_base.cmi +theories/QArith/qArith.cmo: theories/QArith/qArith.cmi +theories/QArith/qArith.cmx: theories/QArith/qArith.cmi +theories/QArith/qreals.cmo: theories/QArith/qArith_base.cmi \ + theories/ZArith/binInt.cmi theories/QArith/qreals.cmi +theories/QArith/qreals.cmx: theories/QArith/qArith_base.cmx \ + theories/ZArith/binInt.cmx theories/QArith/qreals.cmi +theories/QArith/qreduction.cmo: theories/ZArith/znumtheory.cmi \ + theories/Setoids/setoid.cmi theories/QArith/qArith_base.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/QArith/qreduction.cmi +theories/QArith/qreduction.cmx: theories/ZArith/znumtheory.cmx \ + theories/Setoids/setoid.cmx theories/QArith/qArith_base.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/QArith/qreduction.cmi +theories/QArith/qring.cmo: theories/Init/specif.cmi \ + theories/QArith/qArith_base.cmi theories/Init/datatypes.cmi \ + theories/QArith/qring.cmi +theories/QArith/qring.cmx: theories/Init/specif.cmx \ + theories/QArith/qArith_base.cmx theories/Init/datatypes.cmx \ + theories/QArith/qring.cmi theories/Relations/newman.cmo: theories/Relations/newman.cmi theories/Relations/newman.cmx: theories/Relations/newman.cmi theories/Relations/operators_Properties.cmo: \ @@ -314,16 +596,18 @@ theories/Relations/relation_Definitions.cmo: \ theories/Relations/relation_Definitions.cmi theories/Relations/relation_Definitions.cmx: \ theories/Relations/relation_Definitions.cmi -theories/Relations/relation_Operators.cmo: theories/Lists/list.cmi \ - theories/Init/specif.cmi theories/Relations/relation_Operators.cmi -theories/Relations/relation_Operators.cmx: theories/Lists/list.cmx \ - theories/Init/specif.cmx theories/Relations/relation_Operators.cmi +theories/Relations/relation_Operators.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/Relations/relation_Operators.cmi +theories/Relations/relation_Operators.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/Relations/relation_Operators.cmi theories/Relations/relations.cmo: theories/Relations/relations.cmi theories/Relations/relations.cmx: theories/Relations/relations.cmi theories/Relations/rstar.cmo: theories/Relations/rstar.cmi theories/Relations/rstar.cmx: theories/Relations/rstar.cmi -theories/Setoids/setoid.cmo: theories/Setoids/setoid.cmi -theories/Setoids/setoid.cmx: theories/Setoids/setoid.cmi +theories/Setoids/setoid.cmo: theories/Init/datatypes.cmi \ + theories/Setoids/setoid.cmi +theories/Setoids/setoid.cmx: theories/Init/datatypes.cmx \ + theories/Setoids/setoid.cmi theories/Sets/classical_sets.cmo: theories/Sets/classical_sets.cmi theories/Sets/classical_sets.cmx: theories/Sets/classical_sets.cmi theories/Sets/constructive_sets.cmo: theories/Sets/constructive_sets.cmi @@ -340,20 +624,18 @@ theories/Sets/image.cmo: theories/Sets/image.cmi theories/Sets/image.cmx: theories/Sets/image.cmi theories/Sets/infinite_sets.cmo: theories/Sets/infinite_sets.cmi theories/Sets/infinite_sets.cmx: theories/Sets/infinite_sets.cmi -theories/Sets/integers.cmo: theories/Init/datatypes.cmi \ - theories/Sets/partial_Order.cmi theories/Sets/integers.cmi -theories/Sets/integers.cmx: theories/Init/datatypes.cmx \ - theories/Sets/partial_Order.cmx theories/Sets/integers.cmi -theories/Sets/multiset.cmo: theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi \ - theories/Sets/multiset.cmi -theories/Sets/multiset.cmx: theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Init/specif.cmx \ - theories/Sets/multiset.cmi -theories/Sets/partial_Order.cmo: theories/Sets/ensembles.cmi \ - theories/Sets/relations_1.cmi theories/Sets/partial_Order.cmi -theories/Sets/partial_Order.cmx: theories/Sets/ensembles.cmx \ - theories/Sets/relations_1.cmx theories/Sets/partial_Order.cmi +theories/Sets/integers.cmo: theories/Sets/partial_Order.cmi \ + theories/Init/datatypes.cmi theories/Sets/integers.cmi +theories/Sets/integers.cmx: theories/Sets/partial_Order.cmx \ + theories/Init/datatypes.cmx theories/Sets/integers.cmi +theories/Sets/multiset.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Sets/multiset.cmi +theories/Sets/multiset.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/Sets/multiset.cmi +theories/Sets/partial_Order.cmo: theories/Sets/relations_1.cmi \ + theories/Sets/ensembles.cmi theories/Sets/partial_Order.cmi +theories/Sets/partial_Order.cmx: theories/Sets/relations_1.cmx \ + theories/Sets/ensembles.cmx theories/Sets/partial_Order.cmi theories/Sets/permut.cmo: theories/Sets/permut.cmi theories/Sets/permut.cmx: theories/Sets/permut.cmi theories/Sets/powerset_Classical_facts.cmo: \ @@ -362,10 +644,10 @@ theories/Sets/powerset_Classical_facts.cmx: \ theories/Sets/powerset_Classical_facts.cmi theories/Sets/powerset_facts.cmo: theories/Sets/powerset_facts.cmi theories/Sets/powerset_facts.cmx: theories/Sets/powerset_facts.cmi -theories/Sets/powerset.cmo: theories/Sets/ensembles.cmi \ - theories/Sets/partial_Order.cmi theories/Sets/powerset.cmi -theories/Sets/powerset.cmx: theories/Sets/ensembles.cmx \ - theories/Sets/partial_Order.cmx theories/Sets/powerset.cmi +theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmi \ + theories/Sets/ensembles.cmi theories/Sets/powerset.cmi +theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx \ + theories/Sets/ensembles.cmx theories/Sets/powerset.cmi theories/Sets/relations_1_facts.cmo: theories/Sets/relations_1_facts.cmi theories/Sets/relations_1_facts.cmx: theories/Sets/relations_1_facts.cmi theories/Sets/relations_1.cmo: theories/Sets/relations_1.cmi @@ -378,30 +660,46 @@ theories/Sets/relations_3_facts.cmo: theories/Sets/relations_3_facts.cmi theories/Sets/relations_3_facts.cmx: theories/Sets/relations_3_facts.cmi theories/Sets/relations_3.cmo: theories/Sets/relations_3.cmi theories/Sets/relations_3.cmx: theories/Sets/relations_3.cmi -theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Sets/uniset.cmi -theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/Sets/uniset.cmi -theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Sets/multiset.cmi \ - theories/Init/peano.cmi theories/Sorting/sorting.cmi \ - theories/Init/specif.cmi theories/Sorting/heap.cmi -theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \ - theories/Lists/list.cmx theories/Sets/multiset.cmx \ - theories/Init/peano.cmx theories/Sorting/sorting.cmx \ - theories/Init/specif.cmx theories/Sorting/heap.cmi -theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Sets/multiset.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi \ +theories/Sets/uniset.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Sets/uniset.cmi +theories/Sets/uniset.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Sets/uniset.cmi +theories/Sorting/heap.cmo: theories/Init/specif.cmi \ + theories/Sorting/sorting.cmi theories/Init/peano.cmi \ + theories/Sets/multiset.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/Sorting/heap.cmi +theories/Sorting/heap.cmx: theories/Init/specif.cmx \ + theories/Sorting/sorting.cmx theories/Init/peano.cmx \ + theories/Sets/multiset.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/Sorting/heap.cmi +theories/Sorting/permutation.cmo: theories/Init/specif.cmi \ + theories/Init/peano.cmi theories/Sets/multiset.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi \ theories/Sorting/permutation.cmi -theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \ - theories/Lists/list.cmx theories/Sets/multiset.cmx \ - theories/Init/peano.cmx theories/Init/specif.cmx \ +theories/Sorting/permutation.cmx: theories/Init/specif.cmx \ + theories/Init/peano.cmx theories/Sets/multiset.cmx \ + theories/Lists/list.cmx theories/Init/datatypes.cmx \ theories/Sorting/permutation.cmi -theories/Sorting/sorting.cmo: theories/Lists/list.cmi \ - theories/Init/specif.cmi theories/Sorting/sorting.cmi -theories/Sorting/sorting.cmx: theories/Lists/list.cmx \ - theories/Init/specif.cmx theories/Sorting/sorting.cmi +theories/Sorting/permutEq.cmo: theories/Sorting/permutEq.cmi +theories/Sorting/permutEq.cmx: theories/Sorting/permutEq.cmi +theories/Sorting/permutSetoid.cmo: theories/Sorting/permutSetoid.cmi +theories/Sorting/permutSetoid.cmx: theories/Sorting/permutSetoid.cmi +theories/Sorting/sorting.cmo: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/Sorting/sorting.cmi +theories/Sorting/sorting.cmx: theories/Init/specif.cmx \ + theories/Lists/list.cmx theories/Sorting/sorting.cmi +theories/Strings/ascii.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Bool/bool.cmi \ + theories/NArith/binPos.cmi theories/Strings/ascii.cmi +theories/Strings/ascii.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/Bool/bool.cmx \ + theories/NArith/binPos.cmx theories/Strings/ascii.cmi +theories/Strings/string.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Strings/ascii.cmi \ + theories/Strings/string.cmi +theories/Strings/string.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/Strings/ascii.cmx \ + theories/Strings/string.cmi theories/Wellfounded/disjoint_Union.cmo: \ theories/Wellfounded/disjoint_Union.cmi theories/Wellfounded/disjoint_Union.cmx: \ @@ -434,280 +732,405 @@ theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx \ theories/Wellfounded/well_Ordering.cmi theories/ZArith/auxiliary.cmo: theories/ZArith/auxiliary.cmi theories/ZArith/auxiliary.cmx: theories/ZArith/auxiliary.cmi -theories/ZArith/binInt.cmo: theories/NArith/binNat.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ +theories/ZArith/binInt.cmo: theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/NArith/binNat.cmi \ theories/ZArith/binInt.cmi -theories/ZArith/binInt.cmx: theories/NArith/binNat.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ +theories/ZArith/binInt.cmx: theories/Init/datatypes.cmx \ + theories/NArith/binPos.cmx theories/NArith/binNat.cmx \ theories/ZArith/binInt.cmi -theories/ZArith/wf_Z.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi -theories/ZArith/wf_Z.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Init/specif.cmx theories/ZArith/wf_Z.cmi -theories/ZArith/zabs.cmo: theories/ZArith/binInt.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/ZArith/zabs.cmi -theories/ZArith/zabs.cmx: theories/ZArith/binInt.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx theories/ZArith/zabs.cmi +theories/ZArith/wf_Z.cmo: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/wf_Z.cmi +theories/ZArith/wf_Z.cmx: theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/wf_Z.cmi +theories/ZArith/zabs.cmo: theories/Init/specif.cmi theories/ZArith/binInt.cmi \ + theories/ZArith/zabs.cmi +theories/ZArith/zabs.cmx: theories/Init/specif.cmx theories/ZArith/binInt.cmx \ + theories/ZArith/zabs.cmi theories/ZArith/zArith_base.cmo: theories/ZArith/zArith_base.cmi theories/ZArith/zArith_base.cmx: theories/ZArith/zArith_base.cmi -theories/ZArith/zArith_dec.cmo: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi -theories/ZArith/zArith_dec.cmx: theories/ZArith/binInt.cmx \ - theories/Init/datatypes.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmi +theories/ZArith/zArith_dec.cmo: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zArith_dec.cmi +theories/ZArith/zArith_dec.cmx: theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/Init/datatypes.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zArith_dec.cmi theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi -theories/ZArith/zbinary.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Bool/bvector.cmi \ - theories/Init/datatypes.cmi theories/ZArith/zeven.cmi \ +theories/ZArith/zbinary.cmo: theories/ZArith/zeven.cmi \ + theories/Init/datatypes.cmi theories/Bool/bvector.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \ theories/ZArith/zbinary.cmi -theories/ZArith/zbinary.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Bool/bvector.cmx \ - theories/Init/datatypes.cmx theories/ZArith/zeven.cmx \ +theories/ZArith/zbinary.cmx: theories/ZArith/zeven.cmx \ + theories/Init/datatypes.cmx theories/Bool/bvector.cmx \ + theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \ theories/ZArith/zbinary.cmi -theories/ZArith/zbool.cmo: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ - theories/ZArith/zeven.cmi theories/ZArith/zbool.cmi -theories/ZArith/zbool.cmx: theories/ZArith/binInt.cmx \ - theories/Init/datatypes.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmx \ - theories/ZArith/zeven.cmx theories/ZArith/zbool.cmi +theories/ZArith/zbool.cmo: theories/ZArith/zeven.cmi \ + theories/ZArith/zArith_dec.cmi theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zbool.cmi +theories/ZArith/zbool.cmx: theories/ZArith/zeven.cmx \ + theories/ZArith/zArith_dec.cmx theories/Bool/sumbool.cmx \ + theories/Init/specif.cmx theories/Init/datatypes.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zbool.cmi theories/ZArith/zcompare.cmo: theories/ZArith/zcompare.cmi theories/ZArith/zcompare.cmx: theories/ZArith/zcompare.cmi -theories/ZArith/zcomplements.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ - theories/ZArith/zabs.cmi theories/ZArith/zcomplements.cmi -theories/ZArith/zcomplements.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Lists/list.cmx theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \ - theories/ZArith/zabs.cmx theories/ZArith/zcomplements.cmi -theories/ZArith/zdiv.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ - theories/ZArith/zbool.cmi theories/ZArith/zdiv.cmi -theories/ZArith/zdiv.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/ZArith/zArith_dec.cmx \ - theories/ZArith/zbool.cmx theories/ZArith/zdiv.cmi -theories/ZArith/zeven.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/ZArith/zeven.cmi -theories/ZArith/zeven.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/ZArith/zeven.cmi +theories/ZArith/zcomplements.cmo: theories/ZArith/zabs.cmi \ + theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zcomplements.cmi +theories/ZArith/zcomplements.cmx: theories/ZArith/zabs.cmx \ + theories/ZArith/wf_Z.cmx theories/Init/specif.cmx theories/Lists/list.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zcomplements.cmi +theories/ZArith/zdiv.cmo: theories/ZArith/zbool.cmi \ + theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zdiv.cmi +theories/ZArith/zdiv.cmx: theories/ZArith/zbool.cmx \ + theories/ZArith/zArith_dec.cmx theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zdiv.cmi +theories/ZArith/zeven.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zeven.cmi +theories/ZArith/zeven.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zeven.cmi theories/ZArith/zhints.cmo: theories/ZArith/zhints.cmi theories/ZArith/zhints.cmx: theories/ZArith/zhints.cmi -theories/ZArith/zlogarithm.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/ZArith/zlogarithm.cmi -theories/ZArith/zlogarithm.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/ZArith/zlogarithm.cmi -theories/ZArith/zmin.cmo: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/ZArith/zmin.cmi -theories/ZArith/zmin.cmx: theories/ZArith/binInt.cmx \ - theories/Init/datatypes.cmx theories/ZArith/zmin.cmi -theories/ZArith/zmisc.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ +theories/ZArith/zlogarithm.cmo: theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zlogarithm.cmi +theories/ZArith/zlogarithm.cmx: theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zlogarithm.cmi +theories/ZArith/zmax.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zmax.cmi +theories/ZArith/zmax.cmx: theories/Init/datatypes.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zmax.cmi +theories/ZArith/zminmax.cmo: theories/ZArith/zminmax.cmi +theories/ZArith/zminmax.cmx: theories/ZArith/zminmax.cmi +theories/ZArith/zmin.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/ZArith/binInt.cmi \ + theories/ZArith/zmin.cmi +theories/ZArith/zmin.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/ZArith/binInt.cmx \ + theories/ZArith/zmin.cmi +theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi \ theories/ZArith/zmisc.cmi -theories/ZArith/zmisc.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ +theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \ + theories/NArith/binPos.cmx theories/ZArith/binInt.cmx \ theories/ZArith/zmisc.cmi theories/ZArith/znat.cmo: theories/ZArith/znat.cmi theories/ZArith/znat.cmx: theories/ZArith/znat.cmi -theories/ZArith/znumtheory.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ - theories/ZArith/zArith_dec.cmi theories/ZArith/zdiv.cmi \ - theories/ZArith/zorder.cmi theories/ZArith/znumtheory.cmi -theories/ZArith/znumtheory.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \ - theories/ZArith/zArith_dec.cmx theories/ZArith/zdiv.cmx \ - theories/ZArith/zorder.cmx theories/ZArith/znumtheory.cmi -theories/ZArith/zorder.cmo: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ +theories/ZArith/znumtheory.cmo: theories/ZArith/zorder.cmi \ + theories/ZArith/zdiv.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/znumtheory.cmi +theories/ZArith/znumtheory.cmx: theories/ZArith/zorder.cmx \ + theories/ZArith/zdiv.cmx theories/ZArith/zArith_dec.cmx \ + theories/ZArith/wf_Z.cmx theories/Init/specif.cmx theories/Init/peano.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/znumtheory.cmi +theories/ZArith/zorder.cmo: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/ZArith/binInt.cmi \ theories/ZArith/zorder.cmi -theories/ZArith/zorder.cmx: theories/ZArith/binInt.cmx \ - theories/Init/datatypes.cmx theories/Init/specif.cmx \ +theories/ZArith/zorder.cmx: theories/Init/specif.cmx \ + theories/Init/datatypes.cmx theories/ZArith/binInt.cmx \ theories/ZArith/zorder.cmi -theories/ZArith/zpower.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi -theories/ZArith/zpower.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/datatypes.cmx \ - theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi -theories/ZArith/zsqrt.cmo: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/specif.cmi \ - theories/ZArith/zArith_dec.cmi theories/ZArith/zsqrt.cmi -theories/ZArith/zsqrt.cmx: theories/ZArith/binInt.cmx \ - theories/NArith/binPos.cmx theories/Init/specif.cmx \ - theories/ZArith/zArith_dec.cmx theories/ZArith/zsqrt.cmi +theories/ZArith/zpower.cmo: theories/ZArith/zmisc.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zpower.cmi +theories/ZArith/zpower.cmx: theories/ZArith/zmisc.cmx \ + theories/Init/datatypes.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zpower.cmi +theories/ZArith/zsqrt.cmo: theories/ZArith/zArith_dec.cmi \ + theories/Init/specif.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi theories/ZArith/zsqrt.cmi +theories/ZArith/zsqrt.cmx: theories/ZArith/zArith_dec.cmx \ + theories/Init/specif.cmx theories/NArith/binPos.cmx \ + theories/ZArith/binInt.cmx theories/ZArith/zsqrt.cmi theories/ZArith/zwf.cmo: theories/ZArith/zwf.cmi theories/ZArith/zwf.cmx: theories/ZArith/zwf.cmi -theories/Arith/bool_nat.cmi: theories/Arith/compare_dec.cmi \ - theories/Init/datatypes.cmi theories/Arith/peano_dec.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi -theories/Arith/compare_dec.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/Arith/compare.cmi: theories/Arith/compare_dec.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Arith/div2.cmi: theories/Init/datatypes.cmi theories/Init/peano.cmi \ - theories/Init/specif.cmi -theories/Arith/eqNat.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/Arith/euclid.cmi: theories/Arith/compare_dec.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Arith/even.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Arith/factorial.cmi: theories/Init/datatypes.cmi \ - theories/Init/peano.cmi -theories/Arith/max.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Arith/min.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Arith/mult.cmi: theories/Init/datatypes.cmi theories/Arith/plus.cmi -theories/Arith/peano_dec.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/Arith/plus.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/bool_nat.cmi: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Arith/peano_dec.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi +theories/Arith/compare_dec.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi +theories/Arith/compare.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi +theories/Arith/div2.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi +theories/Arith/eqNat.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi +theories/Arith/euclid.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi +theories/Arith/even.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi +theories/Arith/factorial.cmi: theories/Init/peano.cmi \ + theories/Init/datatypes.cmi +theories/Arith/max.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi +theories/Arith/min.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi +theories/Arith/mult.cmi: theories/Arith/plus.cmi theories/Init/datatypes.cmi +theories/Arith/peano_dec.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi +theories/Arith/plus.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi -theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Bool/bvector.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/Init/peano.cmi +theories/Bool/boolEq.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi +theories/Bool/bool.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi +theories/Bool/bvector.cmi: theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Bool/bool.cmi theories/Bool/decBool.cmi: theories/Init/specif.cmi -theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/Bool/sumbool.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi +theories/Bool/ifProp.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi +theories/Bool/sumbool.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Bool/zerob.cmi: theories/Init/datatypes.cmi -theories/Init/logic_Type.cmi: theories/Init/datatypes.cmi +theories/FSets/decidableTypeEx.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedTypeEx.cmi theories/FSets/orderedType.cmi \ + theories/Init/datatypes.cmi +theories/FSets/decidableType.cmi: theories/Init/specif.cmi +theories/FSets/fMapAVL.cmi: theories/Init/wf.cmi theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/FSets/int.cmi theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi +theories/FSets/fMapFacts.cmi: theories/Init/specif.cmi \ + theories/FSets/fMapInterface.cmi theories/Init/datatypes.cmi +theories/FSets/fMapInterface.cmi: theories/FSets/orderedType.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi +theories/FSets/fMapIntMap.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/NArith/ndigits.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/mapcanon.cmi \ + theories/IntMap/map.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binNat.cmi +theories/FSets/fMapList.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fMapPositive.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi +theories/FSets/fMapWeakFacts.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/FSets/fMapWeakInterface.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fMapWeakInterface.cmi: theories/Lists/list.cmi \ + theories/FSets/decidableType.cmi theories/Init/datatypes.cmi +theories/FSets/fMapWeakList.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/FSets/decidableType.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetAVL.cmi: theories/Init/wf.cmi theories/Init/specif.cmi \ + theories/Init/peano.cmi theories/FSets/orderedType.cmi \ + theories/Lists/list.cmi theories/FSets/int.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/FSets/fSetBridge.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi +theories/FSets/fSetEqProperties.cmi: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/Init/peano.cmi \ + theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi \ + theories/Bool/bool.cmi +theories/FSets/fSetFacts.cmi: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/fSetInterface.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetInterface.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetList.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetProperties.cmi: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/Lists/list.cmi \ + theories/FSets/fSetInterface.cmi theories/Init/datatypes.cmi +theories/FSets/fSetToFiniteSet.cmi: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/orderedTypeEx.cmi \ + theories/FSets/orderedType.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetWeakFacts.cmi: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/FSets/fSetWeakInterface.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetWeakInterface.cmi: theories/Lists/list.cmi \ + theories/FSets/decidableType.cmi theories/Init/datatypes.cmi +theories/FSets/fSetWeakList.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/FSets/decidableType.cmi \ + theories/Init/datatypes.cmi +theories/FSets/fSetWeakProperties.cmi: theories/Init/specif.cmi \ + theories/Setoids/setoid.cmi theories/Lists/list.cmi \ + theories/FSets/fSetWeakInterface.cmi theories/Init/datatypes.cmi +theories/FSets/int.cmi: theories/ZArith/zmax.cmi \ + theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi +theories/FSets/orderedTypeAlt.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Init/datatypes.cmi +theories/FSets/orderedTypeEx.cmi: theories/Init/specif.cmi \ + theories/FSets/orderedType.cmi theories/Init/datatypes.cmi \ + theories/Arith/compare_dec.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi theories/ZArith/binInt.cmi +theories/FSets/orderedType.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Init/peano.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi: theories/Init/datatypes.cmi -theories/IntMap/adalloc.cmi: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/NArith/binPos.cmi \ - theories/Init/datatypes.cmi theories/IntMap/map.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi -theories/IntMap/addec.cmi: theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi -theories/IntMap/addr.cmi: theories/NArith/binPos.cmi theories/Bool/bool.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/IntMap/adist.cmi: theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi -theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ - theories/Init/datatypes.cmi theories/IntMap/map.cmi \ - theories/Init/specif.cmi -theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Bool/bool.cmi \ - theories/Init/datatypes.cmi theories/Lists/list.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi -theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi \ - theories/Init/specif.cmi -theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/IntMap/map.cmi theories/Init/peano.cmi \ - theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi -theories/IntMap/mapfold.cmi: theories/IntMap/addr.cmi \ - theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ - theories/Init/specif.cmi -theories/IntMap/mapiter.cmi: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/IntMap/map.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi -theories/IntMap/maplists.cmi: theories/IntMap/addec.cmi \ - theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/IntMap/fset.cmi theories/Lists/list.cmi theories/IntMap/map.cmi \ - theories/IntMap/mapiter.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi -theories/IntMap/map.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi -theories/IntMap/mapsubset.cmi: theories/Bool/bool.cmi \ - theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi -theories/Lists/list.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/Lists/listSet.cmi: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Init/specif.cmi +theories/IntMap/adalloc.cmi: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/NArith/ndec.cmi theories/IntMap/map.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi +theories/IntMap/fset.cmi: theories/Init/specif.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/IntMap/map.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi +theories/IntMap/lsort.cmi: theories/Bool/sumbool.cmi theories/Init/specif.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi +theories/IntMap/mapcanon.cmi: theories/Init/specif.cmi \ + theories/IntMap/map.cmi +theories/IntMap/mapcard.cmi: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Arith/plus.cmi \ + theories/Arith/peano_dec.cmi theories/Init/peano.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/IntMap/map.cmi theories/Init/datatypes.cmi \ + theories/NArith/binNat.cmi +theories/IntMap/mapfold.cmi: theories/Init/specif.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \ + theories/IntMap/fset.cmi theories/Init/datatypes.cmi +theories/IntMap/mapiter.cmi: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/NArith/ndigits.cmi \ + theories/NArith/ndec.cmi theories/IntMap/map.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binNat.cmi +theories/IntMap/maplists.cmi: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/NArith/ndec.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/map.cmi \ + theories/Lists/list.cmi theories/IntMap/fset.cmi \ + theories/Init/datatypes.cmi +theories/IntMap/map.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/NArith/ndigits.cmi theories/NArith/ndec.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi +theories/IntMap/mapsubset.cmi: theories/IntMap/mapiter.cmi \ + theories/IntMap/map.cmi theories/IntMap/fset.cmi \ + theories/Init/datatypes.cmi theories/Bool/bool.cmi +theories/Lists/list.cmi: theories/Init/specif.cmi theories/Init/datatypes.cmi +theories/Lists/listSet.cmi: theories/Init/specif.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/Lists/monoList.cmi: theories/Init/datatypes.cmi +theories/Lists/setoidList.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi theories/Lists/streams.cmi: theories/Init/datatypes.cmi -theories/Lists/theoryList.cmi: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Init/specif.cmi -theories/NArith/binNat.cmi: theories/NArith/binPos.cmi \ +theories/Lists/theoryList.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi +theories/Logic/choiceFacts.cmi: theories/Init/specif.cmi \ theories/Init/datatypes.cmi -theories/NArith/binPos.cmi: theories/Init/datatypes.cmi \ - theories/Init/peano.cmi -theories/Relations/relation_Operators.cmi: theories/Lists/list.cmi \ - theories/Init/specif.cmi +theories/Logic/classicalDescription.cmi: theories/Init/specif.cmi \ + theories/Logic/choiceFacts.cmi +theories/Logic/classicalEpsilon.cmi: theories/Init/specif.cmi \ + theories/Logic/choiceFacts.cmi +theories/Logic/diaconescu.cmi: theories/Init/specif.cmi +theories/Logic/eqdep_dec.cmi: theories/Init/specif.cmi +theories/NArith/binNat.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi +theories/NArith/binPos.cmi: theories/Init/peano.cmi \ + theories/Init/datatypes.cmi +theories/NArith/ndec.cmi: theories/Bool/sumbool.cmi theories/Init/specif.cmi \ + theories/NArith/nnat.cmi theories/NArith/ndigits.cmi \ + theories/Init/datatypes.cmi theories/Arith/compare_dec.cmi \ + theories/NArith/binPos.cmi theories/NArith/binNat.cmi +theories/NArith/ndigits.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Bool/bvector.cmi \ + theories/Bool/bool.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi +theories/NArith/ndist.cmi: theories/NArith/ndigits.cmi theories/Arith/min.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/NArith/binNat.cmi +theories/NArith/nnat.cmi: theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/NArith/binNat.cmi +theories/QArith/qArith_base.cmi: theories/ZArith/zArith_dec.cmi \ + theories/Init/specif.cmi theories/Setoids/setoid.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/QArith/qreals.cmi: theories/QArith/qArith_base.cmi \ + theories/ZArith/binInt.cmi +theories/QArith/qreduction.cmi: theories/ZArith/znumtheory.cmi \ + theories/Setoids/setoid.cmi theories/QArith/qArith_base.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/QArith/qring.cmi: theories/Init/specif.cmi \ + theories/QArith/qArith_base.cmi theories/Init/datatypes.cmi +theories/Relations/relation_Operators.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi +theories/Setoids/setoid.cmi: theories/Init/datatypes.cmi theories/Sets/cpo.cmi: theories/Sets/partial_Order.cmi -theories/Sets/integers.cmi: theories/Init/datatypes.cmi \ - theories/Sets/partial_Order.cmi -theories/Sets/multiset.cmi: theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi -theories/Sets/partial_Order.cmi: theories/Sets/ensembles.cmi \ - theories/Sets/relations_1.cmi -theories/Sets/powerset.cmi: theories/Sets/ensembles.cmi \ - theories/Sets/partial_Order.cmi -theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Sets/multiset.cmi \ - theories/Init/peano.cmi theories/Sorting/sorting.cmi \ - theories/Init/specif.cmi -theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Sets/multiset.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi -theories/Sorting/sorting.cmi: theories/Lists/list.cmi \ - theories/Init/specif.cmi -theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi -theories/ZArith/binInt.cmi: theories/NArith/binNat.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi -theories/ZArith/wf_Z.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/peano.cmi theories/Init/specif.cmi -theories/ZArith/zabs.cmi: theories/ZArith/binInt.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi -theories/ZArith/zArith_dec.cmi: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi -theories/ZArith/zbinary.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Bool/bvector.cmi \ - theories/Init/datatypes.cmi theories/ZArith/zeven.cmi -theories/ZArith/zbool.cmi: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ - theories/ZArith/zeven.cmi -theories/ZArith/zcomplements.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Lists/list.cmi theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ - theories/ZArith/zabs.cmi -theories/ZArith/zdiv.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ - theories/ZArith/zbool.cmi -theories/ZArith/zeven.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi -theories/ZArith/zlogarithm.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi -theories/ZArith/zmin.cmi: theories/ZArith/binInt.cmi \ +theories/Sets/integers.cmi: theories/Sets/partial_Order.cmi \ theories/Init/datatypes.cmi -theories/ZArith/zmisc.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi -theories/ZArith/znumtheory.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ - theories/ZArith/zArith_dec.cmi theories/ZArith/zdiv.cmi \ - theories/ZArith/zorder.cmi -theories/ZArith/zorder.cmi: theories/ZArith/binInt.cmi \ - theories/Init/datatypes.cmi theories/Init/specif.cmi -theories/ZArith/zpower.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/datatypes.cmi \ - theories/ZArith/zmisc.cmi -theories/ZArith/zsqrt.cmi: theories/ZArith/binInt.cmi \ - theories/NArith/binPos.cmi theories/Init/specif.cmi \ - theories/ZArith/zArith_dec.cmi +theories/Sets/multiset.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi +theories/Sets/partial_Order.cmi: theories/Sets/relations_1.cmi \ + theories/Sets/ensembles.cmi +theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi \ + theories/Sets/ensembles.cmi +theories/Sets/uniset.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi +theories/Sorting/heap.cmi: theories/Init/specif.cmi \ + theories/Sorting/sorting.cmi theories/Init/peano.cmi \ + theories/Sets/multiset.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi +theories/Sorting/permutation.cmi: theories/Init/specif.cmi \ + theories/Init/peano.cmi theories/Sets/multiset.cmi \ + theories/Lists/list.cmi theories/Init/datatypes.cmi +theories/Sorting/sorting.cmi: theories/Init/specif.cmi \ + theories/Lists/list.cmi +theories/Strings/ascii.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/Bool/bool.cmi \ + theories/NArith/binPos.cmi +theories/Strings/string.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/Strings/ascii.cmi +theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi +theories/ZArith/binInt.cmi: theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/NArith/binNat.cmi +theories/ZArith/wf_Z.cmi: theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zabs.cmi: theories/Init/specif.cmi theories/ZArith/binInt.cmi +theories/ZArith/zArith_dec.cmi: theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zbinary.cmi: theories/ZArith/zeven.cmi \ + theories/Init/datatypes.cmi theories/Bool/bvector.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi +theories/ZArith/zbool.cmi: theories/ZArith/zeven.cmi \ + theories/ZArith/zArith_dec.cmi theories/Bool/sumbool.cmi \ + theories/Init/specif.cmi theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zcomplements.cmi: theories/ZArith/zabs.cmi \ + theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Lists/list.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zdiv.cmi: theories/ZArith/zbool.cmi \ + theories/ZArith/zArith_dec.cmi theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zeven.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zlogarithm.cmi: theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zmax.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zmin.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/ZArith/binInt.cmi +theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \ + theories/NArith/binPos.cmi theories/ZArith/binInt.cmi +theories/ZArith/znumtheory.cmi: theories/ZArith/zorder.cmi \ + theories/ZArith/zdiv.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/wf_Z.cmi theories/Init/specif.cmi theories/Init/peano.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zorder.cmi: theories/Init/specif.cmi \ + theories/Init/datatypes.cmi theories/ZArith/binInt.cmi +theories/ZArith/zpower.cmi: theories/ZArith/zmisc.cmi \ + theories/Init/datatypes.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi +theories/ZArith/zsqrt.cmi: theories/ZArith/zArith_dec.cmi \ + theories/Init/specif.cmi theories/NArith/binPos.cmi \ + theories/ZArith/binInt.cmi diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index c9bb5623..65a54090 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -10,7 +10,7 @@ AXIOMSVO:= \ theories/Reals/% \ theories/Num/% -DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS)) +DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -path \*.svn\*)) INCL:= $(patsubst %,-I %,$(DIRS)) @@ -34,7 +34,7 @@ all: v2ml ml $(MLI) $(CMO) ml: $(ML) -depend: $(ML) +depend: #$(ML) rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend tree: diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc index 0fb556aa..e7204838 100644 --- a/contrib/extraction/test/custom/Adalloc +++ b/contrib/extraction/test/custom/Adalloc @@ -1,2 +1,2 @@ -Require Import Addr. -Extraction NoInline ad_double ad_double_plus_un. +Require Import BinNat. +Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort index 6a185683..22ab18e3 100644 --- a/contrib/extraction/test/custom/Lsort +++ b/contrib/extraction/test/custom/Lsort @@ -1,2 +1,2 @@ -Require Import Addr. -Extraction NoInline ad_double ad_double_plus_un. +Require Import BinNat. +Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map index 3e464e39..f024dbd7 100644 --- a/contrib/extraction/test/custom/Map +++ b/contrib/extraction/test/custom/Map @@ -1,3 +1,3 @@ -Require Import Addr. -Extraction NoInline ad_double ad_double_plus_un. +Require Import BinNat. +Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard index ca555aa3..5932cf7b 100644 --- a/contrib/extraction/test/custom/Mapcard +++ b/contrib/extraction/test/custom/Mapcard @@ -1,4 +1,4 @@ Require Import Plus. Extraction NoInline plus_is_one. -Require Import Addr. -Extraction NoInline ad_double ad_double_plus_un. +Require Import BinNat. +Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter index 6a185683..22ab18e3 100644 --- a/contrib/extraction/test/custom/Mapiter +++ b/contrib/extraction/test/custom/Mapiter @@ -1,2 +1,2 @@ -Require Import Addr. -Extraction NoInline ad_double ad_double_plus_un. +Require Import BinNat. +Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v deleted file mode 100644 index 0745f62d..00000000 --- a/contrib/extraction/test_extraction.v +++ /dev/null @@ -1,552 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -Require Import Arith. -Require Import List. - -(*** STANDARD EXAMPLES *) - -(** Functions. *) - -Definition idnat (x:nat) := x. -Extraction idnat. -(* let idnat x = x *) - -Definition id (X:Type) (x:X) := x. -Extraction id. (* let id x = x *) -Definition id' := id Set nat. -Extraction id'. (* type id' = nat *) - -Definition test2 (f:nat -> nat) (x:nat) := f x. -Extraction test2. -(* let test2 f x = f x *) - -Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat. -Extraction test3. -(* let test3 f x = f x __ *) - -Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g. -Extraction test4. -(* let test4 f x g = f g *) - -Definition test5 := (1, 0). -Extraction test5. -(* let test5 = Pair ((S O), O) *) - -Definition cf (x:nat) (_:x <= 0) := S x. -Extraction NoInline cf. -Definition test6 := cf 0 (le_n 0). -Extraction test6. -(* let test6 = cf O *) - -Definition test7 := (fun (X:Set) (x:X) => x) nat. -Extraction test7. -(* let test7 x = x *) - -Definition d (X:Type) := X. -Extraction d. (* type 'x d = 'x *) -Definition d2 := d Set. -Extraction d2. (* type d2 = __ d *) -Definition d3 (x:d Set) := 0. -Extraction d3. (* let d3 _ = O *) -Definition d4 := d nat. -Extraction d4. (* type d4 = nat d *) -Definition d5 := (fun x:d Type => 0) Type. -Extraction d5. (* let d5 = O *) -Definition d6 (x:d Type) := x. -Extraction d6. (* type 'x d6 = 'x *) - -Definition test8 := (fun (X:Type) (x:X) => x) Set nat. -Extraction test8. (* type test8 = nat *) - -Definition test9 := let t := nat in id Set t. -Extraction test9. (* type test9 = nat *) - -Definition test10 := (fun (X:Type) (x:X) => 0) Type Type. -Extraction test10. (* let test10 = O *) - -Definition test11 := let n := 0 in let p := S n in S p. -Extraction test11. (* let test11 = S (S O) *) - -Definition test12 := forall x:forall X:Type, X -> X, x Type Type. -Extraction test12. -(* type test12 = (__ -> __ -> __) -> __ *) - - -Definition test13 := match left True I with - | left x => 1 - | right x => 0 - end. -Extraction test13. (* let test13 = S O *) - - -(** example with more arguments that given by the type *) - -Definition test19 := - nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0) - (fun (n:nat) (f:nat -> nat) => f) 0 0. -Extraction test19. -(* let test19 = - let rec f = function - | O -> (fun n0 -> O) - | S n0 -> f n0 - in f O O -*) - - -(** casts *) - -Definition test20 := True:Type. -Extraction test20. -(* type test20 = __ *) - - -(** Simple inductive type and recursor. *) - -Extraction nat. -(* -type nat = - | O - | S of nat -*) - -Extraction sumbool_rect. -(* -let sumbool_rect f f0 = function - | Left -> f __ - | Right -> f0 __ -*) - -(** Less simple inductive type. *) - -Inductive c (x:nat) : nat -> Set := - | refl : c x x - | trans : forall y z:nat, c x y -> y <= z -> c x z. -Extraction c. -(* -type c = - | Refl - | Trans of nat * nat * c -*) - -Definition Ensemble (U:Type) := U -> Prop. -Definition Empty_set (U:Type) (x:U) := False. -Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y. - -Inductive Finite (U:Type) : Ensemble U -> Set := - | Empty_is_finite : Finite U (Empty_set U) - | Union_is_finite : - forall A:Ensemble U, - Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x). -Extraction Finite. -(* -type 'u finite = - | Empty_is_finite - | Union_is_finite of 'u finite * 'u -*) - - -(** Mutual Inductive *) - -Inductive tree : Set := - Node : nat -> forest -> tree -with forest : Set := - | Leaf : nat -> forest - | Cons : tree -> forest -> forest. - -Extraction tree. -(* -type tree = - | Node of nat * forest -and forest = - | Leaf of nat - | Cons of tree * forest -*) - -Fixpoint tree_size (t:tree) : nat := - match t with - | Node a f => S (forest_size f) - end - - with forest_size (f:forest) : nat := - match f with - | Leaf b => 1 - | Cons t f' => tree_size t + forest_size f' - end. - -Extraction tree_size. -(* -let rec tree_size = function - | Node (a, f) -> S (forest_size f) -and forest_size = function - | Leaf b -> S O - | Cons (t, f') -> plus (tree_size t) (forest_size f') -*) - - -(** Eta-expansions of inductive constructor *) - -Inductive titi : Set := - tata : nat -> nat -> nat -> nat -> titi. -Definition test14 := tata 0. -Extraction test14. -(* let test14 x x0 x1 = Tata (O, x, x0, x1) *) -Definition test15 := tata 0 1. -Extraction test15. -(* let test15 x x0 = Tata (O, (S O), x, x0) *) - -Inductive eta : Set := - eta_c : nat -> Prop -> nat -> Prop -> eta. -Extraction eta_c. -(* -type eta = - | Eta_c of nat * nat -*) -Definition test16 := eta_c 0. -Extraction test16. -(* let test16 x = Eta_c (O, x) *) -Definition test17 := eta_c 0 True. -Extraction test17. -(* let test17 x = Eta_c (O, x) *) -Definition test18 := eta_c 0 True 0. -Extraction test18. -(* let test18 _ = Eta_c (O, O) *) - - -(** Example of singleton inductive type *) - -Inductive bidon (A:Prop) (B:Type) : Set := - tb : forall (x:A) (y:B), bidon A B. -Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) - (x:A) (y:B) := f x y. -Extraction bidon. -(* type 'b bidon = 'b *) -Extraction tb. -(* tb : singleton inductive constructor *) -Extraction fbidon. -(* let fbidon f x y = - f x y -*) - -Definition fbidon2 := fbidon True nat (tb True nat). -Extraction fbidon2. (* let fbidon2 y = y *) -Extraction NoInline fbidon. -Extraction fbidon2. -(* let fbidon2 y = fbidon (fun _ x -> x) __ y *) - -(* NB: first argument of fbidon2 has type [True], so it disappears. *) - -(** mutual inductive on many sorts *) - -Inductive test_0 : Prop := - ctest0 : test_0 -with test_1 : Set := - ctest1 : test_0 -> test_1. -Extraction test_0. -(* test0 : logical inductive *) -Extraction test_1. -(* -type test1 = - | Ctest1 -*) - -(** logical singleton *) - -Extraction eq. -(* eq : logical inductive *) -Extraction eq_rect. -(* let eq_rect x f y = - f -*) - -(** No more propagation of type parameters. Obj.t instead. *) - -Inductive tp1 : Set := - T : forall (C:Set) (c:C), tp2 -> tp1 -with tp2 : Set := - T' : tp1 -> tp2. -Extraction tp1. -(* -type tp1 = - | T of __ * tp2 -and tp2 = - | T' of tp1 -*) - -Inductive tp1bis : Set := - Tbis : tp2bis -> tp1bis -with tp2bis : Set := - T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis. -Extraction tp1bis. -(* -type tp1bis = - | Tbis of tp2bis -and tp2bis = - | T'bis of __ * tp1bis -*) - - -(** Strange inductive type. *) - -Inductive Truc : Set -> Set := - | chose : forall A:Set, Truc A - | machin : forall A:Set, A -> Truc bool -> Truc A. -Extraction Truc. -(* -type 'x truc = - | Chose - | Machin of 'x * bool truc -*) - - -(** Dependant type over Type *) - -Definition test24 := sigT (fun a:Set => option a). -Extraction test24. -(* type test24 = (__, __ option) sigT *) - - -(** Coq term non strongly-normalizable after extraction *) - -Require Import Gt. -Definition loop (Ax:Acc gt 0) := - (fix F (a:nat) (b:Acc gt a) {struct b} : nat := - F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax. -Extraction loop. -(* let loop _ = - let rec f a = - f (S a) - in f O -*) - -(*** EXAMPLES NEEDING OBJ.MAGIC *) - -(** False conversion of type: *) - -Lemma oups : forall H:nat = list nat, nat -> nat. -intros. -generalize H0; intros. -rewrite H in H1. -case H1. -exact H0. -intros. -exact n. -Qed. -Extraction oups. -(* -let oups h0 = - match Obj.magic h0 with - | Nil -> h0 - | Cons0 (n, l) -> n -*) - - -(** hybrids *) - -Definition horibilis (b:bool) := - if b as b return (if b then Type else nat) then Set else 0. -Extraction horibilis. -(* -let horibilis = function - | True -> Obj.magic __ - | False -> Obj.magic O -*) - -Definition PropSet (b:bool) := if b then Prop else Set. -Extraction PropSet. (* type propSet = __ *) - -Definition natbool (b:bool) := if b then nat else bool. -Extraction natbool. (* type natbool = __ *) - -Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true. -Extraction zerotrue. -(* -let zerotrue = function - | True -> Obj.magic O - | False -> Obj.magic True -*) - -Definition natProp (b:bool) := if b return Type then nat else Prop. - -Definition natTrue (b:bool) := if b return Type then nat else True. - -Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True. -Extraction zeroTrue. -(* -let zeroTrue = function - | True -> Obj.magic O - | False -> Obj.magic __ -*) - -Definition natTrue2 (b:bool) := if b return Type then nat else True. - -Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I. -Extraction zeroprop. -(* -let zeroprop = function - | True -> Obj.magic O - | False -> Obj.magic __ -*) - -(** polymorphic f applied several times *) - -Definition test21 := (id nat 0, id bool true). -Extraction test21. -(* let test21 = Pair ((id O), (id True)) *) - -(** ok *) - -Definition test22 := - (fun f:forall X:Type, X -> X => (f nat 0, f bool true)) - (fun (X:Type) (x:X) => x). -Extraction test22. -(* let test22 = - let f = fun x -> x in Pair ((f O), (f True)) *) - -(* still ok via optim beta -> let *) - -Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true). -Extraction test23. -(* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *) - -(* problem: fun f -> (f 0, f true) not legal in ocaml *) -(* solution: magic ... *) - - -(** Dummy constant __ can be applied.... *) - -Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0). -Extraction f. -(* let f x y = - y (x O) -*) - -Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true). -Extraction NoInline f. -Extraction f_prop. -(* let f_prop = - f (Obj.magic __) (fun _ -> True) -*) - -Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true). -Extraction f_arity. -(* let f_arity = - f (Obj.magic __) (fun _ -> True) -*) - -Definition f_normal := - f nat (fun x => x) (fun x => match x with - | O => true - | _ => false - end). -Extraction f_normal. -(* let f_normal = - f (fun x -> x) (fun x -> match x with - | O -> True - | S n -> False) -*) - - -(* inductive with magic needed *) - -Inductive Boite : Set := - boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. -Extraction Boite. -(* -type boite = - | Boite of bool * __ -*) - - -Definition boite1 := boite true 0. -Extraction boite1. -(* let boite1 = Boite (True, (Obj.magic O)) *) - -Definition boite2 := boite false (0, 0). -Extraction boite2. -(* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *) - -Definition test_boite (B:Boite) := - match B return nat with - | boite true n => n - | boite false n => fst n + snd n - end. -Extraction test_boite. -(* -let test_boite = function - | Boite (b0, n) -> - (match b0 with - | True -> Obj.magic n - | False -> plus (fst (Obj.magic n)) (snd (Obj.magic n))) -*) - -(* singleton inductive with magic needed *) - -Inductive Box : Set := - box : forall A:Set, A -> Box. -Extraction Box. -(* type box = __ *) - -Definition box1 := box nat 0. -Extraction box1. (* let box1 = Obj.magic O *) - -(* applied constant, magic needed *) - -Definition idzarb (b:bool) (x:if b then nat else bool) := x. -Definition zarb := idzarb true 0. -Extraction NoInline idzarb. -Extraction zarb. -(* let zarb = Obj.magic idzarb True (Obj.magic O) *) - -(** function of variable arity. *) -(** Fun n = nat -> nat -> ... -> nat *) - -Fixpoint Fun (n:nat) : Set := - match n with - | O => nat - | S n => nat -> Fun n - end. - -Fixpoint Const (k n:nat) {struct n} : Fun n := - match n as x return Fun x with - | O => k - | S n => fun p:nat => Const k n - end. - -Fixpoint proj (k n:nat) {struct n} : Fun n := - match n as x return Fun x with - | O => 0 (* ou assert false ....*) - | S n => - match k with - | O => fun x => Const x n - | S k => fun x => proj k n - end - end. - -Definition test_proj := proj 2 4 0 1 2 3. - -Eval compute in test_proj. - -Recursive Extraction test_proj. - - - -(*** TO SUM UP: ***) - - -Extraction - "test_extraction.ml" idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. - |