diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/common.ml | 26 | ||||
| -rw-r--r-- | contrib/extraction/extraction.ml | 98 | ||||
| -rw-r--r-- | contrib/extraction/haskell.ml | 87 | ||||
| -rw-r--r-- | contrib/extraction/haskell.mli | 4 | ||||
| -rw-r--r-- | contrib/extraction/miniml.mli | 14 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 73 | ||||
| -rw-r--r-- | contrib/extraction/modutil.ml | 18 | ||||
| -rw-r--r-- | contrib/extraction/modutil.mli | 4 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 118 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.mli | 8 | ||||
| -rw-r--r-- | contrib/extraction/scheme.ml | 78 | ||||
| -rw-r--r-- | contrib/extraction/scheme.mli | 4 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 18 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 8 | ||||
| -rw-r--r-- | contrib/funind/tacinv.ml4 | 23 | ||||
| -rw-r--r-- | contrib/funind/tacinvutils.ml | 53 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 14 | ||||
| -rwxr-xr-x | contrib/omega/omega.ml | 10 |
18 files changed, 387 insertions, 271 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 diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4 index b358ff39..1500e1ae 100644 --- a/contrib/funind/tacinv.ml4 +++ b/contrib/funind/tacinv.ml4 @@ -157,11 +157,9 @@ let rec npatternify ltypes c = | [] -> c | (mv,nme,t)::ltypes' -> let c'= substitterm 0 mv (mkRel 1) c in -(* let _ = prconstr c' in *) let tlift = lift (List.length ltypes') t in let res = npatternify ltypes' (mkLambda (newname_append nme "", tlift, c')) in -(* let _ = prconstr res in *) res (* fait une application (c m1 m2...mn, où mi est une evar, on rend également @@ -510,15 +508,15 @@ let rec proofPrinc mi lst_vars lst_eqs lst_recs: | u -> let varrels = List.rev (List.map fst lst_vars) in let varnames = List.map snd lst_vars in - let nb_vars = (List.length varnames) in - let nb_eqs = (List.length lst_eqs) in + let nb_vars = List.length varnames in + let nb_eqs = List.length lst_eqs in let eqrels = List.map fst lst_eqs in (* [terms_recs]: appel rec du fixpoint, On concatène les appels recs trouvés dans les let in et les Cases avec ceux trouves dans u (ie mi.mimick). *) (* TODO: il faudra gérer plusieurs pt fixes imbriqués ? *) - let terms_recs = lst_recs @ (hdMatchSub_cpl mi.mimick mi.fonc) in - + let terms_recs = lst_recs @ hdMatchSub_cpl mi.mimick mi.fonc in + (*c construction du terme: application successive des variables, des egalites et des appels rec, a la variable existentielle correspondant a l'hypothese de recurrence en cours. *) @@ -573,7 +571,6 @@ let invfun_proof fonc def_fonc gl_abstr pis env sigma = sigma=sigma; nmefonc=fonc; fonc=(0,0); doeqs=true; fix=false} in let princ_proof,levar,lposeq,evararr,absc,parms = proofPrinc mi [] [] [] in princ_proof,levar,lposeq,evararr,absc,parms - (* Do intros [i] times, then do rewrite on all introduced hyps which are called like [heq_prefix], FIX: have another filter than the name. *) let rec iterintro i = @@ -596,12 +593,12 @@ let rec iterintro i = (* (fun hyp gl -> - let _ = print_string ("nthhyp= "^ string_of_int i) in + let _ = prstr ("nthhyp= "^ string_of_int i) in if isConst hyp && ((name_of_const hyp)==heq_prefix) then - let _ = print_string "YES\n" in + let _ = prstr "YES\n" in rewriteLR hyp gl else - let _ = print_string "NO\n" in + let _ = prstr "NO\n" in tclIDTAC gl) *) @@ -818,9 +815,9 @@ let buildFunscheme fonc mutflist = (* Declaration of the functional scheme. *) let declareFunScheme f fname mutflist = - let scheme = - buildFunscheme (constr_of f) - (Array.of_list (List.map constr_of (f::mutflist))) in + let flist = if mutflist=[] then [f] else mutflist in + let fcstrlist = Array.of_list (List.map constr_of flist) in + let scheme = buildFunscheme (constr_of f) fcstrlist in let _ = prstr "Principe:" in let _ = prconstr scheme in let ce = { diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml index 6e086d95..a125b9a7 100644 --- a/contrib/funind/tacinvutils.ml +++ b/contrib/funind/tacinvutils.ml @@ -21,7 +21,7 @@ open Reductionops (*s printing of constr -- debugging *) (* comment this line to see debug msgs *) -let msg x = () ;; let prterm c = str "" +let msg x = () ;; let prterm c = str "" (* uncomment this to see debugging *) let prconstr c = msg (str" " ++ prterm c ++ str"\n") let prlistconstr lc = List.iter prconstr lc @@ -194,52 +194,53 @@ let rec buildrefl_from_eqs eqs = -(* list of occurrences of a term inside another, no imbricated - occurrence are considered (ie we stop looking inside a termthat is - an occurrence). *) +(* list of occurrences of a term inside another *) +(* Cofix will be wrong, not sure Fix is correct too *) let rec hdMatchSub u t= - if constr_head_match u t then - u::(fold_constr (fun l cstr -> l@(hdMatchSub cstr t)) - [] - u) - else - fold_constr (fun l cstr -> l@(hdMatchSub cstr t)) - [] - u + let subres = + match kind_of_term u with + | Lambda (nm,tp,cstr) | Prod (nm,tp,cstr) -> hdMatchSub (lift 1 cstr) t + | Fix (_,(lna,tl,bl)) -> + Array.fold_left + (fun acc cstr -> acc @ hdMatchSub (lift (Array.length tl) cstr) t) + [] bl + | LetIn _ -> assert false + (* Correct? *) + | _ -> fold_constr (fun l cstr -> l @ hdMatchSub cstr t) [] u + in + if constr_head_match u t then u :: subres else subres + (* let hdMatchSub_list u lt = List.flatten (List.map (hdMatchSub u) lt) *) let hdMatchSub_cpl u (d,f) = - let res = ref [] in - begin - for i = d to f do res := (hdMatchSub u (mkRel i)) @ !res done; - !res - end + let res = ref [] in + begin + for i = d to f do res := hdMatchSub u (mkRel i) @ !res done; + !res + end (* destApplication raises an exception if [t] is not an application *) let exchange_hd_prod subst_hd t = - let (hd,args)= destApplication t in mkApp (subst_hd,args) + let hd,args= destApplication t in mkApp (subst_hd,args) (* substitute t by by_t in head of products inside in_u, reduces each product found *) let rec substit_red prof t by_t in_u = if constr_head_match in_u (lift prof t) then - let _ = prNamedConstr "in_u" in_u in - let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in - let _ = prNamedConstr "xx " x in - let _ = prstr "\n\n" in - x + let x = whd_beta (exchange_hd_prod (lift prof by_t) in_u) in + x else - map_constr_with_binders succ (fun i u -> substit_red i t by_t u) - prof in_u + map_constr_with_binders succ (fun i u -> substit_red i t by_t u) prof in_u (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each reli by tarr.(f-i). *) let exchange_reli_arrayi tarr (d,f) t = let hd,args= destApplication t in let i = destRel hd in - whd_beta (mkApp (tarr.(f-i) ,args)) + let res = whd_beta (mkApp (tarr.(f-i) ,args)) in + res let exchange_reli_arrayi_L tarr (d,f) = List.map (exchange_reli_arrayi tarr (d,f)) diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 50f5b947..02dc57de 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -195,6 +195,11 @@ let xlate_int_opt = function | Some n -> CT_coerce_INT_to_INT_OPT (CT_int n) | None -> CT_coerce_NONE_to_INT_OPT CT_none +let xlate_int_or_var_opt_to_int_opt = function + | Some (ArgArg n) -> CT_coerce_INT_to_INT_OPT (CT_int n) + | Some (ArgVar _) -> xlate_error "int_or_var: TODO" + | None -> CT_coerce_NONE_to_INT_OPT CT_none + let tac_qualid_to_ct_ID ref = CT_ident (Libnames.string_of_qualid (snd (qualid_of_reference ref))) @@ -1026,12 +1031,12 @@ and xlate_tac = (if a3 then CT_destructing else CT_coerce_NONE_to_DESTRUCTING CT_none), (if a4 then CT_usingtdb else CT_coerce_NONE_to_USINGTDB CT_none)) | TacAutoTDB nopt -> CT_autotdb (xlate_int_opt nopt) - | TacAuto (nopt, Some []) -> CT_auto (xlate_int_opt nopt) + | TacAuto (nopt, Some []) -> CT_auto (xlate_int_or_var_opt_to_int_opt nopt) | TacAuto (nopt, None) -> - CT_auto_with (xlate_int_opt nopt, + CT_auto_with (xlate_int_or_var_opt_to_int_opt nopt, CT_coerce_STAR_to_ID_NE_LIST_OR_STAR CT_star) | TacAuto (nopt, Some (id1::idl)) -> - CT_auto_with(xlate_int_opt nopt, + CT_auto_with(xlate_int_or_var_opt_to_int_opt nopt, CT_coerce_ID_NE_LIST_to_ID_NE_LIST_OR_STAR( CT_id_ne_list(CT_ident id1, List.map (fun x -> CT_ident x) idl))) |TacExtend(_, ("autorewritev7"|"autorewritev8"), l::t) -> @@ -1141,7 +1146,8 @@ and xlate_tac = | TacClearBody([]) -> assert false | TacClearBody(a::l) -> CT_clear_body (CT_id_ne_list (xlate_hyp a, List.map xlate_hyp l)) - | TacDAuto (a, b) -> CT_dauto(xlate_int_opt a, xlate_int_opt b) + | TacDAuto (a, b) -> + CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b) | TacNewDestruct(a,b,(c,_)) -> CT_new_destruct (xlate_int_or_constr a, xlate_using b, diff --git a/contrib/omega/omega.ml b/contrib/omega/omega.ml index f2eeb5fe..f0eb1e78 100755 --- a/contrib/omega/omega.ml +++ b/contrib/omega/omega.ml @@ -13,7 +13,7 @@ (* *) (**************************************************************************) -(* $Id: omega.ml,v 1.7.2.1 2004/07/16 19:30:13 herbelin Exp $ *) +(* $Id: omega.ml,v 1.7.2.2 2005/02/17 18:25:20 herbelin Exp $ *) open Util open Hashtbl @@ -520,9 +520,11 @@ let rec depend relie_on accu = function depend (e1.id::e2.id::relie_on) (act::accu) l else depend relie_on accu l - | STATE (e,_,_,_,_) -> - if List.mem e.id relie_on then depend relie_on (act::accu) l - else depend relie_on accu l + | STATE (e,_,o,_,_) -> + if List.mem e.id relie_on then + depend (o.id::relie_on) (act::accu) l + else + depend relie_on accu l | HYP e -> if List.mem e.id relie_on then depend relie_on (act::accu) l else depend relie_on accu l |