summaryrefslogtreecommitdiff
path: root/contrib/extraction/haskell.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction/haskell.ml')
-rw-r--r--contrib/extraction/haskell.ml280
1 files changed, 280 insertions, 0 deletions
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
new file mode 100644
index 00000000..29c8cd18
--- /dev/null
+++ b/contrib/extraction/haskell.ml
@@ -0,0 +1,280 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(*i $Id: haskell.ml,v 1.40.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+
+(*s Production of Haskell syntax. *)
+
+open Pp
+open Util
+open Names
+open Nameops
+open Libnames
+open Table
+open Miniml
+open Mlutil
+open Ocaml
+
+(*s Haskell renaming issues. *)
+
+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"; "_"; "__";
+ "as"; "qualified"; "hiding" ; "unit" ]
+ Idset.empty
+
+let preamble prm used_modules (mldummy,tdummy,tunknown) =
+ let pp_mp = function
+ | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
+ | _ -> assert false
+ in
+ str "module " ++ pr_upper_id prm.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 mldummy then
+ str "__ = Prelude.error \"Logical or arity value used\""
+ ++ fnl () ++ fnl()
+ else mt())
+
+let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO"
+
+let pp_abst = function
+ | [] -> (mt ())
+ | l -> (str "\\" ++
+ prlist_with_sep (fun () -> (str " ")) pr_id l ++
+ str " ->" ++ spc ())
+
+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)
+
+let pp_global r = P.pp_global !local_mpl r
+let empty_env () = [], P.globals()
+
+(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
+ are needed or not. *)
+
+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,l) ->
+ pp_par par
+ (pp_global 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)
+ | Tdummy -> str "()"
+ | Tunknown -> str "()"
+ | Taxiom -> str "() -- AXIOM TO BE REALIZED\n"
+ | Tcustom s -> str s
+ 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 par' = args <> [] || par
+ and apply st = pp_apply st par args in
+ function
+ | MLrel n ->
+ let id = get_db_name n env in apply (pr_id id)
+ | 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_lams a in
+ let fl,env' = push_vars fl env in
+ let st = (pp_abst (List.rev fl) ++ pp_expr false env' [] a') in
+ apply (pp_par par' st)
+ | MLletin (id,a1,a2) ->
+ let i,env' = push_vars [id] env in
+ let pp_id = pr_id (List.hd i)
+ and pp_a1 = pp_expr false env [] a1
+ and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in
+ hv 0
+ (apply
+ (pp_par par'
+ (hv 0
+ (hov 5
+ (str "let" ++ spc () ++ pp_id ++ str " = " ++ pp_a1) ++
+ spc () ++ str "in") ++
+ spc () ++ hov 0 pp_a2)))
+ | MLglob r ->
+ apply (pp_global r)
+ | MLcons (r,[]) ->
+ assert (args=[]); pp_global r
+ | MLcons (r,[a]) ->
+ assert (args=[]);
+ pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
+ | MLcons (r,args') ->
+ assert (args=[]);
+ pp_par par (pp_global r ++ spc () ++
+ prlist_with_sep spc (pp_expr true env []) args')
+ | MLcase (t, pv) ->
+ apply (pp_par par'
+ (v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
+ fnl () ++ str " " ++ pp_pat env pv)))
+ | MLfix (i,ids,defs) ->
+ let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
+ pp_fix par env' i (Array.of_list (List.rev ids'),defs) args
+ | MLexn s ->
+ (* An [MLexn] may be applied, but I don't really care. *)
+ pp_par par (str "Prelude.error" ++ spc () ++ qs s)
+ | MLdummy ->
+ str "__" (* An [MLdummy] may be applied, but I don't really care. *)
+ | MLmagic a -> pp_expr par env args a
+ | MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
+
+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 ++
+ (match ids with
+ | [] -> mt ()
+ | _ -> (str " " ++
+ prlist_with_sep
+ (fun () -> (spc ())) pr_id (List.rev ids))) ++
+ str " ->" ++ spc () ++ pp_expr par env' [] t)
+ in
+ (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 i (ids,bl) args =
+ pp_par par
+ (v 0
+ (v 2 (str "let" ++ fnl () ++
+ prvect_with_sep fnl
+ (fun (fi,ti) -> pp_function env (pr_id fi) ti)
+ (array_map2 (fun a b -> a,b) ids bl)) ++
+ fnl () ++
+ hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args)))
+
+and pp_function env f t =
+ let bl,t' = collect_lams 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'))
+
+(*s Pretty-printing of inductive types declaration. *)
+
+let pp_comment s = str "-- " ++ s ++ fnl ()
+
+let pp_logical_ind packet =
+ pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++
+ pp_comment (str "with constructors : " ++
+ prvect_with_sep spc pr_id packet.ip_consnames)
+
+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 () ++
+ 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 () ++
+ pp_comment (str "singleton inductive, whose constructor was " ++
+ pr_id packet.ip_consnames.(0)))
+
+let pp_one_ind ip pl cv =
+ let pl = rename_tvars keywords pl in
+ let pp_constructor (r,l) =
+ (pp_global r ++
+ match l with
+ | [] -> (mt ())
+ | _ -> (str " " ++
+ prlist_with_sep
+ (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
+ in
+ str (if cv = [||] 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"
+ else
+ (v 0 (str "= " ++
+ prvect_with_sep (fun () -> fnl () ++ str " | ") pp_constructor
+ (Array.mapi (fun i c -> ConstructRef (ip,i+1),c) cv)))
+
+let rec pp_ind first kn i ind =
+ if i >= Array.length ind.ind_packets then
+ if first then mt () else fnl ()
+ else
+ let ip = (kn,i) in
+ let p = ind.ind_packets.(i) in
+ if is_custom (IndRef (kn,i)) then pp_ind first kn (i+1) ind
+ else
+ if p.ip_logical then
+ pp_logical_ind p ++ pp_ind first kn (i+1) ind
+ else
+ pp_one_ind ip p.ip_vars p.ip_types ++ fnl () ++
+ pp_ind false kn (i+1) ind
+
+
+(*s Pretty-printing of a declaration. *)
+
+let pp_decl mpl =
+ local_mpl := mpl;
+ 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)
+ | Dtype (r, l, t) ->
+ if is_inline_custom r then mt ()
+ else
+ let l = rename_tvars keywords l in
+ let l' = List.rev l in
+ hov 2 (str "type " ++ pp_global r ++ spc () ++
+ prlist (fun id -> pr_id id ++ str " ") l ++
+ str "=" ++ spc () ++ pp_type false l' t) ++ fnl () ++ fnl ()
+ | Dfix (rv, defs,_) ->
+ let ppv = Array.map pp_global rv in
+ prlist_with_sep (fun () -> fnl () ++ fnl ())
+ (fun (pi,ti) -> pp_function (empty_env ()) pi ti)
+ (List.combine (Array.to_list ppv) (Array.to_list defs))
+ ++ fnl () ++ fnl ()
+ | Dterm (r, a, _) ->
+ if is_inline_custom r then mt ()
+ else
+ hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+
+let pp_structure_elem mpl = function
+ | (l,SEdecl d) -> pp_decl mpl 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
+
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 14:05:46 +0000