From 74f8c29501ad533bf9bb29c22a885f3bd0f10d04 Mon Sep 17 00:00:00 2001 From: letouzey Date: Mon, 8 Apr 2002 12:25:12 +0000 Subject: ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante dummy git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2619 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/extraction/common.ml | 7 +++++- contrib/extraction/extract_env.ml | 2 +- contrib/extraction/extraction.ml | 42 ++++++++++++++++++++------------ contrib/extraction/haskell.ml | 22 ++++++++--------- contrib/extraction/haskell.mli | 2 +- contrib/extraction/miniml.mli | 1 + contrib/extraction/mlutil.ml | 26 ++++++++++++++------ contrib/extraction/mlutil.mli | 10 +++++--- contrib/extraction/ocaml.ml | 16 +++++++++--- contrib/extraction/ocaml.mli | 2 +- contrib/extraction/test/Makefile.haskell | 2 +- contrib/extraction/test/Unit.hs | 2 -- 12 files changed, 87 insertions(+), 47 deletions(-) delete mode 100644 contrib/extraction/test/Unit.hs (limited to 'contrib') diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index 9cca520ac..3540e9b2a 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -216,6 +216,11 @@ let extract_to_file f prm decls = Idset.remove prm.mod_name (decl_get_modules decls) else Idset.empty in + let print_dummy = match lang() with + | Ocaml -> decl_search MLdummy' decls + | Haskell -> (decl_search MLdummy decls) || (decl_search MLdummy' decls) + | _ -> assert false + in cons_cofix := Refset.empty; current_module := prm.mod_name; Hashtbl.clear renamings; @@ -231,7 +236,7 @@ let extract_to_file f prm decls = if not prm.modular then List.iter (fun r -> pp_with ft (pp_singleton_ind r)) (List.filter decl_is_singleton prm.to_appear); - pp_with ft (preamble prm used_modules); + pp_with ft (preamble prm used_modules print_dummy); begin try List.iter (fun d -> msgnl_with ft (pp_decl d)) decls diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index ef9646b97..d02f9fb32 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -157,7 +157,7 @@ and visit_ast m eenv a = | MLfix (_,_,l) -> Array.iter visit l | MLcast (a,t) -> visit a; visit_type m eenv t | MLmagic a -> visit a - | MLrel _ | MLdummy | MLexn _ -> () + | MLrel _ | MLdummy | MLdummy' | MLexn _ -> () in visit a diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 2c6fb88f6..d3dd78dd5 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -48,7 +48,7 @@ open Nametab type info = Logic | Info -type arity = Arity | NotArity +type arity = Arity | Flexible | Default type flag = info * arity @@ -123,13 +123,20 @@ let _ = declare_summary "Extraction tables" init_function = (fun () -> ()); survive_section = true } -(*S Error messages. *) +(*S Warning & Error messages. *) -let axiom_message sp = +let axiom_error_message sp = errorlabstrm "axiom_message" (str "You must specify an extraction for axiom" ++ spc () ++ pr_sp sp ++ spc () ++ str "first.") +let axiom_warning_message sp = + Options.if_verbose warn + (str "This extraction depends on logical axiom" ++ spc () ++ + pr_sp sp ++ str "." ++ spc() ++ + str "Having false logical axiom in the environment when extracting" ++ + spc () ++ str "may lead to incorrect or non-terminating ML terms.") + let section_message () = errorlabstrm "section_message" (str "You can't extract within a section. Close it and try again.") @@ -147,11 +154,12 @@ let is_axiom sp = (Global.lookup_constant sp).const_body = None (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) -let flag_of_type env t = match find_conclusion env t with +let flag_of_type env t = match find_conclusion env none t with | Sort (Prop Null) -> (Logic,Arity) | Sort _ -> (Info,Arity) - | _ -> if (sort_of env t) = InProp then (Logic,NotArity) - else (Info,NotArity) + | (Case _ | Fix _ | CoFix _) -> + if (sort_of env t) = InProp then (Logic,Flexible) else (Info,Default) + | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default) (*s [is_default] is a particular case of the last function. *) @@ -554,8 +562,10 @@ and extract_constr_to_term env c = (* Same, but With Type (wt). *) and extract_constr_to_term_wt env c t = - if is_default env t then extract_term_wt env c t - else dummy_lams MLdummy (List.length (fst (splay_prod env none t))) + match flag_of_type env t with + | (Info, Default) -> extract_term_wt env c t + | (Logic, Flexible) -> MLdummy' + | _ -> dummy_lams MLdummy (List.length (fst (splay_prod env none t))) (*S Extraction of a constr. *) @@ -572,8 +582,8 @@ and extract_constr_wt env c t = let ctx = ctx_from_sign s in let mlt = extract_type_arity env c ctx (List.length s) in Emltype (mlt, s, vl) - | (Logic, NotArity) -> Emlterm MLdummy - | (Info, NotArity) -> Emlterm (extract_term_wt env c t) + | (Logic, _) -> Emlterm MLdummy + | (Info, _) -> Emlterm (extract_term_wt env c t) (*S Extraction of a constant. *) @@ -584,11 +594,13 @@ and extract_constant sp = let cb = Global.lookup_constant sp in let typ = cb.const_type in match cb.const_body with - | None -> + | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with - | (Info,_) -> axiom_message sp (* We really need some code here *) - | (Logic,NotArity) -> Emlterm MLdummy (* Axiom? I don't mind! *) - | (Logic,Arity) -> Emltype (Tdummy,[],[])) (* Idem *) + | (Info,_) -> axiom_error_message sp + | (Logic,Arity) -> axiom_warning_message sp; + Emltype (Tdummy,[],[]) + | (Logic,_) -> axiom_warning_message sp; + Emlterm MLdummy) | Some body -> let e = match extract_constr_wt env body typ with | Emlterm MLdummy as e -> e @@ -666,7 +678,7 @@ and extract_mib sp = let n = List.length s in let db,ctx = if si=[] then Intmap.empty,[] - else match find_conclusion params_env t with + else match find_conclusion params_env none t with | App (f, args) -> (*i assert (kind_of_term f = Ind ip); i*) let db = parse_ind_args si args in diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 7f6b88d94..9cabd01be 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -27,19 +27,23 @@ let keywords = List.fold_right (fun s -> Idset.add (id_of_string s)) [ "case"; "class"; "data"; "default"; "deriving"; "do"; "else"; "if"; "import"; "in"; "infix"; "infixl"; "infixr"; "instance"; - "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; + "let"; "module"; "newtype"; "of"; "then"; "type"; "where"; "_"; "__"; "as"; "qualified"; "hiding" ; "unit" ] Idset.empty -let preamble prm used_modules = +let preamble prm used_modules print_dummy = let m = String.capitalize (string_of_id prm.mod_name) in str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ - str "import Unit" ++ fnl() ++ str "import qualified Prelude" ++ fnl() ++ Idset.fold (fun m s -> s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl()) used_modules (mt ()) ++ fnl() + ++ + (if print_dummy then + str "__ = Prelude.error \"Logical or arity value used\"" + ++ fnl () ++ fnl() + else mt()) let pp_abst = function | [] -> (mt ()) @@ -152,14 +156,10 @@ let rec pp_expr par env args = (* An [MLexn] may be applied, but I don't really care. *) (open_par par ++ str "Prelude.error" ++ spc () ++ qs s ++ close_par par) - | MLdummy -> - str "unit" (* An [MLdummy] may be applied, but I don't really care. *) - | MLcast (a,t) -> - (open_par true ++ pp_expr false env args a ++ spc () ++ str "::" ++ - spc () ++ pp_type false [] t ++ close_par true) - | MLmagic a -> - (open_par true ++ str "Obj.magic" ++ spc () ++ - pp_expr false env args a ++ close_par true) + | MLdummy | MLdummy' -> + str "__" (* An [MLdummy] may be applied, but I don't really care. *) + | MLcast (a,t) -> pp_expr par env args a + | MLmagic a -> pp_expr par env args a and pp_pat env pv = let pp_one_pat (name,ids,t) = diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 78cabaca9..5d744be2a 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -15,6 +15,6 @@ open Miniml val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> std_ppcmds +val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli index e49f4fa68..67669f8e4 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -43,6 +43,7 @@ type ml_ast = | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy + | MLdummy' | MLcast of ml_ast * ml_type | MLmagic of ml_ast diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index d4941008a..804416a6d 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -30,7 +30,6 @@ exception Impossible let anonymous = id_of_string "x" let dummy_name = id_of_string "_" -let flex_name = id_of_string "flex" let id_of_name = function | Anonymous -> anonymous @@ -70,7 +69,7 @@ let ast_iter_rel f = | MLcons (_,l) -> List.iter (iter n) l | MLcast (a,_) -> iter n a | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy -> () + | MLglob _ | MLexn _ | MLdummy | MLdummy' -> () in iter 0 (*s Map over asts. *) @@ -86,7 +85,7 @@ let ast_map f = function | MLcons (c,l) -> MLcons (c, List.map f l) | MLcast (a,t) -> MLcast (f a, t) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -102,7 +101,7 @@ let ast_map_lift f n = function | MLcons (c,l) -> MLcons (c, List.map (f n) l) | MLcast (a,t) -> MLcast (f n a, t) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> a (*s Iter over asts. *) @@ -117,7 +116,20 @@ let ast_iter f = function | MLcons (c,l) -> List.iter f l | MLcast (a,t) -> f a | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> () + +(*S Searching occurrences of a particular term (no lifting done). *) + +let rec ast_search t a = + if t = a then raise Found else ast_iter (ast_search t) a + +let decl_search t l = + let one_decl = function + | Dglob (_,a) -> ast_search t a + | Dfix (_,c) -> Array.iter (ast_search t) c + | _ -> () + in + try List.iter one_decl l; false with Found -> true (*S Operations concerning De Bruijn indices. *) @@ -379,7 +391,7 @@ let iota_gen br = in iota 0 let is_atomic = function - | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true + | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' -> true | _ -> false (*S The main simplification function. *) @@ -427,7 +439,7 @@ and simpl_app o a = function let a' = List.map (ml_lift k) a in (n, l, simpl o (MLapp (t,a')))) br in simpl o (MLcase (e,br')) - | (MLdummy | MLexn _) as e -> e + | (MLdummy | MLdummy' | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index b4e3d819a..7a6dfb121 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -18,7 +18,6 @@ open Nametab val anonymous : identifier val dummy_name : identifier -val flex_name : identifier val id_of_name : name -> identifier (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns @@ -45,8 +44,6 @@ val sp_of_r : global_reference -> section_path val type_mem_sp : section_path -> ml_type -> bool -(*TODO val get_tvars : ml_type -> identifier list *) - (*s Utility functions over ML terms. [occurs n t] checks whether [Rel n] occurs (freely) in [t]. [ml_lift] is de Bruijn lifting. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. *) @@ -59,6 +56,8 @@ val ml_lift : int -> ml_ast -> ml_ast val ml_subst : ml_ast -> ml_ast -> ml_ast +val decl_search : ml_ast -> ml_decl list -> bool + (*s Some transformations of ML terms. [normalize] simplify all beta redexes (when the argument does not occur, it is just thrown away; when it occurs exactly once it is substituted; otherwise @@ -77,3 +76,8 @@ val optimize : val kill_some_lams : bool list -> identifier list * ml_ast -> identifier list * ml_ast + + + + + diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 36b567203..1df26acc8 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -119,14 +119,19 @@ let keywords = "module"; "mutable"; "new"; "object"; "of"; "open"; "or"; "parser"; "private"; "rec"; "sig"; "struct"; "then"; "to"; "true"; "try"; "type"; "val"; "virtual"; "when"; "while"; "with"; "mod"; - "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ] + "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules = +let preamble _ used_modules print_dummy = Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl()) used_modules (mt ()) ++ - (if Idset.is_empty used_modules then mt () else fnl ()) + (if Idset.is_empty used_modules then mt () else fnl ()) + ++ + (if print_dummy then + str "let (__:unit) = let rec f _ = Obj.magic f in Obj.magic f" + ++ fnl () ++ fnl() + else mt ()) (*s The pretty-printing functor. *) @@ -144,7 +149,8 @@ let empty_env () = [], P.globals() let rec pp_type par vl t = let rec pp_rec par = function - | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i)) + | Tvar i -> (try pp_tvar (List.nth vl (pred i)) + with _ -> (str "'a" ++ int i)) | Tapp l -> (match collapse_type_app l with | [] -> assert false @@ -259,6 +265,8 @@ let rec pp_expr par env args = str ("(* "^s^" *)") ++ close_par par) | MLdummy -> str "()" (* An [MLdummy] may be applied, but I don't really care. *) + | MLdummy' -> + str "__" (* idem *) | MLcast (a,t) -> (open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ spc () ++ pp_type false [] t ++ close_par true) diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 1bfd13b11..2a9170bb0 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -41,7 +41,7 @@ val get_db_name : int -> env -> identifier val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> std_ppcmds +val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds (*s Production of Ocaml syntax. We export both a functor to be used for extraction in the Coq toplevel and a function to extract some diff --git a/contrib/extraction/test/Makefile.haskell b/contrib/extraction/test/Makefile.haskell index ddc6ab4fb..347e99887 100644 --- a/contrib/extraction/test/Makefile.haskell +++ b/contrib/extraction/test/Makefile.haskell @@ -31,7 +31,7 @@ O:= $(patsubst %.hs,%.o,$(HS)) # General rules # -all: v2hs hs Unit.o $(O) +all: v2hs hs $(O) hs: $(HS) diff --git a/contrib/extraction/test/Unit.hs b/contrib/extraction/test/Unit.hs deleted file mode 100644 index 5d104e181..000000000 --- a/contrib/extraction/test/Unit.hs +++ /dev/null @@ -1,2 +0,0 @@ -module Unit where -unit = () -- cgit v1.2.3