diff options
Diffstat (limited to 'contrib/extraction/haskell.ml')
-rw-r--r-- | contrib/extraction/haskell.ml | 90 |
1 files changed, 46 insertions, 44 deletions
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; +} |