diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/extraction/common.ml | 16 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 24 | ||||
-rw-r--r-- | contrib/extraction/extraction.ml | 911 | ||||
-rw-r--r-- | contrib/extraction/haskell.ml | 15 | ||||
-rw-r--r-- | contrib/extraction/haskell.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/miniml.mli | 20 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 414 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 74 | ||||
-rw-r--r-- | contrib/extraction/ocaml.ml | 137 | ||||
-rw-r--r-- | contrib/extraction/ocaml.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/scheme.ml | 13 | ||||
-rw-r--r-- | contrib/extraction/scheme.mli | 2 | ||||
-rw-r--r-- | contrib/extraction/table.mli | 1 | ||||
-rw-r--r-- | contrib/extraction/test/.depend | 732 | ||||
-rw-r--r-- | contrib/extraction/test/Makefile | 18 | ||||
-rwxr-xr-x | contrib/extraction/test/make_mli | 17 | ||||
-rw-r--r-- | contrib/extraction/test_extraction.v | 11 |
17 files changed, 1615 insertions, 794 deletions
diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml index bd08e8d3c..ccf350015 100644 --- a/contrib/extraction/common.ml +++ b/contrib/extraction/common.ml @@ -71,8 +71,9 @@ let decl_get_modules ld = List.iter (fun (_,l) -> List.iter (mltype_get_modules m) l) l) l | Dtype (_,_,t) -> mltype_get_modules m t - | Dterm (_,a) -> ast_get_modules m a - | Dfix(_,c) -> Array.iter (ast_get_modules m) c + | Dterm (_,a,t) -> ast_get_modules m a; mltype_get_modules m t + | Dfix(_,c,t) -> Array.iter (ast_get_modules m) c; + Array.iter (mltype_get_modules m) t | _ -> () in List.iter one_decl ld; @@ -218,11 +219,10 @@ let extract_to_file f prm decls = Idset.remove prm.mod_name (decl_get_modules decls) else Idset.empty in - let print_dummy = match lang() with - | Ocaml | Scheme -> decl_search MLdummy' decls - | Haskell -> (decl_search MLdummy decls) || (decl_search MLdummy' decls) - | _ -> assert false - in + let print_dummys = + (decl_search MLdummy decls, + decl_type_search Tdummy decls, + decl_type_search Tunknown decls) in cons_cofix := Refset.empty; current_module := prm.mod_name; Hashtbl.clear renamings; @@ -236,7 +236,7 @@ let extract_to_file f prm decls = if not prm.modular then List.iter (fun r -> pp_with ft (pp_singleton_ind r)) (List.filter decl_is_singleton prm.to_appear); - pp_with ft (preamble prm used_modules print_dummy); + pp_with ft (preamble prm used_modules print_dummys); begin try List.iter (fun d -> msgnl_with ft (pp_decl d)) decls diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index e6fa6e822..f286883e4 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -52,14 +52,13 @@ let check_r m sm r = then clash_error sm m rlm let check_decl m sm = function - | Dterm (r,_) -> check_r m sm r + | Dterm (r,_,_) -> check_r m sm r | Dtype (r,_,_) -> check_r m sm r | Dind ((_,r,_)::_, _) -> check_r m sm r | Dind ([],_) -> () - | DdummyType r -> check_r m sm r | DcustomTerm (r,_) -> check_r m sm r | DcustomType (r,_) -> check_r m sm r - | Dfix(rv,_) -> Array.iter (check_r m sm) rv + | Dfix(rv,_,_) -> Array.iter (check_r m sm) rv (* [check_one_module] checks that no module names in [l] clashes with [m]. *) @@ -144,6 +143,7 @@ and visit_type m eenv t = | Tglob (r,l) -> visit_reference m eenv r; List.iter visit l | Tarr (t1,t2) -> visit t1; visit t2 | Tvar _ | Tdummy | Tunknown -> () + | Tmeta _ | Tvar' _ -> assert false in visit t @@ -160,7 +160,7 @@ and visit_ast m eenv a = | MLfix (_,_,l) -> Array.iter visit l | MLcast (a,t) -> visit a; visit_type m eenv t | MLmagic a -> visit a - | MLrel _ | MLdummy | MLdummy' | MLexn _ -> () + | MLrel _ | MLdummy | MLexn _ -> () in visit a @@ -172,8 +172,10 @@ and visit_inductive m eenv inds = and visit_decl m eenv = function | Dind (inds,_) -> visit_inductive m eenv inds | Dtype (_,_,t) -> visit_type m eenv t - | Dterm (_,a) -> visit_ast m eenv a - | Dfix (_,c) -> Array.iter (visit_ast m eenv) c + | Dterm (_,a,t) -> visit_ast m eenv a; visit_type m eenv t + | Dfix (_,c,t) -> + Array.iter (visit_ast m eenv) c; + Array.iter (visit_type m eenv) t | _ -> () (*s Recursive extracted environment for a list of reference: we just @@ -204,14 +206,13 @@ let print_user_extract r = spc () ++ str (find_ml_extraction r) ++ fnl ()) let decl_in_r r0 = function - | Dterm (r,_) -> r = r0 + | Dterm (r,_,_) -> r = r0 | Dtype (r,_,_) -> r = r0 | Dind ((_,r,_)::_, _) -> kn_of_r r = kn_of_r r0 | Dind ([],_) -> false - | DdummyType r -> r = r0 | DcustomTerm (r,_) -> r = r0 | DcustomType (r,_) -> r = r0 - | Dfix (rv,_) -> array_exists ((=) r0) rv + | Dfix (rv,_,_) -> array_exists ((=) r0) rv let extraction qid = let r = Nametab.global qid in @@ -275,14 +276,13 @@ let extraction_file f vl = \verb!Extraction Module! [M]. *) let decl_in_m m = function - | Dterm (r,_) -> m = long_module r + | Dterm (r,_,_) -> m = long_module r | Dtype (r,_,_) -> m = long_module r | Dind ((_,r,_)::_, _) -> m = long_module r | Dind ([],_) -> false - | DdummyType r -> m = long_module r | DcustomTerm (r,_) -> m = long_module r | DcustomType (r,_) -> m = long_module r - | Dfix (rv,_) -> m = long_module rv.(0) + | Dfix (rv,_,_) -> m = long_module rv.(0) let module_file_name m = match lang () with | Ocaml -> (String.uncapitalize (string_of_id m)) ^ ".ml" diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 4888c8fef..c46703430 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -32,26 +32,25 @@ open Nametab (*S Extraction results. *) -(* The type [flag] gives us information about an identifier - coming from a Lambda or a Product: +(* The type [flag] gives us information about any Coq term: \begin{itemize} - \item [Arity] denotes identifiers of type an arity of some sort [Set], - [Prop] or [Type], that is $(x_1:X_1)\ldots(x_n:X_n)s$ with [s = Set], - [Prop] or [Type] - \item [NotArity] denotes the other cases. It may be inexact after - instanciation. For example [(X:Type)X] is [NotArity] and may give [Set] - after instanciation, which is rather [Arity] - \item [Logic] denotes identifiers of type an arity of sort [Prop], - or of type of type [Prop] + \item [TypeScheme] denotes a type scheme, that is + something that will become a type after enough applications. + More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with + [s = Set], [Prop] or [Type] + \item [Default] denotes the other cases. It may be inexact after + instanciation. For example [(X:Type)X] is [Default] and may give [Set] + after instanciation, which is rather [TypeScheme] + \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop] \item [Info] is the opposite. The same example [(X:Type)X] shows that an [Info] term might in fact be [Logic] later on. \end{itemize} *) type info = Logic | Info -type arity = Arity | Flexible | Default +type scheme = TypeScheme | Default -type flag = info * arity +type flag = info * scheme (* The [signature] type is used to know how many arguments a CIC object expects, and what these arguments will become in the ML @@ -62,32 +61,31 @@ type flag = info * arity type signature = bool list -(* The [indutive_extraction_result] is used to save the extraction of - an inductive type. It tells whether this inductive is informative - or not, and in the informative case, stores a signature and a type - variable list. *) +(* The [ind_extraction_result] is used to save the extraction of + an inductive type. In the informative case, it stores a signature + and a type variable list. *) -type inductive_extraction_result = - | Iml of signature * identifier list - | Iprop +type ind_extraction_result = signature * identifier list -(* For an informative constructor, the [constructor_extraction_result] - contains the list of the types of its arguments, a signature, and - the number of parameters to discard. *) +(* For an informative constructor, the [cons_extraction_result] + contains the list of the types of its arguments and the number of + parameters to discard. *) -type constructor_extraction_result = - | Cml of ml_type list * signature * int - | Cprop +type cons_extraction_result = ml_type list * int (*S Tables to keep the extraction results. *) +let visited_inductive = ref (Gset.empty : kernel_name Gset.t) +let visit_inductive k = visited_inductive := Gset.add k !visited_inductive +let already_visited_inductive k = Gset.mem k !visited_inductive + let inductive_table = - ref (Gmap.empty : (inductive, inductive_extraction_result) Gmap.t) + ref (Gmap.empty : (inductive, ind_extraction_result) Gmap.t) let add_inductive i e = inductive_table := Gmap.add i e !inductive_table let lookup_inductive i = Gmap.find i !inductive_table let constructor_table = - ref (Gmap.empty : (constructor, constructor_extraction_result) Gmap.t) + ref (Gmap.empty : (constructor, cons_extraction_result) Gmap.t) let add_constructor c e = constructor_table := Gmap.add c e !constructor_table let lookup_constructor c = Gmap.find c !constructor_table @@ -96,18 +94,21 @@ let constant_table = let add_constant kn d = constant_table := Gmap.add kn d !constant_table let lookup_constant kn = Gmap.find kn !constant_table -let signature_table = ref (Gmap.empty : (kernel_name, signature) Gmap.t) -let add_signature kn s = signature_table := Gmap.add kn s !signature_table -let lookup_signature kn = Gmap.find kn !signature_table +let mltype_table = + ref (Gmap.empty : (kernel_name, ml_schema) Gmap.t) +let add_mltype kn s = mltype_table := Gmap.add kn s !mltype_table +let lookup_mltype kn = Gmap.find kn !mltype_table (* Tables synchronization. *) let freeze () = - !inductive_table, !constructor_table, !constant_table, !signature_table + !visited_inductive, !inductive_table, + !constructor_table, !constant_table, !mltype_table -let unfreeze (it,cst,ct,st) = +let unfreeze (vi,it,cst,ct,st) = + visited_inductive := vi; inductive_table := it; constructor_table := cst; - constant_table := ct; signature_table := st + constant_table := ct; mltype_table := st let _ = declare_summary "Extraction tables" { freeze_function = freeze; @@ -143,6 +144,11 @@ let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) let is_axiom kn = (Global.lookup_constant kn).const_body = None +let break_prod env t = + match kind_of_term (whd_betadeltaiota env none t) with + | Prod (n,t1,t2) -> (t1,t2) + | _ -> anomaly ("Non-fonctional construction ") + (*s [flag_of_type] transforms a type [t] into a [flag]. Really important function. *) @@ -150,136 +156,150 @@ let rec flag_of_type env t = let t = whd_betadeltaiota env none t in match kind_of_term t with | Prod (x,t,c) -> flag_of_type (push_rel (x,None,t) env) c - | Sort (Prop Null) -> (Logic,Arity) - | Sort _ -> (Info,Arity) - | (Case _ | Fix _ | CoFix _) -> - if (sort_of env t) = InProp then (Logic,Flexible) else (Info,Default) + | Sort (Prop Null) -> (Logic,TypeScheme) + | Sort _ -> (Info,TypeScheme) | _ -> if (sort_of env t) = InProp then (Logic,Default) else (Info,Default) -(*s [is_default] and [is_info_arity] are particular cases of [flag_of_type]. *) +(*s [is_default] is a particular case of [flag_of_type]. *) let is_default env t = (flag_of_type env t = (Info, Default)) -let is_info_arity env t = (flag_of_type env t = (Info, Arity)) +let is_info_sort env t = + match kind_of_term (whd_betadeltaiota env none t) with + | Sort (Prop Null) -> false + | Sort _ -> true + | _ -> false -(*s [term_sign] gernerates a signature aimed at treating a term - application at the ML term level. *) +let is_info_type_scheme env t = (flag_of_type env t = (Info, TypeScheme)) -let rec term_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with - | Prod (n,t,d) -> - (is_default env t) :: (term_sign (push_rel_assum (n,t) env) d) - | _ -> [] +let is_type env t = isSort (whd_betadeltaiota env none (type_of env t)) -(*s [type_sign] gernerates a signature aimed at treating a term - application at the ML type level. *) - -let rec type_sign env c = - match kind_of_term (whd_betadeltaiota env none c) with - | Prod (n,t,d) -> - (is_info_arity env t)::(type_sign (push_rel_assum (n,t) env) d) - | _ -> [] - -(* There is also a variant producing at the same time a type var list. *) +(*s [type_sign_vl] gernerates a signature aimed at treating a term + application at the ML type level, and a type var list. *) let rec type_sign_vl env c = match kind_of_term (whd_betadeltaiota env none c) with | Prod (n,t,d) -> let s,vl = type_sign_vl (push_rel_assum (n,t) env) d in - if not (is_info_arity env t) then false::s, vl + if not (is_info_type_scheme env t) then false::s, vl else true::s, (next_ident_away (id_of_name n) vl) :: vl | _ -> [],[] -(*s Function recording signatures of section paths. *) - -let signature_of_kn kn = - try lookup_signature kn - with Not_found -> - let env = Global.env () in - let s = term_sign env (constant_type env kn) - in add_signature kn s; s +let rec type_sign env c = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + (is_info_type_scheme env t)::(type_sign (push_rel_assum (n,t) env) d) + | _ -> [] (*S Management of type variable contexts. *) -(*s From a signature toward a type variable context (db). *) +(*s From a type signature toward a type variable context (db). *) let db_from_sign s = - let rec f i = function - | [] -> [] - | true :: l -> i :: (f (i+1) l) - | false :: l -> 0 :: (f i l) - in f 1 (List.rev s) + let rec make i acc = function + | [] -> acc + | true :: l -> make (i+1) (i::acc) l + | false :: l -> make i (0::acc) l + in make 1 [] s (*s Create a type variable context from indications taken from an inductive type (see just below). *) -let db_from_ind dbmap params_nb length_sign = - let rec f i = - if i > params_nb then [] - else try - Intmap.find (i+length_sign) dbmap :: (f (i+1)) - with Not_found -> 0 :: (f (i+1)) - in f 1 +let rec db_from_ind dbmap i = + if i = 0 then [] + else (try Intmap.find i dbmap with Not_found -> 0)::(db_from_ind dbmap (i-1)) + +(*s [parse_ind_args] builds a map: [i->j] iff the i-th Coq argument + of a constructor corresponds to the j-th type var of the ML inductive. *) -(*s [parse_ind_args] is the function used for generating ad-hoc - translation of de Bruijn indices for extraction of inductive type. *) +(* \begin{itemize} + \item [si] : signature of the inductive + \item [i] : counter of Coq args for [(I args)] + \item [j] : counter of ML type vars + \item [relmax] : total args number of the constructor + \end{itemize} *) -let parse_ind_args si args = - let rec parse i k = function +let parse_ind_args si args relmax = + let rec parse i j = function | [] -> Intmap.empty - | false :: s -> parse (i-1) k s + | false :: s -> parse (i+1) j s | true :: s -> - (match kind_of_term args.(i) with - | Rel j -> Intmap.add j k (parse (i-1) (k+1) s) - | _ -> parse (i-1) (k+1) s) - in parse ((Array.length args)-1) 1 (List.rev si) + (match kind_of_term args.(i-1) with + | Rel k -> Intmap.add (relmax+1-k) j (parse (i+1) (j+1) s) + | _ -> parse (i+1) (j+1) s) + in parse 1 1 si (*S Extraction of a type. *) -(*s [extract_type env db c args] is used to produce an ML type from the +(* [extract_type env db c args] is used to produce an ML type from the coq term [(c args)], which is supposed to be a Coq type. *) (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) -let rec extract_type env db c args = +(* [j] stands for the next ML type var. [j=0] means we do not + generate ML type var anymore (in subterms for example). *) + +let rec extract_type env db j c args = match kind_of_term (whd_betaiotazeta c) with + | Var _ -> section_message () + | App (d, args') -> + (* We just accumulate the arguments. *) + extract_type env db j d (Array.to_list args' @ args) | Lambda (_,_,d) -> (match args with | [] -> assert false (* otherwise the lambda would be reductible. *) - | a :: args -> extract_type env db (subst1 a d) args) + | a :: args -> extract_type env db j (subst1 a d) args) | Prod (n,t,d) -> - let mld = extract_type (push_rel_assum (n,t) env) (0::db) d [] in - if mld = Tdummy then Tdummy - else if not (is_default env t) then Tarr (Tdummy, mld) - else Tarr (extract_type env db t [], mld) - | App (d, args') -> - (* We just accumulate the arguments. *) - extract_type env db d (Array.to_list args' @ args) + assert (args = []); + let env' = push_rel_assum (n,t) env in + if j > 0 && is_info_type_scheme env t then + let mld = extract_type env' (j::db) (j+1) d [] in + if mld = Tdummy then Tdummy + else Tarr (Tdummy, mld) + else + let mld = extract_type env' (0::db) j d [] in + if mld = Tdummy then Tdummy + else if not (is_default env t) then Tarr (Tdummy, mld) + else Tarr (extract_type env db 0 t [], mld) + | Sort _ -> Tdummy + | _ when sort_of env (applist (c, args)) = InProp -> Tdummy | Rel n -> (match lookup_rel n env with - | (_,Some t,_) -> - extract_type env db (lift n t) args + | (_,Some t,_) -> extract_type env db j (lift n t) args | _ -> - let n' = List.nth db (n-1) in + if n > List.length db then Tunknown + else let n' = List.nth db (n-1) in if n' = 0 then Tunknown else Tvar n') - | Const kn -> - let t = constant_type env kn in - (match flag_of_type env t with - | (Info,Arity) -> - extract_type_app env db (ConstRef kn, type_sign env t) args - | (Info,_) -> Tunknown - | (Logic,_) -> Tdummy) + | Const sp when is_ml_extraction (ConstRef sp) -> Tglob (ConstRef sp,[]) + | Const sp when is_axiom sp -> Tunknown + | Const sp -> + let body = constant_value env sp in + let mlt1 = extract_type env db j (applist (body, args)) [] in + (match mlt_env (ConstRef sp) with + | Some mlt -> + if mlt = Tdummy then Tdummy + else + let s = type_sign env (constant_type env sp) in + let mlt2 = extract_type_app env db (ConstRef sp,s) args in + if type_eq mlt_env mlt1 mlt2 then mlt2 else mlt1 + | None -> mlt1) | Ind kni -> - (match extract_inductive kni with - | Iml (si,_) -> extract_type_app env db (IndRef kni,si) args - | Iprop -> Tdummy) - | Sort _ -> Tdummy + let si = fst (extract_inductive kni) in + extract_type_app env db (IndRef kni,si) args | Case _ | Fix _ | CoFix _ -> Tunknown - | Var _ -> section_message () | _ -> assert false +(* [extract_maybe_type] calls [extract_type] when used on a Coq type, + and otherwise returns [Tdummy] or [Tunknown] *) + +and extract_maybe_type env db c = + let t = type_of env c in + if isSort (whd_betadeltaiota env none t) + then extract_type env db 0 c [] + else if sort_of env t = InProp then Tdummy else Tunknown + (*s Auxiliary function dealing with type application. - Precondition: [r] is of type an arity represented by the signature [s], + Precondition: [r] is a type scheme represented by the signature [s], and is completely applied: [List.length args = List.length s]. *) and extract_type_app env db (r,s) args = @@ -287,130 +307,166 @@ and extract_type_app env db (r,s) args = List.fold_right (fun (b,c) a -> if b then let p = List.length (fst (splay_prod env none (type_of env c))) in - let db = iterate (fun l -> 0 :: l) p db in - (extract_type_arity env db c p) :: a + let db = iterate (fun l -> 0 :: l) p db in + (extract_type_scheme env db c p) :: a else a) (List.combine s args) [] in Tglob (r, ml_args) -(*s [extract_type_arity env db c p] works on a Coq term [c] whose - type is an arity. It means that [c] is not a Coq type, but will +(*S Extraction of a type scheme. *) + +(* [extract_type_scheme env db c p] works on a Coq term [c] which is + an informative type scheme. It means that [c] is not a Coq type, but will be when applied to sufficiently many arguments ([p] in fact). This function decomposes p lambdas, with eta-expansion if needed. *) (* [db] is a context for translating Coq [Rel] into ML type [Tvar]. *) -and extract_type_arity env db c p = - if p=0 then extract_type env db c [] +and extract_type_scheme env db c p = + if p=0 then extract_type env db 0 c [] else let c = whd_betaiotazeta c in match kind_of_term c with | Lambda (n,t,d) -> - extract_type_arity (push_rel_assum (n,t) env) db d (p-1) + extract_type_scheme (push_rel_assum (n,t) env) db d (p-1) | _ -> - let rels = fst (splay_prod env none (type_of env c)) in - let env = push_rels_assum rels env in - let eta_args = List.rev_map mkRel (interval 1 p) in - extract_type env db (lift p c) eta_args + let rels = fst (splay_prod env none (type_of env c)) in + let env = push_rels_assum rels env in + let eta_args = List.rev_map mkRel (interval 1 p) in + extract_type env db 0 (lift p c) eta_args -(*s [extract_type_ind] extracts the type of an inductive - constructor toward the corresponding list of ML types. *) -(* [p] is the number of product in [c] and [db] is a context for - translating Coq [Rel] into ML type [Tvar] and [dbmap] is a translation - map (produced by a call to [parse_in_args]). *) +(*S Extraction of an inductive type. *) -and extract_type_ind env db dbmap c p = - match kind_of_term (whd_betadeltaiota env none c) with - | Prod (n,t,d) -> - let env' = push_rel_assum (n,t) env in - let db' = (try Intmap.find p dbmap with Not_found -> 0) :: db in - let l = extract_type_ind env' db' dbmap d (p-1) in - if is_default env t then - let mlt = extract_type env db t [] in - if mlt = Tdummy then l else mlt :: l - else l - | _ -> [] +(* [extract_inductive] answers a [ind_extraction_result] in + case of an informative inductive, and raises [Not_found] otherwise *) -(*S Extraction of an inductive. *) - -and extract_inductive ((sp,_) as i) = - extract_mib sp; +and extract_inductive ((kn,_) as i) = + if not (already_visited_inductive kn) then extract_mib kn; lookup_inductive i -and extract_constructor (((sp,_),_) as c) = - extract_mib sp; +(* [extract_constructor] answers a [cons_extraction_result] in + case of an informative constructor, and raises [Not_found] otherwise *) + +and extract_constructor (((kn,_),_) as c) = + if not (already_visited_inductive kn) then extract_mib kn; lookup_constructor c +(* The real job: *) + and extract_mib kn = - let ind = (kn,0) in - if not (Gmap.mem ind !inductive_table) then begin - let (mib,mip) = Global.lookup_inductive ind in + visit_inductive kn; + let env = Global.env () in + let (mib,mip) = Global.lookup_inductive (kn,0) in + (* Everything concerning parameters. *) + (* We do that first, since they are common to all the [mib]. *) + let params_nb = mip.mind_nparams in + let params_env = push_rel_context mip.mind_params_ctxt env in + (* First pass: we store inductive signatures together with *) + (* their type var list. *) + for i = 0 to mib.mind_ntypes - 1 do + let mip = snd (Global.lookup_inductive (kn,i)) in + if mip.mind_sort <> (Prop Null) then + add_inductive (kn,i) (type_sign_vl env mip.mind_nf_arity) + done; + (* Second pass: we extract constructors *) + for i = 0 to mib.mind_ntypes - 1 do + let ip = (kn,i) in + let mip = snd (Global.lookup_inductive ip) in + if mip.mind_sort <> (Prop Null) then + let s = fst (lookup_inductive ip) in + let types = arities_of_constructors env ip in + for j = 0 to Array.length types - 1 do + let t = snd (decompose_prod_n params_nb types.(j)) in + let args = match kind_of_term (snd (decompose_prod t)) with + | App (f,args) -> args (* [kind_of_term f = Ind ip] *) + | _ -> [||] + in + let dbmap = parse_ind_args s args (nb_prod t + params_nb) in + let db = db_from_ind dbmap params_nb in + let l = extract_type_cons params_env db dbmap t (params_nb+1) in + add_constructor (ip,j+1) (l,params_nb) + done + done + +(*s [extract_type_cons] extracts the type of an inductive + constructor toward the corresponding list of ML types. *) + +(* \begin{itemize} + \item [db] is a context for translating Coq [Rel] into ML type [Tvar] + \item [dbmap] is a translation map (produced by a call to [parse_in_args]) + \item [i] is the rank of the current product (initially [params_nb+1]) + \end{itemize} *) + +and extract_type_cons env db dbmap c i = + match kind_of_term (whd_betadeltaiota env none c) with + | Prod (n,t,d) -> + let env' = push_rel_assum (n,t) env in + let db' = (try Intmap.find i dbmap with Not_found -> 0) :: db in + let l = extract_type_cons env' db' dbmap d (i+1) in + (extract_type env db 0 t []) :: l + | _ -> [] + +(*s Recording the ML type abbreviation of a Coq type scheme constant. *) + +and mlt_env r = match r with + | ConstRef kn -> + (try match lookup_constant kn with + | Dtype (_,vl,mlt) -> Some mlt + | _ -> None + with Not_found -> + let env = Global.env() in + let cb = Global.lookup_constant kn in + let typ = cb.const_type in + match cb.const_body with + | None -> None + | Some l_body -> + (match flag_of_type env typ with + | Info,TypeScheme -> + let body = Declarations.force l_body in + let s,vl = type_sign_vl env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db body (List.length s) + in add_constant kn (Dtype (r, vl, t)); Some t + | _ -> None)) + | _ -> None + +let type_expand = type_expand mlt_env +let type_neq = type_neq mlt_env +let type_to_sign = type_to_sign mlt_env +let type_expunge = type_expunge mlt_env + +(*s Extraction of the type of a constant. *) + +let record_constant_type kn = + try lookup_mltype kn + with Not_found -> let env = Global.env () in - (* Everything concerning parameters. *) - (* We do that first, since they are common to all the [mib]. *) - let params_nb = mip.mind_nparams in - let params_env = push_rel_context mip.mind_params_ctxt env in - (* First pass: we store inductive signatures together with *) - (* their type var list. *) - for i = 0 to mib.mind_ntypes - 1 do - let ip = (kn,i) in - let (mib,mip) = Global.lookup_inductive ip in - if mip.mind_sort = (Prop Null) then - add_inductive ip Iprop - else - let arity = mip.mind_nf_arity in - let s,vl = type_sign_vl env arity in - add_inductive ip (Iml (s,vl)) - done; - (* Second pass: we extract constructors *) - for i = 0 to mib.mind_ntypes - 1 do - let ip = (kn,i) in - let (mib,mip) = Global.lookup_inductive ip in - match lookup_inductive ip with - | Iprop -> - for j = 1 to Array.length mip.mind_consnames do - add_constructor (ip,j) Cprop - done - | Iml (si,_) -> - for j = 1 to Array.length mip.mind_consnames do - let cp = (ip,j) in - let t = type_of_constructor env cp in - let t = snd (decompose_prod_n params_nb t) in - let s = term_sign params_env t in - let n = List.length s in - let args = match find_conclusion params_env none t with - | App (f,args) -> args (* [kind_of_term f = Ind ip] *) - | _ -> [||] - in - let dbmap = parse_ind_args si args in - let db = db_from_ind dbmap params_nb n in - let l = extract_type_ind params_env db dbmap t n in - add_constructor cp (Cml (l,s,params_nb)) - done - done - end + let mlt = extract_type env [] 1 (constant_type env kn) [] in + let schema = (type_maxvar mlt, mlt) + in add_mltype kn schema; schema (*s Looking for informative singleton case, i.e. an inductive with one constructor which has one informative argument. This dummy case will be simplified. *) - -let is_singleton_inductive ind = - let (mib,mip) = Global.lookup_inductive ind in + +let is_singleton_inductive ip = + let (mib,mip) = Global.lookup_inductive ip in mib.mind_finite && (mib.mind_ntypes = 1) && (Array.length mip.mind_consnames = 1) && - match extract_constructor (ind,1) with - | Cml ([mlt],_,_)-> not (type_mem_kn (fst ind) mlt) - | _ -> false + try + let l = List.filter (type_neq Tdummy) (fst (extract_constructor (ip,1))) in + List.length l = 1 && not (type_mem_kn (fst ip) (List.hd l)) + with Not_found -> false let is_singleton_constructor ((kn,i),_) = is_singleton_inductive (kn,i) (*S Modification of the signature of terms. *) -(* We sometimes want to suppress [prop] and [arity] in the signature - of a term. It is so: +(* We sometimes want to suppress [Logic] and [TypeScheme] parts + in the signature of a term. It is so: \begin{itemize} \item after a case, in [extract_case] \item for the toplevel definition of a function, in [suppress_prop_eta] @@ -418,16 +474,16 @@ let is_singleton_constructor ((kn,i),_) = [expansion_prop_eta]. \end{itemize} To ensure correction of execution, we then need to reintroduce - [prop] and [arity] lambdas around constructors and functions occurrences. + dummy lambdas around constructors and functions occurrences. This is done by [abstract_constructor] and [abstract_constant]. *) let expansion_prop_eta s (ids,c) = let rec abs ids rels i = function | [] -> let a = List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels - in ids, MLapp (ml_lift (i-1) c, a) + in ids, MLapp (ast_lift (i-1) c, a) | true :: l -> abs (anonymous :: ids) (MLrel i :: rels) (i+1) l - | false :: l -> abs (dummy_name :: ids) (MLdummy' :: rels) (i+1) l + | false :: l -> abs (dummy_name :: ids) (MLdummy :: rels) (i+1) l in abs ids [] 1 s let kill_all_prop_lams_eta e s = @@ -437,222 +493,247 @@ let kill_all_prop_lams_eta e s = else expansion_prop_eta (snd (list_chop n s)) (collect_lams e) in kill_some_lams (List.rev s) p -let kill_prop_lams_eta e s = - if s = [] then e +let kill_prop_lams_eta s (ids,c) = + if s = [] then c else - let ids,e = kill_all_prop_lams_eta e s in - if ids = [] then MLlam (dummy_name, ml_lift 1 e) - else named_lams ids e + let ids,c = kill_some_lams (List.rev s) (ids,c) in + if ids = [] then MLlam (dummy_name, ast_lift 1 c) + else named_lams ids c -(*s Auxiliary functions for [apply_constant] and [apply_constructor]. *) - -let rec anonym_or_dummy_lams c = function - | [] -> c - | true :: l -> MLlam(anonymous, anonym_or_dummy_lams c l) - | false :: l -> MLlam(dummy_name, anonym_or_dummy_lams c l) - -let rec extract_eta_args n = function - | [] -> [] - | true :: s -> (MLrel n) :: (extract_eta_args (n-1) s) - | false :: s -> extract_eta_args (n-1) s - -let rec extract_real_args env args s = - let a = Array.length args in - let rec f i l = function - | [] -> l - | true :: s -> f (i-1) ((extract_constr_to_term env args.(i)) :: l) s - | false :: s -> f (i-1) l s - in f (a-1) [] (List.rev s) - -(*s Abstraction of an constant. *) - -and apply_constant env kn args = - let head = MLglob (ConstRef kn) in - let s = signature_of_kn kn in - let ls = List.length s in - let la = Array.length args in - if ls = 0 then begin - (* if the type of this constant isn't a product, it cannot be applied. *) - assert (la = 0); - head - end else if List.mem true s then - if la = ls then - MLapp (head, extract_real_args env args s) - else if la > ls then - let s' = s @ (iterate (fun l -> true :: l) (la-ls) []) in - MLapp (head, extract_real_args env args s') - else (* [la < ls] *) - let n1 = la - and n2 = ls-la in - let s1,s2 = list_chop n1 s in - let mla1 = List.map (ml_lift n2) (extract_real_args env args s1) in - let mla2 = extract_eta_args n2 s2 in - anonym_or_dummy_lams (MLapp (head, mla1 @ mla2)) s2 - else - if la >= ls then - let s' = iterate (fun l -> true :: l) (la-ls) [] in - MLapp(head, MLdummy' :: (extract_real_args env args s')) - else (* [la < ls] *) - dummy_lams head (ls-la-1) - -(*s Application of an inductive constructor. - \begin{itemize} - \item In ML, contructor arguments are uncurryfied. - \item We managed to suppress logical parts inside inductive definitions, - but they must appears outside (for partial applications for instance) - \item We also suppressed all Coq parameters to the inductives, since - they are fixed, and thus are not used for the computation. - \end{itemize} *) - -and apply_constructor env cp args = - let head mla = - if is_singleton_constructor cp then - List.hd mla (* assert (List.length mla = 1) *) - else MLcons (ConstructRef cp, mla) - in - match extract_constructor cp with - | Cprop -> assert false - | Cml (_,s,params_nb) -> - let ls = List.length s in - let la = Array.length args in - assert (la <= ls + params_nb); - if la = ls + params_nb then - head (extract_real_args env args s) - else if la >= params_nb then - let n1 = la - params_nb in - let n2 = ls - n1 in - let s1,s2 = list_chop n1 s in - let mla1 = List.map (ml_lift n2) (extract_real_args env args s1) in - let mla2 = extract_eta_args n2 s2 in - anonym_or_dummy_lams (head (mla1 @ mla2)) s2 - else (* [la < params_nb] *) - let head' = head (extract_eta_args ls s) in - dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la) - (*S Extraction of a term. *) -(* Precondition: [c] has a type which is not an arity, and is informative. - This is normaly checked in [extract_constr]. *) +(* Precondition: [c] is not a type scheme, and is informative. *) -and extract_term env c = +let rec extract_term env mle mlt c args = match kind_of_term c with + | App (f,a) -> + extract_term env mle mlt f (Array.to_list a @ args) | Lambda (n, t, d) -> let id = id_of_name n in - (* If [d] was of type an arity, [c] too would be so *) - let d' = extract_term (push_rel_assum (Name id,t) env) d in - if is_default env t then MLlam (id, d') - else MLlam (dummy_name, d') + (match args with + | a :: l -> + let d' = mkLetIn (Name id,a,t,applistc d (List.map (lift 1) l)) + in extract_term env mle mlt d' [] + | [] -> + let env' = push_rel_assum (Name id, t) env in + let id, a = + if is_default env t + then id, new_meta () + else dummy_name, Tdummy in + let b = new_meta () in + let magic = needs_magic (mlt, Tarr (a, b)) in + let d' = extract_term env' (Mlenv.push_type mle a) b d [] in + put_magic_if magic (MLlam (id, d'))) | LetIn (n, c1, t1, c2) -> let id = id_of_name n in - (* If [c2] was of type an arity, [c] too would be so *) - let c2' = extract_term (push_rel (Name id,Some c1,t1) env) c2 in - if is_default env t1 then MLletin (id, extract_term env c1, c2') - else ml_pop c2' - | Rel n -> - MLrel n - | App (f,a) -> - (match kind_of_term (strip_outer_cast f) with - | App _ -> assert false - | Const kn -> apply_constant env kn a - | Construct cp -> apply_constructor env cp a - | _ -> - let mlargs = - Array.fold_right - (fun a l -> (extract_constr_to_term env a) :: l) a [] - in MLapp (extract_term env f, mlargs)) + let env' = push_rel (Name id, Some c1, t1) env in + let args' = List.map (lift 1) args in + if is_default env t1 then + let a = new_meta () in + let c1' = extract_term env mle a c1 [] in + let mle' = Mlenv.push_gen mle a in + MLletin (id, c1', extract_term env' mle' mlt c2 args') + else + let mle' = Mlenv.push_std_type mle Tdummy in + ast_pop (extract_term env' mle' mlt c2 args') | Const kn -> - apply_constant env kn [||] + extract_cst_app env mle mlt kn args | Construct cp -> - apply_constructor env cp [||] - | Case ({ci_ind=ip},_,c,br) -> - extract_case env ip c br - | Fix ((_,i),recd) -> - extract_fix env i recd - | CoFix (i,recd) -> - extract_fix env i recd - | Cast (c, _) -> - extract_term env c + extract_cons_app env mle mlt cp args + | Rel n -> + let extract_rel mlt = put_magic (mlt, Mlenv.get mle n) (MLrel n) + in extract_app env mle mlt extract_rel args + | Case ({ci_ind=ip},_,c0,br) -> + extract_app env mle mlt (extract_case env mle (ip,c0,br)) args + | Fix ((_,i),recd) -> + extract_app env mle mlt (extract_fix env mle i recd) args + | CoFix (i,recd) -> + extract_app env mle mlt (extract_fix env mle i recd) args + | Cast (c, _) -> extract_term env mle mlt c args | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false | Var _ -> section_message () +(*s [extract_maybe_term] is [extract_term] for usual terms, else [MLdummy] *) + +and extract_maybe_term env mle mlt c = + if is_default env (type_of env c) then extract_term env mle mlt c [] + else put_magic (mlt, Tdummy) MLdummy + +(*s Generic way to deal with an application. *) + +and extract_app env mle mlt mk_head args = + let metas = List.map new_meta args in + let type_head = type_recomp (metas, mlt) in + let mlargs = List.map2 (extract_maybe_term env mle) metas args in + if mlargs = [] then mk_head type_head else MLapp (mk_head type_head, mlargs) + +(*s Extraction of a constant applied to arguments. *) + +and make_mlargs env mle s args mlts = + let rec f = function + | _, [], [] -> [] + | [], a::args, mlt::mlts -> + (extract_maybe_term env mle mlt a) :: (f ([],args,mlts)) + | true::s, a::args, mlt::mlts -> + (extract_maybe_term env mle mlt a) :: (f (s,args,mlts)) + | false::s, _::args, _::mlts -> f (s,args,mlts) + | _ -> assert false + in f (s,args,mlts) + +and extract_cst_app env mle mlt kn args = + let nb,t = record_constant_type kn in + let schema = nb, type_expand t in + let metas = List.map new_meta args in + let type_head = type_recomp (metas,mlt) in + let head = + let h = MLglob (ConstRef kn) in + put_magic (type_head, instantiation schema) h in + let s = type_to_sign (snd schema) in + let ls = List.length s in + let la = List.length args in + let mla = make_mlargs env mle s args metas in + if ls = 0 then head + else if List.mem true s then + if la >= ls then MLapp (head, mla) + else + let ls' = ls-la in + let s' = list_lastn ls' s in + let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in + anonym_or_dummy_lams (MLapp (head, mla)) s' + else + if la >= ls then MLapp (head, MLdummy :: mla) + else dummy_lams head (ls-la-1) + +(*s Extraction of an inductive constructor applied to arguments. *) -(*s Extraction of a case. *) - -and extract_case env ip c br = - let ni = mis_constr_nargs ip in - (* [ni]: number of arguments without parameters in each branch *) - (* [br]: bodies of each branch (in functional form) *) - let extract_branch j b = - (* Some pathological cases need an [extract_constr] here rather *) - (* than an [extract_term]. See exemples in [test_extraction.v] *) - let e = extract_constr_to_term env b in - let cp = (ip,succ j) in - let s = match extract_constructor cp with - | Cml (_,s,_) -> s - | _ -> assert false - in assert (List.length s = ni.(j)); - let ids,e = kill_all_prop_lams_eta e s in - (ConstructRef cp, List.rev ids, e) - in - if br = [||] then MLexn "absurd case" +(* \begin{itemize} + \item In ML, contructor arguments are uncurryfied. + \item We managed to suppress logical parts inside inductive definitions, + but they must appears outside (for partial applications for instance) + \item We also suppressed all Coq parameters to the inductives, since + they are fixed, and thus are not used for the computation. + \end{itemize} *) + +and extract_cons_app env mle mlt ((ip,_) as cp) args = + let types, params_nb = extract_constructor cp in + let types = List.map type_expand types in + let nb_tvar = List.length (snd (extract_inductive ip)) in + let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in + let type_cons = type_recomp (types, Tglob (IndRef ip, list_tvar)) in + let type_cons = instantiation (nb_tvar, type_cons) in + let s = List.map ((<>) Tdummy) types in + let ls = List.length s in + let la = List.length args in + assert (la <= ls + params_nb); + let la' = max 0 (la - params_nb) in + let args' = list_lastn la' args in + let metas = List.map new_meta args' in + let type_head = type_recomp (metas, mlt) in + let magic = needs_magic (type_cons, type_head) in + let head mla = + if is_singleton_constructor cp then + put_magic_if magic (List.hd mla) (* assert (List.length mla = 1) *) + else put_magic_if magic (MLcons (ConstructRef cp, mla)) + in + if la < params_nb then + let head' = head (eta_args_sign ls s) in + dummy_lams (anonym_or_dummy_lams head' s) (params_nb - la) + else + let mla = make_mlargs env mle s args' metas in + if la = ls + params_nb then head mla + else (* [ params_nb <= la <= ls + params_nb ] *) + let ls' = params_nb + ls - la in + let s' = list_lastn ls' s in + let mla = (List.map (ast_lift ls') mla) @ (eta_args_sign ls' s') in + anonym_or_dummy_lams (head mla) s' + +(*S Extraction of a case. *) + +and extract_case env mle (ip,c,br_vect) mlt = + (* [ni_vect]: number of arguments without parameters in each branch *) + (* [br_vect]: bodies of each branch (in functional form) *) + let ni_vect = mis_constr_nargs ip in + let br_size = Array.length br_vect in + assert (Array.length ni_vect = br_size); + if br_size = 0 then MLexn "absurd case" else - (* [c] has an inductive type, not an arity type. *) + (* [c] has an inductive type, and is not a type scheme type. *) let t = type_of env c in (* The only non-informative case: [c] is of sort [Prop] *) if (sort_of env t) = InProp then begin (* Logical singleton case: *) (* [match c with C i j k -> t] becomes [t'] *) - assert (Array.length br = 1); - let e = extract_constr_to_term env br.(0) in - let s = iterate (fun l -> false :: l) ni.(0) [] in + assert (br_size = 1); + let s = iterate (fun l -> false :: l) ni_vect.(0) [] in + let mlt = iterate (fun t -> Tarr (Tdummy, t)) ni_vect.(0) mlt in + let e = extract_maybe_term env mle mlt br_vect.(0) in snd (kill_all_prop_lams_eta e s) end else - let a = extract_term env c in + let types_vect = Array.make br_size [] + and sign_vect = Array.make br_size [] in + for i = 0 to br_size-1 do + let l = List.map type_expand (fst (extract_constructor (ip,i+1))) in + types_vect.(i) <- l; + sign_vect.(i) <- List.map ((<>) Tdummy) l; + assert (List.length sign_vect.(i) = ni_vect.(i)) + done; + let big_schema = + let nb_tvar = List.length (snd (extract_inductive ip)) in + let list_tvar = List.map (fun i -> Tvar i) (interval 1 nb_tvar) in + let l = array_map_to_list (fun l -> type_recomp (l,mlt)) types_vect in + nb_tvar, type_recomp (l, Tglob (IndRef ip, list_tvar)) + in + let type_list, type_head = type_decomp (instantiation big_schema) in + let type_vect = Array.of_list type_list in + let a = extract_term env mle type_head c [] in + let extract_branch i = + let e = extract_maybe_term env mle type_vect.(i) br_vect.(i) in + let ids,e = kill_all_prop_lams_eta e sign_vect.(i) in + (ConstructRef (ip,i+1), List.rev ids, e) + in if is_singleton_inductive ip then begin (* Informative singleton case: *) (* [match c with C i -> t] becomes [let i = c' in t'] *) - assert (Array.length br = 1); - let (_,ids,e') = extract_branch 0 br.(0) in + assert (br_size = 1); + let (_,ids,e') = extract_branch 0 in assert (List.length ids = 1); MLletin (List.hd ids,a,e') end else (* Standard case: we apply [extract_branch]. *) - MLcase (a, Array.mapi extract_branch br) + MLcase (a, Array.init br_size extract_branch) (*s Extraction of a (co)-fixpoint. *) -and extract_fix env i (fi,ti,ci as recd) = - let n = Array.length ti in - let ti' = Array.mapi lift ti in - let lb = Array.to_list (array_map2 (fun a b -> (a,b)) fi ti') in - let env' = push_rels_assum (List.rev lb) env in - let extract_fix_body c t = - extract_constr_to_term_wt env' c (lift n t) in - let ei = array_map2 extract_fix_body ci ti in - MLfix (i, Array.map id_of_name fi, ei) - -(*s Extraction of a constr seen as a term. *) - -and extract_constr_to_term env c = - extract_constr_to_term_wt env c (type_of env c) - -(* Same, but With Type (wt). *) - -and extract_constr_to_term_wt env c t = - match flag_of_type env t with - | (Info, Default) -> extract_term env c - | (Logic, Flexible) -> MLdummy' - | _ -> MLdummy' -(*i dummy_lams MLdummy (List.length (fst (splay_prod env none t))) i*) +and extract_fix env mle i (fi,ti,ci as recd) mlt = + let n = Array.length fi in + let env = push_rec_types recd env in + let metas = Array.map (fun _ -> new_meta ()) fi in + let magic = needs_magic (mlt, metas.(i)) in + let mle = Array.fold_left Mlenv.push_type mle metas in + let ei = array_map2 (extract_maybe_term env mle) metas ci in + put_magic_if magic (MLfix (i, Array.map id_of_name fi, ei)) (*S ML declarations. *) (*s From a constant to a ML declaration. *) +let rec decomp_n_lams_eta env typ c = + let rels = fst (splay_prod env none typ) in + let n = List.length rels in + let m = nb_lam c in + if m >= n then decompose_lam_n n c + else + let rels',c = decompose_lam c in + let d = n - m in + (* we'd better keep rels' as long as possible. *) + let rels = (list_firstn d rels) @ rels' in + let eta_args = List.rev_map mkRel (interval 1 d) in + rels, applist (lift d c,eta_args) + let extract_constant kn r = let env = Global.env() in let cb = Global.lookup_constant kn in @@ -661,27 +742,36 @@ let extract_constant kn r = | None -> (* A logical axiom is risky, an informative one is fatal. *) (match flag_of_type env typ with | (Info,_) -> axiom_error_message kn - | (Logic,Arity) -> axiom_warning_message kn; - DdummyType r - | (Logic,_) -> axiom_warning_message kn; - Dterm (r, MLdummy')) + | (Logic,TypeScheme) -> + axiom_warning_message kn; + Dtype (r, [], Tdummy) + | (Logic,Default) -> + axiom_warning_message kn; + Dterm (r, MLdummy, Tdummy)) | Some l_body -> (match flag_of_type env typ with - | (Logic, Arity) -> DdummyType r - | (Info, Arity) -> - let s,vl = type_sign_vl env typ in - let db = db_from_sign s in + | (Logic, Default) -> Dterm (r, MLdummy, Tdummy) + | (Logic, TypeScheme) -> Dtype (r, [], Tdummy) + | (Info, Default) -> let body = Declarations.force l_body in - let t = extract_type_arity env db body (List.length s) - in Dtype (r, vl, t) - | (Logic, _) -> Dterm (r, MLdummy') - | (Info, _) -> + let rels,c = decomp_n_lams_eta env typ body in + let env' = push_rels_assum rels env in + let ids = List.map (fun (n,_) -> id_of_name n) rels in + reset_meta_count (); + let t = snd (record_constant_type kn) in + let l,t' = type_decomp (type_expand (var2var' t)) in + let s = List.map ((<>) Tdummy) l in + let mle = List.fold_left Mlenv.push_std_type Mlenv.empty l in + let e = extract_term env' mle t' c [] in + if e = MLdummy then Dterm (r, MLdummy, Tdummy) + else Dterm (r, kill_prop_lams_eta s (ids,e), type_expunge t) + | (Info, TypeScheme) -> let body = Declarations.force l_body in - let a = extract_term env body in - if a <> MLdummy' then - Dterm (r, kill_prop_lams_eta a (signature_of_kn kn)) - else Dterm (r, a)) - + let s,vl = type_sign_vl env typ in + let db = db_from_sign s in + let t = extract_type_scheme env db body (List.length s) in + Dtype (r, vl, t)) + let extract_constant_cache kn r = try lookup_constant kn with Not_found -> @@ -689,19 +779,14 @@ let extract_constant_cache kn r = in add_constant kn d; d (*s From an inductive to a ML declaration. *) - + let extract_inductive_declaration kn = - extract_mib kn; + if not (already_visited_inductive kn) then extract_mib kn; let ip = (kn,0) in if is_singleton_inductive ip then - let t = match lookup_constructor (ip,1) with - | Cml ([t],_,_)-> t - | _ -> assert false - in - let vl = match lookup_inductive ip with - | Iml (_,vl) -> vl - | _ -> assert false - in + let t = + List.hd (List.filter (type_neq Tdummy) (fst (lookup_constructor (ip,1)))) + and vl = snd (lookup_inductive ip) in Dtype (IndRef ip,vl,t) else let mib = Global.lookup_mind kn in @@ -709,18 +794,18 @@ let extract_inductive_declaration kn = iterate_for (-n) (-1) (fun j l -> let cp = (ip,-j) in - match lookup_constructor cp with - | Cml (t,_,_) -> (ConstructRef cp, t)::l - | _ -> assert false) [] + let mlt = fst (lookup_constructor cp) in + (ConstructRef cp, List.filter (type_neq Tdummy) mlt)::l) [] in let l = iterate_for (1 - mib.mind_ntypes) 0 (fun i acc -> let ip = (kn,-i) in let nc = Array.length mib.mind_packets.(-i).mind_consnames in - match lookup_inductive ip with - | Iprop -> acc - | Iml (_,vl) -> (vl, IndRef ip, one_ind ip nc) :: acc) + try + let vl = snd (lookup_inductive ip) in + (vl, IndRef ip, one_ind ip nc) :: acc + with Not_found -> acc) [] in Dind (l, not mib.mind_finite) @@ -728,7 +813,7 @@ let extract_inductive_declaration kn = (*s From a global reference to a ML declaration. *) let extract_declaration r = match r with - | ConstRef kn -> extract_constant kn r + | ConstRef kn -> extract_constant_cache kn r | IndRef (kn,_) -> extract_inductive_declaration kn | ConstructRef ((kn,_),_) -> extract_inductive_declaration kn | VarRef _ -> assert false @@ -736,8 +821,9 @@ let extract_declaration r = match r with (*s Check if a global reference corresponds to a logical inductive. *) let decl_is_logical_ind = function - | IndRef ip -> extract_inductive ip = Iprop - | ConstructRef cp -> extract_constructor cp = Cprop + | IndRef ip -> (try ignore (extract_inductive ip); false with _ -> true) + | ConstructRef cp -> + (try ignore (extract_constructor cp); false with _ -> true) | _ -> false (*s Check if a global reference corresponds to the constructor of @@ -747,3 +833,4 @@ let decl_is_singleton = function | ConstructRef cp -> is_singleton_constructor cp | _ -> false + diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 286747c6f..9b3304602 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -31,16 +31,16 @@ let keywords = "as"; "qualified"; "hiding" ; "unit" ] Idset.empty -let preamble prm used_modules print_dummy = +let preamble prm used_modules (mldummy,tdummy,tunknown) = let m = String.capitalize (string_of_id prm.mod_name) in str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ str "import qualified Prelude" ++ fnl() ++ Idset.fold (fun m s -> - s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl()) + str "import qualified " ++ pr_id (uppercase_id m) ++ fnl() ++ s) used_modules (mt ()) ++ fnl() ++ - (if print_dummy then + (if mldummy then str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl () ++ fnl() else mt()) @@ -69,6 +69,7 @@ let empty_env () = [], P.globals() 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_type_global r | Tglob (r,l) -> @@ -150,7 +151,7 @@ let rec pp_expr par env args = (* An [MLexn] may be applied, but I don't really care. *) (open_par par ++ str "Prelude.error" ++ spc () ++ qs s ++ close_par par) - | MLdummy | MLdummy' -> + | MLdummy -> str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLcast (a,t) -> pp_expr par env args a | MLmagic a -> pp_expr par env args a @@ -232,8 +233,6 @@ let pp_decl = function | Dind ([], _) -> mt () | Dind (i, _) -> hov 0 (pp_inductive i) - | DdummyType r -> - hov 0 (str "type " ++ pp_type_global r ++ str " = ()" ++ fnl ()) | Dtype (r, l, t) -> let l = rename_tvars keywords l in let l' = List.rev l in @@ -241,13 +240,13 @@ let pp_decl = function prlist_with_sep (fun () -> (str " ")) pr_id l ++ (if l <> [] then (str " ") else (mt ())) ++ str "=" ++ spc () ++ pp_type false l' t ++ fnl ()) - | Dfix (rv, defs) -> + | Dfix (rv, defs,_) -> let ids = List.map rename_global (Array.to_list rv) in let env = List.rev ids, P.globals() in (prlist_with_sep (fun () -> fnl () ++ fnl ()) (fun (fi,ti) -> pp_function env (pr_id fi) ti) (List.combine ids (Array.to_list defs)) ++ fnl ()) - | Dterm (r, a) -> + | Dterm (r, a, _) -> hov 0 (pp_function (empty_env ()) (pp_global r) a ++ fnl ()) | DcustomTerm (r,s) -> hov 0 (pp_global r ++ str " =" ++ spc () ++ str s ++ fnl ()) diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli index 5d744be2a..8a0deeca6 100644 --- a/contrib/extraction/haskell.mli +++ b/contrib/extraction/haskell.mli @@ -15,6 +15,6 @@ open Miniml val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds +val preamble : extraction_params -> Idset.t -> 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 eb82e4752..3945e941b 100644 --- a/contrib/extraction/miniml.mli +++ b/contrib/extraction/miniml.mli @@ -14,16 +14,26 @@ open Pp open Names open Term open Libnames +open Util (*s ML type expressions. *) type ml_type = | Tarr of ml_type * ml_type - | Tvar of int | Tglob of global_reference * ml_type list + | Tvar of int + | Tvar' of int (* same as Tvar, used to avoid clash *) + | Tmeta of ml_meta (* used during ML type reconstruction *) | Tdummy | Tunknown - + +and ml_meta = { id : int; mutable contents : ml_type option} + +(* ML type schema. + The integer is the number of variable in the schema. *) + +type ml_schema = int * ml_type + (*s ML inductive types. *) type ml_ind = @@ -42,7 +52,6 @@ type ml_ast = | MLfix of int * identifier array * ml_ast array | MLexn of string | MLdummy - | MLdummy' | MLcast of ml_ast * ml_type | MLmagic of ml_ast @@ -51,11 +60,10 @@ type ml_ast = type ml_decl = | Dind of ml_ind list * bool (* cofix *) | Dtype of global_reference * identifier list * ml_type - | Dterm of global_reference * ml_ast - | DdummyType of global_reference + | Dterm of global_reference * ml_ast * ml_type | DcustomTerm of global_reference * string | DcustomType of global_reference * string - | Dfix of global_reference array * ml_ast array + | Dfix of global_reference array * ml_ast array * ml_type array (*s Pretty-printing of MiniML in a given concrete syntax is parameterized by a function [pp_global] that pretty-prints global references. diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 073d574bb..0aa76805f 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -36,7 +36,155 @@ let id_of_name = function | Name id when id = dummy_name -> anonymous | Name id -> id -(*S Operations upon ML types. *) +(*S Operations upon ML types (with meta). *) + +let meta_count = ref 0 + +let reset_meta_count () = meta_count := 0 + +let new_meta _ = + incr meta_count; + Tmeta {id = !meta_count; contents = None} + +(*s From a type schema to a type. All [Tvar] becomes fresh [Tmeta]. *) + +let instantiation (nb,t) = + let c = !meta_count in + let a = Array.make nb {id=0; contents = None} + in + for i = 0 to nb-1 do + a.(i) <- {id=i+c+1; contents=None} + done; + let rec var2meta t = match t with + | Tvar i -> Tmeta a.(i-1) + | Tmeta {contents=None} -> t + | Tmeta {contents=Some u} -> var2meta u + | Tglob (r,l) -> Tglob(r, List.map var2meta l) + | Tarr (t1,t2) -> Tarr (var2meta t1, var2meta t2) + | t -> t + in + meta_count := !meta_count + nb; + var2meta t + +(*s Occur-check of a uninstantiated meta in a type *) + +let rec type_occurs alpha t = + match t with + | Tmeta {id=beta; contents=None} -> alpha = beta + | Tmeta {contents=Some u} -> type_occurs alpha u + | Tarr (t1, t2) -> type_occurs alpha t1 || type_occurs alpha t2 + | Tglob (r,l) -> List.exists (type_occurs alpha) l + | _ -> false + +(*s Most General Unificator *) + +let rec mgu = function + | Tmeta m, Tmeta m' when m.id = m'.id -> () + | Tmeta m, t when m.contents=None -> + if type_occurs m.id t then raise Impossible + else m.contents <- Some t + | t, Tmeta m when m.contents=None -> + if type_occurs m.id t then raise Impossible + else m.contents <- Some t + | Tmeta {contents=Some u}, t -> mgu (u, t) + | t, Tmeta {contents=Some u} -> mgu (t, u) + | Tarr(a, b), Tarr(a', b') -> + mgu (a, a'); mgu (b, b') + | Tglob (r,l), Tglob (r',l') when r = r' -> + List.iter mgu (List.combine l l') + | Tvar i, Tvar j when i = j -> () + | Tvar' i, Tvar' j when i = j -> () + | Tdummy, Tdummy -> () + | Tunknown, Tunknown -> () + | _ -> raise Impossible + +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 p a = if needs_magic p then MLmagic a else a + + +(*S ML type env. *) + +module Mlenv = struct + + let meta_cmp m m' = compare m.id m'.id + module Metaset = Set.Make(struct type t = ml_meta let compare = meta_cmp end) + + (* Main MLenv type. [env] is the real environment, whereas [free] + (tries to) keep trace of the free meta variables occurring in [env]. *) + + type t = { env : ml_schema list; mutable free : Metaset.t} + + (* Empty environment. *) + + let empty = { env = []; free = Metaset.empty } + + (* [get] returns a instantiated copy of the n-th most recently added + type in the environment. *) + + let get mle n = + assert (List.length mle.env >= n); + instantiation (List.nth mle.env (n-1)) + + (* [find_free] finds the free meta in a type. *) + + let rec find_free set = function + | Tmeta m when m.contents = None -> Metaset.add m set + | Tmeta {contents = Some t} -> find_free set t + | Tarr (a,b) -> find_free (find_free set a) b + | Tglob (_,l) -> List.fold_left find_free set l + | _ -> set + + (* The [free] set of an environment can be outdate after + some unifications. [clean_free] takes care of that. *) + + let clean_free mle = + let rem = ref Metaset.empty + and add = ref Metaset.empty in + let clean m = match m.contents with + | None -> () + | Some u -> rem := Metaset.add m !rem; add := find_free !add u + in + Metaset.iter clean mle.free; + mle.free <- Metaset.union (Metaset.diff mle.free !rem) !add + + (* From a type to a type schema. If a [Tmeta] is still uninstantiated + and does appears in the [mle], then it becomes a [Tvar]. *) + + let generalization mle t = + let c = ref 0 in + let map = ref (Intmap.empty : int Intmap.t) in + let add_new i = incr c; map := Intmap.add i !c !map; !c in + let rec meta2var t = match t with + | Tmeta {contents=Some u} -> meta2var u + | Tmeta ({id=i} as m) -> + (try Tvar (Intmap.find i !map) + with Not_found -> + if Metaset.mem m mle.free then t + else Tvar (add_new i)) + | Tarr (t1,t2) -> Tarr (meta2var t1, meta2var t2) + | Tglob (r,l) -> Tglob (r, List.map meta2var l) + | t -> t + in !c, meta2var t + + (* Adding a type in an environment, after generalizing. *) + + let push_gen mle t = + clean_free mle; + { env = generalization mle t :: mle.env; free = mle.free } + + let push_type {env=e;free=f} t = + { env = (0,t) :: e; free = find_free f t} + + let push_std_type {env=e;free=f} t = + { env = (0,t) :: e; free = f} + +end + + +(*S Operations upon ML types (without meta). *) (*s Does a section path occur in a ML type ? *) @@ -47,10 +195,118 @@ let kn_of_r r = match r with | _ -> assert false let rec type_mem_kn kn = function + | Tmeta _ -> assert false | Tglob (r,l) -> (kn_of_r r) = kn || List.exists (type_mem_kn kn) l | Tarr (a,b) -> (type_mem_kn kn a) || (type_mem_kn kn b) | _ -> false +let type_maxvar t = + let rec parse n = function + | Tmeta _ -> assert false + | Tvar i -> max i n + | Tarr (a,b) -> parse (parse n a) b + | Tglob (_,l) -> List.fold_left parse n l + | _ -> n + in parse 0 t + +let rec type_decomp = function + | Tmeta _ -> assert false + | Tarr (a,b) -> let l,h = type_decomp b in a::l, h + | a -> [],a + +let rec type_recomp (l,t) = match l with + | [] -> t + | a::l -> Tarr (a, type_recomp (l,t)) + +let rec var2var' = function + | Tmeta _ -> assert false + | Tvar i -> Tvar' i + | Tarr (a,b) -> Tarr (var2var' a, var2var' b) + | Tglob (r,l) -> Tglob (r, List.map var2var' l) + | a -> a + +(*s Sustitution of [Tvar i] by [t] in a ML type. *) + +let type_subst i t = + let rec subst = function + | Tvar j when i = j -> t + | Tarr (a,b) -> Tarr (subst a, subst b) + | Tglob (r, l) -> Tglob (r, List.map subst l) + | a -> a + in subst + +(* Simultaneous substitution of [Tvar 1;...; Tvar n] by [l] in a ML type. *) + +let type_subst_all l t = + let rec subst = function + | Tvar j -> List.nth l (j-1) + | Tarr (a,b) -> Tarr (subst a, subst b) + | Tglob (r, l) -> Tglob (r, List.map subst l) + | a -> a + in subst t + +type abbrev_map = global_reference -> ml_type option + +(*s Delta-reduction of type constants everywhere in a ML type [t]. + [env] is a function of type [ml_type_env]. *) + +let type_expand env t = + let rec expand = function + | Tglob (r,l) as t -> + (match env r with + | Some mlt -> expand (type_subst_all l mlt) + | None -> Tglob (r, List.map expand l)) + | Tarr (a,b) -> Tarr (expand a, expand b) + | a -> a + in expand t + +(*s Idem, but only at the top level of implications. *) + +let is_arrow = function Tarr _ -> true | _ -> false + +let type_weak_expand env t = + let rec expand = function + | Tglob (r,l) as t -> + (match env r with + | Some mlt -> + let u = expand (type_subst_all l mlt) in + if is_arrow u then u else t + | None -> t) + | Tarr (a,b) -> Tarr (a, expand b) + | a -> a + in expand t + +(*s Equality over ML types modulo delta-reduction *) + +let type_eq env t t' = (type_expand env t = type_expand env t') + +let type_neq env t t' = (type_expand env t <> type_expand env t') + +let type_to_sign env t = + let rec f = function + | Tarr (a,b) -> (Tdummy <> a) :: (f b) + | _ -> [] + in f (type_expand env t) + +let type_expunge env t = + let s = type_to_sign env t in + if s = [] then t + else if List.mem true s then + let rec f t s = + if List.mem false s then + match t with + | Tarr (a,b) -> + let t = f b (List.tl s) in + if List.hd s then Tarr (a, t) else t + | Tglob (r,l) -> + (match env r with + | Some mlt -> f (type_subst_all l mlt) s + | None -> assert false) + | _ -> assert false + else t + in f t s + else Tarr (Tdummy, snd (type_decomp (type_weak_expand env t))) + (*S Generic functions over ML ast terms. *) (*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care @@ -68,7 +324,7 @@ let ast_iter_rel f = | MLcons (_,l) -> List.iter (iter n) l | MLcast (a,_) -> iter n a | MLmagic a -> iter n a - | MLglob _ | MLexn _ | MLdummy | MLdummy' -> () + | MLglob _ | MLexn _ | MLdummy -> () in iter 0 (*s Map over asts. *) @@ -84,7 +340,7 @@ let ast_map f = function | MLcons (c,l) -> MLcons (c, List.map f l) | MLcast (a,t) -> MLcast (f a, t) | MLmagic a -> MLmagic (f a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a (*s Map over asts, with binding depth as parameter. *) @@ -100,7 +356,7 @@ let ast_map_lift f n = function | MLcons (c,l) -> MLcons (c, List.map (f n) l) | MLcast (a,t) -> MLcast (f n a, t) | MLmagic a -> MLmagic (f n a) - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> a + | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> a (*s Iter over asts. *) @@ -115,7 +371,7 @@ let ast_iter f = function | MLcons (c,l) -> List.iter f l | MLcast (a,t) -> f a | MLmagic a -> f a - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' as a -> () + | MLrel _ | MLglob _ | MLexn _ | MLdummy as a -> () (*S Searching occurrences of a particular term (no lifting done). *) @@ -124,17 +380,35 @@ let rec ast_search t a = let decl_search t l = let one_decl = function - | Dterm (_,a) -> ast_search t a - | Dfix (_,c) -> Array.iter (ast_search t) c + | Dterm (_,a,_) -> ast_search t a + | Dfix (_,c,_) -> Array.iter (ast_search t) c + | _ -> () + in + try List.iter one_decl l; false with Found -> true + +let rec type_search t = function + | Tarr (a,b) -> type_search t a; type_search t b + | Tglob (r,l) -> List.iter (type_search t) l + | u -> if t = u then raise Found + +let decl_type_search t l = + let one_decl = function + | Dind(l,_) -> + List.iter (fun (_,_,l) -> + (List.iter (fun (_,l) -> + List.iter (type_search t) l) l)) l + | Dterm (_,_,u) -> type_search t u + | Dfix (_,_,v) -> Array.iter (type_search t) v + | Dtype (_,_,u) -> type_search t u | _ -> () in try List.iter one_decl l; false with Found -> true (*S Operations concerning De Bruijn indices. *) -(*s [occurs k t] returns [true] if [(Rel k)] occurs in [t]. *) +(*s [ast_occurs k t] returns [true] if [(Rel k)] occurs in [t]. *) -let occurs k t = +let ast_occurs k t = try ast_iter_rel (fun i -> if i = k then raise Found) t; false with Found -> true @@ -157,16 +431,15 @@ let nb_occur_k k t = let nb_occur t = nb_occur_k 1 t (*s Lifting on terms. - [ml_lift k t] lifts the binding depth of [t] across [k] bindings. *) + [ast_lift k t] lifts the binding depth of [t] across [k] bindings. *) -let ml_lift k t = +let ast_lift k t = let rec liftrec n = function | MLrel i as a -> if i-n < 1 then a else MLrel (i+k) | a -> ast_map_lift liftrec n a in if k = 0 then t else liftrec 0 t -let ml_pop t = ml_lift (-1) t - +let ast_pop t = ast_lift (-1) t (*s [permut_rels k k' c] translates [Rel 1 ... Rel k] to [Rel (k'+1) ... Rel (k'+k)] and [Rel (k+1) ... Rel (k+k')] to [Rel 1 ... Rel k'] *) @@ -184,11 +457,11 @@ let permut_rels k k' = (*s Substitution. [ml_subst e t] substitutes [e] for [Rel 1] in [t]. Lifting (of one binder) is done at the same time. *) -let rec ml_subst e = +let ast_subst e = let rec subst n = function | MLrel i as a -> let i' = i-n in - if i'=1 then ml_lift n e + if i'=1 then ast_lift n e else if i'<1 then a else MLrel (i-1) | a -> ast_map_lift subst n a @@ -205,7 +478,7 @@ let gen_subst v d t = let i'= i-n in if i' < 1 then a else if i' < Array.length v then - if v.(i') = 0 then MLdummy' + if v.(i') = 0 then MLdummy else MLrel (v.(i')+n) else MLrel (i+d) | a -> ast_map_lift subst n a @@ -264,6 +537,13 @@ let rec dummy_lams a = function | 0 -> a | n -> dummy_lams (MLlam (dummy_name,a)) (pred n) +(*s mixed according to a signature. *) + +let rec anonym_or_dummy_lams a = function + | [] -> a + | true :: s -> MLlam(anonymous, anonym_or_dummy_lams a s) + | false :: s -> MLlam(dummy_name, anonym_or_dummy_lams a s) + (*S Operations concerning eta. *) (*s The following function creates [MLrel n;...;MLrel 1] *) @@ -271,6 +551,13 @@ let rec dummy_lams a = function let rec eta_args n = if n = 0 then [] else (MLrel n)::(eta_args (pred n)) +(*s Same, but filtered by a signature. *) + +let rec eta_args_sign n = function + | [] -> [] + | true :: s -> (MLrel n) :: (eta_args_sign (n-1) s) + | false :: s -> eta_args_sign (n-1) s + (*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *) let rec test_eta_args_lift k n = function @@ -291,7 +578,7 @@ let eta_red e = let a1,a2 = list_chop m a in let f = if m = 0 then f else MLapp (f,a1) in if test_eta_args_lift 0 n a2 && not (occurs_itvl 1 n f) - then ml_lift (-n) f + then ast_lift (-n) f else e | _ -> e @@ -331,11 +618,11 @@ let check_constant_case br = let (r,l,t) = br.(0) in let n = List.length l in if occurs_itvl 1 n t then raise Impossible; - let cst = ml_lift (-n) t in + let cst = ast_lift (-n) t in for i = 1 to Array.length br - 1 do let (r,l,t) = br.(i) in let n = List.length l in - if (occurs_itvl 1 n t) || (cst <> (ml_lift (-n) t)) + if (occurs_itvl 1 n t) || (cst <> (ast_lift (-n) t)) then raise Impossible done; cst @@ -382,7 +669,7 @@ let iota_gen br = | MLcons (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 = ml_lift k c in + let c = ast_lift k c in MLapp (c,a) | MLcase(e,br') -> let new_br = @@ -392,7 +679,7 @@ let iota_gen br = in iota 0 let is_atomic = function - | MLrel _ | MLglob _ | MLexn _ | MLdummy | MLdummy' -> true + | MLrel _ | MLglob _ | MLexn _ | MLdummy -> true | _ -> false (*S The main simplification function. *) @@ -409,38 +696,38 @@ let rec simpl o = function simpl_case o br (simpl o e) | MLletin(id,c,e) when (id = dummy_name) || (is_atomic c) || (nb_occur e <= 1) -> - simpl o (ml_subst c e) + simpl o (ast_subst c e) | MLfix(i,ids,c) as t when o -> let n = Array.length ids in if occurs_itvl 1 n c.(i) then MLfix (i, ids, Array.map (simpl o) c) - else simpl o (ml_lift (-n) c.(i)) (* Dummy fixpoint *) + else simpl o (ast_lift (-n) c.(i)) (* Dummy fixpoint *) | a -> ast_map (simpl o) a and simpl_app o a = function | MLapp (f',a') -> simpl_app o (a'@a) f' | MLlam (id,t) when id = dummy_name -> - simpl o (MLapp (ml_pop t, List.tl a)) + simpl o (MLapp (ast_pop t, List.tl a)) | MLlam (id,t) -> (* Beta redex *) (match nb_occur t with - | 0 -> simpl o (MLapp (ml_pop t, List.tl a)) + | 0 -> simpl o (MLapp (ast_pop t, List.tl a)) | 1 when o -> - simpl o (MLapp (ml_subst (List.hd a) t, List.tl a)) + simpl o (MLapp (ast_subst (List.hd a) t, List.tl a)) | _ -> - let a' = List.map (ml_lift 1) (List.tl a) in + let a' = List.map (ast_lift 1) (List.tl a) in simpl o (MLletin (id, List.hd a, MLapp (t, a')))) | MLletin (id,e1,e2) -> (* Application of a letin: we push arguments inside *) - MLletin (id, e1, simpl o (MLapp (e2, List.map (ml_lift 1) a))) + MLletin (id, e1, simpl o (MLapp (e2, List.map (ast_lift 1) a))) | MLcase (e,br) -> (* Application of a case: we push arguments inside *) let br' = Array.map (fun (n,l,t) -> let k = List.length l in - let a' = List.map (ml_lift k) a in + let a' = List.map (ast_lift k) a in (n, l, simpl o (MLapp (t,a')))) br in simpl o (MLcase (e,br')) - | (MLdummy | MLdummy' | MLexn _) as e -> e + | (MLdummy | MLexn _) as e -> e (* We just discard arguments in those cases. *) | f -> MLapp (f,a) @@ -461,11 +748,11 @@ and simpl_case o br e = let ids,br = permut_case_fun br [] in let n = List.length ids in if n = 0 then MLcase (e, br) - else named_lams ids (MLcase (ml_lift n e, br)) + else named_lams ids (MLcase (ast_lift n e, br)) let rec post_simpl = function | MLletin(_,c,e) when (is_atomic (eta_red c)) -> - post_simpl (ml_subst (eta_red c) e) + post_simpl (ast_subst (eta_red c) e) | a -> ast_map post_simpl a (*S Local prop elimination. *) @@ -491,7 +778,7 @@ let kill_some_lams bl (ids,c) = let n = List.length bl in let n' = List.fold_left (fun n b -> if b then (n+1) else n) 0 bl in if n = n' then ids,c - else if n' = 0 then [],ml_lift (-n) c + else if n' = 0 then [],ast_lift (-n) c else begin let v = Array.make (n+1) 0 in let rec parse_ids i j = function @@ -523,15 +810,15 @@ let kill_dummy_args ids t0 t = let m = List.length ids in let bl = List.rev_map ((<>) dummy_name) ids in let rec killrec n = function - | MLapp(e, a) when e = ml_lift n t0 -> + | MLapp(e, a) when e = ast_lift n t0 -> let k = max 0 (m - (List.length a)) in let a = List.map (killrec n) a in - let a = List.map (ml_lift k) a in + let a = List.map (ast_lift k) a in let a = select_via_bl bl (a @ (eta_args k)) in - named_lams (list_firstn k ids) (MLapp (ml_lift k e, a)) - | e when e = ml_lift n t0 -> + named_lams (list_firstn k ids) (MLapp (ast_lift k e, a)) + | e when e = ast_lift n t0 -> let a = select_via_bl bl (eta_args m) in - named_lams ids (MLapp (ml_lift m e, a)) + named_lams ids (MLapp (ast_lift m e, a)) | e -> ast_map_lift killrec n e in killrec 0 t @@ -541,14 +828,14 @@ let rec kill_dummy = function | MLfix(i,fi,c) -> (try let ids,c = kill_dummy_fix i fi c in - ml_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1)) + ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1)) with Impossible -> MLfix (i,fi,Array.map kill_dummy c)) | MLapp (MLfix (i,fi,c),a) -> (try let ids,c = kill_dummy_fix i fi c in - let a = List.map (fun t -> ml_lift 1 (kill_dummy t)) a in + let a = List.map (fun t -> ast_lift 1 (kill_dummy t)) a in let e = kill_dummy_args ids (MLrel 1) (MLapp (MLrel 1,a)) in - ml_subst (MLfix (i,fi,c)) e + ast_subst (MLfix (i,fi,c)) e with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),List.map kill_dummy a)) | MLletin(id, MLfix (i,fi,c),e) -> @@ -591,7 +878,7 @@ let general_optimize_fix f ids n args m c = in list_iter_i aux args; let args_f = List.rev_map (fun i -> MLrel (i+m+1)) (Array.to_list v) in let new_f = anonym_lams (MLapp (MLrel (n+m+1),args_f)) m in - let new_c = named_lams ids (normalize (MLapp ((ml_subst new_f c),args))) in + let new_c = named_lams ids (normalize (MLapp ((ast_subst new_f c),args))) in MLfix(0,[|f|],[|new_c|]) let optimize_fix a = @@ -603,7 +890,7 @@ let optimize_fix a = else match a' with | MLfix(_,[|f|],[|c|]) -> let new_f = MLapp (MLrel (n+1),eta_args n) in - let new_c = named_lams ids (normalize (ml_subst new_f c)) + let new_c = named_lams ids (normalize (ast_subst new_f c)) in MLfix(0,[|f|],[|new_c|]) | MLapp(a',args) -> let m = List.length args in @@ -783,7 +1070,7 @@ let subst_glob_ast r m = in substrec let subst_glob_decl r m = function - | Dterm(r',t') -> Dterm(r', subst_glob_ast r m t') + | Dterm(r',t',typ) -> Dterm(r', subst_glob_ast r m t', typ) | d -> d let inline_glob r t l = @@ -802,40 +1089,42 @@ let add_ml_decls prm decls = let l2 = List.map (fun (r,s)-> DcustomTerm (r,s)) l2 in l1 @ l2 @ decls -let rec expunge_fix_decls prm v c b = function - | [] -> b, [] - | Dterm (r, t) :: l when array_exists ((=) r) v -> +let rec expunge_fix_decls prm v c map b = function + | [] -> b, [], map + | Dterm (r, t, typ) :: l when array_exists ((=) r) v -> let t = normalize t in let t' = optimize_fix t in (match t' with | MLfix(_,_,c') when c=c' -> let b',l = inline_glob r t l in - expunge_fix_decls prm v c (b || b' || List.mem r prm.to_appear) l + let b = b || b' || List.mem r prm.to_appear in + let map = Refmap.add r typ map in + expunge_fix_decls prm v c map b l | _ -> raise Impossible) - | d::l -> let b,l = expunge_fix_decls prm v c b l in b, d::l + | d::l -> let b,l,map = expunge_fix_decls prm v c map b l in b, d::l, map let rec optimize prm = function | [] -> [] - | (DdummyType r | Dterm(r,MLdummy')) as d :: l -> + | (Dtype (r,_,Tdummy) | Dterm(r,MLdummy,_)) as d :: l -> if List.mem r prm.to_appear then d :: (optimize prm l) else optimize prm l - | Dterm (r,t) :: l -> + | Dterm (r,t,typ) :: l -> let t = normalize t in let b,l = inline_glob r t l in let b = b || prm.modular || List.mem r prm.to_appear in let t' = optimize_fix t in - (try optimize_Dfix prm r t' b l - with Impossible -> - if b then Dterm (r,t') :: (optimize prm l) - else optimize prm l) + (try optimize_Dfix prm (r,t',typ) b l + with Impossible -> + if b then Dterm (r,t',typ) :: (optimize prm l) + else optimize prm l) | d :: l -> d :: (optimize prm l) -and optimize_Dfix prm r t b l = +and optimize_Dfix prm (r,t,typ) b l = match t with | MLfix (_, f, c) -> if Array.length f = 1 then - if b then Dfix ([|r|], c) :: (optimize prm l) + if b then Dfix ([|r|], c,[|typ|]) :: (optimize prm l) else optimize prm l else let v = try @@ -843,8 +1132,15 @@ and optimize_Dfix prm r t b l = Array.map (fun id -> locate (make_qualid d id)) f with Not_found -> raise Impossible in - let b,l = expunge_fix_decls prm v c b l in - if b then Dfix (v, c) :: (optimize prm l) + let map = Refmap.add r typ (Refmap.empty) in + let b,l,map = expunge_fix_decls prm v c map b l in + if b then + let typs = + Array.map + (fun r -> try Refmap.find r map + with Not_found -> Tunknown) v + in + Dfix (v, c, typs) :: (optimize prm l) else optimize prm l | _ -> raise Impossible diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index 854e3b5e4..bd02958bc 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -12,7 +12,7 @@ open Names open Term open Libnames open Miniml - +open Util (*s Special identifiers. [dummy_name] is to be used for dead code and will be printed as [_] in concrete (Caml) code. *) @@ -25,39 +25,82 @@ val id_of_name : name -> identifier the list [idn;...;id1] and the term [t]. *) val collect_lams : ml_ast -> identifier list * ml_ast - val collect_n_lams : int -> ml_ast -> identifier list * ml_ast - val nb_lams : ml_ast -> int (*s [anonym_lams a n] creates [n] anonymous [MLlam] in front of [a] *) val anonym_lams : ml_ast -> int -> ml_ast - val dummy_lams : ml_ast -> int -> ml_ast - val named_lams : identifier list -> ml_ast -> ml_ast +val anonym_or_dummy_lams : ml_ast -> bool list -> ml_ast + +val eta_args_sign : int -> bool list -> ml_ast list + +(*s Utility functions over ML types with meta. *) + +val reset_meta_count : unit -> unit +val new_meta : 'a -> ml_type + +val instantiation : ml_schema -> ml_type + +val needs_magic : ml_type * ml_type -> bool +val put_magic_if : bool -> ml_ast -> ml_ast +val put_magic : ml_type * ml_type -> ml_ast -> ml_ast + +(*s ML type environment. *) + +module Mlenv : sig + type t + val empty : t + + (* get the n-th more recently entered schema and instantiate it. *) + val get : t -> int -> ml_type -(*s Utility functions over ML types. [update_args sp vl t] puts [vl] - as arguments behind every inductive types [(sp,_)]. *) + (* Adding a type in an environment, after generalizing free meta *) + val push_gen : t -> ml_type -> t + + (* Adding a type with no [Tvar] *) + val push_type : t -> ml_type -> t + + (* Adding a type with no [Tvar] nor [Tmeta] *) + val push_std_type : t -> ml_type -> t +end + +(*s Utility functions over ML types without meta *) val kn_of_r : global_reference -> kernel_name val type_mem_kn : kernel_name -> ml_type -> bool -(*s Utility functions over ML terms. [occurs n t] checks whether [Rel - n] occurs (freely) in [t]. [ml_lift] is de Bruijn - lifting. *) +val type_maxvar : ml_type -> int -val ast_iter : (ml_ast -> unit) -> ml_ast -> unit +val type_decomp : ml_type -> ml_type list * ml_type +val type_recomp : ml_type list * ml_type -> ml_type + +val var2var' : ml_type -> ml_type -val occurs : int -> ml_ast -> bool +val type_subst : int -> ml_type -> ml_type -> ml_type +val type_subst_all : ml_type list -> ml_type -> ml_type -val ml_lift : int -> ml_ast -> ml_ast +type abbrev_map = global_reference -> ml_type option -val ml_subst : ml_ast -> ml_ast -> ml_ast +val type_expand : abbrev_map -> ml_type -> ml_type +val type_eq : abbrev_map -> ml_type -> ml_type -> bool +val type_neq : abbrev_map -> ml_type -> ml_type -> bool +val type_to_sign : abbrev_map -> ml_type -> bool list +val type_expunge : abbrev_map -> ml_type -> ml_type -val ml_pop : ml_ast -> ml_ast + +(*s Utility functions over ML terms. [ast_occurs n t] checks whether [Rel + n] occurs (freely) in [t]. [ml_lift] is de Bruijn + lifting. *) + +val ast_iter : (ml_ast -> unit) -> ml_ast -> unit +val ast_occurs : int -> ml_ast -> bool +val ast_lift : int -> ml_ast -> ml_ast +val ast_subst : ml_ast -> ml_ast -> ml_ast +val ast_pop : ml_ast -> ml_ast (*s Some transformations of ML terms. [optimize] simplify all beta redexes (when the argument does not occur, it is just @@ -71,6 +114,7 @@ val optimize : (* Misc. *) val decl_search : ml_ast -> ml_decl list -> bool +val decl_type_search : ml_type -> ml_decl list -> bool val add_ml_decls : extraction_params -> ml_decl list -> ml_decl list diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 1e4033704..20a1d3776 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -37,6 +37,13 @@ let pp_tvar id = then str ("'"^s) else str ("' "^s) +let pp_tuple_light f = function + | [] -> (mt ()) + | [x] -> f true x + | l -> (str "(" ++ + prlist_with_sep (fun () -> (str "," ++ spc ())) (f false) l ++ + str ")") + let pp_tuple f = function | [] -> (mt ()) | [x] -> f x @@ -118,16 +125,21 @@ let keywords = "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] Idset.empty -let preamble _ used_modules print_dummy = - Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl()) +let preamble _ used_modules (mldummy,tdummy,tunknown) = + Idset.fold (fun m s -> str "open " ++ pr_id (uppercase_id m) ++ fnl() ++ s) used_modules (mt ()) ++ (if Idset.is_empty used_modules then mt () else fnl ()) ++ - (if print_dummy then + (if tdummy || tunknown then str "type __ = Obj.t" ++ fnl() else mt()) + ++ + (if mldummy then str "let __ = let rec f _ = Obj.repr f in Obj.repr f" - ++ fnl () ++ fnl() - else mt ()) + ++ fnl () + else mt ()) + ++ + (if tdummy || tunknown || mldummy then fnl () else mt ()) + (*s The pretty-printing functor. *) @@ -145,16 +157,16 @@ let empty_env () = [], P.globals() let rec pp_type par vl t = let rec pp_rec par = function + | Tmeta _ | Tvar' _ -> assert false | Tvar i -> (try pp_tvar (List.nth vl (pred i)) with _ -> (str "'a" ++ int i)) | Tglob (r,[]) -> pp_type_global r - | Tglob (r,[u]) -> pp_rec true u ++ spc () ++ pp_type_global r - | Tglob (r,l) -> pp_tuple (pp_rec false) l ++ spc () ++ pp_type_global r + | Tglob (r,l) -> pp_tuple_light pp_rec l ++ spc () ++ pp_type_global r | Tarr (t1,t2) -> open_par par ++ pp_rec true t1 ++ spc () ++ str "->" ++ spc () ++ pp_rec false t2 ++ close_par par - | Tdummy -> str "Obj.t" - | Tunknown -> str "Obj.t" + | Tdummy -> str "__" + | Tunknown -> str "__" in hov 0 (pp_rec par t) @@ -206,15 +218,6 @@ let rec pp_expr par env args = if Refset.mem r !cons_cofix then (open_par par ++ str "lazy " ++ pp_global r env ++ close_par par) else pp_global r env - | MLcons (r,[a]) -> - assert (args=[]); - if Refset.mem r !cons_cofix then - (open_par par ++ str "lazy (" ++ - pp_global r env ++ spc () ++ - pp_expr true env [] a ++ str ")" ++ close_par par) - else - (open_par par ++ pp_global r env ++ spc () ++ - pp_expr true env [] a ++ close_par par) | MLcons (r,args') -> assert (args=[]); if Refset.mem r !cons_cofix then @@ -249,21 +252,22 @@ let rec pp_expr par env args = close_par par') | MLfix (i,ids,defs) -> let ids',env' = push_vars (List.rev (Array.to_list ids)) env in - pp_fix par env' (Some i) (Array.of_list (List.rev ids'),defs) args + pp_fix par env' i (Array.of_list (List.rev ids'),defs) args | MLexn s -> (* An [MLexn] may be applied, but I don't really care. *) (open_par par ++ str "assert false" ++ spc () ++ str ("(* "^s^" *)") ++ close_par par) | MLdummy -> - str "()" (* An [MLdummy] may be applied, but I don't really care. *) - | MLdummy' -> - str "__" (* idem *) + str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLcast (a,t) -> - (open_par true ++ pp_expr false env args a ++ spc () ++ str ":" ++ - spc () ++ pp_type false [] t ++ close_par true) + apply + (open_par true ++ pp_expr true env [] a ++ spc () ++ str ":" ++ + spc () ++ pp_type true [] t ++ close_par true) | MLmagic a -> - (open_par true ++ str "Obj.magic" ++ spc () ++ - pp_expr false env args a ++ close_par true) + let args' = pp_expr true env [] a :: args in + hov 2 (open_par par ++ str "Obj.magic" ++ spc () ++ + prlist_with_sep (fun () -> (spc ())) (fun s -> s) args' ++ + close_par par) and pp_one_pat env (r,ids,t) = let ids,env' = push_vars (List.rev ids) env in @@ -278,36 +282,12 @@ and pp_pat env pv = (fun x -> let s1,s2 = pp_one_pat env x in hov 2 (s1 ++ str " ->" ++ spc () ++ s2)) pv -(*s names of the functions ([ids]) are already pushed in [env], - and passed here just for convenience. *) - -and pp_fix par env in_p (ids,bl) args = - (open_par par ++ - v 0 (str "let rec " ++ - prvect_with_sep - (fun () -> (fnl () ++ str "and ")) - (fun (fi,ti) -> pp_function env (pr_id fi) ti) - (array_map2 (fun id b -> (id,b)) ids bl) ++ - fnl () ++ - match in_p with - | Some j -> - hov 2 (str "in " ++ pr_id (ids.(j)) ++ - if args <> [] then - (str " " ++ - prlist_with_sep (fun () -> (str " ")) - (fun s -> s) args) - else - (mt ())) - | None -> - (mt ())) ++ - close_par par) - and pp_function env f t = let bl,t' = collect_lams t in let bl,env' = push_vars bl env in let is_function pv = let ktl = array_map_to_list (fun (_,l,t0) -> (List.length l,t0)) pv in - not (List.exists (fun (k,t0) -> Mlutil.occurs (k+1) t0) ktl) + 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 @@ -326,6 +306,42 @@ and pp_function env f t = | _ -> (f ++ pr_binding (List.rev bl) ++ str " =" ++ fnl () ++ str " " ++ hov 2 (pp_expr false env' [] t')) + +(*s names of the functions ([ids]) are already pushed in [env], + and passed here just for convenience. *) + +and pp_fix par env i (ids,bl) args = + open_par par ++ + v 0 (str "let rec " ++ + prvect_with_sep + (fun () -> (fnl () ++ str "and ")) + (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (array_map2 (fun id b -> (id,b)) ids bl) ++ + fnl () ++ + hov 2 (str "in " ++ pr_id ids.(i) ++ + if args <> [] then + (str " " ++ + prlist_with_sep (fun () -> (str " ")) + (fun s -> s) args) + else mt ())) ++ + close_par par + +let pp_val e typ = + str "(** val " ++ e ++ str " : " ++ pp_type false [] typ ++ + str " **)" ++ fnl() ++ fnl() + +(*s Pretty-printing of [Dfix] *) + +let pp_Dfix env (ids,bl,typs) = + let init = + pp_val (pr_id ids.(0)) (typs.(0)) ++ + str "let rec " ++ pp_function env (pr_id ids.(0)) bl.(0) ++ fnl() + in + iterate_for 1 (Array.length ids - 1) + (fun i acc -> + acc ++ fnl() ++ pp_val (pr_id ids.(i)) (typs.(i)) ++ + str "and " ++ pp_function env (pr_id ids.(i)) bl.(i) ++ fnl()) + init (*s Pretty-printing of inductive types declaration. *) @@ -341,7 +357,7 @@ let pp_one_ind prefix (pl,name,cl) = | _ -> (str " of " ++ prlist_with_sep (fun () -> (spc () ++ str "* ")) - (pp_type true (List.rev pl)) l)) + (pp_type true pl) l)) in (pp_parameters pl ++ str prefix ++ pp_type_global name ++ str " =" ++ if cl = [] then str " unit (* empty inductive *)" @@ -380,23 +396,22 @@ let pp_decl = function hov 0 (pp_coind i) end else hov 0 (pp_ind i) - | DdummyType r -> - hov 0 (str "type " ++ pp_type_global r ++ str " = Obj.t" ++ fnl ()) | Dtype (r, l, t) -> let l = rename_tvars keywords l in hov 0 (str "type" ++ spc () ++ pp_parameters l ++ pp_type_global r ++ spc () ++ str "=" ++ spc () ++ - pp_type false (List.rev l) t ++ fnl ()) - | Dfix (rv, defs) -> + pp_type false l t ++ fnl ()) + | Dfix (rv, defs, typs) -> let ids = Array.map rename_global rv in let env = List.rev (Array.to_list ids), P.globals() in - (hov 2 (pp_fix false env None (ids,defs) [])) - | Dterm (r, a) -> - hov 0 (str "let " ++ - pp_function (empty_env ()) (pp_global' r) a ++ fnl ()) + hov 0 (pp_Dfix env (ids,defs,typs)) + | Dterm (r, a, t) -> + let e = pp_global' r in + (pp_val e t ++ + hov 0 (str "let " ++ pp_function (empty_env ()) e a ++ fnl ())) | DcustomTerm (r,s) -> hov 0 (str "let " ++ pp_global' r ++ - str " =" ++ spc () ++ str s ++ fnl ()) + str " =" ++ spc () ++ str s ++ fnl ()) | DcustomType (r,s) -> hov 0 (str "type " ++ pp_type_global r ++ str " = " ++ str s ++ fnl ()) diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli index 5304199b7..bda89d937 100644 --- a/contrib/extraction/ocaml.mli +++ b/contrib/extraction/ocaml.mli @@ -39,7 +39,7 @@ val get_db_name : int -> env -> identifier val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds +val preamble : extraction_params -> Idset.t -> 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 f0c0f500a..40d0ec5e2 100644 --- a/contrib/extraction/scheme.ml +++ b/contrib/extraction/scheme.ml @@ -32,8 +32,8 @@ let keywords = Idset.empty -let preamble _ _ print_dummy = - (if print_dummy then +let preamble _ _ (mldummy,_,_) = + (if mldummy then str "(define __ (lambda (_) __))" ++ fnl () ++ fnl() else mt ()) @@ -116,9 +116,7 @@ let rec pp_expr env args = (* An [MLexn] may be applied, but I don't really care. *) paren (str "absurd") | MLdummy -> - str "`_" (* An [MLdummy] may be applied, but I don't really care. *) - | MLdummy' -> - str "__" (* idem *) + str "__" (* An [MLdummy] may be applied, but I don't really care. *) | MLcast (a,t) -> pp_expr env args a | MLmagic a -> @@ -156,10 +154,9 @@ and pp_fix env j (ids,bl) args = let pp_decl = function | Dind _ -> mt () - | DdummyType _ -> mt () | Dtype _ -> mt () | DcustomType _ -> mt () - | Dfix (rv, defs) -> + | Dfix (rv, defs,_) -> let ids = Array.map rename_global rv in let env = List.rev (Array.to_list ids), P.globals() in prvect_with_sep @@ -170,7 +167,7 @@ let pp_decl = function (pp_expr env [] ti)) ++ fnl ())) (array_map2 (fun id b -> (id,b)) ids defs) - | Dterm (r, a) -> + | Dterm (r, a, _) -> hov 2 (paren (str "define " ++ (pp_global' r) ++ spc () ++ pp_expr (empty_env ()) [] a)) ++ fnl () | DcustomTerm (r,s) -> diff --git a/contrib/extraction/scheme.mli b/contrib/extraction/scheme.mli index 4a98e9769..51fac4fb7 100644 --- a/contrib/extraction/scheme.mli +++ b/contrib/extraction/scheme.mli @@ -17,7 +17,7 @@ open Nametab val keywords : Idset.t -val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds +val preamble : extraction_params -> Idset.t -> bool * bool * bool -> std_ppcmds module Make : functor(P : Mlpp_param) -> Mlpp diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 063c18a3c..7931dba01 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -23,6 +23,7 @@ val optim : unit -> bool (*s Set and Map over global reference *) module Refset : Set.S with type elt = global_reference +module Refmap : Map.S with type key = global_reference (*s Target language. *) diff --git a/contrib/extraction/test/.depend b/contrib/extraction/test/.depend index 1580ebf92..067abdfbd 100644 --- a/contrib/extraction/test/.depend +++ b/contrib/extraction/test/.depend @@ -1,260 +1,600 @@ -theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmo \ - theories/Arith/peano_dec.cmo theories/Bool/sumbool.cmo +theories/Arith/arithSyntax.cmo: theories/Arith/arithSyntax.cmi +theories/Arith/arithSyntax.cmx: theories/Arith/arithSyntax.cmi +theories/Arith/between.cmo: theories/Arith/between.cmi +theories/Arith/between.cmx: theories/Arith/between.cmi +theories/Arith/bool_nat.cmo: theories/Arith/compare_dec.cmi \ + theories/Arith/peano_dec.cmi theories/Bool/sumbool.cmi \ + theories/Arith/bool_nat.cmi theories/Arith/bool_nat.cmx: theories/Arith/compare_dec.cmx \ - theories/Arith/peano_dec.cmx theories/Bool/sumbool.cmx -theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo -theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Arith/compare.cmo: theories/Arith/compare_dec.cmo \ - theories/Init/specif.cmo + theories/Arith/peano_dec.cmx theories/Bool/sumbool.cmx \ + theories/Arith/bool_nat.cmi +theories/Arith/compare.cmo: theories/Arith/compare_dec.cmi \ + theories/Init/specif.cmi theories/Arith/compare.cmi theories/Arith/compare.cmx: theories/Arith/compare_dec.cmx \ - theories/Init/specif.cmx -theories/Arith/div2.cmo: theories/Init/datatypes.cmo theories/Init/peano.cmo -theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx -theories/Arith/eqNat.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Arith/compare.cmi +theories/Arith/compare_dec.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Arith/compare_dec.cmi +theories/Arith/compare_dec.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmx theories/Arith/compare_dec.cmi +theories/Arith/div2.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi \ + theories/Arith/div2.cmi +theories/Arith/div2.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmx \ + theories/Arith/div2.cmi +theories/Arith/eqNat.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Arith/eqNat.cmi theories/Arith/eqNat.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmo \ - theories/Init/datatypes.cmo theories/Arith/minus.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Arith/eqNat.cmi +theories/Arith/euclid.cmo: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Arith/minus.cmi \ + theories/Init/specif.cmi theories/Arith/euclid.cmi theories/Arith/euclid.cmx: theories/Arith/compare_dec.cmx \ theories/Init/datatypes.cmx theories/Arith/minus.cmx \ - theories/Init/specif.cmx -theories/Arith/even.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo -theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx -theories/Arith/max.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo -theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx -theories/Arith/min.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo -theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx -theories/Arith/minus.cmo: theories/Init/datatypes.cmo -theories/Arith/minus.cmx: theories/Init/datatypes.cmx -theories/Arith/mult.cmo: theories/Init/datatypes.cmo theories/Arith/plus.cmo -theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx -theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Arith/euclid.cmi +theories/Arith/even.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/even.cmi +theories/Arith/even.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/even.cmi +theories/Arith/gt.cmo: theories/Arith/gt.cmi +theories/Arith/gt.cmx: theories/Arith/gt.cmi +theories/Arith/le.cmo: theories/Arith/le.cmi +theories/Arith/le.cmx: theories/Arith/le.cmi +theories/Arith/lt.cmo: theories/Arith/lt.cmi +theories/Arith/lt.cmx: theories/Arith/lt.cmi +theories/Arith/max.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/max.cmi +theories/Arith/max.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/max.cmi +theories/Arith/min.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/min.cmi +theories/Arith/min.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/min.cmi +theories/Arith/minus.cmo: theories/Init/datatypes.cmi \ + theories/Arith/minus.cmi +theories/Arith/minus.cmx: theories/Init/datatypes.cmx \ + theories/Arith/minus.cmi +theories/Arith/mult.cmo: theories/Init/datatypes.cmi theories/Arith/plus.cmi \ + theories/Arith/mult.cmi +theories/Arith/mult.cmx: theories/Init/datatypes.cmx theories/Arith/plus.cmx \ + theories/Arith/mult.cmi +theories/Arith/peano_dec.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Arith/peano_dec.cmi theories/Arith/peano_dec.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Arith/plus.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo -theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx -theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmo -theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx -theories/Bool/boolEq.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Arith/peano_dec.cmi +theories/Arith/plus.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Arith/plus.cmi +theories/Arith/plus.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Arith/plus.cmi +theories/Arith/wf_nat.cmo: theories/Init/datatypes.cmi \ + theories/Arith/wf_nat.cmi +theories/Arith/wf_nat.cmx: theories/Init/datatypes.cmx \ + theories/Arith/wf_nat.cmi +theories/Bool/bool.cmo: theories/Init/datatypes.cmi theories/Init/specif.cmi \ + theories/Bool/bool.cmi +theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx \ + theories/Bool/bool.cmi +theories/Bool/boolEq.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/boolEq.cmi theories/Bool/boolEq.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Bool/bool.cmo: theories/Init/datatypes.cmo theories/Init/specif.cmo -theories/Bool/bool.cmx: theories/Init/datatypes.cmx theories/Init/specif.cmx -theories/Bool/decBool.cmo: theories/Init/specif.cmo -theories/Bool/decBool.cmx: theories/Init/specif.cmx -theories/Bool/ifProp.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Bool/boolEq.cmi +theories/Bool/decBool.cmo: theories/Init/specif.cmi theories/Bool/decBool.cmi +theories/Bool/decBool.cmx: theories/Init/specif.cmx theories/Bool/decBool.cmi +theories/Bool/ifProp.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/ifProp.cmi theories/Bool/ifProp.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Bool/sumbool.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Bool/ifProp.cmi +theories/Bool/sumbool.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi theories/Bool/sumbool.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Bool/zerob.cmo: theories/Init/datatypes.cmo -theories/Bool/zerob.cmx: theories/Init/datatypes.cmx -theories/Init/peano.cmo: theories/Init/datatypes.cmo -theories/Init/peano.cmx: theories/Init/datatypes.cmx -theories/Init/specif.cmo: theories/Init/datatypes.cmo -theories/Init/specif.cmx: theories/Init/datatypes.cmx -theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmo \ - theories/IntMap/addr.cmo theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/IntMap/map.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmi +theories/Bool/zerob.cmo: theories/Init/datatypes.cmi theories/Bool/zerob.cmi +theories/Bool/zerob.cmx: theories/Init/datatypes.cmx theories/Bool/zerob.cmi +theories/Init/datatypes.cmo: theories/Init/datatypes.cmi +theories/Init/datatypes.cmx: theories/Init/datatypes.cmi +theories/Init/datatypesSyntax.cmo: theories/Init/datatypesSyntax.cmi +theories/Init/datatypesSyntax.cmx: theories/Init/datatypesSyntax.cmi +theories/Init/logic.cmo: theories/Init/logic.cmi +theories/Init/logic.cmx: theories/Init/logic.cmi +theories/Init/logicSyntax.cmo: theories/Init/logicSyntax.cmi +theories/Init/logicSyntax.cmx: theories/Init/logicSyntax.cmi +theories/Init/logic_Type.cmo: theories/Init/logic_Type.cmi +theories/Init/logic_Type.cmx: theories/Init/logic_Type.cmi +theories/Init/logic_TypeSyntax.cmo: theories/Init/logic_TypeSyntax.cmi +theories/Init/logic_TypeSyntax.cmx: theories/Init/logic_TypeSyntax.cmi +theories/Init/peano.cmo: theories/Init/datatypes.cmi theories/Init/peano.cmi +theories/Init/peano.cmx: theories/Init/datatypes.cmx theories/Init/peano.cmi +theories/Init/prelude.cmo: theories/Init/prelude.cmi +theories/Init/prelude.cmx: theories/Init/prelude.cmi +theories/Init/specif.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Init/specif.cmx: theories/Init/datatypes.cmx \ + theories/Init/specif.cmi +theories/Init/specifSyntax.cmo: theories/Init/specifSyntax.cmi +theories/Init/specifSyntax.cmx: theories/Init/specifSyntax.cmi +theories/Init/wf.cmo: theories/Init/wf.cmi +theories/Init/wf.cmx: theories/Init/wf.cmi +theories/IntMap/adalloc.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/adalloc.cmi theories/IntMap/adalloc.cmx: theories/IntMap/addec.cmx \ theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/IntMap/map.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/IntMap/addec.cmo: theories/IntMap/addr.cmo \ - theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/adalloc.cmi +theories/IntMap/addec.cmo: theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/addec.cmi theories/IntMap/addec.cmx: theories/IntMap/addr.cmx \ theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/IntMap/addr.cmo: theories/Bool/bool.cmo theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/specif.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/addec.cmi +theories/IntMap/addr.cmo: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/IntMap/addr.cmi theories/IntMap/addr.cmx: theories/Bool/bool.cmx theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/specif.cmx -theories/IntMap/adist.cmo: theories/IntMap/addr.cmo \ - theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \ - theories/Arith/min.cmo + theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ + theories/IntMap/addr.cmi +theories/IntMap/adist.cmo: theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/Arith/min.cmi theories/IntMap/adist.cmi theories/IntMap/adist.cmx: theories/IntMap/addr.cmx \ theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \ - theories/Arith/min.cmx -theories/IntMap/fset.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \ - theories/Init/datatypes.cmo theories/IntMap/map.cmo \ - theories/Init/specif.cmo + theories/Arith/min.cmx theories/IntMap/adist.cmi +theories/IntMap/allmaps.cmo: theories/IntMap/allmaps.cmi +theories/IntMap/allmaps.cmx: theories/IntMap/allmaps.cmi +theories/IntMap/fset.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/IntMap/fset.cmi theories/IntMap/fset.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ theories/Init/datatypes.cmx theories/IntMap/map.cmx \ - theories/Init/specif.cmx -theories/IntMap/lsort.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \ - theories/Bool/bool.cmo theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/IntMap/mapiter.cmo \ - theories/Lists/polyList.cmo theories/Init/specif.cmo \ - theories/Bool/sumbool.cmo + theories/Init/specif.cmx theories/IntMap/fset.cmi +theories/IntMap/lsort.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/IntMap/mapiter.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi theories/IntMap/lsort.cmi theories/IntMap/lsort.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ theories/Bool/bool.cmx theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/IntMap/mapiter.cmx \ theories/Lists/polyList.cmx theories/Init/specif.cmx \ - theories/Bool/sumbool.cmx -theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmo -theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx -theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmo \ - theories/IntMap/addr.cmo theories/Init/datatypes.cmo \ - theories/IntMap/map.cmo theories/Init/peano.cmo \ - theories/Arith/peano_dec.cmo theories/Arith/plus.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo + theories/Bool/sumbool.cmx theories/IntMap/lsort.cmi +theories/IntMap/map.cmo: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi theories/IntMap/map.cmi +theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ + theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \ + theories/Init/peano.cmx theories/Init/specif.cmx theories/IntMap/map.cmi +theories/IntMap/mapaxioms.cmo: theories/IntMap/mapaxioms.cmi +theories/IntMap/mapaxioms.cmx: theories/IntMap/mapaxioms.cmi +theories/IntMap/mapc.cmo: theories/IntMap/mapc.cmi +theories/IntMap/mapc.cmx: theories/IntMap/mapc.cmi +theories/IntMap/mapcanon.cmo: theories/IntMap/map.cmi \ + theories/IntMap/mapcanon.cmi +theories/IntMap/mapcanon.cmx: theories/IntMap/map.cmx \ + theories/IntMap/mapcanon.cmi +theories/IntMap/mapcard.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/map.cmi theories/Init/peano.cmi \ + theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/mapcard.cmi theories/IntMap/mapcard.cmx: theories/IntMap/addec.cmx \ theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ theories/IntMap/map.cmx theories/Init/peano.cmx \ theories/Arith/peano_dec.cmx theories/Arith/plus.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/IntMap/mapfold.cmo: theories/Init/datatypes.cmo \ - theories/IntMap/fset.cmo theories/IntMap/map.cmo \ - theories/IntMap/mapiter.cmo theories/Init/specif.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/mapcard.cmi +theories/IntMap/mapfold.cmo: theories/Init/datatypes.cmi \ + theories/IntMap/fset.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Init/specif.cmi \ + theories/IntMap/mapfold.cmi theories/IntMap/mapfold.cmx: theories/Init/datatypes.cmx \ theories/IntMap/fset.cmx theories/IntMap/map.cmx \ - theories/IntMap/mapiter.cmx theories/Init/specif.cmx -theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmo \ - theories/IntMap/addr.cmo theories/Init/datatypes.cmo \ - theories/IntMap/map.cmo theories/Lists/polyList.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo + theories/IntMap/mapiter.cmx theories/Init/specif.cmx \ + theories/IntMap/mapfold.cmi +theories/IntMap/mapiter.cmo: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/map.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/mapiter.cmi theories/IntMap/mapiter.cmx: theories/IntMap/addec.cmx \ theories/IntMap/addr.cmx theories/Init/datatypes.cmx \ theories/IntMap/map.cmx theories/Lists/polyList.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/IntMap/maplists.cmo: theories/IntMap/addec.cmo \ - theories/Init/datatypes.cmo theories/IntMap/map.cmo \ - theories/IntMap/mapiter.cmo theories/Lists/polyList.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/mapiter.cmi +theories/IntMap/maplists.cmo: theories/IntMap/addec.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/IntMap/maplists.cmi theories/IntMap/maplists.cmx: theories/IntMap/addec.cmx \ theories/Init/datatypes.cmx theories/IntMap/map.cmx \ theories/IntMap/mapiter.cmx theories/Lists/polyList.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/IntMap/map.cmo: theories/IntMap/addec.cmo theories/IntMap/addr.cmo \ - theories/Init/datatypes.cmo theories/ZArith/fast_integer.cmo \ - theories/Init/peano.cmo theories/Init/specif.cmo -theories/IntMap/map.cmx: theories/IntMap/addec.cmx theories/IntMap/addr.cmx \ - theories/Init/datatypes.cmx theories/ZArith/fast_integer.cmx \ - theories/Init/peano.cmx theories/Init/specif.cmx -theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmo \ - theories/Init/datatypes.cmo theories/IntMap/fset.cmo \ - theories/IntMap/map.cmo theories/IntMap/mapiter.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/IntMap/maplists.cmi +theories/IntMap/mapsubset.cmo: theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi \ + theories/IntMap/mapsubset.cmi theories/IntMap/mapsubset.cmx: theories/Bool/bool.cmx \ theories/Init/datatypes.cmx theories/IntMap/fset.cmx \ - theories/IntMap/map.cmx theories/IntMap/mapiter.cmx -theories/Lists/listSet.cmo: theories/Init/datatypes.cmo \ - theories/Lists/polyList.cmo theories/Init/specif.cmo + theories/IntMap/map.cmx theories/IntMap/mapiter.cmx \ + theories/IntMap/mapsubset.cmi +theories/Lists/listSet.cmo: theories/Init/datatypes.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Lists/listSet.cmi theories/Lists/listSet.cmx: theories/Init/datatypes.cmx \ - theories/Lists/polyList.cmx theories/Init/specif.cmx -theories/Lists/polyList.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Lists/polyList.cmx theories/Init/specif.cmx \ + theories/Lists/listSet.cmi +theories/Lists/polyList.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Lists/polyList.cmi theories/Lists/polyList.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Lists/streams.cmo: theories/Init/datatypes.cmo -theories/Lists/streams.cmx: theories/Init/datatypes.cmx -theories/Lists/theoryList.cmo: theories/Init/datatypes.cmo \ - theories/Lists/polyList.cmo theories/Init/specif.cmo + theories/Init/specif.cmx theories/Lists/polyList.cmi +theories/Lists/polyListSyntax.cmo: theories/Lists/polyListSyntax.cmi +theories/Lists/polyListSyntax.cmx: theories/Lists/polyListSyntax.cmi +theories/Lists/streams.cmo: theories/Init/datatypes.cmi \ + theories/Lists/streams.cmi +theories/Lists/streams.cmx: theories/Init/datatypes.cmx \ + theories/Lists/streams.cmi +theories/Lists/theoryList.cmo: theories/Init/datatypes.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Lists/theoryList.cmi theories/Lists/theoryList.cmx: theories/Init/datatypes.cmx \ - theories/Lists/polyList.cmx theories/Init/specif.cmx -theories/Relations/relation_Operators.cmo: theories/Lists/polyList.cmo \ - theories/Init/specif.cmo + theories/Lists/polyList.cmx theories/Init/specif.cmx \ + theories/Lists/theoryList.cmi +theories/Logic/berardi.cmo: theories/Logic/berardi.cmi +theories/Logic/berardi.cmx: theories/Logic/berardi.cmi +theories/Logic/classical.cmo: theories/Logic/classical.cmi +theories/Logic/classical.cmx: theories/Logic/classical.cmi +theories/Logic/classical_Pred_Set.cmo: theories/Logic/classical_Pred_Set.cmi +theories/Logic/classical_Pred_Set.cmx: theories/Logic/classical_Pred_Set.cmi +theories/Logic/classical_Pred_Type.cmo: \ + theories/Logic/classical_Pred_Type.cmi +theories/Logic/classical_Pred_Type.cmx: \ + theories/Logic/classical_Pred_Type.cmi +theories/Logic/classical_Prop.cmo: theories/Logic/classical_Prop.cmi +theories/Logic/classical_Prop.cmx: theories/Logic/classical_Prop.cmi +theories/Logic/classical_Type.cmo: theories/Logic/classical_Type.cmi +theories/Logic/classical_Type.cmx: theories/Logic/classical_Type.cmi +theories/Logic/decidable.cmo: theories/Logic/decidable.cmi +theories/Logic/decidable.cmx: theories/Logic/decidable.cmi +theories/Logic/eqdep.cmo: theories/Logic/eqdep.cmi +theories/Logic/eqdep.cmx: theories/Logic/eqdep.cmi +theories/Logic/eqdep_dec.cmo: theories/Logic/eqdep_dec.cmi +theories/Logic/eqdep_dec.cmx: theories/Logic/eqdep_dec.cmi +theories/Logic/hurkens.cmo: theories/Logic/hurkens.cmi +theories/Logic/hurkens.cmx: theories/Logic/hurkens.cmi +theories/Logic/jMeq.cmo: theories/Logic/jMeq.cmi +theories/Logic/jMeq.cmx: theories/Logic/jMeq.cmi +theories/Logic/proofIrrelevance.cmo: theories/Logic/proofIrrelevance.cmi +theories/Logic/proofIrrelevance.cmx: theories/Logic/proofIrrelevance.cmi +theories/Relations/newman.cmo: theories/Relations/newman.cmi +theories/Relations/newman.cmx: theories/Relations/newman.cmi +theories/Relations/operators_Properties.cmo: \ + theories/Relations/operators_Properties.cmi +theories/Relations/operators_Properties.cmx: \ + theories/Relations/operators_Properties.cmi +theories/Relations/relation_Definitions.cmo: \ + theories/Relations/relation_Definitions.cmi +theories/Relations/relation_Definitions.cmx: \ + theories/Relations/relation_Definitions.cmi +theories/Relations/relation_Operators.cmo: theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Relations/relation_Operators.cmi theories/Relations/relation_Operators.cmx: theories/Lists/polyList.cmx \ - theories/Init/specif.cmx -theories/Sets/cpo.cmo: theories/Sets/partial_Order.cmo -theories/Sets/cpo.cmx: theories/Sets/partial_Order.cmx -theories/Sets/integers.cmo: theories/Sets/partial_Order.cmo -theories/Sets/integers.cmx: theories/Sets/partial_Order.cmx -theories/Sets/multiset.cmo: theories/Init/datatypes.cmo \ - theories/Init/peano.cmo theories/Init/specif.cmo + theories/Init/specif.cmx theories/Relations/relation_Operators.cmi +theories/Relations/relations.cmo: theories/Relations/relations.cmi +theories/Relations/relations.cmx: theories/Relations/relations.cmi +theories/Relations/rstar.cmo: theories/Relations/rstar.cmi +theories/Relations/rstar.cmx: theories/Relations/rstar.cmi +theories/Setoids/setoid.cmo: theories/Setoids/setoid.cmi +theories/Setoids/setoid.cmx: theories/Setoids/setoid.cmi +theories/Sets/classical_sets.cmo: theories/Sets/classical_sets.cmi +theories/Sets/classical_sets.cmx: theories/Sets/classical_sets.cmi +theories/Sets/constructive_sets.cmo: theories/Sets/constructive_sets.cmi +theories/Sets/constructive_sets.cmx: theories/Sets/constructive_sets.cmi +theories/Sets/cpo.cmo: theories/Sets/partial_Order.cmi theories/Sets/cpo.cmi +theories/Sets/cpo.cmx: theories/Sets/partial_Order.cmx theories/Sets/cpo.cmi +theories/Sets/ensembles.cmo: theories/Sets/ensembles.cmi +theories/Sets/ensembles.cmx: theories/Sets/ensembles.cmi +theories/Sets/finite_sets.cmo: theories/Sets/finite_sets.cmi +theories/Sets/finite_sets.cmx: theories/Sets/finite_sets.cmi +theories/Sets/finite_sets_facts.cmo: theories/Sets/finite_sets_facts.cmi +theories/Sets/finite_sets_facts.cmx: theories/Sets/finite_sets_facts.cmi +theories/Sets/image.cmo: theories/Sets/image.cmi +theories/Sets/image.cmx: theories/Sets/image.cmi +theories/Sets/infinite_sets.cmo: theories/Sets/infinite_sets.cmi +theories/Sets/infinite_sets.cmx: theories/Sets/infinite_sets.cmi +theories/Sets/integers.cmo: theories/Sets/partial_Order.cmi \ + theories/Sets/integers.cmi +theories/Sets/integers.cmx: theories/Sets/partial_Order.cmx \ + theories/Sets/integers.cmi +theories/Sets/multiset.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi \ + theories/Sets/multiset.cmi theories/Sets/multiset.cmx: theories/Init/datatypes.cmx \ - theories/Init/peano.cmx theories/Init/specif.cmx -theories/Sets/partial_Order.cmo: theories/Sets/ensembles.cmo \ - theories/Sets/relations_1.cmo -theories/Sets/partial_Order.cmx: theories/Sets/ensembles.cmx \ - theories/Sets/relations_1.cmx -theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmo -theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx -theories/Sets/uniset.cmo: theories/Init/datatypes.cmo \ - theories/Init/specif.cmo + theories/Init/peano.cmx theories/Init/specif.cmx \ + theories/Sets/multiset.cmi +theories/Sets/partial_Order.cmo: theories/Sets/partial_Order.cmi +theories/Sets/partial_Order.cmx: theories/Sets/partial_Order.cmi +theories/Sets/permut.cmo: theories/Sets/permut.cmi +theories/Sets/permut.cmx: theories/Sets/permut.cmi +theories/Sets/powerset.cmo: theories/Sets/partial_Order.cmi \ + theories/Sets/powerset.cmi +theories/Sets/powerset.cmx: theories/Sets/partial_Order.cmx \ + theories/Sets/powerset.cmi +theories/Sets/powerset_Classical_facts.cmo: \ + theories/Sets/powerset_Classical_facts.cmi +theories/Sets/powerset_Classical_facts.cmx: \ + theories/Sets/powerset_Classical_facts.cmi +theories/Sets/powerset_facts.cmo: theories/Sets/powerset_facts.cmi +theories/Sets/powerset_facts.cmx: theories/Sets/powerset_facts.cmi +theories/Sets/relations_1.cmo: theories/Sets/relations_1.cmi +theories/Sets/relations_1.cmx: theories/Sets/relations_1.cmi +theories/Sets/relations_1_facts.cmo: theories/Sets/relations_1_facts.cmi +theories/Sets/relations_1_facts.cmx: theories/Sets/relations_1_facts.cmi +theories/Sets/relations_2.cmo: theories/Sets/relations_2.cmi +theories/Sets/relations_2.cmx: theories/Sets/relations_2.cmi +theories/Sets/relations_2_facts.cmo: theories/Sets/relations_2_facts.cmi +theories/Sets/relations_2_facts.cmx: theories/Sets/relations_2_facts.cmi +theories/Sets/relations_3.cmo: theories/Sets/relations_3.cmi +theories/Sets/relations_3.cmx: theories/Sets/relations_3.cmi +theories/Sets/relations_3_facts.cmo: theories/Sets/relations_3_facts.cmi +theories/Sets/relations_3_facts.cmx: theories/Sets/relations_3_facts.cmi +theories/Sets/uniset.cmo: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi theories/Sets/uniset.cmi theories/Sets/uniset.cmx: theories/Init/datatypes.cmx \ - theories/Init/specif.cmx -theories/Sorting/heap.cmo: theories/Init/datatypes.cmo \ - theories/Init/peano.cmo theories/Lists/polyList.cmo \ - theories/Sorting/sorting.cmo theories/Init/specif.cmo + theories/Init/specif.cmx theories/Sets/uniset.cmi +theories/Sorting/heap.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Lists/polyList.cmi \ + theories/Sorting/sorting.cmi theories/Init/specif.cmi \ + theories/Sorting/heap.cmi theories/Sorting/heap.cmx: theories/Init/datatypes.cmx \ theories/Init/peano.cmx theories/Lists/polyList.cmx \ - theories/Sorting/sorting.cmx theories/Init/specif.cmx -theories/Sorting/permutation.cmo: theories/Init/datatypes.cmo \ - theories/Init/peano.cmo theories/Lists/polyList.cmo \ - theories/Init/specif.cmo + theories/Sorting/sorting.cmx theories/Init/specif.cmx \ + theories/Sorting/heap.cmi +theories/Sorting/permutation.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Sorting/permutation.cmi theories/Sorting/permutation.cmx: theories/Init/datatypes.cmx \ theories/Init/peano.cmx theories/Lists/polyList.cmx \ - theories/Init/specif.cmx -theories/Sorting/sorting.cmo: theories/Lists/polyList.cmo \ - theories/Init/specif.cmo + theories/Init/specif.cmx theories/Sorting/permutation.cmi +theories/Sorting/sorting.cmo: theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Sorting/sorting.cmi theories/Sorting/sorting.cmx: theories/Lists/polyList.cmx \ - theories/Init/specif.cmx -theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmo -theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx -theories/ZArith/fast_integer.cmo: theories/Init/datatypes.cmo \ - theories/Init/peano.cmo + theories/Init/specif.cmx theories/Sorting/sorting.cmi +theories/Wellfounded/disjoint_Union.cmo: \ + theories/Wellfounded/disjoint_Union.cmi +theories/Wellfounded/disjoint_Union.cmx: \ + theories/Wellfounded/disjoint_Union.cmi +theories/Wellfounded/inclusion.cmo: theories/Wellfounded/inclusion.cmi +theories/Wellfounded/inclusion.cmx: theories/Wellfounded/inclusion.cmi +theories/Wellfounded/inverse_Image.cmo: \ + theories/Wellfounded/inverse_Image.cmi +theories/Wellfounded/inverse_Image.cmx: \ + theories/Wellfounded/inverse_Image.cmi +theories/Wellfounded/lexicographic_Exponentiation.cmo: \ + theories/Wellfounded/lexicographic_Exponentiation.cmi +theories/Wellfounded/lexicographic_Exponentiation.cmx: \ + theories/Wellfounded/lexicographic_Exponentiation.cmi +theories/Wellfounded/lexicographic_Product.cmo: \ + theories/Wellfounded/lexicographic_Product.cmi +theories/Wellfounded/lexicographic_Product.cmx: \ + theories/Wellfounded/lexicographic_Product.cmi +theories/Wellfounded/transitive_Closure.cmo: \ + theories/Wellfounded/transitive_Closure.cmi +theories/Wellfounded/transitive_Closure.cmx: \ + theories/Wellfounded/transitive_Closure.cmi +theories/Wellfounded/union.cmo: theories/Wellfounded/union.cmi +theories/Wellfounded/union.cmx: theories/Wellfounded/union.cmi +theories/Wellfounded/well_Ordering.cmo: theories/Init/specif.cmi \ + theories/Wellfounded/well_Ordering.cmi +theories/Wellfounded/well_Ordering.cmx: theories/Init/specif.cmx \ + theories/Wellfounded/well_Ordering.cmi +theories/Wellfounded/wellfounded.cmo: theories/Wellfounded/wellfounded.cmi +theories/Wellfounded/wellfounded.cmx: theories/Wellfounded/wellfounded.cmi +theories/ZArith/auxiliary.cmo: theories/ZArith/auxiliary.cmi +theories/ZArith/auxiliary.cmx: theories/ZArith/auxiliary.cmi +theories/ZArith/fast_integer.cmo: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/ZArith/fast_integer.cmi theories/ZArith/fast_integer.cmx: theories/Init/datatypes.cmx \ - theories/Init/peano.cmx -theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/peano.cmo \ - theories/ZArith/zarith_aux.cmo + theories/Init/peano.cmx theories/ZArith/fast_integer.cmi +theories/ZArith/wf_Z.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/peano.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/wf_Z.cmi theories/ZArith/wf_Z.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/Init/peano.cmx \ - theories/ZArith/zarith_aux.cmx -theories/ZArith/zarith_aux.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/specif.cmo -theories/ZArith/zarith_aux.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/specif.cmx -theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmo \ - theories/Init/specif.cmo theories/Bool/sumbool.cmo + theories/ZArith/zarith_aux.cmx theories/ZArith/wf_Z.cmi +theories/ZArith/zArith.cmo: theories/ZArith/zArith.cmi +theories/ZArith/zArith.cmx: theories/ZArith/zArith.cmi +theories/ZArith/zArith_base.cmo: theories/ZArith/zArith_base.cmi +theories/ZArith/zArith_base.cmx: theories/ZArith/zArith_base.cmi +theories/ZArith/zArith_dec.cmo: theories/ZArith/fast_integer.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zArith_dec.cmx: theories/ZArith/fast_integer.cmx \ - theories/Init/specif.cmx theories/Bool/sumbool.cmx -theories/ZArith/zbool.cmo: theories/Bool/sumbool.cmo \ - theories/ZArith/zArith_dec.cmo theories/ZArith/zmisc.cmo + theories/Init/specif.cmx theories/Bool/sumbool.cmx \ + theories/ZArith/zArith_dec.cmi +theories/ZArith/zarith_aux.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/zarith_aux.cmi +theories/ZArith/zarith_aux.cmx: theories/Init/datatypes.cmx \ + theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ + theories/ZArith/zarith_aux.cmi +theories/ZArith/zbool.cmo: theories/Bool/sumbool.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zmisc.cmi \ + theories/ZArith/zbool.cmi theories/ZArith/zbool.cmx: theories/Bool/sumbool.cmx \ - theories/ZArith/zArith_dec.cmx theories/ZArith/zmisc.cmx -theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \ - theories/ZArith/wf_Z.cmo theories/ZArith/zarith_aux.cmo + theories/ZArith/zArith_dec.cmx theories/ZArith/zmisc.cmx \ + theories/ZArith/zbool.cmi +theories/ZArith/zcomplements.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/wf_Z.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zcomplements.cmi theories/ZArith/zcomplements.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ - theories/ZArith/wf_Z.cmx theories/ZArith/zarith_aux.cmx -theories/ZArith/zdiv.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/specif.cmo \ - theories/ZArith/zArith_dec.cmo theories/ZArith/zarith_aux.cmo \ - theories/ZArith/zmisc.cmo + theories/ZArith/wf_Z.cmx theories/ZArith/zarith_aux.cmx \ + theories/ZArith/zcomplements.cmi +theories/ZArith/zdiv.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zmisc.cmi theories/ZArith/zdiv.cmi theories/ZArith/zdiv.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ theories/ZArith/zArith_dec.cmx theories/ZArith/zarith_aux.cmx \ - theories/ZArith/zmisc.cmx -theories/ZArith/zlogarithm.cmo: theories/ZArith/fast_integer.cmo \ - theories/ZArith/zarith_aux.cmo + theories/ZArith/zmisc.cmx theories/ZArith/zdiv.cmi +theories/ZArith/zhints.cmo: theories/ZArith/zhints.cmi +theories/ZArith/zhints.cmx: theories/ZArith/zhints.cmi +theories/ZArith/zlogarithm.cmo: theories/ZArith/fast_integer.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zlogarithm.cmi theories/ZArith/zlogarithm.cmx: theories/ZArith/fast_integer.cmx \ - theories/ZArith/zarith_aux.cmx -theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/Init/specif.cmo + theories/ZArith/zarith_aux.cmx theories/ZArith/zlogarithm.cmi +theories/ZArith/zmisc.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/zmisc.cmi theories/ZArith/zmisc.cmx: theories/Init/datatypes.cmx \ - theories/ZArith/fast_integer.cmx theories/Init/specif.cmx -theories/ZArith/zpower.cmo: theories/Init/datatypes.cmo \ - theories/ZArith/fast_integer.cmo theories/ZArith/zarith_aux.cmo \ - theories/ZArith/zmisc.cmo + theories/ZArith/fast_integer.cmx theories/Init/specif.cmx \ + theories/ZArith/zmisc.cmi +theories/ZArith/zpower.cmo: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zmisc.cmi theories/ZArith/zpower.cmi theories/ZArith/zpower.cmx: theories/Init/datatypes.cmx \ theories/ZArith/fast_integer.cmx theories/ZArith/zarith_aux.cmx \ - theories/ZArith/zmisc.cmx -theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmo \ - theories/Init/specif.cmo theories/ZArith/zArith_dec.cmo \ - theories/ZArith/zarith_aux.cmo + theories/ZArith/zmisc.cmx theories/ZArith/zpower.cmi +theories/ZArith/zsqrt.cmo: theories/ZArith/fast_integer.cmi \ + theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/zarith_aux.cmi theories/ZArith/zsqrt.cmi theories/ZArith/zsqrt.cmx: theories/ZArith/fast_integer.cmx \ theories/Init/specif.cmx theories/ZArith/zArith_dec.cmx \ - theories/ZArith/zarith_aux.cmx + theories/ZArith/zarith_aux.cmx theories/ZArith/zsqrt.cmi +theories/ZArith/zwf.cmo: theories/ZArith/zwf.cmi +theories/ZArith/zwf.cmx: theories/ZArith/zwf.cmi +theories/Arith/bool_nat.cmi: theories/Arith/compare_dec.cmi \ + theories/Arith/peano_dec.cmi theories/Bool/sumbool.cmi +theories/Arith/compare.cmi: theories/Arith/compare_dec.cmi \ + theories/Init/specif.cmi +theories/Arith/compare_dec.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Arith/div2.cmi: theories/Init/datatypes.cmi theories/Init/peano.cmi +theories/Arith/eqNat.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Arith/euclid.cmi: theories/Arith/compare_dec.cmi \ + theories/Init/datatypes.cmi theories/Arith/minus.cmi \ + theories/Init/specif.cmi +theories/Arith/even.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/max.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/min.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/minus.cmi: theories/Init/datatypes.cmi +theories/Arith/mult.cmi: theories/Init/datatypes.cmi theories/Arith/plus.cmi +theories/Arith/peano_dec.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Arith/plus.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Arith/wf_nat.cmi: theories/Init/datatypes.cmi +theories/Bool/bool.cmi: theories/Init/datatypes.cmi theories/Init/specif.cmi +theories/Bool/boolEq.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Bool/decBool.cmi: theories/Init/specif.cmi +theories/Bool/ifProp.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Bool/sumbool.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Bool/zerob.cmi: theories/Init/datatypes.cmi +theories/Init/peano.cmi: theories/Init/datatypes.cmi +theories/Init/specif.cmi: theories/Init/datatypes.cmi +theories/IntMap/adalloc.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/addec.cmi: theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/addr.cmi: theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi +theories/IntMap/adist.cmi: theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/Arith/min.cmi +theories/IntMap/fset.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/Init/specif.cmi +theories/IntMap/lsort.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Bool/bool.cmi theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/IntMap/mapiter.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi \ + theories/Bool/sumbool.cmi +theories/IntMap/map.cmi: theories/IntMap/addec.cmi theories/IntMap/addr.cmi \ + theories/Init/datatypes.cmi theories/ZArith/fast_integer.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi +theories/IntMap/mapcanon.cmi: theories/IntMap/map.cmi +theories/IntMap/mapcard.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/map.cmi theories/Init/peano.cmi \ + theories/Arith/peano_dec.cmi theories/Arith/plus.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/mapfold.cmi: theories/Init/datatypes.cmi \ + theories/IntMap/fset.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Init/specif.cmi +theories/IntMap/mapiter.cmi: theories/IntMap/addec.cmi \ + theories/IntMap/addr.cmi theories/Init/datatypes.cmi \ + theories/IntMap/map.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/maplists.cmi: theories/IntMap/addec.cmi \ + theories/Init/datatypes.cmi theories/IntMap/map.cmi \ + theories/IntMap/mapiter.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/IntMap/mapsubset.cmi: theories/Bool/bool.cmi \ + theories/Init/datatypes.cmi theories/IntMap/fset.cmi \ + theories/IntMap/map.cmi theories/IntMap/mapiter.cmi +theories/Lists/listSet.cmi: theories/Init/datatypes.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi +theories/Lists/polyList.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Lists/streams.cmi: theories/Init/datatypes.cmi +theories/Lists/theoryList.cmi: theories/Init/datatypes.cmi \ + theories/Lists/polyList.cmi theories/Init/specif.cmi +theories/Relations/relation_Operators.cmi: theories/Lists/polyList.cmi \ + theories/Init/specif.cmi +theories/Sets/cpo.cmi: theories/Sets/partial_Order.cmi +theories/Sets/integers.cmi: theories/Sets/partial_Order.cmi +theories/Sets/multiset.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Init/specif.cmi +theories/Sets/powerset.cmi: theories/Sets/partial_Order.cmi +theories/Sets/uniset.cmi: theories/Init/datatypes.cmi \ + theories/Init/specif.cmi +theories/Sorting/heap.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Lists/polyList.cmi \ + theories/Sorting/sorting.cmi theories/Init/specif.cmi +theories/Sorting/permutation.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi theories/Lists/polyList.cmi \ + theories/Init/specif.cmi +theories/Sorting/sorting.cmi: theories/Lists/polyList.cmi \ + theories/Init/specif.cmi +theories/Wellfounded/well_Ordering.cmi: theories/Init/specif.cmi +theories/ZArith/fast_integer.cmi: theories/Init/datatypes.cmi \ + theories/Init/peano.cmi +theories/ZArith/wf_Z.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/peano.cmi \ + theories/ZArith/zarith_aux.cmi +theories/ZArith/zArith_dec.cmi: theories/ZArith/fast_integer.cmi \ + theories/Init/specif.cmi theories/Bool/sumbool.cmi +theories/ZArith/zarith_aux.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi +theories/ZArith/zbool.cmi: theories/Bool/sumbool.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zmisc.cmi +theories/ZArith/zcomplements.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/wf_Z.cmi theories/ZArith/zarith_aux.cmi +theories/ZArith/zdiv.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi \ + theories/ZArith/zArith_dec.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zmisc.cmi +theories/ZArith/zlogarithm.cmi: theories/ZArith/fast_integer.cmi \ + theories/ZArith/zarith_aux.cmi +theories/ZArith/zmisc.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/Init/specif.cmi +theories/ZArith/zpower.cmi: theories/Init/datatypes.cmi \ + theories/ZArith/fast_integer.cmi theories/ZArith/zarith_aux.cmi \ + theories/ZArith/zmisc.cmi +theories/ZArith/zsqrt.cmi: theories/ZArith/fast_integer.cmi \ + theories/Init/specif.cmi theories/ZArith/zArith_dec.cmi \ + theories/ZArith/zarith_aux.cmi diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 844b71a57..646e8b6ba 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -24,22 +24,30 @@ VO:= $(filter-out $(AXIOMSVO),$(VO)) ML:= $(shell test -x v2ml && ./v2ml $(VO)) +MLI:= $(patsubst %.ml,%.mli,$(ML)) + CMO:= $(patsubst %.ml,%.cmo,$(ML)) # # General rules # -all: v2ml ml $(CMO) +all: v2ml ml $(MLI) $(CMO) ml: $(ML) depend: $(ML) - rm -f .depend; ocamldep $(INCL) theories/*/*.ml > .depend + rm -f .depend; ocamldep $(INCL) theories/*/*.ml theories/*/*.mli > .depend tree: mkdir -p $(DIRS) +%.mli:%.ml + ./make_mli $< > $@ + +%.cmi:%.mli + ocamlc $(INCL) -c -i $< + %.cmo:%.ml ocamlc $(INCL) -c -i $< @@ -47,7 +55,7 @@ $(ML): ml2v ./extract $@ clean: - rm -f theories/*/*.ml theories/*/*.cm* theories/*/*.ml.orig + rm -f theories/*/*.ml* theories/*/*.cm* # @@ -61,10 +69,10 @@ undo_open: find theories -name "*".ml -exec mv \{\}.orig \{\} \; ml2v: ml2v.ml - ocamlc -o $@ $< + ocamlopt -o $@ $< v2ml: v2ml.ml - ocamlc -o $@ $< + ocamlopt -o $@ $< $(MAKE) # diff --git a/contrib/extraction/test/make_mli b/contrib/extraction/test/make_mli new file mode 100755 index 000000000..40ee496ea --- /dev/null +++ b/contrib/extraction/test/make_mli @@ -0,0 +1,17 @@ +#!/usr/bin/awk -We $0 + +{ match($0,"^open") + if (RLENGTH>0) state=1 + match($0,"^type") + if (RLENGTH>0) state=1 + match($0,"^\(\*\* ") + if (RLENGTH>0) state=2 + match($0,"^let") + if (RLENGTH>0) state=0 + match($0,"^and") + if ((RLENGTH>0) && (state==2)) state=0 + if ((RLENGTH>0) && (state==1)) state=1 + gsub("\(\*\* ","") + gsub("\*\*\)","") + if (state>0) print +} diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index ad95428f1..70ca40c4f 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -435,4 +435,13 @@ Extraction loop. let rec f a = f (S a) in f O -*)
\ No newline at end of file +*) + +Extraction "test" + nat test1 c test2 test3 test4 test5 test6 test7 + d d2 d3 d4 d5 d6 test8 id' id'' test9 Finite test10 test11 + test12 tree tree_size test13 sumbool_rect predicate test14 + test15 eta_c test16 test17 test18 bidon tb fbidon fbidon2 + fbidon2 test_0 test_1 eq eq_rect test19 tp1 tp1bis test20 + horibilis PropSet natbool zerotrue zeroTrue zeroprop test21 test22 + test23 f f_prop f_arity f_normal Truc oups test24 loop. |