diff options
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/common.ml | 754 | ||||
-rw-r--r-- | contrib/extraction/common.mli | 48 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 266 | ||||
-rw-r--r-- | contrib/extraction/extract_env.mli | 6 | ||||
-rw-r--r-- | contrib/extraction/extraction.ml | 35 | ||||
-rw-r--r-- | contrib/extraction/extraction.mli | 10 | ||||
-rw-r--r-- | contrib/extraction/g_extraction.ml4 | 7 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 90 | ||||
-rw-r--r-- | contrib/extraction/haskell.mli | 10 | ||||
-rw-r--r-- | contrib/extraction/miniml.mli | 53 | ||||
-rw-r--r-- | contrib/extraction/modutil.ml | 118 | ||||
-rw-r--r-- | contrib/extraction/modutil.mli | 20 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 534 | ||||
-rw-r--r-- | contrib/extraction/ocaml.mli | 44 | ||||
-rw-r--r-- | contrib/extraction/scheme.ml | 55 | ||||
-rw-r--r-- | contrib/extraction/scheme.mli | 18 | ||||
-rw-r--r-- | contrib/extraction/table.ml | 169 | ||||
-rw-r--r-- | contrib/extraction/table.mli | 34 |
18 files changed, 1179 insertions, 1092 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 6db146b1e..855990d25 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -17,42 +17,218 @@ open Nameops open Libnames open Table open Miniml +open Mlutil open Modutil -open Ocaml +open Mod_subst -(*S Renamings. *) +(*s Some pretty-print utility functions. *) + +let pp_par par st = if par then str "(" ++ st ++ str ")" else st + +let pp_apply st par args = match args with + | [] -> st + | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) + +let pr_binding = function + | [] -> mt () + | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l + +let fnl2 () = fnl () ++ fnl () + +let space_if = function true -> str " " | false -> mt () + +let sec_space_if = function true -> spc () | false -> mt () + +let is_digit = function + | '0'..'9' -> true + | _ -> false + +let begins_with_CoqXX s = + let n = String.length s in + n >= 4 && s.[0] = 'C' && s.[1] = 'o' && s.[2] = 'q' && + let i = ref 3 in + try while !i < n do + if s.[!i] = '_' then i:=n (*Stop*) + else if is_digit s.[!i] then incr i + else raise Not_found + done; true + with Not_found -> false + +let unquote s = + if lang () <> Scheme then s + else + let s = String.copy s in + for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; + s + +let rec dottify = function + | [] -> assert false + | [s] -> unquote s + | s::[""] -> unquote s + | s::l -> (dottify l)^"."^(unquote s) + +(*s Uppercase/lowercase renamings. *) + +let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false +let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false + +let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) +let uppercase_id id = id_of_string (String.capitalize (string_of_id id)) + +(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *) +let pr_upper_id id = str (String.capitalize (string_of_id id)) + + +(*s de Bruijn environments for programs *) + +type env = identifier list * Idset.t + +(*s Generic renaming issues for local variable names. *) + +let rec rename_id id avoid = + if Idset.mem id avoid then rename_id (lift_ident id) avoid else id + +let rec rename_vars avoid = function + | [] -> + [], avoid + | id :: idl when id == dummy_name -> + (* we don't rename dummy binders *) + let (idl', avoid') = rename_vars avoid idl in + (id :: idl', avoid') + | id :: idl -> + let (idl, avoid) = rename_vars avoid idl in + let id = rename_id (lowercase_id id) avoid in + (id :: idl, Idset.add id avoid) + +let rename_tvars avoid l = + let rec rename avoid = function + | [] -> [],avoid + | id :: idl -> + let id = rename_id (lowercase_id id) avoid in + let idl, avoid = rename (Idset.add id avoid) idl in + (id :: idl, avoid) in + fst (rename avoid l) + +let push_vars ids (db,avoid) = + let ids',avoid' = rename_vars avoid ids in + ids', (ids' @ db, avoid') + +let get_db_name n (db,_) = + let id = List.nth db (pred n) in + if id = dummy_name then id_of_string "__" else id + + +(*S Renamings of global objects. *) (*s Tables of global renamings *) let keywords = ref Idset.empty +let set_keywords kws = keywords := kws + let global_ids = ref Idset.empty -let modular = ref false +let add_global_ids s = global_ids := Idset.add s !global_ids +let global_ids_list () = Idset.elements !global_ids + +let empty_env () = [], !global_ids + +let mktable () = + let h = Hashtbl.create 97 in + (Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h) + +let mkset () = + let h = Hashtbl.create 97 in + (fun x -> Hashtbl.add h x ()), (Hashtbl.mem h), (fun () -> Hashtbl.clear h) + +let mktriset () = + let h = Hashtbl.create 97 in + (fun x y z -> Hashtbl.add h (x,y,z) ()), + (fun x y z -> Hashtbl.mem h (x,y,z)), + (fun () -> Hashtbl.clear h) (* For each [global_reference], this table will contain the different parts - of its renamings, in [string list] form. *) -let renamings = Hashtbl.create 97 -let rename r l = Hashtbl.add renamings r l -let get_renamings r = Hashtbl.find renamings r + of its renaming, in [string list] form. *) +let add_renaming, get_renaming, clear_renaming = mktable () (* Idem for [module_path]. *) -let mp_renamings = Hashtbl.create 97 -let mp_rename mp l = Hashtbl.add mp_renamings mp l -let mp_get_renamings mp = Hashtbl.find mp_renamings mp +let add_mp_renaming, get_mp_renaming, clear_mp_renaming = mktable () -let modvisited = ref MPset.empty -let modcontents = ref Gset.empty -let add_module_contents mp s = modcontents := Gset.add (mp,s) !modcontents -let module_contents mp s = Gset.mem (mp,s) !modcontents +(* A table for function modfstlev_rename *) +let add_modfstlev, get_modfstlev, clear_modfstlev = mktable () -let to_qualify = ref Refset.empty +(* A set of all external objects that will have to be fully qualified *) +let add_static_clash, static_clash, clear_static_clash = mkset () -let mod_1st_level = ref Idmap.empty +(* Two tables of triplets [kind * module_path * string]. The first one + will record the first level of all MPfile, not only the current one. + The second table will contains local renamings. *) -(*s Uppercase/lowercase renamings. *) +type kind = Term | Type | Cons | Mod -let is_upper s = match s.[0] with 'A' .. 'Z' -> true | _ -> false +let add_ext_mpmem, ext_mpmem, clear_ext_mpmem = mktriset () +let add_loc_mpmem, loc_mpmem, clear_loc_mpmem = mktriset () -let is_lower s = match s.[0] with 'a' .. 'z' | '_' -> true | _ -> false +(* The list of external modules that will be opened initially *) +let add_mpfiles, mem_mpfiles, list_mpfiles, clear_mpfiles = + let m = ref MPset.empty in + (fun mp -> m:= MPset.add mp !m), + (fun mp -> MPset.mem mp !m), + (fun () -> MPset.elements !m), + (fun () -> m:= MPset.empty) + +(*s table containing the visible horizon at a precise moment *) + +let visible = ref ([] : module_path list) +let pop_visible () = visible := List.tl !visible +let push_visible mp = visible := mp :: !visible +let top_visible_mp () = List.hd !visible + +(*s substitutions for printing signatures *) + +let substs = ref empty_subst +let add_subst msid mp = substs := add_msid msid mp !substs +let subst_mp mp = subst_mp !substs mp +let subst_kn kn = subst_kn !substs kn +let subst_con c = fst (subst_con !substs c) +let subst_ref = function + | ConstRef con -> ConstRef (subst_con con) + | IndRef (kn,i) -> IndRef (subst_kn kn,i) + | ConstructRef ((kn,i),j) -> ConstructRef ((subst_kn kn,i),j) + | _ -> assert false + + +let duplicate_index = ref 0 +let to_duplicate = ref Gmap.empty +let add_duplicate mp l = + incr duplicate_index; + let ren = "Coq__" ^ string_of_int (!duplicate_index) in + to_duplicate := Gmap.add (mp,l) ren !to_duplicate +let check_duplicate mp l = + let mp' = subst_mp mp in + Gmap.find (mp',l) !to_duplicate + +type reset_kind = OnlyLocal | AllButExternal | Everything + +let reset_allbutext () = + clear_loc_mpmem (); + global_ids := !keywords; + clear_renaming (); + clear_mp_renaming (); + clear_modfstlev (); + clear_static_clash (); + clear_mpfiles (); + duplicate_index := 0; + to_duplicate := Gmap.empty; + visible := []; + substs := empty_subst + +let reset_everything () = reset_allbutext (); clear_ext_mpmem () + +let reset_renaming_tables = function + | OnlyLocal -> clear_loc_mpmem () + | AllButExternal -> reset_allbutext () + | Everything -> reset_everything () + +(*S Renaming functions *) (* This function creates from [id] a correct uppercase/lowercase identifier. This is done by adding a [Coq_] or [coq_] prefix. To avoid potential clashes @@ -69,389 +245,237 @@ let modular_rename up id = then prefix ^ s else s -let rename_module = modular_rename true - -(* [clash mp0 l s mpl] checks if [mp0-l-s] can be printed as [l-s] when - [mpl] is the context of visible modules. More precisely, we check if - there exists a mp1, module (sub-)path of an element of [mpl], such as - module [mp1-l] contains [s]. - The verification stops if we encounter [mp1=mp0]. *) - -exception Stop - -let clash mp0 l s mpl = - let rec clash_one mp = match mp with - | _ when mp = mp0 -> raise Stop - | MPdot (mp',_) -> - (module_contents (add_labels_mp mp l) s) || (clash_one mp') - | mp when is_toplevel mp -> false - | _ -> module_contents (add_labels_mp mp l) s +(*s [record_contents_fstlev] finds the names of the first-level objects + exported by the ground-level modules in [struc]. *) + +let rec record_contents_fstlev struc = + let upper_type = (lang () = Haskell) in + let addtyp mp id = add_ext_mpmem Type mp (modular_rename upper_type id) in + let addcons mp id = add_ext_mpmem Cons mp (modular_rename true id) in + let addterm mp id = add_ext_mpmem Term mp (modular_rename false id) in + let addmod mp id = add_ext_mpmem Mod mp (modular_rename true id) in + let addfix mp r = + add_ext_mpmem Term mp (modular_rename false (id_of_global r)) in - let rec clash_list = function - | [] -> false - | mp :: mpl -> (clash_one mp) || (clash_list mpl) - in try clash_list mpl with Stop -> false - -(*s [contents_first_level mp] finds the names of the first-level objects - exported by module [mp]. Nota: it might fail if [mp] isn't a directly - visible module. Ex: [MPself] under functor, [MPbound], etc ... *) - -let contents_first_level mp = - if not (MPset.mem mp !modvisited) then begin - modvisited := MPset.add mp !modvisited; - match (Global.lookup_module mp).mod_type with - | MTBsig (msid,msb) -> - let add b id = add_module_contents mp (modular_rename b id) in - let upper_type = (lang () = Haskell) in - List.iter - (function - | (l, SPBconst cb) -> - (match Extraction.constant_kind (Global.env ()) cb with - | Extraction.Logical -> () - | Extraction.Type -> add upper_type (id_of_label l) - | Extraction.Term -> add false (id_of_label l)) - | (_, SPBmind mib) -> - Array.iter - (fun mip -> if snd (Inductive.mind_arity mip) <> InProp - then begin - add upper_type mip.mind_typename; - Array.iter (add true) mip.mind_consnames - end) - mib.mind_packets - | _ -> ()) - (Modops.subst_signature_msid msid mp msb) - | _ -> () - end + let f mp = function + | (l,SEdecl (Dind (_,ind))) -> + Array.iter + (fun ip -> + addtyp mp ip.ip_typename; Array.iter (addcons mp) ip.ip_consnames) + ind.ind_packets + | (l,SEdecl (Dtype _)) -> addtyp mp (id_of_label l) + | (l,SEdecl (Dterm _)) -> addterm mp (id_of_label l) + | (l,SEdecl (Dfix (rv,_,_))) -> Array.iter (addfix mp) rv + | (l,SEmodule _) -> addmod mp (id_of_label l) + | (l,SEmodtype _) -> addmod mp (id_of_label l) + in + List.iter (fun (mp,sel) -> List.iter (f mp) sel) struc -(*s Initial renamings creation, for modular extraction. *) +(*s For monolithic extraction, first-level modules might have to be renamed + with unique numbers *) + +let modfstlev_rename l = + let coqid = id_of_string "Coq" in + let id = id_of_label l in + try + let coqset = get_modfstlev id in + let nextcoq = next_ident_away coqid coqset in + add_modfstlev id (nextcoq::coqset); + (string_of_id nextcoq)^"_"^(string_of_id id) + with Not_found -> + let s = string_of_id id in + if is_lower s || begins_with_CoqXX s then + (add_modfstlev id [coqid]; "Coq_"^s) + else + (add_modfstlev id []; s) + +(*s Creating renaming for a [module_path] *) -let rec mp_create_modular_renamings mp = - try mp_get_renamings mp +let rec mp_create_renaming mp = + try get_mp_renaming mp with Not_found -> let ren = match mp with + | _ when not (modular ()) && at_toplevel mp -> [""] | MPdot (mp,l) -> - (rename_module (id_of_label l)) :: (mp_create_modular_renamings mp) - | MPself msid -> [rename_module (id_of_msid msid)] - | MPbound mbid -> [rename_module (id_of_mbid mbid)] - | MPfile f -> [String.capitalize (string_of_id (List.hd (repr_dirpath f)))] - in mp_rename mp ren; ren + let lmp = mp_create_renaming mp in + if lmp = [""] then (modfstlev_rename l)::lmp + else (modular_rename true (id_of_label l))::lmp + | MPself msid -> [modular_rename true (id_of_msid msid)] + | MPbound mbid -> [modular_rename true (id_of_mbid mbid)] + | MPfile _ when not (modular ()) -> assert false + | MPfile _ -> [string_of_modfile mp] + in add_mp_renaming mp ren; ren + +(* [clash mp0 s mpl] checks if [mp0-s] can be printed as [s] when + [mpl] is the context of visible modules. More precisely, we check if + there exists a [mp] in [mpl] that contains [s]. + The verification stops if we encounter [mp=mp0]. *) +let rec clash mem mp0 s = function + | [] -> false + | mp :: _ when mp = mp0 -> false + | mp :: mpl -> mem mp s || clash mem mp0 s mpl + +(*s Initial renamings creation, for modular extraction. *) let create_modular_renamings struc = let current_module = fst (List.hd struc) in - let modfiles = ref MPset.empty in - let { up = u ; down = d } = struct_get_references_set struc + let { typ = ty ; trm = tr ; cons = co } = struct_get_references_set struc in (* 1) creates renamings of objects *) let add upper r = let mp = modpath_of_r r in - let l = mp_create_modular_renamings mp in + let l = mp_create_renaming mp in let s = modular_rename upper (id_of_global r) in - global_ids := Idset.add (id_of_string s) !global_ids; - rename r (s::l); + add_global_ids (id_of_string s); + add_renaming r (s::l); begin try - let mp = modfile_of_mp mp in - if mp <> current_module then modfiles := MPset.add mp !modfiles + let mp = modfile_of_mp mp in if mp <> current_module then add_mpfiles mp with Not_found -> () end; in - Refset.iter (add true) u; - Refset.iter (add false) d; + Refset.iter (add (lang () = Haskell)) ty; + Refset.iter (add true) co; + Refset.iter (add false) tr; (* 2) determines the opened libraries. *) - let used_modules = MPset.elements !modfiles in - - (* [s] will contain all first-level sub-modules of [cur_mp] *) - let s = ref Stringset.empty in - begin - let add l = s := Stringset.add (rename_module (id_of_label l)) !s in - match (Global.lookup_module current_module).mod_type with - | MTBsig (_,msb) -> - List.iter (function (l,SPBmodule _) -> add l | _ -> ()) msb - | _ -> () - end; - (* We now compare [s] with the modules coming from [used_modules]. *) - List.iter - (function - | MPfile d -> - let s_mp = - String.capitalize (string_of_id (List.hd (repr_dirpath d))) in - if Stringset.mem s_mp !s then error_module_clash s_mp - else s:= Stringset.add s_mp !s - | _ -> assert false) - used_modules; + let used_modules = list_mpfiles () in + let used_modules' = List.rev used_modules in + let str_list = List.map string_of_modfile used_modules' + in + let rec check_elsewhere mpl sl = match mpl, sl with + | [], [] -> [] + | mp::mpl, _::sl -> + if List.exists (ext_mpmem Mod mp) sl then + check_elsewhere mpl sl + else mp :: (check_elsewhere mpl sl) + | _ -> assert false + in + let opened_modules = check_elsewhere used_modules' str_list in + clear_mpfiles (); + List.iter add_mpfiles opened_modules; (* 3) determines the potential clashes *) - List.iter contents_first_level used_modules; - let used_modules' = List.rev used_modules in - let needs_qualify r = + let needs_qualify k r = let mp = modpath_of_r r in if (is_modfile mp) && mp <> current_module && - (clash mp [] (List.hd (get_renamings r)) used_modules') - then to_qualify := Refset.add r !to_qualify + (clash (ext_mpmem k) mp (List.hd (get_renaming r)) opened_modules) + then add_static_clash r in - Refset.iter needs_qualify u; - Refset.iter needs_qualify d; - used_modules + Refset.iter (needs_qualify Type) ty; + Refset.iter (needs_qualify Term) tr; + Refset.iter (needs_qualify Cons) co; + List.rev opened_modules (*s Initial renamings creation, for monolithic extraction. *) -let begins_with_CoqXX s = - (String.length s >= 4) && - (String.sub s 0 3 = "Coq") && - (try - for i = 4 to (String.index s '_')-1 do - match s.[i] with - | '0'..'9' -> () - | _ -> raise Not_found - done; - true - with Not_found -> false) - -let mod_1st_level_rename l = - let coqid = id_of_string "Coq" in - let id = id_of_label l in - try - let coqset = Idmap.find id !mod_1st_level in - let nextcoq = next_ident_away coqid coqset in - mod_1st_level := Idmap.add id (nextcoq::coqset) !mod_1st_level; - (string_of_id nextcoq)^"_"^(string_of_id id) - with Not_found -> - let s = string_of_id id in - if is_lower s || begins_with_CoqXX s then - (mod_1st_level := Idmap.add id [coqid] !mod_1st_level; "Coq_"^s) - else - (mod_1st_level := Idmap.add id [] !mod_1st_level; s) - -let rec mp_create_mono_renamings mp = - try mp_get_renamings mp - with Not_found -> - let ren = match mp with - | _ when (at_toplevel mp) -> [""] - | MPdot (mp,l) -> - let lmp = mp_create_mono_renamings mp in - if lmp = [""] then (mod_1st_level_rename l)::lmp - else (rename_module (id_of_label l))::lmp - | MPself msid -> [rename_module (id_of_msid msid)] - | MPbound mbid -> [rename_module (id_of_mbid mbid)] - | _ -> assert false - in mp_rename mp ren; ren - let create_mono_renamings struc = - let { up = u ; down = d } = struct_get_references_list struc in + let { typ = ty ; trm = tr ; cons = co } = struct_get_references_list struc in let add upper r = let mp = modpath_of_r r in - let l = mp_create_mono_renamings mp in + let l = mp_create_renaming mp in let mycase = if upper then uppercase_id else lowercase_id in let id = if l = [""] then - next_ident_away (mycase (id_of_global r)) (Idset.elements !global_ids) + next_ident_away (mycase (id_of_global r)) (global_ids_list ()) else id_of_string (modular_rename upper (id_of_global r)) in - global_ids := Idset.add id !global_ids; - rename r ((string_of_id id)::l) + add_global_ids id; + add_renaming r ((string_of_id id)::l) in - List.iter (add true) (List.rev u); - List.iter (add false) (List.rev d) - -(*s Renaming issues at toplevel *) - -module TopParams = struct - let globals () = Idset.empty - let pp_global _ r = pr_id (id_of_global r) - let pp_module _ mp = str (string_of_mp mp) -end - -(*s Renaming issues for a monolithic or modular extraction. *) - -module StdParams = struct - - let globals () = !global_ids - - let unquote s = - if lang () <> Scheme then s - else - let s = String.copy s in - for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done; - s - - let rec dottify = function - | [] -> assert false - | [s] -> unquote s - | s::[""] -> unquote s - | s::l -> (dottify l)^"."^(unquote s) - - let pp_global mpl r = - let ls = get_renamings r in - let s = List.hd ls in - let mp = modpath_of_r r in - let ls = - if mp = List.hd mpl then [s] (* simpliest situation *) - else match lang () with - | Scheme -> [s] (* no modular Scheme extraction... *) - | Toplevel -> [s] (* idem *) - | Haskell -> - if !modular then - ls (* for the moment we always qualify in modular Haskell *) - else [s] - | Ocaml -> - try (* has [mp] something in common with one of those in [mpl] ? *) - let pref = common_prefix_from_list mp mpl in - (*i TODO: possibilité de clash i*) - list_firstn ((mp_length mp)-(mp_length pref)+1) ls - with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base = base_mp mp in - if !modular && - (at_toplevel mp) && - not (Refset.mem r !to_qualify) && - not (clash base [] s mpl) - then snd (list_sep_last ls) - else ls - in - add_module_contents mp s; (* update the visible environment *) - str (dottify ls) - - (* The next function is used only in Ocaml extraction...*) - let pp_module mpl mp = - let ls = - if !modular - then mp_create_modular_renamings mp - else mp_create_mono_renamings mp - in - let ls = - try (* has [mp] something in common with one of those in [mpl] ? *) - let pref = common_prefix_from_list mp mpl in - (*i TODO: clash possible i*) - list_firstn ((mp_length mp)-(mp_length pref)) ls - with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - if !modular && (at_toplevel mp) - then snd (list_sep_last ls) - else ls - in str (dottify ls) - -end - -module ToplevelPp = Ocaml.Make(TopParams) -module OcamlPp = Ocaml.Make(StdParams) -module HaskellPp = Haskell.Make(StdParams) -module SchemePp = Scheme.Make(StdParams) - -let pp_decl mp d = match lang () with - | Ocaml -> OcamlPp.pp_decl mp d - | Haskell -> HaskellPp.pp_decl mp d - | Scheme -> SchemePp.pp_decl mp d - | Toplevel -> ToplevelPp.pp_decl mp d - -let pp_struct s = match lang () with - | Ocaml -> OcamlPp.pp_struct s - | Haskell -> HaskellPp.pp_struct s - | Scheme -> SchemePp.pp_struct s - | Toplevel -> ToplevelPp.pp_struct s - -let pp_signature s = match lang () with - | Ocaml -> OcamlPp.pp_signature s - | Haskell -> HaskellPp.pp_signature s - | _ -> assert false - -let set_keywords () = - (match lang () with - | Ocaml -> keywords := Ocaml.keywords - | Haskell -> keywords := Haskell.keywords - | Scheme -> keywords := Scheme.keywords - | Toplevel -> keywords := Idset.empty); - global_ids := !keywords; - to_qualify := Refset.empty + List.iter (add (lang () = Haskell)) (List.rev ty); + List.iter (add false) (List.rev tr); + List.iter (add true) (List.rev co); + [] + +let create_renamings struc = + if modular () then create_modular_renamings struc + else create_mono_renamings struc -let preamble prm = match lang () with - | Ocaml -> Ocaml.preamble prm - | Haskell -> Haskell.preamble prm - | Scheme -> Scheme.preamble prm - | Toplevel -> (fun _ _ _ -> mt ()) - -let preamble_sig prm = match lang () with - | Ocaml -> Ocaml.preamble_sig prm - | _ -> assert false - -(*S Extraction of one decl to stdout. *) - -let print_one_decl struc mp decl = - set_keywords (); - modular := false; - create_mono_renamings struc; - msgnl (pp_decl [mp] decl) - -(*S Extraction to a file. *) - -let info f = - Options.if_verbose msgnl - (str ("The file "^f^" has been created by extraction.")) - -let print_structure_to_file f prm struc = - Hashtbl.clear renamings; - mod_1st_level := Idmap.empty; - modcontents := Gset.empty; - modvisited := MPset.empty; - set_keywords (); - modular := prm.modular; - let used_modules = - if lang () = Toplevel then [] - else if prm.modular then create_modular_renamings struc - else (create_mono_renamings struc; []) - in - let print_dummys = - (struct_ast_search ((=) MLdummy) struc, - struct_type_search Mlutil.isDummy struc, - struct_type_search ((=) Tunknown) struc) - in - let print_magic = - if lang () <> Haskell then false - else struct_ast_search (function MLmagic _ -> true | _ -> false) struc - in - (* print the implementation *) - let cout = option_map (fun (f,_) -> open_out f) f in - let ft = match cout with - | None -> !Pp_control.std_ft - | Some cout -> Pp_control.with_output_to cout in - begin try - msg_with ft (preamble prm used_modules print_dummys print_magic); - msg_with ft (pp_struct struc); - option_iter close_out cout; - with e -> - option_iter close_out cout; raise e - end; - option_iter (fun (f,_) -> info f) f; - (* print the signature *) - match f with - | Some (_,f) when lang () = Ocaml -> - let cout = open_out f in - let ft = Pp_control.with_output_to cout in - begin try - msg_with ft (preamble_sig prm used_modules print_dummys); - msg_with ft (pp_signature (signature_of_structure struc)); - close_out cout; - with e -> - close_out cout; raise e - end; - info f - | _ -> () - - -(*i - (* DO NOT REMOVE: used when making names resolution *) - let cout = open_out (f^".ren") in - let ft = Pp_control.with_output_to cout in - Hashtbl.iter - (fun r id -> - if short_module r = !current_module then - msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r))) - renamings; - pp_flush_with ft (); - close_out cout; -i*) - - - - - - + +(*s On-the-fly qualification issues for both monolithic or modular extraction. *) + +let pp_global k r = + let ls = get_renaming r in + assert (List.length ls > 1); + let s = List.hd ls in + let mp = modpath_of_r r in + if mp = top_visible_mp () then + (* simpliest situation: definition of r (or use in the same context) *) + (* we update the visible environment *) + (add_loc_mpmem k mp s; unquote s) + else match lang () with + | Scheme -> unquote s (* no modular Scheme extraction... *) + | Haskell -> + (* for the moment we always qualify in modular Haskell *) + if modular () then dottify ls else s + | Ocaml -> + try (* has [mp] something in common with one of [!visible] ? *) + let prefix = common_prefix_from_list mp !visible in + let delta = mp_length mp - mp_length prefix in + let ls = list_firstn (delta+1) ls in + (* Difficulty: in ocaml we cannot qualify more than [ls], + but this (not-so-long) name can in fact be hidden. Solution: + duplication of the _definition_ of r in a Coq__XXX module *) + let s,ls' = list_sep_last ls in + let k' = if ls' = [] then k else Mod in + if clash (loc_mpmem k') prefix s !visible then + let front = if ls' = [] then [s] else ls' in + let l = get_nth_label delta r in + try dottify (front @ [check_duplicate prefix l]) + with Not_found -> add_duplicate prefix l; dottify ls + else dottify ls + with Not_found -> + (* [mp] belongs to a closed module, not one of [!visible]. *) + let base = base_mp mp in + let base_s,ls1 = list_sep_last ls in + let s,ls2 = list_sep_last ls1 in + let k' = if ls2 = [] then k else Mod in + if modular () && (mem_mpfiles base) && + not (static_clash r) && + (* k' = Mod can't clash in an opened module, see earlier check *) + not (clash (loc_mpmem k') base s !visible) + then (* Standard situation of an object in another file: *) + (* Thanks to the "open" of this file we remove its name *) + dottify ls1 + else if clash (loc_mpmem Mod) base base_s !visible then + error_module_clash base_s + else dottify ls + +(* The next function is used only in Ocaml extraction...*) +let pp_module mp = + let ls = mp_create_renaming mp in + if List.length ls = 1 then dottify ls + else match mp with + | MPdot (mp0,_) when mp0 = top_visible_mp () -> + (* simpliest situation: definition of mp (or use in the same context) *) + (* we update the visible environment *) + let s = List.hd ls in + add_loc_mpmem Mod mp0 s; s + | _ -> + try (* has [mp] something in common with one of those in [!visible] ? *) + let prefix = common_prefix_from_list mp !visible in + assert (mp <> prefix); (* no use of mp as whole module from itself *) + let delta = mp_length mp - mp_length prefix in + let ls = list_firstn delta ls in + (* Difficulty: in ocaml we cannot qualify more than [ls], + but this (not-so-long) name can in fact be hidden. Solution: + duplication of the _definition_ of mp via a Coq__XXX module *) + let s,ls' = list_sep_last ls in + if clash (loc_mpmem Mod) prefix s !visible then + let l = get_nth_label_mp delta mp in + try dottify (ls' @ [check_duplicate prefix l]) + with Not_found -> add_duplicate prefix l; dottify ls + else dottify ls + with Not_found -> + (* [mp] belongs to a closed module, not one of [!visible]. *) + let base = base_mp mp in + let base_s,ls' = list_sep_last ls in + let s = fst (list_sep_last ls) in + if modular () && (mem_mpfiles base) && + not (clash (loc_mpmem Mod) base s !visible) + then dottify ls' + else if clash (loc_mpmem Mod) base base_s !visible then + error_module_clash base_s + else dottify ls diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index f35c0dea5..e17326bc9 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -9,13 +9,53 @@ (*i $Id$ i*) open Names +open Libnames open Miniml open Mlutil +open Pp -val print_one_decl : - ml_structure -> module_path -> ml_decl -> unit +val fnl2 : unit -> std_ppcmds +val space_if : bool -> std_ppcmds +val sec_space_if : bool -> std_ppcmds -val print_structure_to_file : - (string * string) option -> extraction_params -> ml_structure -> unit +val pp_par : bool -> std_ppcmds -> std_ppcmds +val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pr_binding : identifier list -> std_ppcmds +val rename_id : identifier -> Idset.t -> identifier +val lowercase_id : identifier -> identifier +val uppercase_id : identifier -> identifier + +val pr_upper_id : identifier -> std_ppcmds + +type env = identifier list * Idset.t +val empty_env : unit -> env + +val rename_vars: Idset.t -> identifier list -> env +val rename_tvars: Idset.t -> identifier list -> identifier list +val push_vars : identifier list -> env -> identifier list * env +val get_db_name : int -> env -> identifier + +val record_contents_fstlev : ml_structure -> unit + +val create_renamings : ml_structure -> module_path list + +type kind = Term | Type | Cons | Mod + +val pp_global : kind -> global_reference -> string +val pp_module : module_path -> string + +val top_visible_mp : unit -> module_path +val push_visible : module_path -> unit +val pop_visible : unit -> unit + +val add_subst : mod_self_id -> module_path -> unit + +val check_duplicate : module_path -> label -> string + +type reset_kind = OnlyLocal | AllButExternal | Everything + +val reset_renaming_tables : reset_kind -> unit + +val set_keywords : Idset.t -> unit diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 0ef993057..953e4930b 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -21,7 +21,9 @@ open Modutil open Common open Mod_subst -(*s Obtaining Coq environment. *) +(***************************************) +(*S Part I: computing Coq environment. *) +(***************************************) let toplevel_env () = let seg = Lib.contents_after None in @@ -156,22 +158,19 @@ let rec extract_msig env mp = function (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmodule {msb_modtype=mtb}) :: msig -> - (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig) + (l,Smodule (extract_mtb env mtb)) :: (extract_msig env mp msig) | (l,SPBmodtype mtb) :: msig -> - (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig) + (l,Smodtype (extract_mtb env mtb)) :: (extract_msig env mp msig) -and extract_mtb env mpo = function +and extract_mtb env = function | MTBident kn -> Visit.add_kn kn; MTident kn | MTBfunsig (mbid, mtb, mtb') -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_mtb env None mtb, - extract_mtb env' None mtb') + MTfunsig (mbid, extract_mtb env mtb, + extract_mtb env' mtb') | MTBsig (msid, msig) -> - let mp, msig = match mpo with - | None -> MPself msid, msig - | Some mp -> mp, Modops.subst_signature_msid msid mp msig - in + let mp = MPself msid in let env' = Modops.add_signature mp msig env in MTsig (msid, extract_msig env' mp msig) @@ -216,19 +215,20 @@ let rec extract_msb env mp all = function let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in if all || Visit.needed_kn kn then - (l,SEmodtype (extract_mtb env None mtb)) :: ms + (l,SEmodtype (extract_mtb env mtb)) :: ms else ms and extract_meb env mpo all = function - | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *) - | MEBident mp -> Visit.add_mp mp; MEident mp + | MEBident mp -> + if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp; + Visit.add_mp mp; MEident mp | MEBapply (meb, meb',_) -> MEapply (extract_meb env None true meb, extract_meb env None true meb') | MEBfunctor (mbid, mtb, meb) -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_mtb env None mtb, + MEfunctor (mbid, extract_mtb env mtb, extract_meb env' None true meb) | MEBstruct (msid, msb) -> let mp,msb = match mpo with @@ -247,7 +247,7 @@ and extract_module env mp all mb = (* a msid different from the one of the module. Here is the patch. *) let mtb = replicate_msid meb mtb in { ml_mod_expr = extract_meb env (Some mp) all meb; - ml_mod_type = extract_mtb env None mtb } + ml_mod_type = extract_mtb env mtb } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false @@ -260,14 +260,118 @@ let mono_environment refs mpl = List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l - +(**************************************) +(*S Part II : Input/Output primitives *) +(**************************************) + +let descr () = match lang () with + | Ocaml -> Ocaml.ocaml_descr + | Haskell -> Haskell.haskell_descr + | Scheme -> Scheme.scheme_descr + +(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli" + Works similarly for the other languages. *) + +let mono_filename f = + let d = descr () in + match f with + | None -> None, None, id_of_string "Main" + | Some f -> + let f = + if Filename.check_suffix f d.file_suffix then + Filename.chop_suffix f d.file_suffix + else f + in + Some (f^d.file_suffix), option_map ((^) f) d.sig_suffix, id_of_string f + +(* Builds a suitable filename from a module id *) + +let module_filename m = + let d = descr () in + let f = if d.capital_file then String.capitalize else String.uncapitalize in + let fn = f (string_of_id m) in + Some (fn^d.file_suffix), option_map ((^) fn) d.sig_suffix, m + +(*s Extraction of one decl to stdout. *) + +let print_one_decl struc mp decl = + let d = descr () in + reset_renaming_tables AllButExternal; + ignore (create_renamings struc); + push_visible mp; + msgnl (d.pp_decl decl); + pop_visible () + +(*s Extraction of a ml struct to a file. *) + +let print_structure_to_file (fn,si,mo) struc = + let d = descr () in + reset_renaming_tables AllButExternal; + let used_modules = create_renamings struc in + let unsafe_needs = { + mldummy = struct_ast_search ((=) MLdummy) struc; + tdummy = struct_type_search Mlutil.isDummy struc; + tunknown = struct_type_search ((=) Tunknown) struc; + magic = + if lang () <> Haskell then false + else struct_ast_search (function MLmagic _ -> true | _ -> false) struc } + in + (* print the implementation *) + let cout = option_map open_out fn in + let ft = match cout with + | None -> !Pp_control.std_ft + | Some cout -> Pp_control.with_output_to cout in + let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in + begin try + msg_with ft (d.preamble mo used_modules unsafe_needs); + msg_with devnull (d.pp_struct struc); (* for computing objects to duplicate *) + reset_renaming_tables OnlyLocal; + msg_with ft (d.pp_struct struc); + option_iter close_out cout; + with e -> + option_iter close_out cout; raise e + end; + option_iter info_file fn; + (* print the signature *) + option_iter + (fun si -> + let cout = open_out si in + let ft = Pp_control.with_output_to cout in + begin try + msg_with ft (d.sig_preamble mo used_modules unsafe_needs); + reset_renaming_tables OnlyLocal; + msg_with ft (d.pp_sig (signature_of_structure struc)); + close_out cout; + with e -> + close_out cout; raise e + end; + info_file si) + si + + +(*********************************************) +(*s Part III: the actual extraction commands *) +(*********************************************) + + +let reset () = + Visit.reset (); reset_tables (); reset_renaming_tables Everything + +let init modular = + check_inside_section (); check_inside_module (); + set_keywords (descr ()).keywords; + set_modular modular; + reset (); + if modular && lang () = Scheme then error_scheme () + + (*s Recursive extraction in the Coq toplevel. The vernacular command is - \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] - to get the saturated environment to extract. *) + \verb!Recursive Extraction! [qualid1] ... [qualidn]. Also used when + extracting to a file with the command: + \verb!Extraction "file"! [qualid1] ... [qualidn]. *) -let mono_extraction (f,m) qualids = - check_inside_section (); - check_inside_module (); +let full_extraction f qualids = + init false; let rec find = function | [] -> [],[] | q::l -> @@ -276,116 +380,44 @@ let mono_extraction (f,m) qualids = let mp = Nametab.locate_module (snd (qualid_of_reference q)) in refs,(mp::mps) with Not_found -> (Nametab.global q)::refs, mps - in + in let refs,mps = find qualids in - let prm = {modular=false; mod_name = m; to_appear= refs} in - let struc = optimize_struct prm None (mono_environment refs mps) in - print_structure_to_file f prm struc; - Visit.reset (); - reset_tables () + let struc = optimize_struct refs (mono_environment refs mps) in + warning_axioms (); + print_structure_to_file (mono_filename f) struc; + reset () -let extraction_rec = mono_extraction (None,id_of_string "Main") -(*s Extraction in the Coq toplevel. We display the extracted term in - Ocaml syntax and we use the Coq printers for globals. The - vernacular command is \verb!Extraction! [qualid]. *) +(*s Simple extraction in the Coq toplevel. The vernacular command + is \verb!Extraction! [qualid]. *) -let extraction qid = - check_inside_section (); - check_inside_module (); +let simple_extraction qid = + init false; try let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in - extraction_rec [qid] + full_extraction None [qid] with Not_found -> let r = Nametab.global qid in if is_custom r then msgnl (str "User defined extraction:" ++ spc () ++ str (find_custom r) ++ fnl ()) else - let prm = - { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let struc = optimize_struct prm None (mono_environment [r] []) in + let struc = optimize_struct [r] (mono_environment [r] []) in let d = get_decl_in_structure r struc in + warning_axioms (); print_one_decl struc (modpath_of_r r) d; - Visit.reset (); - reset_tables () - -(*s Extraction to a file (necessarily recursive). - The vernacular command is - \verb!Extraction "file"! [qualid1] ... [qualidn].*) - -let lang_suffix () = match lang () with - | Ocaml -> ".ml",".mli" - | Haskell -> ".hs",".hi" - | Scheme -> ".scm",".scm" - | Toplevel -> assert false - -let filename f = - let s,s' = lang_suffix () in - if Filename.check_suffix f s then - let f' = Filename.chop_suffix f s in - Some (f,f'^s'),id_of_string f' - else Some (f^s,f^s'),id_of_string f - -let extraction_file f vl = - if lang () = Toplevel then error_toplevel () - else mono_extraction (filename f) vl - -(*s Extraction of a module at the toplevel. *) - -let extraction_module m = - check_inside_section (); - check_inside_module (); - begin match lang () with - | Toplevel -> error_toplevel () - | Scheme -> error_scheme () - | _ -> () - end; - let q = snd (qualid_of_reference m) in - let mp = - try Nametab.locate_module q with Not_found -> error_unknown_module q - in - let b = is_modfile mp in - let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in - Visit.reset (); - Visit.add_mp mp; - let env = Global.env () in - let l = List.rev (environment_until None) in - let struc = - List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l - in - let struc = optimize_struct prm None struc in - let struc = - let bmp = base_mp mp in - try [bmp, List.assoc bmp struc] with Not_found -> assert false - in - print_structure_to_file None prm struc; - Visit.reset (); - reset_tables () + reset () (*s (Recursive) Extraction of a library. The vernacular command is \verb!(Recursive) Extraction Library! [M]. *) -let module_file_name m = match lang () with - | Ocaml -> let f = String.uncapitalize (string_of_id m) in f^".ml", f^".mli" - | Haskell -> let f = String.capitalize (string_of_id m) in f^".hs", f^".hi" - | _ -> assert false - -let dir_module_of_id m = - let q = make_short_qualid m in - try Nametab.full_name_module q with Not_found -> error_unknown_module q - let extraction_library is_rec m = - check_inside_section (); - check_inside_module (); - begin match lang () with - | Toplevel -> error_toplevel () - | Scheme -> error_scheme () - | _ -> () - end; - let dir_m = dir_module_of_id m in - Visit.reset (); + init true; + let dir_m = + let q = make_short_qualid m in + try Nametab.full_name_module q with Not_found -> error_unknown_module q + in Visit.add_mp (MPfile dir_m); let env = Global.env () in let l = List.rev (environment_until (Some dir_m)) in @@ -395,22 +427,20 @@ let extraction_library is_rec m = else l in let struc = List.fold_left select [] l in - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let struc = optimize_struct dummy_prm None struc in + let struc = optimize_struct [] struc in + warning_axioms (); + record_contents_fstlev struc; let rec print = function | [] -> () | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l | (MPfile dir, sel) as e :: l -> let short_m = snd (split_dirpath dir) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - print_structure_to_file (Some f) prm [e]; + print_structure_to_file (module_filename short_m) [e]; print l | _ -> assert false in print struc; - Visit.reset (); - reset_tables () + reset () diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 18b106da2..baf79573f 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -13,8 +13,6 @@ open Names open Libnames -val extraction : reference -> unit -val extraction_rec : reference list -> unit -val extraction_file : string -> reference list -> unit -val extraction_module : reference -> unit +val simple_extraction : reference -> unit +val full_extraction : string option -> reference list -> unit val extraction_library : bool -> identifier -> unit diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 3fa318e7e..77067b2b4 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -337,7 +337,10 @@ and extract_ind env kn = (* kn is supposed to be in long form *) {ind_info = Standard; ind_nparams = npar; ind_packets = packets; - ind_equiv = mib.mind_equiv }; + ind_equiv = match mib.mind_equiv with + | None -> NoEquiv + | Some kn -> Equiv kn + }; (* Second pass: we extract constructors *) for i = 0 to mib.mind_ntypes - 1 do let p = packets.(i) in @@ -421,7 +424,9 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets; - ind_equiv = mib.mind_equiv} + ind_equiv = match mib.mind_equiv with + | None -> NoEquiv + | Some kn -> Equiv kn } in add_ind kn mib i; i @@ -828,18 +833,18 @@ let extract_constant env kn cb = | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with | (Info,TypeScheme) -> - if not (is_custom r) then warning_info_ax r; + if not (is_custom r) then add_info_axiom r; let n = type_scheme_nb_args env typ in let ids = iterate (fun l -> anonymous::l) n [] in Dtype (r, ids, Taxiom) | (Info,Default) -> - if not (is_custom r) then warning_info_ax r; + if not (is_custom r) then add_info_axiom r; let t = snd (record_constant_type env kn (Some typ)) in Dterm (r, MLaxiom, type_expunge env t) | (Logic,TypeScheme) -> - warning_log_ax r; Dtype (r, [], Tdummy Ktype) + add_log_axiom r; Dtype (r, [], Tdummy Ktype) | (Logic,Default) -> - warning_log_ax r; Dterm (r, MLdummy, Tdummy Kother)) + add_log_axiom r; Dterm (r, MLdummy, Tdummy Kother)) | Some body -> (match flag_of_type env typ with | (Logic, Default) -> Dterm (r, MLdummy, Tdummy Kother) @@ -880,24 +885,6 @@ let extract_inductive env kn = ind.ind_packets in { ind with ind_packets = packets } -(*s From a global reference to a ML declaration. *) - -let extract_declaration env r = match r with - | ConstRef kn -> extract_constant env kn (Environ.lookup_constant kn env) - | IndRef (kn,_) -> Dind (kn, extract_inductive env kn) - | ConstructRef ((kn,_),_) -> Dind (kn, extract_inductive env kn) - | VarRef kn -> assert false - -(*s Without doing complete extraction, just guess what a constant would be. *) - -type kind = Logical | Term | Type - -let constant_kind env cb = - match flag_of_type env (Typeops.type_of_constant_type env cb.const_type) with - | (Logic,_) -> Logical - | (Info,TypeScheme) -> Type - | (Info,Default) -> Term - (*s Is a [ml_decl] logical ? *) let logical_decl = function diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index b26a577e2..cb0600d05 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -26,16 +26,6 @@ val extract_fixpoint : val extract_inductive : env -> kernel_name -> ml_ind -(*s ML declaration corresponding to a Coq reference. *) - -val extract_declaration : env -> global_reference -> ml_decl - -(*s Without doing complete extraction, just guess what a constant would be. *) - -type kind = Logical | Term | Type - -val constant_kind : env -> constant_body -> kind - (*s Is a [ml_decl] or a [ml_spec] logical ? *) val logical_decl : ml_decl -> bool diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index 13b29c7b5..cb95808d6 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -31,19 +31,18 @@ VERNAC ARGUMENT EXTEND language | [ "Ocaml" ] -> [ Ocaml ] | [ "Haskell" ] -> [ Haskell ] | [ "Scheme" ] -> [ Scheme ] -| [ "Toplevel" ] -> [ Toplevel ] END (* Extraction commands *) VERNAC COMMAND EXTEND Extraction (* Extraction in the Coq toplevel *) -| [ "Extraction" global(x) ] -> [ extraction x ] -| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ extraction_rec l ] +| [ "Extraction" global(x) ] -> [ simple_extraction x ] +| [ "Recursive" "Extraction" ne_global_list(l) ] -> [ full_extraction None l ] (* Monolithic extraction to a file *) | [ "Extraction" string(f) ne_global_list(l) ] - -> [ extraction_file f l ] + -> [ full_extraction (Some f) l ] END (* Modular extraction (one Coq library = one ML module) *) diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 1e26f6c75..f55bc6feb 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -18,7 +18,7 @@ open Libnames open Table open Miniml open Mlutil -open Ocaml +open Common (*s Haskell renaming issues. *) @@ -30,22 +30,22 @@ let keywords = "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ] Idset.empty -let preamble prm used_modules (mldummy,tdummy,tunknown) magic = +let preamble mod_name used_modules usf = let pp_mp = function | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) | _ -> assert false in - (if not magic then mt () + (if not usf.magic then mt () else str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++ str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n") ++ - str "module " ++ pr_upper_id prm.mod_name ++ str " where" ++ fnl () + str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl () ++ fnl() ++ str "import qualified Prelude" ++ fnl() ++ prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules ++ fnl () ++ - (if not magic then mt () + (if not usf.magic then mt () else str "\ #ifdef __GLASGOW_HASKELL__ import qualified GHC.Base @@ -58,13 +58,11 @@ unsafeCoerce = IOExts.unsafeCoerce ++ fnl() ++ fnl() ++ - (if not mldummy then mt () + (if not usf.mldummy then mt () else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl () ++ fnl()) -let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO" - let pp_abst = function | [] -> (mt ()) | l -> (str "\\" ++ @@ -73,17 +71,11 @@ let pp_abst = function let pr_lower_id id = pr_id (lowercase_id id) -(*s The pretty-printing functor. *) - -module Make = functor(P : Mlpp_param) -> struct - -let local_mpl = ref ([] : module_path list) +(*s The pretty-printer for haskell syntax *) -let pp_global r = +let pp_global k r = if is_inline_custom r then str (find_custom r) - else P.pp_global !local_mpl r - -let empty_env () = [], P.globals() + else str (Common.pp_global k r) (*s Pretty-printing of types. [par] is a boolean indicating whether parentheses are needed or not. *) @@ -96,13 +88,14 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> (try pr_id (List.nth vl (pred i)) with _ -> (str "a" ++ int i)) - | Tglob (r,[]) -> pp_global r + | Tglob (r,[]) -> pp_global Type r | Tglob (r,l) -> if r = IndRef (kn_sig,0) then pp_type true vl (List.hd l) else pp_par par - (pp_global r ++ spc () ++ prlist_with_sep spc (pp_type true vl) l) + (pp_global Type r ++ spc () ++ + prlist_with_sep spc (pp_type true vl) l) | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) @@ -151,15 +144,15 @@ let rec pp_expr par env args = spc () ++ str "in") ++ spc () ++ hov 0 pp_a2))) | MLglob r -> - apply (pp_global r) + apply (pp_global Term r) | MLcons (_,r,[]) -> - assert (args=[]); pp_global r + assert (args=[]); pp_global Cons r | MLcons (_,r,[a]) -> assert (args=[]); - pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a) + pp_par par (pp_global Cons r ++ spc () ++ pp_expr true env [] a) | MLcons (_,r,args') -> assert (args=[]); - pp_par par (pp_global r ++ spc () ++ + pp_par par (pp_global Cons r ++ spc () ++ prlist_with_sep spc (pp_expr true env []) args') | MLcase ((_,factors),t, pv) -> apply (pp_par par' @@ -181,7 +174,7 @@ and pp_pat env factors pv = let pp_one_pat (name,ids,t) = let ids,env' = push_vars (List.rev ids) env in let par = expr_needs_par t in - hov 2 (pp_global name ++ + hov 2 (pp_global Cons name ++ (match ids with | [] -> mt () | _ -> (str " " ++ @@ -234,7 +227,7 @@ let pp_logical_ind packet = let pp_singleton kn packet = let l = rename_tvars keywords packet.ip_vars in let l' = List.rev l in - hov 2 (str "type " ++ pp_global (IndRef (kn,0)) ++ spc () ++ + hov 2 (str "type " ++ pp_global Type (IndRef (kn,0)) ++ spc () ++ prlist_with_sep spc pr_id l ++ (if l <> [] then str " " else mt ()) ++ str "=" ++ spc () ++ pp_type false l' (List.hd packet.ip_types.(0)) ++ fnl () ++ @@ -244,7 +237,7 @@ let pp_singleton kn packet = let pp_one_ind ip pl cv = let pl = rename_tvars keywords pl in let pp_constructor (r,l) = - (pp_global r ++ + (pp_global Cons r ++ match l with | [] -> (mt ()) | _ -> (str " " ++ @@ -252,7 +245,7 @@ let pp_one_ind ip pl cv = (fun () -> (str " ")) (pp_type true pl) l)) in str (if Array.length cv = 0 then "type " else "data ") ++ - pp_global (IndRef ip) ++ str " " ++ + pp_global Type (IndRef ip) ++ str " " ++ prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ (if pl = [] then mt () else str " ") ++ if Array.length cv = 0 then str "= () -- empty inductive" @@ -280,9 +273,7 @@ let rec pp_ind first kn i ind = let pp_string_parameters ids = prlist (fun id -> str id ++ str " ") -let pp_decl mpl = - local_mpl := mpl; - function +let pp_decl = function | Dind (kn,i) when i.ind_info = Singleton -> pp_singleton kn i.ind_packets.(0) ++ fnl () | Dind (kn,i) -> hov 0 (pp_ind true kn 0 i) @@ -299,38 +290,49 @@ let pp_decl mpl = if t = Taxiom then str "= () -- AXIOM TO BE REALIZED\n" else str "=" ++ spc () ++ pp_type false l t in - hov 2 (str "type " ++ pp_global r ++ spc () ++ st) ++ fnl () ++ fnl () + hov 2 (str "type " ++ pp_global Type r ++ spc () ++ st) ++ fnl2 () | Dfix (rv, defs, typs) -> let max = Array.length rv in let rec iter i = if i = max then mt () else - let e = pp_global rv.(i) in + let e = pp_global Term rv.(i) in e ++ str " :: " ++ pp_type false [] typs.(i) ++ fnl () - ++ pp_function (empty_env ()) e defs.(i) ++ fnl () ++ fnl () + ++ pp_function (empty_env ()) e defs.(i) ++ fnl2 () ++ iter (i+1) in iter 0 | Dterm (r, a, t) -> if is_inline_custom r then mt () else - let e = pp_global r in + let e = pp_global Term r in e ++ str " :: " ++ pp_type false [] t ++ fnl () ++ if is_custom r then - hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ()) + hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl2 ()) else - hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ()) + hov 0 (pp_function (empty_env ()) e a ++ fnl2 ()) -let pp_structure_elem mpl = function - | (l,SEdecl d) -> pp_decl mpl d +let pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d | (l,SEmodule m) -> failwith "TODO: Haskell extraction of modules not implemented yet" | (l,SEmodtype m) -> failwith "TODO: Haskell extraction of modules not implemented yet" let pp_struct = - prlist (fun (mp,sel) -> prlist (pp_structure_elem [mp]) sel) - -let pp_signature s = failwith "TODO" - -end - + let pp_sel (mp,sel) = + push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p + in + prlist pp_sel + + +let haskell_descr = { + keywords = keywords; + file_suffix = ".hs"; + capital_file = true; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 430ec1fce..1b5dbc711 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -8,13 +8,5 @@ (*i $Id$ i*) -open Pp -open Names -open Miniml +val haskell_descr : Miniml.language_descr -val keywords : Idset.t - -val preamble : - extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds - -module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index d728a8a14..ef963cc90 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -78,11 +78,16 @@ type ml_ind_packet = { (* [ip_nparams] contains the number of parameters. *) +type equiv = + | NoEquiv + | Equiv of kernel_name + | RenEquiv of string + type ml_ind = { ind_info : inductive_info; ind_nparams : int; ind_packets : ml_ind_packet array; - ind_equiv : kernel_name option + ind_equiv : equiv } (*s ML terms. *) @@ -151,24 +156,28 @@ type ml_structure = (module_path * ml_module_structure) list type ml_signature = (module_path * ml_module_sig) list -(*s Pretty-printing of MiniML in a given concrete syntax is parameterized - by a function [pp_global] that pretty-prints global references. - The resulting pretty-printer is a module of type [Mlpp] providing - functions to print types, terms and declarations. *) - -module type Mlpp_param = sig - val globals : unit -> Idset.t - val pp_global : module_path list -> global_reference -> std_ppcmds - val pp_module : module_path list -> module_path -> std_ppcmds -end - -module type Mlpp = sig - val pp_decl : module_path list -> ml_decl -> std_ppcmds - val pp_struct : ml_structure -> std_ppcmds - val pp_signature : ml_signature -> std_ppcmds -end - -type extraction_params = - { modular : bool; - mod_name : identifier; - to_appear : global_reference list } +type unsafe_needs = { + mldummy : bool; + tdummy : bool; + tunknown : bool; + magic : bool +} + +type language_descr = { + keywords : Idset.t; + + (* Concerning the source file *) + file_suffix : string; + capital_file : bool; (* should we capitalize filenames ? *) + preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + pp_struct : ml_structure -> std_ppcmds; + + (* Concerning a possible interface file *) + sig_suffix : string option; + sig_preamble : identifier -> module_path list -> unsafe_needs -> std_ppcmds; + pp_sig : ml_signature -> std_ppcmds; + + (* for an isolated declaration print *) + pp_decl : ml_decl -> std_ppcmds; + +} diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 87713e4d5..760f76c9a 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -86,56 +86,6 @@ let rec replicate_msid meb mtb = match meb,mtb with if msig' == msig then MTBsig (msid, msig) else MTBsig (msid, msig') | _ -> mtb - -(*S More functions concerning [module_path]. *) - -let rec mp_length = function - | MPdot (mp, _) -> 1 + (mp_length mp) - | _ -> 1 - -let rec prefixes_mp mp = match mp with - | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') - | _ -> MPset.singleton mp - -let rec common_prefix prefixes_mp1 mp2 = - if MPset.mem mp2 prefixes_mp1 then mp2 - else match mp2 with - | MPdot (mp,_) -> common_prefix prefixes_mp1 mp - | _ -> raise Not_found - -let common_prefix_from_list mp0 mpl = - let prefixes_mp0 = prefixes_mp mp0 in - let rec f = function - | [] -> raise Not_found - | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l - in f mpl - -let rec modfile_of_mp mp = match mp with - | MPfile _ -> mp - | MPdot (mp,_) -> modfile_of_mp mp - | _ -> raise Not_found - -let rec parse_labels ll = function - | MPdot (mp,l) -> parse_labels (l::ll) mp - | mp -> mp,ll - -let labels_of_mp mp = parse_labels [] mp - -let labels_of_ref r = - let mp,_,l = - match r with - ConstRef con -> repr_con con - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_kn kn - | VarRef _ -> assert false - in - parse_labels [l] mp - -let rec add_labels_mp mp = function - | [] -> mp - | l :: ll -> add_labels_mp (MPdot (mp,l)) ll - - (*S Functions upon ML modules. *) (*s Apply some functions upon all [ml_decl] and [ml_spec] found in a @@ -200,7 +150,9 @@ let ind_iter_references do_term do_cons do_type kn ind = let packet_iter ip p = do_type (IndRef ip); if lang () = Ocaml then - option_iter (fun kne -> do_type (IndRef (kne,snd ip))) ind.ind_equiv; + (match ind.ind_equiv with + | Equiv kne -> do_type (IndRef (kne, snd ip)); + | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in if lang () = Ocaml then record_iter_references do_term ind.ind_info; @@ -228,13 +180,13 @@ let struct_iter_references do_term do_cons do_type = (*s Get all references used in one [ml_structure], either in [list] or [set]. *) -type 'a updown = { mutable up : 'a ; mutable down : 'a } +type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a } let struct_get_references empty add struc = - let o = { up = empty ; down = empty } in - let do_term r = o.down <- add r o.down in - let do_cons r = o.up <- add r o.up in - let do_type = if lang () = Haskell then do_cons else do_term in + let o = { typ = empty ; trm = empty ; cons = empty } in + let do_type r = o.typ <- add r o.typ in + let do_term r = o.trm <- add r o.trm in + let do_cons r = o.cons <- add r o.cons in struct_iter_references do_term do_cons do_type struc; o let struct_get_references_set = struct_get_references Refset.empty Refset.add @@ -251,7 +203,9 @@ end let struct_get_references_list struc = let o = struct_get_references Orefset.empty Orefset.add struc in - { up = Orefset.list o.up; down = Orefset.list o.down } + { typ = Orefset.list o.typ; + trm = Orefset.list o.trm; + cons = Orefset.list o.cons } (*s Searching occurrences of a particular term (no lifting done). *) @@ -363,38 +317,40 @@ let dfix_to_mlfix rv av i = let c = Array.map (subst 0) av in MLfix(i, ids, c) -let rec optim prm s = function +let rec optim to_appear s = function | [] -> [] | (Dtype (r,_,Tdummy _) | Dterm(r,MLdummy,_)) as d :: l -> - if List.mem r prm.to_appear then d :: (optim prm s l) else optim prm s l + if List.mem r to_appear + then d :: (optim to_appear s l) + else optim to_appear s l | Dterm (r,t,typ) :: l -> let t = normalize (ast_glob_subst !s t) in let i = inline r t in if i then s := Refmap.add r t !s; - if not i || prm.modular || List.mem r prm.to_appear + if not i || modular () || List.mem r to_appear then let d = match optimize_fix t with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|typ|]) | t -> Dterm (r, t, typ) - in d :: (optim prm s l) - else optim prm s l - | d :: l -> d :: (optim prm s l) + in d :: (optim to_appear s l) + else optim to_appear s l + | d :: l -> d :: (optim to_appear s l) -let rec optim_se top prm s = function +let rec optim_se top to_appear s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> let a = normalize (ast_glob_subst !s a) in let i = inline r a in if i then s := Refmap.add r a !s; - if top && i && not prm.modular && not (List.mem r prm.to_appear) - then optim_se top prm s lse + if top && i && not (modular ()) && not (List.mem r to_appear) + then optim_se top to_appear s lse else let d = match optimize_fix a with | MLfix (0, _, [|c|]) -> Dfix ([|r|], [|ast_subst (MLglob r) c|], [|t|]) | a -> Dterm (r, a, t) - in (l,SEdecl d) :: (optim_se top prm s lse) + in (l,SEdecl d) :: (optim_se top to_appear s lse) | (l,SEdecl (Dfix (rv,av,tv))) :: lse -> let av = Array.map (fun a -> normalize (ast_glob_subst !s a)) av in let all = ref true in @@ -405,22 +361,22 @@ let rec optim_se top prm s = function then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; - if !all && top && not prm.modular - && (array_for_all (fun r -> not (List.mem r prm.to_appear)) rv) - then optim_se top prm s lse - else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top prm s lse) + if !all && top && not (modular ()) + && (array_for_all (fun r -> not (List.mem r to_appear)) rv) + then optim_se top to_appear s lse + else (l,SEdecl (Dfix (rv, av, tv))) :: (optim_se top to_appear s lse) | (l,SEmodule m) :: lse -> - let m = { m with ml_mod_expr = optim_me prm s m.ml_mod_expr} - in (l,SEmodule m) :: (optim_se top prm s lse) - | se :: lse -> se :: (optim_se top prm s lse) + let m = { m with ml_mod_expr = optim_me to_appear s m.ml_mod_expr} + in (l,SEmodule m) :: (optim_se top to_appear s lse) + | se :: lse -> se :: (optim_se top to_appear s lse) -and optim_me prm s = function - | MEstruct (msid, lse) -> MEstruct (msid, optim_se false prm s lse) +and optim_me to_appear s = function + | MEstruct (msid, lse) -> MEstruct (msid, optim_se false to_appear s lse) | MEident mp as me -> me - | MEapply (me, me') -> MEapply (optim_me prm s me, optim_me prm s me') - | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me) + | MEapply (me, me') -> + MEapply (optim_me to_appear s me, optim_me to_appear s me') + | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me) -let optimize_struct prm before struc = +let optimize_struct to_appear struc = let subst = ref (Refmap.empty : ml_ast Refmap.t) in - option_iter (fun l -> ignore (optim prm subst l)) before; - List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc + List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index 46c7dbc3f..c89590daa 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -33,14 +33,6 @@ val subst_msb : substitution -> module_structure_body -> module_structure_body val replicate_msid : module_expr_body -> module_type_body -> module_type_body -(*s More utilities concerning [module_path]. *) - -val mp_length : module_path -> int -val prefixes_mp : module_path -> MPset.t -val modfile_of_mp : module_path -> module_path -val common_prefix_from_list : module_path -> module_path list -> module_path -val add_labels_mp : module_path -> label list -> module_path - (*s Functions upon ML modules. *) val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool @@ -52,10 +44,10 @@ val decl_iter_references : do_ref -> do_ref -> do_ref -> ml_decl -> unit val spec_iter_references : do_ref -> do_ref -> do_ref -> ml_spec -> unit val struct_iter_references : do_ref -> do_ref -> do_ref -> ml_structure -> unit -type 'a updown = { mutable up : 'a ; mutable down : 'a } +type 'a kinds = { mutable typ : 'a ; mutable trm : 'a; mutable cons : 'a } -val struct_get_references_set : ml_structure -> Refset.t updown -val struct_get_references_list : ml_structure -> global_reference list updown +val struct_get_references_set : ml_structure -> Refset.t kinds +val struct_get_references_list : ml_structure -> global_reference list kinds val signature_of_structure : ml_structure -> ml_signature @@ -65,7 +57,7 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl all beta redexes (when the argument does not occur, it is just thrown away; when it occurs exactly once it is substituted; otherwise a let-in redex is created for clarity) and iota redexes, plus some other - optimizations. *) + optimizations. The first argument is the list of objects we want to appear. +*) -val optimize_struct : - extraction_params -> ml_decl list option -> ml_structure -> ml_structure +val optimize_struct : global_reference list -> ml_structure -> ml_structure diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 600e6ebca..7548c1487 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -19,10 +19,7 @@ open Table open Miniml open Mlutil open Modutil - -(*s Some utility functions. *) - -let pp_par par st = if par then str "(" ++ st ++ str ")" else st +open Common let pp_tvar id = let s = string_of_id id in @@ -52,70 +49,12 @@ let pp_abst = function str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ str " ->" ++ spc () -let pp_apply st par args = match args with - | [] -> st - | _ -> hov 2 (pp_par par (st ++ spc () ++ prlist_with_sep spc identity args)) - -let pr_binding = function - | [] -> mt () - | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l - -let space_if = function true -> str " " | false -> mt () - -let sec_space_if = function true -> spc () | false -> mt () - -let fnl2 () = fnl () ++ fnl () - let pp_parameters l = (pp_boxed_tuple pp_tvar l ++ space_if (l<>[])) let pp_string_parameters l = (pp_boxed_tuple str l ++ space_if (l<>[])) -(*s Generic renaming issues. *) - -let rec rename_id id avoid = - if Idset.mem id avoid then rename_id (lift_ident id) avoid else id - -let lowercase_id id = id_of_string (String.uncapitalize (string_of_id id)) -let uppercase_id id = id_of_string (String.capitalize (string_of_id id)) - -(* [pr_upper_id id] makes 2 String.copy lesser than [pr_id (uppercase_id id)] *) -let pr_upper_id id = str (String.capitalize (string_of_id id)) - -(*s de Bruijn environments for programs *) - -type env = identifier list * Idset.t - -let rec rename_vars avoid = function - | [] -> - [], avoid - | id :: idl when id == dummy_name -> - (* we don't rename dummy binders *) - let (idl', avoid') = rename_vars avoid idl in - (id :: idl', avoid') - | id :: idl -> - let (idl, avoid) = rename_vars avoid idl in - let id = rename_id (lowercase_id id) avoid in - (id :: idl, Idset.add id avoid) - -let rename_tvars avoid l = - let rec rename avoid = function - | [] -> [],avoid - | id :: idl -> - let id = rename_id (lowercase_id id) avoid in - let idl, avoid = rename (Idset.add id avoid) idl in - (id :: idl, avoid) in - fst (rename avoid l) - -let push_vars ids (db,avoid) = - let ids',avoid' = rename_vars avoid ids in - ids', (ids' @ db, avoid') - -let get_db_name n (db,_) = - let id = List.nth db (pred n) in - if id = dummy_name then id_of_string "__" else id - (*s Ocaml renaming issues. *) let keywords = @@ -130,7 +69,7 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules (mldummy,tdummy,tunknown) _ = +let preamble _ used_modules usf = let pp_mp = function | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) | _ -> assert false @@ -139,15 +78,15 @@ let preamble _ used_modules (mldummy,tdummy,tunknown) _ = ++ (if used_modules = [] then mt () else fnl ()) ++ - (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() else mt()) ++ - (if mldummy then + (if usf.mldummy then str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl () else mt ()) ++ - (if tdummy || tunknown || mldummy then fnl () else mt ()) + (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ()) -let preamble_sig _ used_modules (_,tdummy,tunknown) = +let sig_preamble _ used_modules usf = let pp_mp = function | MPfile d -> pr_upper_id (List.hd (repr_dirpath d)) | _ -> assert false @@ -156,18 +95,16 @@ let preamble_sig _ used_modules (_,tdummy,tunknown) = ++ (if used_modules = [] then mt () else fnl ()) ++ - (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () + (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () else mt()) -(*s The pretty-printing functor. *) - -module Make = functor(P : Mlpp_param) -> struct +(*s The pretty-printer for Ocaml syntax*) -let local_mpl = ref ([] : module_path list) - -let pp_global r = +let pp_global k r = if is_inline_custom r then str (find_custom r) - else P.pp_global !local_mpl r + else str (Common.pp_global k r) + +let pp_modname mp = str (Common.pp_module mp) let is_infix r = is_inline_custom r && @@ -177,8 +114,6 @@ let get_infix r = let s = find_custom r in String.sub s 1 (String.length s - 2) -let empty_env () = [], P.globals () - exception NoRecord let find_projections = function Record l -> l | _ -> raise NoRecord @@ -199,12 +134,12 @@ let rec pp_type par vl t = pp_par par (pp_rec true a1 ++ spc () ++ str (get_infix r) ++ spc () ++ pp_rec true a2) - | Tglob (r,[]) -> pp_global r + | Tglob (r,[]) -> pp_global Type r | Tglob (r,l) -> if r = IndRef (kn_sig,0) then pp_tuple_light pp_rec l else - pp_tuple_light pp_rec l ++ spc () ++ pp_global r + pp_tuple_light pp_rec l ++ spc () ++ pp_global Type r | Tarr (t1,t2) -> pp_par par (pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2) @@ -256,18 +191,18 @@ let rec pp_expr par env args = (try let args = list_skipn (projection_arity r) args in let record = List.hd args in - pp_apply (record ++ str "." ++ pp_global r) par (List.tl args) - with _ -> apply (pp_global r)) + pp_apply (record ++ str "." ++ pp_global Term r) par (List.tl args) + with _ -> apply (pp_global Term r)) | MLcons (Coinductive,r,[]) -> assert (args=[]); - pp_par par (str "lazy " ++ pp_global r) + pp_par par (str "lazy " ++ pp_global Cons r) | MLcons (Coinductive,r,args') -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")") + pp_par par (str "lazy (" ++ pp_global Cons r ++ spc() ++ tuple ++str ")") | MLcons (_,r,[]) -> assert (args=[]); - pp_global r + pp_global Cons r | MLcons (Record projs, r, args') -> assert (args=[]); pp_record_pat (projs, List.map (pp_expr true env []) args') @@ -279,7 +214,7 @@ let rec pp_expr par env args = | MLcons (_,r,args') -> assert (args=[]); let tuple = pp_tuple (pp_expr true env []) args' in - pp_par par (pp_global r ++ spc () ++ tuple) + pp_par par (pp_global Cons r ++ spc () ++ tuple) | MLcase ((i,factors), t, pv) -> let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) @@ -293,7 +228,7 @@ let rec pp_expr par env args = match c with | MLrel i when i <= n -> apply (pp_par par' (pp_expr true env [] t ++ str "." ++ - pp_global (List.nth projs (n-i)))) + pp_global Term (List.nth projs (n-i)))) | MLapp (MLrel i, a) when i <= n -> if List.exists (ast_occurs_itvl 1 n) a then raise NoRecord @@ -301,7 +236,7 @@ let rec pp_expr par env args = let ids,env' = push_vars (List.rev ids) env in (pp_apply (pp_expr true env [] t ++ str "." ++ - pp_global (List.nth projs (n-i))) + pp_global Term (List.nth projs (n-i))) par ((List.map (pp_expr true env' []) a) @ args)) | _ -> raise NoRecord with NoRecord -> @@ -336,7 +271,7 @@ let rec pp_expr par env args = and pp_record_pat (projs, args) = str "{ " ++ prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,a) -> pp_global r ++ str " =" ++ spc () ++ a) + (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a) (List.combine projs args) ++ str " }" @@ -350,8 +285,8 @@ and pp_one_pat env i (r,ids,t) = (match List.rev ids with | [i1;i2] when is_infix r -> pr_id i1 ++ str " " ++ str (get_infix r) ++ str " " ++ pr_id i2 - | [] -> pp_global r - | ids -> pp_global r ++ str " " ++ pp_boxed_tuple pr_id ids), + | [] -> pp_global Cons r + | ids -> pp_global Cons r ++ str " " ++ pp_boxed_tuple pr_id ids), expr and pp_pat env (info,factors) pv = @@ -369,23 +304,23 @@ and pp_pat env (info,factors) pv = let t = ast_lift (-List.length ids) t in hov 2 (str "_ ->" ++ spc () ++ pp_expr (expr_needs_par t) env [] t) -and pp_function env f t = +and pp_function env t = let bl,t' = collect_lams t in let bl,env' = push_vars bl env in match t' with | MLcase(i,MLrel 1,pv) when fst i=Standard -> if not (ast_occurs 1 (MLcase(i,MLdummy,pv))) then - (f ++ pr_binding (List.rev (List.tl bl)) ++ - str " = function" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv)) + pr_binding (List.rev (List.tl bl)) ++ + str " = function" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) else - (f ++ pr_binding (List.rev bl) ++ - str " = match " ++ - pr_id (List.hd bl) ++ str " with" ++ fnl () ++ - v 0 (str " | " ++ pp_pat env' i pv)) - | _ -> (f ++ pr_binding (List.rev bl) ++ - str " =" ++ fnl () ++ str " " ++ - hov 2 (pp_expr false env' [] t')) + pr_binding (List.rev bl) ++ + str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ + v 0 (str " | " ++ pp_pat env' i pv) + | _ -> + pr_binding (List.rev bl) ++ + str " =" ++ fnl () ++ str " " ++ + hov 2 (pp_expr false env' [] t') (*s names of the functions ([ids]) are already pushed in [env], and passed here just for convenience. *) @@ -395,54 +330,57 @@ and pp_fix par env i (ids,bl) args = (v 0 (str "let rec " ++ prvect_with_sep (fun () -> fnl () ++ str "and ") - (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (fun (fi,ti) -> pr_id fi ++ pp_function env ti) (array_map2 (fun id b -> (id,b)) ids bl) ++ fnl () ++ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) let pp_val e typ = - str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ - str " **)" ++ fnl2 () + hov 4 (str "(** val " ++ e ++ str " :" ++ spc () ++ pp_type false [] typ ++ + str " **)") ++ fnl2 () (*s Pretty-printing of [Dfix] *) -let rec pp_Dfix init i ((rv,c,t) as fix) = - if i >= Array.length rv then mt () - else - if is_inline_custom rv.(i) then pp_Dfix init (i+1) fix +let pp_Dfix (rv,c,t) = + let names = Array.map + (fun r -> if is_inline_custom r then mt () else pp_global Term r) rv + in + let rec pp sep letand i = + if i >= Array.length rv then mt () + else if is_inline_custom rv.(i) then pp sep letand (i+1) else - let e = pp_global rv.(i) in - (if init then mt () else fnl2 ()) ++ - pp_val e t.(i) ++ - str (if init then "let rec " else "and ") ++ - (if is_custom rv.(i) then e ++ str " = " ++ str (find_custom rv.(i)) - else pp_function (empty_env ()) e c.(i)) ++ - pp_Dfix false (i+1) fix - + let def = + if is_custom rv.(i) then str " = " ++ str (find_custom rv.(i)) + else pp_function (empty_env ()) c.(i) + in + sep () ++ pp_val names.(i) t.(i) ++ + str letand ++ names.(i) ++ def ++ pp fnl2 "and " (i+1) + in pp mt "let rec " 0 + (*s Pretty-printing of inductive types declaration. *) -let pp_equiv param_list = function - | None -> mt () - | Some ip_equiv -> - str " = " ++ pp_parameters param_list ++ pp_global (IndRef ip_equiv) +let pp_equiv param_list name = function + | NoEquiv, _ -> mt () + | Equiv kn, i -> + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (kn,i)) + | RenEquiv ren, _ -> + str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name let pp_comment s = str "(* " ++ s ++ str " *)" -let pp_one_ind prefix ip ip_equiv pl cv = +let pp_one_ind prefix ip_equiv pl name cnames ctyps = let pl = rename_tvars keywords pl in - let pp_constructor (r,l) = - hov 2 (str " | " ++ pp_global r ++ - match l with - | [] -> mt () - | _ -> (str " of " ++ - prlist_with_sep - (fun () -> spc () ++ str "* ") (pp_type true pl) l)) + let pp_constructor i typs = + (if i=0 then mt () else fnl ()) ++ + hov 5 (str " | " ++ cnames.(i) ++ + (if typs = [] then mt () else str " of ") ++ + prlist_with_sep + (fun () -> spc () ++ str "* ") (pp_type true pl) typs) in - pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ - pp_equiv pl ip_equiv ++ str " =" ++ - if Array.length cv = 0 then str " unit (* empty inductive *)" - else fnl () ++ v 0 (prvect_with_sep fnl pp_constructor - (Array.mapi (fun i c -> ConstructRef (ip,i+1), c) cv)) + pp_parameters pl ++ str prefix ++ name ++ + pp_equiv pl name ip_equiv ++ str " =" ++ + if Array.length ctyps = 0 then str " unit (* empty inductive *)" + else fnl () ++ v 0 (prvecti pp_constructor ctyps) let pp_logical_ind packet = pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ @@ -452,38 +390,51 @@ let pp_logical_ind packet = fnl () let pp_singleton kn packet = + let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in - hov 2 (str "type " ++ pp_parameters l ++ - pp_global (IndRef (kn,0)) ++ str " =" ++ spc () ++ + hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ pr_id packet.ip_consnames.(0))) let pp_record kn projs ip_equiv packet = - let l = List.combine projs packet.ip_types.(0) in + let name = pp_global Type (IndRef (kn,0)) in + let projnames = List.map (pp_global Term) projs in + let l = List.combine projnames packet.ip_types.(0) in let pl = rename_tvars keywords packet.ip_vars in - str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ - pp_equiv pl ip_equiv ++ str " = { "++ + str "type " ++ pp_parameters pl ++ name ++ + pp_equiv pl name ip_equiv ++ str " = { "++ hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ()) - (fun (r,t) -> pp_global r ++ str " : " ++ pp_type true pl t) l) + (fun (p,t) -> p ++ str " : " ++ pp_type true pl t) l) ++ str " }" -let pp_coind ip pl = - let r = IndRef ip in +let pp_coind pl name = let pl = rename_tvars keywords pl in - pp_parameters pl ++ pp_global r ++ str " = " ++ - pp_parameters pl ++ str "__" ++ pp_global r ++ str " Lazy.t" ++ + pp_parameters pl ++ name ++ str " = " ++ + pp_parameters pl ++ str "__" ++ name ++ str " Lazy.t" ++ fnl() ++ str "and " let pp_ind co kn ind = let prefix = if co then "__" else "" in let some = ref false in let init= ref (str "type ") in + let names = + Array.mapi (fun i p -> if p.ip_logical then mt () else + pp_global Type (IndRef (kn,i))) + ind.ind_packets + in + let cnames = + Array.mapi + (fun i p -> if p.ip_logical then [||] else + Array.mapi (fun j _ -> pp_global Cons (ConstructRef ((kn,i),j+1))) + p.ip_types) + ind.ind_packets + in let rec pp i = if i >= Array.length ind.ind_packets then mt () else let ip = (kn,i) in - let ip_equiv = option_map (fun kn -> (kn,i)) ind.ind_equiv in + let ip_equiv = ind.ind_equiv, 0 in let p = ind.ind_packets.(i) in if is_custom (IndRef ip) then pp (i+1) else begin @@ -494,8 +445,9 @@ let pp_ind co kn ind = begin init := (fnl () ++ str "and "); s ++ - (if co then pp_coind ip p.ip_vars else mt ()) - ++ pp_one_ind prefix ip ip_equiv p.ip_vars p.ip_types ++ + (if co then pp_coind p.ip_vars names.(i) else mt ()) ++ + pp_one_ind + prefix ip_equiv p.ip_vars names.(i) cnames.(i) p.ip_types ++ pp (i+1) end end @@ -510,159 +462,215 @@ let pp_mind kn i = | Singleton -> pp_singleton kn i.ind_packets.(0) | Coinductive -> pp_ind true kn i | Record projs -> - let ip_equiv = option_map (fun kn -> (kn,0)) i.ind_equiv in - pp_record kn projs ip_equiv i.ind_packets.(0) + pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0) | Standard -> pp_ind false kn i -let pp_decl mpl = - local_mpl := mpl; - function +let pp_decl = function + | Dtype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Dterm (r,_,_) when is_inline_custom r -> failwith "empty phrase" | Dind (kn,i) -> pp_mind kn i - | Dtype (r, l, t) -> - if is_inline_custom r then failwith "empty phrase" - else - let pp_r = pp_global r in - let l = rename_tvars keywords l in - let ids, def = try + | Dtype (r, l, t) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids, def = + try let ids,s = find_type_custom r in pp_string_parameters ids, str "=" ++ spc () ++ str s - with not_found -> + with Not_found -> pp_parameters l, if t = Taxiom then str "(* AXIOM TO BE REALIZED *)" else str "=" ++ spc () ++ pp_type false l t - in - hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++ - spc () ++ def) + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) | Dterm (r, a, t) -> - if is_inline_custom r then failwith "empty phrase" - else - let e = pp_global r in - pp_val e t ++ - hov 0 - (str "let " ++ - if is_custom r then - e ++ str " = " ++ str (find_custom r) - else if is_projection r then - let s = prvecti (fun _ -> str) - (Array.make (projection_arity r) " _") in - e ++ s ++ str " x = x." ++ e - else pp_function (empty_env ()) e a) + let def = + if is_custom r then str (" = " ^ find_custom r) + else if is_projection r then + (prvect str (Array.make (projection_arity r) " _")) ++ + str " x = x." + else pp_function (empty_env ()) a + in + let name = pp_global Term r in + let postdef = if is_projection r then name else mt () in + pp_val name t ++ hov 0 (str "let " ++ name ++ def ++ postdef) | Dfix (rv,defs,typs) -> - pp_Dfix true 0 (rv,defs,typs) - -let pp_spec mpl = - local_mpl := mpl; - function - | Sind (kn,i) -> pp_mind kn i - | Sval (r,t) -> - if is_inline_custom r then failwith "empty phrase" - else - hov 2 (str "val" ++ spc () ++ pp_global r ++ str " :" ++ spc () ++ - pp_type false [] t) - | Stype (r,vl,ot) -> - if is_inline_custom r then failwith "empty phrase" - else - let l = rename_tvars keywords vl in - let ids, def = - try - let ids, s = find_type_custom r in - pp_string_parameters ids, str "= " ++ str s - with not_found -> - let ids = pp_parameters l in - match ot with - | None -> ids, mt () - | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" - | Some t -> ids, str "=" ++ spc () ++ pp_type false l t - in - hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++ spc () ++ def) - -let rec pp_specif mpl = function - | (_,Spec s) -> pp_spec mpl s + pp_Dfix (rv,defs,typs) + +let pp_alias_decl ren = function + | Dind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Dtype (r, l, _) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Dterm (r, a, t) -> + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) + | Dfix (rv, _, _) -> + prvecti (fun i r -> if is_inline_custom r then mt () else + let name = pp_global Term r in + hov 2 (str "let " ++ name ++ str (" = "^ren^".") ++ name) ++ + fnl ()) + rv + +let pp_spec = function + | Sval (r,_) when is_inline_custom r -> failwith "empty phrase" + | Stype (r,_,_) when is_inline_custom r -> failwith "empty phrase" + | Sind (kn,i) -> pp_mind kn i + | Sval (r,t) -> + let def = pp_type false [] t in + let name = pp_global Term r in + hov 2 (str "val " ++ name ++ str " :" ++ spc () ++ def) + | Stype (r,vl,ot) -> + let name = pp_global Type r in + let l = rename_tvars keywords vl in + let ids, def = + try + let ids, s = find_type_custom r in + pp_string_parameters ids, str "= " ++ str s + with Not_found -> + let ids = pp_parameters l in + match ot with + | None -> ids, mt () + | Some Taxiom -> ids, str "(* AXIOM TO BE REALIZED *)" + | Some t -> ids, str "=" ++ spc () ++ pp_type false l t + in + hov 2 (str "type " ++ ids ++ name ++ spc () ++ def) + +let pp_alias_spec ren = function + | Sind (kn,i) -> pp_mind kn { i with ind_equiv = RenEquiv ren } + | Stype (r,l,_) -> + let name = pp_global Type r in + let l = rename_tvars keywords l in + let ids = pp_parameters l in + hov 2 (str "type " ++ ids ++ name ++ str " =" ++ spc () ++ ids ++ + str (ren^".") ++ name) + | Sval _ -> assert false + +let rec pp_specif = function + | (_,Spec (Sval _ as s)) -> pp_spec s + | (l,Spec s) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" : sig ") ++ fnl () ++ pp_spec s) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_spec ren s + with Not_found -> pp_spec s) | (l,Smodule mt) -> - hov 1 - (str "module " ++ - P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " : " ++ fnl () ++ pp_module_type mpl None (* (Some l) *) mt) + let def = pp_module_type (Some l) mt in + let def' = pp_module_type (Some l) mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module " ++ name ++ str " : " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ hov 1 (str ("module "^ren^" : ") ++ fnl () ++ def') + with Not_found -> Pp.mt ()) | (l,Smodtype mt) -> - hov 1 - (str "module type " ++ - P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " = " ++ fnl () ++ pp_module_type mpl None mt) - -and pp_module_type mpl ol = function + let def = pp_module_type None mt in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> Pp.mt ()) + +and pp_module_type ol = function | MTident kn -> - let mp,_,l = repr_kn kn in P.pp_module mpl (MPdot (mp,l)) + let mp,_,l = repr_kn kn in pp_modname (MPdot (mp,l)) | MTfunsig (mbid, mt, mt') -> - str "functor (" ++ - P.pp_module mpl (MPbound mbid) ++ - str ":" ++ - pp_module_type mpl None mt ++ - str ") ->" ++ fnl () ++ - pp_module_type mpl None mt' + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type None mt in + let def = pp_module_type None mt' in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MTsig (msid, sign) -> - let mpl = match ol, mpl with - | None, _ -> (MPself msid) :: mpl - | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl - | _ -> assert false - in - let l = map_succeed (pp_specif mpl) sign in + let tvm = top_visible_mp () in + option_iter (fun l -> add_subst msid (MPdot (tvm, l))) ol; + let mp = MPself msid in + push_visible mp; + let l = map_succeed pp_specif sign in + pop_visible (); str "sig " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ fnl () ++ str "end" let is_short = function MEident _ | MEapply _ -> true | _ -> false -let rec pp_structure_elem mpl = function - | (_,SEdecl d) -> pp_decl mpl d +let rec pp_structure_elem = function + | (l,SEdecl d) -> + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + hov 1 (str ("module "^ren^" = struct ") ++ fnl () ++ pp_decl d) ++ + fnl () ++ str "end" ++ fnl () ++ + pp_alias_decl ren d + with Not_found -> pp_decl d) | (l,SEmodule m) -> + let def = pp_module_expr (Some l) m.ml_mod_expr in + let name = pp_modname (MPdot (top_visible_mp (), l)) in hov 1 - (str "module " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - (*i if you want signatures everywhere: i*) - (*i str " :" ++ fnl () ++ i*) - (*i pp_module_type mpl None m.ml_mod_type ++ fnl () ++ i*) - str " = " ++ - (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ - pp_module_expr mpl (Some l) m.ml_mod_expr) + (str "module " ++ name ++ str " = " ++ + (if (is_short m.ml_mod_expr) then mt () else fnl ()) ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module "^ren^" = ") ++ name + with Not_found -> mt ()) | (l,SEmodtype m) -> - hov 1 - (str "module type " ++ P.pp_module mpl (MPdot (List.hd mpl, l)) ++ - str " = " ++ fnl () ++ pp_module_type mpl None m) - -and pp_module_expr mpl ol = function - | MEident mp' -> P.pp_module mpl mp' + let def = pp_module_type None m in + let name = pp_modname (MPdot (top_visible_mp (), l)) in + hov 1 (str "module type " ++ name ++ str " = " ++ fnl () ++ def) ++ + (try + let ren = Common.check_duplicate (top_visible_mp ()) l in + fnl () ++ str ("module type "^ren^" = ") ++ name + with Not_found -> mt ()) + +and pp_module_expr ol = function + | MEident mp' -> pp_modname mp' | MEfunctor (mbid, mt, me) -> - str "functor (" ++ - P.pp_module mpl (MPbound mbid) ++ - str ":" ++ - pp_module_type mpl None mt ++ - str ") ->" ++ fnl () ++ - pp_module_expr mpl None me + let name = pp_modname (MPbound mbid) in + let typ = pp_module_type None mt in + let def = pp_module_expr None me in + str "functor (" ++ name ++ str ":" ++ typ ++ str ") ->" ++ fnl () ++ def | MEapply (me, me') -> - pp_module_expr mpl None me ++ str "(" ++ - pp_module_expr mpl None me' ++ str ")" + pp_module_expr None me ++ str "(" ++ pp_module_expr None me' ++ str ")" | MEstruct (msid, sel) -> - let mpl = match ol, mpl with - | None, _ -> (MPself msid) :: mpl - | Some l, mp :: mpl -> (MPdot (mp,l)) :: mpl - | _ -> assert false - in - let l = map_succeed (pp_structure_elem mpl) sel in + let tvm = top_visible_mp () in + let mp = match ol with None -> MPself msid | Some l -> MPdot (tvm,l) in + push_visible mp; + let l = map_succeed pp_structure_elem sel in + pop_visible (); str "struct " ++ fnl () ++ v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ fnl () ++ str "end" let pp_struct s = - let pp mp s = pp_structure_elem [mp] s ++ fnl2 () in + let pp mp s = + push_visible mp; + let p = pp_structure_elem s ++ fnl2 () in + pop_visible (); p + in prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s let pp_signature s = - let pp mp s = pp_specif [mp] s ++ fnl2 () in + let pp mp s = + push_visible mp; + let p = pp_specif s ++ fnl2 () in + pop_visible (); p + in prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s -let pp_decl mpl d = - try pp_decl mpl d with Failure "empty phrase" -> mt () - -end - +let pp_decl d = + try pp_decl d with Failure "empty phrase" -> mt () + +let ocaml_descr = { + keywords = keywords; + file_suffix = ".ml"; + capital_file = false; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = Some ".mli"; + sig_preamble = sig_preamble; + pp_sig = pp_signature; + pp_decl = pp_decl; +} diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 7a13590e2..c127fc1d1 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -8,47 +8,5 @@ (*i $Id$ i*) -(*s Some utility functions to be reused in module [Haskell]. *) - -open Pp -open Names -open Libnames -open Miniml - -val pp_par : bool -> std_ppcmds -> std_ppcmds -val pp_abst : identifier list -> std_ppcmds -val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds -val pr_binding : identifier list -> std_ppcmds - -val rename_id : identifier -> Idset.t -> identifier - -val lowercase_id : identifier -> identifier -val uppercase_id : identifier -> identifier - -val pr_upper_id : identifier -> std_ppcmds - -type env = identifier list * Idset.t - -val rename_vars: Idset.t -> identifier list -> env -val rename_tvars: Idset.t -> identifier list -> identifier list -val push_vars : identifier list -> env -> identifier list * env -val get_db_name : int -> env -> identifier - -val keywords : Idset.t - -val preamble : - extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds - -val preamble_sig : - extraction_params -> module_path list -> bool*bool*bool -> std_ppcmds - -(*s Production of Ocaml syntax. We export both a functor to be used for - extraction in the Coq toplevel and a function to extract some - declarations to a file. *) - -module Make : functor(P : Mlpp_param) -> Mlpp - - - - +val ocaml_descr : Miniml.language_descr diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 0b358f77d..5048002d0 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -18,7 +18,7 @@ open Libnames open Miniml open Mlutil open Table -open Ocaml +open Common (*s Scheme renaming issues. *) @@ -29,14 +29,14 @@ let keywords = "error"; "delay"; "force"; "_"; "__"] Idset.empty -let preamble _ _ (mldummy,_,_) _ = +let preamble _ _ usf = str ";; This extracted scheme code relies on some additional macros" ++ fnl () ++ str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++ fnl () ++ str "(load \"macros_extr.scm\")" ++ fnl () ++ fnl () ++ - (if mldummy then + (if usf.mldummy then str "(define __ (lambda (_) __))" ++ fnl () ++ fnl() else mt ()) @@ -62,12 +62,9 @@ let pp_apply st _ = function | args -> hov 2 (paren (str "@ " ++ st ++ (prlist (fun x -> spc () ++ x) args))) -(*s The pretty-printing functor. *) +(*s The pretty-printer for Scheme syntax *) -module Make = functor(P : Mlpp_param) -> struct - -let pp_global r = P.pp_global [initial_path] r -let empty_env () = [], P.globals() +let pp_global k r = str (Common.pp_global k r) (*s Pretty-printing of expressions. *) @@ -95,12 +92,12 @@ let rec pp_expr env args = (pr_id (List.hd i) ++ spc () ++ pp_expr env [] a1)) ++ spc () ++ hov 0 (pp_expr env' [] a2))))) | MLglob r -> - apply (pp_global r) + apply (pp_global Term r) | MLcons (i,r,args') -> assert (args=[]); let st = str "`" ++ - paren (pp_global r ++ + paren (pp_global Cons r ++ (if args' = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args') in @@ -125,7 +122,7 @@ let rec pp_expr env args = and pp_cons_args env = function | MLcons (i,r,args) when i<>Coinductive -> - paren (pp_global r ++ + paren (pp_global Cons r ++ (if args = [] then mt () else spc ()) ++ prlist_with_sep spc (pp_cons_args env) args) | e -> str "," ++ pp_expr env [] e @@ -137,7 +134,7 @@ and pp_one_pat env (r,ids,t) = if ids = [] then mt () else (str " " ++ prlist_with_sep spc pr_id (List.rev ids)) in - (pp_global r ++ args), (pp_expr env' [] t) + (pp_global Cons r ++ args), (pp_expr env' [] t) and pp_pat env pv = prvect_with_sep fnl @@ -160,11 +157,11 @@ and pp_fix env j (ids,bl) args = (*s Pretty-printing of a declaration. *) -let pp_decl _ = function +let pp_decl = function | Dind _ -> mt () | Dtype _ -> mt () | Dfix (rv, defs,_) -> - let ppv = Array.map pp_global rv in + let ppv = Array.map (pp_global Term) rv in prvect_with_sep fnl (fun (pi,ti) -> hov 2 @@ -177,23 +174,33 @@ let pp_decl _ = function if is_inline_custom r then mt () else if is_custom r then - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ str (find_custom r))) ++ fnl () ++ fnl () else - hov 2 (paren (str "define " ++ pp_global r ++ spc () ++ + hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++ pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl () -let pp_structure_elem mp = function - | (l,SEdecl d) -> pp_decl mp d +let pp_structure_elem = function + | (l,SEdecl d) -> pp_decl d | (l,SEmodule m) -> failwith "TODO: Scheme extraction of modules not implemented yet" | (l,SEmodtype m) -> failwith "TODO: Scheme extraction of modules not implemented yet" let pp_struct = - prlist (fun (mp,sel) -> prlist (pp_structure_elem mp) sel) - -let pp_signature s = assert false - -end - + let pp_sel (mp,sel) = + push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p + in + prlist pp_sel + +let scheme_descr = { + keywords = keywords; + file_suffix = ".scm"; + capital_file = false; + preamble = preamble; + pp_struct = pp_struct; + sig_suffix = None; + sig_preamble = (fun _ _ _ -> mt ()); + pp_sig = (fun _ -> mt ()); + pp_decl = pp_decl; +} diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index bded1a8a8..573bb9cef 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -8,20 +8,4 @@ (*i $Id$ i*) -(*s Some utility functions to be reused in module [Haskell]. *) - -open Pp -open Miniml -open Names - -val keywords : Idset.t - -val preamble : - extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds - -module Make : functor(P : Mlpp_param) -> Mlpp - - - - - +val scheme_descr : Miniml.language_descr diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 204319099..7a8ff95ed 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -20,37 +20,49 @@ open Util open Pp open Miniml -(*S Utilities concerning [module_path] and [kernel_names] *) +(*S Utilities about [module_path] and [kernel_names] and [global_reference] *) -let occur_kn_in_ref kn = - function +let occur_kn_in_ref kn = function | IndRef (kn',_) | ConstructRef ((kn',_),_) -> kn = kn' | ConstRef _ -> false | VarRef _ -> assert false - -let modpath_of_r r = match r with - | ConstRef kn -> con_modpath kn - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> modpath kn - | VarRef _ -> assert false - -let label_of_r r = match r with - | ConstRef kn -> con_label kn - | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> label kn - | VarRef _ -> assert false - -let current_toplevel () = fst (Lib.current_prefix ()) + +let modpath_of_r = function + | ConstRef kn -> con_modpath kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> modpath kn + | VarRef _ -> assert false + +let label_of_r = function + | ConstRef kn -> con_label kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> label kn + | VarRef _ -> assert false let rec base_mp = function | MPdot (mp,l) -> base_mp mp | mp -> mp +let rec mp_length = function + | MPdot (mp, _) -> 1 + (mp_length mp) + | _ -> 1 + let is_modfile = function | MPfile _ -> true | _ -> false +let string_of_modfile = function + | MPfile f -> String.capitalize (string_of_id (List.hd (repr_dirpath f))) + | _ -> assert false + +let rec modfile_of_mp = function + | (MPfile _) as mp -> mp + | MPdot (mp,_) -> modfile_of_mp mp + | _ -> raise Not_found + +let current_toplevel () = fst (Lib.current_prefix ()) + let is_toplevel mp = mp = initial_path || mp = current_toplevel () @@ -60,8 +72,56 @@ let at_toplevel mp = let visible_kn kn = at_toplevel (base_mp (modpath kn)) let visible_con kn = at_toplevel (base_mp (con_modpath kn)) +let rec prefixes_mp mp = match mp with + | MPdot (mp',_) -> MPset.add mp (prefixes_mp mp') + | _ -> MPset.singleton mp + +let rec get_nth_label_mp n mp = match mp with + | MPdot (mp,l) -> if n=1 then l else get_nth_label_mp (n-1) mp + | _ -> failwith "get_nth_label: not enough MPdot" + +let get_nth_label n r = + if n=0 then label_of_r r else get_nth_label_mp n (modpath_of_r r) + +let rec common_prefix prefixes_mp1 mp2 = + if MPset.mem mp2 prefixes_mp1 then mp2 + else match mp2 with + | MPdot (mp,_) -> common_prefix prefixes_mp1 mp + | _ -> raise Not_found + +let common_prefix_from_list mp0 mpl = + let prefixes_mp0 = prefixes_mp mp0 in + let rec f = function + | [] -> raise Not_found + | mp1 :: l -> try common_prefix prefixes_mp0 mp1 with Not_found -> f l + in f mpl + +let rec parse_labels ll = function + | MPdot (mp,l) -> parse_labels (l::ll) mp + | mp -> mp,ll + +let labels_of_mp mp = parse_labels [] mp + +let labels_of_ref r = + let mp,_,l = + match r with + ConstRef con -> repr_con con + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_kn kn + | VarRef _ -> assert false + in + parse_labels [l] mp + +let rec add_labels_mp mp = function + | [] -> mp + | l :: ll -> add_labels_mp (MPdot (mp,l)) ll + + (*S The main tables: constants, inductives, records, ... *) +(* Theses tables are not registered within coq save/undo mechanism + since we reset their contents at each run of Extraction *) + (*s Constants tables. *) let terms = ref (Cmap.empty : ml_decl Cmap.t) @@ -109,11 +169,26 @@ let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs let is_projection r = Refmap.mem r !projs let projection_arity r = Refmap.find r !projs +(*s Table of used axioms *) + +let info_axioms = ref Refset.empty +let log_axioms = ref Refset.empty +let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty +let add_info_axiom r = info_axioms := Refset.add r !info_axioms +let add_log_axiom r = log_axioms := Refset.add r !log_axioms + +(*s Extraction mode: modular or monolithic *) + +let modular_ref = ref false + +let set_modular b = modular_ref := b +let modular () = !modular_ref + (*s Tables synchronization. *) let reset_tables () = init_terms (); init_types (); init_inductives (); init_recursors (); - init_projs () + init_projs (); init_axioms () (*s Printing. *) @@ -146,21 +221,34 @@ let pr_long_global r = let err s = errorlabstrm "Extraction" s +let warning_axioms () = + let info_axioms = Refset.elements !info_axioms in + if info_axioms = [] then () + else begin + let s = if List.length info_axioms = 1 then "axiom" else "axioms" in + msg_warning + (str ("The following "^s^" must be realized in the extracted code:") + ++ hov 1 (spc () ++ prlist_with_sep spc pr_global info_axioms) + ++ str "." ++ fnl ()) + end; + let log_axioms = Refset.elements !log_axioms in + if log_axioms = [] then () + else begin + let s = if List.length log_axioms = 1 then "axiom was" else "axioms were" + in + msg_warning + (str ("The following logical "^s^" encountered:") ++ + hov 1 (spc () ++ prlist_with_sep spc pr_global log_axioms ++ str ".\n") ++ + str "Having invalid logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ + fnl ()) + end + let error_axiom_scheme r i = err (str "The type scheme axiom " ++ spc () ++ pr_global r ++ spc () ++ str "needs " ++ pr_int i ++ str " type variable(s).") -let warning_info_ax r = - msg_warning (str "You must realize axiom " ++ - pr_global r ++ str " in the extracted code.") - -let warning_log_ax r = - msg_warning (str "This extraction depends on logical axiom" ++ spc () ++ - pr_global r ++ str "." ++ spc() ++ - str "Having false logical axiom in the environment when extracting" ++ - spc () ++ str "may lead to incorrect or non-terminating ML terms.") - let check_inside_module () = if Lib.is_modtype () then err (str "You can't do that within a Module Type." ++ fnl () ++ @@ -186,15 +274,11 @@ let error_nb_cons () = let error_module_clash s = err (str ("There are two Coq modules with ML name " ^ s ^".\n") ++ - str "This is not allowed in ML. Please do some renaming first.") + str "This is not supported yet. Please do some renaming first.") let error_unknown_module m = err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.") -let error_toplevel () = - err (str "Toplevel pseudo-ML language can be used only at Coq toplevel.\n" ++ - str "You should use Extraction Language Ocaml or Haskell before.") - let error_scheme () = err (str "No Scheme modular extraction available yet.") @@ -203,9 +287,11 @@ let error_not_visible r = str "For example, it may be inside an applied functor." ++ str "Use Recursive Extraction to get the whole environment.") -let error_MPfile_as_mod d = - err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^ - "Extraction cannot currently deal with this situation.\n")) +let error_MPfile_as_mod mp = + err (str ("The whole file "^(string_of_modfile mp)^ + ".v is used somewhere as a module.\n"^ + "Monolithic Extraction cannot deal with this situation.\n"^ + "Please use (Recursive) Extraction Library instead.\n")) let error_record r = err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++ @@ -216,8 +302,16 @@ let check_loaded_modfile mp = match base_mp mp with err (str ("Please load library "^(string_of_dirpath dp^" first."))) | _ -> () +let info_file f = + Options.if_verbose message + ("The file "^f^" has been created by extraction.") + + (*S The Extraction auxiliary commands *) +(* The objects defined below should survive an arbitrary time, + so we register them to coq save/undo mechanism. *) + (*s Extraction AutoInline *) let auto_inline_ref = ref true @@ -305,7 +399,7 @@ let _ = declare_int_option (*s Extraction Lang *) -type lang = Ocaml | Haskell | Scheme | Toplevel +type lang = Ocaml | Haskell | Scheme let lang_ref = ref Ocaml @@ -327,7 +421,6 @@ let _ = declare_summary "Extraction Lang" let extraction_language x = Lib.add_anonymous_leaf (extr_lang x) - (*s Extraction Inline/NoInline *) let empty_inline_table = (Refset.empty,Refset.empty) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 55402d94a..304e374b5 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -14,39 +14,49 @@ open Miniml open Declarations val id_of_global : global_reference -> identifier +val pr_long_global : global_reference -> Pp.std_ppcmds + (*s Warning and Error messages. *) +val warning_axioms : unit -> unit val error_axiom_scheme : global_reference -> int -> 'a -val warning_info_ax : global_reference -> unit -val warning_log_ax : global_reference -> unit val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a val error_module_clash : string -> 'a val error_unknown_module : qualid -> 'a -val error_toplevel : unit -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_MPfile_as_mod : dir_path -> 'a +val error_MPfile_as_mod : module_path -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit val check_loaded_modfile : module_path -> unit -(*s utilities concerning [module_path]. *) +val info_file : string -> unit + +(*s utilities about [module_path] and [kernel_names] and [global_reference] *) val occur_kn_in_ref : kernel_name -> global_reference -> bool val modpath_of_r : global_reference -> module_path val label_of_r : global_reference -> label - val current_toplevel : unit -> module_path val base_mp : module_path -> module_path -val is_modfile : module_path -> bool +val is_modfile : module_path -> bool +val string_of_modfile : module_path -> string val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool val visible_con : constant -> bool +val mp_length : module_path -> int +val prefixes_mp : module_path -> MPset.t +val modfile_of_mp : module_path -> module_path +val common_prefix_from_list : module_path -> module_path list -> module_path +val add_labels_mp : module_path -> label list -> module_path +val get_nth_label_mp : int -> module_path -> label +val get_nth_label : int -> global_reference -> label +val labels_of_ref : global_reference -> module_path * label list (*s Some table-related operations *) @@ -66,6 +76,9 @@ val add_projection : int -> constant -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int +val add_info_axiom : global_reference -> unit +val add_log_axiom : global_reference -> unit + val reset_tables : unit -> unit (*s AutoInline parameter *) @@ -95,9 +108,14 @@ val optims : unit -> opt_flag (*s Target language. *) -type lang = Ocaml | Haskell | Scheme | Toplevel +type lang = Ocaml | Haskell | Scheme val lang : unit -> lang +(*s Extraction mode: modular or monolithic *) + +val set_modular : bool -> unit +val modular : unit -> bool + (*s Table for custom inlining *) val to_inline : global_reference -> bool |