diff options
| -rw-r--r-- | contrib/extraction/common.ml | 213 | ||||
| -rw-r--r-- | contrib/extraction/miniml.mli | 3 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 16 | ||||
| -rw-r--r-- | contrib/extraction/modutil.mli | 6 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 16 | ||||
| -rw-r--r-- | contrib/extraction/test/.depend | 163 |
6 files changed, 218 insertions, 199 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index f7767f46d7..48e169f706 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -28,10 +28,17 @@ let keywords = ref Idset.empty let global_ids = ref Idset.empty let modular = ref false +(* For each [global_reference], this table will contain the different parts + of its renamings, in [string list] form. *) let renamings = Hashtbl.create 97 -let rename r s = Hashtbl.add renamings r s +let rename r l = Hashtbl.add renamings r l let get_renamings r = Hashtbl.find renamings r +(* Idem for [module_path]. *) +let mp_renamings = Hashtbl.create 97 +let mp_rename mp l = Hashtbl.add mp_renamings mp l +let mp_get_renamings mp = Hashtbl.find mp_renamings mp + let modvisited = ref MPset.empty let modcontents = ref Gset.empty let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents @@ -39,12 +46,19 @@ let module_contents mp s = Gset.mem (mp,s) !modcontents let to_qualify = ref Refset.empty +let mod_1st_level = ref Idmap.empty + (*s Uppercase/lowercase renamings. *) let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false +(* This function creates from [id] a correct uppercase/lowercase identifier. + This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes + with previous [Coq_id] variable, these prefixes are duplicated if already + existing. *) + let modular_rename up id = let s = string_of_id id in let prefix = if up then "Coq_" else "coq_" in @@ -57,28 +71,6 @@ let modular_rename up id = let rename_module = modular_rename true -let print_labels = List.map (fun l -> rename_module (id_of_label l)) - -let print_base_mp = function - | MPfile d -> String.capitalize (string_of_id (List.hd (repr_dirpath d))) - | MPself msid -> rename_module (id_of_msid msid) - | MPbound mbid -> rename_module (id_of_mbid mbid) - | _ -> assert false - -(*s From a [module_path] to a list of [identifier]. *) - -let mp2l mp = - let base_mp,l = labels_of_mp mp in - if !modular || not (at_toplevel base_mp) - then (print_base_mp base_mp) :: (print_labels l) - else print_labels l - -let string_of_modlist l = - List.fold_right (fun s s' -> if s' = "" then s else s ^ "." ^ s') l "" - -let string_of_ren l s = - if l = [] then s else (string_of_modlist l)^"."^s - (* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when [mpl] is the context of visible modules. More precisely, we check if there exists a mp1, module (sub-)path of an element of [mpl], such as @@ -132,6 +124,18 @@ let contents_first_level mp = (*s Initial renamings creation, for modular extraction. *) +let rec mp_create_modular_renamings mp = + try mp_get_renamings mp + with Not_found -> + let ren = match mp with + | MPdot (mp,l) -> + (rename_module (id_of_label l)) :: (mp_create_modular_renamings mp) + | MPself msid -> [rename_module (id_of_msid msid)] + | MPbound mbid -> [rename_module (id_of_mbid mbid)] + | MPfile f -> [String.capitalize (string_of_id (List.hd (repr_dirpath f)))] + in mp_rename mp ren; ren + + let create_modular_renamings struc = let current_module = fst (List.hd struc) in let modfiles = ref MPset.empty in @@ -140,14 +144,15 @@ let create_modular_renamings struc = (* 1) creates renamings of objects *) let add upper r = let mp = modpath (kn_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; + rename r (s::l); begin try let mp = modfile_of_mp mp in if mp <> current_module then modfiles := MPset.add mp !modfiles with Not_found -> () end; - let s = modular_rename upper (id_of_global r) in - global_ids := Idset.add (id_of_string s) !global_ids; - Hashtbl.add renamings r s in Refset.iter (add true) u; Refset.iter (add false) d; @@ -181,7 +186,7 @@ let create_modular_renamings struc = let needs_qualify r = let mp = modpath (kn_of_r r) in if (is_modfile mp) && mp <> current_module && - (clash mp [] (get_renamings r) used_modules') + (clash mp [] (List.hd (get_renamings r)) used_modules') then to_qualify := Refset.add r !to_qualify in Refset.iter needs_qualify u; @@ -190,29 +195,60 @@ let create_modular_renamings struc = (*s Initial renamings creation, for monolithic extraction. *) +let begins_with_CoqXX s = + (String.length s >= 4) && + (String.sub s 0 3 = "Coq") && + (try + for i = 4 to (String.index s '_')-1 do + match s.[i] with + | '0'..'9' -> () + | _ -> raise Not_found + done; + true + with Not_found -> false) + +let mod_1st_level_rename l = + let coqid = id_of_string "Coq" in + let id = id_of_label l in + try + let coqset = Idmap.find id !mod_1st_level in + let nextcoq = next_ident_away coqid coqset in + mod_1st_level := Idmap.add id (nextcoq::coqset) !mod_1st_level; + (string_of_id nextcoq)^"_"^(string_of_id id) + with Not_found -> + let s = string_of_id id in + if is_lower s || begins_with_CoqXX s then + (mod_1st_level := Idmap.add id [coqid] !mod_1st_level; "Coq_"^s) + else + (mod_1st_level := Idmap.add id [] !mod_1st_level; s) + +let rec mp_create_mono_renamings mp = + try mp_get_renamings mp + with Not_found -> + let ren = match mp with + | _ when (at_toplevel mp) -> [""] + | MPdot (mp,l) -> + let lmp = mp_create_mono_renamings mp in + if lmp = [""] then (mod_1st_level_rename l)::lmp + else (rename_module (id_of_label l))::lmp + | MPself msid -> [rename_module (id_of_msid msid)] + | MPbound mbid -> [rename_module (id_of_mbid mbid)] + | _ -> assert false + in mp_rename mp ren; ren + let create_mono_renamings struc = - let fst_level_modules = ref Idmap.empty in - let { up = u ; down = d } = struct_get_references_list struc - in - (* 1) create renamings of objects *) + let { up = u ; down = d } = struct_get_references_list struc in let add upper r = let mp = modpath (kn_of_r r) in - begin try - let mp,l = fst_level_module_of_mp mp in - let id = id_of_label l in - if Idmap.find id !fst_level_modules <> mp then - error_module_clash (string_of_id id) - else fst_level_modules := Idmap.add id mp !fst_level_modules - with Not_found -> () - end; - let my_id = if upper then uppercase_id else lowercase_id in + let l = mp_create_mono_renamings mp in + let mycase = if upper then uppercase_id else lowercase_id in let id = - if at_toplevel (modpath (kn_of_r r)) then - next_ident_away (my_id (id_of_global r)) (Idset.elements !global_ids) - else id_of_string (modular_rename upper (id_of_global r)) + if l = [""] then + next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids) + else id_of_string (modular_rename upper (id_of_global r)) in global_ids := Idset.add id !global_ids; - Hashtbl.add renamings r (string_of_id id) + rename r ((string_of_id id)::l) in List.iter (add true) (List.rev u); List.iter (add false) (List.rev d) @@ -222,8 +258,7 @@ let create_mono_renamings struc = module TopParams = struct let globals () = Idset.empty let pp_global _ r = pr_id (id_of_global r) - let pp_long_module _ mp = str (string_of_mp mp) - let pp_short_module id = pr_id id + let pp_module _ mp = str (string_of_mp mp) end (*s Renaming issues for a monolithic or modular extraction. *) @@ -234,62 +269,53 @@ module StdParams = struct (* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *) + let rec dottify = function + | [] -> assert false + | [s] -> s + | s::[""] -> s + | s::l -> (dottify l)^"."^s + let pp_global mpl r = - let s = get_renamings r in + let ls = get_renamings r in + let s = List.hd ls in let mp = modpath (kn_of_r r) in - let final = - if mp = List.hd mpl then s (* simpliest situation *) + 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 - let l = labels_after_prefix pref mp in -(*i TODO: traiter proprement. - if clash pref l s mpl - then error_unqualified_name (string_of_ren (print_labels l) s) - (string_of_modlist (mp2l (List.hd mpl))) - else i*) - string_of_ren (print_labels l) s + (*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, l = labels_of_mp mp in - let short = string_of_ren (print_labels l) s in - if !modular then - if (at_toplevel mp) && - not (Refset.mem r !to_qualify) && - not (clash base [] s mpl) - then short - else (print_base_mp base)^"."^short - else - if (at_toplevel base) - then short - else (print_base_mp base)^"."^short + 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 final - - let pp_long_module mpl mp = - try (* has [mp] something in common with one of those in [mpl] ? *) - let pref = common_prefix_from_list mp mpl in - let l = labels_after_prefix pref mp in -(*i TODO: comment adapter cela ?? - if clash pref l s mpl - then error_unqualified_name (string_of_ren (print_labels l) s) - (string_of_modlist (mp2l (List.hd mpl))) - else -i*) - str (string_of_modlist (print_labels l)) - with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base, l = labels_of_mp mp in - let short = string_of_modlist (print_labels l) in - if !modular then - if (at_toplevel mp) - then str short - else str ((print_base_mp base)^(if short = "" then "" else "."^short)) - else - if (at_toplevel base) - then str short - else str ((print_base_mp base)^(if short = "" then "" else "."^short)) + str (dottify ls) + + let pp_module mpl mp = + let ls = + if !modular + then mp_create_modular_renamings mp + else mp_create_mono_renamings mp + in + let ls = + try (* has [mp] something in common with one of those in [mpl] ? *) + let pref = common_prefix_from_list mp mpl in + (*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 + in str (dottify ls) - let pp_short_module id = str (rename_module id) end module ToplevelPp = Ocaml.Make(TopParams) @@ -346,6 +372,7 @@ let print_one_decl struc mp decl = let print_structure_to_file f prm struc = cons_cofix := Refset.empty; Hashtbl.clear renamings; + mod_1st_level := Idmap.empty; modcontents := Gset.empty; modvisited := MPset.empty; set_keywords (); diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 4a92f48337..1ed396c2d6 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -143,8 +143,7 @@ type ml_signature = (module_path * ml_module_sig) list module type Mlpp_param = sig val globals : unit -> Idset.t val pp_global : module_path list -> global_reference -> std_ppcmds - val pp_long_module : module_path list -> module_path -> std_ppcmds - val pp_short_module : identifier -> std_ppcmds + val pp_module : module_path list -> module_path -> std_ppcmds end module type Mlpp = sig diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 245318107d..0ab363bc68 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -84,6 +84,10 @@ let rec replicate_msid meb mtb = match meb,mtb with (*S More functions concerning [module_path]. *) +let rec mp_length = function + | MPdot (mp, _) -> 1 + (mp_length mp) + | _ -> 1 + let rec prefixes_mp mp = match mp with | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') | _ -> MPset.singleton mp @@ -106,11 +110,6 @@ let rec modfile_of_mp mp = match mp with | MPdot (mp,_) -> modfile_of_mp mp | _ -> raise Not_found -let rec fst_level_module_of_mp mp = match mp with - | MPdot (mp, l) when at_toplevel mp -> mp,l - | MPdot (mp, l) -> fst_level_module_of_mp mp - | _ -> raise Not_found - let rec parse_labels ll = function | MPdot (mp,l) -> parse_labels (l::ll) mp | mp -> mp,ll @@ -120,13 +119,6 @@ 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_after_prefix mp0 mp = - let n0 = List.length (snd (labels_of_mp mp0)) - and l = snd (labels_of_mp mp) - in - assert (n0 <= List.length l); - list_skipn n0 l - let rec add_labels_mp mp = function | [] -> mp | l :: ll -> add_labels_mp (MPdot (mp,l)) ll diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index 41a041d9a8..1e054f6d52 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -34,12 +34,10 @@ val replicate_msid : module_expr_body -> module_type_body -> module_type_body (*s More utilities concerning [module_path]. *) -val modfile_of_mp : module_path -> module_path -val fst_level_module_of_mp : module_path -> module_path * label +val mp_length : module_path -> int val prefixes_mp : module_path -> MPset.t +val modfile_of_mp : module_path -> module_path val common_prefix_from_list : module_path -> module_path list -> module_path -val labels_after_prefix : module_path -> module_path -> label list -val labels_of_mp : module_path -> module_path * label list val add_labels_mp : module_path -> label list -> module_path (*s Functions upon ML modules. *) diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 0f67cfde81..f6d8ab04bb 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -534,20 +534,20 @@ let rec pp_specif mpl = function | (l,Smodule mt) -> hov 1 (str "module " ++ - P.pp_short_module (id_of_label l) ++ + P.pp_module mpl (MPdot (List.hd mpl, l)) ++ str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt) | (l,Smodtype mt) -> hov 1 (str "module type " ++ - P.pp_short_module (id_of_label l) ++ + P.pp_module mpl (MPdot (List.hd mpl, l)) ++ str " = " ++ fnl () ++ pp_module_type mpl None mt) and pp_module_type mpl ol = function | MTident kn -> - let mp,_,l = repr_kn kn in P.pp_long_module mpl (MPdot (mp,l)) + let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l)) | MTfunsig (mbid, mt, mt') -> str "functor (" ++ - P.pp_short_module (id_of_mbid mbid) ++ + P.pp_module mpl (MPbound mbid) ++ str ":" ++ pp_module_type mpl None mt ++ str ") ->" ++ fnl () ++ @@ -569,7 +569,7 @@ let rec pp_structure_elem mpl = function | (_,SEdecl d) -> pp_decl mpl d | (l,SEmodule m) -> hov 1 - (str "module " ++ P.pp_short_module (id_of_label l) ++ + (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ (* if you want signatures everywhere: *) (*i str " :" ++ fnl () ++ i*) (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*) @@ -578,14 +578,14 @@ let rec pp_structure_elem mpl = function pp_module_expr mpl (Some l) m.ml_mod_expr) | (l,SEmodtype m) -> hov 1 - (str "module type " ++ P.pp_short_module (id_of_label l) ++ + (str "module type " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ str " = " ++ fnl () ++ pp_module_type mpl None m) and pp_module_expr mpl ol = function - | MEident mp' -> P.pp_long_module mpl mp' + | MEident mp' -> P.pp_module mpl mp' | MEfunctor (mbid, mt, me) -> str "functor (" ++ - P.pp_short_module (id_of_mbid mbid) ++ + P.pp_module mpl (MPbound mbid) ++ str ":" ++ pp_module_type mpl None mt ++ str ") ->" ++ fnl () ++ diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index f70e81319a..a355933e53 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -27,15 +27,19 @@ theories/Arith/eqNat.cmo: theories/Init/datatypes.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/Arith/minus.cmi \ - theories/Init/specif.cmi theories/Arith/euclid.cmi + theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/euclid.cmi theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \ - theories/Init/datatypes.cmx theories/Arith/minus.cmx \ - theories/Init/specif.cmx theories/Arith/euclid.cmi + theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/euclid.cmi theories/Arith/even.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ theories/Arith/even.cmi theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.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/gt.cmo: theories/Arith/gt.cmi theories/Arith/gt.cmx: theories/Arith/gt.cmi theories/Arith/le.cmo: theories/Arith/le.cmi @@ -50,10 +54,8 @@ theories/Arith/min.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ theories/Arith/min.cmi theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ theories/Arith/min.cmi -theories/Arith/minus.cmo: theories/Init/datatypes.cmi \ - theories/Arith/minus.cmi -theories/Arith/minus.cmx: theories/Init/datatypes.cmx \ - theories/Arith/minus.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.cmi theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx \ @@ -79,11 +81,9 @@ theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ theories/Bool/bool.cmi theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/Arith/minus.cmi theories/Init/peano.cmi \ - theories/Bool/bvector.cmi + theories/Init/peano.cmi theories/Bool/bvector.cmi theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \ - theories/Arith/minus.cmx theories/Init/peano.cmx \ - theories/Bool/bvector.cmi + theories/Init/peano.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 \ @@ -108,6 +108,8 @@ theories/Init/logic_Type.cmo: theories/Init/logic_Type.cmi theories/Init/logic_Type.cmx: theories/Init/logic_Type.cmi theories/Init/logic_TypeSyntax.cmo: theories/Init/logic_TypeSyntax.cmi theories/Init/logic_TypeSyntax.cmx: theories/Init/logic_TypeSyntax.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 theories/Init/peano.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmi theories/Init/peanoSyntax.cmo: theories/Init/peanoSyntax.cmi @@ -148,10 +150,10 @@ theories/IntMap/addr.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \ theories/IntMap/addr.cmi theories/IntMap/adist.cmo: theories/IntMap/addr.cmi \ theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ - theories/Arith/min.cmi theories/IntMap/adist.cmi + theories/IntMap/adist.cmi theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \ theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \ - theories/Arith/min.cmx theories/IntMap/adist.cmi + theories/IntMap/adist.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 \ @@ -162,16 +164,16 @@ theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ theories/Init/specif.cmx theories/IntMap/fset.cmi theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ theories/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ - theories/Lists/polyList.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi theories/IntMap/lsort.cmi + theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Lists/polyList.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/Bool/bool.cmx theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \ - theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ - theories/Lists/polyList.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx theories/IntMap/lsort.cmi + theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \ + theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \ + theories/Init/specif.cmx theories/Bool/sumbool.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 \ @@ -180,13 +182,13 @@ 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/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.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/Init/logic.cmx theories/IntMap/map.cmx theories/Init/peano.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 @@ -260,6 +262,8 @@ theories/Lists/theoryList.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/classicalFacts.cmo: theories/Logic/classicalFacts.cmi theories/Logic/classicalFacts.cmx: theories/Logic/classicalFacts.cmi theories/Logic/classical.cmo: theories/Logic/classical.cmi @@ -332,8 +336,10 @@ theories/Sets/multiset.cmo: theories/Init/datatypes.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/partial_Order.cmi -theories/Sets/partial_Order.cmx: theories/Sets/partial_Order.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/permut.cmo: theories/Sets/permut.cmi theories/Sets/permut.cmx: theories/Sets/permut.cmi theories/Sets/powerset_Classical_facts.cmo: \ @@ -342,10 +348,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/partial_Order.cmi \ - theories/Sets/powerset.cmi -theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx \ - theories/Sets/powerset.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/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 @@ -363,15 +369,13 @@ theories/Sets/uniset.cmo: theories/Init/datatypes.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/Init/logic.cmi theories/Sets/multiset.cmi \ - theories/Init/peano.cmi theories/Lists/polyList.cmi \ - theories/Sorting/sorting.cmi theories/Init/specif.cmi \ - theories/Sorting/heap.cmi + theories/Sets/multiset.cmi theories/Init/peano.cmi \ + theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \ + theories/Init/specif.cmi theories/Sorting/heap.cmi theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \ - theories/Init/logic.cmx theories/Sets/multiset.cmx \ - theories/Init/peano.cmx theories/Lists/polyList.cmx \ - theories/Sorting/sorting.cmx theories/Init/specif.cmx \ - theories/Sorting/heap.cmi + theories/Sets/multiset.cmx theories/Init/peano.cmx \ + theories/Lists/polyList.cmx theories/Sorting/sorting.cmx \ + theories/Init/specif.cmx theories/Sorting/heap.cmi theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \ theories/Sets/multiset.cmi theories/Init/peano.cmi \ theories/Lists/polyList.cmi theories/Init/specif.cmi \ @@ -380,12 +384,10 @@ theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \ theories/Sets/multiset.cmx theories/Init/peano.cmx \ theories/Lists/polyList.cmx theories/Init/specif.cmx \ theories/Sorting/permutation.cmi -theories/Sorting/sorting.cmo: theories/Init/logic.cmi \ - theories/Lists/polyList.cmi theories/Init/specif.cmi \ - theories/Sorting/sorting.cmi -theories/Sorting/sorting.cmx: theories/Init/logic.cmx \ - theories/Lists/polyList.cmx theories/Init/specif.cmx \ - theories/Sorting/sorting.cmi +theories/Sorting/sorting.cmo: theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Sorting/sorting.cmi +theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \ + theories/Init/specif.cmx theories/Sorting/sorting.cmi theories/Wellfounded/disjoint_Union.cmo: \ theories/Wellfounded/disjoint_Union.cmi theories/Wellfounded/disjoint_Union.cmx: \ @@ -463,13 +465,13 @@ theories/ZArith/zbool.cmx: theories/Init/datatypes.cmx \ theories/Bool/sumbool.cmx theories/ZArith/zArith_dec.cmx \ theories/ZArith/zmisc.cmx theories/ZArith/zbool.cmi theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ - theories/ZArith/wf_Z.cmi theories/ZArith/zarith_aux.cmi \ - theories/ZArith/zcomplements.cmi + theories/ZArith/fast_integer.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zcomplements.cmi theories/ZArith/zcomplements.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ - theories/ZArith/wf_Z.cmx theories/ZArith/zarith_aux.cmx \ - theories/ZArith/zcomplements.cmi + theories/ZArith/fast_integer.cmx theories/Lists/polyList.cmx \ + theories/Init/specif.cmx theories/ZArith/wf_Z.cmx \ + theories/ZArith/zarith_aux.cmx theories/ZArith/zcomplements.cmi theories/ZArith/zdiv.cmo: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ theories/ZArith/zArith_dec.cmi theories/ZArith/zarith_aux.cmi \ @@ -486,18 +488,16 @@ theories/ZArith/zlogarithm.cmx: theories/ZArith/fast_integer.cmx \ theories/ZArith/zarith_aux.cmx theories/ZArith/zlogarithm.cmi theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ - theories/ZArith/zmisc.cmi + theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ - theories/ZArith/zmisc.cmi + theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmo: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ - theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \ - theories/ZArith/zpower.cmi + theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \ - theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \ - theories/ZArith/zpower.cmi + theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \ + theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmi \ theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ theories/ZArith/zarith_aux.cmi theories/ZArith/zsqrt.cmi @@ -518,12 +518,12 @@ theories/Arith/div2.cmi: theories/Init/datatypes.cmi theories/Init/peano.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/Arith/minus.cmi \ - theories/Init/specif.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/minus.cmi: theories/Init/datatypes.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 @@ -533,7 +533,7 @@ 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/Arith/minus.cmi theories/Init/peano.cmi + theories/Init/peano.cmi theories/Bool/decBool.cmi: theories/Init/specif.cmi theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \ theories/Init/specif.cmi @@ -552,22 +552,20 @@ theories/IntMap/addec.cmi: theories/IntMap/addr.cmi \ theories/IntMap/addr.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi theories/IntMap/adist.cmi: theories/IntMap/addr.cmi \ - theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ - theories/Arith/min.cmi + theories/Init/datatypes.cmi theories/ZArith/fast_integer.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/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ - theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ - theories/Lists/polyList.cmi theories/Init/specif.cmi \ - theories/Bool/sumbool.cmi + theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Lists/polyList.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/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.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 \ @@ -603,18 +601,21 @@ 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/powerset.cmi: theories/Sets/partial_Order.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/Init/logic.cmi theories/Sets/multiset.cmi \ - theories/Init/peano.cmi theories/Lists/polyList.cmi \ - theories/Sorting/sorting.cmi theories/Init/specif.cmi + theories/Sets/multiset.cmi theories/Init/peano.cmi \ + theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \ + theories/Init/specif.cmi theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \ theories/Sets/multiset.cmi theories/Init/peano.cmi \ theories/Lists/polyList.cmi theories/Init/specif.cmi -theories/Sorting/sorting.cmi: theories/Init/logic.cmi \ - theories/Lists/polyList.cmi theories/Init/specif.cmi +theories/Sorting/sorting.cmi: theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi theories/ZArith/fast_integer.cmi: theories/Init/datatypes.cmi \ theories/Init/peano.cmi @@ -633,8 +634,9 @@ theories/ZArith/zbool.cmi: theories/Init/datatypes.cmi \ theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ theories/ZArith/zmisc.cmi theories/ZArith/zcomplements.cmi: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ - theories/ZArith/wf_Z.cmi theories/ZArith/zarith_aux.cmi + theories/ZArith/fast_integer.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/ZArith/wf_Z.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zdiv.cmi: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ theories/ZArith/zArith_dec.cmi theories/ZArith/zarith_aux.cmi \ @@ -642,10 +644,11 @@ theories/ZArith/zdiv.cmi: theories/Init/datatypes.cmi \ theories/ZArith/zlogarithm.cmi: theories/ZArith/fast_integer.cmi \ theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/specif.cmi + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zpower.cmi: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ - theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi + theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zmisc.cmi theories/ZArith/zsqrt.cmi: theories/ZArith/fast_integer.cmi \ theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ theories/ZArith/zarith_aux.cmi |