diff options
author | 2001-05-14 14:49:58 +0000 | |
---|---|---|
committer | 2001-05-14 14:49:58 +0000 | |
commit | 4645fdff5c79865a89444353d4bc6b4b3728fb6f (patch) | |
tree | fed077136746d56e74c3b4929072837a2972413e | |
parent | 3e5ac6441c5241b5082222f139ba33411b28d300 (diff) |
mise en place extraction haskell
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1751 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | .depend | 30 | ||||
-rw-r--r-- | Makefile | 1 | ||||
-rw-r--r-- | contrib/extraction/Extraction.v | 21 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 44 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 430 | ||||
-rw-r--r-- | contrib/extraction/haskell.mli | 16 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 1 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 1 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 38 | ||||
-rw-r--r-- | contrib/extraction/ocaml.mli | 17 | ||||
-rw-r--r-- | contrib/extraction/test/.cvsignore | 1 |
11 files changed, 555 insertions, 45 deletions
@@ -253,11 +253,13 @@ contrib/correctness/pwp.cmi: contrib/correctness/peffect.cmi \ kernel/term.cmi contrib/extraction/extraction.cmi: kernel/environ.cmi \ contrib/extraction/miniml.cmi kernel/names.cmi kernel/term.cmi +contrib/extraction/haskell.cmi: contrib/extraction/miniml.cmi \ + contrib/extraction/mlutil.cmi contrib/extraction/miniml.cmi: kernel/names.cmi lib/pp.cmi kernel/term.cmi contrib/extraction/mlutil.cmi: contrib/extraction/miniml.cmi kernel/names.cmi \ kernel/term.cmi contrib/extraction/ocaml.cmi: contrib/extraction/miniml.cmi \ - contrib/extraction/mlutil.cmi + contrib/extraction/mlutil.cmi kernel/names.cmi lib/pp.cmi contrib/interface/dad.cmi: parsing/coqast.cmi proofs/proof_type.cmi \ proofs/tacmach.cmi contrib/interface/debug_tac.cmi: parsing/coqast.cmi proofs/proof_type.cmi \ @@ -1138,6 +1140,8 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx \ proofs/logic.cmx kernel/names.cmx lib/pp.cmx proofs/proof_trees.cmx \ kernel/reduction.cmx kernel/sign.cmx proofs/tacmach.cmx kernel/term.cmx \ lib/util.cmx tactics/wcclausenv.cmi +tools/coq_vo2xml.cmo: config/coq_config.cmi toplevel/usage.cmi +tools/coq_vo2xml.cmx: config/coq_config.cmx toplevel/usage.cmx tools/coqdep.cmo: config/coq_config.cmi tools/coqdep_lexer.cmo tools/coqdep.cmx: config/coq_config.cmx tools/coqdep_lexer.cmx tools/coqdep_lexer.cmo: config/coq_config.cmi @@ -1392,14 +1396,16 @@ contrib/correctness/peffect.cmx: toplevel/himsg.cmx kernel/names.cmx \ contrib/correctness/peffect.cmi contrib/correctness/penv.cmo: toplevel/himsg.cmi library/lib.cmi \ library/libobject.cmi library/library.cmi kernel/names.cmi \ - contrib/correctness/past.cmi contrib/correctness/perror.cmi \ - contrib/correctness/pmisc.cmi lib/pp.cmi contrib/correctness/ptype.cmi \ - library/summary.cmi kernel/term.cmi contrib/correctness/penv.cmi + lib/options.cmi contrib/correctness/past.cmi \ + contrib/correctness/perror.cmi contrib/correctness/pmisc.cmi lib/pp.cmi \ + contrib/correctness/ptype.cmi library/summary.cmi kernel/term.cmi \ + contrib/correctness/penv.cmi contrib/correctness/penv.cmx: toplevel/himsg.cmx library/lib.cmx \ library/libobject.cmx library/library.cmx kernel/names.cmx \ - contrib/correctness/past.cmi contrib/correctness/perror.cmx \ - contrib/correctness/pmisc.cmx lib/pp.cmx contrib/correctness/ptype.cmi \ - library/summary.cmx kernel/term.cmx contrib/correctness/penv.cmi + lib/options.cmx contrib/correctness/past.cmi \ + contrib/correctness/perror.cmx contrib/correctness/pmisc.cmx lib/pp.cmx \ + contrib/correctness/ptype.cmi library/summary.cmx kernel/term.cmx \ + contrib/correctness/penv.cmi contrib/correctness/perror.cmo: library/declare.cmi kernel/evd.cmi \ library/global.cmi toplevel/himsg.cmi kernel/names.cmi \ contrib/correctness/past.cmi contrib/correctness/peffect.cmi lib/pp.cmi \ @@ -1604,6 +1610,16 @@ contrib/extraction/extraction.cmx: kernel/closure.cmx kernel/declarations.cmx \ contrib/extraction/mlutil.cmx kernel/names.cmx lib/pp.cmx \ kernel/reduction.cmx library/summary.cmx kernel/term.cmx \ pretyping/typing.cmx lib/util.cmx contrib/extraction/extraction.cmi +contrib/extraction/haskell.cmo: kernel/environ.cmi library/global.cmi \ + contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmi \ + kernel/names.cmi contrib/extraction/ocaml.cmi lib/options.cmi lib/pp.cmi \ + lib/pp_control.cmi kernel/term.cmi lib/util.cmi \ + contrib/extraction/haskell.cmi +contrib/extraction/haskell.cmx: kernel/environ.cmx library/global.cmx \ + contrib/extraction/miniml.cmi contrib/extraction/mlutil.cmx \ + kernel/names.cmx contrib/extraction/ocaml.cmx lib/options.cmx lib/pp.cmx \ + lib/pp_control.cmx kernel/term.cmx lib/util.cmx \ + contrib/extraction/haskell.cmi contrib/extraction/mlutil.cmo: kernel/declarations.cmi library/global.cmi \ library/lib.cmi library/libobject.cmi contrib/extraction/miniml.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ @@ -134,6 +134,7 @@ USERTACCMO=$(USERTAC:.ml4=.cmo) USERTACCMX=$(USERTAC:.ml4=.cmx) EXTRACTIONCMO=contrib/extraction/mlutil.cmo contrib/extraction/ocaml.cmo \ + contrib/extraction/haskell.cmo \ contrib/extraction/extraction.cmo \ contrib/extraction/extract_env.cmo diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index b8d295aef..bfe459b18 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -7,17 +7,31 @@ (***********************************************************************) Grammar vernac vernac : ast := + +(* Extraction in the Coq toplevel *) extr_constr [ "Extraction" constrarg($c) "." ] -> [ (Extraction $c) ] | extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] -> [ (ExtractionRec ($LIST $l)) ] -| extr_list + +(* Monolithic extraction to a file *) +| extr_file [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] - -> [ (ExtractionFile $o $f ($LIST $l)) ] + -> [ (ExtractionFile "ocaml" $o $f ($LIST $l)) ] +| haskell_extr_file + [ "Haskell" "Extraction" stringarg($f) options($o) + ne_qualidarg_list($l) "." ] + -> [ (ExtractionFile "haskell" $o $f ($LIST $l)) ] + +(* Modular extraction (one Coq module = one ML module) *) | extr_module [ "Extraction" "Module" options($o) identarg($m) "." ] - -> [ (ExtractionModule $o $m) ] + -> [ (ExtractionModule "ocaml" $o $m) ] +| haskell_extr_module + [ "Haskell" "Extraction" "Module" options($o) identarg($m) "." ] + -> [ (ExtractionModule "haskell" $o $m) ] +(* Overriding of a Coq object by an ML one *) | extract_constant [ "Extract" "Constant" qualidarg($x) "=>" idorstring($y) "." ] -> [ (EXTRACT_CONSTANT $x $y) ] @@ -26,6 +40,7 @@ Grammar vernac vernac : ast := [ "Extract" "Inductive" qualidarg($x) "=>" mindnames($y) "."] -> [ (EXTRACT_INDUCTIVE $x $y) ] +(* Utility entries *) with mindnames : ast := mlconstr [ idorstring($id) "[" idorstring_list($idl) "]" ] -> [(VERNACARGLIST $id ($LIST $idl))] diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index f08e69161..da3d464bb 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -167,15 +167,22 @@ let _ = (*s Extraction parameters. *) -let interp_options keep modular = function +let strict_language = function + | "ocaml" -> true + | "haskell" -> false + | _ -> assert false + +let interp_options lang keep modular m = function | [VARG_STRING "noopt"] -> - { optimization = false; modular = modular; + { optimization = false; modular = modular; module_name = m; to_keep = refs_set_of_list keep; to_expand = Refset.empty } | [VARG_STRING "nooption"] -> - { optimization = true; modular = modular; + { optimization = strict_language lang; + modular = modular; module_name = m; to_keep = refs_set_of_list keep; to_expand = Refset.empty } | VARG_STRING "expand" :: l -> - { optimization = true; modular = modular; + { optimization = strict_language lang; + modular = modular; module_name = m; to_keep = refs_set_of_list keep; to_expand = refs_set_of_list (refs_of_vargl l) } | _ -> @@ -185,17 +192,23 @@ let interp_options keep modular = function The vernacular command is \verb!Extraction "file"! [qualid1] ... [qualidn]. We just call [extract_to_file] on the saturated environment. *) +let extract_to_file = function + | "ocaml" -> Ocaml.extract_to_file + | "haskell" -> Haskell.extract_to_file + | _ -> assert false + let _ = vinterp_add "ExtractionFile" (function - | VARG_VARGLIST o :: VARG_STRING f :: vl -> + | VARG_STRING lang :: VARG_VARGLIST o :: VARG_STRING f :: vl -> let refs = refs_of_vargl vl in - let prm = interp_options refs false o in + let prm = interp_options lang refs false "" o in (fun () -> let decls = decl_of_refs refs in let decls = optimize prm decls in - Ocaml.extract_to_file f prm decls) + extract_to_file lang f prm decls) | _ -> assert false) + (*s Extraction of a module. The vernacular command is \verb!Extraction Module! [M]. We build the environment to extract by traversing the segment of module [M]. We just keep constants and inductives, and we remove @@ -216,20 +229,25 @@ let extract_module m = let decl_mem rl = function | Dglob (r,_) -> List.mem r rl | Dabbrev (r,_,_) -> List.mem r rl - | Dtype((_,r,_)::_, _) -> List.mem r rl - | Dtype([],_) -> false + | Dtype ((_,r,_)::_, _) -> List.mem r rl + | Dtype ([],_) -> false + +let file_suffix = function + | "ocaml" -> ".ml" + | "haskell" -> ".hs" + | _ -> assert false let _ = vinterp_add "ExtractionModule" (function - | [VARG_VARGLIST o; VARG_IDENTIFIER m] -> + | [VARG_STRING lang; VARG_VARGLIST o; VARG_IDENTIFIER m] -> (fun () -> let m = Names.string_of_id m in Ocaml.current_module := m; - let f = (String.uncapitalize m) ^ ".ml" in - let prm = interp_options [] true o in + let f = (String.uncapitalize m) ^ (file_suffix lang) in + let prm = interp_options lang [] true m o in let rl = extract_module m in let decls = optimize prm (decl_of_refs rl) in let decls = List.filter (decl_mem rl) decls in - Ocaml.extract_to_file f prm decls) + extract_to_file lang f prm decls) | _ -> assert false) diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml new file mode 100644 index 000000000..827381d1c --- /dev/null +++ b/contrib/extraction/haskell.ml @@ -0,0 +1,430 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*s Production of Haskell syntax. *) + +open Pp +open Util +open Names +open Term +open Miniml +open Mlutil +open Options +open Ocaml + +let rec collapse_type_app = function + | (Tapp l1) :: l2 -> collapse_type_app (l1 @ l2) + | l -> l + +let space_if = function true -> [< 'sTR " " >] | false -> [< >] + +let sec_space_if = function true -> [< 'sPC >] | false -> [< >] + +(*s Haskell renaming issues. *) + +let haskell_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"; "_"; + "as"; "qualified"; "hiding" ] + Idset.empty + +let current_ids = ref haskell_keywords + +let rec rename_id id avoid = + if Idset.mem id avoid then rename_id (lift_ident id) avoid else id + +let rename_global id = + let id' = rename_id id !current_ids in + current_ids := Idset.add id' !current_ids; + 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)) + +let rename_lower_global id = rename_global (lowercase_id id) +let rename_upper_global id = rename_global (uppercase_id id) + +let pr_lower_id id = pr_id (lowercase_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 == prop_name -> + (* we don't rename propositions binders *) + let (idl', avoid') = rename_vars avoid idl in + (id :: idl', avoid') + | id :: idl -> + let id' = rename_id (lowercase_id id) avoid in + let (idl', avoid') = rename_vars (Idset.add id' avoid) idl in + (id' :: idl', avoid') + +let push_vars ids (db,avoid) = + let ids',avoid' = rename_vars avoid ids in + ids', (ids' @ db, avoid') + +let empty_env () = ([], !current_ids) + +let get_db_name n (db,_) = List.nth db (pred n) + +(*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns + the list [id1;...;idn] and the term [t]. *) + +let collect_lambda = + let rec collect acc = function + | MLlam(id,t) -> collect (id::acc) t + | x -> acc,x + in + collect [] + +let abst = function + | [] -> [< >] + | l -> [< 'sTR "\\ "; + prlist_with_sep (fun ()-> [< 'sTR " " >]) pr_id l; + 'sTR " ->"; 'sPC >] + +let pr_binding = function + | [] -> [< >] + | l -> [< 'sTR " "; prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l >] + +(*s The pretty-printing functor. *) + +module Make = functor(P : Mlpp_param) -> struct + +let pp_reference f r = + try let s = find_ml_extraction r in [< 'sTR s >] + with Not_found -> f r + +let pp_type_global = pp_reference P.pp_type_global +let pp_global = pp_reference P.pp_global + +(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses + are needed or not. *) + +let rec pp_type par t = + let rec pp_rec par = function + | Tvar id -> + pr_id (lowercase_id id) (* TODO: possible clash with Haskell kw *) + | Tapp l -> + (match collapse_type_app l with + | [] -> assert false + | [t] -> pp_rec par t + | t::l -> + [< open_par par; + pp_rec false t; 'sPC; + prlist_with_sep (fun () -> [< 'sPC >]) (pp_type true) l; + close_par par >]) + | Tarr (t1,t2) -> + [< open_par par; pp_rec true t1; 'sPC; 'sTR "->"; 'sPC; + pp_rec false t2; close_par par >] + | Tglob r -> + pp_type_global r + | Tprop -> + string "Prop" + | Tarity -> + string "Arity" + in + hOV 0 (pp_rec par t) + +(*s Pretty-printing of expressions. [par] indicates whether + parentheses are needed or not. [env] is the list of names for the + de Bruijn variables. [args] is the list of collected arguments + (already pretty-printed). *) + +let expr_needs_par = function + | MLlam _ -> true + | MLcase _ -> true + | _ -> false + +let rec pp_expr par env args = + let apply st = match args with + | [] -> st + | _ -> hOV 2 [< open_par par; st; 'sPC; + prlist_with_sep (fun () -> [< 'sPC >]) (fun s -> s) args; + close_par par >] + in + function + | MLrel n -> + apply (pr_id (get_db_name n env)) + | MLapp (f,args') -> + let stl = List.map (pp_expr true env []) args' in + pp_expr par env (stl @ args) f + | MLlam _ as a -> + let fl,a' = collect_lambda a in + let fl,env' = push_vars fl env in + let st = [< abst (List.rev fl); pp_expr false env' [] a' >] in + if args = [] then + [< open_par par; st; close_par par >] + else + apply [< 'sTR "("; st; 'sTR ")" >] + | MLletin (id,a1,a2) -> + let id',env' = push_vars [id] env in + let par' = par || args <> [] in + let par2 = not par' && expr_needs_par a2 in + apply + (hOV 0 [< open_par par'; + hOV 2 [< 'sTR "let "; pr_id (List.hd id'); 'sTR " ="; 'sPC; + pp_expr false env [] a1; 'sPC; 'sTR "in" >]; + 'sPC; + pp_expr par2 env' [] a2; + close_par par' >]) + | MLglob r -> + apply (pp_global r) + | MLcons (r,[]) -> + pp_global r + | MLcons (r,[a]) -> + [< open_par par; pp_global r; 'sPC; + pp_expr true env [] a; close_par par >] + | MLcons (r,args') -> + [< open_par par; pp_global r; 'sPC; + prlist_with_sep (fun () -> [< 'sPC >]) (pp_expr true env []) args'; + close_par par >] + | MLcase (t, pv) -> + apply + [< if args <> [] then [< 'sTR "(" >] else open_par par; + v 0 [< 'sTR "case "; pp_expr false env [] t; 'sTR " of"; + 'fNL; 'sTR " "; pp_pat env pv >]; + if args <> [] then [< 'sTR ")" >] else close_par par >] + | MLfix (i,ids,defs) -> + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args + | MLexn id -> + [< open_par par; 'sTR "error"; 'sPC; + 'qS (string_of_id id); close_par par >] + | MLprop -> + string "prop" + | MLarity -> + string "arity" + | 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 >] + +and pp_pat env 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; + begin match ids with + | [] -> [< >] + | _ -> [< 'sTR " "; + prlist_with_sep + (fun () -> [< 'sPC >]) pr_id (List.rev ids) >] + end; + 'sTR " ->"; 'sPC; pp_expr par env' [] t >] + in + if pv = [||] then + [< 'sTR "_ -> error \"shouldn't happen\" -- empty inductive" >] + else + [< prvect_with_sep (fun () -> [< 'fNL; 'sTR " " >]) pp_one_pat pv >] + +(*s names of the functions ([ids]) are already pushed in [env], + and passed here just for convenience. *) + +and pp_fix par env in_p (ids,bl) args = + [< open_par par; + v 0 [< 'sTR "let { " ; + prvect_with_sep + (fun () -> [< 'sTR "; "; 'fNL >]) + (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (array_map2 (fun id b -> (id,b)) ids bl); + 'sTR " }";'fNL; + match in_p with + | Some j -> + hOV 2 [< 'sTR "in "; pr_id ids.(j); + if args <> [] then + [< 'sTR " "; + prlist_with_sep (fun () -> [<'sTR " ">]) + (fun s -> s) args >] + else + [< >] >] + | None -> + [< >] >]; + close_par par >] + +and pp_function env f t = + let bl,t' = collect_lambda t in + let bl,env' = push_vars bl env in + [< f; pr_binding (List.rev bl); + 'sTR " ="; 'fNL; 'sTR " "; + hOV 2 (pp_expr false env' [] t') >] + +let pp_ast a = hOV 0 (pp_expr false (empty_env ()) [] a) + +(*s Pretty-printing of inductive types declaration. *) + +let pp_one_inductive (pl,name,cl) = + let pp_constructor (id,l) = + [< pp_global id; + match l with + | [] -> [< >] + | _ -> [< 'sTR " " ; + prlist_with_sep + (fun () -> [< 'sTR " " >]) (pp_type true) l >] >] + in + [< 'sTR (if cl = [] then "type " else "data "); + pp_type_global name; 'sTR " "; + prlist_with_sep (fun () -> [< 'sTR " " >]) pr_lower_id pl; + if pl = [] then [< >] else [< 'sTR " " >]; + if cl = [] then + [< 'sTR "= () -- empty inductive" >] + else + [< v 0 [< 'sTR "= "; + prlist_with_sep (fun () -> [< 'fNL; 'sTR " | " >]) + pp_constructor cl >] >] >] + +let pp_inductive il = + [< prlist_with_sep (fun () -> [< 'fNL >]) pp_one_inductive il; 'fNL >] + +(*s Pretty-printing of a declaration. *) + +let pp_decl = function + | Dtype ([], _) -> + [< >] + | Dtype (i, _) -> + hOV 0 (pp_inductive i) + | Dabbrev (r, l, t) -> + hOV 0 [< 'sTR "type "; pp_type_global r; 'sPC; + prlist_with_sep (fun () -> [< 'sTR " " >]) pr_lower_id l; + if l <> [] then [< 'sTR " " >] else [< >]; 'sTR "="; 'sPC; + pp_type false t; 'fNL >] + | Dglob (r, MLfix (i,ids,defs)) -> + let env = empty_env () in + let ids',env' = push_vars (List.rev (Array.to_list ids)) env in + [< prlist_with_sep (fun () -> [< 'fNL >]) + (fun (fi,ti) -> pp_function env' (pr_id fi) ti) + (List.combine (List.rev ids') (Array.to_list defs)); + 'fNL; + let id = P.rename_global r in + let idi = List.nth (List.rev ids') i in + if id <> idi then + [< 'fNL; pr_id id; 'sTR " = "; pr_id idi; 'fNL >] + else + [< >] >] + | Dglob (r, a) -> + hOV 0 [< pp_function (empty_env ()) (pp_global r) a; 'fNL >] + +let pp_type = pp_type false + +end + +(*s Renaming issues for a monolithic extraction. *) + +module MonoParams = struct + +let renamings = Hashtbl.create 97 + +let cache r f = + try Hashtbl.find renamings r + with Not_found -> let id = f r in Hashtbl.add renamings r id; id + +let rename_type_global r = + cache r + (fun r -> + let id = Environ.id_of_global (Global.env()) r in + rename_upper_global id) + +let pp_type_global r = pr_id (rename_type_global r) + +let rename_global r = + cache r + (fun r -> + let id = Environ.id_of_global (Global.env()) r in + match r with + | ConstructRef _ -> rename_upper_global id + | _ -> rename_lower_global id) + +let pp_global r = pr_id (rename_global r) + +let cofix_warning = true + +end + +module MonoPp = Make(MonoParams) + +(*s Renaming issues in a modular extraction. *) + +module ModularParams = struct + + let avoid = + Idset.add (id_of_string "prop") + (Idset.add (id_of_string "arity") haskell_keywords) + + let rename_lower id = + if Idset.mem id avoid || id <> lowercase_id id then + "coq_" ^ string_of_id id + else + string_of_id id + + let rename_upper id = + if Idset.mem id avoid || id <> uppercase_id id then + "Coq_" ^ string_of_id id + else + string_of_id id + + let id_of_global r s = + let sp = match r with + | ConstRef sp -> sp + | IndRef (sp,_) -> sp + | ConstructRef ((sp,_),_) -> sp + | _ -> assert false + in + let m = list_last (dirpath sp) in + id_of_string + (if m = !current_module then s else (String.capitalize m) ^ "." ^ s) + + let rename_type_global r = + let id = Environ.id_of_global (Global.env()) r in + id_of_global r (rename_upper id) + + let rename_global r = + let id = Environ.id_of_global (Global.env()) r in + match r with + | ConstructRef _ -> id_of_global r (rename_upper id) + | _ -> id_of_global r (rename_lower id) + + let pp_type_global r = pr_id (rename_type_global r) + let pp_global r = pr_id (rename_global r) + + let cofix_warning = true +end + +module ModularPp = Make(ModularParams) + +(*s Extraction to a file. *) + +let haskell_preamble prm = + let m = if prm.modular then String.capitalize prm.module_name else "Main" in + [< 'sTR "module "; 'sTR m; 'sTR " where"; 'fNL; 'fNL; + 'sTR "type Prop = ()"; 'fNL; + 'sTR "prop = ()"; 'fNL; 'fNL; + 'sTR "type Arity = ()"; 'fNL; + 'sTR "arity = ()"; 'fNL; 'fNL >] + +let extract_to_file f prm decls = + let pp_decl = if prm.modular then ModularPp.pp_decl else MonoPp.pp_decl in + let cout = open_out f in + let ft = Pp_control.with_output_to cout in + pP_with ft (hV 0 (haskell_preamble prm)); + begin + try + List.iter (fun d -> mSGNL_with ft (pp_decl d)) decls + with e -> + pp_flush_with ft (); close_out cout; raise e + end; + pp_flush_with ft (); + close_out cout diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli new file mode 100644 index 000000000..8e09da5c4 --- /dev/null +++ b/contrib/extraction/haskell.mli @@ -0,0 +1,16 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(*i $Id$ i*) + +(*s Production of Haskell syntax. *) + +open Miniml +open Mlutil + +val extract_to_file : string -> extraction_params -> ml_decl list -> unit diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index fafdcdd01..6413e1ec4 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -227,6 +227,7 @@ module Refset = type extraction_params = { modular : bool; (* modular extraction *) + module_name : string; (* module name if [modular] *) optimization : bool; (* we need optimization *) to_keep : Refset.t; (* globals to keep *) to_expand : Refset.t; (* globals to expand *) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index abfccc36b..381033a01 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -50,6 +50,7 @@ module Refset : Set.S with type elt = global_reference type extraction_params = { modular : bool; (* modular extraction *) + module_name : string; (* module name if [modular] *) optimization : bool; (* we need optimization *) to_keep : Refset.t; (* globals to keep *) to_expand : Refset.t; (* globals to expand *) diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 2fdc8c8ac..750afc782 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -115,7 +115,7 @@ let collect_lambda = let abst = function | [] -> [< >] | l -> [< 'sTR "fun "; - prlist_with_sep (fun ()-> [< 'sTR " " >]) pr_id l; + prlist_with_sep (fun () -> [< 'sTR " " >]) pr_id l; 'sTR " ->"; 'sPC >] let pr_binding = function @@ -311,35 +311,31 @@ let pp_one_inductive (pl,name,cl) = | [] -> [< >] | _ -> [< 'sTR " of " ; prlist_with_sep - (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >] - >] + (fun () -> [< 'sPC ; 'sTR "* " >]) (pp_type true) l >] >] in - [< pp_parameters pl; pp_global name; 'sTR " ="; - if cl = [] then - [< 'sTR " unit (* empty inductive *)" >] - else - [< 'fNL; - v 0 [< 'sTR " "; - prlist_with_sep (fun () -> [< 'fNL; 'sTR " | " >]) - (fun c -> hOV 2 (pp_constructor c)) cl >] >] >] + [< pp_parameters pl; pp_type_global name; 'sTR " ="; + if cl = [] then + [< 'sTR " unit (* empty inductive *)" >] + else + [< 'fNL; + v 0 [< 'sTR " "; + prlist_with_sep (fun () -> [< 'fNL; 'sTR " | " >]) + (fun c -> hOV 2 (pp_constructor c)) cl >] >] >] let pp_inductive il = [< 'sTR "type "; - prlist_with_sep - (fun () -> [< 'fNL; 'sTR "and " >]) - (fun i -> pp_one_inductive i) - il; + prlist_with_sep (fun () -> [< 'fNL; 'sTR "and " >]) pp_one_inductive il; 'fNL >] (*s Pretty-printing of a declaration. *) let warning_coinductive r = - wARN (hOV 0 [< 'sTR "You are trying to extract the CoInductive definition"; 'sPC; - Printer.pr_global r; 'sPC; 'sTR "in Ocaml."; 'sPC; - 'sTR "This is in general NOT a good idea,"; 'sPC; - 'sTR "since Ocaml is not lazy."; 'sPC; - 'sTR "You should consider using Haskell instead." >]) - + wARN (hOV 0 + [< 'sTR "You are trying to extract the CoInductive definition"; 'sPC; + Printer.pr_global r; 'sPC; 'sTR "in Ocaml."; 'sPC; + 'sTR "This is in general NOT a good idea,"; 'sPC; + 'sTR "since Ocaml is not lazy."; 'sPC; + 'sTR "You should consider using Haskell instead." >]) let pp_decl = function | Dtype ([], _) -> diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 74d751051..057d909fa 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -8,11 +8,26 @@ (*i $Id$ i*) +(*s Some utility functions to be reused in module [Haskell]. *) + +open Pp +open Miniml +open Names + +val string : string -> std_ppcmds +val open_par : bool -> std_ppcmds +val close_par : bool -> std_ppcmds + +val collect_lambda : ml_ast -> identifier list * ml_ast +val push_vars : identifier list -> identifier list * Idset.t -> + identifier list * (identifier list * Idset.t) + +val current_module : string ref + (*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. *) -open Miniml open Mlutil module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/test/.cvsignore b/contrib/extraction/test/.cvsignore index 042418cd3..087fa7d9d 100644 --- a/contrib/extraction/test/.cvsignore +++ b/contrib/extraction/test/.cvsignore @@ -3,3 +3,4 @@ ml2v v2ml log +*.h* |