summaryrefslogtreecommitdiff
path: root/contrib/extraction
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/extraction')
-rw-r--r--contrib/extraction/common.ml26
-rw-r--r--contrib/extraction/extraction.ml98
-rw-r--r--contrib/extraction/haskell.ml87
-rw-r--r--contrib/extraction/haskell.mli4
-rw-r--r--contrib/extraction/miniml.mli14
-rw-r--r--contrib/extraction/mlutil.ml73
-rw-r--r--contrib/extraction/modutil.ml18
-rw-r--r--contrib/extraction/modutil.mli4
-rw-r--r--contrib/extraction/ocaml.ml118
-rw-r--r--contrib/extraction/ocaml.mli8
-rw-r--r--contrib/extraction/scheme.ml78
-rw-r--r--contrib/extraction/scheme.mli4
-rw-r--r--contrib/extraction/table.ml18
-rw-r--r--contrib/extraction/table.mli8
14 files changed, 334 insertions, 224 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 53a2631e..8e441613 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.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: common.ml,v 1.51.2.4 2005/12/16 03:07:39 letouzey Exp $ i*)
open Pp
open Util
@@ -269,11 +269,18 @@ module StdParams = struct
(* TODO: remettre des conditions [lang () = Haskell] disant de qualifier. *)
+ let unquote s =
+ if lang () <> Scheme then s
+ else
+ let s = String.copy s in
+ for i=0 to String.length s - 1 do if s.[i] = '\'' then s.[i] <- '~' done;
+ s
+
let rec dottify = function
| [] -> assert false
- | [s] -> s
- | s::[""] -> s
- | s::l -> (dottify l)^"."^s
+ | [s] -> unquote s
+ | s::[""] -> unquote s
+ | s::l -> (dottify l)^"."^(unquote s)
let pp_global mpl r =
let ls = get_renamings r in
@@ -353,7 +360,7 @@ let preamble prm = match lang () with
| Ocaml -> Ocaml.preamble prm
| Haskell -> Haskell.preamble prm
| Scheme -> Scheme.preamble prm
- | Toplevel -> (fun _ _ -> mt ())
+ | Toplevel -> (fun _ _ _ -> mt ())
let preamble_sig prm = match lang () with
| Ocaml -> Ocaml.preamble_sig prm
@@ -374,7 +381,6 @@ let info f =
(str ("The file "^f^" has been created by extraction."))
let print_structure_to_file f prm struc =
- cons_cofix := Refset.empty;
Hashtbl.clear renamings;
mod_1st_level := Idmap.empty;
modcontents := Gset.empty;
@@ -387,9 +393,13 @@ let print_structure_to_file f prm struc =
else (create_mono_renamings struc; [])
in
let print_dummys =
- (struct_ast_search MLdummy struc,
+ (struct_ast_search ((=) MLdummy) struc,
struct_type_search Tdummy struc,
struct_type_search Tunknown struc)
+ in
+ let print_magic =
+ if lang () <> Haskell then false
+ else struct_ast_search (function MLmagic _ -> true | _ -> false) struc
in
(* print the implementation *)
let cout = option_app (fun (f,_) -> open_out f) f in
@@ -397,7 +407,7 @@ let print_structure_to_file f prm struc =
| None -> !Pp_control.std_ft
| Some cout -> Pp_control.with_output_to cout in
begin try
- msg_with ft (preamble prm used_modules print_dummys);
+ msg_with ft (preamble prm used_modules print_dummys print_magic);
msg_with ft (pp_struct struc);
option_iter close_out cout;
with e ->
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 46bf06dd..6bfe861f 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.1 2004/07/16 19:30:07 herbelin Exp $ i*)
+(*i $Id: extraction.ml,v 1.136.2.4 2005/12/01 11:27:15 letouzey Exp $ i*)
(*i*)
open Util
@@ -183,15 +183,17 @@ let rec extract_type env db j c args =
| (Info, Default) ->
(* Standard case: two [extract_type] ... *)
let mld = extract_type env' (0::db) j d [] in
- if mld = Tdummy then Tdummy
+ if type_eq (mlt_env env) mld Tdummy then Tdummy
else Tarr (extract_type env db 0 t [], mld)
| (Info, TypeScheme) when j > 0 ->
(* A new type var. *)
let mld = extract_type env' (j::db) (j+1) d [] in
- if mld = Tdummy then Tdummy else Tarr (Tdummy, mld)
+ if type_eq (mlt_env env) mld Tdummy then Tdummy
+ else Tarr (Tdummy, mld)
| _ ->
let mld = extract_type env' (0::db) j d [] in
- if mld = Tdummy then Tdummy else Tarr (Tdummy, mld))
+ if type_eq (mlt_env env) mld Tdummy then Tdummy
+ else Tarr (Tdummy, mld))
| Sort _ -> Tdummy (* The two logical cases. *)
| _ when sort_of env (applist (c, args)) = InProp -> Tdummy
| Rel n ->
@@ -343,38 +345,53 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
if List.length l = 1 && not (type_mem_kn kn (List.hd l))
then raise (I Singleton);
if l = [] then raise (I Standard);
+ if not mib.mind_record then raise (I Standard);
let ip = (kn, 0) in
- if is_custom (IndRef ip) then raise (I Standard);
- let projs =
- try (find_structure ip).s_PROJ
- with Not_found -> raise (I Standard);
+ let r = IndRef ip in
+ if is_custom r then raise (I Standard);
+ (* Now we're sure it's a record. *)
+ (* First, we find its field names. *)
+ 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
+ | _ -> []
in
- let n = nb_default_params env mip0.mind_nf_arity in
- let projs = try List.map out_some projs with _ -> raise (I Standard) in
- let is_true_proj kn =
- let (_,body) = Sign.decompose_lam_assum (constant_value env kn) in
- match kind_of_term body with
- | Rel _ -> false
- | Case _ -> true
- | _ -> assert false
+ let field_names =
+ list_skipn mip0.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 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
+ if not (List.mem false (type_to_sign (mlt_env env) typ)) then
+ projs := KNset.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
+ else error_record r
+ | _ -> assert false
in
- let projs = List.filter is_true_proj projs in
- let rec check = function
- | [] -> [],[]
- | (typ, kn) :: l ->
- let l1,l2 = check l in
- if type_eq (mlt_env env) Tdummy typ then l1,l2
- else
- let r = ConstRef kn in
- if List.mem false (type_to_sign (mlt_env env) typ)
- then r :: l1, l2
- else r :: l1, r :: l2
- in
- add_record kn n (check (List.combine typ projs));
- raise (I Record)
+ let field_glob = select_fields field_names typ
+ in
+ (* Is this record officially declared with its projections ? *)
+ (* If so, we use this information. *)
+ begin try
+ 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
+ with Not_found -> ()
+ end;
+ Record field_glob
with (I info) -> info
in
- let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
+ let i = {ind_info = ind_info; ind_nparams = npar; ind_packets = packets} in
add_ind kn i;
internal_call := KNset.remove kn !internal_call;
i
@@ -564,7 +581,9 @@ and extract_cst_app env mle mlt kn args =
(* Different situations depending of the number of arguments: *)
if ls = 0 then put_magic_if magic2 head
else if List.mem true s then
- if la >= ls then put_magic_if (magic2 && not magic1) (MLapp (head, mla))
+ if la >= ls || not (List.mem false s)
+ then
+ put_magic_if (magic2 && not magic1) (MLapp (head, mla))
else
(* Not enough arguments. We complete via eta-expansion. *)
let ls' = ls-la in
@@ -599,7 +618,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in
let type_cons = instantiation (nb_tvars, type_cons) in
(* Then, the usual variables [s], [ls], [la], ... *)
- let s = List.map ((<>) Tdummy) types in
+ let s = List.map (type_neq env Tdummy) types in
let ls = List.length s in
let la = List.length args in
assert (la <= ls + params_nb);
@@ -614,7 +633,7 @@ and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args =
let head mla =
if mi.ind_info = Singleton then
put_magic_if magic1 (List.hd mla) (* assert (List.length mla = 1) *)
- else put_magic_if magic1 (MLcons (ConstructRef cp, mla))
+ else put_magic_if magic1 (MLcons (mi.ind_info, ConstructRef cp, mla))
in
(* Different situations depending of the number of arguments: *)
if la < params_nb then
@@ -670,10 +689,12 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
(* The types of the arguments of the corresponding constructor. *)
let f t = type_subst_vect metas (type_expand env t) in
let l = List.map f oi.ip_types.(i) in
+ (* the corresponding signature *)
+ let s = List.map (type_neq env Tdummy) oi.ip_types.(i) in
(* Extraction of the branch (in functional form). *)
let e = extract_maybe_term env mle (type_recomp (l,mlt)) br.(i) in
(* We suppress dummy arguments according to signature. *)
- let ids,e = case_expunge (List.map ((<>) Tdummy) l) e in
+ let ids,e = case_expunge s e in
(ConstructRef (ip,i+1), List.rev ids, e)
in
if mi.ind_info = Singleton then
@@ -687,7 +708,7 @@ and extract_case env mle ((kn,i) as ip,c,br) mlt =
end
else
(* Standard case: we apply [extract_branch]. *)
- MLcase (a, Array.init br_size extract_branch)
+ MLcase (mi.ind_info, a, Array.init br_size extract_branch)
(*s Extraction of a (co)-fixpoint. *)
@@ -726,7 +747,7 @@ let extract_std_constant env kn body typ =
(* The real type [t']: without head lambdas, expanded, *)
(* and with [Tvar] translated to [Tvar'] (not instantiable). *)
let l,t' = type_decomp (type_expand env (var2var' t)) in
- let s = List.map ((<>) Tdummy) l in
+ let s = List.map (type_neq env Tdummy) l in
(* The initial ML environment. *)
let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in
(* Decomposing the top level lambdas of [body]. *)
@@ -836,7 +857,8 @@ let logical_decl = function
| Dterm (_,MLdummy,Tdummy) -> true
| Dtype (_,[],Tdummy) -> true
| Dfix (_,av,tv) ->
- (array_for_all ((=) MLdummy) av) && (array_for_all ((=) Tdummy) tv)
+ (array_for_all ((=) MLdummy) av) &&
+ (array_for_all ((=) Tdummy) tv)
| Dind (_,i) -> array_for_all (fun ip -> ip.ip_logical) i.ind_packets
| _ -> false
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 29c8cd18..3834fe81 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: haskell.ml,v 1.40.2.5 2005/12/16 04:11:28 letouzey Exp $ i*)
(*s Production of Haskell syntax. *)
@@ -27,23 +27,41 @@ let keywords =
[ "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" ]
+ "as"; "qualified"; "hiding" ; "unit" ; "unsafeCoerce" ]
Idset.empty
-let preamble prm used_modules (mldummy,tdummy,tunknown) =
+let preamble prm used_modules (mldummy,tdummy,tunknown) magic =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
in
+ (if not 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 ()
++ fnl() ++
str "import qualified Prelude" ++ fnl() ++
prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
++ fnl () ++
- (if mldummy then
+ (if not magic then mt ()
+ else str "\
+#ifdef __GLASGOW_HASKELL__
+import qualified GHC.Base
+unsafeCoerce = GHC.Base.unsafeCoerce#
+#else
+-- HUGS
+import qualified IOExts
+unsafeCoerce = IOExts.unsafeCoerce
+#endif")
+ ++
+ fnl() ++ fnl()
+ ++
+ (if not mldummy then mt ()
+ else
str "__ = Prelude.error \"Logical or arity value used\""
- ++ fnl () ++ fnl()
- else mt())
+ ++ fnl () ++ fnl())
let preamble_sig prm used_modules (mldummy,tdummy,tunknown) = failwith "TODO"
@@ -61,27 +79,36 @@ 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 pp_global r =
+ if is_inline_custom r then str (find_custom r)
+ else 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 kn_sig =
+ let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
+ make_kn specif empty_dirpath (mk_label "sig")
+
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)
+ 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)
| 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)
@@ -125,16 +152,16 @@ let rec pp_expr par env args =
spc () ++ hov 0 pp_a2)))
| MLglob r ->
apply (pp_global r)
- | MLcons (r,[]) ->
+ | MLcons (_,r,[]) ->
assert (args=[]); pp_global r
- | MLcons (r,[a]) ->
+ | MLcons (_,r,[a]) ->
assert (args=[]);
pp_par par (pp_global r ++ spc () ++ pp_expr true env [] a)
- | MLcons (r,args') ->
+ | MLcons (_,r,args') ->
assert (args=[]);
pp_par par (pp_global r ++ spc () ++
prlist_with_sep spc (pp_expr true env []) args')
- | MLcase (t, pv) ->
+ | MLcase (_,t, pv) ->
apply (pp_par par'
(v 0 (str "case " ++ pp_expr false env [] t ++ str " of" ++
fnl () ++ str " " ++ pp_pat env pv)))
@@ -146,7 +173,8 @@ let rec pp_expr par env args =
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
+ | MLmagic a ->
+ pp_apply (str "unsafeCoerce") par (pp_expr true env [] a :: args)
| MLaxiom -> pp_par par (str "Prelude.error \"AXIOM TO BE REALIZED\"")
and pp_pat env pv =
@@ -210,7 +238,7 @@ let pp_one_ind ip pl cv =
| [] -> (mt ())
| _ -> (str " " ++
prlist_with_sep
- (fun () -> (str " ")) (pp_type true (List.rev pl)) l))
+ (fun () -> (str " ")) (pp_type true pl) l))
in
str (if cv = [||] then "type " else "data ") ++
pp_global (IndRef ip) ++ str " " ++
@@ -239,6 +267,8 @@ let rec pp_ind first kn i ind =
(*s Pretty-printing of a declaration. *)
+let pp_string_parameters ids = prlist (fun id -> str id ++ str " ")
+
let pp_decl mpl =
local_mpl := mpl;
function
@@ -248,21 +278,32 @@ let pp_decl mpl =
| 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 ()
+ let l = rename_tvars keywords l in
+ let st =
+ try
+ let ids,s = find_type_custom r in
+ prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s
+ with not_found ->
+ prlist (fun id -> pr_id id ++ str " ") l ++
+ 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 ()
| 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, _) ->
+ | Dterm (r, a, t) ->
if is_inline_custom r then mt ()
else
- hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl () ++ fnl ())
+ let e = pp_global r in
+ e ++ str " :: " ++ pp_type false [] t ++ fnl () ++
+ if is_custom r then
+ hov 0 (e ++ str " = " ++ str (find_custom r) ++ fnl() ++ fnl ())
+ else
+ hov 0 (pp_function (empty_env ()) e a ++ fnl () ++ fnl ())
let pp_structure_elem mpl = function
| (l,SEdecl d) -> pp_decl mpl d
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 4da5db0c..822444bd 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: haskell.mli,v 1.15.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
open Pp
open Names
@@ -15,6 +15,6 @@ open Miniml
val keywords : Idset.t
val preamble :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 866ff847..7c18f9f5 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: miniml.mli,v 1.46.2.3 2005/12/01 16:43:58 letouzey Exp $ i*)
(*s Target language for extraction: a core ML called MiniML. *)
@@ -35,7 +35,6 @@ type ml_type =
| Tdummy
| Tunknown
| Taxiom
- | Tcustom of string
and ml_meta = { id : int; mutable contents : ml_type option }
@@ -46,7 +45,11 @@ type ml_schema = int * ml_type
(*s ML inductive types. *)
-type inductive_info = Record | Singleton | Coinductive | Standard
+type inductive_info =
+ | Singleton
+ | Coinductive
+ | Standard
+ | Record of global_reference list
(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
If the inductive is logical ([ip_logical = false]), then all other fields
@@ -79,8 +82,9 @@ type ml_ast =
| MLlam of identifier * ml_ast
| MLletin of identifier * ml_ast * ml_ast
| MLglob of global_reference
- | MLcons of global_reference * ml_ast list
- | MLcase of ml_ast * (global_reference * identifier list * ml_ast) array
+ | MLcons of inductive_info * global_reference * ml_ast list
+ | MLcase of inductive_info * ml_ast *
+ (global_reference * identifier list * ml_ast) array
| MLfix of int * identifier array * ml_ast array
| MLexn of string
| MLdummy
diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml
index fbe423a7..c01766b0 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: mlutil.ml,v 1.104.2.3 2005/12/01 16:28:04 letouzey Exp $ i*)
(*i*)
open Pp
@@ -117,9 +117,9 @@ let rec mgu = function
let needs_magic p = try mgu p; false with Impossible -> true
-let put_magic_if b a = if b then MLmagic a else a
+let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
-let put_magic p a = if needs_magic p then MLmagic a else a
+let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
(*S ML type env. *)
@@ -327,11 +327,11 @@ let ast_iter_rel f =
| MLrel i -> f (i-n)
| MLlam (_,a) -> iter (n+1) a
| MLletin (_,a,b) -> iter n a; iter (n+1) b
- | MLcase (a,v) ->
+ | MLcase (_,a,v) ->
iter n a; Array.iter (fun (_,l,t) -> iter (n + (List.length l)) t) v
| MLfix (_,ids,v) -> let k = Array.length ids in Array.iter (iter (n+k)) v
| MLapp (a,l) -> iter n a; List.iter (iter n) l
- | MLcons (_,l) -> List.iter (iter n) l
+ | MLcons (_,_,l) -> List.iter (iter n) l
| MLmagic a -> iter n a
| MLglob _ | MLexn _ | MLdummy | MLaxiom -> ()
in iter 0
@@ -343,10 +343,10 @@ let ast_map_case f (c,ids,a) = (c,ids,f a)
let ast_map f = function
| MLlam (i,a) -> MLlam (i, f a)
| MLletin (i,a,b) -> MLletin (i, f a, f b)
- | MLcase (a,v) -> MLcase (f a, Array.map (ast_map_case f) v)
+ | MLcase (i,a,v) -> MLcase (i,f a, Array.map (ast_map_case f) v)
| MLfix (i,ids,v) -> MLfix (i, ids, Array.map f v)
| MLapp (a,l) -> MLapp (f a, List.map f l)
- | MLcons (c,l) -> MLcons (c, List.map f l)
+ | MLcons (i,c,l) -> MLcons (i,c, List.map f l)
| MLmagic a -> MLmagic (f a)
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
@@ -357,11 +357,11 @@ let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a)
let ast_map_lift f n = function
| MLlam (i,a) -> MLlam (i, f (n+1) a)
| MLletin (i,a,b) -> MLletin (i, f n a, f (n+1) b)
- | MLcase (a,v) -> MLcase (f n a,Array.map (ast_map_lift_case f n) v)
+ | MLcase (i,a,v) -> MLcase (i,f n a,Array.map (ast_map_lift_case f n) v)
| MLfix (i,ids,v) ->
let k = Array.length ids in MLfix (i,ids,Array.map (f (k+n)) v)
| MLapp (a,l) -> MLapp (f n a, List.map (f n) l)
- | MLcons (c,l) -> MLcons (c, List.map (f n) l)
+ | MLcons (i,c,l) -> MLcons (i,c, List.map (f n) l)
| MLmagic a -> MLmagic (f n a)
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> a
@@ -372,10 +372,10 @@ let ast_iter_case f (c,ids,a) = f a
let ast_iter f = function
| MLlam (i,a) -> f a
| MLletin (i,a,b) -> f a; f b
- | MLcase (a,v) -> f a; Array.iter (ast_iter_case f) v
+ | MLcase (_,a,v) -> f a; Array.iter (ast_iter_case f) v
| MLfix (i,ids,v) -> Array.iter f v
| MLapp (a,l) -> f a; List.iter f l
- | MLcons (c,l) -> List.iter f l
+ | MLcons (_,c,l) -> List.iter f l
| MLmagic a -> f a
| MLrel _ | MLglob _ | MLexn _ | MLdummy | MLaxiom as a -> ()
@@ -411,7 +411,7 @@ let nb_occur t = nb_occur_k 1 t
let nb_occur_match =
let rec nb k = function
| MLrel i -> if i = k then 1 else 0
- | MLcase(a,v) ->
+ | MLcase(_,a,v) ->
(nb k a) +
Array.fold_left
(fun r (_,ids,a) -> max r (nb (k+(List.length ids)) a)) 0 v
@@ -420,7 +420,7 @@ let nb_occur_match =
Array.fold_left (fun r a -> r+(nb k a)) 0 v
| MLlam (_,a) -> nb (k+1) a
| MLapp (a,l) -> List.fold_left (fun r a -> r+(nb k a)) (nb k a) l
- | MLcons (_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
+ | MLcons (_,_,l) -> List.fold_left (fun r a -> r+(nb k a)) 0 l
| MLmagic a -> nb k a
| MLglob _ | MLexn _ | MLdummy | MLaxiom -> 0
in nb 1
@@ -616,7 +616,7 @@ let check_and_generalize (r0,l,c) =
if i'<1 then c
else if i'>nargs then MLrel (i-nargs+1)
else raise Impossible
- | MLcons(r,args) when r=r0 && (test_eta_args_lift n nargs args) ->
+ | MLcons(_,r,args) when r=r0 && (test_eta_args_lift n nargs args) ->
MLrel (n+1)
| a -> ast_map_lift genrec n a
in genrec 0 c
@@ -707,7 +707,7 @@ let rec permut_case_fun br acc =
let rec is_iota_gen = function
| MLcons _ -> true
- | MLcase(_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
+ | MLcase(_,_,br)-> array_for_all (fun (_,_,t)->is_iota_gen t) br
| _ -> false
let constructor_index = function
@@ -716,15 +716,15 @@ let constructor_index = function
let iota_gen br =
let rec iota k = function
- | MLcons (r,a) ->
+ | MLcons (i,r,a) ->
let (_,ids,c) = br.(constructor_index r) in
let c = List.fold_right (fun id t -> MLlam (id,t)) ids c in
let c = ast_lift k c in
MLapp (c,a)
- | MLcase(e,br') ->
+ | MLcase(i,e,br') ->
let new_br =
Array.map (fun (n,i,c)->(n,i,iota (k+(List.length i)) c)) br'
- in MLcase(e, new_br)
+ in MLcase(i,e, new_br)
| _ -> assert false
in iota 0
@@ -741,13 +741,18 @@ let rec simpl o = function
simpl o f
| MLapp (f, a) ->
simpl_app o (List.map (simpl o) a) (simpl o f)
- | MLcase (e,br) ->
+ | MLcase (i,e,br) ->
let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in
- simpl_case o br (simpl o e)
- | MLletin(id,c,e) when
- (id = dummy_name) || (is_atomic c) || (is_atomic e) ||
- (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let)) ->
+ simpl_case o i br (simpl o e)
+ | MLletin(id,c,e) ->
+ let e = (simpl o e) in
+ if
+ (id = dummy_name) || (is_atomic c) || (is_atomic e) ||
+ (let n = nb_occur_match e in n = 0 || (n=1 && o.opt_lin_let))
+ then
simpl o (ast_subst c e)
+ else
+ MLletin(id, simpl o c, e)
| MLfix(i,ids,c) ->
let n = Array.length ids in
if ast_occurs_itvl 1 n c.(i) then
@@ -770,7 +775,7 @@ and simpl_app o a = function
| MLletin (id,e1,e2) when o.opt_let_app ->
(* Application of a letin: we push arguments inside *)
MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a)))
- | MLcase (e,br) when o.opt_case_app ->
+ | MLcase (i,e,br) when o.opt_case_app ->
(* Application of a case: we push arguments inside *)
let br' =
Array.map
@@ -778,16 +783,16 @@ and simpl_app o a = function
let k = List.length l in
let a' = List.map (ast_lift k) a in
(n, l, simpl o (MLapp (t,a')))) br
- in simpl o (MLcase (e,br'))
+ in simpl o (MLcase (i,e,br'))
| (MLdummy | MLexn _) as e -> e
(* We just discard arguments in those cases. *)
| f -> MLapp (f,a)
-and simpl_case o br e =
+and simpl_case o i br e =
if o.opt_case_iot && (is_iota_gen e) then (* Generalized iota-redex *)
simpl o (iota_gen br e)
else
- try (* Does a term [f] exist such as each branch is [(f e)] ? *)
+ try (* Does a term [f] exist such that each branch is [(f e)] ? *)
if not o.opt_case_idr then raise Impossible;
let f = check_generalizable_case o.opt_case_idg br in
simpl o (MLapp (MLlam (anonymous,f),[e]))
@@ -801,9 +806,9 @@ and simpl_case o br e =
then
let ids,br = permut_case_fun br [] in
let n = List.length ids in
- if n <> 0 then named_lams ids (MLcase (ast_lift n e, br))
- else MLcase (e, br)
- else MLcase (e,br)
+ if n <> 0 then named_lams ids (MLcase (i,ast_lift n e, br))
+ else MLcase (i,e,br)
+ else MLcase (i,e,br)
let rec post_simpl = function
| MLletin(_,c,e) when (is_atomic (eta_red c)) ->
@@ -1006,8 +1011,8 @@ let optimize_fix a =
let rec ml_size = function
| MLapp(t,l) -> List.length l + ml_size t + ml_size_list l
| MLlam(_,t) -> 1 + ml_size t
- | MLcons(_,l) -> ml_size_list l
- | MLcase(t,pv) ->
+ | MLcons(_,_,l) -> ml_size_list l
+ | MLcase(_,t,pv) ->
1 + ml_size t + (Array.fold_right (fun (_,_,t) a -> a + ml_size t) pv 0)
| MLfix(_,_,f) -> ml_size_array f
| MLletin (_,_,t) -> ml_size t
@@ -1061,7 +1066,7 @@ let rec non_stricts add cand = function
| MLapp (t,l)->
let cand = non_stricts false cand t in
List.fold_left (non_stricts false) cand l
- | MLcons (_,l) ->
+ | MLcons (_,_,l) ->
List.fold_left (non_stricts false) cand l
| MLletin (_,t1,t2) ->
let cand = non_stricts false cand t1 in
@@ -1071,7 +1076,7 @@ let rec non_stricts add cand = function
let cand = lift n cand in
let cand = Array.fold_left (non_stricts false) cand f in
pop n cand
- | MLcase (t,v) ->
+ | MLcase (_,t,v) ->
(* The only interesting case: for a variable to be non-strict, *)
(* it is sufficient that it appears non-strict in at least one branch, *)
(* so we make an union (in fact a merge). *)
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index feb9e54e..54f0c992 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: modutil.ml,v 1.7.2.4 2005/12/01 17:01:22 letouzey Exp $ i*)
open Names
open Declarations
@@ -157,6 +157,10 @@ let struct_iter do_decl do_spec s =
type do_ref = global_reference -> unit
+let record_iter_references do_term = function
+ | Record l -> List.iter do_term l
+ | _ -> ()
+
let type_iter_references do_type t =
let rec iter = function
| Tglob (r,l) -> do_type r; List.iter iter l
@@ -169,8 +173,12 @@ let ast_iter_references do_term do_cons do_type a =
ast_iter iter a;
match a with
| MLglob r -> do_term r
- | MLcons (r,_) -> do_cons r
- | MLcase (_,v) as a -> Array.iter (fun (r,_,_) -> do_cons r) v
+ | MLcons (i,r,_) ->
+ if lang () = Ocaml then record_iter_references do_term i;
+ do_cons r
+ | MLcase (i,_,v) as a ->
+ if lang () = Ocaml then record_iter_references do_term i;
+ Array.iter (fun (r,_,_) -> do_cons r) v
| _ -> ()
in iter a
@@ -180,7 +188,7 @@ let ind_iter_references do_term do_cons do_type kn ind =
let packet_iter ip p =
do_type (IndRef ip); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types
in
- if ind.ind_info = Record then List.iter do_term (find_projections kn);
+ if lang () = Ocaml then record_iter_references do_term ind.ind_info;
Array.iteri (fun i -> packet_iter (kn,i)) ind.ind_packets
let decl_iter_references do_term do_cons do_type =
@@ -236,7 +244,7 @@ let struct_get_references_list struc =
exception Found
let rec ast_search t a =
- if t = a then raise Found else ast_iter (ast_search t) a
+ if t a then raise Found else ast_iter (ast_search t) a
let decl_ast_search t = function
| Dterm (_,a,_) -> ast_search t a
diff --git a/contrib/extraction/modutil.mli b/contrib/extraction/modutil.mli
index f73e18f7..7f8c4113 100644
--- a/contrib/extraction/modutil.mli
+++ b/contrib/extraction/modutil.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: modutil.mli,v 1.2.2.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: modutil.mli,v 1.2.2.2 2005/12/01 17:01:22 letouzey Exp $ i*)
open Names
open Declarations
@@ -42,7 +42,7 @@ val add_labels_mp : module_path -> label list -> module_path
(*s Functions upon ML modules. *)
-val struct_ast_search : ml_ast -> ml_structure -> bool
+val struct_ast_search : (ml_ast -> bool) -> ml_structure -> bool
val struct_type_search : ml_type -> ml_structure -> bool
type do_ref = global_reference -> unit
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 707ef94f..ff9cfd21 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: ocaml.ml,v 1.100.2.6 2005/12/01 17:01:22 letouzey Exp $ i*)
(*s Production of Ocaml syntax. *)
@@ -20,8 +20,6 @@ open Miniml
open Mlutil
open Modutil
-let cons_cofix = ref Refset.empty
-
(*s Some utility functions. *)
let pp_par par st = if par then str "(" ++ st ++ str ")" else st
@@ -68,6 +66,12 @@ let sec_space_if = function true -> spc () | false -> mt ()
let fnl2 () = fnl () ++ fnl ()
+let pp_parameters l =
+ (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
+
+let pp_string_parameters l =
+ (pp_boxed_tuple str l ++ space_if (l<>[]))
+
(*s Generic renaming issues. *)
let rec rename_id id avoid =
@@ -126,7 +130,7 @@ let keywords =
"land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ]
Idset.empty
-let preamble _ used_modules (mldummy,tdummy,tunknown) =
+let preamble _ used_modules (mldummy,tdummy,tunknown) _ =
let pp_mp = function
| MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
| _ -> assert false
@@ -167,22 +171,33 @@ let pp_global r =
let empty_env () = [], P.globals ()
+exception NoRecord
+
+let find_projections = function Record l -> l | _ -> raise NoRecord
+
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
+let kn_sig =
+ let specif = MPfile (dirpath_of_string "Coq.Init.Specif") in
+ make_kn specif empty_dirpath (mk_label "sig")
+
let rec pp_type par vl t =
let rec pp_rec par = function
| Tmeta _ | Tvar' _ | Taxiom -> assert false
| Tvar i -> (try pp_tvar (List.nth vl (pred i))
with _ -> (str "'a" ++ int i))
| Tglob (r,[]) -> pp_global r
- | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_global r
+ | Tglob (r,l) ->
+ if r = IndRef (kn_sig,0) then
+ pp_tuple_light pp_rec l
+ else
+ pp_tuple_light pp_rec l ++ spc () ++ pp_global r
| Tarr (t1,t2) ->
pp_par par
(pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2)
| Tdummy -> str "__"
| Tunknown -> str "__"
- | Tcustom s -> str s
in
hov 0 (pp_rec par t)
@@ -193,7 +208,7 @@ let rec pp_type par vl t =
let expr_needs_par = function
| MLlam _ -> true
- | MLcase (_,[|_|]) -> false
+ | MLcase (_,_,[|_|]) -> false
| MLcase _ -> true
| _ -> false
@@ -231,30 +246,32 @@ let rec pp_expr par env args =
let record = List.hd args in
pp_apply (record ++ str "." ++ pp_global r) par (List.tl args)
with _ -> apply (pp_global r))
- | MLcons (r,[]) ->
+ | MLcons (Coinductive,r,[]) ->
assert (args=[]);
- if Refset.mem r !cons_cofix then
- pp_par par (str "lazy " ++ pp_global r)
- else pp_global r
- | MLcons (r,args') ->
- (try
- let projs = find_projections (kn_of_r r) in
- pp_record_pat (projs, List.map (pp_expr true env []) args')
- with Not_found ->
- assert (args=[]);
- let tuple = pp_tuple (pp_expr true env []) args' in
- if Refset.mem r !cons_cofix then
- pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
- else pp_par par (pp_global r ++ spc () ++ tuple))
- | MLcase (t, pv) ->
+ pp_par par (str "lazy " ++ pp_global r)
+ | MLcons (Coinductive,r,args') ->
+ assert (args=[]);
+ let tuple = pp_tuple (pp_expr true env []) args' in
+ pp_par par (str "lazy (" ++ pp_global r ++ spc() ++ tuple ++str ")")
+ | MLcons (_,r,[]) ->
+ assert (args=[]);
+ pp_global r
+ | MLcons (Record projs, r, args') ->
+ assert (args=[]);
+ pp_record_pat (projs, List.map (pp_expr true env []) args')
+ | MLcons (_,r,args') ->
+ assert (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 Refset.mem r !cons_cofix then
+ let expr = if i = Coinductive then
(str "Lazy.force" ++ spc () ++ pp_expr true env [] t)
else
(pp_expr false env [] t)
in
(try
- let projs = find_projections (kn_of_r r) in
+ let projs = find_projections i in
let (_, ids, c) = pv.(0) in
let n = List.length ids in
match c with
@@ -263,17 +280,17 @@ let rec pp_expr par env args =
pp_global (List.nth projs (n-i))))
| MLapp (MLrel i, a) when i <= n ->
if List.exists (ast_occurs_itvl 1 n) a
- then raise Not_found
+ then raise NoRecord
else
let ids,env' = push_vars (List.rev ids) env in
(pp_apply
(pp_expr true env [] t ++ str "." ++
pp_global (List.nth projs (n-i)))
par ((List.map (pp_expr true env' []) a) @ args))
- | _ -> raise Not_found
- with Not_found ->
+ | _ -> raise NoRecord
+ with NoRecord ->
if Array.length pv = 1 then
- let s1,s2 = pp_one_pat env pv.(0) in
+ let s1,s2 = pp_one_pat env i pv.(0) in
apply
(hv 0
(pp_par par'
@@ -285,7 +302,7 @@ let rec pp_expr par env args =
apply
(pp_par par'
(v 0 (str "match " ++ expr ++ str " with" ++
- fnl () ++ str " | " ++ pp_pat env pv))))
+ fnl () ++ str " | " ++ pp_pat env i 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
@@ -307,21 +324,21 @@ and pp_record_pat (projs, args) =
(List.combine projs args) ++
str " }"
-and pp_one_pat env (r,ids,t) =
+and pp_one_pat env i (r,ids,t) =
let ids,env' = push_vars (List.rev ids) env in
let expr = pp_expr (expr_needs_par t) env' [] t in
try
- let projs = find_projections (kn_of_r r) in
+ let projs = find_projections i in
pp_record_pat (projs, List.rev_map pr_id ids), expr
- with Not_found ->
+ with NoRecord ->
let args =
if ids = [] then (mt ())
else str " " ++ pp_boxed_tuple pr_id (List.rev ids) in
pp_global r ++ args, expr
-and pp_pat env pv =
+and pp_pat env i pv =
prvect_with_sep (fun () -> (fnl () ++ str " | "))
- (fun x -> let s1,s2 = pp_one_pat env x in
+ (fun x -> let s1,s2 = pp_one_pat env i x in
hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv
and pp_function env f t =
@@ -331,20 +348,17 @@ and pp_function env f t =
let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in
not (List.exists (fun (k,t0) -> ast_occurs (k+1) t0) ktl)
in
- let is_not_cofix pv =
- let (r,_,_) = pv.(0) in not (Refset.mem r !cons_cofix)
- in
match t' with
- | MLcase(MLrel 1,pv) when is_not_cofix pv ->
+ | MLcase(i,MLrel 1,pv) when i=Standard ->
if is_function pv then
(f ++ pr_binding (List.rev (List.tl bl)) ++
str " = function" ++ fnl () ++
- v 0 (str " | " ++ pp_pat env' pv))
+ v 0 (str " | " ++ pp_pat env' i pv))
else
(f ++ pr_binding (List.rev bl) ++
str " = match " ++
pr_id (List.hd bl) ++ str " with" ++ fnl () ++
- v 0 (str " | " ++ pp_pat env' pv))
+ v 0 (str " | " ++ pp_pat env' i pv))
| _ -> (f ++ pr_binding (List.rev bl) ++
str " =" ++ fnl () ++ str " " ++
@@ -384,12 +398,6 @@ let rec pp_Dfix init i ((rv,c,t) as fix) =
(*s Pretty-printing of inductive types declaration. *)
-let pp_parameters l =
- (pp_boxed_tuple pp_tvar l ++ space_if (l<>[]))
-
-let pp_string_parameters l =
- (pp_boxed_tuple str l ++ space_if (l<>[]))
-
let pp_one_ind prefix ip pl cv =
let pl = rename_tvars keywords pl in
let pp_constructor (r,l) =
@@ -420,9 +428,8 @@ let pp_singleton kn packet =
pp_comment (str "singleton inductive, whose constructor was " ++
pr_id packet.ip_consnames.(0)))
-let pp_record kn packet =
- let l = List.combine (find_projections kn) packet.ip_types.(0) in
- let projs = find_projections kn in
+let pp_record kn projs packet =
+ let l = List.combine projs packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
str "type " ++ pp_parameters pl ++ pp_global (IndRef (kn,0)) ++ str " = { "++
hov 0 (prlist_with_sep (fun () -> str ";" ++ spc ())
@@ -466,13 +473,9 @@ let pp_ind co kn ind =
let pp_mind kn i =
match i.ind_info with
| Singleton -> pp_singleton kn i.ind_packets.(0)
- | Coinductive ->
- let nop _ = ()
- and add r = cons_cofix := Refset.add r !cons_cofix in
- decl_iter_references nop add nop (Dind (kn,i));
- pp_ind true kn i
- | Record -> pp_record kn i.ind_packets.(0)
- | _ -> pp_ind false kn i
+ | Coinductive -> pp_ind true kn i
+ | Record projs -> pp_record kn projs i.ind_packets.(0)
+ | Standard -> pp_ind false kn i
let pp_decl mpl =
local_mpl := mpl;
@@ -481,6 +484,7 @@ let pp_decl mpl =
| Dtype (r, l, t) ->
if is_inline_custom r then failwith "empty phrase"
else
+ let pp_r = pp_global r in
let l = rename_tvars keywords l in
let ids, def = try
let ids,s = find_type_custom r in
@@ -490,7 +494,7 @@ let pp_decl mpl =
if t = Taxiom then str "(* AXIOM TO BE REALIZED *)"
else str "=" ++ spc () ++ pp_type false l t
in
- hov 2 (str "type" ++ spc () ++ ids ++ pp_global r ++
+ hov 2 (str "type" ++ spc () ++ ids ++ pp_r ++
spc () ++ def)
| Dterm (r, a, t) ->
if is_inline_custom r then failwith "empty phrase"
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 711c15da..5015a50d 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: ocaml.mli,v 1.26.6.3 2005/12/01 17:01:22 letouzey Exp $ i*)
(*s Some utility functions to be reused in module [Haskell]. *)
@@ -15,8 +15,6 @@ open Names
open Libnames
open Miniml
-val cons_cofix : Refset.t ref
-
val pp_par : bool -> std_ppcmds -> std_ppcmds
val pp_abst : identifier list -> std_ppcmds
val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
@@ -39,10 +37,10 @@ val get_db_name : int -> env -> identifier
val keywords : Idset.t
val preamble :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
val preamble_sig :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*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/scheme.ml b/contrib/extraction/scheme.ml
index 61045304..4a881da2 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: scheme.ml,v 1.9.2.5 2005/12/16 03:07:39 letouzey Exp $ i*)
(*s Production of Scheme syntax. *)
@@ -24,17 +24,30 @@ open Ocaml
let keywords =
List.fold_right (fun s -> Idset.add (id_of_string s))
- [ "define"; "let"; "lambda"; "lambdas"; "match-case";
+ [ "define"; "let"; "lambda"; "lambdas"; "match";
"apply"; "car"; "cdr";
"error"; "delay"; "force"; "_"; "__"]
Idset.empty
-let preamble _ _ (mldummy,_,_) =
+let preamble _ _ (mldummy,_,_) _ =
+ str ";; This extracted scheme code relies on some additional macros" ++
+ fnl () ++
+ str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
+ fnl () ++
+ str "(load \"macros_extr.scm\")" ++
+ fnl () ++ fnl () ++
(if mldummy then
str "(define __ (lambda (_) __))"
++ fnl () ++ fnl()
else mt ())
+let pr_id id =
+ let s = string_of_id id in
+ for i = 0 to String.length s - 1 do
+ if s.[i] = '\'' then s.[i] <- '~'
+ done;
+ str s
+
let paren = pp_par true
let pp_abst st = function
@@ -43,6 +56,12 @@ let pp_abst st = function
| l -> paren
(str "lambdas " ++ paren (prlist_with_sep spc pr_id l) ++ spc () ++ st)
+let pp_apply st _ = function
+ | [] -> st
+ | [a] -> hov 2 (paren (st ++ spc () ++ a))
+ | args -> hov 2 (paren (str "@ " ++ st ++
+ (prlist (fun x -> spc () ++ x) args)))
+
(*s The pretty-printing functor. *)
module Make = functor(P : Mlpp_param) -> struct
@@ -63,7 +82,7 @@ let rec pp_expr env args =
| MLlam _ as a ->
let fl,a' = collect_lams a in
let fl,env' = push_vars fl env in
- pp_abst (pp_expr env' [] a') (List.rev fl)
+ apply (pp_abst (pp_expr env' [] a') (List.rev fl))
| MLletin (id,a1,a2) ->
let i,env' = push_vars [id] env in
apply
@@ -77,46 +96,46 @@ let rec pp_expr env args =
++ spc () ++ hov 0 (pp_expr env' [] a2)))))
| MLglob r ->
apply (pp_global r)
- | MLcons (r,args') ->
+ | MLcons (i,r,args') ->
assert (args=[]);
let st =
str "`" ++
paren (pp_global r ++
- (if args' = [] then mt () else (spc () ++ str ",")) ++
- prlist_with_sep
- (fun () -> spc () ++ str ",")
- (pp_expr env []) args')
+ (if args' = [] then mt () else spc ()) ++
+ prlist_with_sep spc (pp_cons_args env) args')
in
- if Refset.mem r !cons_cofix then
- paren (str "delay " ++ st)
- else st
- | MLcase (t, pv) ->
- let r,_,_ = pv.(0) in
- let e = if Refset.mem r !cons_cofix then
- paren (str "force" ++ spc () ++ pp_expr env [] t)
- else
- pp_expr env [] t
- in apply (v 3 (paren
- (str "match-case " ++ e ++ fnl () ++ pp_pat env pv)))
+ if i = Coinductive then paren (str "delay " ++ st) else st
+ | MLcase (i,t, pv) ->
+ let e =
+ if i <> Coinductive then pp_expr env [] t
+ else paren (str "force" ++ spc () ++ pp_expr env [] t)
+ in
+ apply (v 3 (paren (str "match " ++ e ++ fnl () ++ pp_pat env pv)))
| MLfix (i,ids,defs) ->
let ids',env' = push_vars (List.rev (Array.to_list ids)) env in
pp_fix env' i (Array.of_list (List.rev ids'),defs) args
| MLexn s ->
(* An [MLexn] may be applied, but I don't really care. *)
- paren (str "absurd")
+ paren (str "error" ++ spc () ++ qs s)
| MLdummy ->
str "__" (* An [MLdummy] may be applied, but I don't really care. *)
| MLmagic a ->
pp_expr env args a
- | MLaxiom -> paren (str "absurd ;;AXIOM TO BE REALIZED\n")
+ | MLaxiom -> paren (str "error \"AXIOM TO BE REALIZED\"")
+
+and pp_cons_args env = function
+ | MLcons (i,r,args) when i<>Coinductive ->
+ paren (pp_global r ++
+ (if args = [] then mt () else spc ()) ++
+ prlist_with_sep spc (pp_cons_args env) args)
+ | e -> str "," ++ pp_expr env [] e
and pp_one_pat env (r,ids,t) =
- let pp_arg id = str "?" ++ pr_id id in
let ids,env' = push_vars (List.rev ids) env in
let args =
if ids = [] then mt ()
- else (str " " ++ prlist_with_sep spc pp_arg (List.rev ids))
+ else (str " " ++ prlist_with_sep spc pr_id (List.rev ids))
in
(pp_global r ++ args), (pp_expr env' [] t)
@@ -133,7 +152,8 @@ and pp_fix env j (ids,bl) args =
(str "letrec " ++
(v 0 (paren
(prvect_with_sep fnl
- (fun (fi,ti) -> paren ((pr_id fi) ++ (pp_expr env [] ti)))
+ (fun (fi,ti) ->
+ paren ((pr_id fi) ++ spc () ++ (pp_expr env [] ti)))
(array_map2 (fun id b -> (id,b)) ids bl)) ++
fnl () ++
hov 2 (pp_apply (pr_id (ids.(j))) true args))))
@@ -156,8 +176,12 @@ let pp_decl _ = function
| Dterm (r, a, _) ->
if is_inline_custom r then mt ()
else
- hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
- pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
+ if is_custom r then
+ hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+ str (find_custom r))) ++ fnl () ++ fnl ()
+ else
+ hov 2 (paren (str "define " ++ pp_global r ++ spc () ++
+ pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
let pp_structure_elem mp = function
| (l,SEdecl d) -> pp_decl mp d
diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli
index 6e689a47..2a828fb9 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: scheme.mli,v 1.6.6.2 2005/12/01 17:01:22 letouzey Exp $ i*)
(*s Some utility functions to be reused in module [Haskell]. *)
@@ -17,7 +17,7 @@ open Names
val keywords : Idset.t
val preamble :
- extraction_params -> module_path list -> bool * bool * bool -> std_ppcmds
+ extraction_params -> module_path list -> bool*bool*bool -> bool -> std_ppcmds
module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index a65c51a4..9d73d13f 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.1 2004/07/16 19:30:08 herbelin Exp $ i*)
+(*i $Id: table.ml,v 1.35.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
open Names
open Term
@@ -90,17 +90,9 @@ let is_recursor = function
(*s Record tables. *)
-let records = ref (KNmap.empty : global_reference list KNmap.t)
-let init_records () = records := KNmap.empty
-
let projs = ref (Refmap.empty : int Refmap.t)
let init_projs () = projs := Refmap.empty
-
-let add_record kn n (l1,l2) =
- records := KNmap.add kn l1 !records;
- projs := List.fold_right (fun r -> Refmap.add r n) l2 !projs
-
-let find_projections kn = KNmap.find kn !records
+let add_projection n kn = projs := Refmap.add (ConstRef kn) n !projs
let is_projection r = Refmap.mem r !projs
let projection_arity r = Refmap.find r !projs
@@ -108,7 +100,7 @@ let projection_arity r = Refmap.find r !projs
let reset_tables () =
init_terms (); init_types (); init_inductives (); init_recursors ();
- init_records (); init_projs ()
+ init_projs ()
(*s Printing. *)
@@ -196,6 +188,10 @@ let error_MPfile_as_mod d =
err (str ("The whole file "^(string_of_dirpath d)^".v is used somewhere as a module.\n"^
"Extraction cannot currently deal with this situation.\n"))
+let error_record r =
+ err (str "Record " ++ Printer.pr_global r ++ str " has an anonymous field." ++ fnl () ++
+ str "To help extraction, please use an explicit name.")
+
(*S The Extraction auxiliary commands *)
(*s Extraction AutoInline *)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 680638e5..6160452a 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.1 2004/07/16 19:30:09 herbelin Exp $ i*)
+(*i $Id: table.mli,v 1.25.2.2 2005/11/29 21:40:51 letouzey Exp $ i*)
open Names
open Libnames
@@ -29,7 +29,7 @@ val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
val error_unqualified_name : string -> string -> 'a
val error_MPfile_as_mod : dir_path -> 'a
-
+val error_record : global_reference -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
@@ -58,9 +58,7 @@ val lookup_ind : kernel_name -> ml_ind
val add_recursors : Environ.env -> kernel_name -> unit
val is_recursor : global_reference -> bool
-val add_record :
- kernel_name -> int -> global_reference list * global_reference list -> unit
-val find_projections : kernel_name -> global_reference list
+val add_projection : int -> kernel_name -> unit
val is_projection : global_reference -> bool
val projection_arity : global_reference -> int
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-07 03:18:15 +0000