diff options
Diffstat (limited to 'contrib/extraction')
-rw-r--r-- | contrib/extraction/common.ml | 11 | ||||
-rw-r--r-- | contrib/extraction/common.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 47 | ||||
-rw-r--r-- | contrib/extraction/extract_env.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/extraction.ml | 29 | ||||
-rw-r--r-- | contrib/extraction/extraction.mli | 8 | ||||
-rw-r--r-- | contrib/extraction/g_extraction.ml4 | 20 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 6 | ||||
-rw-r--r-- | contrib/extraction/haskell.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/miniml.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 38 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 4 | ||||
-rw-r--r-- | contrib/extraction/modutil.ml | 41 | ||||
-rw-r--r-- | contrib/extraction/modutil.mli | 3 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 11 | ||||
-rw-r--r-- | contrib/extraction/ocaml.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/scheme.ml | 2 | ||||
-rw-r--r-- | contrib/extraction/scheme.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/table.ml | 76 | ||||
-rw-r--r-- | contrib/extraction/table.mli | 21 |
20 files changed, 185 insertions, 144 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 8e441613..8d8438dc 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*) +(*i $Id: common.ml 7651 2005-12-16 03:19:20Z letouzey $ i*) open Pp open Util @@ -143,7 +143,7 @@ let create_modular_renamings struc = in (* 1) creates renamings of objects *) let add upper r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let l = mp_create_modular_renamings mp in let s = modular_rename upper (id_of_global r) in global_ids := Idset.add (id_of_string s) !global_ids; @@ -184,7 +184,7 @@ let create_modular_renamings struc = List.iter contents_first_level used_modules; let used_modules' = List.rev used_modules in let needs_qualify r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in if (is_modfile mp) && mp <> current_module && (clash mp [] (List.hd (get_renamings r)) used_modules') then to_qualify := Refset.add r !to_qualify @@ -239,7 +239,7 @@ let rec mp_create_mono_renamings mp = let create_mono_renamings struc = let { up = u ; down = d } = struct_get_references_list struc in let add upper r = - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let l = mp_create_mono_renamings mp in let mycase = if upper then uppercase_id else lowercase_id in let id = @@ -285,7 +285,7 @@ module StdParams = struct let pp_global mpl r = let ls = get_renamings r in let s = List.hd ls in - let mp = modpath (kn_of_r r) in + let mp = modpath_of_r r in let ls = if mp = List.hd mpl then [s] (* simpliest situation *) else @@ -317,7 +317,6 @@ module StdParams = struct (*i TODO: clash possible i*) list_firstn ((mp_length mp)-(mp_length pref)) ls with Not_found -> (* [mp] is othogonal with every element of [mp]. *) - let base = base_mp mp in if !modular && (at_toplevel mp) then snd (list_sep_last ls) else ls diff --git a/contrib/extraction/common.mli b/contrib/extraction/common.mli index 3e5efa0c..2ba51e1c 100644 --- a/contrib/extraction/common.mli +++ b/contrib/extraction/common.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: common.mli,v 1.19.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: common.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) open Names open Miniml diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index d725a1d7..c581c620 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.ml,v 1.74.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extract_env.ml 6328 2004-11-18 17:31:41Z sacerdot $ i*) open Term open Declarations @@ -19,6 +19,7 @@ open Table open Extraction open Modutil open Common +open Mod_subst (*s Obtaining Coq environment. *) @@ -28,7 +29,7 @@ let toplevel_env () = | (_,kn), Lib.Leaf o -> let mp,_,l = repr_kn kn in let seb = match Libobject.object_tag o with - | "CONSTANT" -> SEBconst (Global.lookup_constant kn) + | "CONSTANT" -> SEBconst (Global.lookup_constant (constant_of_kn kn)) | "INDUCTIVE" -> SEBmind (Global.lookup_mind kn) | "MODULE" -> SEBmodule (Global.lookup_module (MPdot (mp,l))) | "MODULE TYPE" -> SEBmodtype (Global.lookup_modtype kn) @@ -52,14 +53,23 @@ let environment_until dir_opt = | _ -> assert false in parse (Library.loaded_libraries ()) -type visit = { mutable kn : KNset.t; mutable mp : MPset.t } +type visit = + { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t } let in_kn v kn = KNset.mem kn v.kn +let in_ref v ref = Refset.mem ref v.ref let in_mp v mp = MPset.mem mp v.mp let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn) -let visit_ref v r = visit_kn v (kn_of_r r) +let visit_ref v r = + let r = + (* if we meet a constructor we must export the inductive definition *) + match r with + ConstructRef (r,_) -> IndRef r + | _ -> r + in + v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) exception Impossible @@ -102,7 +112,7 @@ let get_spec_references v s = let rec extract_msig env v mp = function | [] -> [] | (l,SPBconst cb) :: msig -> - let kn = make_kn mp empty_dirpath l in + let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in if logical_spec s then extract_msig env v mp msig else begin @@ -143,9 +153,9 @@ let rec extract_msb env v mp all = function | (l,SEBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vkn = Array.map (fun id -> make_kn mp empty_dirpath id) vl in + let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in let ms = extract_msb env v mp all msb in - let b = array_exists (in_kn v) vkn in + let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in if all || b then let d = extract_fixpoint env vkn recd in if (not b) && (logical_decl d) then ms @@ -153,8 +163,8 @@ let rec extract_msb env v mp all = function else ms with Impossible -> let ms = extract_msb env v mp all msb in - let kn = make_kn mp empty_dirpath l in - let b = in_kn v kn in + let kn = make_con mp empty_dirpath l in + let b = in_ref v (ConstRef kn) in if all || b then let d = extract_constant env kn cb in if (not b) && (logical_decl d) then ms @@ -163,7 +173,7 @@ let rec extract_msb env v mp all = function | (l,SEBmind mib) :: msb -> let ms = extract_msb env v mp all msb in let kn = make_kn mp empty_dirpath l in - let b = in_kn v kn in + let b = in_ref v (IndRef (kn,0)) in (* 0 is dummy *) if all || b then let d = Dind (kn, extract_inductive env kn) in if (not b) && (logical_decl d) then ms @@ -217,12 +227,12 @@ let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = let l = environment_until None in let v = - let add_kn r = KNset.add (kn_of_r r) in - let kns = List.fold_right add_kn refs KNset.empty in + let add_ref r = Refset.add r in + let refs = List.fold_right add_ref refs Refset.empty in let add_mp mp = MPset.union (prefixes_mp mp) in let mps = List.fold_right add_mp mpl MPset.empty in - let mps = KNset.fold (fun k -> add_mp (modpath k)) kns mps in - { kn = kns; mp = mps } + let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in + { kn = KNset.empty; ref = refs; mp = mps } in let env = Global.env () in List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) @@ -270,10 +280,9 @@ let extraction qid = else begin let prm = { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in - let kn = kn_of_r r in let struc = optimize_struct prm None (mono_environment [r] []) in let d = get_decl_in_structure r struc in - print_one_decl struc (modpath kn) d; + print_one_decl struc (modpath_of_r r) d; reset_tables () end @@ -315,7 +324,7 @@ let extraction_module m = let b = is_modfile mp in let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in let l = environment_until None in - let v = { kn = KNset.empty ; mp = prefixes_mp mp } in + let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in let env = Global.env () in let struc = List.rev_map @@ -350,7 +359,9 @@ let extraction_library is_rec m = | Scheme -> error_scheme () | _ -> let dir_m = dir_module_of_id m in - let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in + let v = + { kn = KNset.empty; ref = Refset.empty; + mp = MPset.singleton (MPfile dir_m) } in let l = environment_until (Some dir_m) in let struc = let env = Global.env () in diff --git a/contrib/extraction/extract_env.mli b/contrib/extraction/extract_env.mli index 8ce64342..a09464a1 100644 --- a/contrib/extraction/extract_env.mli +++ b/contrib/extraction/extract_env.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extract_env.mli,v 1.13.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extract_env.mli 5920 2004-07-16 20:01:26Z herbelin $ i*) (*s This module declares the extraction commands. *) diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 6bfe861f..a4bf973d 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*) +(*i $Id: extraction.ml 7639 2005-12-02 10:01:15Z gregoire $ i*) (*i*) open Util @@ -230,7 +230,7 @@ let rec extract_type env db j c args = (* We try to reduce. *) let newc = applist (Declarations.force lbody, args) in extract_type env db j newc [])) - | Ind ((kn,i) as ip) -> + | Ind (kn,i) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args | Case _ | Fix _ | CoFix _ -> Tunknown @@ -295,8 +295,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in - let npar = mip0.mind_nparams in - let epar = push_rel_context mip0.mind_params_ctxt env in + let npar = mib.mind_nparams in + let epar = push_rel_context mib.mind_params_ctxt env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = @@ -354,22 +354,22 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let rec names_prod t = match kind_of_term t with | Prod(n,_,t) -> n::(names_prod t) | LetIn(_,_,_,t) -> names_prod t - | Cast(t,_) -> names_prod t + | Cast(t,_,_) -> names_prod t | _ -> [] in let field_names = - list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); - let projs = ref KNset.empty in + let projs = ref Cset.empty in let mp,d,_ = repr_kn kn in let rec select_fields l typs = match l,typs with | [],[] -> [] | (Name id)::l, typ::typs -> if type_eq (mlt_env env) Tdummy typ then select_fields l typs else - let knp = make_kn mp d (label_of_id id) in + let knp = make_con mp d (label_of_id id) in if not (List.mem false (type_to_sign (mlt_env env) typ)) then - projs := KNset.add knp !projs; + projs := Cset.add knp !projs; (ConstRef knp) :: (select_fields l typs) | Anonymous::l, typ::typs -> if type_eq (mlt_env env) Tdummy typ then select_fields l typs @@ -384,8 +384,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) let n = nb_default_params env mip0.mind_nf_arity in List.iter (option_iter - (fun kn -> if KNset.mem kn !projs then add_projection n kn)) - (find_structure ip).s_PROJ + (fun kn -> if Cset.mem kn !projs then add_projection n kn)) + (lookup_structure ip).s_PROJ with Not_found -> () end; Record field_glob @@ -419,7 +419,7 @@ and extract_type_cons env db dbmap c i = and mlt_env env r = match r with | ConstRef kn -> (try - if not (visible_kn kn) then raise Not_found; + if not (visible_con kn) then raise Not_found; match lookup_term kn with | Dtype (_,vl,mlt) -> Some mlt | _ -> None @@ -448,7 +448,7 @@ let type_expunge env = type_expunge (mlt_env env) let record_constant_type env kn opt_typ = try - if not (visible_kn kn) then raise Not_found; + if not (visible_con kn) then raise Not_found; lookup_type kn with Not_found -> let typ = match opt_typ with @@ -515,7 +515,7 @@ let rec extract_term env mle mlt c args = extract_app env mle mlt (extract_fix env mle i recd) args | CoFix (i,recd) -> extract_app env mle mlt (extract_fix env mle i recd) args - | Cast (c, _) -> extract_term env mle mlt c args + | Cast (c,_,_) -> extract_term env mle mlt c args | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ | Var _ -> assert false (*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) @@ -678,7 +678,6 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt = end else let mi = extract_ind env kn in - let params_nb = mi.ind_nparams in let oi = mi.ind_packets.(i) in let metas = Array.init (List.length oi.ip_vars) new_meta in (* The extraction of the head. *) diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index fc5782c9..1dfd7e1a 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: extraction.mli,v 1.27.2.1 2004/07/16 19:30:07 herbelin Exp $ i*) +(*i $Id: extraction.mli 6303 2004-11-16 12:37:40Z sacerdot $ i*) (*s Extraction from Coq terms to Miniml. *) @@ -17,12 +17,12 @@ open Environ open Libnames open Miniml -val extract_constant : env -> kernel_name -> constant_body -> ml_decl +val extract_constant : env -> constant -> constant_body -> ml_decl -val extract_constant_spec : env -> kernel_name -> constant_body -> ml_spec +val extract_constant_spec : env -> constant -> constant_body -> ml_spec val extract_fixpoint : - env -> kernel_name array -> (constr, types) prec_declaration -> ml_decl + env -> constant array -> (constr, types) prec_declaration -> ml_decl val extract_inductive : env -> kernel_name -> ml_ind diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4 index 33a6117d..13b29c7b 100644 --- a/contrib/extraction/g_extraction.ml4 +++ b/contrib/extraction/g_extraction.ml4 @@ -15,10 +15,7 @@ open Pcoq open Genarg open Pp -let pr_mlname _ _ s = - spc () ++ - (if !Options.v7 && not (Options.do_translate()) then qs s - else Pptacticnew.qsnew s) +let pr_mlname _ _ _ s = spc () ++ qs s ARGUMENT EXTEND mlname TYPED AS string @@ -37,21 +34,6 @@ VERNAC ARGUMENT EXTEND language | [ "Toplevel" ] -> [ Toplevel ] END -(* Temporary for translator *) -if !Options.v7 then - let pr_language _ _ = function - | Ocaml -> str " Ocaml" - | Haskell -> str " Haskell" - | Scheme -> str " Scheme" - | Toplevel -> str " Toplevel" - in - let globwit_language = Obj.magic rawwit_language in - let wit_language = Obj.magic rawwit_language in - Pptactic.declare_extra_genarg_pprule true - (rawwit_language, pr_language) - (globwit_language, pr_language) - (wit_language, pr_language); - (* Extraction commands *) VERNAC COMMAND EXTEND Extraction diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 3834fe81..c4ed364a 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*) +(*i $Id: haskell.ml 7653 2005-12-16 04:12:26Z letouzey $ i*) (*s Production of Haskell syntax. *) @@ -240,11 +240,11 @@ let pp_one_ind ip pl cv = prlist_with_sep (fun () -> (str " ")) (pp_type true pl) l)) in - str (if cv = [||] then "type " else "data ") ++ + str (if Array.length cv = 0 then "type " else "data ") ++ pp_global (IndRef ip) ++ str " " ++ prlist_with_sep (fun () -> str " ") pr_lower_id pl ++ (if pl = [] then mt () else str " ") ++ - if cv = [||] then str "= () -- empty inductive" + if Array.length cv = 0 then str "= () -- empty inductive" else (v 0 (str "= " ++ prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 822444bd..106f7868 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: haskell.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) open Pp open Names diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index 7c18f9f5..cf722e4e 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*) +(*i $Id: miniml.mli 6064 2004-09-06 07:49:51Z letouzey $ i*) (*s Target language for extraction: a core ML called MiniML. *) diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index c01766b0..facab18e 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*) +(*i $Id: mlutil.ml 7574 2005-11-17 15:48:45Z letouzey $ i*) (*i*) open Pp @@ -209,8 +209,8 @@ end (*s Does a section path occur in a ML type ? *) let rec type_mem_kn kn = function - | Tmeta _ -> assert false - | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l + | Tmeta {contents = Some t} -> type_mem_kn kn t + | Tglob (r,l) -> occur_kn_in_ref kn r || List.exists (type_mem_kn kn) l | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b) | _ -> false @@ -218,7 +218,7 @@ let rec type_mem_kn kn = function let type_maxvar t = let rec parse n = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> parse n t | Tvar i -> max i n | Tarr (a,b) -> parse (parse n a) b | Tglob (_,l) -> List.fold_left parse n l @@ -228,7 +228,7 @@ let type_maxvar t = (*s From [a -> b -> c] to [[a;b],c]. *) let rec type_decomp = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> type_decomp t | Tarr (a,b) -> let l,h = type_decomp b in a::l, h | a -> [],a @@ -241,7 +241,7 @@ let rec type_recomp (l,t) = match l with (*s Translating [Tvar] to [Tvar'] to avoid clash. *) let rec var2var' = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> var2var' t | Tvar i -> Tvar' i | Tarr (a,b) -> Tarr (var2var' a, var2var' b) | Tglob (r,l) -> Tglob (r, List.map var2var' l) @@ -252,16 +252,17 @@ type abbrev_map = global_reference -> ml_type option (*s Delta-reduction of type constants everywhere in a ML type [t]. [env] is a function of type [ml_type_env]. *) + let type_expand env t = let rec expand = function - | Tmeta _ -> assert false - | Tglob (r,l) as t -> + | Tmeta {contents = Some t} -> expand t + | Tglob (r,l) -> (match env r with | Some mlt -> expand (type_subst_list l mlt) | None -> Tglob (r, List.map expand l)) | Tarr (a,b) -> Tarr (expand a, expand b) | a -> a - in expand t + in if Table.type_expand () then expand t else t (*s Idem, but only at the top level of implications. *) @@ -269,7 +270,7 @@ let is_arrow = function Tarr _ -> true | _ -> false let type_weak_expand env t = let rec expand = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> expand t | Tglob (r,l) as t -> (match env r with | Some mlt -> @@ -290,7 +291,7 @@ let type_neq env t t' = (type_expand env t <> type_expand env t') let type_to_sign env t = let rec f = function - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> f t | Tarr (a,b) -> (Tdummy <> a) :: (f b) | _ -> [] in f (type_expand env t) @@ -304,7 +305,7 @@ let type_expunge env t = let rec f t s = if List.mem false s then match t with - | Tmeta _ -> assert false + | Tmeta {contents = Some t} -> f t s | Tarr (a,b) -> let t = f b (List.tl s) in if List.hd s then Tarr (a, t) else t @@ -377,7 +378,7 @@ let ast_iter f = function | MLapp (a,l) -> f a; List.iter f l | MLcons (_,c,l) -> List.iter f l | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom -> () (*S Operations concerning De Bruijn indices. *) @@ -594,11 +595,12 @@ let rec linear_beta_red a t = match a,t with linear beta reductions at modified positions. *) let rec ast_glob_subst s t = match t with - | MLapp ((MLglob (ConstRef kn)) as f, a) -> + | MLapp ((MLglob ((ConstRef kn) as refe)) as f, a) -> let a = List.map (ast_glob_subst s) a in - (try linear_beta_red a (KNmap.find kn s) + (try linear_beta_red a (Refmap.find refe s) with Not_found -> MLapp (f, a)) - | MLglob (ConstRef kn) -> (try KNmap.find kn s with Not_found -> t) + | MLglob ((ConstRef kn) as refe) -> + (try Refmap.find refe s with Not_found -> t) | _ -> ast_map (ast_glob_subst s) t @@ -653,7 +655,7 @@ let check_generalizable_case unsafe br = (*s Do all branches correspond to the same thing? *) let check_constant_case br = - if br = [||] then raise Impossible; + if Array.length br = 0 then raise Impossible; let (r,l,t) = br.(0) in let n = List.length l in if ast_occurs_itvl 1 n t then raise Impossible; @@ -1117,7 +1119,7 @@ let inline_test t = let manual_inline_list = let mp = MPfile (dirpath_of_string "Coq.Init.Wf") in - List.map (fun s -> (make_kn mp empty_dirpath (mk_label s))) + List.map (fun s -> (make_con mp empty_dirpath (mk_label s))) [ "well_founded_induction_type"; "well_founded_induction"; "Acc_rect"; "Acc_rec" ; "Acc_iter" ] diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index eaf38778..1ba1df64 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mlutil.mli,v 1.47.2.1 2004/07/16 19:30:08 herbelin Exp $ i*) +(*i $Id: mlutil.mli 6303 2004-11-16 12:37:40Z sacerdot $ i*) open Util open Names @@ -101,7 +101,7 @@ val ast_lift : int -> ml_ast -> ml_ast val ast_pop : ml_ast -> ml_ast val ast_subst : ml_ast -> ml_ast -> ml_ast -val ast_glob_subst : ml_ast KNmap.t -> ml_ast -> ml_ast +val ast_glob_subst : ml_ast Refmap.t -> ml_ast -> ml_ast val normalize : ml_ast -> ml_ast val optimize_fix : ml_ast -> ml_ast diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml index 54f0c992..ff8daf46 100644 --- a/contrib/extraction/modutil.ml +++ b/contrib/extraction/modutil.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: modutil.ml 7632 2005-12-01 14:35:21Z letouzey $ i*) open Names open Declarations @@ -16,6 +16,7 @@ open Util open Miniml open Table open Mlutil +open Mod_subst (*S Functions upon modules missing in [Modops]. *) @@ -25,8 +26,9 @@ open Mlutil let add_structure mp msb env = let add_one env (l,elem) = let kn = make_kn mp empty_dirpath l in + let con = make_con mp empty_dirpath l in match elem with - | SEBconst cb -> Environ.add_constant kn cb env + | SEBconst cb -> Environ.add_constant con cb env | SEBmind mib -> Environ.add_mind kn mib env | SEBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env | SEBmodtype mtb -> Environ.add_modtype kn mtb env @@ -116,8 +118,15 @@ let rec parse_labels ll = function let labels_of_mp mp = parse_labels [] mp -let labels_of_kn kn = - let mp,_,l = repr_kn kn in parse_labels [l] mp +let labels_of_ref r = + let mp,_,l = + match r with + ConstRef con -> repr_con con + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> repr_kn kn + | VarRef _ -> assert false + in + parse_labels [l] mp let rec add_labels_mp mp = function | [] -> mp @@ -176,7 +185,7 @@ let ast_iter_references do_term do_cons do_type a = | MLcons (i,r,_) -> if lang () = Ocaml then record_iter_references do_term i; do_cons r - | MLcase (i,_,v) as a -> + | MLcase (i,_,v) -> if lang () = Ocaml then record_iter_references do_term i; Array.iter (fun (r,_,_) -> do_cons r) v | _ -> () @@ -307,8 +316,7 @@ let signature_of_structure s = let get_decl_in_structure r struc = try - let kn = kn_of_r r in - let base_mp,ll = labels_of_kn kn in + let base_mp,ll = labels_of_ref r in if not (at_toplevel base_mp) then error_not_visible r; let sel = List.assoc base_mp struc in let rec go ll sel = match ll with @@ -336,16 +344,16 @@ let get_decl_in_structure r struc = let dfix_to_mlfix rv av i = let rec make_subst n s = if n < 0 then s - else make_subst (n-1) (KNmap.add (kn_of_r rv.(n)) (n+1) s) + else make_subst (n-1) (Refmap.add rv.(n) (n+1) s) in - let s = make_subst (Array.length rv - 1) KNmap.empty + let s = make_subst (Array.length rv - 1) Refmap.empty in let rec subst n t = match t with - | MLglob (ConstRef kn) -> - (try MLrel (n + (KNmap.find kn s)) with Not_found -> t) + | MLglob ((ConstRef kn) as refe) -> + (try MLrel (n + (Refmap.find refe s)) with Not_found -> t) | _ -> ast_map_lift subst n t in - let ids = Array.map (fun r -> id_of_label (label (kn_of_r r))) rv in + let ids = Array.map (fun r -> id_of_label (label_of_r r)) rv in let c = Array.map (subst 0) av in MLfix(i, ids, c) @@ -356,7 +364,7 @@ let rec optim prm s = function | Dterm (r,t,typ) :: l -> let t = normalize (ast_glob_subst !s t) in let i = inline r t in - if i then s := KNmap.add (kn_of_r r) t !s; + if i then s := Refmap.add r t !s; if not i || prm.modular || List.mem r prm.to_appear then let d = match optimize_fix t with @@ -370,10 +378,9 @@ let rec optim prm s = function let rec optim_se top prm s = function | [] -> [] | (l,SEdecl (Dterm (r,a,t))) :: lse -> - let kn = kn_of_r r in let a = normalize (ast_glob_subst !s a) in let i = inline r a in - if i then s := KNmap.add kn a !s; + if i then s := Refmap.add r a !s; if top && i && not prm.modular && not (List.mem r prm.to_appear) then optim_se top prm s lse else @@ -389,7 +396,7 @@ let rec optim_se top prm s = function let fake_body = MLfix (0,[||],[||]) in for i = 0 to Array.length rv - 1 do if inline rv.(i) fake_body - then s := KNmap.add (kn_of_r rv.(i)) (dfix_to_mlfix rv av i) !s + then s := Refmap.add rv.(i) (dfix_to_mlfix rv av i) !s else all := false done; if !all && top && not prm.modular @@ -408,6 +415,6 @@ and optim_me prm s = function | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me prm s me) let optimize_struct prm before struc = - let subst = ref (KNmap.empty : ml_ast KNmap.t) in + let subst = ref (Refmap.empty : ml_ast Refmap.t) in option_iter (fun l -> ignore (optim prm subst l)) before; List.map (fun (mp,lse) -> (mp, optim_se true prm subst lse)) struc diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli index 7f8c4113..f5208c0d 100644 --- a/contrib/extraction/modutil.mli +++ b/contrib/extraction/modutil.mli @@ -6,13 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: modutil.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) open Names open Declarations open Environ open Libnames open Miniml +open Mod_subst (*s Functions upon modules missing in [Modops]. *) diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index ff9cfd21..a0620d72 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: ocaml.ml 7632 2005-12-01 14:35:21Z letouzey $ i*) (*s Production of Ocaml syntax. *) @@ -264,7 +264,6 @@ let rec pp_expr par env args = let tuple = pp_tuple (pp_expr true env []) args' in pp_par par (pp_global r ++ spc () ++ tuple) | MLcase (i, t, pv) -> - let r,_,_ = pv.(0) in let expr = if i = Coinductive then (str "Lazy.force" ++ spc () ++ pp_expr true env [] t) else @@ -409,7 +408,7 @@ let pp_one_ind prefix ip pl cv = (fun () -> spc () ++ str "* ") (pp_type true pl) l)) in pp_parameters pl ++ str prefix ++ pp_global (IndRef ip) ++ str " =" ++ - if cv = [||] then str " unit (* empty inductive *)" + 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)) @@ -480,13 +479,13 @@ let pp_mind kn i = let pp_decl mpl = local_mpl := mpl; function - | Dind (kn,i) as d -> pp_mind kn i + | Dind (kn,i) -> pp_mind kn i | Dtype (r, l, t) -> if is_inline_custom r then failwith "empty phrase" else - let pp_r = pp_global r in + let pp_r = pp_global r in let l = rename_tvars keywords l in - let ids, def = try + let ids, def = try let ids,s = find_type_custom r in pp_string_parameters ids, str "=" ++ spc () ++ str s with not_found -> diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 5015a50d..8c521ccd 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: ocaml.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) (*s Some utility functions to be reused in module [Haskell]. *) diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 4a881da2..7004a202 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*) +(*i $Id: scheme.ml 7651 2005-12-16 03:19:20Z letouzey $ i*) (*s Production of Scheme syntax. *) diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index 2a828fb9..ef4a3a63 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*) +(*i $Id: scheme.mli 7632 2005-12-01 14:35:21Z letouzey $ i*) (*s Some utility functions to be reused in module [Haskell]. *) diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 9d73d13f..bd4fe924 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) +(*i $Id: table.ml 6555 2005-01-03 19:25:36Z sacerdot $ i*) open Names open Term @@ -22,10 +22,23 @@ open Miniml (*S Utilities concerning [module_path] and [kernel_names] *) -let kn_of_r r = match r with - | ConstRef kn -> kn - | IndRef (kn,_) -> kn - | ConstructRef ((kn,_),_) -> kn +let occur_kn_in_ref kn = + function + | IndRef (kn',_) + | ConstructRef ((kn',_),_) -> kn = kn' + | ConstRef _ -> false + | VarRef _ -> assert false + +let modpath_of_r r = match r with + | ConstRef kn -> con_modpath kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> modpath kn + | VarRef _ -> assert false + +let label_of_r r = match r with + | ConstRef kn -> con_label kn + | IndRef (kn,_) + | ConstructRef ((kn,_),_) -> label kn | VarRef _ -> assert false let current_toplevel () = fst (Lib.current_prefix ()) @@ -45,21 +58,22 @@ let at_toplevel mp = is_modfile mp || is_toplevel mp let visible_kn kn = at_toplevel (base_mp (modpath kn)) +let visible_con kn = at_toplevel (base_mp (con_modpath kn)) (*S The main tables: constants, inductives, records, ... *) (*s Constants tables. *) -let terms = ref (KNmap.empty : ml_decl KNmap.t) -let init_terms () = terms := KNmap.empty -let add_term kn d = terms := KNmap.add kn d !terms -let lookup_term kn = KNmap.find kn !terms +let terms = ref (Cmap.empty : ml_decl Cmap.t) +let init_terms () = terms := Cmap.empty +let add_term kn d = terms := Cmap.add kn d !terms +let lookup_term kn = Cmap.find kn !terms -let types = ref (KNmap.empty : ml_schema KNmap.t) -let init_types () = types := KNmap.empty -let add_type kn s = types := KNmap.add kn s !types -let lookup_type kn = KNmap.find kn !types +let types = ref (Cmap.empty : ml_schema Cmap.t) +let init_types () = types := Cmap.empty +let add_type kn s = types := Cmap.add kn s !types +let lookup_type kn = Cmap.find kn !types (*s Inductives table. *) @@ -70,22 +84,22 @@ let lookup_ind kn = KNmap.find kn !inductives (*s Recursors table. *) -let recursors = ref KNset.empty -let init_recursors () = recursors := KNset.empty +let recursors = ref Cset.empty +let init_recursors () = recursors := Cset.empty let add_recursors env kn = - let make_kn id = make_kn (modpath kn) empty_dirpath (label_of_id id) in + let make_kn id = make_con (modpath kn) empty_dirpath (label_of_id id) in let mib = Environ.lookup_mind kn env in Array.iter (fun mip -> let id = mip.mind_typename in let kn_rec = make_kn (Nameops.add_suffix id "_rec") and kn_rect = make_kn (Nameops.add_suffix id "_rect") in - recursors := KNset.add kn_rec (KNset.add kn_rect !recursors)) + recursors := Cset.add kn_rec (Cset.add kn_rect !recursors)) mib.mind_packets let is_recursor = function - | ConstRef kn -> KNset.mem kn !recursors + | ConstRef kn -> Cset.mem kn !recursors | _ -> false (*s Record tables. *) @@ -109,7 +123,7 @@ let reset_tables () = done before. *) let id_of_global = function - | ConstRef kn -> let _,_,l = repr_kn kn in id_of_label l + | ConstRef kn -> let _,_,l = repr_con kn in id_of_label l | IndRef (kn,i) -> (lookup_ind kn).ind_packets.(i).ip_typename | ConstructRef ((kn,i),j) -> (lookup_ind kn).ind_packets.(i).ip_consnames.(j-1) | _ -> assert false @@ -207,6 +221,18 @@ let _ = declare_bool_option optread = auto_inline; optwrite = (:=) auto_inline_ref} +(*s Extraction TypeExpand *) + +let type_expand_ref = ref true + +let type_expand () = !type_expand_ref + +let _ = declare_bool_option + {optsync = true; + optname = "Extraction TypeExpand"; + optkey = SecondaryTable ("Extraction", "TypeExpand"); + optread = type_expand; + optwrite = (:=) type_expand_ref} (*s Extraction Optimize *) @@ -311,14 +337,22 @@ let add_inline_entries b l = (* Registration of operations for rollback. *) -let (inline_extraction,_) = +let (inline_extraction,_) = declare_object {(default_object "Extraction Inline") with cache_function = (fun (_,(b,l)) -> add_inline_entries b l); load_function = (fun _ (_,(b,l)) -> add_inline_entries b l); export_function = (fun x -> Some x); classify_function = (fun (_,o) -> Substitute o); - subst_function = (fun (_,s,(b,l)) -> (b,(List.map (subst_global s) l))) } + (*CSC: The following substitution may istantiate a realized parameter. + The right solution would be to make the substitution erase the + realizer from the table. However, this is not allowed by Coq. + In this particular case, though, keeping the realizer is place seems + to be harmless since the current code looks for a realizer only + when the constant is a parameter. However, if this behaviour changes + subtle bugs can happear in the future. *) + subst_function = + (fun (_,s,(b,l)) -> (b,(List.map (fun x -> fst (subst_global s x)) l)))} let _ = declare_summary "Extraction Inline" { freeze_function = (fun () -> !inline_table); diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 6160452a..66662138 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*) +(*i $Id: table.mli 6441 2004-12-09 02:27:09Z letouzey $ i*) open Names open Libnames @@ -35,7 +35,9 @@ val check_inside_section : unit -> unit (*s utilities concerning [module_path]. *) -val kn_of_r : global_reference -> kernel_name +val occur_kn_in_ref : kernel_name -> global_reference -> bool +val modpath_of_r : global_reference -> module_path +val label_of_r : global_reference -> label val current_toplevel : unit -> module_path val base_mp : module_path -> module_path @@ -43,14 +45,15 @@ val is_modfile : module_path -> bool val is_toplevel : module_path -> bool val at_toplevel : module_path -> bool val visible_kn : kernel_name -> bool +val visible_con : constant -> bool (*s Some table-related operations *) -val add_term : kernel_name -> ml_decl -> unit -val lookup_term : kernel_name -> ml_decl +val add_term : constant -> ml_decl -> unit +val lookup_term : constant -> ml_decl -val add_type : kernel_name -> ml_schema -> unit -val lookup_type : kernel_name -> ml_schema +val add_type : constant -> ml_schema -> unit +val lookup_type : constant -> ml_schema val add_ind : kernel_name -> ml_ind -> unit val lookup_ind : kernel_name -> ml_ind @@ -58,7 +61,7 @@ val lookup_ind : kernel_name -> ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool -val add_projection : int -> kernel_name -> unit +val add_projection : int -> constant -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int @@ -68,6 +71,10 @@ val reset_tables : unit -> unit val auto_inline : unit -> bool +(*s TypeExpand parameter *) + +val type_expand : unit -> bool + (*s Optimize parameter *) type opt_flag = |