diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 01:22:34 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-01-22 01:22:34 +0000 |
commit | 7da1f2925cd7c355d38f5cfac7d5d3195f6191e9 (patch) | |
tree | 1b16a7d57c23678e45bd4b400726c836e0c597d8 | |
parent | 7c4ffd70946030c74105323f8b45d6d9edfa7ac0 (diff) |
Extraction des modules, enfin !
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3569 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 118 | ||||
-rw-r--r-- | contrib/extraction/common.ml | 403 | ||||
-rw-r--r-- | contrib/extraction/common.mli | 14 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 764 | ||||
-rw-r--r-- | contrib/extraction/extract_env.mli | 17 | ||||
-rw-r--r-- | contrib/extraction/extraction.ml | 289 | ||||
-rw-r--r-- | contrib/extraction/extraction.mli | 20 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 94 | ||||
-rw-r--r-- | contrib/extraction/haskell.mli | 3 | ||||
-rw-r--r-- | contrib/extraction/miniml.mli | 48 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 314 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 30 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 258 | ||||
-rw-r--r-- | contrib/extraction/ocaml.mli | 8 | ||||
-rw-r--r-- | contrib/extraction/scheme.ml | 31 | ||||
-rw-r--r-- | contrib/extraction/scheme.mli | 3 | ||||
-rw-r--r-- | contrib/extraction/table.ml | 387 | ||||
-rw-r--r-- | contrib/extraction/table.mli | 83 | ||||
-rw-r--r-- | contrib/extraction/test/.depend | 96 | ||||
-rw-r--r-- | contrib/extraction/test/Makefile | 4 | ||||
-rw-r--r-- | contrib/extraction/test/Makefile.haskell | 359 |
21 files changed, 1957 insertions, 1386 deletions
@@ -356,13 +356,13 @@ contrib/correctness/putil.cmi: kernel/names.cmi contrib/correctness/past.cmi \ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \ contrib/correctness/penv.cmi contrib/correctness/prename.cmi \ kernel/term.cmi -contrib/extraction/common.cmi: library/lib.cmi library/libnames.cmi \ +contrib/extraction/common.cmi: library/libnames.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ kernel/names.cmi lib/pp.cmi -contrib/extraction/extract_env.cmi: kernel/declarations.cmi \ - kernel/environ.cmi library/libnames.cmi kernel/names.cmi -contrib/extraction/extraction.cmi: library/libnames.cmi \ - contrib/extraction/miniml.cmi +contrib/extraction/extract_env.cmi: library/libnames.cmi kernel/names.cmi +contrib/extraction/extraction.cmi: kernel/declarations.cmi kernel/environ.cmi \ + library/libnames.cmi contrib/extraction/miniml.cmi kernel/names.cmi \ + kernel/term.cmi contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \ kernel/names.cmi lib/pp.cmi contrib/extraction/miniml.cmi: library/libnames.cmi kernel/names.cmi \ @@ -374,8 +374,8 @@ contrib/extraction/ocaml.cmi: library/libnames.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi contrib/extraction/scheme.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \ lib/pp.cmi -contrib/extraction/table.cmi: library/libnames.cmi \ - contrib/extraction/miniml.cmi kernel/names.cmi +contrib/extraction/table.cmi: kernel/environ.cmi library/libnames.cmi \ + contrib/extraction/miniml.cmi kernel/names.cmi lib/pp.cmi contrib/interface/blast.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ proofs/tacmach.cmi contrib/interface/dad.cmi: proofs/proof_type.cmi proofs/tacexpr.cmo \ @@ -2320,54 +2320,52 @@ contrib/correctness/pwp.cmx: kernel/environ.cmx library/global.cmx \ contrib/correctness/ptyping.cmx contrib/correctness/putil.cmx \ kernel/reduction.cmx pretyping/reductionops.cmx kernel/term.cmx \ pretyping/termops.cmx lib/util.cmx contrib/correctness/pwp.cmi -contrib/extraction/common.cmo: library/declaremods.cmi \ - contrib/extraction/haskell.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi contrib/extraction/miniml.cmi \ +contrib/extraction/common.cmo: kernel/declarations.cmi kernel/environ.cmi \ + contrib/extraction/extraction.cmi contrib/extraction/haskell.cmi \ + library/libnames.cmi contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \ - library/nametab.cmi contrib/extraction/ocaml.cmi lib/pp.cmi \ - lib/pp_control.cmi parsing/printer.cmi contrib/extraction/scheme.cmi \ - contrib/extraction/table.cmi lib/util.cmi contrib/extraction/common.cmi -contrib/extraction/common.cmx: library/declaremods.cmx \ - contrib/extraction/haskell.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx contrib/extraction/miniml.cmi \ + contrib/extraction/ocaml.cmi lib/pp.cmi lib/pp_control.cmi \ + contrib/extraction/scheme.cmi contrib/extraction/table.cmi \ + kernel/term.cmi lib/util.cmi contrib/extraction/common.cmi +contrib/extraction/common.cmx: kernel/declarations.cmx kernel/environ.cmx \ + contrib/extraction/extraction.cmx contrib/extraction/haskell.cmx \ + library/libnames.cmx contrib/extraction/miniml.cmi \ contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \ - library/nametab.cmx contrib/extraction/ocaml.cmx lib/pp.cmx \ - lib/pp_control.cmx parsing/printer.cmx contrib/extraction/scheme.cmx \ - contrib/extraction/table.cmx lib/util.cmx contrib/extraction/common.cmi + contrib/extraction/ocaml.cmx lib/pp.cmx lib/pp_control.cmx \ + contrib/extraction/scheme.cmx contrib/extraction/table.cmx \ + kernel/term.cmx lib/util.cmx contrib/extraction/common.cmi contrib/extraction/extract_env.cmo: contrib/extraction/common.cmi \ - kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \ - pretyping/evd.cmi contrib/extraction/extraction.cmi library/global.cmi \ - kernel/inductive.cmi library/lib.cmi library/libnames.cmi \ - library/libobject.cmi library/library.cmi contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmi kernel/modops.cmi library/nameops.cmi \ - kernel/names.cmi library/nametab.cmi lib/pp.cmi parsing/printer.cmi \ - pretyping/retyping.cmi contrib/extraction/table.cmi lib/util.cmi \ - contrib/extraction/extract_env.cmi + kernel/declarations.cmi kernel/environ.cmi \ + contrib/extraction/extraction.cmi library/global.cmi library/lib.cmi \ + library/libnames.cmi library/libobject.cmi library/library.cmi \ + contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ + kernel/modops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + kernel/reduction.cmi contrib/extraction/table.cmi kernel/term.cmi \ + lib/util.cmi contrib/extraction/extract_env.cmi contrib/extraction/extract_env.cmx: contrib/extraction/common.cmx \ - kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \ - pretyping/evd.cmx contrib/extraction/extraction.cmx library/global.cmx \ - kernel/inductive.cmx library/lib.cmx library/libnames.cmx \ - library/libobject.cmx library/library.cmx contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmx kernel/modops.cmx library/nameops.cmx \ - kernel/names.cmx library/nametab.cmx lib/pp.cmx parsing/printer.cmx \ - pretyping/retyping.cmx contrib/extraction/table.cmx lib/util.cmx \ - contrib/extraction/extract_env.cmi + kernel/declarations.cmx kernel/environ.cmx \ + contrib/extraction/extraction.cmx library/global.cmx library/lib.cmx \ + library/libnames.cmx library/libobject.cmx library/library.cmx \ + contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ + kernel/modops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + kernel/reduction.cmx contrib/extraction/table.cmx kernel/term.cmx \ + lib/util.cmx contrib/extraction/extract_env.cmi contrib/extraction/extraction.cmo: kernel/declarations.cmi kernel/environ.cmi \ - pretyping/evd.cmi library/global.cmi kernel/inductive.cmi \ - pretyping/inductiveops.cmi library/libnames.cmi \ - contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ - library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ - pretyping/recordops.cmi pretyping/reductionops.cmi pretyping/retyping.cmi \ - library/summary.cmi contrib/extraction/table.cmi kernel/term.cmi \ - pretyping/termops.cmi lib/util.cmi contrib/extraction/extraction.cmi + pretyping/evd.cmi kernel/inductive.cmi pretyping/inductiveops.cmi \ + library/libnames.cmi contrib/extraction/miniml.cmi \ + contrib/extraction/mlutil.cmi library/nameops.cmi kernel/names.cmi \ + library/nametab.cmi lib/pp.cmi pretyping/recordops.cmi \ + pretyping/reductionops.cmi pretyping/retyping.cmi library/summary.cmi \ + contrib/extraction/table.cmi kernel/term.cmi pretyping/termops.cmi \ + lib/util.cmi contrib/extraction/extraction.cmi contrib/extraction/extraction.cmx: kernel/declarations.cmx kernel/environ.cmx \ - pretyping/evd.cmx library/global.cmx kernel/inductive.cmx \ - pretyping/inductiveops.cmx library/libnames.cmx \ - contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ - library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ - pretyping/recordops.cmx pretyping/reductionops.cmx pretyping/retyping.cmx \ - library/summary.cmx contrib/extraction/table.cmx kernel/term.cmx \ - pretyping/termops.cmx lib/util.cmx contrib/extraction/extraction.cmi + pretyping/evd.cmx kernel/inductive.cmx pretyping/inductiveops.cmx \ + library/libnames.cmx contrib/extraction/miniml.cmi \ + contrib/extraction/mlutil.cmx library/nameops.cmx kernel/names.cmx \ + library/nametab.cmx lib/pp.cmx pretyping/recordops.cmx \ + pretyping/reductionops.cmx pretyping/retyping.cmx library/summary.cmx \ + contrib/extraction/table.cmx kernel/term.cmx pretyping/termops.cmx \ + lib/util.cmx contrib/extraction/extraction.cmi contrib/extraction/g_extraction.cmo: toplevel/cerrors.cmi \ parsing/egrammar.cmi parsing/extend.cmi \ contrib/extraction/extract_env.cmi interp/genarg.cmi parsing/pcoq.cmi \ @@ -2381,12 +2379,12 @@ contrib/extraction/g_extraction.cmx: toplevel/cerrors.cmx \ contrib/extraction/haskell.cmo: library/libnames.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ library/nameops.cmi kernel/names.cmi contrib/extraction/ocaml.cmi \ - lib/pp.cmi parsing/printer.cmi lib/util.cmi \ + lib/pp.cmi contrib/extraction/table.cmi lib/util.cmi \ contrib/extraction/haskell.cmi contrib/extraction/haskell.cmx: library/libnames.cmx \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ library/nameops.cmx kernel/names.cmx contrib/extraction/ocaml.cmx \ - lib/pp.cmx parsing/printer.cmx lib/util.cmx \ + lib/pp.cmx contrib/extraction/table.cmx lib/util.cmx \ contrib/extraction/haskell.cmi contrib/extraction/mlutil.cmo: library/libnames.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi library/nametab.cmi \ @@ -2398,32 +2396,34 @@ contrib/extraction/mlutil.cmx: library/libnames.cmx \ contrib/extraction/mlutil.cmi contrib/extraction/ocaml.cmo: library/libnames.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ - library/nameops.cmi kernel/names.cmi lib/pp.cmi parsing/printer.cmi \ + library/nameops.cmi kernel/names.cmi lib/pp.cmi \ contrib/extraction/table.cmi lib/util.cmi contrib/extraction/ocaml.cmi contrib/extraction/ocaml.cmx: library/libnames.cmx \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ - library/nameops.cmx kernel/names.cmx lib/pp.cmx parsing/printer.cmx \ + library/nameops.cmx kernel/names.cmx lib/pp.cmx \ contrib/extraction/table.cmx lib/util.cmx contrib/extraction/ocaml.cmi contrib/extraction/scheme.cmo: library/libnames.cmi \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ library/nameops.cmi kernel/names.cmi contrib/extraction/ocaml.cmi \ - lib/pp.cmi lib/util.cmi contrib/extraction/scheme.cmi + lib/pp.cmi contrib/extraction/table.cmi lib/util.cmi \ + contrib/extraction/scheme.cmi contrib/extraction/scheme.cmx: library/libnames.cmx \ contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ library/nameops.cmx kernel/names.cmx contrib/extraction/ocaml.cmx \ - lib/pp.cmx lib/util.cmx contrib/extraction/scheme.cmi + lib/pp.cmx contrib/extraction/table.cmx lib/util.cmx \ + contrib/extraction/scheme.cmi contrib/extraction/table.cmo: kernel/declarations.cmi kernel/environ.cmi \ library/global.cmi library/goptions.cmi library/lib.cmi \ library/libnames.cmi library/libobject.cmi contrib/extraction/miniml.cmi \ library/nameops.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \ - lib/pp.cmi parsing/printer.cmi kernel/reduction.cmi library/summary.cmi \ - kernel/term.cmi lib/util.cmi contrib/extraction/table.cmi + lib/pp.cmi kernel/reduction.cmi library/summary.cmi kernel/term.cmi \ + lib/util.cmi contrib/extraction/table.cmi contrib/extraction/table.cmx: kernel/declarations.cmx kernel/environ.cmx \ library/global.cmx library/goptions.cmx library/lib.cmx \ library/libnames.cmx library/libobject.cmx contrib/extraction/miniml.cmi \ library/nameops.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \ - lib/pp.cmx parsing/printer.cmx kernel/reduction.cmx library/summary.cmx \ - kernel/term.cmx lib/util.cmx contrib/extraction/table.cmi + lib/pp.cmx kernel/reduction.cmx library/summary.cmx kernel/term.cmx \ + lib/util.cmx contrib/extraction/table.cmi contrib/field/field.cmo: toplevel/cerrors.cmi interp/constrintern.cmi \ library/declare.cmi parsing/egrammar.cmi pretyping/evd.cmi \ parsing/extend.cmi interp/genarg.cmi library/global.cmi lib/gmap.cmi \ diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 28f560d96..0f07658fb 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -11,15 +11,16 @@ open Pp open Util open Names +open Term +open Declarations open Nameops open Libnames -open Nametab open Table open Miniml open Mlutil open Ocaml -(*s Get all references used in one [ml_decl list]. *) +(*s Get all references used in one [ml_structure]. *) module Orefset = struct type t = { set : Refset.t ; list : global_reference list } @@ -33,51 +34,12 @@ end type updown = { mutable up : Orefset.t ; mutable down : Orefset.t } -let decl_get_references ld = +let struct_get_references struc = let o = { up = Orefset.empty ; down = Orefset.empty } in - let do_term r = o.down <- Orefset.add r o.down in - let do_cons r = o.up <- Orefset.add r o.up in + let do_term r = o.down <- Orefset.add (long_r r) o.down in + let do_cons r = o.up <- Orefset.add (long_r r) o.up in let do_type = if lang () = Haskell then do_cons else do_term in - List.iter (decl_iter_references do_term do_cons do_type) ld; o - -(*S Modules considerations. *) - -let long_module r = - match modpath (kn_of_r r) with - | MPfile d -> d - | _ -> anomaly "TODO: extraction not ready for true modules" - -let short_module r = List.hd (repr_dirpath (long_module r)) - -(*s [extract_module m] returns all the global reference declared - in a module. This is done by traversing the segment of module [m]. - We just keep constants and inductives. *) - -let segment_contents seg = - let get_reference = function - | (_,kn), Lib.Leaf o -> - (match Libobject.object_tag o with - | "CONSTANT" -> ConstRef kn - | "INDUCTIVE" -> IndRef (kn,0) - | _ -> failwith "caught") - | _ -> failwith "caught" - in - Util.map_succeed get_reference seg - -let module_contents m = - segment_contents (Declaremods.module_objects (MPfile m)) - -(*s The next function finds all names common to at least two used modules. *) - -let modules_reference_clashes modules = - let id_of_r r = lowercase_id (id_of_global None r) in - let map = - Dirset.fold - (fun mod_name map -> - let rl = List.map id_of_r (module_contents mod_name) in - List.fold_left (fun m id -> Idmap.add id (Idmap.mem id m) m) map rl) - modules Idmap.empty - in Idmap.fold (fun i b s -> if b then Idset.add i s else s) map Idset.empty + struct_iter_references do_term do_cons do_type struc; o (*S Renamings. *) @@ -85,80 +47,238 @@ let modules_reference_clashes modules = let keywords = ref Idset.empty let global_ids = ref Idset.empty +let modular = ref false let renamings = Hashtbl.create 97 let rename r s = Hashtbl.add renamings r s let get_renamings r = Hashtbl.find renamings r -let create_mono_renamings decls = - let { up = u ; down = d } = decl_get_references decls in - let add upper r = - try if not (to_inline r) then raise Not_found; - rename r (find_ml_extraction r) +let must_qualify = ref Refset.empty + +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 modular_rename up id = + let s = string_of_id id in + let prefix = if up then "Coq_" else "coq_" in + let check = if up then is_upper else is_lower in + if not (check s) || + (Idset.mem id !keywords) || + (String.length s >= 4 && String.sub s 0 4 = prefix) + then prefix ^ s + else s + +let rename_module = modular_rename true + +let mp_to_list mp = + let rec f ls = function + | MPfile d -> + String.capitalize (string_of_id (List.hd (repr_dirpath d))) :: ls + | MPself msid -> rename_module (id_of_msid msid) :: ls + | MPbound mbid -> rename_module (id_of_mbid mbid) :: ls + | MPdot (mp,l) -> f (rename_module (id_of_label l) :: ls) mp + in f [] mp + +let mp_to_list' mp = + let rec f ls = function + | mp when at_toplevel mp -> ls + | MPself msid -> rename_module (id_of_msid msid) :: ls + | MPbound mbid -> rename_module (id_of_mbid mbid) :: ls + | MPdot (mp,l) -> f (rename_module (id_of_label l) :: ls) mp + | _ -> assert false + in f [] mp + +let string_of_modlist l = + List.fold_right (fun s s' -> if s' = "" then s else s ^ "." ^ s') l "" + +let string_of_ren l s = + if l = [] then s else (string_of_modlist l)^"."^s + +let contents_first_level mp = + let s = ref Stringset.empty in + let add b id = s := Stringset.add (modular_rename b id) !s in + let upper_type = (lang () = Haskell) in + let contents_seb = function + | (l, SEBconst cb) -> + let id = id_of_label l in + (match Extraction.constant_kind !cur_env cb with + | Extraction.Logical -> () + | Extraction.Type -> add upper_type (id_of_label l) + | Extraction.Term -> add false (id_of_label l)) + | (_, SEBmind mib) -> + Array.iter + (fun mip -> + if mip.mind_sort = (Prop Null) then () + else begin + add upper_type mip.mind_typename; + Array.iter (add true) mip.mind_consnames + end) + mib.mind_packets + | _ -> () + in + match (Environ.lookup_module mp !cur_env).mod_expr with + | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; (mp,!s) + | _ -> mp,!s + +let modules_first_level mp = + let s = ref Stringset.empty in + let add id = s := Stringset.add (rename_module id) !s in + let contents_seb = function + | (l, (SEBmodule _ | SEBmodtype _)) -> add (id_of_label l) + | _ -> () + in + match (Environ.lookup_module mp !cur_env).mod_expr with + | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s + | _ -> !s + +let contents_first_level = + let cache = ref MPmap.empty in + fun mp -> + try MPmap.find mp !cache with Not_found -> - let id = id_of_global None r in - let id = if upper then uppercase_id id else lowercase_id id in - let id = rename_id id !global_ids in - global_ids := Idset.add id !global_ids; - rename r (string_of_id id) + let res = contents_first_level mp in + cache := MPmap.add mp res !cache; + res + +let rec clash_in_contents mp0 s = function + | [] -> false + | (mp,_) :: _ when mp = mp0 -> false + | (mp,ss) :: l -> (Stringset.mem s ss) || (clash_in_contents mp0 s l) + +let create_modular_renamings struc = + let cur_mp = fst (List.hd struc) in + let modfiles = ref MPset.empty in + let { up = u ; down = d } = struct_get_references struc in - List.iter (add true) (List.rev (Orefset.list u)); - List.iter (add false) (List.rev (Orefset.list d)) - -let create_modular_renamings current_module decls = - let { up = u ; down = d } = decl_get_references decls in - let modules = - let f r s = Dirset.add (long_module r) s in - Refset.fold f (Orefset.set u) (Refset.fold f (Orefset.set d) Dirset.empty) - in - let modular_clashs = modules_reference_clashes modules + (* 1) create renamings of objects *) + let add upper r = + let mp = modpath (kn_of_r r) in + begin try + let mp = modfile_of_mp mp in + if mp <> cur_mp then modfiles := MPset.add mp !modfiles + with Not_found -> () + end; + let mplist = mp_to_list (modpath (kn_of_r r)) in + let s = modular_rename upper (id_of_global r) in + global_ids := Idset.add (id_of_string s) !global_ids; + Hashtbl.add renamings r (mplist,s) + in + Refset.iter (add true) (Orefset.set u); + Refset.iter (add false) (Orefset.set d); + + (* 2) determine the opened libraries and the potential clashes *) + let used_modules = MPset.elements !modfiles in + let s = ref (modules_first_level cur_mp) in + 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 env = List.rev_map contents_first_level used_modules in + let needs_qualify r = + let mp = modpath (kn_of_r r) in + if not (is_modfile mp) || mp = cur_mp then () + else + let s = snd (get_renamings r) in + if clash_in_contents mp s env + then must_qualify := Refset.add r !must_qualify in - let clash r id = - exists_cci (make_path (dirpath (sp_of_global None r)) id) + Refset.iter needs_qualify (Orefset.set u); + Refset.iter needs_qualify (Orefset.set d); + used_modules + +let create_mono_renamings struc = + let fst_level_modules = ref Idmap.empty in + let { up = u ; down = d } = struct_get_references struc in - let prefix upper r id = - let prefix = if upper then "Coq_" else "coq_" in - let id' = if upper then uppercase_id id else lowercase_id id in - if (Idset.mem id' !keywords) || (id <> id' && clash r id') then - id_of_string (prefix^(string_of_id id)) - else id' - in + (* 1) create renamings of objects *) let add upper r = - try if not (to_inline r) then raise Not_found; - rename r (find_ml_extraction r) - with Not_found -> - let id = id_of_global None r in - let m = short_module r in - let id' = prefix upper r id in - let qualify = - (m <> current_module) && (Idset.mem (lowercase_id id) modular_clashs) - in - if qualify then - let s = String.capitalize (string_of_id m) ^ "." ^ (string_of_id id') in - Hashtbl.add renamings r s - else begin - global_ids := Idset.add id' !global_ids; - Hashtbl.add renamings r (string_of_id id') - end + let mp = modpath (kn_of_r r) in + begin try + let mp,l = fst_level_module_of_mp mp in + let id = id_of_label l in + if Idmap.find id !fst_level_modules <> mp then + error_module_clash (string_of_id id) + else fst_level_modules := Idmap.add id mp !fst_level_modules + with Not_found -> () + end; + let mplist = mp_to_list' (modpath (kn_of_r r)) in + let my_id = if upper then uppercase_id else lowercase_id in + let id = + if mplist = [] then + next_ident_away (my_id (id_of_global r)) (Idset.elements !global_ids) + else id_of_string (modular_rename upper (id_of_global r)) + in + global_ids := Idset.add id !global_ids; + Hashtbl.add renamings r (mplist,string_of_id id) in List.iter (add true) (List.rev (Orefset.list u)); - List.iter (add false) (List.rev (Orefset.list d)); - Idset.remove current_module - (Dirset.fold (fun m s -> Idset.add (List.hd (repr_dirpath m)) s) - modules Idset.empty) + List.iter (add false) (List.rev (Orefset.list d)) (*s Renaming issues at toplevel *) module ToplevelParams = struct let globals () = Idset.empty - let pp_global r = Printer.pr_global r + let pp_global _ r = pr_global r + let pp_long_module mp = str (string_of_mp mp) + let pp_short_module id = pr_id id end (*s Renaming issues for a monolithic or modular extraction. *) +let rec remove_common l l' = match l,l' with + | [], _ -> l' + | s::q, s'::q' -> if s = s' then remove_common q q' else l' + | _ -> assert false + +let rec length_common_prefix l l' = match l,l' with + | [],_ -> 0 + | _, [] -> 0 + | s::q, s'::q' -> if s <> s' then 0 else 1+(length_common_prefix q q') + +let rec decreasing_contents mp = match mp with + | MPdot (mp',_) -> (contents_first_level mp) :: (decreasing_contents mp') + | mp when is_toplevel mp -> [] + | _ -> [contents_first_level mp] + module StdParams = struct + let globals () = !global_ids - let pp_global r = str (Hashtbl.find renamings r) + + let pp_global cur_mp r = + let cur_mp = long_mp cur_mp in + let cur_l = if !modular then mp_to_list cur_mp else mp_to_list' cur_mp in + let r = long_r r in + let mp = modpath (kn_of_r r) in + let l,s = get_renamings r in + let n = length_common_prefix cur_l l in + if n = 0 && !modular (* [r] is in another module *) + then + if (Refset.mem r !must_qualify) || (lang () = Haskell) + then str (string_of_ren l s) + else + if clash_in_contents mp s (decreasing_contents cur_mp) + then str (string_of_ren l s) + else str s + else + let nl = List.length l in + if n = nl && nl < List.length cur_l then (* strict prefix *) + if clash_in_contents mp s (decreasing_contents cur_mp) + then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l) + else str s + else (* [cur_mp] and [mp] are orthogonal *) + let l = remove_common cur_l l + in str (string_of_ren l s) + + let pp_long_module mp = + str (string_of_modlist (if !modular then mp_to_list mp else mp_to_list' mp)) + + let pp_short_module id = str (rename_module id) end module ToplevelPp = Ocaml.Make(ToplevelParams) @@ -166,11 +286,22 @@ module OcamlPp = Ocaml.Make(StdParams) module HaskellPp = Haskell.Make(StdParams) module SchemePp = Scheme.Make(StdParams) -let pp_decl () = match lang () with - | Ocaml -> OcamlPp.pp_decl - | Haskell -> HaskellPp.pp_decl - | Scheme -> SchemePp.pp_decl - | Toplevel -> ToplevelPp.pp_decl +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 @@ -178,7 +309,8 @@ let set_keywords () = | Haskell -> keywords := Haskell.keywords | Scheme -> keywords := Scheme.keywords | Toplevel -> keywords := Idset.empty); - global_ids := !keywords + global_ids := !keywords; + must_qualify := Refset.empty let preamble prm = match lang () with | Ocaml -> Ocaml.preamble prm @@ -186,36 +318,59 @@ let preamble prm = match lang () with | 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 extract_to_file f prm decls = +let print_structure_to_file f prm struc = cons_cofix := Refset.empty; Hashtbl.clear renamings; set_keywords (); - let used_modules = - if lang () = Toplevel then Idset.empty - else if prm.modular then - create_modular_renamings prm.mod_name decls - else begin create_mono_renamings decls; Idset.empty end + 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 pp_decl = pp_decl () in - let cout = match f with - | None -> stdout - | Some f -> open_out f in + let print_dummys = + (struct_ast_search MLdummy struc, + struct_type_search Tdummy struc, + struct_type_search Tunknown struc) + in + (* print the implementation *) + let cout = match f with None -> stdout | Some (f,_) -> open_out f in let ft = Pp_control.with_output_to cout in - let print_dummys = - (decl_search MLdummy decls, - decl_type_search Tdummy decls, - decl_type_search Tunknown decls) in - pp_with ft (preamble prm used_modules print_dummys); - begin try - List.iter (fun d -> msgnl_with ft (pp_decl d)) decls - with e -> - pp_flush_with ft (); if f <> None then close_out cout; raise e + begin try + msg_with ft (preamble prm used_modules print_dummys); + msg_with ft (pp_struct struc); + if f <> None then close_out cout; + with e -> + if f <> None then close_out cout; raise e end; - pp_flush_with ft (); - if f <> None then close_out cout; - + (* 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 + | _ -> () + (*i (* DO NOT REMOVE: used when making names resolution *) let cout = open_out (f^".ren") in diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index fb2291edf..7dae2ae19 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -14,16 +14,10 @@ open Libnames open Miniml open Mlutil -val long_module : global_reference -> dir_path +val print_one_decl : + ml_structure -> module_path -> ml_decl -> unit -val create_mono_renamings : ml_decl list -> unit -val set_keywords : unit -> unit +val print_structure_to_file : + (string * string) option -> extraction_params -> ml_structure -> unit -val pp_decl : unit -> ml_decl -> std_ppcmds -val segment_contents : Lib.library_segment -> global_reference list - -val module_contents : dir_path -> global_reference list - -val extract_to_file : - string option -> extraction_params -> ml_decl list -> unit diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 0e5325a2e..ab798eebf 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -8,22 +8,56 @@ (*i $Id$ i*) -open Pp -open Util +open Term open Declarations open Names -open Nameops open Libnames +open Pp +open Util open Miniml open Table open Extraction open Mlutil open Common -let mp_of_kn kn = - let mp,_,l = repr_kn kn in MPdot (mp,l) +(*s Recursive computation of the global references to extract. + We use a set of functions visiting the extracted objects in + a depth-first way. + We maintain an (imperative) structure [visit'] containing + the set of already visited references and the list of + references to extract. The entry point is the function [visit]: + it first normalizes the reference, and then check it has already been + visisted; if not, it adds it to the set of visited references, then + recursively traverses its extraction and finally adds it to the [result]. *) + +(* Recursive extracted environment for a list of reference: we just + iterate [visit] on the list, starting with an empty + extracted environment, and we return the reversed list of + declaration in the field [result]. *) + +type visit' = { mutable visited : KNset.t; mutable result : ml_decl list } -let toplevel () = +let extract_env rl = + let knset = + Refset.fold (compose KNset.add kn_of_r) (all_customs ()) KNset.empty in + let v = { visited = knset; result = [] } in + let rec visit r = + let kn = kn_of_r r in + if not (KNset.mem kn v.visited) then begin + (* we put [kn] in [visited] first to avoid loops in inductive defs *) + v.visited <- KNset.add kn v.visited; + let d = extract_declaration !cur_env r in + decl_iter_references visit visit visit d; + v.result <- d :: v.result + end + in + List.iter visit rl; + List.rev v.result + + +(*s Obtaining Coq environment. *) + +let toplevel_env () = let seg = Lib.contents_after None in let get_reference = function | (_,kn), Lib.Leaf o -> @@ -37,30 +71,36 @@ let toplevel () = in l,seb | _ -> failwith "caught" in - MEBstruct (initial_msid, List.rev (map_succeed get_reference seg)) + match current_toplevel () with + | MPself msid -> MEBstruct (msid, List.rev (map_succeed get_reference seg)) + | _ -> assert false let environment_until dir_opt = let rec parse = function + | [] when dir_opt = None -> [current_toplevel (), toplevel_env ()] | [] -> [] - | d :: l when dir_opt = Some d -> [] | d :: l -> match (Global.lookup_module (MPfile d)).mod_expr with - | Some meb -> (d, meb) :: (parse l) + | Some meb -> + if dir_opt = Some d then [MPfile d, meb] + else (MPfile d, meb) :: (parse l) | _ -> assert false in parse (Library.loaded_libraries ()) -let std_kn mp l = make_kn mp empty_dirpath l +(*s Aux. functions *) -let rec sub_modpath mp = match mp with - | MPdot (mp',_) -> MPset.add mp (sub_modpath mp') - | _ -> MPset.singleton mp +let r_of_kn env kn = + try let _ = Environ.lookup_constant kn env in ConstRef kn + with Not_found -> + try let _ = Environ.lookup_mind kn env in IndRef (kn,0) + with Not_found -> assert false (* 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 = std_kn mp l in + let kn = make_kn mp empty_dirpath l in match elem with | SEBconst cb -> Environ.add_constant kn cb env | SEBmind mib -> Environ.add_mind kn mib env @@ -70,486 +110,366 @@ let add_structure mp msb env = let add_functor mbid mtb env = Modops.add_module (MPbound mbid) (Modops.module_body_of_type mtb) env - -let mp_short = ref initial_path -let cur_env = ref (Global.env ()) - -let pr_label l = str (string_of_label l) -let pr_term t = Printer.prterm_env !cur_env t - -let rec print_seb = function - | l, SEBconst {const_body=None; const_type=t} -> - msg (str "Cst " ++ pr_label l ++ str " : " ++ - pr_term t ++ fnl ()) - | l, SEBconst {const_body=Some lbody} -> - let body = Declarations.force lbody in - let t = Retyping.get_type_of !cur_env Evd.empty body in - msg (str "Cst " ++ pr_label l ++ str " = " ++ - pr_term body ++ fnl () ++ - str " : " ++ pr_term t ++ fnl ()) - | l, SEBmind mind -> - let t = Inductive.type_of_inductive !cur_env ((std_kn !mp_short l),0) in - msg (str "Ind " ++ pr_label l ++ str " : " ++ pr_term t ++ fnl ()) - | l, SEBmodule mb -> print_module l mb - | l, SEBmodtype mtb -> print_modtype l mtb - -and print_msb = function - | [] -> () - | seb :: msb -> print_seb seb; print_msb msb - -and print_module l mb = - msg (str "Begin Module " ++ pr_label l ++ fnl ()); - (match mb.mod_expr with - | None -> () - | Some meb -> print_meb meb); - msg (str "End Module " ++ pr_label l ++ fnl ()) - -and print_meb = function + +(*s First, we parse everything in order to produce 1) an env containing + every internal objects and 2) a table of aliases between short and long + [module_path]. *) + +let rec init_env_seb loc abs = function + | l, SEBmodule mb -> + init_env_module loc (option_app (fun mp -> MPdot (mp,l)) abs) mb + | l, SEBmodtype mtb -> init_env_modtype loc mtb + | _ -> () + +and init_env_module loc abs mb = + option_iter (init_env_meb loc abs) mb.mod_expr + +and init_env_meb loc abs = function | MEBident mp -> () + | MEBapply (meb, meb',_) -> + init_env_meb loc None meb; init_env_meb loc None meb' | MEBfunctor (mbid, mtb, meb) -> cur_env := add_functor mbid mtb !cur_env; - print_meb meb + init_env_modtype loc mtb; + init_env_meb loc None meb | MEBstruct (msid, msb) -> - let mp_old = !mp_short in - mp_short := MPself msid; - cur_env := add_structure !mp_short msb !cur_env; - msg (str "Begin Struct " ++ str (string_of_mp !mp_short) ++ fnl ()); - print_msb msb; - msg (str "End Struct " ++ str (string_of_mp !mp_short) ++ fnl ()); - mp_short := mp_old - | MEBapply (meb, meb',_) -> - print_meb meb; msg (str "@" ++ fnl ()); print_meb meb' - -and print_modtype l mtb = - msg (str "Begin Module Type " ++ pr_label l ++ fnl ()); - (match mtb with - | MTBident mp -> () - | MTBfunsig (mbid, mtb, mtb') -> - cur_env := add_functor mbid mtb !cur_env; - print_modtype l mtb' - | MTBsig (msid, sign) -> - let mp_old = !mp_short in - mp_short := MPself msid; - cur_env := Modops.add_signature !mp_short sign !cur_env; - msg (str "Begin Sig " ++ str (string_of_mp !mp_short) ++ fnl ()); - print_sign sign; - msg (str "End Sig " ++ str (string_of_mp !mp_short) ++ fnl ()); - mp_short := mp_old); - msg (str "End Module Type " ++ pr_label l ++ fnl ()) - -and print_sign = function - | [] -> () - | spec :: sign -> print_spec spec; print_sign sign + let loc = MPself msid in + cur_env := add_structure loc msb !cur_env; + option_iter (add_aliases loc) abs; + List.iter (init_env_seb loc abs) msb + +and init_env_modtype loc = function + | MTBident mp -> () + | MTBfunsig (mbid, mtb, mtb') -> + cur_env := add_functor mbid mtb !cur_env; + init_env_modtype loc mtb; + init_env_modtype loc mtb' + | MTBsig (msid, sign) -> + let loc = MPself msid in + cur_env := Modops.add_signature loc sign !cur_env; + List.iter (init_env_spec loc) sign -and print_spec = function - | l, SPBconst {const_type=t} -> - msg (str "Cst " ++ pr_label l ++ str " : " ++ pr_term t ++ fnl ()) - | l, SPBmind mind -> - let t = Inductive.type_of_inductive !cur_env ((std_kn !mp_short l),0) in - msg (str "Ind " ++ pr_label l ++ str " : " ++ pr_term t ++ fnl ()) - | l, SPBmodule {msb_modtype=mtb} -> print_modtype l mtb - | l, SPBmodtype mtb -> print_modtype l mtb - +and init_env_spec loc = function + | l, SPBmodule {msb_modtype=mtb} -> init_env_modtype loc mtb + | l, SPBmodtype mtb -> init_env_modtype loc mtb + | _ -> () -let print_all () = +let init_env l = cur_env := Global.env (); - mp_short := initial_path; List.iter - (fun (d,meb) -> - msg (str "Library " ++ pr_dirpath d ++ fnl ()); print_meb meb) - (environment_until None); - msg (str "Toplevel" ++ fnl ()); print_meb (toplevel ()) + (fun (mp,meb) -> init_env_meb (current_toplevel ()) (Some mp) meb) l -(* +(*s The extraction pass. *) type visit = { mutable kn : KNset.t; mutable mp : MPset.t } -let in_kn kn v = KNset.mem kn v.kn -let in_mp mp v = MPset.mem mp v.mp - -let rec visit_type m eenv t = - let rec visit = function - | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l - | Tarr (t1,t2) -> visit t1; visit t2 - | Tvar _ | Tdummy | Tunknown | Tcustom _ -> () - | Tmeta _ | Tvar' _ -> assert false - in - visit t - -and visit_ast m eenv a = - let rec visit = function - | MLglob r -> visit_reference m eenv r - | MLapp (a,l) -> visit a; List.iter visit l - | MLlam (_,a) -> visit a - | MLletin (_,a,b) -> visit a; visit b - | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l - | MLcase (a,br) -> - visit a; - Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br - | MLfix (_,_,l) -> Array.iter visit l - | MLcast (a,t) -> visit a; visit_type m eenv t - | MLmagic a -> visit a - | MLrel _ | MLdummy | MLexn _ | MLcustom _ -> () - in - visit a - -and visit_inductive m eenv inds = - let visit_constructor (_,tl) = List.iter (visit_type m eenv) tl in - let visit_ind (_,_,cl) = List.iter visit_constructor cl in - List.iter visit_ind inds - -and visit_decl m eenv = function - | Dind (inds,_) -> visit_inductive m eenv inds - | Dtype (_,_,t) -> visit_type m eenv t - | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t - | Dfix (_,c,t) -> - Array.iter (visit_ast m eenv) c; - Array.iter (visit_type m eenv) t - | _ -> () - - -let rec get_structure_elem_references = function - | SEind ml_ind -> - -let rec extract_msb mp all v = function - | [] -> [] - | (l,seb) -> - let ml_msb = extract_msb v in - match seb with - | SEBconst cb -> - let kn = std_kn mp l in - if all || in_kn kn v then - let ml_se = extraction_constant_body kn cb in - get_structure_elem_references ml_se v; - ml_se :: ml_msb - else ml_msb - | SEBmind mib -> - let kn = std_kn mp l in - if all || in_kn kn v then - let ml_se = extraction_inductive_body kn mib in - search_visit ml_se v; - ml_se :: ml_msb - else ml_msb - | SEBmodule mb -> - let mp = MPdot (mp,l) in - if all || in_mp mp v then - SEmodule (extraction_module mp true v m) :: ml_msb - else msb - | SEBmodtype mtb -> - let kn = std_kn mp l in - if all || in_kn kn v then - SEmodtype (extraction_mtb (MPdot (mp,l)) true v m) :: ml_msb - else msb - - -let mono_environment kn_set = - let add_mp kn mpset = KNset.union (sub_modpath (modpath kn)) mpset - let kn_to_visit = ref kn_set - and mp_to_visit = ref (KNset.fold add_mp kn_set MPset.empty) - in - - let rec extract_structure_body = +let in_kn v kn = KNset.mem (long_kn kn) v.kn +let in_mp v mp = MPset.mem (long_mp mp) v.mp + +let visit_ref v r = + let kn = long_kn (kn_of_r r) in + v.kn <- KNset.add kn v.kn; + v.mp <- MPset.union (prefixes_mp (modpath kn)) v.mp + +exception Impossible + +let check_arity cb = + if Reduction.is_arity !cur_env cb.const_type then raise Impossible + +let check_fix cb i = + match cb.const_body with + | None -> raise Impossible + | Some lbody -> + match kind_of_term (Declarations.force lbody) with + | Fix ((_,j),recd) when i=j -> check_arity cb; (true,recd) + | CoFix (j,recd) when i=j -> check_arity cb; (false,recd) + | _ -> raise Impossible + +let factor_fix l cb msb = + let _,recd as check = check_fix cb 0 in + let n = Array.length (let fi,_,_ = recd in fi) in + if n = 1 then [|l|], recd, msb + else begin + if List.length msb < n-1 then raise Impossible; + let msb', msb'' = list_chop (n-1) msb in + let labels = Array.make n l in + list_iter_i + (fun j -> + function + | (l,SEBconst cb') -> + if check <> check_fix cb' (j+1) then raise Impossible; + labels.(j+1) <- l; + | _ -> raise Impossible) msb'; + labels, recd, msb'' + end +let logical_decl = function + | Dterm (_,MLdummy,Tdummy) -> true + | Dtype (_,[],Tdummy) -> true + | Dfix (_,av,tv) -> + (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv) + | Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + | _ -> false - let top = toplevel_structure_body () +let logical_spec = function + | Stype (_, [], Some Tdummy) -> true + | Sval (_,Tdummy) -> true + | Sind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets + | _ -> false -*) +let get_decl_references v d = + let f = visit_ref v in decl_iter_references f f f d -(*s Auxiliary functions dealing with modules. *) +let get_spec_references v s = + let f = visit_ref v in spec_iter_references f f f s -let dir_module_of_id m = - try - Nametab.full_name_module (make_short_qualid m) - with Not_found -> - errorlabstrm "module_message" - (str "Module" ++ spc () ++ pr_id m ++ spc () ++ str "not found.") - -(*s Module name clash verification. *) - -let clash_error sn n1 n2 = - errorlabstrm "clash_module_message" - (str ("There are two Coq modules with ML name " ^ sn ^" :") ++ - fnl () ++ str (" "^(string_of_dirpath n1)) ++ - fnl () ++ str (" "^(string_of_dirpath n2)) ++ - fnl () ++ str "This is not allowed in ML. Please do some renaming first.") - -let check_r m sm r = - let rlm = long_module r in - let rsm = List.hd (repr_dirpath rlm) in - if (String.capitalize (string_of_id rsm)) = sm && m <> rlm - then clash_error sm m rlm - -let check_decl m sm = function - | Dterm (r,_,_) -> check_r m sm r - | Dtype (r,_,_) -> check_r m sm r - | Dind (kn,_) -> check_r m sm (IndRef (kn,0)) - | DcustomTerm (r,_) -> check_r m sm r - | DcustomType (r,_) -> check_r m sm r - | Dfix(rv,_,_) -> Array.iter (check_r m sm) rv - -(* [check_one_module] checks that no module names in [l] clashes with [m]. *) - -let check_one_module m l = - let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in - List.iter (check_decl m sm) l - -(* [check_modules] checks if there are conflicts within the set [m] - of modules dirpath. *) - -let check_modules m = - let map = ref Idmap.empty in - Dirset.iter - (fun m -> - let sm = String.capitalize (string_of_id (snd (split_dirpath m))) in - let idm = id_of_string sm in - try - let m' = Idmap.find idm !map in clash_error sm m m' - with Not_found -> map := Idmap.add idm m !map) m +let rec extract_msb v all loc = function + | [] -> [] + | (l,SEBconst cb) :: msb -> + (try + let vl,recd,msb = factor_fix l cb msb in + let vkn = Array.map (make_kn loc empty_dirpath) vl in + let vkn = Array.map long_kn vkn in + let ms = extract_msb v all loc msb in + let b = array_exists (in_kn v) vkn in + if all || b then + let d = extract_fixpoint !cur_env vkn recd in + if (not b) && (logical_decl d) then ms + else begin get_decl_references v d; (l,SEdecl d) :: ms end + else ms + with Impossible -> + let ms = extract_msb v all loc msb in + let kn = make_kn loc empty_dirpath l in + let b = in_kn v kn in + if all || b then + let d = extract_constant !cur_env kn cb in + if (not b) && (logical_decl d) then ms + else begin get_decl_references v d; (l,SEdecl d) :: ms end + else ms) + | (l,SEBmind mib) :: msb -> + let ms = extract_msb v all loc msb in + let kn = make_kn loc empty_dirpath l in + let b = in_kn v kn in + if all || b then + let d = Dind (kn, extract_inductive !cur_env kn) in + if (not b) && (logical_decl d) then ms + else begin get_decl_references v d; (l,SEdecl d) :: ms end + else ms + | (l,SEBmodule mb) :: msb -> + let ms = extract_msb v all loc msb in + let loc = MPdot (loc,l) in + if all || in_mp v loc then + (l,SEmodule (extract_module v true mb)) :: ms + else ms + | (l,SEBmodtype mtb) :: msb -> + let ms = extract_msb v all loc msb in + let kn = make_kn loc empty_dirpath l in + if all || in_kn v kn then + (l,SEmodtype (extract_mtb v mtb)) :: ms + else ms + +and extract_meb v all = function + | MEBident mp -> MEident mp + | MEBapply (meb, meb',_) -> + MEapply (extract_meb v true meb, extract_meb v true meb') + | MEBfunctor (mbid, mtb, meb) -> + MEfunctor (mbid, extract_mtb v mtb, extract_meb v true meb) + | MEBstruct (msid, msb) -> + MEstruct (msid, extract_msb v all (MPself msid) msb) + +and extract_module v all mb = + { ml_mod_expr = option_app (extract_meb v all) mb.mod_expr; + ml_mod_type = (match mb.mod_user_type with + | None -> extract_mtb v mb.mod_type + | Some mtb -> extract_mtb v mtb); + ml_mod_equiv = mb.mod_equiv } + +and extract_mtb v = function + | MTBident kn -> MTident kn + | MTBfunsig (mbid, mtb, mtb') -> + MTfunsig (mbid, extract_mtb v mtb, extract_mtb v mtb') + | MTBsig (msid, msig) -> + MTsig (msid, extract_msig v (MPself msid) msig) -(*s Recursive computation of the global references to extract. - We use a set of functions visiting the extracted objects in - a depth-first way ([visit_type], [visit_ast] and [visit_decl]). - We maintain an (imperative) structure [extracted_env] containing - the set of already visited references and the list of - references to extract. The entry point is the function [visit_reference]: - it first normalizes the reference, and then check it has already been - visisted; if not, it adds it to the set of visited references, then - recursively traverses its extraction and finally adds it to the - list of references to extract. *) - -type extracted_env = { - mutable visited : Refset.t; - mutable to_extract : global_reference list; - mutable modules : Dirset.t -} - -let empty () = - { visited = ml_extractions (); - to_extract = []; - modules = Dirset.empty } - -let rec visit_reference m eenv r = - let r' = match r with - | ConstructRef ((sp,_),_) -> IndRef (sp,0) - | IndRef (sp,i) -> if i = 0 then r else IndRef (sp,0) - | _ -> r - in - if not (Refset.mem r' eenv.visited) then begin - (* we put [r'] in [visited] first to avoid loops in inductive defs - and in module extraction *) - eenv.visited <- Refset.add r' eenv.visited; - if m then begin - let m_name = Declare.library_part r' in - if not (Dirset.mem m_name eenv.modules) then begin - eenv.modules <- Dirset.add m_name eenv.modules; - List.iter (visit_reference m eenv) (module_contents m_name) +and extract_msig v loc = function + | [] -> [] + | (l,SPBconst cb) :: msig -> + let kn = make_kn loc empty_dirpath l in + let s = extract_constant_spec !cur_env kn cb in + if logical_spec s then extract_msig v loc msig + else begin + get_spec_references v s; + (l,Spec s) :: (extract_msig v loc msig) end - end; - visit_decl m eenv (extract_declaration r); - eenv.to_extract <- r' :: eenv.to_extract - end - -(* and visit_fixpoint m eenv r = - match (kind_of_term (constant_value (Global.env()) (kn_of_r r))) with - | Fix (_,(f,_,_)) -> - (try - let d = dirpath (sp_of_global None r) in - let v = Array.map (fun id -> locate (make_qualid d id)) f in *) - -and visit_type m eenv t = - let rec visit = function - | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l - | Tarr (t1,t2) -> visit t1; visit t2 - | Tvar _ | Tdummy | Tunknown | Tcustom _ -> () - | Tmeta _ | Tvar' _ -> assert false - in - visit t - -and visit_ast m eenv a = - let rec visit = function - | MLglob r -> visit_reference m eenv r - | MLapp (a,l) -> visit a; List.iter visit l - | MLlam (_,a) -> visit a - | MLletin (_,a,b) -> visit a; visit b - | MLcons (r,l) -> visit_reference m eenv r; List.iter visit l - | MLcase (a,br) -> - visit a; - Array.iter (fun (r,_,a) -> visit_reference m eenv r; visit a) br - | MLfix (_,_,l) -> Array.iter visit l - | MLcast (a,t) -> visit a; visit_type m eenv t - | MLmagic a -> visit a - | MLrel _ | MLdummy | MLexn _ | MLcustom _ -> () - in - visit a - -and visit_inductive m eenv ind = - let visit_constructor tl = List.iter (visit_type m eenv) tl in - let visit_packet p = Array.iter visit_constructor p.ip_types in - Array.iter visit_packet ind.ind_packets - -and visit_decl m eenv = function - | Dind (_,ind) -> visit_inductive m eenv ind - | Dtype (_,_,t) -> visit_type m eenv t - | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t - | Dfix (_,c,t) -> - Array.iter (visit_ast m eenv) c; - Array.iter (visit_type m eenv) t - | _ -> () - -(*s Recursive extracted environment for a list of reference: we just - iterate [visit_reference] on the list, starting with an empty - extracted environment, and we return the reversed list of - references in the field [to_extract], and the visited_modules in - case of recursive module extraction *) - -let extract_env rl = - let eenv = empty () in - List.iter (visit_reference false eenv) rl; - List.rev eenv.to_extract - -let modules_extract_env m = - let eenv = empty () in - eenv.modules <- Dirset.singleton m; - List.iter (visit_reference true eenv) (module_contents m); - eenv.modules, List.rev eenv.to_extract - -(* let toplevel_contents () = - segment_contents (contents_after None) + | (l,SPBmind cb) :: msig -> + let kn = make_kn loc empty_dirpath l in + let s = Sind (kn, extract_inductive !cur_env kn) in + if logical_spec s then extract_msig v loc msig + else begin + get_spec_references v s; + (l,Spec s) :: (extract_msig v loc msig) + end + | (l,SPBmodule {msb_modtype=mtb}) :: msig -> + (l,Smodule (extract_mtb v mtb)) :: (extract_msig v loc msig) + | (l,SPBmodtype mtb) :: msig -> + (l,Smodtype (extract_mtb v mtb)) :: (extract_msig v loc msig) -let extract_env rl = - let modules = List.rev (loaded_libraries ()) in - let toplevel_list = toplevel_contents () in - let modules_list = *) +(* Searching one [ml_decl] in a [ml_structure] by its [kernel_name] *) +let get_decl_in_structure r struc = + try + let kn = kn_of_r r in + let base_mp,ll = labels_of_kn (long_kn kn) in + if not (at_toplevel base_mp) then error_not_visible r; + let sel = List.assoc base_mp struc in + let rec go ll sel = match ll with + | [] -> assert false + | l :: ll -> + match List.assoc l sel with + | SEdecl d -> d + | SEmodtype m -> assert false + | SEmodule m -> + match m.ml_mod_expr with + | Some (MEstruct (_,sel)) -> go ll sel + | _ -> error_not_visible r + in go ll sel + with Not_found -> assert false (*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]. *) -let decl_of_refs refs = List.map extract_declaration (extract_env refs) - -let print_user_extract r = - msgnl (str "User defined extraction:" ++ - spc () ++ str (find_ml_extraction r) ++ fnl ()) +let unpack = function MEstruct (_,sel) -> sel | _ -> assert false -let decl_in_r r0 = function - | Dterm (r,_,_) -> r = r0 - | Dtype (r,_,_) -> r = r0 - | Dind (kn, _) -> kn = kn_of_r r0 - | DcustomTerm (r,_) -> r = r0 - | DcustomType (r,_) -> r = r0 - | Dfix (rv,_,_) -> array_exists ((=) r0) rv +let mono_environment refs = + let l = environment_until None in + init_env l; + let v = + let kns = List.fold_right (fun r -> KNset.add (kn_of_r r)) refs KNset.empty + in let add_mp kn = MPset.union (prefixes_mp (modpath kn)) + in { kn = kns; mp = KNset.fold add_mp kns MPset.empty } + in + List.rev_map (fun (mp,m) -> mp, unpack (extract_meb v false m)) (List.rev l) -let extraction qid = +let extraction qid = + if is_something_opened () then error_section (); let r = Nametab.global qid in - if is_ml_extraction r then - print_user_extract r - else + if is_custom r then + msgnl (str "User defined extraction:" ++ spc () ++ + str (find_custom r) ++ fnl ()) + else begin let prm = { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let decls = optimize prm (decl_of_refs [r]) in - let d = list_last decls in - let d = if (decl_in_r r d) then d - else List.find (decl_in_r r) decls in - set_keywords (); - create_mono_renamings decls; - msgnl (pp_decl () d) + let kn = kn_of_r r in + let struc = optimize_struct prm None (mono_environment [r]) in + let d = get_decl_in_structure r struc in + print_one_decl struc (long_mp (modpath kn)) d; + reset_tables () + end (*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. *) let mono_extraction (f,m) vl = + if is_something_opened () then error_section (); let refs = List.map Nametab.global vl in let prm = {modular=false; mod_name = m; to_appear= refs} in - let decls = decl_of_refs refs in - let decls = add_ml_decls prm decls in - let decls = optimize prm decls in - extract_to_file f prm decls + let struc = optimize_struct prm None (mono_environment refs) in + print_structure_to_file f prm struc; + reset_tables () let extraction_rec = mono_extraction (None,id_of_string "Main") (*s Extraction to a file (necessarily recursive). - The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn]. - We just call [extract_to_file] on the saturated environment. *) + The vernacular command is + \verb!Extraction "file"! [qualid1] ... [qualidn].*) let lang_suffix () = match lang () with - | Ocaml -> ".ml" - | Haskell -> ".hs" - | Scheme -> ".scm" + | Ocaml -> ".ml",".mli" + | Haskell -> ".hs",".hi" + | Scheme -> ".scm",".scm" | Toplevel -> assert false let filename f = - let s = lang_suffix () in + let s,s' = lang_suffix () in if Filename.check_suffix f s then - Some f,id_of_string (Filename.chop_suffix f s) - else Some (f^s),id_of_string f - -let toplevel_error () = - errorlabstrm "toplevel_extraction_language" - (str "Toplevel pseudo-ML language cannot be used outside Coq toplevel." - ++ fnl () ++ - str "You should use Extraction Language Ocaml or Haskell before.") + 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 toplevel_error () + if lang () = Toplevel then error_toplevel () else mono_extraction (filename f) vl (*s Extraction of a module. The vernacular command is \verb!Extraction Module! [M]. *) -let decl_in_m m = function - | Dterm (r,_,_) -> m = long_module r - | Dtype (r,_,_) -> m = long_module r - | Dind (kn,_) -> m = long_module (IndRef (kn,0)) - | DcustomTerm (r,_) -> m = long_module r - | DcustomType (r,_) -> m = long_module r - | Dfix (rv,_,_) -> m = long_module rv.(0) - let module_file_name m = match lang () with - | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml" - | Haskell -> (String.capitalize (string_of_id m)) ^ ".hs" + | 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 scheme_error () = - errorlabstrm "scheme_extraction_language" - (str "No Scheme modular extraction available yet." ++ fnl ()) +let dir_module_of_id m = + try Nametab.full_name_module (make_short_qualid m) + with Not_found -> error_unknown_module m let extraction_module m = + if is_something_opened () then error_section (); match lang () with - | Toplevel -> toplevel_error () - | Scheme -> scheme_error () + | Toplevel -> error_toplevel () + | Scheme -> error_scheme () | _ -> let dir_m = dir_module_of_id m in - let f = module_file_name m in + let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in + let l = environment_until (Some dir_m) in + init_env l; + let mp,meb = list_last l in + let struc = [mp, unpack (extract_meb v true meb)] in + let extern_decls = + let filter kn l = + if base_mp (modpath kn) = mp then l else r_of_kn !cur_env kn :: l + in extract_env (KNset.fold filter v.kn []) + in let prm = {modular=true; mod_name=m; to_appear=[]} in - let rl = module_contents dir_m in - let decls = optimize prm (decl_of_refs rl) in - let decls = add_ml_decls prm decls in - check_one_module dir_m decls; - let decls = List.filter (decl_in_m dir_m) decls in - extract_to_file (Some f) prm decls + let struc = optimize_struct prm (Some extern_decls) struc in + print_structure_to_file (Some (module_file_name m)) prm struc; + reset_tables () (*s Recursive Extraction of all the modules [M] depends on. The vernacular command is \verb!Recursive Extraction Module! [M]. *) let recursive_extraction_module m = + if is_something_opened () then error_section (); match lang () with - | Toplevel -> toplevel_error () - | Scheme -> scheme_error () + | Toplevel -> error_toplevel () + | Scheme -> error_scheme () | _ -> let dir_m = dir_module_of_id m in - let modules,refs = modules_extract_env dir_m in - check_modules modules; + let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in + let l = environment_until (Some dir_m) in + init_env l; + let struc = + let select l (mp,meb) = + if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l + in List.fold_left select [] (List.rev l) + in let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let decls = optimize dummy_prm (decl_of_refs refs) in - let decls = add_ml_decls dummy_prm decls in - Dirset.iter - (fun m -> - let short_m = snd (split_dirpath m) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - let decls = List.filter (decl_in_m m) decls in - if decls <> [] then extract_to_file (Some f) prm decls) - modules + let struc = optimize_struct dummy_prm None struc in + let rec print = function + | [] -> () + | (MPfile dir, sel) as e :: l -> + let short_m = snd (split_dirpath dir) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + print_structure_to_file (Some f) prm [e]; + print l + | _ -> assert false + in print struc; + reset_tables () + + + + + diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 1dcd9abef..625afc7d1 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -18,20 +18,3 @@ val extraction_rec : reference list -> unit val extraction_file : string -> reference list -> unit val extraction_module : identifier -> unit val recursive_extraction_module : identifier -> unit - -(* debug modules -- en cours *) - -open Declarations - -val cur_env : Environ.env ref -val mp_short : module_path ref -val toplevel : unit -> module_expr_body -val environment_until : dir_path option -> (dir_path * module_expr_body) list -val print_seb : label * structure_elem_body -> unit -val print_msb : module_structure_body -> unit -val print_module : label -> module_body -> unit -val print_meb : module_expr_body -> unit -val print_modtype : label -> module_type_body -> unit -val print_sign : module_signature_body -> unit -val print_spec : label * specification_body -> unit -val print_all : unit -> unit diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 363d6c177..c676c26c2 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -37,7 +37,7 @@ let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) -let is_axiom kn = (Global.lookup_constant kn).const_body = None +let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None (*S Generation of flags and signatures. *) @@ -149,7 +149,6 @@ let parse_ind_args si args relmax = let rec extract_type env db j c args = match kind_of_term (whd_betaiotazeta c) with - | Var _ -> error_section () | App (d, args') -> (* We just accumulate the arguments. *) extract_type env db j d (Array.to_list args' @ args) @@ -183,31 +182,32 @@ let rec extract_type env db j c args = if n > List.length db then Tunknown else let n' = List.nth db (n-1) in if n' = 0 then Tunknown else Tvar n') - | Const kn when is_ml_extraction (ConstRef kn) -> - assert (args = []); - Tglob (ConstRef kn,[]) - | Const kn when is_axiom kn -> - (* There are two kinds of informative axioms here, *) - (* - the types that should be realized via [Extract Constant] *) - (* - the type schemes that are not realizable (yet). *) - if args = [] then error_axiom (ConstRef kn) - else error_axiom_scheme (ConstRef kn) - | Const kn -> - let body = constant_value env kn in - let mlt1 = extract_type env db j (applist (body, args)) [] in - (match mlt_env (ConstRef kn) with - | Some mlt -> - if mlt = Tdummy then Tdummy - else - let s = type_sign env (constant_type env kn) in - let mlt2 = extract_type_app env db (ConstRef kn,s) args in - (* ML type abbreviation behave badly with respect to Coq *) - (* reduction. Try to find the shortest correct answer. *) - if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1 - | None -> mlt1) + | Const kn -> + let kn = long_kn kn in + let r = ConstRef kn in + if is_custom r then Tglob (r,[]) + else if is_axiom env kn then + (* There are two kinds of informative axioms here, *) + (* - the types that should be realized via [Extract Constant] *) + (* - the type schemes that are not realizable (yet). *) + if args = [] then error_axiom r else error_axiom_scheme r + else + let body = constant_value env kn in + let mlt1 = extract_type env db j (applist (body, args)) [] in + (match mlt_env env r with + | Some mlt -> + if mlt = Tdummy then Tdummy + else + let s = type_sign env (constant_type env kn) in + let mlt2 = extract_type_app env db (r,s) args in + (* ML type abbreviation behave badly with respect to Coq *) + (* reduction. Try to find the shortest correct answer. *) + if type_eq (mlt_env env) mlt1 mlt2 then mlt2 else mlt1 + | None -> mlt1) | Ind ((kn,i) as ip) -> - let s = (extract_inductive kn).ind_packets.(i).ip_sign in - extract_type_app env db (IndRef ip,s) args + let kn = long_kn kn in + let s = (extract_ind env kn).ind_packets.(i).ip_sign in + extract_type_app env db (IndRef (kn,i),s) args | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false @@ -259,15 +259,14 @@ and extract_type_scheme env db c p = (*S Extraction of an inductive type. *) -and extract_inductive kn = +and extract_ind env kn = (* kn is supposed to be in long form *) try lookup_ind kn with Not_found -> - add_recursors kn; - let env = Global.env () in - let (mib,mip) = Global.lookup_inductive (kn,0) in + let mib = Environ.lookup_mind kn env in (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) - let npar = mip.mind_nparams in - let epar = push_rel_context mip.mind_params_ctxt env in + let mip0 = mib.mind_packets.(0) in + let npar = mip0.mind_nparams in + let epar = push_rel_context mip0.mind_params_ctxt env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = @@ -276,7 +275,12 @@ and extract_inductive kn = let b = mip.mind_sort <> (Prop Null) in let s,v = if b then type_sign_vl env mip.mind_nf_arity else [],[] in let t = Array.make (Array.length mip.mind_nf_lc) [] in - { ip_logical = (not b); ip_sign = s; ip_vars = v; ip_types = t }) + { ip_typename = mip.mind_typename; + ip_consnames = mip.mind_consnames; + ip_logical = (not b); + ip_sign = s; + ip_vars = v; + ip_types = t }) mib.mind_packets in add_ind kn {ind_info = Standard; ind_nparams = npar; ind_packets = packets}; @@ -305,15 +309,17 @@ and extract_inductive kn = if p.ip_logical then raise (I Standard); if Array.length p.ip_types <> 1 then raise (I Standard); let typ = p.ip_types.(0) in - let l = List.filter (type_neq mlt_env Tdummy) typ in + let l = List.filter (type_neq (mlt_env env) Tdummy) typ in if List.length l = 1 && not (type_mem_kn kn (List.hd l)) then raise (I Singleton); - if l = [] then raise (I Standard); + if l = [] then raise (I Standard); + let ip = (kn, 0) in + if is_custom (IndRef ip) then raise (I Standard); let projs = - try (find_structure (kn,0)).s_PROJ + try (find_structure ip).s_PROJ with Not_found -> raise (I Standard); in - let s = List.map (type_neq mlt_env Tdummy) typ in + let s = List.map (type_neq (mlt_env env) Tdummy) typ in let check (_,o) = match o with | None -> raise (I Standard) | Some kn -> ConstRef kn @@ -345,14 +351,14 @@ and extract_type_cons env db dbmap c i = (*s Recording the ML type abbreviation of a Coq type scheme constant. *) -and mlt_env r = match r with +and mlt_env env r = match r with | ConstRef kn -> + let kn = long_kn kn in (try match lookup_term kn with | Dtype (_,vl,mlt) -> Some mlt | _ -> None with Not_found -> - let env = Global.env() in - let cb = Global.lookup_constant kn in + let cb = Environ.lookup_constant kn env in let typ = cb.const_type in match cb.const_body with | None -> None @@ -367,19 +373,22 @@ and mlt_env r = match r with | _ -> None)) | _ -> None -let type_expand = type_expand mlt_env -let type_neq = type_neq mlt_env -let type_to_sign = type_to_sign mlt_env -let type_expunge = type_expunge mlt_env +let type_expand env = type_expand (mlt_env env) +let type_neq env = type_neq (mlt_env env) +let type_to_sign env = type_to_sign (mlt_env env) +let type_expunge env = type_expunge (mlt_env env) (*s Extraction of the type of a constant. *) -let record_constant_type kn = +let record_constant_type env kn opt_typ = + let kn = long_kn kn in try lookup_type kn with Not_found -> - let env = Global.env () in - let mlt = extract_type env [] 1 (constant_type env kn) [] in - let schema = (type_maxvar mlt, mlt) + let typ = match opt_typ with + | None -> constant_type env kn + | Some typ -> typ + in let mlt = extract_type env [] 1 typ [] + in let schema = (type_maxvar mlt, mlt) in add_type kn schema; schema (*S Extraction of a term. *) @@ -425,23 +434,23 @@ let rec extract_term env mle mlt c args = let mle' = Mlenv.push_std_type mle Tdummy in ast_pop (extract_term env' mle' mlt c2 args') | Const kn -> - extract_cst_app env mle mlt kn args - | Construct cp -> - extract_cons_app env mle mlt cp args + extract_cst_app env mle mlt (long_kn kn) args + | Construct ((kn,i),j) -> + extract_cons_app env mle mlt (((long_kn kn),i),j) args | Rel n -> (* As soon as the expected [mlt] for the head is known, *) (* we unify it with an fresh copy of the stored type of [Rel n]. *) let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) in extract_app env mle mlt extract_rel args - | Case ({ci_ind=ip},_,c0,br) -> + | Case ({ci_ind=(kn,i)},_,c0,br) -> + let ip = long_kn kn, i in extract_app env mle mlt (extract_case env mle (ip,c0,br)) args | Fix ((_,i),recd) -> extract_app env mle mlt (extract_fix env mle i recd) args | CoFix (i,recd) -> extract_app env mle mlt (extract_fix env mle i recd) args | Cast (c, _) -> extract_term env mle mlt c args - | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false - | Var _ -> error_section () + | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) @@ -477,8 +486,8 @@ and make_mlargs env e s args typs = and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) - let nb,t = record_constant_type kn in - let schema = nb, type_expand t in + let nb,t = record_constant_type env kn None in + let schema = nb, type_expand env t in (* Then the expected type of this constant. *) let metas = List.map new_meta args in let type_head = type_recomp (metas,mlt) in @@ -487,7 +496,7 @@ and extract_cst_app env mle mlt kn args = let h = MLglob (ConstRef kn) in put_magic (type_recomp (metas,mlt), instantiation schema) h in (* Now, the extraction of the arguments. *) - let s = type_to_sign (snd schema) in + let s = type_to_sign env (snd schema) in let ls = List.length s in let la = List.length args in let mla = make_mlargs env mle s args metas in @@ -519,11 +528,11 @@ and extract_cst_app env mle mlt kn args = and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) - let mi = extract_inductive kn in + let mi = extract_ind env kn in let params_nb = mi.ind_nparams in let oi = mi.ind_packets.(i) in let nb_tvars = List.length oi.ip_vars - and types = List.map type_expand oi.ip_types.(j-1) in + and types = List.map (type_expand env) oi.ip_types.(j-1) in let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvars) in let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in let type_cons = instantiation (nb_tvars, type_cons) in @@ -562,11 +571,10 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = and extract_case env mle ((kn,i) as ip,c,br) mlt = (* [br]: bodies of each branch (in functional form) *) (* [ni]: number of arguments without parameters in each branch *) - let ni = mis_constr_nargs ip in + let ni = mis_constr_nargs_env env ip in let br_size = Array.length br in assert (Array.length ni = br_size); - if br_size = 0 then begin - add_recursors kn; + if br_size = 0 then begin MLexn "absurd case" end else (* [c] has an inductive type, and is not a type scheme type. *) @@ -576,7 +584,6 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = begin (* Logical singleton case: *) (* [match c with C i j k -> t] becomes [t'] *) - add_recursors kn; assert (br_size = 1); let s = iterate (fun l -> false :: l) ni.(0) [] in let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni.(0) mlt in @@ -584,7 +591,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = snd (case_expunge s e) end else - let mi = extract_inductive kn in + let mi = extract_ind env kn in let params_nb = mi.ind_nparams in let oi = mi.ind_packets.(i) in let metas = Array.init (List.length oi.ip_vars) new_meta in @@ -594,7 +601,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (* The extraction of each branch. *) let extract_branch i = (* The types of the arguments of the corresponding constructor. *) - let f t = type_subst_vect metas (type_expand t) in + let f t = type_subst_vect metas (type_expand env t) in let l = List.map f oi.ip_types.(i) in (* Extraction of the branch (in functional form). *) let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in @@ -618,13 +625,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = (*s Extraction of a (co)-fixpoint. *) and extract_fix env mle i (fi,ti,ci as recd) mlt = - let n = Array.length fi in let env = push_rec_types recd env in - let metas = Array.map (fun _ -> new_meta ()) fi in - let magic = needs_magic (mlt, metas.(i)) in + let metas = Array.map new_meta fi in + metas.(i) <- mlt; let mle = Array.fold_left Mlenv.push_type mle metas in let ei = array_map2 (extract_maybe_term env mle) metas ci in - put_magic_if magic (MLfix (i, Array.map id_of_name fi, ei)) + MLfix (i, Array.map id_of_name fi, ei) (*S ML declarations. *) @@ -646,72 +652,125 @@ let rec decomp_lams_eta env c t = (*s From a constant to a ML declaration. *) -let extract_constant kn r = - let env = Global.env() in - let cb = Global.lookup_constant kn in +let extract_std_constant env kn body typ = + (* Decomposing the top level lambdas of [body]. *) + let rels,c = decomp_lams_eta env body typ in + (* The lambdas names. *) + let ids = List.map (fun (n,_) -> id_of_name n) rels in + (* The according Coq environment. *) + let env = push_rels_assum rels env in + (* The ML part: *) + reset_meta_count (); + (* The short type [t] (i.e. possibly with abbreviations). *) + let t = snd (record_constant_type env kn (Some typ)) in + (* The real type [t']: without head lambdas, expanded, *) + (* and with [Tvar] translated to [Tvar'] (not instantiable). *) + let l,t' = type_decomp (type_expand env (var2var' t)) in + let s = List.map ((<>) Tdummy) l in + (* The initial ML environment. *) + let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in + (* The real extraction: *) + let e = extract_term env mle t' c [] in + (* Expunging term and type from dummy lambdas. *) + term_expunge s (ids,e), type_expunge env t + +let extract_fixpoint env vkn (fi,ti,ci) = + let n = Array.length vkn in + let types = Array.make n Tdummy + and terms = Array.make n MLdummy in + (* for replacing recursive calls [Rel ..] by the corresponding [Const]: *) + let sub = List.rev_map mkConst (Array.to_list vkn) in + for i = 0 to n-1 do + if sort_of env ti.(i) <> InProp then begin + let e,t = extract_std_constant env vkn.(i) (substl sub ci.(i)) ti.(i) in + terms.(i) <- e; + types.(i) <- t; + end + done; + Dfix (Array.map (fun kn -> ConstRef kn) vkn, terms, types) + +let extract_constant env kn cb = + let kn = long_kn kn in + let r = ConstRef kn in let typ = cb.const_type in match cb.const_body with | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with | (Info,TypeScheme) -> - if isSort typ then error_axiom r + if isSort typ then + if is_custom (long_r r) then Dtype (r, [], Tunknown) + else error_axiom r else error_axiom_scheme r - | (Info,Default) -> error_axiom r + | (Info,Default) -> + if is_custom (long_r r) then + let t = snd (record_constant_type env kn (Some typ)) in + Dterm (r, MLexn "axiom!", type_expunge env t) + else error_axiom r | (Logic,TypeScheme) -> warning_axiom r; Dtype (r, [], Tdummy) | (Logic,Default) -> warning_axiom r; Dterm (r, MLdummy, Tdummy)) - | Some l_body -> + | Some body -> (match flag_of_type env typ with | (Logic, Default) -> Dterm (r, MLdummy, Tdummy) | (Logic, TypeScheme) -> Dtype (r, [], Tdummy) | (Info, Default) -> - let body = Declarations.force l_body in - (* Decomposing the top level lambdas of [body]. *) - let rels,c = decomp_lams_eta env body typ in - (* The lambdas names. *) - let ids = List.map (fun (n,_) -> id_of_name n) rels in - (* The according Coq environment. *) - let env = push_rels_assum rels env in - (* The ML part: *) - reset_meta_count (); - (* The short type [t] (i.e. possibly with abbreviations). *) - let t = snd (record_constant_type kn) in - (* The real type [t']: without head lambdas, expanded, *) - (* and with [Tvar] translated to [Tvar'] (not instantiable). *) - let l,t' = type_decomp (type_expand (var2var' t)) in - let s = List.map ((<>) Tdummy) l in - (* The initial ML environment. *) - let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in - (* The real extraction: *) - let e = extract_term env mle t' c [] in - (* Expunging term and type from dummy lambdas. *) - Dterm (r, term_expunge s (ids,e), type_expunge t) + let e,t = extract_std_constant env kn (force body) typ in + Dterm (r,e,t) | (Info, TypeScheme) -> - let body = Declarations.force l_body in let s,vl = type_sign_vl env typ in let db = db_from_sign s in - let t = extract_type_scheme env db body (List.length s) in - Dtype (r, vl, t)) - -let extract_constant_cache kn r = - try lookup_term kn - with Not_found -> - let d = extract_constant kn r - in add_term kn d; d - -let extract_inductive_declaration kn = - let ind = extract_inductive kn in - let f l = List.filter (type_neq Tdummy) l in + let t = extract_type_scheme env db (force body) (List.length s) + in Dtype (r, vl, t)) + +let extract_constant_spec env kn cb = + let kn = long_kn kn in + let r = ConstRef kn in + let typ = cb.const_type in + match flag_of_type env typ with + | (Logic, TypeScheme) -> Stype (r, [], Some Tdummy) + | (Logic, Default) -> Sval (r, Tdummy) + | (Info, TypeScheme) -> + let s,vl = type_sign_vl env typ in + (match cb.const_body with + | None -> Stype (r, vl, None) + | Some body -> + let db = db_from_sign s in + let t = extract_type_scheme env db (force body) (List.length s) + in Stype (r, vl, Some t)) + | (Info, Default) -> + let t = snd (record_constant_type env kn (Some typ)) in + Sval (r, type_expunge env t) + +let extract_inductive env kn = + let ind = extract_ind env kn in + add_recursors env kn; + let f l = List.filter (type_neq env Tdummy) l in let packets = Array.map (fun p -> { p with ip_types = Array.map f p.ip_types }) ind.ind_packets - in Dind (kn,{ ind with ind_packets = packets }) + in { ind with ind_packets = packets } (*s From a global reference to a ML declaration. *) -let extract_declaration r = match r with - | ConstRef kn -> extract_constant_cache kn r - | IndRef (kn,_) -> extract_inductive_declaration kn - | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn - | VarRef kn -> error_section () +let extract_declaration env r = match r with + | ConstRef kn -> extract_constant env kn (Environ.lookup_constant kn env) + | IndRef (kn,_) -> let kn = long_kn kn in Dind (kn, extract_inductive env kn) + | ConstructRef ((kn,_),_) -> + let kn = long_kn kn in 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 cb.const_type with + | (Logic,_) -> Logical + | (Info,TypeScheme) -> Type + | (Info,Default) -> Term + + + + + diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index 268a68692..c9654d25c 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -10,10 +10,28 @@ (*s Extraction from Coq terms to Miniml. *) +open Names +open Term +open Declarations +open Environ open Libnames open Miniml +val extract_constant : env -> kernel_name -> constant_body -> ml_decl + +val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec + +val extract_fixpoint : + env -> kernel_name 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 : global_reference -> ml_decl +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 diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 81ec48767..aac7f8778 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -15,6 +15,7 @@ open Util open Names open Nameops open Libnames +open Table open Miniml open Mlutil open Ocaml @@ -30,18 +31,22 @@ let keywords = Idset.empty let preamble prm used_modules (mldummy,tdummy,tunknown) = - let m = String.capitalize (string_of_id prm.mod_name) in - str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ + let pp_mp = function + | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) + | _ -> assert false + in + str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () + ++ fnl() ++ str "import qualified Prelude" ++ fnl() ++ - Idset.fold - (fun m s -> str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s) - used_modules (mt ()) ++ fnl() - ++ + prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules + ++ fnl () ++ (if mldummy then str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl () ++ fnl() else mt()) +let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" + let pp_abst = function | [] -> (mt ()) | l -> (str "\\" ++ @@ -54,7 +59,9 @@ let pr_lower_id id = pr_id (lowercase_id id) module Make = functor(P : Mlpp_param) -> struct -let pp_global r = P.pp_global r +let local_mp = ref initial_path + +let pp_global r = P.pp_global !local_mp r let empty_env () = [], P.globals() (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses @@ -111,7 +118,7 @@ let rec pp_expr par env args = hv 0 (pp_par par (hv 0 - (hov 2 (str "let" ++ pp_id ++ str " = " ++ pp_a1) ++ + (hov 5 (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++ spc () ++ str "in") ++ spc () ++ hov 0 pp_a2)) | MLglob r -> @@ -139,7 +146,6 @@ let rec pp_expr par env args = str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLcast (a,t) -> pp_expr par env args a | MLmagic a -> pp_expr par env args a - | MLcustom s -> str s and pp_pat env pv = let pp_one_pat (name,ids,t) = @@ -180,20 +186,20 @@ and pp_function env f t = let pp_comment s = str "-- " ++ s ++ fnl () let pp_logical_ind ip packet = - pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++ + pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc Printer.pr_global + prvect_with_sep spc pr_global (Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) let pp_singleton kn packet = let l = rename_tvars keywords packet.ip_vars in let l' = List.rev l in - hov 0 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++ + hov 2 (str "type " ++ pp_global (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 () ++ pp_comment (str "singleton inductive, whose constructor was " ++ - Printer.pr_global (ConstructRef ((kn,0),1)))) + pr_global (ConstructRef ((kn,0),1)))) let pp_one_ind ip pl cv = let pl = rename_tvars keywords pl in @@ -215,40 +221,60 @@ let pp_one_ind ip pl cv = prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv))) -let rec pp_ind kn i ind = - if i >= Array.length ind.ind_packets then mt () +let rec pp_ind first kn i ind = + if i >= Array.length ind.ind_packets then + if first then mt () else fnl () else let ip = (kn,i) in let p = ind.ind_packets.(i) in - if p.ip_logical then - pp_logical_ind ip p ++ pp_ind kn (i+1) ind + if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind else - pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ pp_ind kn (i+1) ind - + if p.ip_logical then + pp_logical_ind ip p ++ pp_ind first kn (i+1) ind + else + pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++ + pp_ind false kn (i+1) ind + (*s Pretty-printing of a declaration. *) -let pp_decl = function - | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton kn i.ind_packets.(0) - | Dind (kn,i) -> hov 0 (pp_ind kn 0 i) +let pp_decl mp = + local_mp := mp; + 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) | Dtype (r, l, t) -> - let l = rename_tvars keywords l in - let l' = List.rev l in - hov 0 (str "type " ++ pp_global r ++ spc () ++ + if is_inline_custom r then mt () + else + let l = rename_tvars keywords l in + let l' = List.rev l in + hov 2 (str "type " ++ pp_global r ++ spc () ++ prlist_with_sep (fun () -> (str " ")) pr_id l ++ (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++ - pp_type false l' t ++ fnl ()) + pp_type false l' t ++ fnl () ++ fnl ()) | Dfix (rv, defs,_) -> let ppv = Array.map pp_global rv in - (prlist_with_sep (fun () -> fnl () ++ fnl ()) - (fun (pi,ti) -> pp_function (empty_env ()) pi ti) - (List.combine (Array.to_list ppv) (Array.to_list defs)) ++ fnl ()) + prlist_with_sep (fun () -> fnl () ++ fnl ()) + (fun (pi,ti) -> pp_function (empty_env ()) pi ti) + (List.combine (Array.to_list ppv) (Array.to_list defs)) + ++ fnl () ++ fnl () | Dterm (r, a, _) -> - hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ()) - | DcustomTerm (r,s) -> - hov 0 (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ()) - | DcustomType (r,s) -> - hov 0 (str "type " ++ pp_global r ++ str " = " ++ str s ++ fnl ()) + if is_inline_custom r then mt () + else + hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ()) + +let pp_structure_elem mp = function + | (l,SEdecl d) -> pp_decl mp 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 diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index be60cf1c1..062b236ca 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -14,6 +14,7 @@ open Miniml val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds +val preamble : + extraction_params -> module_path list -> 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 6f56f36e3..235847f32 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -56,6 +56,8 @@ type inductive_info = Record | Singleton | Coinductive | Standard *) type ml_ind_packet = { + ip_typename : identifier; + ip_consnames : identifier array; ip_logical : bool; ip_sign : signature; ip_vars : identifier list; @@ -83,23 +85,23 @@ type ml_ast = | MLdummy | MLcast of ml_ast * ml_type | MLmagic of ml_ast - | MLcustom of string (*s ML declarations. *) type ml_decl = | Dind of kernel_name * ml_ind | Dtype of global_reference * identifier list * ml_type - | Dterm of global_reference * ml_ast * ml_type - | DcustomTerm of global_reference * string - | DcustomType of global_reference * string - | Dfix of global_reference array * ml_ast array * ml_type array + | Dterm of global_reference * ml_ast * ml_type + | Dfix of global_reference array * ml_ast array * ml_type array + +type ml_spec = + | Sind of kernel_name * ml_ind + | Stype of global_reference * identifier list * ml_type option + | Sval of global_reference * ml_type type ml_specif = - | Sval of ml_type - | Stype of ml_type option - | Smind of ml_ind - | Smodule of ml_module_type (* et un module_path option ?? *) + | Spec of ml_spec + | Smodule of ml_module_type | Smodtype of ml_module_type and ml_module_sig = (label * ml_specif) list @@ -116,10 +118,7 @@ and ml_module_expr = | MEapply of ml_module_expr * ml_module_expr and ml_structure_elem = - | SEind of ml_ind - | SEtype of identifier list * ml_type - | SEterm of ml_ast * ml_type - | SEfix of global_reference array * ml_ast array * ml_type array + | SEdecl of ml_decl | SEmodule of ml_module (* pourquoi pas plutot ml_module_expr *) | SEmodtype of ml_module_type @@ -127,25 +126,32 @@ and ml_module_structure = (label * ml_structure_elem) list and ml_module = { ml_mod_expr : ml_module_expr option; - ml_mod_type : ml_module_type } + ml_mod_type : ml_module_type; + ml_mod_equiv : module_path option } + +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. *) -type extraction_params = - { modular : bool; - mod_name : identifier; - to_appear : global_reference list } - module type Mlpp_param = sig val globals : unit -> Idset.t - val pp_global : global_reference -> std_ppcmds + val pp_global : module_path -> global_reference -> std_ppcmds + val pp_long_module : module_path -> std_ppcmds + val pp_short_module : identifier -> std_ppcmds end module type Mlpp = sig - val pp_decl : ml_decl -> std_ppcmds + val pp_decl : module_path -> 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 } diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 145d700cc..3355fc2aa 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -212,7 +212,7 @@ let kn_of_r r = match r with | ConstRef kn -> kn | IndRef (kn,_) -> kn | ConstructRef ((kn,_),_) -> kn - | VarRef _ -> error_section () + | VarRef _ -> assert false let rec type_mem_kn kn = function | Tmeta _ -> assert false @@ -340,7 +340,7 @@ let ast_iter_rel f = | MLcons (_,l) -> List.iter (iter n) l | MLcast (a,_) -> iter n a | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy | MLcustom _ -> () + | MLglob _ | MLexn _ | MLdummy -> () in iter 0 (*s Map over asts. *) @@ -356,7 +356,7 @@ let ast_map f = function | MLcons (c,l) -> MLcons (c, List.map f l) | MLcast (a,t) -> MLcast (f a, t) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -372,7 +372,7 @@ let ast_map_lift f n = function | MLcons (c,l) -> MLcons (c, List.map (f n) l) | MLcast (a,t) -> MLcast (f n a, t) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a (*s Iter over asts. *) @@ -387,37 +387,7 @@ let ast_iter f = function | MLcons (c,l) -> List.iter f l | MLcast (a,t) -> f a | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLcustom _ as a -> () - -(*S Searching occurrences of a particular term (no lifting done). *) - -let rec ast_search t a = - if t = a then raise Found else ast_iter (ast_search t) a - -let decl_search t l = - let one_decl = function - | Dterm (_,a,_) -> ast_search t a - | Dfix (_,c,_) -> Array.iter (ast_search t) c - | _ -> () - in - try List.iter one_decl l; false with Found -> true - -let rec type_search t = function - | Tarr (a,b) -> type_search t a; type_search t b - | Tglob (r,l) -> List.iter (type_search t) l - | u -> if t = u then raise Found - -let decl_type_search t l = - let one_decl = function - | Dind (_,{ind_packets=p}) -> - Array.iter - (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p - | Dterm (_,_,u) -> type_search t u - | Dfix (_,_,v) -> Array.iter (type_search t) v - | Dtype (_,_,u) -> type_search t u - | _ -> () - in - try List.iter one_decl l; false with Found -> true + | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> () (*S Operations concerning De Bruijn indices. *) @@ -1032,7 +1002,7 @@ let rec non_stricts add cand = function | MLcase (t,v) -> (* The only interesting case: for a variable to be non-strict, *) (* it is sufficient that it appears non-strict in at least one branch, *) - (* so he make an union (in fact a merge). *) + (* so we make an union (in fact a merge). *) let cand = non_stricts false cand t in Array.fold_left (fun c (_,i,t)-> @@ -1062,10 +1032,10 @@ let is_not_strict t = If we could inline [t] (the user said nothing special), should we inline ? - We don't expand fixpoints, but always inductive constructors - and small terms. - Last case of inlining is a term with at least one non-strict - variable (i.e. a variable that may not be evaluated). *) + We expand small terms with at least one non-strict + variable (i.e. a variable that may not be evaluated). + + Futhermore we don't expand fixpoints. *) let inline_test t = not (is_fix t) && (ml_size t < 12 && is_not_strict t) @@ -1087,109 +1057,99 @@ let manual_inline = function we are free to act (AutoInline is set) \end{itemize} *) -(*i DEBUG - let inline_test' r t = - let b = inline_test t in - if b then msgnl (Printer.pr_global r); - b i*) - let inline r t = not (to_keep r) (* The user DOES want to keep it *) + && not (is_inline_custom r) && (to_inline r (* The user DOES want to inline it *) || (auto_inline () && lang () <> Haskell && (is_recursor r || manual_inline r || inline_test t))) (*S Optimization. *) -let subst_glob_ast r m = - let rec substrec = function - | MLglob r' as t -> if r = r' then m else t - | t -> ast_map substrec t - in substrec - -let subst_glob_decl r m = function - | Dterm(r',t',typ) -> Dterm(r', subst_glob_ast r m t', typ) - | d -> d - -let inline_glob r t l = - if not (inline r t) then true, l - else false, List.map (subst_glob_decl r t) l - -let print_ml_decl prm (r,_) = - not (to_inline r) || List.mem r prm.to_appear - -let add_ml_decls prm decls = - let l1 = ml_type_extractions () in - let l1 = List.filter (print_ml_decl prm) l1 in - let l1 = List.map (fun (r,s)-> DcustomType (r,s)) l1 in - let l2 = ml_term_extractions () in - let l2 = List.filter (print_ml_decl prm) l2 in - let l2 = List.map (fun (r,s)-> DcustomTerm (r,s)) l2 in - l1 @ l2 @ decls - -let rec expunge_fix_decls prm v c map b = function - | [] -> b, [], map - | Dterm (r, t, typ) :: l when array_exists ((=) r) v -> - let t = normalize t in - let t' = optimize_fix t in - (match t' with - | MLfix(_,_,c') when c=c' -> - let b',l = inline_glob r t l in - let b = b || b' || List.mem r prm.to_appear in - let map = Refmap.add r typ map in - expunge_fix_decls prm v c map b l - | _ -> raise Impossible) - | d::l -> let b,l,map = expunge_fix_decls prm v c map b l in b, d::l, map - -let rec optimize prm = function - | [] -> - [] +let rec subst_glob_ast s t = match t with + | MLglob (ConstRef kn) -> (try KNmap.find (long_kn kn) !s with Not_found -> t) + | _ -> ast_map (subst_glob_ast s) t + +let rec optim prm s = function + | [] -> [] | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l -> - if List.mem r prm.to_appear then d :: (optimize prm l) - else optimize prm l + if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l | Dterm (r,t,typ) :: l -> - let t = normalize t in - let b,l = inline_glob r t l in - let b = b || prm.modular || List.mem r prm.to_appear in - let t' = optimize_fix t in - (try optimize_Dfix prm (r,t',typ) b l - with Impossible -> - if b then Dterm (r,t',typ) :: (optimize prm l) - else optimize prm l) - | d :: l -> d :: (optimize prm l) - -and optimize_Dfix prm (r,t,typ) b l = - match t with - | MLfix (_, f, c) -> - let len = Array.length f in - if len = 1 then - if b then - let c = [|ast_subst (MLglob r) c.(0)|] in - Dfix ([|r|], c, [|typ|]) :: (optimize prm l) - else optimize prm l - else - let v = try - let d = dirpath (sp_of_global None r) in - Array.map (fun id -> locate (make_qualid d id)) f - with Not_found -> raise Impossible - in - let map = Refmap.add r typ (Refmap.empty) in - let b,l,map = expunge_fix_decls prm v c map b l in - if b then - let typs = - Array.map - (fun r -> try Refmap.find r map - with Not_found -> Tunknown) v - in - let c = - let gv = Array.init len (fun i -> MLglob v.(len-i-1)) in - Array.map (gen_subst gv (-len)) c in - Dfix (v, c, typs) :: (optimize prm l) - else optimize prm l - | _ -> raise Impossible + let t = normalize (subst_glob_ast s t) in + let i = inline r t in + if i then s := KNmap.add (long_kn (kn_of_r r)) t !s; + if not i || prm.modular || List.mem r prm.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) + +let rec optim_se top prm s = function + | [] -> [] + | (l,SEdecl (Dterm (r,a,t))) :: lse -> + let r = long_r r in + let kn = kn_of_r r in + let a = normalize (subst_glob_ast s a) in + let i = inline r a in + if i then s := KNmap.add kn a !s; + if top && i && not prm.modular && not (List.mem r prm.to_appear) + then optim_se top prm 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) + | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> + let av = Array.map (fun a -> normalize (subst_glob_ast s a)) av in + (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse) + | (l,SEmodule m) :: lse -> + let m = { m with ml_mod_expr = option_app (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) + +and optim_me prm s = function + | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm 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) + +let optimize_struct prm before struc = + let subst = ref (KNmap.empty : ml_ast KNmap.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 + +(*s Apply some functions upon all [ml_decl] and [ml_spec] found in a + [ml_structure]. *) + +let struct_iter do_decl do_spec s = + let rec se_iter = function + | (_,SEdecl d) -> do_decl d + | (_,SEmodule m) -> + option_iter me_iter m.ml_mod_expr; mt_iter m.ml_mod_type + | (_,SEmodtype m) -> mt_iter m + and me_iter = function + | MEident _ -> () + | MEfunctor (_,mt,me) -> me_iter me; mt_iter mt + | MEapply (me,me') -> me_iter me; me_iter me' + | MEstruct (msid, sel) -> List.iter se_iter sel + and mt_iter = function + | MTident _ -> () + | MTfunsig (_,mt,mt') -> mt_iter mt; mt_iter mt' + | MTsig (_, sign) -> List.iter spec_iter sign + and spec_iter = function + | (_,Spec s) -> do_spec s + | (_,Smodule mt) -> mt_iter mt + | (_,Smodtype mt) -> mt_iter mt + in + List.iter (function (_,sel) -> List.iter se_iter sel) s -(* Apply some fonctions upon all references in - [ml_type], [ml_ast], [ml_decl]. *) +(*s Apply some fonctions upon all references in [ml_type], [ml_ast], + [ml_decl], [ml_spec] and [ml_structure]. *) type do_ref = global_reference -> unit @@ -1210,25 +1170,93 @@ let ast_iter_references do_term do_cons do_type a = | MLcast (_,t) -> type_iter_references do_type t | _ -> () in iter a + +let ind_iter_references do_term do_cons do_type kn ind = + let type_iter = type_iter_references do_type in + let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in + let packet_iter ip p = + do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types + in + if ind.ind_info = Record then List.iter do_term (find_projections kn); + Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets let decl_iter_references do_term do_cons do_type = let type_iter = type_iter_references do_type - and ast_iter = ast_iter_references do_term do_cons do_type in - let cons_iter cp l = do_cons (ConstructRef cp); List.iter type_iter l in - let packet_iter ip p = - do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in - let ind_iter kn ind = - if ind.ind_info = Record then List.iter do_term (find_projections kn); - Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets - in + and ast_iter = ast_iter_references do_term do_cons do_type in function - | Dind (kn,ind) -> ind_iter kn ind + | Dind (kn,ind) -> ind_iter_references do_term do_cons do_type kn ind | Dtype (r,_,t) -> do_type r; type_iter t | Dterm (r,a,t) -> do_term r; ast_iter a; type_iter t | Dfix(rv,c,t) -> Array.iter do_term rv; Array.iter ast_iter c; Array.iter type_iter t - | DcustomTerm (r,_) -> do_term r - | DcustomType (r,_) -> do_type r +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 + | Sval (r,t) -> do_term r; type_iter_references do_type t + +let struct_iter_references do_term do_cons do_type = + struct_iter + (decl_iter_references do_term do_cons do_type) + (spec_iter_references do_term do_cons do_type) + +(*S Searching occurrences of a particular term (no lifting done). *) + +let rec ast_search t a = + if t = a then raise Found else ast_iter (ast_search t) a + +let decl_ast_search t = function + | Dterm (_,a,_) -> ast_search t a + | Dfix (_,c,_) -> Array.iter (ast_search t) c + | _ -> () + +let struct_ast_search t s = + try struct_iter (decl_ast_search t) (fun _ -> ()) s; false + with Found -> true + +let rec type_search t = function + | Tarr (a,b) -> type_search t a; type_search t b + | Tglob (r,l) -> List.iter (type_search t) l + | u -> if t = u then raise Found + +let decl_type_search t = function + | Dind (_,{ind_packets=p}) -> + Array.iter + (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p + | Dterm (_,_,u) -> type_search t u + | Dfix (_,_,v) -> Array.iter (type_search t) v + | Dtype (_,_,u) -> type_search t u + +let spec_type_search t = function + | Sind (_,{ind_packets=p}) -> + Array.iter + (fun {ip_types=v} -> Array.iter (List.iter (type_search t)) v) p + | Stype (_,_,ot) -> option_iter (type_search t) ot + | Sval (_,u) -> type_search t u + +let struct_type_search t s = + try struct_iter (decl_type_search t) (spec_type_search t) s; false + with Found -> true + + +(*s Generating the signature. *) + +let rec msig_of_ms = function + | [] -> [] + | (l,SEdecl (Dind (kn,i))) :: ms -> (l,Spec (Sind (kn,i))) :: (msig_of_ms ms) + | (l,SEdecl (Dterm (r,_,t))) :: ms -> (l,Spec (Sval (r,t))) :: (msig_of_ms ms) + | (l,SEdecl (Dtype (r,v,t))) :: ms -> + (l,Spec (Stype (r,v,Some t))) :: (msig_of_ms ms) + | (l,SEdecl (Dfix (rv,_,tv))) :: ms -> + let msig = ref (msig_of_ms ms) in + for i = Array.length rv - 1 downto 0 do + msig := (l,Spec (Sval (rv.(i),tv.(i))))::!msig + done; + !msig + | (l,SEmodule m) :: ms -> (l,Smodule m.ml_mod_type) :: (msig_of_ms ms) + | (l,SEmodtype m) :: ms -> (l,Smodtype m) :: (msig_of_ms ms) + +let signature_of_structure s = + List.map (fun (mp,ms) -> mp,msig_of_ms ms) s diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index c061a5369..b8f817eab 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -69,6 +69,10 @@ val type_neq : abbrev_map -> ml_type -> ml_type -> bool val type_to_sign : abbrev_map -> ml_type -> bool list val type_expunge : abbrev_map -> ml_type -> ml_type +val case_expunge : bool list -> ml_ast -> identifier list * ml_ast +val term_expunge : bool list -> identifier list * ml_ast -> ml_ast + + (*s Special identifiers. [dummy_name] is to be used for dead code and will be printed as [_] in concrete (Caml) code. *) @@ -95,34 +99,24 @@ val ast_occurs : int -> ml_ast -> bool val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast -(*s Some transformations of ML terms. [optimize] simplify +(*s Some transformations of ML terms. [optimize_struct] simplify 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. *) -val optimize : - extraction_params -> ml_decl list -> ml_decl list +val optimize_struct : + extraction_params -> ml_decl list option -> ml_structure -> ml_structure (* Misc. *) -val decl_search : ml_ast -> ml_decl list -> bool -val decl_type_search : ml_type -> ml_decl list -> bool - -val add_ml_decls : - extraction_params -> ml_decl list -> ml_decl list - -val case_expunge : - bool list -> ml_ast -> identifier list * ml_ast - -val term_expunge : - bool list -> identifier list * ml_ast -> ml_ast +val struct_ast_search : ml_ast -> ml_structure -> bool +val struct_type_search : ml_type -> ml_structure -> bool type do_ref = global_reference -> unit -val type_iter_references : do_ref -> ml_type -> unit -val ast_iter_references : do_ref -> do_ref -> do_ref -> ml_ast -> unit 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 - - +val signature_of_structure : ml_structure -> ml_signature diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 56108a225..f7a07f581 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -73,6 +73,9 @@ let rec rename_id id avoid = 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 @@ -119,27 +122,46 @@ let keywords = Idset.empty let preamble _ used_modules (mldummy,tdummy,tunknown) = - Idset.fold (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl() ++ s) - used_modules (mt ()) + 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 Idset.is_empty used_modules then mt () else fnl ()) + (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 () + 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()) (*s The pretty-printing functor. *) module Make = functor(P : Mlpp_param) -> struct -let pp_global r = P.pp_global r -let empty_env () = [], P.globals() +let local_mp = ref initial_path + +let pp_global r = + let r = long_r r in + if is_inline_custom r then str (find_custom r) + else P.pp_global !local_mp r + +let empty_env () = [], P.globals () (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) @@ -205,7 +227,7 @@ let rec pp_expr par env args = apply (pp_global r) | MLcons (r,[]) -> assert (args=[]); - if Refset.mem r !cons_cofix then + if Refset.mem (long_r r) !cons_cofix then pp_par par (str "lazy " ++ pp_global r) else pp_global r | MLcons (r,args') -> @@ -215,12 +237,12 @@ let rec pp_expr par env args = with Not_found -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in - if Refset.mem r !cons_cofix then + if Refset.mem (long_r r) !cons_cofix then pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") else pp_par par (pp_global r ++ spc () ++ tuple)) | MLcase (t, pv) -> let r,_,_ = pv.(0) in - let expr = if Refset.mem r !cons_cofix then + let expr = if Refset.mem (long_r r) !cons_cofix then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else (pp_expr false env [] t) @@ -256,7 +278,6 @@ let rec pp_expr par env args = spc () ++ pp_type true [] t)) | MLmagic a -> pp_apply (str "Obj.magic") par (pp_expr true env [] a :: args) - | MLcustom s -> str s and pp_record_pat (projs, args) = str "{ " ++ @@ -289,7 +310,8 @@ and pp_function env f t = let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl) in - let is_not_cofix pv = let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix) + let is_not_cofix pv = + let (r,_,_) = pv.(0) in not (Refset.mem (long_r r) !cons_cofix) in match t' with | MLcase(MLrel 1,pv) when is_not_cofix pv -> @@ -326,14 +348,20 @@ let pp_val e typ = (*s Pretty-printing of [Dfix] *) -let pp_Dfix env (p,c,t) = - let init = - pp_val p.(0) t.(0) ++ str "let rec " ++ pp_function env p.(0) c.(0) ++ fnl () - in - iterate_for 1 (Array.length p - 1) - (fun i acc -> acc ++ fnl () ++ - pp_val p.(i) t.(i) ++ str "and " ++ pp_function env p.(i) c.(i) ++ fnl ()) - init +let rec pp_Dfix init i ((rv,c,t) as fix) = + if i >= Array.length rv then mt () + else + let r = long_r rv.(i) in + if is_inline_custom r then pp_Dfix init (i+1) fix + else + let e = pp_global r in + (if init then mt () else fnl ()) ++ + pp_val e t.(i) ++ + str (if init then "let rec " else "and ") ++ + (if is_custom r then e ++ str " = " ++ str (find_custom r) + else pp_function (empty_env ()) e c.(i)) ++ + fnl () ++ + pp_Dfix false (i+1) fix (*s Pretty-printing of inductive types declaration. *) @@ -358,20 +386,22 @@ let pp_one_ind prefix ip pl cv = let pp_comment s = str "(* " ++ s ++ str " *)" ++ fnl () let pp_logical_ind ip packet = - pp_comment (Printer.pr_global (IndRef ip) ++ str " : logical inductive") ++ + pp_comment (pr_global (IndRef ip) ++ str " : logical inductive") ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc Printer.pr_global + prvect_with_sep spc pr_global (Array.mapi (fun i _ -> ConstructRef (ip,i+1)) packet.ip_types)) let pp_singleton kn packet = let l = rename_tvars keywords packet.ip_vars in - hov 0 (str "type " ++ pp_parameters l ++ - pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++ + hov 2 (str "type " ++ pp_parameters l ++ + P.pp_global !local_mp (IndRef (kn,0)) ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ - pp_comment (str "singleton inductive, whose constructor was " ++ - Printer.pr_global (ConstructRef ((kn,0),1)))) + pp_comment + (str "singleton inductive, whose constructor was " ++ + pr_id packet.ip_consnames.(0))) let pp_record kn packet = + let kn = long_kn kn in let l = List.combine (find_projections kn) packet.ip_types.(0) in let projs = find_projections kn in let pl = rename_tvars keywords packet.ip_vars in @@ -387,54 +417,148 @@ let pp_coind ip pl = pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" let rec pp_ind co first kn i ind = - if i >= Array.length ind.ind_packets then mt () + if i >= Array.length ind.ind_packets then + if first then mt () else fnl () else let ip = (kn,i) in let p = ind.ind_packets.(i) in - if p.ip_logical then - pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind + if is_custom (IndRef (kn,i)) then pp_ind co first kn (i+1) ind else - str (if first then "type " else "and ") ++ - (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ - pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++ - fnl () ++ pp_ind co false kn (i+1) ind + if p.ip_logical then + pp_logical_ind ip p ++ pp_ind co first kn (i+1) ind + else + str (if first then "type " else "and ") ++ + (if co then pp_coind ip p.ip_vars ++ fnl () ++ str "and " else mt ()) ++ + pp_one_ind (if co then "__" else "") ip p.ip_vars p.ip_types ++ + fnl () ++ pp_ind co false kn (i+1) ind (*s Pretty-printing of a declaration. *) -let pp_decl = function - | Dind (kn,i) as d -> - (match i.ind_info with - | Singleton -> pp_singleton kn i.ind_packets.(0) - | Record -> pp_record kn i.ind_packets.(0) - | Coinductive -> - let nop _ = () - and add r = cons_cofix := Refset.add r !cons_cofix in - decl_iter_references nop add nop d; - hov 0 (pp_ind true true kn 0 i) - | Standard -> - hov 0 (pp_ind false true kn 0 i)) - | Dtype (r, l, t) -> - let l = rename_tvars keywords l in - hov 0 (str "type" ++ spc () ++ pp_parameters l ++ - pp_global r ++ spc () ++ str "=" ++ spc () ++ - pp_type false l t ++ fnl ()) - | Dfix (rv, defs, typs) -> - (* We compute renamings of [rv] before asking [empty_env ()]... *) - let ppv = Array.map pp_global rv in - hov 0 (pp_Dfix (empty_env ()) (ppv,defs,typs)) - | Dterm (r, a, t) when is_projection r -> - let e = pp_global r in - (pp_val e t ++ - hov 0 (str "let " ++ e ++ str " x = x." ++ e ++ fnl())) - | Dterm (r, a, t) -> - let e = pp_global r in - (pp_val e t ++ - hov 0 (str "let " ++ pp_function (empty_env ()) e a ++ fnl ())) - | DcustomTerm (r,s) -> - hov 0 (str "let " ++ pp_global r ++ - str " =" ++ spc () ++ str s ++ fnl ()) - | DcustomType (r,s) -> - hov 0 (str "type " ++ pp_global r ++ str " = " ++ str s ++ fnl ()) +let pp_mind kn i = + let kn = long_kn kn in + (match i.ind_info with + | Singleton -> pp_singleton kn i.ind_packets.(0) ++ fnl () + | Coinductive -> + let nop _ = () + and add r = cons_cofix := Refset.add (long_r r) !cons_cofix in + decl_iter_references nop add nop (Dind (kn,i)); + hov 0 (pp_ind true true kn 0 i) ++ fnl () + | Record -> pp_record kn i.ind_packets.(0) ++ fnl () + | _ -> hov 0 (pp_ind false true kn 0 i)) + +let pp_decl mp = + local_mp := mp; + function + | Dind (kn,i) as d -> pp_mind kn i + | Dtype (r, l, t) -> + if is_inline_custom r then mt () + else + let l = rename_tvars keywords l in + let def = try str (find_custom r) with not_found -> pp_type false l t + in + hov 0 (str "type" ++ spc () ++ pp_parameters l ++ pp_global r ++ + spc () ++ str "=" ++ spc () ++ def ++ fnl () ++ fnl ()) + | Dterm (r, a, t) -> + if is_inline_custom r then mt () + 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) ++ fnl () + else if is_projection r then e ++ str " x = x." ++ e ++ fnl () + else pp_function (empty_env ()) e a ++ fnl ()) ++ fnl () + | Dfix (rv,defs,typs) -> + hov 0 (pp_Dfix true 0 (rv,defs,typs)) ++ fnl () + +let pp_spec mp = + local_mp := mp; + function + | Sind (kn,i) -> pp_mind kn i + | Sval (r,t) -> + if is_inline_custom r then mt () + else + hov 0 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++ + pp_type false [] t ++ fnl () ++ fnl ()) + | Stype (r,vl,ot) -> + if is_inline_custom r then mt () + else + let l = rename_tvars keywords vl in + let def = + try str "= " ++ str (find_custom r) + with not_found -> + match ot with + | None -> mt () + | Some t -> str "=" ++ spc () ++ pp_type false l t + in + hov 0 (str "type" ++ spc () ++ pp_parameters l ++ + pp_global r ++ spc () ++ def ++ fnl () ++ fnl ()) + +let rec pp_structure_elem mp = function + | (_,SEdecl d) -> pp_decl mp d + | (l,SEmodule m) -> + str "module " ++ P.pp_short_module (id_of_label l) ++ + (match m.ml_mod_equiv with + | None -> + str ":" ++ fnl () ++ pp_module_type m.ml_mod_type ++ fnl () ++ + str " = " ++ fnl () ++ + (match m.ml_mod_expr with + | None -> failwith "TODO: if this happens, see Jacek" + | Some me -> pp_module_expr me ++ fnl ()) + | Some mp -> str " = " ++ P.pp_long_module mp ++ fnl ()) ++ fnl () + | (l,SEmodtype m) -> + str "module type " ++ P.pp_short_module (id_of_label l) ++ + str " = " ++ pp_module_type m ++ fnl () ++ fnl () + +and pp_module_expr = function + | MEident mp -> P.pp_long_module mp + | MEfunctor (mbid, mt, me) -> + str "functor (" ++ + P.pp_short_module (id_of_mbid mbid) ++ + str ":" ++ + pp_module_type mt ++ + str ") ->" ++ + pp_module_expr me + | MEapply (me, me') -> + str "(" ++ pp_module_expr me ++ str " (" ++ pp_module_expr me' ++ str ")" + | MEstruct (msid, sel) -> + str "struct " ++ fnl () ++ + prlist_with_sep fnl (pp_structure_elem (MPself msid)) sel ++ fnl () ++ + str "end" + +and pp_module_type = function + | MTident kn -> + let mp,_,l = repr_kn kn in P.pp_long_module (MPdot (mp,l)) + | MTfunsig (mbid, mt, mt') -> + str "functor (" ++ + P.pp_short_module (id_of_mbid mbid) ++ + str ":" ++ + pp_module_type mt ++ + str ") ->" ++ + pp_module_type mt' + | MTsig (msid, sign) -> + str "sig " ++ fnl () ++ + prlist_with_sep fnl (pp_specif (MPself msid)) sign ++ fnl () ++ + str "end" + +and pp_specif mp = function + | (_,Spec s) -> pp_spec mp s + | (l,Smodule mt) -> + str "module " ++ + P.pp_short_module (id_of_label l) ++ + str " : " ++ pp_module_type mt ++ fnl () ++ fnl () + | (l,Smodtype mt) -> + str "module type " ++ + P.pp_short_module (id_of_label l) ++ + str " : " ++ pp_module_type mt ++ fnl () ++ fnl () + +let pp_struct = + prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel) + +let pp_signature = + prlist (fun (mp,sign) -> prlist (pp_specif mp) sign) end + + diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index da2706f68..babe170c2 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -27,6 +27,8 @@ 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 @@ -36,7 +38,11 @@ val get_db_name : int -> env -> identifier val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds +val preamble : + extraction_params -> module_path list -> 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 diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 75533f788..b6d0014ac 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -17,6 +17,7 @@ open Nameops open Libnames open Miniml open Mlutil +open Table open Ocaml (*s Scheme renaming issues. *) @@ -46,7 +47,7 @@ let pp_abst st = function module Make = functor(P : Mlpp_param) -> struct -let pp_global r = P.pp_global r +let pp_global r = P.pp_global initial_path r let empty_env () = [], P.globals() (*s Pretty-printing of expressions. *) @@ -109,8 +110,6 @@ let rec pp_expr env args = pp_expr env args a | MLmagic a -> pp_expr env args a - | MLcustom s -> str s - and pp_one_pat env (r,ids,t) = let pp_arg id = str "?" ++ pr_id id in @@ -141,10 +140,9 @@ 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 () - | DcustomType _ -> mt () | Dfix (rv, defs,_) -> let ppv = Array.map pp_global rv in prvect_with_sep fnl @@ -153,12 +151,25 @@ let pp_decl = function (paren (str "define " ++ pi ++ spc () ++ (pp_expr (empty_env ()) [] ti)) ++ fnl ())) - (array_map2 (fun p b -> (p,b)) ppv defs) + (array_map2 (fun p b -> (p,b)) ppv defs) ++ + fnl () | Dterm (r, a, _) -> - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ - pp_expr (empty_env ()) [] a)) ++ fnl () - | DcustomTerm (r,s) -> - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ str s) ++ fnl ()) + if is_inline_custom r then mt () + else + hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () + +let pp_structure_elem mp = function + | (l,SEdecl d) -> pp_decl mp 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 diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index 84940bbe7..4bd2a3d8b 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -16,7 +16,8 @@ open Names val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds +val preamble : + extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 223bc77b3..1aa3daec2 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -11,6 +11,7 @@ open Names open Term open Declarations +open Nameops open Summary open Libobject open Goptions @@ -19,46 +20,239 @@ open Util open Pp open Miniml +(*S Extraction environment, shared with [extract_env.ml] *) + +let cur_env = ref Environ.empty_env + +let id_of_global = function + | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l + | IndRef (kn,i) -> + let mib = Environ.lookup_mind kn !cur_env in + mib.mind_packets.(i).mind_typename + | ConstructRef ((kn,i),j) -> + let mib = Environ.lookup_mind kn !cur_env in + mib.mind_packets.(i).mind_consnames.(j-1) + | _ -> assert false + +let pr_global r = pr_id (id_of_global r) + (*S Warning and Error messages. *) +let err s = errorlabstrm "Extraction" s + let error_axiom_scheme r = - errorlabstrm "Extraction" - (str "Extraction cannot accept the type scheme axiom " ++ spc () ++ - Printer.pr_global r ++ spc () ++ str ".") + err (str "Extraction cannot accept the type scheme axiom " ++ spc () ++ + pr_global r ++ spc () ++ str ".") let error_axiom r = - errorlabstrm "Extraction" - (str "You must specify an extraction for axiom" ++ spc () ++ - Printer.pr_global r ++ spc () ++ str "first.") + err (str "You must specify an extraction for axiom" ++ spc () ++ + pr_global r ++ spc () ++ str "first.") let warning_axiom r = Options.if_verbose warn (str "This extraction depends on logical axiom" ++ spc () ++ - Printer.pr_global r ++ str "." ++ 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 error_section () = - errorlabstrm "Extraction" - (str "You can't do that within a section. Close it and try again.") + err (str "You can't do that within a module or a section." ++ fnl () ++ + str "Close it and try again.") let error_constant r = - errorlabstrm "Extraction" - (Printer.pr_global r ++ spc () ++ str "is not a constant.") + err (pr_global r ++ str " is not a constant.") + +let error_fixpoint r = + err (str "Fixpoint " ++ pr_global r ++ str " cannot be inlined.") let error_type_scheme r = - errorlabstrm "Extraction" - (Printer.pr_global r ++ spc () ++ str "is a type scheme, not a type.") + err (pr_global r ++ spc () ++ str "is a type scheme, not a type.") let error_inductive r = - errorlabstrm "Extraction" - (Printer.pr_global r ++ spc () ++ str "is not an inductive type.") + err (pr_global r ++ spc () ++ str "is not an inductive type.") let error_nb_cons () = - errorlabstrm "Extraction" (str "Not the right number of constructors.") + err (str "Not the right number of constructors.") + +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.") + +let error_unknown_module m = + err (str "Module" ++ spc () ++ pr_id 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.") + +let error_not_visible r = + err (pr_global r ++ str " is not directly visible.\n" ++ + str "For example, it may be inside an applied functor." ++ + str "Use Recursive Extraction to get the whole environment.") + +let error_unqualified_name s1 s2 = + err (str (s1 ^ " is used in " ^ s2 ^ " where it cannot be disambiguated\n" ^ + "in ML from another name sharing the same basename.\n" ^ + "Please do some renaming.\n")) + +(*S Utilities concerning [module_path] *) + +let current_toplevel () = fst (Lib.current_prefix ()) + +let is_toplevel mp = + mp = initial_path || mp = current_toplevel () + +let is_something_opened () = + try ignore (Lib.what_is_opened ()); true + with Not_found -> false + +let rec base_mp = function + | MPdot (mp,l) -> base_mp mp + | mp -> mp + +let rec prefixes_mp mp = match mp with + | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') + | _ -> MPset.singleton mp + +let is_modfile = function + | MPfile _ -> true + | _ -> false + +let rec modfile_of_mp mp = match mp with + | MPfile _ -> mp + | MPdot (mp,_) -> modfile_of_mp mp + | _ -> raise Not_found + +let at_toplevel mp = + is_modfile mp || is_toplevel mp + +let rec fst_level_module_of_mp mp = match mp with + | MPdot (mp, l) when is_toplevel mp -> mp,l + | MPdot (mp, l) -> fst_level_module_of_mp mp + | _ -> raise Not_found + +let rec parse_labels ll = function + | MPdot (mp,l) -> parse_labels (l::ll) mp + | mp -> mp,ll + +let labels_of_mp mp = parse_labels [] mp + +let labels_of_kn kn = + let mp,_,l = repr_kn kn in parse_labels [l] mp + +(*S The main tables: constants, inductives, records, ... *) + +(*s Module path aliases. *) + +(* A [MPbound] has no aliases except itself: it's its own long and short form.*) +(* A [MPself] is a short form, and the table contains its long form. *) +(* A [MPfile] is a long form, and the table contains its short form. *) +(* Since the table does not contain all intermediate forms, a [MPdot] + is dealt by first expending its head, and then looking in the table. *) + +let aliases = ref (MPmap.empty : module_path MPmap.t) +let init_aliases () = aliases := MPmap.empty +let add_aliases mp mp' = aliases := MPmap.add mp mp' (MPmap.add mp' mp !aliases) + +let rec long_mp mp = match mp with + | MPbound _ | MPfile _ -> mp + | MPself _ -> (try MPmap.find mp !aliases with Not_found -> mp) + | MPdot (mp1,l) -> + let mp2 = long_mp mp1 in + if mp1 == mp2 then mp else MPdot (mp2,l) +(*i let short_mp mp = match mp with + | MPself _ | MPbound _ -> mp + | MPfile _ -> (try MPmap.find mp !aliases with Not_found -> mp) + | MPdot _ -> (try MPmap.find (long_mp mp) !aliases with Not_found -> mp) +i*) -(*S Extraction AutoInline *) +let long_kn kn = + let (mp,s,l) = repr_kn kn in + let mp' = long_mp mp in + if mp' == mp then kn else make_kn mp' s l + +(*i let short_kn kn = + let (mp,s,l) = repr_kn kn in + let mp' = short_mp mp in + if mp' == mp then kn else make_kn mp' s l +i*) + +let long_r = function + | ConstRef kn -> ConstRef (long_kn kn) + | IndRef (kn,i) -> IndRef (long_kn kn, i) + | ConstructRef ((kn,i),j) -> ConstructRef ((long_kn kn,i),j) + | _ -> assert false + +(*s Constants tables. *) + +let terms = ref (KNmap.empty : ml_decl KNmap.t) +let init_terms () = terms := KNmap.empty +let add_term kn d = terms := KNmap.add (long_kn kn) d !terms +let lookup_term kn = KNmap.find (long_kn kn) !terms + +let types = ref (KNmap.empty : ml_schema KNmap.t) +let init_types () = types := KNmap.empty +let add_type kn s = types := KNmap.add (long_kn kn) s !types +let lookup_type kn = KNmap.find (long_kn kn) !types + +(*s Inductives table. *) + +let inductives = ref (KNmap.empty : ml_ind KNmap.t) +let init_inductives () = inductives := KNmap.empty +let add_ind kn m = inductives := KNmap.add (long_kn kn) m !inductives +let lookup_ind kn = KNmap.find (long_kn kn) !inductives + +(*s Recursors table. *) + +let recursors = ref KNset.empty +let init_recursors () = recursors := KNset.empty + +let add_recursors env kn = + let kn = long_kn kn in + let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in + let mib = Environ.lookup_mind kn env in + Array.iter + (fun mip -> + let id = mip.mind_typename in + let kn_rec = make_kn (Nameops.add_suffix id "_rec") + and kn_rect = make_kn (Nameops.add_suffix id "_rect") in + recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) + mib.mind_packets + +let is_recursor = function + | ConstRef kn -> KNset.mem (long_kn kn) !recursors + | _ -> false + +(*s Record tables. *) + +let records = ref (KNmap.empty : global_reference list KNmap.t) +let init_records () = records := KNmap.empty + +let projs = ref Refset.empty +let init_projs () = projs := Refset.empty + +let add_record kn l = + records := KNmap.add (long_kn kn) l !records; + projs := List.fold_right (fun r -> Refset.add (long_r r)) l !projs + +let find_projections kn = KNmap.find (long_kn kn) !records +let is_projection r = Refset.mem (long_r r) !projs + +(*s Tables synchronization. *) + +let reset_tables () = + init_terms (); init_types (); init_inductives (); init_recursors (); + init_records (); init_projs (); init_aliases () + + + +(*S The Extraction auxiliary commands *) + +(*s Extraction AutoInline *) let auto_inline_ref = ref true @@ -72,7 +266,7 @@ let _ = declare_bool_option optwrite = (:=) auto_inline_ref} -(*S Extraction Optimize *) +(*s Extraction Optimize *) let optim_ref = ref true @@ -86,7 +280,7 @@ let _ = declare_bool_option optwrite = (:=) optim_ref} -(*S Extraction Lang *) +(*s Extraction Lang *) type lang = Ocaml | Haskell | Scheme | Toplevel @@ -110,15 +304,15 @@ let _ = declare_summary "Extraction Lang" let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) -(*S Extraction Inline/NoInline *) +(*s Extraction Inline/NoInline *) let empty_inline_table = (Refset.empty,Refset.empty) let inline_table = ref empty_inline_table -let to_inline r = Refset.mem r (fst !inline_table) +let to_inline r = Refset.mem (long_r r) (fst !inline_table) -let to_keep r = Refset.mem r (snd !inline_table) +let to_keep r = Refset.mem (long_r r) (snd !inline_table) let add_inline_entries b l = let f b = if b then Refset.add else Refset.remove in @@ -127,7 +321,14 @@ let add_inline_entries b l = (List.fold_right (f b) l i), (List.fold_right (f (not b)) l k) -(*s Registration of operations for rollback. *) +let is_fixpoint kn = + match (Global.lookup_constant kn).const_body with + | None -> false + | Some body -> match kind_of_term (force body) with + | Fix _ | CoFix _ -> true + | _ -> false + +(* Registration of operations for rollback. *) let (inline_extraction,_) = declare_object @@ -142,15 +343,19 @@ let _ = declare_summary "Extraction Inline" init_function = (fun () -> inline_table := empty_inline_table); survive_section = true } -(*s Grammar entries. *) +(* Grammar entries. *) let extraction_inline b l = - if Lib.sections_are_opened () then error_section (); + if is_something_opened () then error_section (); let refs = List.map Nametab.global l in - List.iter (function ConstRef _ -> () | r -> error_constant r) refs; + List.iter + (fun r -> match r with + | ConstRef kn when b && is_fixpoint kn -> error_fixpoint r + | ConstRef _ -> () + | _ -> error_constant r) refs; Lib.add_anonymous_leaf (inline_extraction (b,refs)) -(*s Printing part *) +(* Printing part *) let print_extraction_inline () = let (i,n)= !inline_table in @@ -159,13 +364,13 @@ let print_extraction_inline () = (str "Extraction Inline:" ++ fnl () ++ Refset.fold (fun r p -> - (p ++ str " " ++ Printer.pr_global r ++ fnl ())) i' (mt ()) ++ + (p ++ str " " ++ pr_global r ++ fnl ())) i' (mt ()) ++ str "Extraction NoInline:" ++ fnl () ++ Refset.fold (fun r p -> - (p ++ str " " ++ Printer.pr_global r ++ fnl ())) n (mt ())) + (p ++ str " " ++ pr_global r ++ fnl ())) n (mt ())) -(*s Reset part *) +(* Reset part *) let (reset_inline,_) = declare_object @@ -177,7 +382,7 @@ let (reset_inline,_) = let reset_extraction_inline () = Lib.add_anonymous_leaf (reset_inline ()) -(*S Extract Constant/Inductive. *) +(*s Extract Constant/Inductive. *) type kind = Term | Type | Ind | Construct @@ -191,131 +396,63 @@ let check_term_or_type r = match r with else (r,Term) | _ -> error_constant r -let empty_extractions = (Refmap.empty, Refset.empty) +let customs = ref Refmap.empty -let extractions = ref empty_extractions +let all_customs () = + Refmap.fold (fun r _ -> Refset.add r) !customs Refset.empty -let ml_extractions () = snd !extractions +let term_customs () = + Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l) !customs [] -let ml_term_extractions () = - Refmap.fold (fun r (k,s) l -> if k=Term then (r,s)::l else l) - (fst !extractions) [] - -let ml_type_extractions () = - Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) - (fst !extractions) [] +let type_customs () = + Refmap.fold (fun r (k,s) l -> if k=Type then (r,s)::l else l) !customs [] -let add_ml_extraction r k s = - let (map,set) = !extractions in - extractions := (Refmap.add r (k,s) map, Refset.add r set) +let add_custom r k s = customs := Refmap.add r (k,s) !customs + +let is_custom r = Refmap.mem (long_r r) !customs -let is_ml_extraction r = Refset.mem r (snd !extractions) +let is_inline_custom r = + let r = long_r r in (is_custom r) && (to_inline r) -let find_ml_extraction r = snd (Refmap.find r (fst !extractions)) +let find_custom r = snd (Refmap.find (long_r r) !customs) -(*s Registration of operations for rollback. *) +(* Registration of operations for rollback. *) -let (in_ml_extraction,_) = +let (in_customs,_) = declare_object {(default_object "ML extractions") with - cache_function = (fun (_,(r,k,s)) -> add_ml_extraction r k s); - load_function = (fun _ (_,(r,k,s)) -> add_ml_extraction r k s); + cache_function = (fun (_,(r,k,s)) -> add_custom r k s); + load_function = (fun _ (_,(r,k,s)) -> add_custom r k s); export_function = (fun x -> Some x)} let _ = declare_summary "ML extractions" - { freeze_function = (fun () -> !extractions); - unfreeze_function = ((:=) extractions); - init_function = (fun () -> extractions := empty_extractions); + { freeze_function = (fun () -> !customs); + unfreeze_function = ((:=) customs); + init_function = (fun () -> customs := Refmap.empty); survive_section = true } -(*s Grammar entries. *) +(* Grammar entries. *) let extract_constant_inline inline r s = - if Lib.sections_are_opened () then error_section (); + if is_something_opened () then error_section (); let g,k = check_term_or_type (Nametab.global r) in Lib.add_anonymous_leaf (inline_extraction (inline,[g])); - Lib.add_anonymous_leaf (in_ml_extraction (g,k,s)) + Lib.add_anonymous_leaf (in_customs (g,k,s)) let extract_inductive r (s,l) = - if Lib.sections_are_opened () then error_section (); + if is_something_opened () then error_section (); let g = Nametab.global r in match g with | IndRef ((kn,i) as ip) -> let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets.(i).mind_consnames in if n <> List.length l then error_nb_cons (); Lib.add_anonymous_leaf (inline_extraction (true,[g])); - Lib.add_anonymous_leaf (in_ml_extraction (g,Ind,s)); + Lib.add_anonymous_leaf (in_customs (g,Ind,s)); list_iter_i (fun j s -> let g = ConstructRef (ip,succ j) in Lib.add_anonymous_leaf (inline_extraction (true,[g])); - Lib.add_anonymous_leaf (in_ml_extraction (g,Construct,s))) l + Lib.add_anonymous_leaf (in_customs (g,Construct,s))) l | _ -> error_inductive g -(*S The other tables: constants, inductives, records, ... *) - -(*s Constants tables. *) - -let terms = ref (KNmap.empty : ml_decl KNmap.t) -let add_term kn d = terms := KNmap.add kn d !terms -let lookup_term kn = KNmap.find kn !terms - -let types = ref (KNmap.empty : ml_schema KNmap.t) -let add_type kn s = types := KNmap.add kn s !types -let lookup_type kn = KNmap.find kn !types - -(*s Inductives table. *) - -let inductives = ref (KNmap.empty : ml_ind KNmap.t) -let add_ind kn m = inductives := KNmap.add kn m !inductives -let lookup_ind kn = KNmap.find kn !inductives - -(*s Recursors table. *) - -let recursors = ref KNset.empty - -let add_recursors kn = - let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in - let mib = Global.lookup_mind kn in - Array.iter - (fun mip -> - let id = mip.mind_typename in - let kn_rec = make_kn (Nameops.add_suffix id "_rec") - and kn_rect = make_kn (Nameops.add_suffix id "_rect") in - recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) - mib.mind_packets - -let is_recursor = function - | ConstRef kn -> KNset.mem kn !recursors - | _ -> false - -(*s Record tables. *) - -let records = ref (KNmap.empty : global_reference list KNmap.t) -let projs = ref Refset.empty - -let add_record kn l = - records := KNmap.add kn l !records; - projs := List.fold_right Refset.add l !projs - -let find_projections kn = KNmap.find kn !records -let is_projection r = Refset.mem r !projs - -(*s Tables synchronization. *) - -let freeze () = !terms, !types, !inductives, !recursors, !records, !projs - -let unfreeze (te,ty,id,re,rd,pr) = - terms:=te; types:=ty; inductives:=id; recursors:=re; records:=rd; projs:=pr - -let _ = declare_summary "Extraction tables" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = (fun () -> ()); - survive_section = true } - - - - - diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index e6495add6..917e7884a 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -12,6 +12,12 @@ open Names open Libnames open Miniml +val cur_env : Environ.env ref + +val id_of_global : global_reference -> identifier + +val pr_global : global_reference -> Pp.std_ppcmds + (*s Warning and Error messages. *) val error_axiom_scheme : global_reference -> 'a @@ -19,9 +25,57 @@ val error_axiom : global_reference -> 'a val warning_axiom : global_reference -> unit val error_section : unit -> 'a val error_constant : global_reference -> 'a +val error_fixpoint : global_reference -> 'a val error_type_scheme : 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 : identifier -> 'a +val error_toplevel : unit -> 'a +val error_scheme : unit -> 'a +val error_not_visible : global_reference -> 'a +val error_unqualified_name : string -> string -> 'a + +(*s utilities concerning [module_path]. *) + +val current_toplevel : unit -> module_path + +val is_toplevel : module_path -> bool +val at_toplevel : module_path -> bool +val base_mp : module_path -> module_path +val prefixes_mp : module_path -> MPset.t +val is_modfile : module_path -> bool +val modfile_of_mp : module_path -> module_path +val fst_level_module_of_mp : module_path -> module_path * label +val labels_of_mp : module_path -> module_path * label list +val labels_of_kn : kernel_name -> module_path * label list + +val is_something_opened : unit -> bool + +(*s Some table-related operations *) + +val add_term : kernel_name -> ml_decl -> unit +val lookup_term : kernel_name -> ml_decl + +val add_type : kernel_name -> ml_schema -> unit +val lookup_type : kernel_name -> ml_schema + +val add_ind : kernel_name -> ml_ind -> unit +val lookup_ind : kernel_name -> ml_ind + +val add_recursors : Environ.env -> kernel_name -> unit +val is_recursor : global_reference -> bool + +val add_record : kernel_name -> global_reference list -> unit +val find_projections : kernel_name -> global_reference list +val is_projection : global_reference -> bool + +val add_aliases : module_path -> module_path -> unit +val long_mp : module_path -> module_path +val long_kn : kernel_name -> kernel_name +val long_r : global_reference -> global_reference + +val reset_tables : unit -> unit (*s AutoInline parameter *) @@ -41,13 +95,14 @@ val lang : unit -> lang val to_inline : global_reference -> bool val to_keep : global_reference -> bool -(*s Table for direct ML extractions. *) +(*s Table for user-given custom ML extractions. *) -val is_ml_extraction : global_reference -> bool -val find_ml_extraction : global_reference -> string -val ml_extractions : unit -> Refset.t -val ml_type_extractions : unit -> (global_reference * string) list -val ml_term_extractions : unit -> (global_reference * string) list +val is_custom : global_reference -> bool +val is_inline_custom : global_reference -> bool +val find_custom : global_reference -> string +val all_customs : unit -> Refset.t +val type_customs : unit -> (global_reference * string) list +val term_customs : unit -> (global_reference * string) list (*s Extraction commands. *) @@ -58,22 +113,6 @@ val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string -> unit val extract_inductive : reference -> string * string list -> unit -(*s Some table-related operations *) - -val add_term : kernel_name -> ml_decl -> unit -val lookup_term : kernel_name -> ml_decl - -val add_type : kernel_name -> ml_schema -> unit -val lookup_type : kernel_name -> ml_schema - -val add_ind : kernel_name -> ml_ind -> unit -val lookup_ind : kernel_name -> ml_ind -val add_recursors : kernel_name -> unit -val is_recursor : global_reference -> bool - -val add_record : kernel_name -> global_reference list -> unit -val find_projections : kernel_name -> global_reference list -val is_projection : global_reference -> bool diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index 952a8e087..f70e81319 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -78,6 +78,12 @@ theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ theories/Bool/bool.cmi theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ theories/Bool/bool.cmi +theories/Bool/bvector.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/Arith/minus.cmi theories/Init/peano.cmi \ + theories/Bool/bvector.cmi +theories/Bool/bvector.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \ + theories/Arith/minus.cmx theories/Init/peano.cmx \ + theories/Bool/bvector.cmi theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \ @@ -156,16 +162,16 @@ theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ theories/Init/specif.cmx theories/IntMap/fset.cmi theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ theories/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \ - theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi \ - theories/IntMap/lsort.cmi + theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/IntMap/lsort.cmi theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ theories/Bool/bool.cmx theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \ - theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx \ - theories/IntMap/lsort.cmi + theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \ + theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ + theories/Lists/polyList.cmx theories/Init/specif.cmx \ + theories/Bool/sumbool.cmx theories/IntMap/lsort.cmi theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \ @@ -174,13 +180,13 @@ theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \ theories/Init/specif.cmx theories/IntMap/mapcanon.cmi theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \ theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/IntMap/map.cmi theories/Init/peano.cmi \ + theories/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.cmi \ theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ theories/Init/specif.cmi theories/Bool/sumbool.cmi \ theories/IntMap/mapcard.cmi theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \ theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ - theories/IntMap/map.cmx theories/Init/peano.cmx \ + theories/Init/logic.cmx theories/IntMap/map.cmx theories/Init/peano.cmx \ theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \ theories/Init/specif.cmx theories/Bool/sumbool.cmx \ theories/IntMap/mapcard.cmi @@ -357,13 +363,15 @@ theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \ theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \ theories/Init/specif.cmx theories/Sets/uniset.cmi theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \ - theories/Sets/multiset.cmi theories/Init/peano.cmi \ - theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \ - theories/Init/specif.cmi theories/Sorting/heap.cmi + theories/Init/logic.cmi theories/Sets/multiset.cmi \ + theories/Init/peano.cmi theories/Lists/polyList.cmi \ + theories/Sorting/sorting.cmi theories/Init/specif.cmi \ + theories/Sorting/heap.cmi theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \ - theories/Sets/multiset.cmx theories/Init/peano.cmx \ - theories/Lists/polyList.cmx theories/Sorting/sorting.cmx \ - theories/Init/specif.cmx theories/Sorting/heap.cmi + theories/Init/logic.cmx theories/Sets/multiset.cmx \ + theories/Init/peano.cmx theories/Lists/polyList.cmx \ + theories/Sorting/sorting.cmx theories/Init/specif.cmx \ + theories/Sorting/heap.cmi theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \ theories/Sets/multiset.cmi theories/Init/peano.cmi \ theories/Lists/polyList.cmi theories/Init/specif.cmi \ @@ -372,10 +380,12 @@ theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \ theories/Sets/multiset.cmx theories/Init/peano.cmx \ theories/Lists/polyList.cmx theories/Init/specif.cmx \ theories/Sorting/permutation.cmi -theories/Sorting/sorting.cmo: theories/Lists/polyList.cmi \ - theories/Init/specif.cmi theories/Sorting/sorting.cmi -theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \ - theories/Init/specif.cmx theories/Sorting/sorting.cmi +theories/Sorting/sorting.cmo: theories/Init/logic.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Sorting/sorting.cmi +theories/Sorting/sorting.cmx: theories/Init/logic.cmx \ + theories/Lists/polyList.cmx theories/Init/specif.cmx \ + theories/Sorting/sorting.cmi theories/Wellfounded/disjoint_Union.cmo: \ theories/Wellfounded/disjoint_Union.cmi theories/Wellfounded/disjoint_Union.cmx: \ @@ -436,6 +446,14 @@ theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.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/Bool/bvector.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \ + theories/ZArith/zbinary.cmi +theories/ZArith/zbinary.cmx: theories/Bool/bvector.cmx \ + theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \ + theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \ + theories/ZArith/zbinary.cmi theories/ZArith/zbool.cmo: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ @@ -473,11 +491,13 @@ theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmo: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \ - theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi + theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi \ + theories/ZArith/zpower.cmi theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \ - theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi + theories/ZArith/fast_integer.cmx theories/Init/logic.cmx \ + theories/ZArith/zarith_aux.cmx theories/ZArith/zmisc.cmx \ + theories/ZArith/zpower.cmi theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmi \ theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ theories/ZArith/zarith_aux.cmi theories/ZArith/zsqrt.cmi @@ -512,6 +532,8 @@ theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \ theories/Init/specif.cmi theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Bool/bvector.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/Arith/minus.cmi theories/Init/peano.cmi theories/Bool/decBool.cmi: theories/Init/specif.cmi theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \ theories/Init/specif.cmi @@ -537,14 +559,15 @@ theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ theories/Init/specif.cmi theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ theories/Bool/bool.cmi theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \ - theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \ - theories/Init/specif.cmi theories/Bool/sumbool.cmi + theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi \ theories/Init/specif.cmi theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \ theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ - theories/IntMap/map.cmi theories/Init/peano.cmi \ + theories/Init/logic.cmi theories/IntMap/map.cmi theories/Init/peano.cmi \ theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ theories/Init/specif.cmi theories/Bool/sumbool.cmi theories/IntMap/mapfold.cmi: theories/IntMap/addr.cmi \ @@ -584,14 +607,14 @@ theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \ theories/Init/specif.cmi theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \ - theories/Sets/multiset.cmi theories/Init/peano.cmi \ - theories/Lists/polyList.cmi theories/Sorting/sorting.cmi \ - theories/Init/specif.cmi + theories/Init/logic.cmi theories/Sets/multiset.cmi \ + theories/Init/peano.cmi theories/Lists/polyList.cmi \ + theories/Sorting/sorting.cmi theories/Init/specif.cmi theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \ theories/Sets/multiset.cmi theories/Init/peano.cmi \ theories/Lists/polyList.cmi theories/Init/specif.cmi -theories/Sorting/sorting.cmi: theories/Lists/polyList.cmi \ - theories/Init/specif.cmi +theories/Sorting/sorting.cmi: theories/Init/logic.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi theories/ZArith/fast_integer.cmi: theories/Init/datatypes.cmi \ theories/Init/peano.cmi @@ -602,6 +625,9 @@ theories/ZArith/zarith_aux.cmi: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi: theories/ZArith/fast_integer.cmi \ theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/ZArith/zbinary.cmi: theories/Bool/bvector.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi theories/ZArith/zbool.cmi: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ theories/Bool/sumbool.cmi theories/ZArith/zArith_dec.cmi \ @@ -618,8 +644,8 @@ theories/ZArith/zlogarithm.cmi: theories/ZArith/fast_integer.cmi \ theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \ theories/ZArith/fast_integer.cmi theories/Init/specif.cmi theories/ZArith/zpower.cmi: theories/Init/datatypes.cmi \ - theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \ - theories/ZArith/zmisc.cmi + theories/ZArith/fast_integer.cmi theories/Init/logic.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zmisc.cmi theories/ZArith/zsqrt.cmi: theories/ZArith/fast_integer.cmi \ theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ theories/ZArith/zarith_aux.cmi diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 646e8b6ba..4ab5fe7fb 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -42,8 +42,8 @@ depend: $(ML) tree: mkdir -p $(DIRS) -%.mli:%.ml - ./make_mli $< > $@ +#%.mli:%.ml +# ./make_mli $< > $@ %.cmi:%.mli ocamlc $(INCL) -c -i $< diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell index 347e99887..bd50f9bf5 100644 --- a/contrib/extraction/test/Makefile.haskell +++ b/contrib/extraction/test/Makefile.haskell @@ -7,6 +7,7 @@ TOPDIR=../../.. # Files with axioms to be realized: can't be extracted directly AXIOMSVO:= \ +theories/Init/PeanoSyntax.vo \ theories/Init/Prelude.vo \ theories/Arith/Arith.vo \ theories/Lists/List.vo \ @@ -68,69 +69,77 @@ v2hs: v2hs.ml # DO NOT DELETE: Beginning of Haskell dependencies theories/Arith/Between.o : theories/Arith/Between.hs -theories/Arith/Compare.o : theories/Arith/Compare.hs -theories/Arith/Compare.o : theories/Arith/Compare_dec.o -theories/Arith/Compare.o : theories/Init/Specif.o +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/Datatypes.o -theories/Arith/Compare_dec.o : theories/Init/Logic.o 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/Datatypes.o +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/Datatypes.o theories/Arith/EqNat.o : theories/Init/Specif.o -theories/Arith/Euclid.o : theories/Arith/Compare_dec.o +theories/Arith/EqNat.o : theories/Init/Datatypes.o theories/Arith/Euclid.o : theories/Arith/Euclid.hs -theories/Arith/Euclid.o : theories/Arith/Minus.o theories/Arith/Euclid.o : theories/Arith/Wf_nat.o -theories/Arith/Euclid.o : theories/Init/Datatypes.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/Datatypes.o 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/Datatypes.o -theories/Arith/Max.o : theories/Init/Logic.o 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/Datatypes.o -theories/Arith/Min.o : theories/Init/Logic.o 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/Datatypes.o 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/Datatypes.o -theories/Arith/Plus.o : theories/Init/Logic.o 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/Datatypes.o -theories/Arith/Wf_nat.o : theories/Init/Logic.o theories/Arith/Wf_nat.o : theories/Init/Wf.o -theories/Bool/Bool.o : theories/Bool/Bool.hs -theories/Bool/Bool.o : theories/Init/Datatypes.o -theories/Bool/Bool.o : theories/Init/Specif.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/Datatypes.o 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/Datatypes.o 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/Datatypes.o 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 @@ -139,188 +148,200 @@ 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/Datatypes.o theories/Init/Peano.o : theories/Init/Peano.hs -theories/Init/Specif.o : theories/Init/Datatypes.o -theories/Init/Specif.o : theories/Init/Logic.o +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/Datatypes.o -theories/IntMap/Adalloc.o : theories/Init/Logic.o theories/IntMap/Adalloc.o : theories/Init/Specif.o -theories/IntMap/Adalloc.o : theories/IntMap/Adalloc.hs -theories/IntMap/Adalloc.o : theories/IntMap/Addec.o -theories/IntMap/Adalloc.o : theories/IntMap/Addr.o theories/IntMap/Adalloc.o : theories/IntMap/Map.o -theories/IntMap/Adalloc.o : theories/ZArith/Fast_integer.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/Datatypes.o theories/IntMap/Addec.o : theories/Init/Specif.o -theories/IntMap/Addec.o : theories/IntMap/Addec.hs +theories/IntMap/Addec.o : theories/Init/Datatypes.o theories/IntMap/Addec.o : theories/IntMap/Addr.o -theories/IntMap/Addec.o : theories/ZArith/Fast_integer.o -theories/IntMap/Addr.o : theories/Bool/Bool.o -theories/IntMap/Addr.o : theories/Init/Datatypes.o -theories/IntMap/Addr.o : theories/Init/Specif.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/Adist.o : theories/IntMap/Adist.hs -theories/IntMap/Adist.o : theories/ZArith/Fast_integer.o theories/IntMap/Allmaps.o : theories/IntMap/Allmaps.hs -theories/IntMap/Fset.o : theories/Init/Datatypes.o -theories/IntMap/Fset.o : theories/Init/Logic.o -theories/IntMap/Fset.o : theories/Init/Specif.o -theories/IntMap/Fset.o : theories/IntMap/Addec.o -theories/IntMap/Fset.o : theories/IntMap/Addr.o 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/Lsort.o : theories/Bool/Bool.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/Datatypes.o -theories/IntMap/Lsort.o : theories/Init/Logic.o theories/IntMap/Lsort.o : theories/Init/Specif.o -theories/IntMap/Lsort.o : theories/IntMap/Addec.o -theories/IntMap/Lsort.o : theories/IntMap/Addr.o -theories/IntMap/Lsort.o : theories/IntMap/Lsort.hs -theories/IntMap/Lsort.o : theories/IntMap/Mapiter.o theories/IntMap/Lsort.o : theories/Lists/PolyList.o -theories/IntMap/Lsort.o : theories/ZArith/Fast_integer.o -theories/IntMap/Map.o : theories/Init/Datatypes.o -theories/IntMap/Map.o : theories/Init/Peano.o -theories/IntMap/Map.o : theories/Init/Specif.o -theories/IntMap/Map.o : theories/IntMap/Addec.o -theories/IntMap/Map.o : theories/IntMap/Addr.o -theories/IntMap/Map.o : theories/IntMap/Map.hs -theories/IntMap/Map.o : theories/ZArith/Fast_integer.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/Mapc.o : theories/IntMap/Mapc.hs -theories/IntMap/Mapcanon.o : theories/IntMap/Map.o theories/IntMap/Mapcanon.o : theories/IntMap/Mapcanon.hs -theories/IntMap/Mapcard.o : theories/Arith/Peano_dec.o -theories/IntMap/Mapcard.o : theories/Arith/Plus.o +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/Datatypes.o -theories/IntMap/Mapcard.o : theories/Init/Logic.o -theories/IntMap/Mapcard.o : theories/Init/Peano.o theories/IntMap/Mapcard.o : theories/Init/Specif.o -theories/IntMap/Mapcard.o : theories/IntMap/Addec.o -theories/IntMap/Mapcard.o : theories/IntMap/Addr.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/IntMap/Mapcard.hs -theories/IntMap/Mapfold.o : theories/Init/Datatypes.o -theories/IntMap/Mapfold.o : theories/Init/Logic.o -theories/IntMap/Mapfold.o : theories/Init/Specif.o -theories/IntMap/Mapfold.o : theories/IntMap/Fset.o -theories/IntMap/Mapfold.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/Datatypes.o -theories/IntMap/Mapiter.o : theories/Init/Logic.o theories/IntMap/Mapiter.o : theories/Init/Specif.o -theories/IntMap/Mapiter.o : theories/IntMap/Addec.o -theories/IntMap/Mapiter.o : theories/IntMap/Addr.o -theories/IntMap/Mapiter.o : theories/IntMap/Map.o -theories/IntMap/Mapiter.o : theories/IntMap/Mapiter.hs theories/IntMap/Mapiter.o : theories/Lists/PolyList.o -theories/IntMap/Maplists.o : theories/Bool/Bool.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/Datatypes.o -theories/IntMap/Maplists.o : theories/Init/Logic.o theories/IntMap/Maplists.o : theories/Init/Specif.o -theories/IntMap/Maplists.o : theories/IntMap/Addec.o -theories/IntMap/Maplists.o : theories/IntMap/Map.o -theories/IntMap/Maplists.o : theories/IntMap/Mapiter.o -theories/IntMap/Maplists.o : theories/IntMap/Maplists.hs theories/IntMap/Maplists.o : theories/Lists/PolyList.o -theories/IntMap/Mapsubset.o : theories/Bool/Bool.o -theories/IntMap/Mapsubset.o : theories/Init/Datatypes.o -theories/IntMap/Mapsubset.o : theories/IntMap/Fset.o -theories/IntMap/Mapsubset.o : theories/IntMap/Map.o -theories/IntMap/Mapsubset.o : theories/IntMap/Mapiter.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/Lists/ListSet.o : theories/Init/Datatypes.o -theories/Lists/ListSet.o : theories/Init/Logic.o -theories/Lists/ListSet.o : theories/Init/Specif.o +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/PolyList.o : theories/Init/Datatypes.o -theories/Lists/PolyList.o : theories/Init/Specif.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/Init/Datatypes.o theories/Lists/Streams.o : theories/Lists/Streams.hs -theories/Lists/TheoryList.o : theories/Bool/DecBool.o -theories/Lists/TheoryList.o : theories/Init/Datatypes.o +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/Lists/TheoryList.hs +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/Elimdep.o : theories/Logic/Elimdep.hs -theories/Logic/Eqdep.o : theories/Logic/Eqdep.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.o : theories/Sets/Finite_sets.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/Multiset.o : theories/Init/Datatypes.o -theories/Sets/Multiset.o : theories/Init/Peano.o -theories/Sets/Multiset.o : theories/Init/Specif.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.o : theories/Sets/Partial_Order.o -theories/Sets/Powerset.o : theories/Sets/Powerset.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/Relations_1.o : theories/Sets/Relations_1.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_2.o : theories/Sets/Relations_2.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_3.o : theories/Sets/Relations_3.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/Uniset.o : theories/Bool/Bool.o -theories/Sets/Uniset.o : theories/Init/Datatypes.o -theories/Sets/Uniset.o : theories/Init/Specif.o +theories/Sets/Relations_3.o : theories/Sets/Relations_3.hs theories/Sets/Uniset.o : theories/Sets/Uniset.hs -theories/Sorting/Heap.o : theories/Init/Logic.o +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/Sorting/Heap.hs -theories/Sorting/Heap.o : theories/Sorting/Sorting.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/Permutation.o : theories/Sorting/Permutation.hs -theories/Sorting/Sorting.o : theories/Init/Logic.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/Sorting/Sorting.hs +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 @@ -328,51 +349,73 @@ theories/Wellfounded/Lexicographic_Exponentiation.o : theories/Wellfounded/Lexic 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/Well_Ordering.o : theories/Init/Specif.o -theories/Wellfounded/Well_Ordering.o : theories/Init/Wf.o -theories/Wellfounded/Well_Ordering.o : theories/Wellfounded/Well_Ordering.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/Init/Datatypes.o -theories/ZArith/Fast_integer.o : theories/Init/Peano.o theories/ZArith/Fast_integer.o : theories/ZArith/Fast_integer.hs -theories/ZArith/Wf_Z.o : theories/Init/Datatypes.o -theories/ZArith/Wf_Z.o : theories/Init/Logic.o -theories/ZArith/Wf_Z.o : theories/Init/Peano.o -theories/ZArith/Wf_Z.o : theories/Init/Specif.o -theories/ZArith/Wf_Z.o : theories/ZArith/Fast_integer.o +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/ZArith.o : theories/ZArith/ZArith.hs +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/Logic.o theories/ZArith/ZArith_dec.o : theories/Init/Specif.o -theories/ZArith/ZArith_dec.o : theories/ZArith/Fast_integer.o -theories/ZArith/ZArith_dec.o : theories/ZArith/ZArith_dec.hs -theories/ZArith/Zarith_aux.o : theories/Init/Datatypes.o -theories/ZArith/Zarith_aux.o : theories/Init/Specif.o -theories/ZArith/Zarith_aux.o : theories/ZArith/Fast_integer.o -theories/ZArith/Zarith_aux.o : theories/ZArith/Zarith_aux.hs -theories/ZArith/Zcomplements.o : theories/Init/Datatypes.o -theories/ZArith/Zcomplements.o : theories/Init/Logic.o -theories/ZArith/Zcomplements.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/ZArith/ZArith_dec.o -theories/ZArith/Zcomplements.o : theories/ZArith/Zarith_aux.o -theories/ZArith/Zcomplements.o : theories/ZArith/Zcomplements.hs +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/Fast_integer.o -theories/ZArith/Zlogarithm.o : theories/ZArith/Zarith_aux.o theories/ZArith/Zlogarithm.o : theories/ZArith/Zlogarithm.hs -theories/ZArith/Zmisc.o : theories/Init/Datatypes.o -theories/ZArith/Zmisc.o : theories/Init/Specif.o -theories/ZArith/Zmisc.o : theories/ZArith/Fast_integer.o +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/Zpower.o : theories/Init/Datatypes.o -theories/ZArith/Zpower.o : theories/Init/Logic.o -theories/ZArith/Zpower.o : theories/ZArith/Fast_integer.o +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/ZArith/Zpower.hs +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 |