diff options
Diffstat (limited to 'contrib/extraction')
56 files changed, 1598 insertions, 3202 deletions
diff --git a/contrib/extraction/CHANGES b/contrib/extraction/CHANGES index 83ea4910..acd1dbda 100644 --- a/contrib/extraction/CHANGES +++ b/contrib/extraction/CHANGES @@ -346,8 +346,8 @@ Dyade/BDDS boolean tautology checker. Lyon/CIRCUITS multiplication via a modelization of a circuit. Lyon/FIRING-SQUAD print the states of the firing squad. Marseille/CIRCUITS compares integers via a modelization of a circuit. -Nancy/FOUnify unification of two first-orderde deux termes. -Rocq/ARITH/Chinese computation of the chinese remaindering. +Nancy/FOUnify unification of two first-order terms. +Rocq/ARITH/Chinese computation of the chinese remainder. Rocq/COC small coc typechecker. (test by B. Barras, not by me) Rocq/HIGMAN run the proof on one example. Rocq/GRAPHS linear constraints checker in Z. diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 346201ec..5ad4a288 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 8930 2006-06-09 02:14:34Z letouzey $ i*) +(*i $Id: common.ml 10596 2008-02-27 15:30:11Z letouzey $ i*) open Pp open Util @@ -17,42 +17,218 @@ open Nameops open Libnames open Table open Miniml +open Mlutil open Modutil -open Ocaml +open Mod_subst -(*S Renamings. *) +(*s Some pretty-print utility functions. *) + +let pp_par par st = if par then str "(" ++ st ++ str ")" else st + +let pp_apply st par args = match args with + | [] -> st + | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) + +let pr_binding = function + | [] -> mt () + | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l + +let fnl2 () = fnl () ++ fnl () + +let space_if = function true -> str " " | false -> mt () + +let sec_space_if = function true -> spc () | false -> mt () + +let is_digit = function + | '0'..'9' -> true + | _ -> false + +let begins_with_CoqXX s = + let n = String.length s in + n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' && + let i = ref 3 in + try while !i < n do + if s.[!i] = '_' then i:=n (*Stop*) + else if is_digit s.[!i] then incr i + else raise Not_found + done; true + with Not_found -> false + +let unquote s = + if lang () <> Scheme then s + else + let s = String.copy s in + for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; + s + +let rec dottify = function + | [] -> assert false + | [s] -> unquote s + | s::[""] -> unquote s + | s::l -> (dottify l)^"."^(unquote s) + +(*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 + +let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) +let uppercase_id id = id_of_string (String.capitalize (string_of_id id)) + +(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *) +let pr_upper_id id = str (String.capitalize (string_of_id id)) + + +(*s de Bruijn environments for programs *) + +type env = identifier list * Idset.t + +(*s Generic renaming issues for local variable names. *) + +let rec rename_id id avoid = + if Idset.mem id avoid then rename_id (lift_ident id) avoid else id + +let rec rename_vars avoid = function + | [] -> + [], avoid + | id :: idl when id == dummy_name -> + (* we don't rename dummy binders *) + let (idl', avoid') = rename_vars avoid idl in + (id :: idl', avoid') + | id :: idl -> + let (idl, avoid) = rename_vars avoid idl in + let id = rename_id (lowercase_id id) avoid in + (id :: idl, Idset.add id avoid) + +let rename_tvars avoid l = + let rec rename avoid = function + | [] -> [],avoid + | id :: idl -> + let id = rename_id (lowercase_id id) avoid in + let idl, avoid = rename (Idset.add id avoid) idl in + (id :: idl, avoid) in + fst (rename avoid l) + +let push_vars ids (db,avoid) = + let ids',avoid' = rename_vars avoid ids in + ids', (ids' @ db, avoid') + +let get_db_name n (db,_) = + let id = List.nth db (pred n) in + if id = dummy_name then id_of_string "__" else id + + +(*S Renamings of global objects. *) (*s Tables of global renamings *) let keywords = ref Idset.empty +let set_keywords kws = keywords := kws + let global_ids = ref Idset.empty -let modular = ref false +let add_global_ids s = global_ids := Idset.add s !global_ids +let global_ids_list () = Idset.elements !global_ids + +let empty_env () = [], !global_ids + +let mktable () = + let h = Hashtbl.create 97 in + (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h) + +let mkset () = + let h = Hashtbl.create 97 in + (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h) + +let mktriset () = + let h = Hashtbl.create 97 in + (fun x y z -> Hashtbl.add h (x,y,z) ()), + (fun x y z -> Hashtbl.mem h (x,y,z)), + (fun () -> Hashtbl.clear h) (* 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 l = Hashtbl.add renamings r l -let get_renamings r = Hashtbl.find renamings r + of its renaming, in [string list] form. *) +let add_renaming, get_renaming, clear_renaming = mktable () (* 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 add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable () -let modvisited = ref MPset.empty -let modcontents = ref Gset.empty -let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents -let module_contents mp s = Gset.mem (mp,s) !modcontents +(* A table for function modfstlev_rename *) +let add_modfstlev, get_modfstlev, clear_modfstlev = mktable () -let to_qualify = ref Refset.empty +(* A set of all external objects that will have to be fully qualified *) +let add_static_clash, static_clash, clear_static_clash = mkset () -let mod_1st_level = ref Idmap.empty +(* Two tables of triplets [kind * module_path * string]. The first one + will record the first level of all MPfile, not only the current one. + The second table will contains local renamings. *) -(*s Uppercase/lowercase renamings. *) +type kind = Term | Type | Cons | Mod -let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false +let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset () +let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset () + +(* The list of external modules that will be opened initially *) +let add_mpfiles, mem_mpfiles, list_mpfiles, clear_mpfiles = + let m = ref MPset.empty in + (fun mp -> m:= MPset.add mp !m), + (fun mp -> MPset.mem mp !m), + (fun () -> MPset.elements !m), + (fun () -> m:= MPset.empty) + +(*s table containing the visible horizon at a precise moment *) + +let visible = ref ([] : module_path list) +let pop_visible () = visible := List.tl !visible +let push_visible mp = visible := mp :: !visible +let top_visible_mp () = List.hd !visible + +(*s substitutions for printing signatures *) + +let substs = ref empty_subst +let add_subst msid mp = substs := add_msid msid mp !substs +let subst_mp mp = subst_mp !substs mp +let subst_kn kn = subst_kn !substs kn +let subst_con c = fst (subst_con !substs c) +let subst_ref = function + | ConstRef con -> ConstRef (subst_con con) + | IndRef (kn,i) -> IndRef (subst_kn kn,i) + | ConstructRef ((kn,i),j) -> ConstructRef ((subst_kn kn,i),j) + | _ -> assert false -let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false + +let duplicate_index = ref 0 +let to_duplicate = ref Gmap.empty +let add_duplicate mp l = + incr duplicate_index; + let ren = "Coq__" ^ string_of_int (!duplicate_index) in + to_duplicate := Gmap.add (mp,l) ren !to_duplicate +let check_duplicate mp l = + let mp' = subst_mp mp in + Gmap.find (mp',l) !to_duplicate + +type reset_kind = OnlyLocal | AllButExternal | Everything + +let reset_allbutext () = + clear_loc_mpmem (); + global_ids := !keywords; + clear_renaming (); + clear_mp_renaming (); + clear_modfstlev (); + clear_static_clash (); + clear_mpfiles (); + duplicate_index := 0; + to_duplicate := Gmap.empty; + visible := []; + substs := empty_subst + +let reset_everything () = reset_allbutext (); clear_ext_mpmem () + +let reset_renaming_tables = function + | OnlyLocal -> clear_loc_mpmem () + | AllButExternal -> reset_allbutext () + | Everything -> reset_everything () + +(*S Renaming functions *) (* This function creates from [id] a correct uppercase/lowercase identifier. This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes @@ -69,389 +245,238 @@ let modular_rename up id = then prefix ^ s else s -let rename_module = modular_rename true - -(* [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 - module [mp1-l] contains [s]. - The verification stops if we encounter [mp1=mp0]. *) - -exception Stop - -let clash mp0 l s mpl = - let rec clash_one mp = match mp with - | _ when mp = mp0 -> raise Stop - | MPdot (mp',_) -> - (module_contents (add_labels_mp mp l) s) || (clash_one mp') - | mp when is_toplevel mp -> false - | _ -> module_contents (add_labels_mp mp l) s +(*s [record_contents_fstlev] finds the names of the first-level objects + exported by the ground-level modules in [struc]. *) + +let rec record_contents_fstlev struc = + let upper_type = (lang () = Haskell) in + let addtyp mp id = add_ext_mpmem Type mp (modular_rename upper_type id) in + let addcons mp id = add_ext_mpmem Cons mp (modular_rename true id) in + let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in + let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in + let addfix mp r = + add_ext_mpmem Term mp (modular_rename false (id_of_global r)) + in + let f mp = function + | (l,SEdecl (Dind (_,ind))) -> + Array.iter + (fun ip -> + addtyp mp ip.ip_typename; Array.iter (addcons mp) ip.ip_consnames) + ind.ind_packets + | (l,SEdecl (Dtype _)) -> addtyp mp (id_of_label l) + | (l,SEdecl (Dterm _)) -> addterm mp (id_of_label l) + | (l,SEdecl (Dfix (rv,_,_))) -> Array.iter (addfix mp) rv + | (l,SEmodule _) -> addmod mp (id_of_label l) + | (l,SEmodtype _) -> addmod mp (id_of_label l) in - let rec clash_list = function - | [] -> false - | mp :: mpl -> (clash_one mp) || (clash_list mpl) - in try clash_list mpl with Stop -> false - -(*s [contents_first_level mp] finds the names of the first-level objects - exported by module [mp]. Nota: it might fail if [mp] isn't a directly - visible module. Ex: [MPself] under functor, [MPbound], etc ... *) - -let contents_first_level mp = - if not (MPset.mem mp !modvisited) then begin - modvisited := MPset.add mp !modvisited; - match (Global.lookup_module mp).mod_type with - | MTBsig (msid,msb) -> - let add b id = add_module_contents mp (modular_rename b id) in - let upper_type = (lang () = Haskell) in - List.iter - (function - | (l, SPBconst cb) -> - (match Extraction.constant_kind (Global.env ()) cb with - | Extraction.Logical -> () - | Extraction.Type -> add upper_type (id_of_label l) - | Extraction.Term -> add false (id_of_label l)) - | (_, SPBmind mib) -> - Array.iter - (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) - mib.mind_packets - | _ -> ()) - (Modops.subst_signature_msid msid mp msb) - | _ -> () - end + List.iter (fun (mp,sel) -> List.iter (f mp) sel) struc -(*s Initial renamings creation, for modular extraction. *) +(*s For monolithic extraction, first-level modules might have to be renamed + with unique numbers *) -let rec mp_create_modular_renamings mp = - try mp_get_renamings mp +let modfstlev_rename l = + let coqid = id_of_string "Coq" in + let id = id_of_label l in + try + let coqset = get_modfstlev id in + let nextcoq = next_ident_away coqid coqset in + add_modfstlev id (nextcoq::coqset); + (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 + (add_modfstlev id [coqid]; "Coq_"^s) + else + (add_modfstlev id []; s) + + +(*s Creating renaming for a [module_path] *) + +let rec mp_create_renaming mp = + try get_mp_renaming mp with Not_found -> let ren = match mp with + | _ when not (modular ()) && at_toplevel mp -> [""] | 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 lmp = mp_create_renaming mp in + if lmp = [""] then (modfstlev_rename l)::lmp + else (modular_rename true (id_of_label l))::lmp + | MPself msid -> [modular_rename true (id_of_msid msid)] + | MPbound mbid -> [modular_rename true (id_of_mbid mbid)] + | MPfile _ when not (modular ()) -> assert false + | MPfile _ -> [string_of_modfile mp] + in add_mp_renaming mp ren; ren + +(* [clash mp0 s mpl] checks if [mp0-s] can be printed as [s] when + [mpl] is the context of visible modules. More precisely, we check if + there exists a [mp] in [mpl] that contains [s]. + The verification stops if we encounter [mp=mp0]. *) +let rec clash mem mp0 s = function + | [] -> false + | mp :: _ when mp = mp0 -> false + | mp :: mpl -> mem mp s || clash mem mp0 s mpl + +(*s Initial renamings creation, for modular extraction. *) let create_modular_renamings struc = let current_module = fst (List.hd struc) in - let modfiles = ref MPset.empty in - let { up = u ; down = d } = struct_get_references_set struc + let { typ = ty ; trm = tr ; cons = co } = struct_get_references_set struc in (* 1) creates renamings of objects *) let add upper r = let mp = modpath_of_r r in - let l = mp_create_modular_renamings mp in + let l = mp_create_renaming 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); + add_global_ids (id_of_string s); + add_renaming r (s::l); begin try - let mp = modfile_of_mp mp in - if mp <> current_module then modfiles := MPset.add mp !modfiles + let mp = modfile_of_mp mp in if mp <> current_module then add_mpfiles mp with Not_found -> () end; in - Refset.iter (add true) u; - Refset.iter (add false) d; + Refset.iter (add (lang () = Haskell)) ty; + Refset.iter (add true) co; + Refset.iter (add false) tr; (* 2) determines the opened libraries. *) - let used_modules = MPset.elements !modfiles in - - (* [s] will contain all first-level sub-modules of [cur_mp] *) - let s = ref Stringset.empty in - begin - let add l = s := Stringset.add (rename_module (id_of_label l)) !s in - match (Global.lookup_module current_module).mod_type with - | MTBsig (_,msb) -> - List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb - | _ -> () - end; - (* We now compare [s] with the modules coming from [used_modules]. *) - List.iter - (function - | MPfile d -> - let s_mp = - String.capitalize (string_of_id (List.hd (repr_dirpath d))) in - if Stringset.mem s_mp !s then error_module_clash s_mp - else s:= Stringset.add s_mp !s - | _ -> assert false) - used_modules; + let used_modules = list_mpfiles () in + let used_modules' = List.rev used_modules in + let str_list = List.map string_of_modfile used_modules' + in + let rec check_elsewhere mpl sl = match mpl, sl with + | [], [] -> [] + | mp::mpl, _::sl -> + if List.exists (ext_mpmem Mod mp) sl then + check_elsewhere mpl sl + else mp :: (check_elsewhere mpl sl) + | _ -> assert false + in + let opened_modules = check_elsewhere used_modules' str_list in + clear_mpfiles (); + List.iter add_mpfiles opened_modules; (* 3) determines the potential clashes *) - List.iter contents_first_level used_modules; - let used_modules' = List.rev used_modules in - let needs_qualify r = + let needs_qualify k r = 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 + if (is_modfile mp) && mp <> current_module && + (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules) + then add_static_clash r in - Refset.iter needs_qualify u; - Refset.iter needs_qualify d; - used_modules + Refset.iter (needs_qualify Type) ty; + Refset.iter (needs_qualify Term) tr; + Refset.iter (needs_qualify Cons) co; + List.rev opened_modules (*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 { up = u ; down = d } = struct_get_references_list struc in + let { typ = ty ; trm = tr ; cons = co } = struct_get_references_list struc in let add upper r = let mp = modpath_of_r r in - let l = mp_create_mono_renamings mp in + let l = mp_create_renaming mp in let mycase = if upper then uppercase_id else lowercase_id in let id = if l = [""] then - next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids) + next_ident_away (mycase (id_of_global r)) (global_ids_list ()) else id_of_string (modular_rename upper (id_of_global r)) in - global_ids := Idset.add id !global_ids; - rename r ((string_of_id id)::l) + add_global_ids id; + add_renaming r ((string_of_id id)::l) in - List.iter (add true) (List.rev u); - List.iter (add false) (List.rev d) - -(*s Renaming issues at toplevel *) - -module TopParams = struct - let globals () = Idset.empty - let pp_global _ r = pr_id (id_of_global r) - let pp_module _ mp = str (string_of_mp mp) -end - -(*s Renaming issues for a monolithic or modular extraction. *) - -module StdParams = struct - - let globals () = !global_ids - - let unquote s = - if lang () <> Scheme then s - else - let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; - s - - let rec dottify = function - | [] -> assert false - | [s] -> unquote s - | s::[""] -> unquote s - | s::l -> (dottify l)^"."^(unquote s) - - let pp_global mpl r = - let ls = get_renamings r in - let s = List.hd ls in - let mp = modpath_of_r r in - let ls = - if mp = List.hd mpl then [s] (* simpliest situation *) - 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 - 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]. *) - if !modular && (at_toplevel mp) - then snd (list_sep_last ls) - else ls - in str (dottify ls) - -end - -module ToplevelPp = Ocaml.Make(TopParams) -module OcamlPp = Ocaml.Make(StdParams) -module HaskellPp = Haskell.Make(StdParams) -module SchemePp = Scheme.Make(StdParams) - -let pp_decl mp d = match lang () with - | Ocaml -> OcamlPp.pp_decl mp d - | Haskell -> HaskellPp.pp_decl mp d - | Scheme -> SchemePp.pp_decl mp d - | Toplevel -> ToplevelPp.pp_decl mp d - -let pp_struct s = match lang () with - | Ocaml -> OcamlPp.pp_struct s - | Haskell -> HaskellPp.pp_struct s - | Scheme -> SchemePp.pp_struct s - | Toplevel -> ToplevelPp.pp_struct s - -let pp_signature s = match lang () with - | Ocaml -> OcamlPp.pp_signature s - | Haskell -> HaskellPp.pp_signature s - | _ -> assert false - -let set_keywords () = - (match lang () with - | Ocaml -> keywords := Ocaml.keywords - | Haskell -> keywords := Haskell.keywords - | Scheme -> keywords := Scheme.keywords - | Toplevel -> keywords := Idset.empty); - global_ids := !keywords; - to_qualify := Refset.empty + List.iter (add (lang () = Haskell)) (List.rev ty); + List.iter (add false) (List.rev tr); + List.iter (add true) (List.rev co); + [] + +let create_renamings struc = + if modular () then create_modular_renamings struc + else create_mono_renamings struc -let preamble prm = match lang () with - | Ocaml -> Ocaml.preamble prm - | Haskell -> Haskell.preamble prm - | Scheme -> Scheme.preamble prm - | Toplevel -> (fun _ _ _ -> mt ()) - -let preamble_sig prm = match lang () with - | Ocaml -> Ocaml.preamble_sig prm - | _ -> assert false - -(*S Extraction of one decl to stdout. *) - -let print_one_decl struc mp decl = - set_keywords (); - modular := false; - create_mono_renamings struc; - msgnl (pp_decl [mp] decl) - -(*S Extraction to a file. *) - -let info f = - Options.if_verbose msgnl - (str ("The file "^f^" has been created by extraction.")) - -let print_structure_to_file f prm struc = - Hashtbl.clear renamings; - mod_1st_level := Idmap.empty; - modcontents := Gset.empty; - modvisited := MPset.empty; - set_keywords (); - modular := prm.modular; - let used_modules = - if lang () = Toplevel then [] - else if prm.modular then create_modular_renamings struc - else (create_mono_renamings struc; []) - in - let print_dummys = - (struct_ast_search ((=) MLdummy) 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_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 - begin try - msg_with ft (preamble prm used_modules print_dummys print_magic); - msg_with ft (pp_struct struc); - option_iter close_out cout; - with e -> - option_iter close_out cout; raise e - end; - option_iter (fun (f,_) -> info f) f; - (* print the signature *) - match f with - | Some (_,f) when lang () = Ocaml -> - let cout = open_out f in - let ft = Pp_control.with_output_to cout in - begin try - msg_with ft (preamble_sig prm used_modules print_dummys); - msg_with ft (pp_signature (signature_of_structure struc)); - close_out cout; - with e -> - close_out cout; raise e - end; - info f - | _ -> () - - -(*i - (* DO NOT REMOVE: used when making names resolution *) - let cout = open_out (f^".ren") in - let ft = Pp_control.with_output_to cout in - Hashtbl.iter - (fun r id -> - if short_module r = !current_module then - msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r))) - renamings; - pp_flush_with ft (); - close_out cout; -i*) - - - - - - + +(*s On-the-fly qualification issues for both monolithic or modular extraction. *) + +let pp_global k r = + let ls = get_renaming r in + assert (List.length ls > 1); + let s = List.hd ls in + let mp = modpath_of_r r in + if mp = top_visible_mp () then + (* simpliest situation: definition of r (or use in the same context) *) + (* we update the visible environment *) + (add_loc_mpmem k mp s; unquote s) + else match lang () with + | Scheme -> unquote s (* no modular Scheme extraction... *) + | Haskell -> + (* for the moment we always qualify in modular Haskell *) + if modular () then dottify ls else s + | Ocaml -> + try (* has [mp] something in common with one of [!visible] ? *) + let prefix = common_prefix_from_list mp !visible in + let delta = mp_length mp - mp_length prefix in + let ls = list_firstn (delta+1) ls in + (* Difficulty: in ocaml we cannot qualify more than [ls], + but this (not-so-long) name can in fact be hidden. Solution: + duplication of the _definition_ of r in a Coq__XXX module *) + let s,ls' = list_sep_last ls in + let k' = if ls' = [] then k else Mod in + if clash (loc_mpmem k') prefix s !visible then + let front = if ls' = [] then [s] else ls' in + let l = get_nth_label delta r in + try dottify (front @ [check_duplicate prefix l]) + with Not_found -> add_duplicate prefix l; dottify ls + else dottify ls + with Not_found -> + (* [mp] belongs to a closed module, not one of [!visible]. *) + let base = base_mp mp in + let base_s,ls1 = list_sep_last ls in + let s,ls2 = list_sep_last ls1 in + let k' = if ls2 = [] then k else Mod in + if modular () && (mem_mpfiles base) && + not (static_clash r) && + (* k' = Mod can't clash in an opened module, see earlier check *) + not (clash (loc_mpmem k') base s !visible) + then (* Standard situation of an object in another file: *) + (* Thanks to the "open" of this file we remove its name *) + dottify ls1 + else if clash (loc_mpmem Mod) base base_s !visible then + error_module_clash base_s + else dottify ls + +(* The next function is used only in Ocaml extraction...*) +let pp_module mp = + let ls = mp_create_renaming mp in + if List.length ls = 1 then dottify ls + else match mp with + | MPdot (mp0,_) when mp0 = top_visible_mp () -> + (* simpliest situation: definition of mp (or use in the same context) *) + (* we update the visible environment *) + let s = List.hd ls in + add_loc_mpmem Mod mp0 s; s + | _ -> + try (* has [mp] something in common with one of those in [!visible] ? *) + let prefix = common_prefix_from_list mp !visible in + assert (mp <> prefix); (* no use of mp as whole module from itself *) + let delta = mp_length mp - mp_length prefix in + let ls = list_firstn delta ls in + (* Difficulty: in ocaml we cannot qualify more than [ls], + but this (not-so-long) name can in fact be hidden. Solution: + duplication of the _definition_ of mp via a Coq__XXX module *) + let s,ls' = list_sep_last ls in + if clash (loc_mpmem Mod) prefix s !visible then + let l = get_nth_label_mp delta mp in + try dottify (ls' @ [check_duplicate prefix l]) + with Not_found -> add_duplicate prefix l; dottify ls + else dottify ls + with Not_found -> + (* [mp] belongs to a closed module, not one of [!visible]. *) + let base = base_mp mp in + let base_s,ls' = list_sep_last ls in + let s = fst (list_sep_last ls) in + if modular () && (mem_mpfiles base) && + not (clash (loc_mpmem Mod) base s !visible) + then dottify ls' + else if clash (loc_mpmem Mod) base base_s !visible then + error_module_clash base_s + else dottify ls diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 2ba51e1c..5cd26584 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -6,16 +6,56 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: common.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) open Names +open Libnames open Miniml open Mlutil +open Pp -val print_one_decl : - ml_structure -> module_path -> ml_decl -> unit +val fnl2 : unit -> std_ppcmds +val space_if : bool -> std_ppcmds +val sec_space_if : bool -> std_ppcmds -val print_structure_to_file : - (string * string) option -> extraction_params -> ml_structure -> unit +val pp_par : bool -> std_ppcmds -> std_ppcmds +val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pr_binding : identifier list -> std_ppcmds +val rename_id : identifier -> Idset.t -> identifier +val lowercase_id : identifier -> identifier +val uppercase_id : identifier -> identifier + +val pr_upper_id : identifier -> std_ppcmds + +type env = identifier list * Idset.t +val empty_env : unit -> env + +val rename_vars: Idset.t -> identifier list -> env +val rename_tvars: Idset.t -> identifier list -> identifier list +val push_vars : identifier list -> env -> identifier list * env +val get_db_name : int -> env -> identifier + +val record_contents_fstlev : ml_structure -> unit + +val create_renamings : ml_structure -> module_path list + +type kind = Term | Type | Cons | Mod + +val pp_global : kind -> global_reference -> string +val pp_module : module_path -> string + +val top_visible_mp : unit -> module_path +val push_visible : module_path -> unit +val pop_visible : unit -> unit + +val add_subst : mod_self_id -> module_path -> unit + +val check_duplicate : module_path -> label -> string + +type reset_kind = OnlyLocal | AllButExternal | Everything + +val reset_renaming_tables : reset_kind -> unit + +val set_keywords : Idset.t -> unit diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 825b3554..311b42c0 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 10209 2007-10-09 21:49:37Z letouzey $ i*) +(*i $Id: extract_env.ml 10794 2008-04-15 00:12:06Z letouzey $ i*) open Term open Declarations @@ -21,7 +21,9 @@ open Modutil open Common open Mod_subst -(*s Obtaining Coq environment. *) +(***************************************) +(*S Part I: computing Coq environment. *) +(***************************************) let toplevel_env () = let seg = Lib.contents_after None in @@ -29,16 +31,17 @@ 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 (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) + | "CONSTANT" -> SFBconst (Global.lookup_constant (constant_of_kn kn)) + | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) + | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l))) + | "MODULE TYPE" -> + SFBmodtype (Global.lookup_modtype (MPdot (mp,l))) | _ -> failwith "caught" in l,seb | _ -> failwith "caught" in match current_toplevel () with - | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg)) + | MPself msid -> SEBstruct (msid, List.rev (map_succeed get_reference seg)) | _ -> assert false let environment_until dir_opt = @@ -130,58 +133,87 @@ let factor_fix env l cb msb = list_iter_i (fun j -> function - | (l,SEBconst cb') -> + | (l,SFBconst cb') -> if check <> check_fix env cb' (j+1) then raise Impossible; labels.(j+1) <- l; | _ -> raise Impossible) msb'; labels, recd, msb'' end -let rec extract_msig env mp = function +(* From a [structure_body] (i.e. a list of [structure_field_body]) + to specifications. *) + +let rec extract_sfb_spec env mp = function | [] -> [] - | (l,SPBconst cb) :: msig -> + | (l,SFBconst cb) :: msig -> 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 mp msig - else begin - Visit.add_spec_deps s; - (l,Spec s) :: (extract_msig env mp msig) - end - | (l,SPBmind cb) :: msig -> + let specs = extract_sfb_spec env mp msig in + if logical_spec s then specs + else begin Visit.add_spec_deps s; (l,Spec s) :: specs end + | (l,SFBmind 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 mp msig - else begin - Visit.add_spec_deps s; - (l,Spec s) :: (extract_msig env mp msig) - end - | (l,SPBmodule {msb_modtype=mtb}) :: msig -> - (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig) - | (l,SPBmodtype mtb) :: msig -> - (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig) - -and extract_mtb env mpo = function - | MTBident kn -> Visit.add_kn kn; MTident kn - | MTBfunsig (mbid, mtb, mtb') -> + let specs = extract_sfb_spec env mp msig in + if logical_spec s then specs + else begin Visit.add_spec_deps s; (l,Spec s) :: specs end + | (l,SFBmodule mb) :: msig -> + let specs = extract_sfb_spec env mp msig in + let mtb = Modops.type_of_mb env mb in + let spec = extract_seb_spec env (mb.mod_type<>None) mtb in + (l,Smodule spec) :: specs + | (l,SFBmodtype mtb) :: msig -> + let specs = extract_sfb_spec env mp msig in + (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs + | (l,SFBalias(mp1,_))::msig -> + extract_sfb_spec env mp + ((l,SFBmodule {mod_expr = Some (SEBident mp1); + mod_type = None; + mod_constraints = Univ.Constraint.empty; + mod_alias = Mod_subst.empty_subst; + mod_retroknowledge = []})::msig) + +(* From [struct_expr_body] to specifications *) + + +and extract_seb_spec env truetype = function + | SEBident kn when truetype -> Visit.add_mp kn; MTident kn + | SEBwith(mtb',With_definition_body(idl,cb))-> + let mtb''= extract_seb_spec env truetype mtb' in + (match extract_with_type env cb with (* cb peut contenir des kn *) + | None -> mtb'' + | Some (vl,typ) -> MTwith(mtb'',ML_With_type(idl,vl,typ))) + | SEBwith(mtb',With_module_body(idl,mp,_))-> + Visit.add_mp mp; + MTwith(extract_seb_spec env truetype mtb', + ML_With_module(idl,mp)) + | SEBfunctor (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 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_module mp (Modops.module_body_of_type mtb) env in + MTfunsig (mbid, extract_seb_spec env true mtb.typ_expr, + extract_seb_spec env' truetype mtb') + | SEBstruct (msid, msig) -> + let mp = MPself msid in let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_msig env' mp msig) + MTsig (msid, extract_sfb_spec env' mp msig) + | (SEBapply _|SEBident _ (*when not truetype*)) as mtb -> + extract_seb_spec env truetype (Modops.eval_struct env mtb) + + +(* From a [structure_body] (i.e. a list of [structure_field_body]) + to implementations. -let rec extract_msb env mp all = function + NB: when [all=false], the evaluation order of the list is + important: last to first ensures correct dependencies. +*) + +let rec extract_sfb env mp all = function | [] -> [] - | (l,SEBconst cb) :: msb -> + | (l,SFBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in let vc = Array.map (make_con mp empty_dirpath) vl in - let ms = extract_msb env mp all msb in + let ms = extract_sfb env mp all msb in let b = array_exists Visit.needed_con vc in if all || b then let d = extract_fixpoint env vc recd in @@ -189,7 +221,7 @@ let rec extract_msb env mp all = function else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_msb env mp all msb in + let ms = extract_sfb 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 @@ -197,8 +229,8 @@ let rec extract_msb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) - | (l,SEBmind mib) :: msb -> - let ms = extract_msb env mp all msb in + | (l,SFBmind mib) :: msb -> + let ms = extract_sfb env mp all msb in let kn = make_kn mp empty_dirpath l in let b = Visit.needed_kn kn in if all || b then @@ -206,48 +238,68 @@ let rec extract_msb env mp all = function if (not b) && (logical_decl d) then ms else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms - | (l,SEBmodule mb) :: msb -> - let ms = extract_msb env mp all msb in + | (l,SFBmodule mb) :: msb -> + let ms = extract_sfb env mp all msb in let mp = MPdot (mp,l) in 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 mp all msb in - let kn = make_kn mp empty_dirpath l in - if all || Visit.needed_kn kn then - (l,SEmodtype (extract_mtb env None mtb)) :: ms + | (l,SFBmodtype mtb) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms + else ms + | (l,SFBalias (mp1,cst)) :: msb -> + let ms = extract_sfb env mp all msb in + let mp = MPdot (mp,l) in + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true + {mod_expr = Some (SEBident mp1); + mod_type = None; + mod_constraints= Univ.Constraint.empty; + mod_alias = empty_subst; + mod_retroknowledge = []})) :: ms else ms -and extract_meb env mpo all = function - | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *) - | MEBident mp -> Visit.add_mp mp; MEident mp - | MEBapply (meb, meb',_) -> - MEapply (extract_meb env None true meb, - extract_meb env None true meb') - | MEBfunctor (mbid, mtb, meb) -> +(* From [struct_expr_body] to implementations *) + +and extract_seb env mpo all = function + | SEBident mp -> + if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; + Visit.add_mp mp; MEident mp + | SEBapply (meb, meb',_) -> + MEapply (extract_seb env None true meb, + extract_seb env None true meb') + | SEBfunctor (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 None mtb, - extract_meb env' None true meb) - | MEBstruct (msid, msb) -> + MEfunctor (mbid, extract_seb_spec env true mtb.typ_expr, + extract_seb env' None true meb) + | SEBstruct (msid, msb) -> let mp,msb = match mpo with | None -> MPself msid, msb - | Some mp -> mp, subst_msb (map_msid msid mp) msb + | Some mp -> mp, Modops.subst_structure (map_msid msid mp) msb in - let env' = add_structure mp msb env in - MEstruct (msid, extract_msb env' mp all msb) + let env' = Modops.add_signature mp msb env in + MEstruct (msid, extract_sfb env' mp all msb) + | SEBwith (_,_) -> anomaly "Not available yet" 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 - let mtb = match mb.mod_user_type with None -> mb.mod_type | Some mt -> mt in + let meb = Option.get mb.mod_expr in + let mtb = match mb.mod_type with + | None -> Modops.eval_struct env meb + | Some mt -> mt + in (* 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 (Some mp) all meb; - ml_mod_type = extract_mtb env None mtb } + (* PL 26/02/2008: is this still relevant ? + let mtb = replicate_msid meb mtb in *) + { ml_mod_expr = extract_seb env (Some mp) all meb; + ml_mod_type = extract_seb_spec env (mb.mod_type<>None) mtb } + let unpack = function MEstruct (_,sel) -> sel | _ -> assert false @@ -258,161 +310,198 @@ let mono_environment refs mpl = let env = Global.env () in let l = List.rev (environment_until None) in List.rev_map - (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l + (fun (mp,m) -> mp, unpack (extract_seb env (Some mp) false m)) l + +(**************************************) +(*S Part II : Input/Output primitives *) +(**************************************) + +let descr () = match lang () with + | Ocaml -> Ocaml.ocaml_descr + | Haskell -> Haskell.haskell_descr + | Scheme -> Scheme.scheme_descr + +(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" + Works similarly for the other languages. *) + +let default_id = id_of_string "Main" + +let mono_filename f = + let d = descr () in + match f with + | None -> None, None, default_id + | Some f -> + let f = + if Filename.check_suffix f d.file_suffix then + Filename.chop_suffix f d.file_suffix + else f + in + let id = + if lang () <> Haskell then default_id + else try id_of_string (Filename.basename f) + with _ -> error "Extraction: provided filename is not a valid identifier" + in + Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id + +(* Builds a suitable filename from a module id *) + +let module_filename m = + let d = descr () in + let f = if d.capital_file then String.capitalize else String.uncapitalize in + let fn = f (string_of_id m) in + Some (fn^d.file_suffix), Option.map ((^) fn) d.sig_suffix, m + +(*s Extraction of one decl to stdout. *) + +let print_one_decl struc mp decl = + let d = descr () in + reset_renaming_tables AllButExternal; + ignore (create_renamings struc); + push_visible mp; + msgnl (d.pp_decl decl); + pop_visible () + +(*s Extraction of a ml struct to a file. *) + +let print_structure_to_file (fn,si,mo) struc = + let d = descr () in + reset_renaming_tables AllButExternal; + let used_modules = create_renamings struc in + let unsafe_needs = { + mldummy = struct_ast_search ((=) MLdummy) struc; + tdummy = struct_type_search Mlutil.isDummy struc; + tunknown = struct_type_search ((=) Tunknown) struc; + magic = + if lang () <> Haskell then false + else struct_ast_search (function MLmagic _ -> true | _ -> false) struc } + in + (* print the implementation *) + let cout = Option.map open_out fn in + let ft = match cout with + | None -> !Pp_control.std_ft + | Some cout -> Pp_control.with_output_to cout in + begin try + msg_with ft (d.preamble mo used_modules unsafe_needs); + if lang () = Ocaml then begin + (* for computing objects to duplicate *) + let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in + msg_with devnull (d.pp_struct struc); + reset_renaming_tables OnlyLocal; + end; + msg_with ft (d.pp_struct struc); + Option.iter close_out cout; + with e -> + Option.iter close_out cout; raise e + end; + Option.iter info_file fn; + (* print the signature *) + Option.iter + (fun si -> + let cout = open_out si in + let ft = Pp_control.with_output_to cout in + begin try + msg_with ft (d.sig_preamble mo used_modules unsafe_needs); + reset_renaming_tables OnlyLocal; + msg_with ft (d.pp_sig (signature_of_structure struc)); + close_out cout; + with e -> + close_out cout; raise e + end; + info_file si) + si + + +(*********************************************) +(*s Part III: the actual extraction commands *) +(*********************************************) + + +let reset () = + Visit.reset (); reset_tables (); reset_renaming_tables Everything + +let init modular = + check_inside_section (); check_inside_module (); + set_keywords (descr ()).keywords; + set_modular modular; + reset (); + if modular && lang () = Scheme then error_scheme () + - (*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. *) + \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when + extracting to a file with the command: + \verb!Extraction "file"! [qualid1] ... [qualidn]. *) -let mono_extraction (f,m) qualids = - check_inside_section (); - check_inside_module (); +let full_extraction f qualids = + init false; let rec find = function | [] -> [],[] | q::l -> let refs,mps = find l in try - let mp = Nametab.locate_module (snd (qualid_of_reference q)) - in refs,(mp::mps) + let mp = Nametab.locate_module (snd (qualid_of_reference q)) in + if is_modfile mp then error_MPfile_as_mod mp true; + refs,(mp::mps) with Not_found -> (Nametab.global q)::refs, mps - in + in let refs,mps = find qualids in - 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 struc = optimize_struct refs (mono_environment refs mps) in + warning_axioms (); + print_structure_to_file (mono_filename f) struc; + reset () -let extraction_rec = mono_extraction (None,id_of_string "Main") -(*s Extraction in the Coq toplevel. We display the extracted term in - Ocaml syntax and we use the Coq printers for globals. The - vernacular command is \verb!Extraction! [qualid]. *) +(*s Simple extraction in the Coq toplevel. The vernacular command + is \verb!Extraction! [qualid]. *) -let extraction qid = - check_inside_section (); - check_inside_module (); +let simple_extraction qid = + init false; try - let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in - extraction_rec [qid] + let mp = Nametab.locate_module (snd (qualid_of_reference qid)) in + if is_modfile mp then error_MPfile_as_mod mp true; + full_extraction None [qid] with Not_found -> let r = Nametab.global qid in if is_custom r then msgnl (str "User defined extraction:" ++ spc () ++ str (find_custom r) ++ fnl ()) else - let prm = - { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let struc = optimize_struct prm None (mono_environment [r] []) in + let struc = optimize_struct [r] (mono_environment [r] []) in let d = get_decl_in_structure r struc in + warning_axioms (); print_one_decl struc (modpath_of_r r) d; - Visit.reset (); - reset_tables () - -(*s Extraction to a file (necessarily recursive). - The vernacular command is - \verb!Extraction "file"! [qualid1] ... [qualidn].*) - -let lang_suffix () = match lang () with - | Ocaml -> ".ml",".mli" - | Haskell -> ".hs",".hi" - | Scheme -> ".scm",".scm" - | Toplevel -> assert false - -let filename f = - let s,s' = lang_suffix () in - if Filename.check_suffix f s then - let f' = Filename.chop_suffix f s in - Some (f,f'^s'),id_of_string f' - else Some (f^s,f^s'),id_of_string f - -let extraction_file f vl = - if lang () = Toplevel then error_toplevel () - else mono_extraction (filename f) vl - -(*s Extraction of a module at the toplevel. *) - -let extraction_module m = - check_inside_section (); - check_inside_module (); - begin match lang () with - | Toplevel -> error_toplevel () - | Scheme -> error_scheme () - | _ -> () - 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 () + reset () (*s (Recursive) Extraction of a library. The vernacular command is \verb!(Recursive) Extraction Library! [M]. *) -let module_file_name m = match lang () with - | Ocaml -> let f = String.uncapitalize (string_of_id m) in f^".ml", f^".mli" - | Haskell -> let f = String.capitalize (string_of_id m) in f^".hs", f^".hi" - | _ -> assert false - -let dir_module_of_id m = - let q = make_short_qualid m in - try Nametab.full_name_module q with Not_found -> error_unknown_module q - let extraction_library is_rec m = - check_inside_section (); - check_inside_module (); - begin match lang () with - | Toplevel -> error_toplevel () - | Scheme -> error_scheme () - | _ -> () - end; - let dir_m = dir_module_of_id m in - Visit.reset (); + init true; + let dir_m = + let q = make_short_qualid m in + try Nametab.full_name_module q with Not_found -> error_unknown_module q + in 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 + then (mp, unpack (extract_seb 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 struc = optimize_struct [] struc in + warning_axioms (); + record_contents_fstlev struc; 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_structure_to_file (module_filename short_m) [e]; print l | _ -> assert false in print struc; - Visit.reset (); - reset_tables () - - - - - + reset () diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index a09464a1..8d906985 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -6,15 +6,18 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: extract_env.mli 10895 2008-05-07 16:06:26Z letouzey $ i*) (*s This module declares the extraction commands. *) open Names open Libnames -val extraction : reference -> unit -val extraction_rec : reference list -> unit -val extraction_file : string -> reference list -> unit -val extraction_module : reference -> unit +val simple_extraction : reference -> unit +val full_extraction : string option -> reference list -> unit val extraction_library : bool -> identifier -> unit + +(* For debug / external output via coqtop.byte + Drop : *) + +val mono_environment : + global_reference list -> module_path list -> Miniml.ml_structure diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6982ffc6..fdc84a64 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 10195 2007-10-08 01:47:55Z letouzey $ i*) +(*i $Id: extraction.ml 10497 2008-02-01 12:18:37Z soubiran $ i*) (*i*) open Util @@ -310,7 +310,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) with Not_found -> (* 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; + 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 @@ -337,7 +337,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *) {ind_info = Standard; ind_nparams = npar; ind_packets = packets; - ind_equiv = mib.mind_equiv }; + ind_equiv = match mib.mind_equiv with + | None -> NoEquiv + | Some kn -> Equiv kn + }; (* Second pass: we extract constructors *) for i = 0 to mib.mind_ntypes - 1 do let p = packets.(i) in @@ -410,7 +413,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (Inductive.type_of_inductive env (mib,mip0)) in List.iter - (option_iter + (Option.iter (fun kn -> if Cset.mem kn !projs then add_projection n kn)) (lookup_projections ip) with Not_found -> () @@ -421,7 +424,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets; - ind_equiv = mib.mind_equiv} + ind_equiv = match mib.mind_equiv with + | None -> NoEquiv + | Some kn -> Equiv kn } in add_ind kn mib i; i @@ -750,7 +755,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = end else (* Standard case: we apply [extract_branch]. *) - MLcase (mi.ind_info, a, Array.init br_size extract_branch) + MLcase ((mi.ind_info,[]), a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) @@ -828,18 +833,18 @@ let extract_constant env kn cb = | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with | (Info,TypeScheme) -> - if not (is_custom r) then warning_info_ax r; + if not (is_custom r) then add_info_axiom r; let n = type_scheme_nb_args env typ in let ids = iterate (fun l -> anonymous::l) n [] in Dtype (r, ids, Taxiom) | (Info,Default) -> - if not (is_custom r) then warning_info_ax r; + if not (is_custom r) then add_info_axiom 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 Ktype) + add_log_axiom r; Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> - warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother)) + add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother)) | Some body -> (match flag_of_type env typ with | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother) @@ -871,6 +876,20 @@ let extract_constant_spec env kn cb = let t = snd (record_constant_type env kn (Some typ)) in Sval (r, type_expunge env t) +let extract_with_type env cb = + let typ = Typeops.type_of_constant_type env cb.const_type in + match flag_of_type env typ with + | (_ , Default) -> None + | (Logic, TypeScheme) ->Some ([],Tdummy Ktype) + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + (match cb.const_body with + | None -> assert false + | Some body -> + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) + in Some ( vl, t) ) + let extract_inductive env kn = let ind = extract_ind env kn in add_recursors env kn; @@ -880,24 +899,6 @@ let extract_inductive env kn = ind.ind_packets in { ind with ind_packets = packets } -(*s From a global reference to a ML declaration. *) - -let extract_declaration env r = match r with - | ConstRef kn -> extract_constant env kn (Environ.lookup_constant kn env) - | IndRef (kn,_) -> Dind (kn, extract_inductive env kn) - | ConstructRef ((kn,_),_) -> Dind (kn, extract_inductive env kn) - | VarRef kn -> assert false - -(*s Without doing complete extraction, just guess what a constant would be. *) - -type kind = Logical | Term | Type - -let constant_kind env cb = - match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with - | (Logic,_) -> Logical - | (Info,TypeScheme) -> Type - | (Info,Default) -> Term - (*s Is a [ml_decl] logical ? *) let logical_decl = function @@ -916,9 +917,3 @@ let logical_spec = function | 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 1dfd7e1a..6d41b630 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 6303 2004-11-16 12:37:40Z sacerdot $ i*) +(*i $Id: extraction.mli 10497 2008-02-01 12:18:37Z soubiran $ i*) (*s Extraction from Coq terms to Miniml. *) @@ -21,21 +21,13 @@ val extract_constant : env -> constant -> constant_body -> ml_decl val extract_constant_spec : env -> constant -> constant_body -> ml_spec +val extract_with_type : env -> constant_body -> ( identifier list * ml_type ) option + val extract_fixpoint : env -> constant array -> (constr, types) prec_declaration -> ml_decl val extract_inductive : env -> kernel_name -> ml_ind -(*s ML declaration corresponding to a Coq reference. *) - -val extract_declaration : env -> global_reference -> ml_decl - -(*s Without doing complete extraction, just guess what a constant would be. *) - -type kind = Logical | Term | Type - -val constant_kind : env -> constant_body -> kind - (*s Is a [ml_decl] or a [ml_spec] logical ? *) val logical_decl : ml_decl -> bool diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index 13b29c7b..cb95808d 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -31,19 +31,18 @@ VERNAC ARGUMENT EXTEND language | [ "Ocaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] -| [ "Toplevel" ] -> [ Toplevel ] END (* Extraction commands *) VERNAC COMMAND EXTEND Extraction (* Extraction in the Coq toplevel *) -| [ "Extraction" global(x) ] -> [ extraction x ] -| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ extraction_rec l ] +| [ "Extraction" global(x) ] -> [ simple_extraction x ] +| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ] (* Monolithic extraction to a file *) | [ "Extraction" string(f) ne_global_list(l) ] - -> [ extraction_file f l ] + -> [ full_extraction (Some f) l ] END (* Modular extraction (one Coq library = one ML module) *) diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index f924396c..0ef225c0 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 8930 2006-06-09 02:14:34Z letouzey $ i*) +(*i $Id: haskell.ml 10233 2007-10-17 23:29:08Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -18,7 +18,7 @@ open Libnames open Table open Miniml open Mlutil -open Ocaml +open Common (*s Haskell renaming issues. *) @@ -30,22 +30,19 @@ let keywords = "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] Idset.empty -let preamble prm used_modules (mldummy,tdummy,tunknown) magic = - let pp_mp = function - | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) - | _ -> assert false - in - (if not magic then mt () +let preamble mod_name used_modules usf = + let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n") + in + (if not usf.magic then mt () else str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++ str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n") ++ - str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () - ++ fnl() ++ - str "import qualified Prelude" ++ fnl() ++ - prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules - ++ fnl () ++ - (if not magic then mt () + str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++ + str "import qualified Prelude" ++ fnl () ++ + prlist pp_import used_modules ++ fnl () ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if not usf.magic then mt () else str "\ #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base @@ -54,16 +51,10 @@ unsafeCoerce = GHC.Base.unsafeCoerce# -- HUGS import qualified IOExts unsafeCoerce = IOExts.unsafeCoerce -#endif") - ++ - fnl() ++ fnl() +#endif" ++ fnl2 ()) ++ - (if not mldummy then mt () - else - str "__ = Prelude.error \"Logical or arity value used\"" - ++ fnl () ++ fnl()) - -let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" + (if not usf.mldummy then mt () + else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ()) let pp_abst = function | [] -> (mt ()) @@ -73,17 +64,11 @@ let pp_abst = function let pr_lower_id id = pr_id (lowercase_id id) -(*s The pretty-printing functor. *) +(*s The pretty-printer for haskell syntax *) -module Make = functor(P : Mlpp_param) -> struct - -let local_mpl = ref ([] : module_path list) - -let pp_global r = +let pp_global k r = if is_inline_custom r then str (find_custom r) - else P.pp_global !local_mpl r - -let empty_env () = [], P.globals() + else str (Common.pp_global k r) (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) @@ -96,13 +81,14 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) - | Tglob (r,[]) -> pp_global r + | Tglob (r,[]) -> pp_global Type r | Tglob (r,l) -> if r = IndRef (kn_sig,0) then pp_type true vl (List.hd l) else pp_par par - (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l) + (pp_global Type r ++ spc () ++ + prlist_with_sep spc (pp_type true vl) l) | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) @@ -151,20 +137,20 @@ let rec pp_expr par env args = spc () ++ str "in") ++ spc () ++ hov 0 pp_a2))) | MLglob r -> - apply (pp_global r) + apply (pp_global Term r) | MLcons (_,r,[]) -> - assert (args=[]); pp_global r + assert (args=[]); pp_global Cons r | MLcons (_,r,[a]) -> assert (args=[]); - pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a) + pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) | MLcons (_,r,args') -> assert (args=[]); - pp_par par (pp_global r ++ spc () ++ + pp_par par (pp_global Cons r ++ spc () ++ prlist_with_sep spc (pp_expr true env []) args') - | MLcase (_,t, pv) -> + | MLcase ((_,factors),t, pv) -> apply (pp_par par' (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++ - fnl () ++ str " " ++ pp_pat env pv))) + fnl () ++ str " " ++ pp_pat env factors pv))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -177,11 +163,11 @@ let rec pp_expr par env args = pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args) | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"") -and pp_pat env pv = +and pp_pat env factors pv = let pp_one_pat (name,ids,t) = let ids,env' = push_vars (List.rev ids) env in let par = expr_needs_par t in - hov 2 (pp_global name ++ + hov 2 (pp_global Cons name ++ (match ids with | [] -> mt () | _ -> (str " " ++ @@ -189,7 +175,18 @@ and pp_pat env pv = (fun () -> (spc ())) pr_id (List.rev ids))) ++ str " ->" ++ spc () ++ pp_expr par env' [] t) in - (prvect_with_sep (fun () -> (fnl () ++ str " ")) pp_one_pat pv) + prvecti + (fun i x -> if List.mem i factors then mt () else + (pp_one_pat pv.(i) ++ + if factors = [] && i = Array.length pv - 1 then mt () + else fnl () ++ str " ")) pv + ++ + match factors with + | [] -> mt () + | i::_ -> + let (_,ids,t) = pv.(i) in + let t = ast_lift (-List.length ids) t in + hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t) (*s names of the functions ([ids]) are already pushed in [env], and passed here just for convenience. *) @@ -223,7 +220,7 @@ let pp_logical_ind packet = let pp_singleton kn packet = let l = rename_tvars keywords packet.ip_vars in let l' = List.rev l in - hov 2 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++ + hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ prlist_with_sep spc pr_id l ++ (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++ pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -233,7 +230,7 @@ let pp_singleton kn packet = let pp_one_ind ip pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = - (pp_global r ++ + (pp_global Cons r ++ match l with | [] -> (mt ()) | _ -> (str " " ++ @@ -241,7 +238,7 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.length cv = 0 then "type " else "data ") ++ - pp_global (IndRef ip) ++ str " " ++ + pp_global Type (IndRef ip) ++ str " " ++ prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ (if pl = [] then mt () else str " ") ++ if Array.length cv = 0 then str "= () -- empty inductive" @@ -269,9 +266,7 @@ let rec pp_ind first kn i ind = let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") -let pp_decl mpl = - local_mpl := mpl; - function +let pp_decl = function | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton kn i.ind_packets.(0) ++ fnl () | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i) @@ -288,38 +283,51 @@ let pp_decl mpl = if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n" else str "=" ++ spc () ++ pp_type false l t in - hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl () + hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () | 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 + let e = pp_global Term rv.(i) in e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () - ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl () + ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 () ++ iter (i+1) in iter 0 | Dterm (r, a, t) -> if is_inline_custom r then mt () else - let e = pp_global r in + let e = pp_global Term r in e ++ str " :: " ++ pp_type false [] t ++ fnl () ++ if is_custom r then - hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ()) + hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) else - hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ()) + hov 0 (pp_function (empty_env ()) e a ++ fnl2 ()) -let pp_structure_elem mpl = function - | (l,SEdecl d) -> pp_decl mpl d +let pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d | (l,SEmodule m) -> failwith "TODO: Haskell extraction of modules not implemented yet" | (l,SEmodtype m) -> failwith "TODO: Haskell extraction of modules not implemented yet" let pp_struct = - prlist (fun (mp,sel) -> prlist (pp_structure_elem [mp]) sel) - -let pp_signature s = failwith "TODO" - -end - + let pp_sel (mp,sel) = + push_visible mp; + let p = prlist_strict pp_structure_elem sel in + pop_visible (); p + in + prlist_strict pp_sel + + +let haskell_descr = { + keywords = keywords; + file_suffix = ".hs"; + capital_file = true; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 106f7868..1af9c231 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -6,15 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) +(*i $Id: haskell.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) -open Pp -open Names -open Miniml +val haskell_descr : Miniml.language_descr -val keywords : Idset.t - -val preamble : - extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds - -module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 3b4146f8..dfe4eb48 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 9456 2006-12-17 20:08:38Z letouzey $ i*) +(*i $Id: miniml.mli 10497 2008-02-01 12:18:37Z soubiran $ i*) (*s Target language for extraction: a core ML called MiniML. *) @@ -58,6 +58,8 @@ type inductive_info = | Standard | Record of global_reference list +type case_info = int list (* list of branches to merge in a _ pattern *) + (* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body]. If the inductive is logical ([ip_logical = false]), then all other fields are unused. Otherwise, @@ -76,11 +78,16 @@ type ml_ind_packet = { (* [ip_nparams] contains the number of parameters. *) +type equiv = + | NoEquiv + | Equiv of kernel_name + | RenEquiv of string + type ml_ind = { ind_info : inductive_info; ind_nparams : int; ind_packets : ml_ind_packet array; - ind_equiv : kernel_name option + ind_equiv : equiv } (*s ML terms. *) @@ -92,7 +99,7 @@ type ml_ast = | MLletin of identifier * ml_ast * ml_ast | MLglob of global_reference | MLcons of inductive_info * global_reference * ml_ast list - | MLcase of inductive_info * ml_ast * + | MLcase of (inductive_info*case_info) * ml_ast * (global_reference * identifier list * ml_ast) array | MLfix of int * identifier array * ml_ast array | MLexn of string @@ -119,9 +126,14 @@ type ml_specif = | Smodtype of ml_module_type and ml_module_type = - | MTident of kernel_name + | MTident of module_path | MTfunsig of mod_bound_id * ml_module_type * ml_module_type | MTsig of mod_self_id * ml_module_sig + | MTwith of ml_module_type * ml_with_declaration + +and ml_with_declaration = + | ML_With_type of identifier list * identifier list * ml_type + | ML_With_module of identifier list * module_path and ml_module_sig = (label * ml_specif) list @@ -149,24 +161,28 @@ type ml_structure = (module_path * ml_module_structure) list type ml_signature = (module_path * ml_module_sig) list -(*s Pretty-printing of MiniML in a given concrete syntax is parameterized - by a function [pp_global] that pretty-prints global references. - The resulting pretty-printer is a module of type [Mlpp] providing - functions to print types, terms and declarations. *) - -module type Mlpp_param = sig - val globals : unit -> Idset.t - val pp_global : module_path list -> global_reference -> std_ppcmds - val pp_module : module_path list -> module_path -> std_ppcmds -end - -module type Mlpp = sig - val pp_decl : module_path list -> ml_decl -> std_ppcmds - val pp_struct : ml_structure -> std_ppcmds - val pp_signature : ml_signature -> std_ppcmds -end - -type extraction_params = - { modular : bool; - mod_name : identifier; - to_appear : global_reference list } +type unsafe_needs = { + mldummy : bool; + tdummy : bool; + tunknown : bool; + magic : bool +} + +type language_descr = { + keywords : Idset.t; + + (* Concerning the source file *) + file_suffix : string; + capital_file : bool; (* should we capitalize filenames ? *) + preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + pp_struct : ml_structure -> std_ppcmds; + + (* Concerning a possible interface file *) + sig_suffix : string option; + sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + pp_sig : ml_signature -> std_ppcmds; + + (* for an isolated declaration print *) + pp_decl : ml_decl -> std_ppcmds; + +} diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 6bfedce5..79aeea33 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 8886 2006-06-01 13:53:45Z letouzey $ i*) +(*i $Id: mlutil.ml 10329 2007-11-21 21:21:36Z letouzey $ i*) (*i*) open Pp @@ -573,14 +573,20 @@ let eta_red e = if n = 0 then e else match t with | MLapp (f,a) -> - let m = (List.length a) - n in - if m < 0 then e - else - let a1,a2 = list_chop m a in - let f = if m = 0 then f else MLapp (f,a1) in - if test_eta_args_lift 0 n a2 && not (ast_occurs_itvl 1 n f) - then ast_lift (-n) f - else e + let m = List.length a in + let ids,body,args = + if m = n then + [], f, a + else if m < n then + snd (list_chop (n-m) ids), f, a + else (* m > n *) + let a1,a2 = list_chop (m-n) a in + [], MLapp (f,a1), a2 + in + let p = List.length args in + if test_eta_args_lift 0 p args && not (ast_occurs_itvl 1 p body) + then named_lams ids (ast_lift (-p) body) + else e | _ -> e (*s Computes all head linear beta-reductions possible in [(t a)]. @@ -658,20 +664,27 @@ let check_generalizable_case unsafe br = if check_and_generalize br.(i) <> f then raise Impossible done; f -(*s Do all branches correspond to the same thing? *) +(*s Detecting similar branches of a match *) -let check_constant_case br = - 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; - let cst = ast_lift (-n) t in - for i = 1 to Array.length br - 1 do - let (r,l,t) = br.(i) in - let n = List.length l in - if (ast_occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) - then raise Impossible - done; cst +(* If several branches of a match are equal (and independent from their + patterns) we will print them using a _ pattern. If _all_ branches + are equal, we remove the match. +*) + +let common_branches br = + let tab = Hashtbl.create 13 in + for i = 0 to Array.length br - 1 do + let (r,ids,t) = br.(i) in + let n = List.length ids in + if not (ast_occurs_itvl 1 n t) then + let t = ast_lift (-n) t in + let l = try Hashtbl.find tab t with Not_found -> [] in + Hashtbl.replace tab t (i::l) + done; + let best = ref [] in + Hashtbl.iter + (fun _ l -> if List.length l > List.length !best then best := l) tab; + if List.length !best < 2 then [] else !best (*s If all branches are functions, try to permut the case and the functions. *) @@ -805,18 +818,20 @@ and simpl_case o i br e = let f = check_generalizable_case o.opt_case_idg br in simpl o (MLapp (MLlam (anonymous,f),[e])) with Impossible -> - try (* Is each branch independant of [e] ? *) - if not o.opt_case_cst then raise Impossible; - check_constant_case br - with Impossible -> + (* Detect common branches *) + let common_br = if not o.opt_case_cst then [] else common_branches br in + if List.length common_br = Array.length br && br <> [||] then + let (_,ids,t) = br.(0) in ast_lift (-List.length ids) t + else + let new_i = (fst i, common_br) in (* Swap the case and the lam if possible *) if o.opt_case_fun then let ids,br = permut_case_fun br [] in let n = List.length ids in - if n <> 0 then named_lams ids (MLcase (i,ast_lift n e, br)) - else MLcase (i,e,br) - else MLcase (i,e,br) + if n <> 0 then named_lams ids (MLcase (new_i,ast_lift n e, br)) + else MLcase (new_i,e,br) + else MLcase (new_i,e,br) let rec post_simpl = function | MLletin(_,c,e) when (is_atomic (eta_red c)) -> @@ -1122,13 +1137,15 @@ let is_not_strict t = Futhermore we don't expand fixpoints. *) let inline_test t = - not (is_fix (eta_red t)) && (ml_size t < 12 && is_not_strict t) + let t1 = eta_red t in + let t2 = snd (collect_lams t1) in + not (is_fix t2) && ml_size t < 12 && is_not_strict t let manual_inline_list = let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in 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" ] + "Acc_rect"; "Acc_rec" ; "Acc_iter" ; "Fix" ] let manual_inline = function | ConstRef c -> List.mem c manual_inline_list diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index c9d4e237..48444509 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 9456 2006-12-17 20:08:38Z letouzey $ i*) +(*i $Id: modutil.ml 10665 2008-03-14 12:10:09Z soubiran $ i*) open Names open Declarations @@ -20,121 +20,34 @@ open Mod_subst (*S Functions upon modules missing in [Modops]. *) -(*s Add _all_ direct subobjects of a module, not only those exported. - Build on the [Modops.add_signature] model. *) - -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 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 - in List.fold_left add_one env msb - -(*s Apply a module path substitution on a module. - Build on the [Modops.subst_modtype] model. *) - -let rec subst_module sub mb = - let mtb' = Modops.subst_modtype sub mb.mod_type - and meb' = option_smartmap (subst_meb sub) mb.mod_expr - and mtb'' = option_smartmap (Modops.subst_modtype sub) mb.mod_user_type - and mpo' = option_smartmap (subst_mp sub) mb.mod_equiv in - if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) && - (mtb''==mb.mod_user_type) && (mpo'==mb.mod_equiv) - then mb - else { mod_expr= meb'; - mod_type=mtb'; - mod_user_type=mtb''; - mod_equiv=mpo'; - mod_constraints=mb.mod_constraints } - -and subst_meb sub = function - | MEBident mp -> MEBident (subst_mp sub mp) - | MEBfunctor (mbid, mtb, meb) -> - assert (not (occur_mbid mbid sub)); - MEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb) - | MEBstruct (msid, msb) -> - assert (not (occur_msid msid sub)); - MEBstruct (msid, subst_msb sub msb) - | MEBapply (meb, meb', c) -> - MEBapply (subst_meb sub meb, subst_meb sub meb', c) - -and subst_msb sub msb = - let subst_body = function - | SEBconst cb -> SEBconst (subst_const_body sub cb) - | SEBmind mib -> SEBmind (subst_mind sub mib) - | SEBmodule mb -> SEBmodule (subst_module sub mb) - | SEBmodtype mtb -> SEBmodtype (Modops.subst_modtype sub mtb) - in List.map (fun (l,b) -> (l,subst_body b)) msb - (*s Change a msid in a module type, to follow a module expr. Because of the "with" construct, the module type of a module can be a [MTBsig] with a msid different from the one of the module. *) let rec replicate_msid meb mtb = match meb,mtb with - | MEBfunctor (_, _, meb), MTBfunsig (mbid, mtb1, mtb2) -> + | SEBfunctor (_, _, meb), SEBfunctor (mbid, mtb1, mtb2) -> let mtb' = replicate_msid meb mtb2 in - if mtb' == mtb2 then mtb else MTBfunsig (mbid, mtb1, mtb') - | MEBstruct (msid, _), MTBsig (msid1, msig) when msid <> msid1 -> + if mtb' == mtb2 then mtb else SEBfunctor (mbid, mtb1, mtb') + | SEBstruct (msid, _), SEBstruct (msid1, msig) when msid <> msid1 -> let msig' = Modops.subst_signature_msid msid1 (MPself msid) msig in - if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig') + if msig' == msig then SEBstruct (msid, msig) else SEBstruct (msid, msig') | _ -> mtb - -(*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 - -let rec common_prefix prefixes_mp1 mp2 = - if MPset.mem mp2 prefixes_mp1 then mp2 - else match mp2 with - | MPdot (mp,_) -> common_prefix prefixes_mp1 mp - | _ -> raise Not_found - -let common_prefix_from_list mp0 mpl = - let prefixes_mp0 = prefixes_mp mp0 in - let rec f = function - | [] -> raise Not_found - | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l - in f mpl - -let rec modfile_of_mp mp = match mp with - | MPfile _ -> mp - | MPdot (mp,_) -> modfile_of_mp mp - | _ -> raise Not_found - -let rec parse_labels ll = function - | MPdot (mp,l) -> parse_labels (l::ll) mp - | mp -> mp,ll - -let labels_of_mp mp = parse_labels [] mp - -let 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 - | l :: ll -> add_labels_mp (MPdot (mp,l)) ll - - (*S Functions upon ML modules. *) - +let rec msid_of_mt = function + | MTident mp -> begin + match Modops.eval_struct (Global.env()) (SEBident mp) with + | SEBstruct(msid,_) -> MPself msid + | _ -> anomaly "Extraction:the With can't be applied to a funsig" + end + | MTwith(mt,_)-> msid_of_mt mt + | _ -> anomaly "Extraction:the With operator isn't applied to a name" + +let make_mp_with mp idl = + let idl_rev = List.rev idl in + let idl' = List.rev (List.tl idl_rev) in + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp idl') (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a [ml_structure]. *) @@ -142,6 +55,16 @@ let struct_iter do_decl do_spec s = let rec mt_iter = function | MTident _ -> () | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' + | MTwith (mt,ML_With_type(idl,l,t))-> + let mp_mt = msid_of_mt mt in + let mp = make_mp_with mp_mt idl in + let gr = ConstRef ( + (make_con mp empty_dirpath + (label_of_id ( + List.hd (List.rev idl))))) in + mt_iter mt;do_decl + (Dtype(gr,l,t)) + | MTwith (mt,_)->mt_iter mt | MTsig (_, sign) -> List.iter spec_iter sign and spec_iter = function | (_,Spec s) -> do_spec s @@ -186,7 +109,7 @@ let ast_iter_references do_term do_cons do_type a = if lang () = Ocaml then record_iter_references do_term i; do_cons r | MLcase (i,_,v) -> - if lang () = Ocaml then record_iter_references do_term i; + if lang () = Ocaml then record_iter_references do_term (fst i); Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () in iter a @@ -197,7 +120,9 @@ let ind_iter_references do_term do_cons do_type kn ind = let packet_iter ip p = do_type (IndRef ip); if lang () = Ocaml then - option_iter (fun kne -> do_type (IndRef (kne,snd ip))) ind.ind_equiv; + (match ind.ind_equiv with + | Equiv kne -> do_type (IndRef (kne, snd ip)); + | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in if lang () = Ocaml then record_iter_references do_term ind.ind_info; @@ -215,7 +140,7 @@ let decl_iter_references do_term do_cons do_type = let spec_iter_references do_term do_cons do_type = function | Sind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind - | Stype (r,_,ot) -> do_type r; option_iter (type_iter_references do_type) ot + | Stype (r,_,ot) -> do_type r; Option.iter (type_iter_references do_type) ot | Sval (r,t) -> do_term r; type_iter_references do_type t let struct_iter_references do_term do_cons do_type = @@ -225,13 +150,13 @@ let struct_iter_references do_term do_cons do_type = (*s Get all references used in one [ml_structure], either in [list] or [set]. *) -type 'a updown = { mutable up : 'a ; mutable down : 'a } +type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a } let struct_get_references empty add struc = - let o = { up = empty ; down = empty } in - let do_term r = o.down <- add r o.down in - let do_cons r = o.up <- add r o.up in - let do_type = if lang () = Haskell then do_cons else do_term in + let o = { typ = empty ; trm = empty ; cons = empty } in + let do_type r = o.typ <- add r o.typ in + let do_term r = o.trm <- add r o.trm in + let do_cons r = o.cons <- add r o.cons in struct_iter_references do_term do_cons do_type struc; o let struct_get_references_set = struct_get_references Refset.empty Refset.add @@ -248,7 +173,9 @@ end let struct_get_references_list struc = let o = struct_get_references Orefset.empty Orefset.add struc in - { up = Orefset.list o.up; down = Orefset.list o.down } + { typ = Orefset.list o.typ; + trm = Orefset.list o.trm; + cons = Orefset.list o.cons } (*s Searching occurrences of a particular term (no lifting done). *) @@ -284,7 +211,7 @@ let spec_type_search f = function | Sind (_,{ind_packets=p}) -> Array.iter (fun {ip_types=v} -> Array.iter (List.iter (type_search f)) v) p - | Stype (_,_,ot) -> option_iter (type_search f) ot + | Stype (_,_,ot) -> Option.iter (type_search f) ot | Sval (_,u) -> type_search f u let struct_type_search f s = @@ -360,38 +287,40 @@ let dfix_to_mlfix rv av i = let c = Array.map (subst 0) av in MLfix(i, ids, c) -let rec optim prm s = function +let rec optim to_appear s = function | [] -> [] | (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 + if List.mem r to_appear + then d :: (optim to_appear s l) + else optim to_appear s l | Dterm (r,t,typ) :: l -> let t = normalize (ast_glob_subst !s t) in let i = inline r t in if i then s := Refmap.add r t !s; - if not i || prm.modular || List.mem r prm.to_appear + if not i || modular () || List.mem r to_appear then let d = match optimize_fix t with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|]) | t -> Dterm (r, t, typ) - in d :: (optim prm s l) - else optim prm s l - | d :: l -> d :: (optim prm s l) + in d :: (optim to_appear s l) + else optim to_appear s l + | d :: l -> d :: (optim to_appear s l) -let rec optim_se top prm s = function +let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap.add r a !s; - if top && i && not prm.modular && not (List.mem r prm.to_appear) - then optim_se top prm s lse + if top && i && not (modular ()) && not (List.mem r to_appear) + then optim_se top to_appear s lse else let d = match optimize_fix a with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) | a -> Dterm (r, a, t) - in (l,SEdecl d) :: (optim_se top prm s lse) + in (l,SEdecl d) :: (optim_se top to_appear s lse) | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in let all = ref true in @@ -402,22 +331,22 @@ let rec optim_se top prm s = function then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; - if !all && top && not prm.modular - && (array_for_all (fun r -> not (List.mem r prm.to_appear)) rv) - then optim_se top prm s lse - else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse) + if !all && top && not (modular ()) + && (array_for_all (fun r -> not (List.mem r to_appear)) rv) + then optim_se top to_appear s lse + else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> - let m = { m with ml_mod_expr = optim_me prm s m.ml_mod_expr} - in (l,SEmodule m) :: (optim_se top prm s lse) - | se :: lse -> se :: (optim_se top prm s lse) + let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} + in (l,SEmodule m) :: (optim_se top to_appear s lse) + | se :: lse -> se :: (optim_se top to_appear s lse) -and optim_me prm s = function - | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm s lse) +and optim_me to_appear s = function + | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse) | MEident mp as me -> me - | MEapply (me, me') -> MEapply (optim_me prm s me, optim_me prm s me') - | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me) + | MEapply (me, me') -> + MEapply (optim_me to_appear s me, optim_me to_appear s me') + | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) -let optimize_struct prm before struc = +let optimize_struct to_appear struc = 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 + List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index 115a42ca..85d58a4b 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.mli 8724 2006-04-20 09:57:01Z letouzey $ i*) +(*i $Id: modutil.mli 10620 2008-03-05 10:54:41Z letouzey $ i*) open Names open Declarations @@ -17,29 +17,9 @@ open Mod_subst (*s Functions upon modules missing in [Modops]. *) -(* Add _all_ direct subobjects of a module, not only those exported. - Build on the [Modops.add_signature] model. *) - -val add_structure : module_path -> module_structure_body -> env -> env - -(* Apply a module path substitution on a module. - Build on the [Modops.subst_modtype] model. *) - -val subst_module : substitution -> module_body -> module_body -val subst_meb : substitution -> module_expr_body -> module_expr_body -val subst_msb : substitution -> module_structure_body -> module_structure_body - (* Change a msid in a module type, to follow a module expr. *) -val replicate_msid : module_expr_body -> module_type_body -> module_type_body - -(*s More utilities concerning [module_path]. *) - -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 add_labels_mp : module_path -> label list -> module_path +val replicate_msid : struct_expr_body -> struct_expr_body -> struct_expr_body (*s Functions upon ML modules. *) @@ -52,10 +32,10 @@ val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit val struct_iter_references : do_ref -> do_ref -> do_ref -> ml_structure -> unit -type 'a updown = { mutable up : 'a ; mutable down : 'a } +type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a } -val struct_get_references_set : ml_structure -> Refset.t updown -val struct_get_references_list : ml_structure -> global_reference list updown +val struct_get_references_set : ml_structure -> Refset.t kinds +val struct_get_references_list : ml_structure -> global_reference list kinds val signature_of_structure : ml_structure -> ml_signature @@ -65,7 +45,7 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl all beta redexes (when the argument does not occur, it is just thrown away; when it occurs exactly once it is substituted; otherwise a let-in redex is created for clarity) and iota redexes, plus some other - optimizations. *) + optimizations. The first argument is the list of objects we want to appear. +*) -val optimize_struct : - extraction_params -> ml_decl list option -> ml_structure -> ml_structure +val optimize_struct : global_reference list -> ml_structure -> ml_structure diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 35f9a83c..64c80a2a 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 9472 2007-01-05 15:49:32Z letouzey $ i*) +(*i $Id: ocaml.ml 10592 2008-02-27 14:16:07Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -19,10 +19,27 @@ open Table open Miniml open Mlutil open Modutil +open Common +open Declarations + (*s Some utility functions. *) -let pp_par par st = if par then str "(" ++ st ++ str ")" else st +let rec msid_of_mt = function + | MTident mp -> begin + match Modops.eval_struct (Global.env()) (SEBident mp) with + | SEBstruct(msid,_) -> MPself msid + | _ -> anomaly "Extraction:the With can't be applied to a funsig" + end + | MTwith(mt,_)-> msid_of_mt mt + | _ -> anomaly "Extraction:the With operator isn't applied to a name" + +let make_mp_with mp idl = + let idl_rev = List.rev idl in + let idl' = List.rev (List.tl idl_rev) in + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp idl') + let pp_tvar id = let s = string_of_id id in @@ -52,70 +69,12 @@ let pp_abst = function str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ str " ->" ++ spc () -let pp_apply st par args = match args with - | [] -> st - | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) - -let pr_binding = function - | [] -> mt () - | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l - -let space_if = function true -> str " " | false -> mt () - -let sec_space_if = function true -> spc () | false -> mt () - -let fnl2 () = fnl () ++ fnl () - let pp_parameters l = (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) let pp_string_parameters l = (pp_boxed_tuple str l ++ space_if (l<>[])) -(*s Generic renaming issues. *) - -let rec rename_id id avoid = - if Idset.mem id avoid then rename_id (lift_ident id) avoid else id - -let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) -let uppercase_id id = id_of_string (String.capitalize (string_of_id id)) - -(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *) -let pr_upper_id id = str (String.capitalize (string_of_id id)) - -(*s de Bruijn environments for programs *) - -type env = identifier list * Idset.t - -let rec rename_vars avoid = function - | [] -> - [], avoid - | id :: idl when id == dummy_name -> - (* we don't rename dummy binders *) - let (idl', avoid') = rename_vars avoid idl in - (id :: idl', avoid') - | id :: idl -> - let (idl, avoid) = rename_vars avoid idl in - let id = rename_id (lowercase_id id) avoid in - (id :: idl, Idset.add id avoid) - -let rename_tvars avoid l = - let rec rename avoid = function - | [] -> [],avoid - | id :: idl -> - let id = rename_id (lowercase_id id) avoid in - let idl, avoid = rename (Idset.add id avoid) idl in - (id :: idl, avoid) in - fst (rename avoid l) - -let push_vars ids (db,avoid) = - let ids',avoid' = rename_vars avoid ids in - ids', (ids' @ db, avoid') - -let get_db_name n (db,_) = - let id = List.nth db (pred n) in - if id = dummy_name then id_of_string "__" else id - (*s Ocaml renaming issues. *) let keywords = @@ -130,46 +89,39 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules (mldummy,tdummy,tunknown) _ = - let pp_mp = function - | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) - | _ -> assert false - in - prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules - ++ - (if used_modules = [] then mt () else fnl ()) - ++ - (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) - ++ - (if mldummy then - str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl () - else mt ()) - ++ - (if tdummy || tunknown || mldummy then fnl () else mt ()) - -let preamble_sig _ used_modules (_,tdummy,tunknown) = - let pp_mp = function - | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) - | _ -> assert false - in - prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules - ++ - (if used_modules = [] then mt () else fnl ()) - ++ - (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () - else mt()) +let pp_open mp = str ("open "^ string_of_modfile mp ^"\n") -(*s The pretty-printing functor. *) +let preamble _ used_modules usf = + prlist pp_open used_modules ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++ + (if usf.mldummy then + str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n" + else mt ()) ++ + (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ()) -module Make = functor(P : Mlpp_param) -> struct +let sig_preamble _ used_modules usf = + prlist pp_open used_modules ++ + (if used_modules = [] then mt () else fnl ()) ++ + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt()) -let local_mpl = ref ([] : module_path list) +(*s The pretty-printer for Ocaml syntax*) -let pp_global r = +let pp_global k r = if is_inline_custom r then str (find_custom r) - else P.pp_global !local_mpl r + else str (Common.pp_global k r) + +let pp_modname mp = str (Common.pp_module mp) -let empty_env () = [], P.globals () +let is_infix r = + is_inline_custom r && + (let s = find_custom r in + let l = String.length s in + l >= 2 && s.[0] = '(' && s.[l-1] = ')') + +let get_infix r = + let s = find_custom r in + String.sub s 1 (String.length s - 2) exception NoRecord @@ -187,12 +139,16 @@ let rec pp_type par vl t = | Tmeta _ | Tvar' _ | Taxiom -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i)) - | Tglob (r,[]) -> pp_global r + | Tglob (r,[a1;a2]) when is_infix r -> + pp_par par + (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++ + pp_rec true a2) + | Tglob (r,[]) -> pp_global Type r | Tglob (r,l) -> if r = IndRef (kn_sig,0) then pp_tuple_light pp_rec l else - pp_tuple_light pp_rec l ++ spc () ++ pp_global r + pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) @@ -206,10 +162,16 @@ let rec pp_type par vl t = de Bruijn variables. [args] is the list of collected arguments (already pretty-printed). *) +let is_ifthenelse = function + | [|(r1,[],_);(r2,[],_)|] -> + (try (find_custom r1 = "true") && (find_custom r2 = "false") + with Not_found -> false) + | _ -> false + let expr_needs_par = function | MLlam _ -> true | MLcase (_,_,[|_|]) -> false - | MLcase _ -> true + | MLcase (_,_,pv) -> not (is_ifthenelse pv) | _ -> false @@ -244,26 +206,31 @@ let rec pp_expr par env args = (try let args = list_skipn (projection_arity r) args in let record = List.hd args in - pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) - with _ -> apply (pp_global r)) + pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) + with _ -> apply (pp_global Term r)) | MLcons (Coinductive,r,[]) -> assert (args=[]); - pp_par par (str "lazy " ++ pp_global r) + pp_par par (str "lazy " ++ pp_global Cons r) | MLcons (Coinductive,r,args') -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") + pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") | MLcons (_,r,[]) -> assert (args=[]); - pp_global r + pp_global Cons r | MLcons (Record projs, r, args') -> assert (args=[]); pp_record_pat (projs, List.map (pp_expr true env []) args') + | MLcons (_,r,[arg1;arg2]) when is_infix r -> + assert (args=[]); + pp_par par + ((pp_expr true env [] arg1) ++ spc () ++ str (get_infix r) ++ + spc () ++ (pp_expr true env [] arg2)) | MLcons (_,r,args') -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (pp_global r ++ spc () ++ tuple) - | MLcase (i, t, pv) -> + pp_par par (pp_global Cons r ++ spc () ++ tuple) + | MLcase ((i,factors), t, pv) -> let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else @@ -276,7 +243,7 @@ let rec pp_expr par env args = match c with | MLrel i when i <= n -> apply (pp_par par' (pp_expr true env [] t ++ str "." ++ - pp_global (List.nth projs (n-i)))) + pp_global Term (List.nth projs (n-i)))) | MLapp (MLrel i, a) when i <= n -> if List.exists (ast_occurs_itvl 1 n) a then raise NoRecord @@ -284,7 +251,7 @@ let rec pp_expr par env args = let ids,env' = push_vars (List.rev ids) env in (pp_apply (pp_expr true env [] t ++ str "." ++ - pp_global (List.nth projs (n-i))) + pp_global Term (List.nth projs (n-i))) par ((List.map (pp_expr true env' []) a) @ args)) | _ -> raise NoRecord with NoRecord -> @@ -297,11 +264,13 @@ let rec pp_expr par env args = (hov 2 (str "let " ++ s1 ++ str " =" ++ spc () ++ expr) ++ spc () ++ str "in") ++ spc () ++ hov 0 s2))) - else - apply + else + apply (pp_par par' - (v 0 (str "match " ++ expr ++ str " with" ++ - fnl () ++ str " | " ++ pp_pat env i pv)))) + (try pp_ifthenelse par' env expr pv + with Not_found -> + v 0 (str "match " ++ expr ++ str " with" ++ fnl () ++ + str " | " ++ pp_pat env (i,factors) pv)))) | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in pp_fix par env' i (Array.of_list (List.rev ids'),defs) args @@ -319,10 +288,21 @@ let rec pp_expr par env args = and pp_record_pat (projs, args) = str "{ " ++ prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a) + (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a) (List.combine projs args) ++ str " }" +and pp_ifthenelse par env expr pv = match pv with + | [|(tru,[],the);(fal,[],els)|] when + (find_custom tru = "true") && (find_custom fal = "false") + -> + hv 0 (hov 2 (str "if " ++ expr) ++ spc () ++ + hov 2 (str "then " ++ + hov 2 (pp_expr (expr_needs_par the) env [] the)) ++ spc () ++ + hov 2 (str "else " ++ + hov 2 (pp_expr (expr_needs_par els) env [] els))) + | _ -> raise Not_found + and pp_one_pat env i (r,ids,t) = let ids,env' = push_vars (List.rev ids) env in let expr = pp_expr (expr_needs_par t) env' [] t in @@ -330,33 +310,45 @@ and pp_one_pat env i (r,ids,t) = let projs = find_projections i in pp_record_pat (projs, List.rev_map pr_id ids), expr with NoRecord -> - let args = - if ids = [] then (mt ()) - else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in - pp_global r ++ args, expr + (match List.rev ids with + | [i1;i2] when is_infix r -> + pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2 + | [] -> pp_global Cons r + | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), + expr -and pp_pat env i pv = - prvect_with_sep (fun () -> (fnl () ++ str " | ")) - (fun x -> let s1,s2 = pp_one_pat env i x in - hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv - -and pp_function env f t = +and pp_pat env (info,factors) pv = + prvecti + (fun i x -> if List.mem i factors then mt () else + let s1,s2 = pp_one_pat env info x in + hov 2 (s1 ++ str " ->" ++ spc () ++ s2) ++ + (if factors = [] && i = Array.length pv-1 then mt () + else fnl () ++ str " | ")) pv + ++ + match factors with + | [] -> mt () + | i::_ -> + let (_,ids,t) = pv.(i) in + let t = ast_lift (-List.length ids) t in + hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t) + +and pp_function env t = let bl,t' = collect_lams t in let bl,env' = push_vars bl env in match t' with - | MLcase(i,MLrel 1,pv) when i=Standard -> + | MLcase(i,MLrel 1,pv) when fst 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)) + pr_binding (List.rev (List.tl bl)) ++ + str " = function" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) else - (f ++ pr_binding (List.rev bl) ++ - 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')) + pr_binding (List.rev bl) ++ + str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) + | _ -> + pr_binding (List.rev bl) ++ + str " =" ++ fnl () ++ str " " ++ + hov 2 (pp_expr false env' [] t') (*s names of the functions ([ids]) are already pushed in [env], and passed here just for convenience. *) @@ -366,93 +358,111 @@ and pp_fix par env i (ids,bl) args = (v 0 (str "let rec " ++ prvect_with_sep (fun () -> fnl () ++ str "and ") - (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (fun (fi,ti) -> pr_id fi ++ pp_function env ti) (array_map2 (fun id b -> (id,b)) ids bl) ++ fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) let pp_val e typ = - str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ - str " **)" ++ fnl2 () + hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ + str " **)") ++ fnl2 () (*s Pretty-printing of [Dfix] *) -let rec pp_Dfix init i ((rv,c,t) as fix) = - if i >= Array.length rv then mt () - else - if is_inline_custom rv.(i) then pp_Dfix init (i+1) fix +let pp_Dfix (rv,c,t) = + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + let rec pp sep letand i = + if i >= Array.length rv then mt () + else if is_inline_custom rv.(i) then pp sep letand (i+1) else - let e = pp_global rv.(i) in - (if init then mt () else fnl2 ()) ++ - pp_val e t.(i) ++ - str (if init then "let rec " else "and ") ++ - (if is_custom rv.(i) then e ++ str " = " ++ str (find_custom rv.(i)) - else pp_function (empty_env ()) e c.(i)) ++ - pp_Dfix false (i+1) fix - + let def = + if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) + else pp_function (empty_env ()) c.(i) + in + sep () ++ pp_val names.(i) t.(i) ++ + str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) + in pp mt "let rec " 0 + (*s Pretty-printing of inductive types declaration. *) -let pp_equiv param_list = function - | None -> mt () - | Some ip_equiv -> - str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv) +let pp_equiv param_list name = function + | NoEquiv, _ -> mt () + | Equiv kn, i -> + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i)) + | RenEquiv ren, _ -> + str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name let pp_comment s = str "(* " ++ s ++ str " *)" -let pp_one_ind prefix ip ip_equiv pl cv = +let pp_one_ind prefix ip_equiv pl name cnames ctyps = let pl = rename_tvars keywords pl in - let pp_constructor (r,l) = - hov 2 (str " | " ++ pp_global r ++ - match l with - | [] -> mt () - | _ -> (str " of " ++ - prlist_with_sep - (fun () -> spc () ++ str "* ") (pp_type true pl) l)) + let pp_constructor i typs = + (if i=0 then mt () else fnl ()) ++ + hov 5 (str " | " ++ cnames.(i) ++ + (if typs = [] then mt () else str " of ") ++ + prlist_with_sep + (fun () -> spc () ++ str "* ") (pp_type true pl) typs) in - 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)) + pp_parameters pl ++ str prefix ++ name ++ + pp_equiv pl name ip_equiv ++ str " =" ++ + if Array.length ctyps = 0 then str " unit (* empty inductive *)" + else fnl () ++ v 0 (prvecti pp_constructor ctyps) let pp_logical_ind packet = pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ - fnl () ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc pr_id packet.ip_consnames) + fnl () ++ + pp_comment (str "with constructors : " ++ + prvect_with_sep spc pr_id packet.ip_consnames) ++ + fnl () let pp_singleton kn packet = + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in - hov 2 (str "type " ++ pp_parameters l ++ - pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++ + hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) let pp_record kn projs ip_equiv packet = - let l = List.combine projs packet.ip_types.(0) in + let name = pp_global Type (IndRef (kn,0)) in + let projnames = List.map (pp_global Term) projs in + let l = List.combine projnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in - str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ - pp_equiv pl ip_equiv ++ str " = { "++ + str "type " ++ pp_parameters pl ++ name ++ + pp_equiv pl name ip_equiv ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) + (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) ++ str " }" -let pp_coind ip pl = - let r = IndRef ip in +let pp_coind pl name = 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 ++ name ++ str " = " ++ + pp_parameters pl ++ str "__" ++ name ++ 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 names = + Array.mapi (fun i p -> if p.ip_logical then mt () else + pp_global Type (IndRef (kn,i))) + ind.ind_packets + in + let cnames = + Array.mapi + (fun i p -> if p.ip_logical then [||] else + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) + p.ip_types) + ind.ind_packets + 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 ip_equiv = ind.ind_equiv, 0 in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) else begin @@ -463,8 +473,9 @@ let pp_ind co kn ind = begin init := (fnl () ++ str "and "); s ++ - (if co then pp_coind ip p.ip_vars else mt ()) - ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++ + (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ + pp_one_ind + prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ pp (i+1) end end @@ -479,159 +490,248 @@ let pp_mind kn i = | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i | 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) + pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0) | Standard -> pp_ind false kn i -let pp_decl mpl = - local_mpl := mpl; - function +let pp_decl = function + | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase" | 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 l = rename_tvars keywords l in - let ids, def = try + | Dtype (r, l, t) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids, def = + try let ids,s = find_type_custom r in pp_string_parameters ids, str "=" ++ spc () ++ str s - with not_found -> + with Not_found -> pp_parameters l, if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" else str "=" ++ spc () ++ pp_type false l t - in - hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++ - spc () ++ def) + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) | Dterm (r, a, t) -> - if is_inline_custom r then failwith "empty phrase" - else - let e = pp_global r in - pp_val e t ++ - hov 0 - (str "let " ++ - if is_custom r then - e ++ str " = " ++ str (find_custom r) - else if is_projection r then - let s = prvecti (fun _ -> str) - (Array.make (projection_arity r) " _") in - e ++ s ++ str " x = x." ++ e - else pp_function (empty_env ()) e a) + let def = + if is_custom r then str (" = " ^ find_custom r) + else if is_projection r then + (prvect str (Array.make (projection_arity r) " _")) ++ + str " x = x." + else pp_function (empty_env ()) a + in + let name = pp_global Term r in + let postdef = if is_projection r then name else mt () in + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) | Dfix (rv,defs,typs) -> - pp_Dfix true 0 (rv,defs,typs) - -let pp_spec mpl = - local_mpl := mpl; - function - | Sind (kn,i) -> pp_mind kn i - | Sval (r,t) -> - if is_inline_custom r then failwith "empty phrase" - else - hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++ - pp_type false [] t) - | Stype (r,vl,ot) -> - if is_inline_custom r then failwith "empty phrase" - else - let l = rename_tvars keywords vl in - let ids, def = - try - let ids, s = find_type_custom r in - pp_string_parameters ids, str "= " ++ str s - with not_found -> - let ids = pp_parameters l in - match ot with - | None -> ids, mt () - | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" - | Some t -> ids, str "=" ++ spc () ++ pp_type false l t - in - hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def) - -let rec pp_specif mpl = function - | (_,Spec s) -> pp_spec mpl s + pp_Dfix (rv,defs,typs) + +let pp_alias_decl ren = function + | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Dtype (r, l, _) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Dterm (r, a, t) -> + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) + | Dfix (rv, _, _) -> + prvecti (fun i r -> if is_inline_custom r then mt () else + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ + fnl ()) + rv + +let pp_spec = function + | Sval (r,_) when is_inline_custom r -> failwith "empty phrase" + | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Sind (kn,i) -> pp_mind kn i + | Sval (r,t) -> + let def = pp_type false [] t in + let name = pp_global Term r in + hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def) + | Stype (r,vl,ot) -> + let name = pp_global Type r in + let l = rename_tvars keywords vl in + let ids, def = + try + let ids, s = find_type_custom r in + pp_string_parameters ids, str "= " ++ str s + with Not_found -> + let ids = pp_parameters l in + match ot with + | None -> ids, mt () + | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" + | Some t -> ids, str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + +let pp_alias_spec ren = function + | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Stype (r,l,_) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Sval _ -> assert false + +let rec pp_specif = function + | (_,Spec (Sval _ as s)) -> pp_spec s + | (l,Spec s) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_spec ren s + with Not_found -> pp_spec s) | (l,Smodule mt) -> - hov 1 - (str "module " ++ - P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt) + let def = pp_module_type (Some l) mt in + let def' = pp_module_type (Some l) mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') + with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> - hov 1 - (str "module type " ++ - P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " = " ++ fnl () ++ pp_module_type mpl None mt) - -and pp_module_type mpl ol = function + let def = pp_module_type None mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> Pp.mt ()) + +and pp_module_type ol = function | MTident kn -> - let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l)) + pp_modname kn | MTfunsig (mbid, mt, mt') -> - str "functor (" ++ - P.pp_module mpl (MPbound mbid) ++ - str ":" ++ - pp_module_type mpl None mt ++ - str ") ->" ++ fnl () ++ - pp_module_type mpl None mt' + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type None mt in + let def = pp_module_type None mt' in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (msid, sign) -> - let mpl = match ol, mpl with - | None, _ -> (MPself msid) :: mpl - | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl - | _ -> assert false - in - let l = map_succeed (pp_specif mpl) sign in + let tvm = top_visible_mp () in + Option.iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; + let mp = MPself msid in + push_visible mp; + let l = map_succeed pp_specif sign in + pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ - fnl () ++ str "end" - + fnl () ++ str "end" + | MTwith(mt,ML_With_type(idl,vl,typ)) -> + let l = rename_tvars keywords vl in + let ids = pp_parameters l in + let mp_mt = msid_of_mt mt in + let mp = make_mp_with mp_mt idl in + let gr = ConstRef ( + (make_con mp empty_dirpath + (label_of_id ( + List.hd (List.rev idl))))) in + push_visible mp_mt; + let s = pp_module_type None mt ++ + str " with type " ++ + pp_global Type gr ++ + ids in + pop_visible(); + s ++ str "=" ++ spc () ++ + pp_type false vl typ + | MTwith(mt,ML_With_module(idl,mp)) -> + let mp_mt=msid_of_mt mt in + push_visible mp_mt; + let s = + pp_module_type None mt ++ + str " with module " ++ + (pp_modname + (List.fold_left (fun mp id -> MPdot(mp,label_of_id id)) + mp_mt idl)) + ++ str " = " + in + pop_visible (); + s ++ (pp_modname mp) + + let is_short = function MEident _ | MEapply _ -> true | _ -> false - -let rec pp_structure_elem mpl = function - | (_,SEdecl d) -> pp_decl mpl d + +let rec pp_structure_elem = function + | (l,SEdecl d) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_decl ren d + with Not_found -> pp_decl d) | (l,SEmodule m) -> + let def = pp_module_expr (Some l) m.ml_mod_expr in + let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 - (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - (*i if you want signatures everywhere: i*) - (*i str " :" ++ fnl () ++ i*) - (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*) - str " = " ++ - (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ - pp_module_expr mpl (Some l) m.ml_mod_expr) + (str "module " ++ name ++ str " = " ++ + (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module "^ren^" = ") ++ name + with Not_found -> mt ()) | (l,SEmodtype m) -> - hov 1 - (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_module mpl mp' + let def = pp_module_type None m in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> mt ()) + +and pp_module_expr ol = function + | MEident mp' -> pp_modname mp' | MEfunctor (mbid, mt, me) -> - str "functor (" ++ - P.pp_module mpl (MPbound mbid) ++ - str ":" ++ - pp_module_type mpl None mt ++ - str ") ->" ++ fnl () ++ - pp_module_expr mpl None me + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type None mt in + let def = pp_module_expr None me in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEapply (me, me') -> - pp_module_expr mpl None me ++ str "(" ++ - pp_module_expr mpl None me' ++ str ")" + pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")" | MEstruct (msid, sel) -> - let mpl = match ol, mpl with - | None, _ -> (MPself msid) :: mpl - | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl - | _ -> assert false - in - let l = map_succeed (pp_structure_elem mpl) sel in + let tvm = top_visible_mp () in + let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in + push_visible mp; + let l = map_succeed pp_structure_elem sel in + pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ fnl () ++ str "end" let pp_struct s = - let pp mp s = pp_structure_elem [mp] s ++ fnl2 () in - prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s + let pp mp s = + push_visible mp; + let p = pp_structure_elem s ++ fnl2 () in + pop_visible (); p + in + prlist_strict + (fun (mp,sel) -> prlist_strict identity (map_succeed (pp mp) sel)) s let pp_signature s = - let pp mp s = pp_specif [mp] s ++ fnl2 () in - prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s - -let pp_decl mpl d = - try pp_decl mpl d with Failure "empty phrase" -> mt () - -end - + let pp mp s = + push_visible mp; + let p = pp_specif s ++ fnl2 () in + pop_visible (); p + in + prlist_strict + (fun (mp,sign) -> prlist_strict identity (map_succeed (pp mp) sign)) s + +let pp_decl d = + try pp_decl d with Failure "empty phrase" -> mt () + +let ocaml_descr = { + keywords = keywords; + file_suffix = ".ml"; + capital_file = false; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = Some ".mli"; + sig_preamble = sig_preamble; + pp_sig = pp_signature; + pp_decl = pp_decl; +} diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 8c521ccd..3d90e74c 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -6,49 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) - -(*s Some utility functions to be reused in module [Haskell]. *) - -open Pp -open Names -open Libnames -open Miniml - -val pp_par : bool -> std_ppcmds -> std_ppcmds -val pp_abst : identifier list -> std_ppcmds -val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds -val pr_binding : identifier list -> std_ppcmds - -val rename_id : identifier -> Idset.t -> identifier - -val lowercase_id : identifier -> identifier -val uppercase_id : identifier -> identifier - -val pr_upper_id : identifier -> std_ppcmds - -type env = identifier list * Idset.t - -val rename_vars: Idset.t -> identifier list -> env -val rename_tvars: Idset.t -> identifier list -> identifier list -val push_vars : identifier list -> env -> identifier list * env -val get_db_name : int -> env -> identifier - -val keywords : Idset.t - -val preamble : - extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds - -val preamble_sig : - extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds - -(*s Production of Ocaml syntax. We export both a functor to be used for - extraction in the Coq toplevel and a function to extract some - declarations to a file. *) - -module Make : functor(P : Mlpp_param) -> Mlpp - - - +(*i $Id: ocaml.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) +val ocaml_descr : Miniml.language_descr diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 7004a202..600f64db 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 7651 2005-12-16 03:19:20Z letouzey $ i*) +(*i $Id: scheme.ml 10233 2007-10-17 23:29:08Z letouzey $ i*) (*s Production of Scheme syntax. *) @@ -18,7 +18,7 @@ open Libnames open Miniml open Mlutil open Table -open Ocaml +open Common (*s Scheme renaming issues. *) @@ -29,17 +29,11 @@ let keywords = "error"; "delay"; "force"; "_"; "__"] Idset.empty -let preamble _ _ (mldummy,_,_) _ = - str ";; This extracted scheme code relies on some additional macros" ++ - fnl () ++ - str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++ - fnl () ++ - str "(load \"macros_extr.scm\")" ++ - fnl () ++ fnl () ++ - (if mldummy then - str "(define __ (lambda (_) __))" - ++ fnl () ++ fnl() - else mt ()) +let preamble _ _ usf = + str ";; This extracted scheme code relies on some additional macros\n" ++ + str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++ + str "(load \"macros_extr.scm\")\n\n" ++ + (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ()) let pr_id id = let s = string_of_id id in @@ -60,14 +54,11 @@ let pp_apply st _ = function | [] -> st | [a] -> hov 2 (paren (st ++ spc () ++ a)) | args -> hov 2 (paren (str "@ " ++ st ++ - (prlist (fun x -> spc () ++ x) args))) + (prlist_strict (fun x -> spc () ++ x) args))) -(*s The pretty-printing functor. *) +(*s The pretty-printer for Scheme syntax *) -module Make = functor(P : Mlpp_param) -> struct - -let pp_global r = P.pp_global [initial_path] r -let empty_env () = [], P.globals() +let pp_global k r = str (Common.pp_global k r) (*s Pretty-printing of expressions. *) @@ -95,17 +86,17 @@ let rec pp_expr env args = (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> - apply (pp_global r) + apply (pp_global Term r) | MLcons (i,r,args') -> assert (args=[]); let st = str "`" ++ - paren (pp_global r ++ + paren (pp_global Cons r ++ (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in if i = Coinductive then paren (str "delay " ++ st) else st - | MLcase (i,t, pv) -> + | MLcase ((i,_),t, pv) -> let e = if i <> Coinductive then pp_expr env [] t else paren (str "force" ++ spc () ++ pp_expr env [] t) @@ -125,7 +116,7 @@ let rec pp_expr env args = and pp_cons_args env = function | MLcons (i,r,args) when i<>Coinductive -> - paren (pp_global r ++ + paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) | e -> str "," ++ pp_expr env [] e @@ -137,7 +128,7 @@ and pp_one_pat env (r,ids,t) = if ids = [] then mt () else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) in - (pp_global r ++ args), (pp_expr env' [] t) + (pp_global Cons r ++ args), (pp_expr env' [] t) and pp_pat env pv = prvect_with_sep fnl @@ -160,11 +151,11 @@ and pp_fix env j (ids,bl) args = (*s Pretty-printing of a declaration. *) -let pp_decl _ = function +let pp_decl = function | Dind _ -> mt () | Dtype _ -> mt () | Dfix (rv, defs,_) -> - let ppv = Array.map pp_global rv in + let ppv = Array.map (pp_global Term) rv in prvect_with_sep fnl (fun (pi,ti) -> hov 2 @@ -177,23 +168,35 @@ let pp_decl _ = function if is_inline_custom r then mt () else if is_custom r then - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ str (find_custom r))) ++ fnl () ++ fnl () else - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () -let pp_structure_elem mp = function - | (l,SEdecl d) -> pp_decl mp d +let pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d | (l,SEmodule m) -> failwith "TODO: Scheme extraction of modules not implemented yet" | (l,SEmodtype m) -> failwith "TODO: Scheme extraction of modules not implemented yet" let pp_struct = - prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel) - -let pp_signature s = assert false - -end - + let pp_sel (mp,sel) = + push_visible mp; + let p = prlist_strict pp_structure_elem sel in + pop_visible (); p + in + prlist_strict pp_sel + +let scheme_descr = { + keywords = keywords; + file_suffix = ".scm"; + capital_file = false; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index ef4a3a63..a88bb6db 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -6,22 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) - -(*s Some utility functions to be reused in module [Haskell]. *) - -open Pp -open Miniml -open Names - -val keywords : Idset.t - -val preamble : - extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds - -module Make : functor(P : Mlpp_param) -> Mlpp - - - - +(*i $Id: scheme.mli 10232 2007-10-17 12:32:10Z letouzey $ i*) +val scheme_descr : Miniml.language_descr diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 6d39faee..abf461c1 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 10209 2007-10-09 21:49:37Z letouzey $ i*) +(*i $Id: table.ml 10348 2007-12-06 17:36:14Z aspiwack $ i*) open Names open Term @@ -20,37 +20,49 @@ open Util open Pp open Miniml -(*S Utilities concerning [module_path] and [kernel_names] *) +(*S Utilities about [module_path] and [kernel_names] and [global_reference] *) -let occur_kn_in_ref kn = - function +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 ()) + +let modpath_of_r = function + | ConstRef kn -> con_modpath kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> modpath kn + | VarRef _ -> assert false + +let label_of_r = function + | ConstRef kn -> con_label kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> label kn + | VarRef _ -> assert false let rec base_mp = function | MPdot (mp,l) -> base_mp mp | mp -> mp +let rec mp_length = function + | MPdot (mp, _) -> 1 + (mp_length mp) + | _ -> 1 + let is_modfile = function | MPfile _ -> true | _ -> false +let string_of_modfile = function + | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) + | _ -> assert false + +let rec modfile_of_mp = function + | (MPfile _) as mp -> mp + | MPdot (mp,_) -> modfile_of_mp mp + | _ -> raise Not_found + +let current_toplevel () = fst (Lib.current_prefix ()) + let is_toplevel mp = mp = initial_path || mp = current_toplevel () @@ -60,8 +72,56 @@ let at_toplevel mp = let visible_kn kn = at_toplevel (base_mp (modpath kn)) let visible_con kn = at_toplevel (base_mp (con_modpath kn)) +let rec prefixes_mp mp = match mp with + | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') + | _ -> MPset.singleton mp + +let rec get_nth_label_mp n mp = match mp with + | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp + | _ -> failwith "get_nth_label: not enough MPdot" + +let get_nth_label n r = + if n=0 then label_of_r r else get_nth_label_mp n (modpath_of_r r) + +let rec common_prefix prefixes_mp1 mp2 = + if MPset.mem mp2 prefixes_mp1 then mp2 + else match mp2 with + | MPdot (mp,_) -> common_prefix prefixes_mp1 mp + | _ -> raise Not_found + +let common_prefix_from_list mp0 mpl = + let prefixes_mp0 = prefixes_mp mp0 in + let rec f = function + | [] -> raise Not_found + | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l + in f mpl + +let rec parse_labels ll = function + | MPdot (mp,l) -> parse_labels (l::ll) mp + | mp -> mp,ll + +let labels_of_mp mp = parse_labels [] mp + +let 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 + | l :: ll -> add_labels_mp (MPdot (mp,l)) ll + + (*S The main tables: constants, inductives, records, ... *) +(* Theses tables are not registered within coq save/undo mechanism + since we reset their contents at each run of Extraction *) + (*s Constants tables. *) let terms = ref (Cmap.empty : ml_decl Cmap.t) @@ -109,11 +169,26 @@ let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs let is_projection r = Refmap.mem r !projs let projection_arity r = Refmap.find r !projs +(*s Table of used axioms *) + +let info_axioms = ref Refset.empty +let log_axioms = ref Refset.empty +let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty +let add_info_axiom r = info_axioms := Refset.add r !info_axioms +let add_log_axiom r = log_axioms := Refset.add r !log_axioms + +(*s Extraction mode: modular or monolithic *) + +let modular_ref = ref false + +let set_modular b = modular_ref := b +let modular () = !modular_ref + (*s Tables synchronization. *) let reset_tables () = init_terms (); init_types (); init_inductives (); init_recursors (); - init_projs () + init_projs (); init_axioms () (*s Printing. *) @@ -146,21 +221,34 @@ let pr_long_global r = let err s = errorlabstrm "Extraction" s +let warning_axioms () = + let info_axioms = Refset.elements !info_axioms in + if info_axioms = [] then () + else begin + let s = if List.length info_axioms = 1 then "axiom" else "axioms" in + msg_warning + (str ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms) + ++ str "." ++ fnl ()) + end; + let log_axioms = Refset.elements !log_axioms in + if log_axioms = [] then () + else begin + let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" + in + msg_warning + (str ("The following logical "^s^" encountered:") ++ + hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++ + str "Having invalid logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ + fnl ()) + end + let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ str " type variable(s).") -let warning_info_ax r = - msg_warning (str "You must realize axiom " ++ - pr_global r ++ str " in the extracted code.") - -let warning_log_ax r = - 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 () = if Lib.is_modtype () then err (str "You can't do that within a Module Type." ++ fnl () ++ @@ -186,15 +274,11 @@ let error_nb_cons () = let error_module_clash s = err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ - str "This is not allowed in ML. Please do some renaming first.") + str "This is not supported yet. Please do some renaming first.") let error_unknown_module m = err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") -let error_toplevel () = - err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++ - str "You should use Extraction Language Ocaml or Haskell before.") - let error_scheme () = err (str "No Scheme modular extraction available yet.") @@ -203,9 +287,13 @@ let error_not_visible r = str "For example, it may be inside an applied functor." ++ str "Use Recursive Extraction to get the whole environment.") -let error_MPfile_as_mod d = - err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^ - "Extraction cannot currently deal with this situation.\n")) +let error_MPfile_as_mod mp b = + let s1 = if b then "asked" else "required" in + let s2 = if b then "extract some objects of this module or\n" else "" in + err (str ("Extraction of file "^(string_of_modfile mp)^ + ".v as a module is "^s1^".\n"^ + "Monolithic Extraction cannot deal with this situation.\n"^ + "Please "^s2^"use (Recursive) Extraction Library instead.\n")) let error_record r = err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++ @@ -216,8 +304,16 @@ let check_loaded_modfile mp = match base_mp mp with err (str ("Please load library "^(string_of_dirpath dp^" first."))) | _ -> () +let info_file f = + Flags.if_verbose message + ("The file "^f^" has been created by extraction.") + + (*S The Extraction auxiliary commands *) +(* The objects defined below should survive an arbitrary time, + so we register them to coq save/undo mechanism. *) + (*s Extraction AutoInline *) let auto_inline_ref = ref true @@ -305,7 +401,7 @@ let _ = declare_int_option (*s Extraction Lang *) -type lang = Ocaml | Haskell | Scheme | Toplevel +type lang = Ocaml | Haskell | Scheme let lang_ref = ref Ocaml @@ -327,7 +423,6 @@ let _ = declare_summary "Extraction Lang" let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) - (*s Extraction Inline/NoInline *) let empty_inline_table = (Refset.empty,Refset.empty) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index c9a4e8da..ca02cb4d 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 10209 2007-10-09 21:49:37Z letouzey $ i*) +(*i $Id: table.mli 10245 2007-10-21 13:41:53Z letouzey $ i*) open Names open Libnames @@ -14,39 +14,49 @@ open Miniml open Declarations val id_of_global : global_reference -> identifier +val pr_long_global : global_reference -> Pp.std_ppcmds + (*s Warning and Error messages. *) +val warning_axioms : unit -> unit val error_axiom_scheme : global_reference -> int -> 'a -val warning_info_ax : global_reference -> unit -val warning_log_ax : global_reference -> unit val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : string -> 'a val error_unknown_module : qualid -> 'a -val error_toplevel : unit -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_MPfile_as_mod : dir_path -> 'a +val error_MPfile_as_mod : module_path -> bool -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -(*s utilities concerning [module_path]. *) +val info_file : string -> unit + +(*s utilities about [module_path] and [kernel_names] and [global_reference] *) 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 -val is_modfile : module_path -> bool +val is_modfile : module_path -> bool +val string_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool val visible_con : constant -> bool +val mp_length : module_path -> int +val prefixes_mp : module_path -> MPset.t +val modfile_of_mp : module_path -> module_path +val common_prefix_from_list : module_path -> module_path list -> module_path +val add_labels_mp : module_path -> label list -> module_path +val get_nth_label_mp : int -> module_path -> label +val get_nth_label : int -> global_reference -> label +val labels_of_ref : global_reference -> module_path * label list (*s Some table-related operations *) @@ -66,6 +76,9 @@ val add_projection : int -> constant -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int +val add_info_axiom : global_reference -> unit +val add_log_axiom : global_reference -> unit + val reset_tables : unit -> unit (*s AutoInline parameter *) @@ -95,9 +108,14 @@ val optims : unit -> opt_flag (*s Target language. *) -type lang = Ocaml | Haskell | Scheme | Toplevel +type lang = Ocaml | Haskell | Scheme val lang : unit -> lang +(*s Extraction mode: modular or monolithic *) + +val set_modular : bool -> unit +val modular : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend deleted file mode 100644 index 31d46eeb..00000000 --- a/contrib/extraction/test/.depend +++ /dev/null @@ -1,1136 +0,0 @@ -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/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/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/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/Init/specif.cmx \ - theories/Init/datatypes.cmx theories/Arith/compare_dec.cmx \ - theories/Arith/compare.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/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/specif.cmi theories/Init/datatypes.cmi \ - theories/Arith/even.cmi -theories/Arith/even.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ - theories/Arith/even.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/specif.cmi theories/Init/datatypes.cmi \ - theories/Arith/max.cmi -theories/Arith/max.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ - theories/Arith/max.cmi -theories/Arith/min.cmo: theories/Init/specif.cmi theories/Init/datatypes.cmi \ - theories/Arith/min.cmi -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/Arith/plus.cmi theories/Init/datatypes.cmi \ - theories/Arith/mult.cmi -theories/Arith/mult.cmx: theories/Arith/plus.cmx theories/Init/datatypes.cmx \ - theories/Arith/mult.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/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/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/specif.cmx theories/Init/datatypes.cmx \ - theories/Bool/bool.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/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/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 -theories/Init/peano.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmi -theories/Init/prelude.cmo: theories/Init/prelude.cmi -theories/Init/prelude.cmx: theories/Init/prelude.cmi -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/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/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/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/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/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/specif.cmi theories/Init/datatypes.cmi \ - theories/Lists/list.cmi -theories/Lists/list.cmx: theories/Init/specif.cmx theories/Init/datatypes.cmx \ - theories/Lists/list.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/specif.cmi \ - theories/Lists/list.cmi theories/Init/datatypes.cmi \ - theories/Lists/theoryList.cmi -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/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/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 -theories/Logic/classical.cmx: theories/Logic/classical.cmi -theories/Logic/classical_Pred_Set.cmo: theories/Logic/classical_Pred_Set.cmi -theories/Logic/classical_Pred_Set.cmx: theories/Logic/classical_Pred_Set.cmi -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/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/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/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/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: \ - theories/Relations/operators_Properties.cmi -theories/Relations/operators_Properties.cmx: \ - theories/Relations/operators_Properties.cmi -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/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/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 -theories/Sets/constructive_sets.cmx: theories/Sets/constructive_sets.cmi -theories/Sets/cpo.cmo: theories/Sets/partial_Order.cmi theories/Sets/cpo.cmi -theories/Sets/cpo.cmx: theories/Sets/partial_Order.cmx theories/Sets/cpo.cmi -theories/Sets/ensembles.cmo: theories/Sets/ensembles.cmi -theories/Sets/ensembles.cmx: theories/Sets/ensembles.cmi -theories/Sets/finite_sets_facts.cmo: theories/Sets/finite_sets_facts.cmi -theories/Sets/finite_sets_facts.cmx: theories/Sets/finite_sets_facts.cmi -theories/Sets/finite_sets.cmo: theories/Sets/finite_sets.cmi -theories/Sets/finite_sets.cmx: theories/Sets/finite_sets.cmi -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/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: \ - theories/Sets/powerset_Classical_facts.cmi -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/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 -theories/Sets/relations_1.cmx: theories/Sets/relations_1.cmi -theories/Sets/relations_2_facts.cmo: theories/Sets/relations_2_facts.cmi -theories/Sets/relations_2_facts.cmx: theories/Sets/relations_2_facts.cmi -theories/Sets/relations_2.cmo: theories/Sets/relations_2.cmi -theories/Sets/relations_2.cmx: theories/Sets/relations_2.cmi -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/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/specif.cmx \ - theories/Init/peano.cmx theories/Sets/multiset.cmx \ - theories/Lists/list.cmx theories/Init/datatypes.cmx \ - theories/Sorting/permutation.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: \ - theories/Wellfounded/disjoint_Union.cmi -theories/Wellfounded/inclusion.cmo: theories/Wellfounded/inclusion.cmi -theories/Wellfounded/inclusion.cmx: theories/Wellfounded/inclusion.cmi -theories/Wellfounded/inverse_Image.cmo: \ - theories/Wellfounded/inverse_Image.cmi -theories/Wellfounded/inverse_Image.cmx: \ - theories/Wellfounded/inverse_Image.cmi -theories/Wellfounded/lexicographic_Exponentiation.cmo: \ - theories/Wellfounded/lexicographic_Exponentiation.cmi -theories/Wellfounded/lexicographic_Exponentiation.cmx: \ - theories/Wellfounded/lexicographic_Exponentiation.cmi -theories/Wellfounded/lexicographic_Product.cmo: \ - theories/Wellfounded/lexicographic_Product.cmi -theories/Wellfounded/lexicographic_Product.cmx: \ - theories/Wellfounded/lexicographic_Product.cmi -theories/Wellfounded/transitive_Closure.cmo: \ - theories/Wellfounded/transitive_Closure.cmi -theories/Wellfounded/transitive_Closure.cmx: \ - theories/Wellfounded/transitive_Closure.cmi -theories/Wellfounded/union.cmo: theories/Wellfounded/union.cmi -theories/Wellfounded/union.cmx: theories/Wellfounded/union.cmi -theories/Wellfounded/wellfounded.cmo: theories/Wellfounded/wellfounded.cmi -theories/Wellfounded/wellfounded.cmx: theories/Wellfounded/wellfounded.cmi -theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmi \ - theories/Wellfounded/well_Ordering.cmi -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/Init/datatypes.cmi \ - theories/NArith/binPos.cmi theories/NArith/binNat.cmi \ - theories/ZArith/binInt.cmi -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/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/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/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/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/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/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/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/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/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/Init/specif.cmx \ - theories/Init/datatypes.cmx theories/ZArith/binInt.cmx \ - theories/ZArith/zorder.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/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/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/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/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/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/specif.cmi \ - theories/Lists/list.cmi theories/Init/datatypes.cmi -theories/Logic/choiceFacts.cmi: theories/Init/specif.cmi \ - theories/Init/datatypes.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/Sets/partial_Order.cmi \ - theories/Init/datatypes.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 deleted file mode 100644 index 65a54090..00000000 --- a/contrib/extraction/test/Makefile +++ /dev/null @@ -1,109 +0,0 @@ -# -# General variables -# - -TOPDIR=../../.. - -# Files with axioms to be realized: can't be extracted directly - -AXIOMSVO:= \ -theories/Reals/% \ -theories/Num/% - -DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -path \*.svn\*)) - -INCL:= $(patsubst %,-I %,$(DIRS)) - -VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo)) - -VO:= $(filter-out $(AXIOMSVO),$(VO)) - -ML:= $(shell test -x v2ml && ./v2ml $(VO)) - -MLI:= $(patsubst %.ml,%.mli,$(ML)) - -CMO:= $(patsubst %.ml,%.cmo,$(ML)) - -OSTDLIB:=$(shell (ocamlc -where)) - -# -# General rules -# - -all: v2ml ml $(MLI) $(CMO) - -ml: $(ML) - -depend: #$(ML) - rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend - -tree: - mkdir -p $(DIRS) - cp $(OSTDLIB)/pervasives.cmi $(OSTDLIB)/obj.cmi $(OSTDLIB)/lazy.cmi theories - -#%.mli:%.ml -# ./make_mli $< > $@ - -%.cmi:%.mli - ocamlc -c $(INCL) -nostdlib $< - -%.cmo:%.ml - ocamlc -c $(INCL) -nostdlib $< - -$(ML): ml2v - ./extract $@ - -clean: - rm -f theories/*/*.ml* theories/*/*.cm* - - -# -# Utilities -# - -open: - find theories -name "*".ml -exec ./qualify2open \{\} \; - -undo_open: - find theories -name "*".ml -exec mv \{\}.orig \{\} \; - -ml2v: ml2v.ml - ocamlopt -o $@ $< - -v2ml: v2ml.ml - ocamlopt -o $@ $< - $(MAKE) - -# -# Extraction of Reals -# - - -REALSAXIOMSVO:=theories/Reals/Rsyntax.vo - -REALSALLVO:=$(shell cd $(TOPDIR); ls -tr theories/Reals/*.vo) -REALSVO:=$(filter-out $(REALSAXIOMSVO),$(REALSALLVO)) -REALSML:=$(shell test -x v2ml && ./v2ml $(REALSVO)) -REALSCMO:= $(patsubst %.ml,%.cmo,$(REALSML)) - -reals: all realsml theories/Reals/addReals.cmo $(REALSCMO) - -realsml: $(REALSML) - -theories/Reals/addReals.ml: - cp -f addReals theories/Reals/addReals.ml - -$(REALSML): - ./extract $@ - - -# -# The End -# - -.PHONY: all tree clean reals realsml depend - -include .depend - - - diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell deleted file mode 100644 index 6e1e15d1..00000000 --- a/contrib/extraction/test/Makefile.haskell +++ /dev/null @@ -1,416 +0,0 @@ -# -# General variables -# - -TOPDIR=../../.. - -# Files with axioms to be realized: can't be extracted directly - -AXIOMSVO:= \ -theories/Init/Prelude.vo \ -theories/Reals/% \ -theories/Num/% - -DIRS:= $(shell (cd $(TOPDIR);find theories -type d ! -name CVS)) - -INCL:= $(patsubst %,-i%,$(DIRS)) - -VO:= $(shell (cd $(TOPDIR);find theories -name \*.vo)) - -VO:= $(filter-out $(AXIOMSVO),$(VO)) - -HS:= $(shell test -x v2hs && ./v2hs $(VO)) - -O:= $(patsubst %.hs,%.o,$(HS)) - -# -# General rules -# - -all: v2hs hs $(O) - -hs: $(HS) - -tree: - mkdir -p $(DIRS) - -%.o:%.hs - ghc $(INCL) -c $< - -$(HS): hs2v - ./extract.haskell $@ - -clean: - rm -f theories/*/*.h* theories/*/*.o - - -# -# Utilities -# - -hs2v: hs2v.ml - ocamlc -o $@ $< - -v2hs: v2hs.ml - ocamlc -o $@ $< - $(MAKE) -f Makefile.haskell - - -# -# The End -# - -.PHONY: all tree clean depend - -# DO NOT DELETE: Beginning of Haskell dependencies -theories/Arith/Between.o : theories/Arith/Between.hs -theories/Arith/Bool_nat.o : theories/Arith/Bool_nat.hs -theories/Arith/Bool_nat.o : theories/Bool/Sumbool.o -theories/Arith/Bool_nat.o : theories/Init/Specif.o -theories/Arith/Bool_nat.o : theories/Arith/Peano_dec.o -theories/Arith/Bool_nat.o : theories/Init/Datatypes.o -theories/Arith/Bool_nat.o : theories/Arith/Compare_dec.o -theories/Arith/Compare_dec.o : theories/Arith/Compare_dec.hs -theories/Arith/Compare_dec.o : theories/Init/Specif.o -theories/Arith/Compare_dec.o : theories/Init/Logic.o -theories/Arith/Compare_dec.o : theories/Init/Datatypes.o -theories/Arith/Compare.o : theories/Arith/Compare.hs -theories/Arith/Compare.o : theories/Init/Specif.o -theories/Arith/Compare.o : theories/Init/Datatypes.o -theories/Arith/Compare.o : theories/Arith/Compare_dec.o -theories/Arith/Div2.o : theories/Arith/Div2.hs -theories/Arith/Div2.o : theories/Init/Specif.o -theories/Arith/Div2.o : theories/Init/Peano.o -theories/Arith/Div2.o : theories/Init/Datatypes.o -theories/Arith/EqNat.o : theories/Arith/EqNat.hs -theories/Arith/EqNat.o : theories/Init/Specif.o -theories/Arith/EqNat.o : theories/Init/Datatypes.o -theories/Arith/Euclid.o : theories/Arith/Euclid.hs -theories/Arith/Euclid.o : theories/Arith/Wf_nat.o -theories/Arith/Euclid.o : theories/Init/Specif.o -theories/Arith/Euclid.o : theories/Arith/Minus.o -theories/Arith/Euclid.o : theories/Init/Datatypes.o -theories/Arith/Euclid.o : theories/Arith/Compare_dec.o -theories/Arith/Even.o : theories/Arith/Even.hs -theories/Arith/Even.o : theories/Init/Specif.o -theories/Arith/Even.o : theories/Init/Datatypes.o -theories/Arith/Gt.o : theories/Arith/Gt.hs -theories/Arith/Le.o : theories/Arith/Le.hs -theories/Arith/Lt.o : theories/Arith/Lt.hs -theories/Arith/Max.o : theories/Arith/Max.hs -theories/Arith/Max.o : theories/Init/Specif.o -theories/Arith/Max.o : theories/Init/Logic.o -theories/Arith/Max.o : theories/Init/Datatypes.o -theories/Arith/Min.o : theories/Arith/Min.hs -theories/Arith/Min.o : theories/Init/Specif.o -theories/Arith/Min.o : theories/Init/Logic.o -theories/Arith/Min.o : theories/Init/Datatypes.o -theories/Arith/Minus.o : theories/Arith/Minus.hs -theories/Arith/Minus.o : theories/Init/Datatypes.o -theories/Arith/Mult.o : theories/Arith/Mult.hs -theories/Arith/Mult.o : theories/Arith/Plus.o -theories/Arith/Mult.o : theories/Init/Datatypes.o -theories/Arith/Peano_dec.o : theories/Arith/Peano_dec.hs -theories/Arith/Peano_dec.o : theories/Init/Specif.o -theories/Arith/Peano_dec.o : theories/Init/Datatypes.o -theories/Arith/Plus.o : theories/Arith/Plus.hs -theories/Arith/Plus.o : theories/Init/Specif.o -theories/Arith/Plus.o : theories/Init/Logic.o -theories/Arith/Plus.o : theories/Init/Datatypes.o -theories/Arith/Wf_nat.o : theories/Arith/Wf_nat.hs -theories/Arith/Wf_nat.o : theories/Init/Wf.o -theories/Arith/Wf_nat.o : theories/Init/Logic.o -theories/Arith/Wf_nat.o : theories/Init/Datatypes.o -theories/Bool/BoolEq.o : theories/Bool/BoolEq.hs -theories/Bool/BoolEq.o : theories/Init/Specif.o -theories/Bool/BoolEq.o : theories/Init/Datatypes.o -theories/Bool/Bool.o : theories/Bool/Bool.hs -theories/Bool/Bool.o : theories/Init/Specif.o -theories/Bool/Bool.o : theories/Init/Datatypes.o -theories/Bool/DecBool.o : theories/Bool/DecBool.hs -theories/Bool/DecBool.o : theories/Init/Specif.o -theories/Bool/IfProp.o : theories/Bool/IfProp.hs -theories/Bool/IfProp.o : theories/Init/Specif.o -theories/Bool/IfProp.o : theories/Init/Datatypes.o -theories/Bool/Sumbool.o : theories/Bool/Sumbool.hs -theories/Bool/Sumbool.o : theories/Init/Specif.o -theories/Bool/Sumbool.o : theories/Init/Datatypes.o -theories/Bool/Zerob.o : theories/Bool/Zerob.hs -theories/Bool/Zerob.o : theories/Init/Datatypes.o -theories/Init/Datatypes.o : theories/Init/Datatypes.hs -theories/Init/DatatypesSyntax.o : theories/Init/DatatypesSyntax.hs -theories/Init/Logic.o : theories/Init/Logic.hs -theories/Init/LogicSyntax.o : theories/Init/LogicSyntax.hs -theories/Init/Logic_Type.o : theories/Init/Logic_Type.hs -theories/Init/Logic_TypeSyntax.o : theories/Init/Logic_TypeSyntax.hs -theories/Init/Peano.o : theories/Init/Peano.hs -theories/Init/Peano.o : theories/Init/Datatypes.o -theories/Init/Specif.o : theories/Init/Specif.hs -theories/Init/Specif.o : theories/Init/Logic.o -theories/Init/Specif.o : theories/Init/Datatypes.o -theories/Init/SpecifSyntax.o : theories/Init/SpecifSyntax.hs -theories/Init/Wf.o : theories/Init/Wf.hs -theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs -theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.o -theories/IntMap/Adalloc.o : theories/Bool/Sumbool.o -theories/IntMap/Adalloc.o : theories/Init/Specif.o -theories/IntMap/Adalloc.o : theories/IntMap/Map.o -theories/IntMap/Adalloc.o : theories/Init/Logic.o -theories/IntMap/Adalloc.o : theories/Init/Datatypes.o -theories/IntMap/Adalloc.o : theories/IntMap/Addr.o -theories/IntMap/Adalloc.o : theories/IntMap/Addec.o -theories/IntMap/Addec.o : theories/IntMap/Addec.hs -theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o -theories/IntMap/Addec.o : theories/Bool/Sumbool.o -theories/IntMap/Addec.o : theories/Init/Specif.o -theories/IntMap/Addec.o : theories/Init/Datatypes.o -theories/IntMap/Addec.o : theories/IntMap/Addr.o -theories/IntMap/Addr.o : theories/IntMap/Addr.hs -theories/IntMap/Addr.o : theories/ZArith/Fast_integer.o -theories/IntMap/Addr.o : theories/Init/Specif.o -theories/IntMap/Addr.o : theories/Init/Datatypes.o -theories/IntMap/Addr.o : theories/Bool/Bool.o -theories/IntMap/Adist.o : theories/IntMap/Adist.hs -theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o -theories/IntMap/Adist.o : theories/Arith/Min.o -theories/IntMap/Adist.o : theories/Init/Datatypes.o -theories/IntMap/Adist.o : theories/IntMap/Addr.o -theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs -theories/IntMap/Fset.o : theories/IntMap/Fset.hs -theories/IntMap/Fset.o : theories/Init/Specif.o -theories/IntMap/Fset.o : theories/IntMap/Map.o -theories/IntMap/Fset.o : theories/Init/Logic.o -theories/IntMap/Fset.o : theories/Init/Datatypes.o -theories/IntMap/Fset.o : theories/IntMap/Addr.o -theories/IntMap/Fset.o : theories/IntMap/Addec.o -theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs -theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o -theories/IntMap/Lsort.o : theories/Bool/Sumbool.o -theories/IntMap/Lsort.o : theories/Init/Specif.o -theories/IntMap/Lsort.o : theories/Lists/PolyList.o -theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o -theories/IntMap/Lsort.o : theories/IntMap/Map.o -theories/IntMap/Lsort.o : theories/Init/Logic.o -theories/IntMap/Lsort.o : theories/Init/Datatypes.o -theories/IntMap/Lsort.o : theories/Bool/Bool.o -theories/IntMap/Lsort.o : theories/IntMap/Addr.o -theories/IntMap/Lsort.o : theories/IntMap/Addec.o -theories/IntMap/Mapaxioms.o : theories/IntMap/Mapaxioms.hs -theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs -theories/IntMap/Mapcanon.o : theories/Init/Specif.o -theories/IntMap/Mapcanon.o : theories/IntMap/Map.o -theories/IntMap/Mapcard.o : theories/IntMap/Mapcard.hs -theories/IntMap/Mapcard.o : theories/Bool/Sumbool.o -theories/IntMap/Mapcard.o : theories/Init/Specif.o -theories/IntMap/Mapcard.o : theories/Arith/Plus.o -theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o -theories/IntMap/Mapcard.o : theories/Init/Peano.o -theories/IntMap/Mapcard.o : theories/IntMap/Map.o -theories/IntMap/Mapcard.o : theories/Init/Logic.o -theories/IntMap/Mapcard.o : theories/Init/Datatypes.o -theories/IntMap/Mapcard.o : theories/IntMap/Addr.o -theories/IntMap/Mapcard.o : theories/IntMap/Addec.o -theories/IntMap/Mapc.o : theories/IntMap/Mapc.hs -theories/IntMap/Mapfold.o : theories/IntMap/Mapfold.hs -theories/IntMap/Mapfold.o : theories/Init/Specif.o -theories/IntMap/Mapfold.o : theories/IntMap/Mapiter.o -theories/IntMap/Mapfold.o : theories/IntMap/Map.o -theories/IntMap/Mapfold.o : theories/Init/Logic.o -theories/IntMap/Mapfold.o : theories/IntMap/Fset.o -theories/IntMap/Mapfold.o : theories/Init/Datatypes.o -theories/IntMap/Mapfold.o : theories/IntMap/Addr.o -theories/IntMap/Map.o : theories/IntMap/Map.hs -theories/IntMap/Map.o : theories/ZArith/Fast_integer.o -theories/IntMap/Map.o : theories/Init/Specif.o -theories/IntMap/Map.o : theories/Init/Peano.o -theories/IntMap/Map.o : theories/Init/Datatypes.o -theories/IntMap/Map.o : theories/IntMap/Addr.o -theories/IntMap/Map.o : theories/IntMap/Addec.o -theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs -theories/IntMap/Mapiter.o : theories/Bool/Sumbool.o -theories/IntMap/Mapiter.o : theories/Init/Specif.o -theories/IntMap/Mapiter.o : theories/Lists/PolyList.o -theories/IntMap/Mapiter.o : theories/IntMap/Map.o -theories/IntMap/Mapiter.o : theories/Init/Logic.o -theories/IntMap/Mapiter.o : theories/Init/Datatypes.o -theories/IntMap/Mapiter.o : theories/IntMap/Addr.o -theories/IntMap/Mapiter.o : theories/IntMap/Addec.o -theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs -theories/IntMap/Maplists.o : theories/Bool/Sumbool.o -theories/IntMap/Maplists.o : theories/Init/Specif.o -theories/IntMap/Maplists.o : theories/Lists/PolyList.o -theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o -theories/IntMap/Maplists.o : theories/IntMap/Map.o -theories/IntMap/Maplists.o : theories/Init/Logic.o -theories/IntMap/Maplists.o : theories/IntMap/Fset.o -theories/IntMap/Maplists.o : theories/Init/Datatypes.o -theories/IntMap/Maplists.o : theories/Bool/Bool.o -theories/IntMap/Maplists.o : theories/IntMap/Addr.o -theories/IntMap/Maplists.o : theories/IntMap/Addec.o -theories/IntMap/Mapsubset.o : theories/IntMap/Mapsubset.hs -theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.o -theories/IntMap/Mapsubset.o : theories/IntMap/Map.o -theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o -theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o -theories/IntMap/Mapsubset.o : theories/Bool/Bool.o -theories/Lists/ListSet.o : theories/Lists/ListSet.hs -theories/Lists/ListSet.o : theories/Init/Specif.o -theories/Lists/ListSet.o : theories/Lists/PolyList.o -theories/Lists/ListSet.o : theories/Init/Logic.o -theories/Lists/ListSet.o : theories/Init/Datatypes.o -theories/Lists/PolyList.o : theories/Lists/PolyList.hs -theories/Lists/PolyList.o : theories/Init/Specif.o -theories/Lists/PolyList.o : theories/Init/Datatypes.o -theories/Lists/PolyListSyntax.o : theories/Lists/PolyListSyntax.hs -theories/Lists/Streams.o : theories/Lists/Streams.hs -theories/Lists/Streams.o : theories/Init/Datatypes.o -theories/Lists/TheoryList.o : theories/Lists/TheoryList.hs -theories/Lists/TheoryList.o : theories/Init/Specif.o -theories/Lists/TheoryList.o : theories/Lists/PolyList.o -theories/Lists/TheoryList.o : theories/Bool/DecBool.o -theories/Lists/TheoryList.o : theories/Init/Datatypes.o -theories/Logic/Berardi.o : theories/Logic/Berardi.hs -theories/Logic/ClassicalFacts.o : theories/Logic/ClassicalFacts.hs -theories/Logic/Classical.o : theories/Logic/Classical.hs -theories/Logic/Classical_Pred_Set.o : theories/Logic/Classical_Pred_Set.hs -theories/Logic/Classical_Pred_Type.o : theories/Logic/Classical_Pred_Type.hs -theories/Logic/Classical_Prop.o : theories/Logic/Classical_Prop.hs -theories/Logic/Classical_Type.o : theories/Logic/Classical_Type.hs -theories/Logic/Decidable.o : theories/Logic/Decidable.hs -theories/Logic/Eqdep_dec.o : theories/Logic/Eqdep_dec.hs -theories/Logic/Eqdep.o : theories/Logic/Eqdep.hs -theories/Logic/Hurkens.o : theories/Logic/Hurkens.hs -theories/Logic/JMeq.o : theories/Logic/JMeq.hs -theories/Logic/ProofIrrelevance.o : theories/Logic/ProofIrrelevance.hs -theories/Relations/Newman.o : theories/Relations/Newman.hs -theories/Relations/Operators_Properties.o : theories/Relations/Operators_Properties.hs -theories/Relations/Relation_Definitions.o : theories/Relations/Relation_Definitions.hs -theories/Relations/Relation_Operators.o : theories/Relations/Relation_Operators.hs -theories/Relations/Relation_Operators.o : theories/Init/Specif.o -theories/Relations/Relation_Operators.o : theories/Lists/PolyList.o -theories/Relations/Relations.o : theories/Relations/Relations.hs -theories/Relations/Rstar.o : theories/Relations/Rstar.hs -theories/Setoids/Setoid.o : theories/Setoids/Setoid.hs -theories/Sets/Classical_sets.o : theories/Sets/Classical_sets.hs -theories/Sets/Constructive_sets.o : theories/Sets/Constructive_sets.hs -theories/Sets/Cpo.o : theories/Sets/Cpo.hs -theories/Sets/Cpo.o : theories/Sets/Partial_Order.o -theories/Sets/Ensembles.o : theories/Sets/Ensembles.hs -theories/Sets/Finite_sets_facts.o : theories/Sets/Finite_sets_facts.hs -theories/Sets/Finite_sets.o : theories/Sets/Finite_sets.hs -theories/Sets/Image.o : theories/Sets/Image.hs -theories/Sets/Infinite_sets.o : theories/Sets/Infinite_sets.hs -theories/Sets/Integers.o : theories/Sets/Integers.hs -theories/Sets/Integers.o : theories/Sets/Partial_Order.o -theories/Sets/Integers.o : theories/Init/Datatypes.o -theories/Sets/Multiset.o : theories/Sets/Multiset.hs -theories/Sets/Multiset.o : theories/Init/Specif.o -theories/Sets/Multiset.o : theories/Init/Peano.o -theories/Sets/Multiset.o : theories/Init/Datatypes.o -theories/Sets/Partial_Order.o : theories/Sets/Partial_Order.hs -theories/Sets/Permut.o : theories/Sets/Permut.hs -theories/Sets/Powerset_Classical_facts.o : theories/Sets/Powerset_Classical_facts.hs -theories/Sets/Powerset_facts.o : theories/Sets/Powerset_facts.hs -theories/Sets/Powerset.o : theories/Sets/Powerset.hs -theories/Sets/Powerset.o : theories/Sets/Partial_Order.o -theories/Sets/Relations_1_facts.o : theories/Sets/Relations_1_facts.hs -theories/Sets/Relations_1.o : theories/Sets/Relations_1.hs -theories/Sets/Relations_2_facts.o : theories/Sets/Relations_2_facts.hs -theories/Sets/Relations_2.o : theories/Sets/Relations_2.hs -theories/Sets/Relations_3_facts.o : theories/Sets/Relations_3_facts.hs -theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs -theories/Sets/Uniset.o : theories/Sets/Uniset.hs -theories/Sets/Uniset.o : theories/Init/Specif.o -theories/Sets/Uniset.o : theories/Init/Datatypes.o -theories/Sets/Uniset.o : theories/Bool/Bool.o -theories/Sorting/Heap.o : theories/Sorting/Heap.hs -theories/Sorting/Heap.o : theories/Init/Specif.o -theories/Sorting/Heap.o : theories/Sorting/Sorting.o -theories/Sorting/Heap.o : theories/Lists/PolyList.o -theories/Sorting/Heap.o : theories/Sets/Multiset.o -theories/Sorting/Heap.o : theories/Init/Logic.o -theories/Sorting/Permutation.o : theories/Sorting/Permutation.hs -theories/Sorting/Permutation.o : theories/Init/Specif.o -theories/Sorting/Permutation.o : theories/Lists/PolyList.o -theories/Sorting/Permutation.o : theories/Sets/Multiset.o -theories/Sorting/Sorting.o : theories/Sorting/Sorting.hs -theories/Sorting/Sorting.o : theories/Init/Specif.o -theories/Sorting/Sorting.o : theories/Lists/PolyList.o -theories/Sorting/Sorting.o : theories/Init/Logic.o -theories/Wellfounded/Disjoint_Union.o : theories/Wellfounded/Disjoint_Union.hs -theories/Wellfounded/Inclusion.o : theories/Wellfounded/Inclusion.hs -theories/Wellfounded/Inverse_Image.o : theories/Wellfounded/Inverse_Image.hs -theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexicographic_Exponentiation.hs -theories/Wellfounded/Lexicographic_Product.o : theories/Wellfounded/Lexicographic_Product.hs -theories/Wellfounded/Transitive_Closure.o : theories/Wellfounded/Transitive_Closure.hs -theories/Wellfounded/Union.o : theories/Wellfounded/Union.hs -theories/Wellfounded/Wellfounded.o : theories/Wellfounded/Wellfounded.hs -theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.hs -theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o -theories/Wellfounded/Well_Ordering.o : theories/Init/Specif.o -theories/ZArith/Auxiliary.o : theories/ZArith/Auxiliary.hs -theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs -theories/ZArith/Fast_integer.o : theories/Init/Peano.o -theories/ZArith/Fast_integer.o : theories/Init/Datatypes.o -theories/ZArith/Wf_Z.o : theories/ZArith/Wf_Z.hs -theories/ZArith/Wf_Z.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o -theories/ZArith/Wf_Z.o : theories/Init/Specif.o -theories/ZArith/Wf_Z.o : theories/Init/Peano.o -theories/ZArith/Wf_Z.o : theories/Init/Logic.o -theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o -theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs -theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zarith_aux.o : theories/Init/Specif.o -theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o -theories/ZArith/ZArith_base.o : theories/ZArith/ZArith_base.hs -theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs -theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o -theories/ZArith/ZArith_dec.o : theories/Bool/Sumbool.o -theories/ZArith/ZArith_dec.o : theories/Init/Specif.o -theories/ZArith/ZArith_dec.o : theories/Init/Logic.o -theories/ZArith/ZArith.o : theories/ZArith/ZArith.hs -theories/ZArith/Zbool.o : theories/ZArith/Zbool.hs -theories/ZArith/Zbool.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zbool.o : theories/ZArith/Zmisc.o -theories/ZArith/Zbool.o : theories/ZArith/ZArith_dec.o -theories/ZArith/Zbool.o : theories/Bool/Sumbool.o -theories/ZArith/Zbool.o : theories/Init/Specif.o -theories/ZArith/Zbool.o : theories/Init/Datatypes.o -theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs -theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Zcomplements.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zcomplements.o : theories/ZArith/Wf_Z.o -theories/ZArith/Zcomplements.o : theories/Init/Specif.o -theories/ZArith/Zcomplements.o : theories/Init/Logic.o -theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o -theories/ZArith/Zdiv.o : theories/ZArith/Zdiv.hs -theories/ZArith/Zdiv.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Zdiv.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zdiv.o : theories/ZArith/Zmisc.o -theories/ZArith/Zdiv.o : theories/ZArith/ZArith_dec.o -theories/ZArith/Zdiv.o : theories/Init/Specif.o -theories/ZArith/Zdiv.o : theories/Init/Logic.o -theories/ZArith/Zdiv.o : theories/Init/Datatypes.o -theories/ZArith/Zhints.o : theories/ZArith/Zhints.hs -theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs -theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Zlogarithm.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zmisc.o : theories/ZArith/Zmisc.hs -theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zmisc.o : theories/Init/Specif.o -theories/ZArith/Zmisc.o : theories/Init/Datatypes.o -theories/ZArith/Zpower.o : theories/ZArith/Zpower.hs -theories/ZArith/Zpower.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zpower.o : theories/ZArith/Zmisc.o -theories/ZArith/Zpower.o : theories/Init/Logic.o -theories/ZArith/Zpower.o : theories/Init/Datatypes.o -theories/ZArith/Zsqrt.o : theories/ZArith/Zsqrt.hs -theories/ZArith/Zsqrt.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Zsqrt.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zsqrt.o : theories/ZArith/ZArith_dec.o -theories/ZArith/Zsqrt.o : theories/Init/Specif.o -theories/ZArith/Zsqrt.o : theories/Init/Logic.o -theories/ZArith/Zwf.o : theories/ZArith/Zwf.hs -# DO NOT DELETE: End of Haskell dependencies diff --git a/contrib/extraction/test/addReals b/contrib/extraction/test/addReals deleted file mode 100644 index fb73d47b..00000000 --- a/contrib/extraction/test/addReals +++ /dev/null @@ -1,21 +0,0 @@ -open TypeSyntax -open Fast_integer - - -let total_order_T x y = -if x = y then InleftT RightT -else if x < y then InleftT LeftT -else InrightT - -let rec int_to_positive i = - if i = 1 then XH - else - if (i mod 2) = 0 then XO (int_to_positive (i/2)) - else XI (int_to_positive (i/2)) - -let rec int_to_Z i = - if i = 0 then ZERO - else if i > 0 then POS (int_to_positive i) - else NEG (int_to_positive (-i)) - -let my_ceil x = int_to_Z (succ (int_of_float (floor x))) diff --git a/contrib/extraction/test/custom/Adalloc b/contrib/extraction/test/custom/Adalloc deleted file mode 100644 index e7204838..00000000 --- a/contrib/extraction/test/custom/Adalloc +++ /dev/null @@ -1,2 +0,0 @@ -Require Import BinNat. -Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Euclid b/contrib/extraction/test/custom/Euclid deleted file mode 100644 index a58e3940..00000000 --- a/contrib/extraction/test/custom/Euclid +++ /dev/null @@ -1 +0,0 @@ -Extraction Inline Wf_nat.gt_wf_rec Wf_nat.lt_wf_rec. diff --git a/contrib/extraction/test/custom/List b/contrib/extraction/test/custom/List deleted file mode 100644 index ffee7dc9..00000000 --- a/contrib/extraction/test/custom/List +++ /dev/null @@ -1 +0,0 @@ -Extraction NoInline map. diff --git a/contrib/extraction/test/custom/ListSet b/contrib/extraction/test/custom/ListSet deleted file mode 100644 index c9bea52a..00000000 --- a/contrib/extraction/test/custom/ListSet +++ /dev/null @@ -1 +0,0 @@ -Extraction NoInline set_add set_mem. diff --git a/contrib/extraction/test/custom/Lsort b/contrib/extraction/test/custom/Lsort deleted file mode 100644 index 22ab18e3..00000000 --- a/contrib/extraction/test/custom/Lsort +++ /dev/null @@ -1,2 +0,0 @@ -Require Import BinNat. -Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Map b/contrib/extraction/test/custom/Map deleted file mode 100644 index f024dbd7..00000000 --- a/contrib/extraction/test/custom/Map +++ /dev/null @@ -1,3 +0,0 @@ -Require Import BinNat. -Extraction NoInline Ndouble Ndouble_plus_one. - diff --git a/contrib/extraction/test/custom/Mapcard b/contrib/extraction/test/custom/Mapcard deleted file mode 100644 index 5932cf7b..00000000 --- a/contrib/extraction/test/custom/Mapcard +++ /dev/null @@ -1,4 +0,0 @@ -Require Import Plus. -Extraction NoInline plus_is_one. -Require Import BinNat. -Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/Mapiter b/contrib/extraction/test/custom/Mapiter deleted file mode 100644 index 22ab18e3..00000000 --- a/contrib/extraction/test/custom/Mapiter +++ /dev/null @@ -1,2 +0,0 @@ -Require Import BinNat. -Extraction NoInline Ndouble Ndouble_plus_one. diff --git a/contrib/extraction/test/custom/R_Ifp b/contrib/extraction/test/custom/R_Ifp deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/R_Ifp +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/R_sqr b/contrib/extraction/test/custom/R_sqr deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/R_sqr +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Ranalysis b/contrib/extraction/test/custom/Ranalysis deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Ranalysis +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Raxioms b/contrib/extraction/test/custom/Raxioms deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Raxioms +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rbase b/contrib/extraction/test/custom/Rbase deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rbase +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rbasic_fun b/contrib/extraction/test/custom/Rbasic_fun deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rbasic_fun +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rdefinitions b/contrib/extraction/test/custom/Rdefinitions deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rdefinitions +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Reals.v b/contrib/extraction/test/custom/Reals.v deleted file mode 100644 index 45d0a224..00000000 --- a/contrib/extraction/test/custom/Reals.v +++ /dev/null @@ -1,17 +0,0 @@ -Require Import Reals. -Extract Inlined Constant R => float. -Extract Inlined Constant R0 => "0.0". -Extract Inlined Constant R1 => "1.0". -Extract Inlined Constant Rplus => "(+.)". -Extract Inlined Constant Rmult => "( *.)". -Extract Inlined Constant Ropp => "(~-.)". -Extract Inlined Constant Rinv => "(fun x -> 1.0 /. x)". -Extract Inlined Constant Rlt => "(<)". -Extract Inlined Constant up => "AddReals.my_ceil". -Extract Inlined Constant total_order_T => "AddReals.total_order_T". -Extract Inlined Constant sqrt => "sqrt". -Extract Inlined Constant sigma => "(fun l h -> sigma_aux l h (Minus.minus h l))". -Extract Inlined Constant PI => "3.141593". -Extract Inlined Constant cos => cos. -Extract Inlined Constant sin => sin. -Extract Inlined Constant derive_pt => "(fun f x -> ((f (x+.1E-5))-.(f x))*.1E5)". diff --git a/contrib/extraction/test/custom/Rfunctions b/contrib/extraction/test/custom/Rfunctions deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rfunctions +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rgeom b/contrib/extraction/test/custom/Rgeom deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rgeom +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rlimit b/contrib/extraction/test/custom/Rlimit deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rlimit +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rseries b/contrib/extraction/test/custom/Rseries deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rseries +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rsigma b/contrib/extraction/test/custom/Rsigma deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rsigma +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/Rtrigo b/contrib/extraction/test/custom/Rtrigo deleted file mode 100644 index d8f1b3e7..00000000 --- a/contrib/extraction/test/custom/Rtrigo +++ /dev/null @@ -1,2 +0,0 @@ -Load "custom/Reals". - diff --git a/contrib/extraction/test/custom/ZArith_dec b/contrib/extraction/test/custom/ZArith_dec deleted file mode 100644 index 2201419e..00000000 --- a/contrib/extraction/test/custom/ZArith_dec +++ /dev/null @@ -1 +0,0 @@ -Extraction Inline Dcompare_inf Zcompare_rec. diff --git a/contrib/extraction/test/custom/fast_integer b/contrib/extraction/test/custom/fast_integer deleted file mode 100644 index e2b24953..00000000 --- a/contrib/extraction/test/custom/fast_integer +++ /dev/null @@ -1 +0,0 @@ -Extraction NoInline Zero_suivi_de Un_suivi_de. diff --git a/contrib/extraction/test/e b/contrib/extraction/test/e deleted file mode 100644 index 88b6c90b..00000000 --- a/contrib/extraction/test/e +++ /dev/null @@ -1,17 +0,0 @@ - -(* To trace Extraction, you can use this file via: *) -(* Drop. #use "e";; *) -(* *) - -#use "include";; -open Extraction;; -open Miniml;; -#trace extract_declaration;; -go();; - - - - - - - diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract deleted file mode 100755 index 83444be3..00000000 --- a/contrib/extraction/test/extract +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh -rm -f /tmp/extr$$.v -vfile=`./ml2v $1` -d=`dirname $vfile` -n=`basename $vfile .v` -if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi -echo "Cd \"$d\". Extraction Library $n. " >> /tmp/extr$$.v -../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v -out=$? -rm -f /tmp/extr$$.v -exit $out - diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell deleted file mode 100755 index d11bc706..00000000 --- a/contrib/extraction/test/extract.haskell +++ /dev/null @@ -1,12 +0,0 @@ -#!/bin/sh -rm -f /tmp/extr$$.v -vfile=`./hs2v $1` -d=`dirname $vfile` -n=`basename $vfile .v` -if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi -echo "Cd \"$d\". Extraction Language Haskell. Extraction Library $n. " >> /tmp/extr$$.v -../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v -out=$? -rm -f /tmp/extr$$.v -exit $out - diff --git a/contrib/extraction/test/hs2v.ml b/contrib/extraction/test/hs2v.ml deleted file mode 100644 index fd8b9b26..00000000 --- a/contrib/extraction/test/hs2v.ml +++ /dev/null @@ -1,14 +0,0 @@ -let _ = - for j = 1 to ((Array.length Sys.argv)-1) do - let fml = Sys.argv.(j) in - let f = Filename.chop_extension fml in - let fv = f ^ ".v" in - if Sys.file_exists ("../../../" ^ fv) then - print_string (fv^" ") - else - let d = Filename.dirname f in - let b = String.uncapitalize (Filename.basename f) in - let fv = Filename.concat d (b ^ ".v ") in - print_string fv - done; - print_newline() diff --git a/contrib/extraction/test/make_mli b/contrib/extraction/test/make_mli deleted file mode 100755 index 40ee496e..00000000 --- a/contrib/extraction/test/make_mli +++ /dev/null @@ -1,17 +0,0 @@ -#!/usr/bin/awk -We $0 - -{ match($0,"^open") - if (RLENGTH>0) state=1 - match($0,"^type") - if (RLENGTH>0) state=1 - match($0,"^\(\*\* ") - if (RLENGTH>0) state=2 - match($0,"^let") - if (RLENGTH>0) state=0 - match($0,"^and") - if ((RLENGTH>0) && (state==2)) state=0 - if ((RLENGTH>0) && (state==1)) state=1 - gsub("\(\*\* ","") - gsub("\*\*\)","") - if (state>0) print -} diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml deleted file mode 100644 index 363ea642..00000000 --- a/contrib/extraction/test/ml2v.ml +++ /dev/null @@ -1,14 +0,0 @@ -let _ = - for j = 1 to ((Array.length Sys.argv)-1) do - let fml = Sys.argv.(j) in - let f = Filename.chop_extension fml in - let fv = f ^ ".v" in - if Sys.file_exists ("../../../" ^ fv) then - print_string (fv^" ") - else - let d = Filename.dirname f in - let b = String.capitalize (Filename.basename f) in - let fv = Filename.concat d (b ^ ".v ") in - print_string fv - done; - print_newline() diff --git a/contrib/extraction/test/v2hs.ml b/contrib/extraction/test/v2hs.ml deleted file mode 100644 index 88632875..00000000 --- a/contrib/extraction/test/v2hs.ml +++ /dev/null @@ -1,9 +0,0 @@ -let _ = - for j = 1 to ((Array.length Sys.argv) -1) do - let s = Sys.argv.(j) in - let b = Filename.chop_extension (Filename.basename s) in - let b = String.capitalize b in - let d = Filename.dirname s in - print_string (Filename.concat d (b ^ ".hs ")) - done; - print_newline() diff --git a/contrib/extraction/test/v2ml.ml b/contrib/extraction/test/v2ml.ml deleted file mode 100644 index 245a1b1e..00000000 --- a/contrib/extraction/test/v2ml.ml +++ /dev/null @@ -1,9 +0,0 @@ -let _ = - for j = 1 to ((Array.length Sys.argv) -1) do - let s = Sys.argv.(j) in - let b = Filename.chop_extension (Filename.basename s) in - let b = String.uncapitalize b in - let d = Filename.dirname s in - print_string (Filename.concat d (b ^ ".ml ")) - done; - print_newline() |