diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/extraction/extraction.ml | 691 | ||||
| -rw-r--r-- | contrib/extraction/extraction.mli | 2 | ||||
| -rw-r--r-- | contrib/extraction/haskell.ml | 6 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.ml | 506 | ||||
| -rw-r--r-- | contrib/extraction/mlutil.mli | 18 | ||||
| -rw-r--r-- | contrib/extraction/ocaml.ml | 6 | ||||
| -rw-r--r-- | contrib/extraction/test_extraction.v | 41 |
7 files changed, 610 insertions, 660 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 58bcd927e..7dc1b4c47 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -8,6 +8,7 @@ (*i $Id$ i*) +(*i*) open Pp open Util open Names @@ -26,8 +27,9 @@ open Mlutil open Closure open Summary open Nametab +(*i*) -(*s Extraction results. *) +(*S Extraction results. *) (* The flag [type_var] gives us information about an identifier coming from a Lambda or a Product: @@ -63,14 +65,6 @@ let default = (Info, NotArity) type signature = type_var list -(* When dealing with CIC contexts, we maintain corresponding contexts - telling whether a variable will be kept or will disappear. - Cf. [renum_db]. *) - -(* Convention: innermost ([Rel 1]) is at the head of the list *) - -type extraction_context = bool list - (* The [type_extraction_result] is the result of the [extract_type] function that extracts a CIC object into an ML type. It is either: \begin{itemize} @@ -84,55 +78,93 @@ type type_extraction_result = | Tarity | Tprop -(* The [term_extraction_result] is the result of the [extract_term] - function that extracts a CIC object into an ML term *) +(* The [indutive_extraction_result] is the dual of [type_extraction_result], + but for inductive types. *) + +type inductive_extraction_result = + | Iml of signature * identifier list + | Iprop -type term_extraction_result = - | Rmlterm of ml_ast - | Rprop +(* 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. *) + +type constructor_extraction_result = + | Cml of ml_type list * signature * int + | Cprop (* The [extraction_result] is the result of the [extract_constr] - function that extracts any CIC object. It is either a ML type, a ML - object or something non-informative. *) + function that extracts any CIC object. It is either a ML type or + a ML object. *) type extraction_result = | Emltype of ml_type * signature * identifier list | Emlterm of ml_ast -(*s Utility functions. *) +(*S Tables to keep the extraction results. *) + +let inductive_table = + ref (Gmap.empty : (inductive, inductive_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) +let add_constructor c e = constructor_table := Gmap.add c e !constructor_table +let lookup_constructor c = Gmap.find c !constructor_table + +let constant_table = + ref (Gmap.empty : (section_path, extraction_result) Gmap.t) +let add_constant sp e = constant_table := Gmap.add sp e !constant_table +let lookup_constant sp = Gmap.find sp !constant_table + +let signature_table = ref (Gmap.empty : (section_path, signature) Gmap.t) +let add_signature sp s = signature_table := Gmap.add sp s !signature_table +let lookup_signature sp = Gmap.find sp !signature_table + +(* Tables synchronization. *) + +let freeze () = + !inductive_table, !constructor_table, !constant_table, !signature_table + +let unfreeze (it,cst,ct,st) = + inductive_table := it; constructor_table := cst; + constant_table := ct; signature_table := st + +let _ = declare_summary "Extraction tables" + { freeze_function = freeze; + unfreeze_function = unfreeze; + init_function = (fun () -> ()); + survive_section = true } + +(*S Utility functions. *) let none = Evd.empty -let type_of env c = Retyping.get_type_of env Evd.empty (strip_outer_cast c) +let type_of env c = Retyping.get_type_of env none (strip_outer_cast c) -let sort_of env c = - Retyping.get_sort_family_of env Evd.empty (strip_outer_cast c) +let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c) open RedFlags -let whd_betaiotalet = clos_norm_flags (mkflags [fBETA;fIOTA;fZETA]) +let betaiotazeta = clos_norm_flags (mkflags [fBETA;fIOTA;fZETA]) +(* TODO: verifier si c'est bien de la réduction de tete... *) let is_axiom sp = (Global.lookup_constant sp).const_body = None type lamprod = Lam | Product -let flexible_name = id_of_string "flex" - -let id_of_name = function - | Anonymous -> id_of_string "x" - | Name id -> id - -(* [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t] +(*s [list_of_ml_arrows] applied to the ML type [a->b->]\dots[z->t] returns the list [[a;b;...;z]]. It is used when making the ML types - of inductive definitions. We also suppress [Prop] parts. *) + of inductive definitions. We also suppress [prop] and [arity] parts. *) let rec list_of_ml_arrows = function - | Tarr (Miniml.Tarity, b) -> assert false + | Tarr (Miniml.Tarity, b) -> list_of_ml_arrows b | Tarr (Miniml.Tprop, b) -> list_of_ml_arrows b | Tarr (a, b) -> a :: list_of_ml_arrows b | t -> [] (*s [get_arity c] returns [Some s] if [c] is an arity of sort [s], - and [None] otherwise. *) + and [None] otherwise. *) let rec get_arity env c = match kind_of_term (whd_betadeltaiota env none c) with @@ -141,49 +173,21 @@ let rec get_arity env c = | Sort s -> Some (family_of_sort s) | _ -> None -(* idem, but goes through [Lambda] as well. Cf. [find_conclusion]. *) - -let rec get_lam_arity env c = - match kind_of_term (whd_betadeltaiota env none c) with - | Lambda (x,t,c0) -> get_lam_arity (push_rel (x,None,t) env) c0 - | Prod (x,t,c0) -> get_lam_arity (push_rel (x,None,t) env) c0 - | Cast (t,_) -> get_lam_arity env t - | Sort s -> Some (family_of_sort s) - | _ -> None - -(*s Detection of non-informative parts. *) - -let is_non_info_sort env s = is_Prop (whd_betadeltaiota env none s) - -let is_non_info_type env t = - (sort_of env t) = InProp || (get_arity env t) = Some InProp - -(*i This one is not used, left only to precise what we call a non-informative - term. - -let is_non_info_term env c = - let t = type_of env c in - let s = sort_of env t in - (s <> InProp) || - match get_arity env t with - | Some InProp -> true - | Some InType -> (get_lam_arity env c = Some InProp) - | _ -> false -i*) - -(* [v_of_t] transforms a type [t] into a [type_var] flag. *) +(*s [v_of_t] transforms a type [t] into a [type_var] flag. + Really important function. *) let v_of_t env t = match get_arity env t with | Some InProp -> logic_arity | Some _ -> info_arity - | _ -> if is_non_info_type env t then logic else default + | None when (sort_of env t) = InProp -> logic + | None -> default -(*s Operations on binders *) +(*S Operations on binders. *) type binders = (name * constr) list (* Convention: right binders give [Rel 1] at the head, like those answered by - [decompose_prod]. Left binders are the converse. *) + [decompose_prod]. Left binders are the converse, like [signature]. *) let rec lbinders_fold f acc env = function | [] -> acc @@ -191,7 +195,7 @@ let rec lbinders_fold f acc env = function f n t (v_of_t env t) (lbinders_fold f acc (push_rel_assum b env) l) -(* [sign_of_arity] transforms an arity into a signature. It is used +(*s [sign_of_arity] transforms an arity into a signature. It is used for example with the types of inductive definitions, which are known to be already in arity form. *) @@ -200,91 +204,70 @@ let sign_of_lbinders = lbinders_fold (fun _ _ v a -> v::a) [] let sign_of_arity env c = sign_of_lbinders env (List.rev (fst (decompose_prod c))) -(* [vl_of_arity] returns the list of the lambda variables tagged [info_arity] +(*s [vl_of_arity] returns the list of the lambda variables tagged [info_arity] in an arity. Renaming is done. *) let vl_of_lbinders = - lbinders_fold - (fun n _ v a -> - if v = info_arity - then (next_ident_away (id_of_name n) (prop_name::a))::a - else a) [] + let f n _ v a = if v <> info_arity then a + else (next_ident_away (id_of_name n) a) :: a + in lbinders_fold f [] let vl_of_arity env c = vl_of_lbinders env (List.rev (fst (decompose_prod c))) -(*s [renum_db] gives the new de Bruijn indices for variables in an ML - term. This translation is made according to an [extraction_context]. *) - -let renum_db ctx n = - let rec renum = function - | (1, true :: _) -> 1 - | (n, true :: s) -> succ (renum (pred n, s)) - | (n, false :: s) -> renum (pred n, s) - | _ -> assert false - in - renum (n, ctx) - -(*s Decomposition of a function expecting n arguments at least. We eta-expanse - if needed *) - -let force_n_prod n env c = - if nb_prod c < n then whd_betadeltaiota env none c else c - -let decompose_lam_eta n env c = - let dif = n - (nb_lam c) in - if dif <= 0 then - decompose_lam_n n c - else - let t = type_of env c in - let (trb,_) = decompose_prod_n n (force_n_prod n env t) in - let (rb, e) = decompose_lam c in - let rb = (list_firstn dif trb) @ rb in - let e = applist (lift dif e, List.rev_map mkRel (interval 1 dif)) in - (rb, e) - -(*s TODO commentaires *) +(*S Modification of the signature of terms. *) -let prop_abstract_1 f = +(* We sometimes want to suppress [prop] and [arity] 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] + below. By the way we do some eta-expansion if needed using + [expansion_prop_eta]. + \end{itemize} + To ensure correction of execution, we then need to reintroduce + [prop] and [arity] 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) + | (_,Arity) :: l -> abs (prop_name :: ids) (MLarity :: rels) (succ i) l + | (Logic,_) :: l -> abs (prop_name :: ids) (MLprop :: rels) (succ i) l + | (Info,_) :: l -> abs (anonymous :: ids) (MLrel i :: rels) (succ i) l + in abs ids [] 1 s + +let kill_all_prop_lams_eta e s = + let m = List.length s in + let n = nb_lams e in + let p = if m <= n then collect_n_lams m e + else expansion_prop_eta (snd (list_chop n s)) (collect_lams e) in + kill_some_lams (List.rev_map ((=) default) s) p + +let kill_prop_lams_eta e s = + let ids,e = kill_all_prop_lams_eta e s in + if ids = [] then MLlam (prop_name, ml_lift 1 e) + else named_lams ids e + +(*s Auxiliary function for [abstract_constant] and [abstract_constructor]. *) + +let prop_abstract f = let rec abs rels i = function | [] -> f (List.rev_map (fun x -> MLrel (i-x)) rels) - | (_,Arity) :: l -> abs rels i l + | ((_,Arity)|(Logic,_)) :: l -> MLlam (prop_name, abs rels (succ i) l) | (Info,_) :: l -> MLlam (anonymous, abs (i :: rels) (succ i) l) - | (Logic,_) :: l -> MLlam (prop_name, abs rels (succ i) l) in abs [] 1 - -let prop_abstract_2 f = - let rec abs rels i = function - | [] -> f i (List.rev_map (function MLrel x -> MLrel (i-x) | a -> a) rels) - | (_,Arity) :: l -> abs rels i l - | (Info,_) :: l -> MLlam (anonymous, abs (MLrel i :: rels) (succ i) l) - | (Logic,_) :: l -> MLlam (prop_name, abs (MLprop :: rels) (succ i) l) - in abs [] 1 - (*s Abstraction of an constant. *) -let abstract_const sp s = - if List.mem default s then - prop_abstract_1 (fun a -> MLapp(MLglob (ConstRef sp), a)) s - else MLglob (ConstRef sp) - -(*s The opposite function. *) - -let eta_expanse_w_prop e s = - let s = List.filter (function (_,NotArity) -> true | _ -> false) s in - let ids,e = collect_lams e in - let m = List.length ids in - assert (m <= (List.length s)); - let _,s = list_chop m s in - let core = if s <> [] then - prop_abstract_2 (fun i a -> MLapp (ml_lift (i-1) e,a)) s - else e - in let new_e = named_lams core ids in - try - let new_e,_,_ = kill_prop_aux new_e in new_e - with Impossible -> new_e - -(*s Error message when extraction ends on an axiom. *) +let abstract_constant sp s = + let f a = + if List.mem default s then MLapp (MLglob (ConstRef sp), a) + else MLapp (MLglob (ConstRef sp), [MLprop]) (* or MLarity, I don't mind *) + in prop_abstract f s + +(*S Error messages. *) let axiom_message sp = errorlabstrm "axiom_message" @@ -295,58 +278,7 @@ let section_message () = errorlabstrm "section_message" (str "You can't extract within a section. Close it and try again.") -(*s Tables to keep the extraction of inductive types and constructors. *) - -type inductive_extraction_result = - | Iml of signature * identifier list - | Iprop - -let inductive_extraction_table = - ref (Gmap.empty : (inductive, inductive_extraction_result) Gmap.t) - -let add_inductive_extraction i e = - inductive_extraction_table := Gmap.add i e !inductive_extraction_table - -let lookup_inductive_extraction i = Gmap.find i !inductive_extraction_table - -type constructor_extraction_result = - | Cml of ml_type list * signature * int - | Cprop - -let constructor_extraction_table = - ref (Gmap.empty : (constructor, constructor_extraction_result) Gmap.t) - -let add_constructor_extraction c e = - constructor_extraction_table := Gmap.add c e !constructor_extraction_table - -let lookup_constructor_extraction i = Gmap.find i !constructor_extraction_table - -let constant_table = - ref (Gmap.empty : (section_path, extraction_result) Gmap.t) - -let signature_table = - ref (Gmap.empty : (section_path, signature) Gmap.t) - -(* Tables synchronization. *) - -let freeze () = - !inductive_extraction_table, !constructor_extraction_table, - !constant_table, !signature_table - -let unfreeze (it,cst,ct,st) = - inductive_extraction_table := it; - constructor_extraction_table := cst; - constant_table := ct; - signature_table := st - -let _ = declare_summary "Extraction tables" - { freeze_function = freeze; - unfreeze_function = unfreeze; - init_function = (fun () -> ()); - survive_section = true } - - -(*s Extraction of a type. *) +(*S Extraction of a type. *) (* When calling [extract_type] we suppose that the type of [c] is an arity. This is for example checked in [extract_constr]. *) @@ -373,18 +305,18 @@ let rec extract_type env c = and extract_type_rec env c vl args = (* We accumulate the context, arguments and generated variables list *) let t = type_of env (applist (c, args)) in - (* Since [t] is an arity, there is two non-informative case: - [t] is an arity of sort [Prop], or - [c] has a non-informative head symbol *) - match get_arity env t with - | None -> - assert false (* Cf. precondition. *) - | Some InProp -> - Tprop - | Some _ -> extract_type_rec_info env c vl args - + (* Since [t] is an arity, there is two non-informative case: *) + (* [t] is an arity of sort [Prop], or *) + (* [c] has a non-informative head symbol *) + match get_arity env t with + | None -> + assert false (* Cf. precondition. *) + | Some InProp -> + Tprop + | Some _ -> extract_type_rec_info env c vl args + and extract_type_rec_info env c vl args = - match (kind_of_term (whd_betaiotalet env none c)) with + match (kind_of_term (betaiotazeta env none c)) with | Sort _ -> assert (args = []); (* A sort can't be applied. *) Tarity @@ -428,7 +360,7 @@ and extract_type_rec_info env c vl args = extract_type_app env (IndRef spi,si,vli) vl args |Iprop -> assert false (* Cf. initial tests *)) | Case _ | Fix _ | CoFix _ -> - let id = next_ident_away flexible_name (prop_name::vl) in + let id = next_ident_away flex_name (prop_name::vl) in Tmltype (Tvar id, id :: vl) (* Type without counterpart in ML: we generate a new flexible type variable. *) @@ -438,7 +370,7 @@ and extract_type_rec_info env c vl args = | _ -> assert false -(* Auxiliary function used to factor code in lambda and product cases *) +(*s Auxiliary function used to factor code in lambda and product cases *) and extract_prod_lam env (n,t,d) vl flag = let tag = v_of_t env t in @@ -447,11 +379,11 @@ and extract_prod_lam env (n,t,d) vl flag = | (Info, Arity), _ -> (* We rename before the [push_rel], to be sure that the corresponding*) (* [lookup_rel] will be correct. *) - let id' = next_ident_away (id_of_name n) (prop_name::vl) in + let id' = next_ident_away (id_of_name n) vl in let env' = push_rel_assum (Name id', t) env in - extract_type_rec_info env' d (id'::vl) [] + extract_type_rec_info env' d (id'::vl) [] (* TODO !!!!!!!!!! *) | (Logic, Arity), _ | _, Lam -> - extract_type_rec_info env' d vl [] + extract_type_rec_info env' d vl [] (* TODO !!!!!!!!!!!! *) | (Logic, NotArity), Product -> (match extract_type_rec_info env' d vl [] with | Tmltype (mld, vl') -> Tmltype (Tarr (Miniml.Tprop, mld), vl') @@ -467,21 +399,21 @@ and extract_prod_lam env (n,t,d) vl flag = | Tmltype (mlt,vl'') -> Tmltype (Tarr(mlt,mld), vl'')) | et -> et) - (* Auxiliary function dealing with type application. - Precondition: [r] is of type an arity. *) +(*s Auxiliary function dealing with type application. + Precondition: [r] is of type an arity. *) and extract_type_app env (r,sc,vlc) vl args = let diff = (List.length args - List.length sc ) in let args = if diff > 0 then begin - (* This can (normally) only happen when r is a flexible type. - We discard the remaining arguments *) + (* This can (normally) only happen when r is a flexible type. *) + (* We discard the remaining arguments *) (*i wARN (hov 0 (str ("Discarding " ^ (string_of_int diff) ^ " type(s) argument(s)."))); i*) list_firstn (List.length sc) args end else args in let nargs = List.length args in - (* [r] is of type an arity, so it can't be applied to more than n args, - where n is the number of products in this arity type. *) + (* [r] is of type an arity, so it can't be applied to more than n args, *) + (* where n is the number of products in this arity type. *) (* But there are flexibles ... *) let sign_args = list_firstn nargs sc in let (mlargs,vl') = @@ -497,8 +429,8 @@ and extract_type_app env (r,sc,vlc) vl args = (List.combine sign_args args) ([],vl) in - (* The type variable list is [vl'] plus those variables of [c] not - corresponding to arguments. There is [nvlargs] such variables of [c] *) + (* The type variable list is [vl'] plus those variables of [c] not *) + (* corresponding to arguments. There is [nvlargs] such variables of [c] *) let nvlargs = List.length vlc - List.length mlargs in assert (nvlargs >= 0); let vl'' = @@ -512,13 +444,13 @@ and extract_type_app env (r,sc,vlc) vl args = Tmltype (Tapp ((Tglob r) :: mlargs @ vlargs), vl'') -(*s Signature of a type. *) +(*S Signature of a type. *) (* Precondition: [c] is of type an arity. This function is built on the [extract_type] model. *) and signature env c = - signature_rec env (whd_betaiotalet env none c) [] + signature_rec env (betaiotazeta env none c) [] and signature_rec env c args = match kind_of_term c with @@ -531,25 +463,25 @@ and signature_rec env c args = | Rel n -> (match lookup_rel n env with | (_,Some t,_) -> - let c' = whd_betaiotalet env none (lift n t) in + let c' = betaiotazeta env none (lift n t) in signature_rec env c' args | _ -> []) | Const sp when args = [] && is_ml_extraction (ConstRef sp) -> [] | Const sp when is_axiom sp -> [] | Const sp -> - let t = constant_type env sp in - if is_arity env none t then - (match extract_constant sp with - | Emltype (Miniml.Tarity,_,_) -> [] - | Emltype (Miniml.Tprop,_,_) -> [] - | Emltype (_,sc,_) -> - let d = List.length sc - List.length args in - if d <= 0 then [] else list_lastn d sc - | Emlterm _ -> assert false) - else - let cvalue = constant_value env sp in - let c' = whd_betaiotalet env none (applist (cvalue, args)) in - signature_rec env c' [] + let t = constant_type env sp in + if is_arity env none t then + (match extract_constant sp with + | Emltype (Miniml.Tarity,_,_) -> [] + | Emltype (Miniml.Tprop,_,_) -> [] + | Emltype (_,sc,_) -> + let d = List.length sc - List.length args in + if d <= 0 then [] else list_lastn d sc + | Emlterm _ -> assert false) + else + let cvalue = constant_value env sp in + let c' = betaiotazeta env none (applist (cvalue, args)) in + signature_rec env c' [] | Ind spi -> (match extract_inductive spi with |Iml (si,_) -> @@ -564,84 +496,59 @@ and signature_rec env c args = (*s signature of a section path *) and signature_of_sp sp typ = - try - Gmap.find sp !signature_table + try lookup_signature sp with Not_found -> - let s = signature (Global.env()) typ in - signature_table := Gmap.add sp s !signature_table; s + let s = signature (Global.env()) typ in + add_signature sp s; s -(*s Extraction of a term. - Precondition: [c] has a type which is not an arity. - This is normaly checked in [extract_constr]. *) +(*S Extraction of a term. *) -and extract_term env ctx c = - extract_term_wt env ctx c (type_of env c) +(* Precondition: [c] has a type which is not an arity, and is informative. + This is normaly checked in [extract_constr]. *) -(* Same, but With Type (wt). *) - -and extract_term_wt env ctx c t = - let s = sort_of env t in - (* The only non-informative case: [s] is [Prop] *) - if (s = InProp) then - Rprop - else - Rmlterm (extract_term_info_wt env ctx c t) - -(* Variants with a stronger precondition: [c] is informative. - We directly return a [ml_ast], not a [term_extraction_result] *) - -and extract_term_info env ctx c = - extract_term_info_wt env ctx c (type_of env c) +and extract_term env c = + extract_term_wt env c (type_of env c) (* Same, but With Type (wt). *) -and extract_term_info_wt env ctx c t = +and extract_term_wt env c t = match kind_of_term c with | Lambda (n, t, d) -> - let v = v_of_t env t in let id = id_of_name n in - let id = if id=prop_name then anonymous else id in - let env' = push_rel_assum (Name id,t) env in - let ctx' = (snd v = NotArity) :: ctx in - let d' = extract_term_info env' ctx' d in (* If [d] was of type an arity, [c] too would be so *) - (match v with - | _,Arity -> d' - | Logic,NotArity -> MLlam (prop_name, d') - | Info,NotArity -> MLlam (id, d')) + let d' = extract_term (push_rel_assum (Name id,t) env) d in + if (v_of_t env t)=default then MLlam (id, d') + else MLlam(prop_name, d') | LetIn (n, c1, t1, c2) -> - let v = v_of_t env t1 in let id = id_of_name n in - let id = if id=prop_name then anonymous else id in - let env' = push_rel (Name id,Some c1,t1) env in - (match v with - | (Info, NotArity) -> - let c1' = extract_term_info_wt env ctx c1 t1 in - let c2' = extract_term_info env' (true :: ctx) c2 in - (* If [c2] was of type an arity, [c] too would be so *) - MLletin (id,c1',c2') - | _ -> extract_term_info env' (false :: ctx) c2) + (* 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 + (match v_of_t env t1 with + | _,Arity -> MLletin (prop_name,MLarity,c2') + | Logic,NotArity -> MLletin (prop_name, MLprop, c2') + | Info, NotArity -> + let c1' = extract_term_wt env c1 t1 in + MLletin (id,c1',c2')) | Rel n -> - MLrel (renum_db ctx n) + MLrel n | Const sp -> - abstract_const sp (signature_of_sp sp t) + abstract_constant sp (signature_of_sp sp t) | App (f,a) -> - extract_app env ctx f a + extract_app env f a | Construct cp -> abstract_constructor cp (signature_of_constructor cp) | Case ({ci_ind=ip},_,c,br) -> - extract_case env ctx ip c br + extract_case env ip c br | Fix ((_,i),recd) -> - extract_fix env ctx i recd + extract_fix env i recd | CoFix (i,recd) -> - extract_fix env ctx i recd + extract_fix env i recd | Cast (c, _) -> - extract_term_info_wt env ctx c t - | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> - assert false + extract_term_wt env c t + | Ind _ | Prod _ | Sort _ | Meta _ | Evar _ -> assert false | Var _ -> section_message () -(*s Abstraction of an inductive constructor: +(*s Abstraction of an inductive constructor. \begin{itemize} \item In ML, contructor arguments are uncurryfied. \item We managed to suppress logical parts inside inductive definitions, @@ -652,90 +559,78 @@ and extract_term_info_wt env ctx c t = The following code deals with those 3 questions: from constructor [C], it produces: - [fun ]$p_1 \ldots p_n ~ x_1 \ldots x_n $[-> C(]$x_{i_1},\ldots, x_{i_k}$[)]. - This ML term will be reduced later on when applied, see [mlutil.ml]. + This ML term will be reduced later on when applied, see [mlutil.ml].\\ - In the special case of a informative singleton inductive, [C] is identity *) + In the special case of a informative singleton inductive, [C] is identity. *) -and abstract_constructor cp (s,n) = - let f = if is_singleton_constructor cp then - function [x] -> x | _ -> assert false - else - fun a -> MLcons (ConstructRef cp, a) - in anonym_lams (ml_lift n (prop_abstract_1 f s)) n +and abstract_constructor cp (s,params_nb) = + let f a = if is_singleton_constructor cp then List.hd a + else MLcons (ConstructRef cp, a) + in prop_lams (ml_lift params_nb (prop_abstract f s)) params_nb -(* Extraction of a case *) +(*s Extraction of a case. *) -and extract_case env ctx ip c br = +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,_) = signature_of_constructor cp in assert (List.length s = ni.(j)); - let (rb,e) = decompose_lam_eta ni.(j) env b in - let lb = List.rev rb in - (* We suppose that [sign_of_lbinders env lb] gives back [s] *) - (* So we trust [s] when making [ctx'] *) - let ctx' = List.fold_left (fun l v -> (v = default)::l) ctx s in - (* Some pathological cases need an [extract_constr] here rather *) - (* than an [extract_term]. See exemples in [test_extraction.v] *) - let env' = push_rel_context (List.map (fun (x,t) -> (x,None,t)) rb) env in - let e' = extract_constr_to_term env' ctx' e in - let ids = - List.fold_right - (fun (v,(n,_)) a -> if v = default then (id_of_name n :: a) else a) - (List.combine s lb) [] - in - (ConstructRef cp, ids, e') + let ids,e = kill_all_prop_lams_eta e s in + (ConstructRef cp, List.rev ids, e) in if br = [||] then MLexn "absurd case" else - (* [c] has an inductive type, not an arity type *) - match extract_term env ctx c with - | Rmlterm a when is_singleton_inductive ip -> - (* 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 (List.length ids = 1); - MLletin (List.hd ids,a,e') - | Rmlterm a -> - (* Standard case: we apply [extract_branch]. *) - MLcase (a, Array.mapi extract_branch br) - | Rprop -> - (* Logical singleton case: *) - (* [match c with C i j k -> t] becomes [t'] *) + (* [c] has an inductive type, not an arity 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 -> logic :: l) ni.(0) [] in + snd (kill_all_prop_lams_eta e s) + end + else + let a = extract_term_wt env c t 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 (rb,e) = decompose_lam_eta ni.(0) env br.(0) in - let env' = push_rels_assum rb env in - (* We know that all arguments are logic. *) - let ctx' = iterate (fun l -> false :: l) ni.(0) ctx in - extract_constr_to_term env' ctx' e - + let (_,ids,e') = extract_branch 0 br.(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) -(* Extraction of a (co)-fixpoint *) +(*s Extraction of a (co)-fixpoint. *) -and extract_fix env ctx i (fi,ti,ci as recd) = +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 ctx' = - (List.rev_map (fun (_,a) -> a = NotArity) (sign_of_lbinders env lb)) @ ctx - in let extract_fix_body c t = - extract_constr_to_term_wt env' ctx' c (lift n t) in + 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) -(* Auxiliary function dealing with term application. - Precondition: the head [f] is [Info]. *) +(*s Extraction of an term application. + Precondition: the head [f] is [Info]. *) -and extract_app env ctx f args = +and extract_app env f args = let tyf = type_of env f in let nargs = Array.length args in let sf = signature_of_application env f tyf args in @@ -745,31 +640,30 @@ and extract_app env ctx f args = let mlargs = List.fold_right (fun (v,a) args -> match v with - | (_,Arity) -> args + | (_,Arity) -> MLarity :: args | (Logic,NotArity) -> MLprop :: args | (Info,NotArity) -> (* We can't trust tag [default], so we use [extract_constr]. *) - (extract_constr_to_term env ctx a) :: args) + (extract_constr_to_term env a) :: args) (List.combine (list_firstn nargs sf) args) [] in (* [f : arity] implies [(f args):arity], that can't be *) - let f' = extract_term_info_wt env ctx f tyf in + let f' = extract_term_wt env f tyf in MLapp (f', mlargs) -(* [signature_of_application] is used to generate a long enough signature. +(*s [signature_of_application] is used to generate a long enough signature. Precondition: the head [f] is [Info]. - Postcondition: the returned signature is longer than the arguments *) + Postcondition: the output signature is at least as long as the arguments. *) and signature_of_application env f t a = let nargs = Array.length a in - let t = force_n_prod nargs env t in - (* It does not really ensure that [t] start by [n] products, - but it reduces as much as possible *) + let t = if nb_prod t >= nargs then t else whd_betadeltaiota env none t in + (* It does not really ensure that [t] start by [n] products, *) + (* but it reduces as much as possible *) let nbp = nb_prod t in let s = signature env t in - if nbp >= nargs then - s + if nbp >= nargs then s else (* This case can really occur. Cf [test_extraction.v]. *) let f' = mkApp (f, Array.sub a 0 nbp) in @@ -777,21 +671,20 @@ and signature_of_application env f t a = let t' = type_of env f' in s @ signature_of_application env f' t' a' - (*s Extraction of a constr seen as a term. *) -and extract_constr_to_term env ctx c = - extract_constr_to_term_wt env ctx c (type_of env c) +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 ctx c t = +and extract_constr_to_term_wt env c t = match v_of_t env t with | (_, Arity) -> MLarity | (Logic, NotArity) -> MLprop - | (Info, NotArity) -> extract_term_info_wt env ctx c t + | (Info, NotArity) -> extract_term_wt env c t -(* Extraction of a constr. *) +(*S Extraction of a constr. *) and extract_constr env c = extract_constr_wt env c (type_of env c) @@ -808,13 +701,12 @@ and extract_constr_wt env c t = | Tarity -> Emltype (Miniml.Tarity, [], []) | Tmltype (t, vl) -> Emltype (t, (signature env c), vl)) | (Info, NotArity) -> - Emlterm (extract_term_info_wt env [] c t) + Emlterm (extract_term_wt env c t) -(*s Extraction of a constant. *) +(*S Extraction of a constant. *) and extract_constant sp = - try - Gmap.find sp !constant_table + try lookup_constant sp with Not_found -> let env = Global.env() in let cb = Global.lookup_constant sp in @@ -830,26 +722,25 @@ and extract_constant sp = | Emlterm MLprop as e -> e | Emlterm MLarity as e -> e | Emlterm a -> - Emlterm (eta_expanse_w_prop a (signature_of_sp sp typ)) + Emlterm (kill_prop_lams_eta a (signature_of_sp sp typ)) | e -> e - in constant_table := Gmap.add sp e !constant_table; - e + in add_constant sp e; e -(*s Extraction of an inductive. *) +(*S Extraction of an inductive. *) and extract_inductive ((sp,_) as i) = extract_mib sp; - lookup_inductive_extraction i + lookup_inductive i and extract_constructor (((sp,_),_) as c) = extract_mib sp; - lookup_constructor_extraction c + lookup_constructor c and signature_of_constructor cp = match extract_constructor cp with | Cprop -> assert false | Cml (_,s,n) -> (s,n) -(* Looking for informative singleton case, i.e. an inductive with one +(*s Looking for informative singleton case, i.e. an inductive with one constructor which has one informative argument. This dummy case will be simplified. *) @@ -867,39 +758,33 @@ and is_singleton_constructor ((sp,i),_) = and extract_mib sp = let ind = (sp,0) in - if not (Gmap.mem ind !inductive_extraction_table) then begin + if not (Gmap.mem ind !inductive_table) then begin let (mib,mip) = Global.lookup_inductive ind in - let genv = Global.env () in - (* Everything concerning parameters. - We do that first, since they are common to all the [mib]. *) - let nb = mip.mind_nparams in - let rb = mip.mind_params_ctxt in - let env = push_rel_context rb genv in - let lb = List.rev_map (fun (n,s,t)->(n,t)) rb in - let nbtokeep = - lbinders_fold - (fun _ _ (_,j) a -> if j = NotArity then a+1 else a) 0 genv lb in - let vl = vl_of_lbinders genv lb in - (* First pass: we store inductive signatures together with - an initial type var list. *) + let env = Global.env () in + (* Everything concerning parameters. *) + (* We do that first, since they are common to all the [mib]. *) + let par_nb = mip.mind_nparams in + let par_env = push_rel_context mip.mind_params_ctxt env in + (* First pass: we store inductive signatures together with *) + (* an initial type var list. *) let vl0 = iterate_for 0 (mib.mind_ntypes - 1) (fun i vl -> let ip = (sp,i) in let (mib,mip) = Global.lookup_inductive ip in if mip.mind_sort = (Prop Null) then begin - add_inductive_extraction ip Iprop; vl + add_inductive ip Iprop; vl end else begin let arity = mip.mind_nf_arity in - let vla = List.rev (vl_of_arity genv arity) in - add_inductive_extraction ip - (Iml (sign_of_arity genv arity, vla)); + let vla = List.rev (vl_of_arity env arity) in + add_inductive ip + (Iml (sign_of_arity env arity, vla)); vla @ vl end ) [] in - (* Second pass: we extract constructors arities and we accumulate - type variables. Thanks to on-the-fly renaming in [extract_type], - the [vl] list should be correct. *) + (* Second pass: we extract constructors arities and we accumulate *) + (* type variables. Thanks to on-the-fly renaming in [extract_type], *) + (* the [vl] list should be correct. *) let vl = iterate_for 0 (mib.mind_ntypes - 1) (fun i vl -> @@ -907,20 +792,20 @@ and extract_mib sp = let (mib,mip) = Global.lookup_inductive ip in if mip.mind_sort = Prop Null then begin for j = 1 to Array.length mip.mind_consnames do - add_constructor_extraction (ip,j) Cprop + add_constructor (ip,j) Cprop done; vl end else iterate_for 1 (Array.length mip.mind_consnames) (fun j vl -> - let t = type_of_constructor genv (ip,j) in - let t = snd (decompose_prod_n nb t) in - match extract_type_rec_info env t vl [] with + let t = type_of_constructor env (ip,j) in + let t = snd (decompose_prod_n par_nb t) in + match extract_type_rec_info par_env t vl [] with | Tarity | Tprop -> assert false | Tmltype (mlt, v) -> let l = list_of_ml_arrows mlt - and s = signature env t in - add_constructor_extraction (ip,j) (Cml (l,s,nbtokeep)); + and s = signature par_env t in + add_constructor (ip,j) (Cml (l,s,par_nb)); v) vl) vl0 @@ -929,21 +814,21 @@ and extract_mib sp = (* Third pass: we update the type variables list in the inductives table *) for i = 0 to mib.mind_ntypes-1 do let ip = (sp,i) in - match lookup_inductive_extraction ip with + match lookup_inductive ip with | Iprop -> () - | Iml (s,l) -> add_inductive_extraction ip (Iml (s,vl@l)); + | Iml (s,l) -> add_inductive ip (Iml (s,vl@l)); done; (* Fourth pass: we also update the constructors table *) for i = 0 to mib.mind_ntypes-1 do let ip = (sp,i) in for j = 1 to Array.length mib.mind_packets.(i).mind_consnames do let cp = (ip,j) in - match lookup_constructor_extraction cp with + match lookup_constructor cp with | Cprop -> () | Cml (t,s,n) -> let vl = List.rev_map (fun i -> Tvar i) vl in let t' = List.map (update_args sp vl) t in - add_constructor_extraction cp (Cml (t',s, n)) + add_constructor cp (Cml (t',s, n)) done done end @@ -952,11 +837,11 @@ and extract_inductive_declaration sp = extract_mib sp; let ip = (sp,0) in if is_singleton_inductive ip then - let t = match lookup_constructor_extraction (ip,1) with + let t = match lookup_constructor (ip,1) with | Cml ([t],_,_)-> t | _ -> assert false in - let vl = match lookup_inductive_extraction ip with + let vl = match lookup_inductive ip with | Iml (_,vl) -> vl | _ -> assert false in @@ -967,7 +852,7 @@ and extract_inductive_declaration sp = iterate_for (-n) (-1) (fun j l -> let cp = (ip,-j) in - match lookup_constructor_extraction cp with + match lookup_constructor cp with | Cprop -> assert false | Cml (t,_,_) -> (ConstructRef cp, t)::l) [] in @@ -976,7 +861,7 @@ and extract_inductive_declaration sp = (fun i acc -> let ip = (sp,-i) in let nc = Array.length mib.mind_packets.(-i).mind_consnames in - match lookup_inductive_extraction ip with + match lookup_inductive ip with | Iprop -> acc | Iml (_,vl) -> (List.rev vl, IndRef ip, one_ind ip nc) :: acc) @@ -984,7 +869,9 @@ and extract_inductive_declaration sp = in Dtype (l, not mib.mind_finite) -(*s Extraction of a global reference i.e. a constant or an inductive. *) +(*S Extraction of a global reference. *) + +(* It is either a constant or an inductive. *) let extract_declaration r = match r with | ConstRef sp -> diff --git a/contrib/extraction/extraction.mli b/contrib/extraction/extraction.mli index e3a747ce0..df11ee14c 100644 --- a/contrib/extraction/extraction.mli +++ b/contrib/extraction/extraction.mli @@ -46,3 +46,5 @@ val decl_is_logical_ind : global_reference -> bool a singleton inductive. *) val decl_is_singleton : global_reference -> bool + +val signature : env -> constr -> signature diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml index 53c1b4bc5..201458bb7 100644 --- a/contrib/extraction/haskell.ml +++ b/contrib/extraction/haskell.ml @@ -156,13 +156,13 @@ let rec pp_expr par env args = 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 | MLexn s -> - (* An [MLexn] may be applied, but I don't really care *) + (* An [MLexn] may be applied, but I don't really care. *) (open_par par ++ str "Prelude.error" ++ spc () ++ qs s ++ close_par par) | MLprop -> - assert (args=[]); str "prop" + str "prop" (* An [MLprop] may be applied, but I don't really care. *) | MLarity -> - assert (args=[]); str "arity" + str "arity" (* Idem for [MLarity].*) | MLcast (a,t) -> let tvars = get_tvars t in let _,ren = rename_tvars keywords tvars in diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index d9286f441..32c72519c 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -8,6 +8,7 @@ (*i $Id$ i*) +(*i*) open Pp open Names open Term @@ -18,16 +19,25 @@ open Nametab open Table open Options open Nameops +(*i*) (*s Exceptions. *) exception Found exception Impossible -(*s Dummy names. *) +(*S Names operations. *) let anonymous = id_of_string "x" let prop_name = id_of_string "_" +let flex_name = id_of_string "flex" + +let id_of_name = function + | Anonymous -> anonymous + | Name id when id = prop_name -> anonymous + | Name id -> id + +(*S Operations upon ML types. *) (*s Get all type variables from a ML type *) @@ -64,66 +74,10 @@ let rec update_args sp vl = function | Tarr (a,b)-> Tarr (update_args sp vl a, update_args sp vl b) | a -> a - -(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns - the list [idn;...;id1] and the term [t]. *) - -let collect_lams = - let rec collect acc = function - | MLlam(id,t) -> collect (id::acc) t - | x -> acc,x - in collect [] - -(* [collect_n_lams] does the same for a precise number of [MLlam] *) - -let collect_n_lams = - let rec collect acc n t = - if n = 0 then acc,t - else match t with - | MLlam(id,t) -> collect (id::acc) (n-1) t - | _ -> assert false - in collect [] - -(* [remove_n_lams] just remove some [MLlam] *) - -let rec remove_n_lams n t = - if n = 0 then t - else match t with - | MLlam(_,t) -> remove_n_lams (n-1) t - | _ -> assert false - -(* [nb_lams] gives the number of head [MLlam] *) - -let rec nb_lams = function - | MLlam(_,t) -> succ (nb_lams t) - | _ -> 0 - -(*s [named_lams] does the converse of [collect_lams] *) - -let rec named_lams a = function - | [] -> a - | id :: ids -> named_lams (MLlam(id,a)) ids - -(* The same in anonymous version. *) - -let rec anonym_lams a = function - | 0 -> a - | n -> anonym_lams (MLlam(anonymous,a)) (pred n) - -(*s The following function create [MLrel n;...;MLrel 1] *) - -let rec make_eta_args n = - if n = 0 then [] else (MLrel n)::(make_eta_args (pred n)) - -(* This one tests [MLrel (n+k); ... ;MLrel (1+k)] *) - -let rec test_eta_args_lift k n = function - | [] -> n=0 - | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q) -(*s Generic functions overs [ml_ast]. *) +(*S Generic functions over ML ast terms. *) -(* [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care +(*s [ast_iter_rel f t] applies [f] on every [MLrel] in t. It takes care of the number of bingings crossed before reaching the [MLrel]. *) let ast_iter_rel f = @@ -141,7 +95,7 @@ let ast_iter_rel f = | MLglob _ | MLexn _ | MLprop | MLarity -> () in iter 0 -(* Map over asts. *) +(*s Map over asts. *) let ast_map_case f (c,ids,a) = (c,ids,f a) @@ -156,7 +110,7 @@ let ast_map f = function | MLmagic a -> MLmagic (f a) | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a -(* Map over asts, with binding depth as parameter. *) +(*s Map over asts, with binding depth as parameter. *) let ast_map_lift_case f n (c,ids,a) = (c,ids, f (n+(List.length ids)) a) @@ -172,7 +126,7 @@ let ast_map_lift f n = function | MLmagic a -> MLmagic (f n a) | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> a -(* Iter over asts. *) +(*s Iter over asts. *) let ast_iter_case f (c,ids,a) = f a @@ -187,14 +141,16 @@ let ast_iter f = function | MLmagic a -> f a | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity as a -> () -(*s [occurs k t] returns true if [(Rel k)] occurs in [t]. *) +(*S Operations concerning De Bruijn indices. *) + +(*s [occurs k t] returns [true] if [(Rel k)] occurs in [t]. *) let occurs k t = try ast_iter_rel (fun i -> if i = k then raise Found) t; false with Found -> true -(*s [occurs_itvl k k' t] return true if there is a [(Rel i)] +(*s [occurs_itvl k k' t] returns [true] if there is a [(Rel i)] in [t] with [k<=i<=k'] *) let occurs_itvl k k' t = @@ -222,22 +178,6 @@ let ml_lift k t = let ml_pop t = ml_lift (-1) t -(*s Computes a eta-reduction *) - -let eta_red e = - let ids,t = collect_lams e in - let n = List.length ids in - if n = 0 then e - else match t with - | MLapp (f,a) -> - let m = (List.length a) - n in - if m < 0 then e else - let a',a'' = list_chop m a in - let f = if m = 0 then f else MLapp (f,a') in - if test_eta_args_lift 0 n a'' && not (occurs_itvl 1 n f) - then ml_lift (-n) f - else e - | _ -> e (*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'] *) @@ -265,6 +205,106 @@ let rec ml_subst e = | a -> ast_map_lift subst n a in subst 0 +(*s Generalized substitution. + [gensubst v m d t] applies to [t] the substitution coded in the + [v] array: [(Rel i)] becomes [(Rel v.(i))]. [d] is the correction applies + to [Rel] greater than [m]. *) + +let gen_subst v d t = + let rec subst n = function + | MLrel i as a -> + let i'= i-n in + if i' < 1 then a + else if i' < Array.length v then MLrel (v.(i')+n) + else MLrel (i+d) + | a -> ast_map_lift subst n a + in subst 0 t + +(*S Operations concerning lambdas. *) + +(*s [collect_lams MLlam(id1,...MLlam(idn,t)...)] returns + [[idn;...;id1]] and the term [t]. *) + +let collect_lams = + let rec collect acc = function + | MLlam(id,t) -> collect (id::acc) t + | x -> acc,x + in collect [] + +(*s [collect_n_lams] does the same for a precise number of [MLlam]. *) + +let collect_n_lams = + let rec collect acc n t = + if n = 0 then acc,t + else match t with + | MLlam(id,t) -> collect (id::acc) (n-1) t + | _ -> assert false + in collect [] + +(*s [remove_n_lams] just removes some [MLlam]. *) + +let rec remove_n_lams n t = + if n = 0 then t + else match t with + | MLlam(_,t) -> remove_n_lams (n-1) t + | _ -> assert false + +(*s [nb_lams] gives the number of head [MLlam]. *) + +let rec nb_lams = function + | MLlam(_,t) -> succ (nb_lams t) + | _ -> 0 + +(*s [named_lams] does the converse of [collect_lams]. *) + +let rec named_lams ids a = match ids with + | [] -> a + | id :: ids -> named_lams ids (MLlam(id,a)) + +(*s The same in anonymous version. *) + +let rec anonym_lams a = function + | 0 -> a + | n -> anonym_lams (MLlam(anonymous,a)) (pred n) + +(*s Idem for [prop_name]. *) + +let rec prop_lams a = function + | 0 -> a + | n -> anonym_lams (MLlam(prop_name,a)) (pred n) + +(*S Operations concerning eta. *) + +(*s The following function creates [MLrel n;...;MLrel 1] *) + +let rec eta_args n = + if n = 0 then [] else (MLrel n)::(eta_args (pred n)) + +(*s This one tests [MLrel (n+k); ... ;MLrel (1+k)] *) + +let rec test_eta_args_lift k n = function + | [] -> n=0 + | a :: q -> (a = (MLrel (k+n))) && (test_eta_args_lift k (pred n) q) + +(*s Computes a eta-reduction. *) + +let eta_red e = + let ids,t = collect_lams e in + let n = List.length ids in + if n = 0 then e + else match t with + | MLapp (f,a) -> + let m = (List.length a) - n in + if m < 0 then e else + let a',a'' = list_chop m a in + let f = if m = 0 then f else MLapp (f,a') in + if test_eta_args_lift 0 n a'' && not (occurs_itvl 1 n f) + then ml_lift (-n) f + else e + | _ -> e + +(*S Auxiliary functions used in simplification of ML cases. *) + (*s [check_and_generalize (r0,l,c)] transforms any [MLcons(r0,l)] in [MLrel 1] and raises [Impossible] if any variable in [l] occurs outside such a [MLcons] *) @@ -282,8 +322,6 @@ let check_and_generalize (r0,l,c) = | a -> ast_map_lift genrec n a in genrec 0 c -(*s Auxialiary functions used during simplifications of [MLcase]. *) - let check_generalizable_case br = let f = check_and_generalize br.(0) in for i = 1 to Array.length br - 1 do @@ -319,10 +357,11 @@ let rec permut_case_fun br acc = done; (ids,br) -(*s Generalized iota-reduction. *) +(*S Generalized iota-reduction. *) (* Definition of a generalized iota-redex: it's a [MLcase(e,_)] - with [(is_iota_gen e)=true]. *) + with [(is_iota_gen e)=true]. Any generalized iota-redex is + transformed into beta-redexes. *) let rec is_iota_gen = function | MLcons _ -> true @@ -333,8 +372,6 @@ let constructor_index = function | ConstructRef (_,j) -> pred j | _ -> assert false -(* Any generalized iota-redex is transformed into beta-redexes. *) - let iota_gen br = let rec iota k = function | MLcons (r,a) -> @@ -349,12 +386,14 @@ let iota_gen br = | _ -> assert false in iota 0 -(*s Some beta-iota reductions + simplifications. *) - let is_atomic = function | MLrel _ | MLglob _ | MLexn _ | MLprop | MLarity -> true | _ -> false +(*S The main simplification function. *) + +(* Some beta-iota reductions + simplifications. *) + let rec simpl o = function | MLapp (f, []) -> simpl o f @@ -363,8 +402,9 @@ let rec simpl o = function | MLcase (e,br) -> let br = Array.map (fun (n,l,t) -> (n,l,simpl o t)) br in simpl_case o br (simpl o e) - | MLletin(_,c,e) when (is_atomic c) || (nb_occur e <= 1) -> - simpl o (ml_subst c e) + | MLletin(id,c,e) when + (id = prop_name) || (is_atomic c) || (nb_occur e <= 1) -> + simpl o (ml_subst c e) | MLletin(_,c,e) when (is_atomic (eta_red c)) -> simpl o (ml_subst (eta_red c) e) | MLfix(i,ids,c) as t when o -> @@ -376,6 +416,8 @@ let rec simpl o = function and simpl_app o a = function | MLapp (f',a') -> simpl_app o (a'@a) f' + | MLlam (id,t) when id = prop_name -> + simpl o (MLapp (ml_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)) @@ -394,7 +436,9 @@ and simpl_app o a = function let k = List.length l in let a' = List.map (ml_lift k) a in (n, l, simpl o (MLapp (t,a')))) br - in simpl o (MLcase (e,br')) + in simpl o (MLcase (e,br')) + | (MLarity | MLprop | MLexn _) as e -> e + (* We just discard arguments in those cases. *) | f -> MLapp (f,a) and simpl_case o br e = @@ -414,117 +458,121 @@ 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 (MLcase (ml_lift n e, br)) ids - -(*s Local [prop] elimination. *) -(* Try to eliminate as many [prop] as possible inside an [ml_ast]. *) - -(* Given the names of the variables, build a substitution array. *) - -let rels_to_kill ids = - let n = List.length ids in - let v = Array.make (n+1) 0 in - for i = 1 to n do v.(i) <- i done; - let rec parse_ids i j = function - | [] -> () - | id :: q when id <> prop_name -> - v.(i) <- j; parse_ids (i+1) (j+1) q - | _ :: q -> parse_ids (i+1) j q - in parse_ids 1 1 ids ; v - -(* [kill_prop_rels v m d t] applies to [t] the substitution coded with the - [v] array. [m] is the number of [Rel] concerned by this substitution, - and [d] is the correction applies to [Rel] greater than [m]. *) - -let rec kill_prop_rels v m d t = - let rec killrec n = function - | MLrel i as a -> - let i'= i-n in - if i' < 1 then a - else if i' <= m then MLrel (v.(i')+n) - else MLrel (i-d) - | a -> ast_map_lift killrec n a - in killrec 0 t - -(* In a list of args, kill the ones corresponding to a [prop]. *) + else named_lams ids (MLcase (ml_lift n e, br)) -let rec kill_some_args ids args = match ids,args with - | [],_ -> args - | i::l,t::q -> let a = kill_some_args l q in - if i = prop_name then a else t::a - | _ -> assert false +(*S Local prop elimination. *) +(* We try to eliminate as many [prop] as possible inside an [ml_ast]. *) -(* Apply the previous function recursively on a whole term *) +(*s In a list, it selects only the elements corresponding to a [true] + in the boolean list [l]. *) -let kill_prop_args t0 ids m t = - let rids = List.rev ids in +let rec select_via_bl l args = match l,args with + | [],_ -> args + | true::l,a::args -> a :: (select_via_bl l args) + | false::l,a::args -> select_via_bl l args + | _ -> assert false + +(*s [kill_some_lams] removes some head lambdas according to the bool list [bl]. + This list is build on the identifier list model: outermost lambda + is on the right. [true] means "to keep" and [false] means "to eliminate". + [Rels] corresponding to removed lambdas are supposed not to occur, and + the other [Rels] are made correct via a [gen_subst]. + Output is not directly a [ml_ast], compose with [named_lams] if needed. *) + +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 begin + let v = Array.make (n+1) 0 in + let rec parse_ids i j = function + | [] -> () + | true :: q -> + v.(i) <- j; parse_ids (i+1) (j+1) q + | false :: q -> parse_ids (i+1) j q + in parse_ids 1 1 bl ; + select_via_bl bl ids, gen_subst v (n'-n) c + end + +(*s [kill_prop_lams] uses the last function to kill the lambdas corresponding + to a [prop_name]. It can raise [Impossible] if there is nothing to do, or + if there is no lambda left at all. *) + +let kill_prop_lams c = + let ids,c = collect_lams c in + let bl = List.map ((<>) prop_name) ids in + if (List.mem true bl) && (List.mem false bl) then + let ids',c = kill_some_lams bl (ids,c) in + ids, named_lams ids' c + else raise Impossible + +(*s [kill_prop_args ids t0 t] looks for occurences of [t0] in [t] and + purge the args of [t0] corresponding to a [prop_name]. + It makes eta-expansion if needed. *) + +let kill_prop_args ids t0 t = + let m = List.length ids in + let bl = List.rev_map ((<>) prop_name) ids in let rec killrec n = function | MLapp(e, a) when e = ml_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 = kill_some_args rids (a @ (make_eta_args k)) in - named_lams (MLapp (ml_lift k e, a)) (list_firstn k ids) + 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 -> - let a = kill_some_args rids (make_eta_args m) in - named_lams (MLapp (ml_lift m e, a)) ids + let a = select_via_bl bl (eta_args m) in + named_lams ids (MLapp (ml_lift m e, a)) | e -> ast_map_lift killrec n e in killrec 0 t -let kill_prop_aux c = - let ids,c = collect_lams c in - let m = List.length ids in - let ids' = List.filter ((<>) prop_name) ids in - let diff = m - List.length ids' in - if ids' = [] || diff = 0 then raise Impossible; - let db = rels_to_kill ids in - let c = named_lams (kill_prop_rels db m diff c) ids' in - (c,ids,m) - -(* The main function for local [prop] elimination. *) +(*s The main function for local [prop] elimination. *) let rec kill_prop = function | MLfix(i,fi,c) -> (try - let c,ids,m = kill_prop_fix i fi c in - ml_subst (MLfix (i,fi,c)) (kill_prop_args (MLrel 1) ids m (MLrel 1)) + let ids,c = kill_prop_fix i fi c in + ml_subst (MLfix (i,fi,c)) (kill_prop_args ids (MLrel 1) (MLrel 1)) with Impossible -> MLfix (i,fi,Array.map kill_prop c)) | MLapp (MLfix (i,fi,c),a) -> (try - let c,ids,m = kill_prop_fix i fi c in + let ids,c = kill_prop_fix i fi c in let a = List.map (fun t -> ml_lift 1 (kill_prop t)) a in - let e = kill_prop_args (MLrel 1) ids m (MLapp (MLrel 1,a)) in + let e = kill_prop_args ids (MLrel 1) (MLapp (MLrel 1,a)) in ml_subst (MLfix (i,fi,c)) e with Impossible -> MLapp(MLfix(i,fi,Array.map kill_prop c),List.map kill_prop a)) | MLletin(id, MLfix (i,fi,c),e) -> (try - let c,ids,m = kill_prop_fix i fi c in - let e = kill_prop (kill_prop_args (MLrel 1) ids m e) in + let ids,c = kill_prop_fix i fi c in + let e = kill_prop (kill_prop_args ids (MLrel 1) e) in MLletin(id, MLfix(i,fi,c),e) with Impossible -> MLletin(id, MLfix(i,fi,Array.map kill_prop c),kill_prop e)) | MLletin(id,c,e) -> (try - let c,ids,m = kill_prop_aux c in - let e = kill_prop_args (MLrel 1) ids m e in + let ids,c = kill_prop_lams c in + let e = kill_prop_args ids (MLrel 1) e in MLletin (id, kill_prop c,kill_prop e) with Impossible -> MLletin(id,kill_prop c,kill_prop e)) | a -> ast_map kill_prop a and kill_prop_fix i fi c = let n = Array.length fi in - let ci,ids,m = kill_prop_aux c.(i) in + let ids,ci = kill_prop_lams c.(i) in let c = Array.copy c in c.(i) <- ci; for j = 0 to (n-1) do - c.(j) <- kill_prop (kill_prop_args (MLrel (n-i)) ids m c.(j)) + c.(j) <- kill_prop (kill_prop_args ids (MLrel (n-i)) c.(j)) done; - c,ids,m + ids,c + +(*s Putting things together. *) let normalize a = if (optim()) then kill_prop (simpl true a) else simpl false a -(*s Special treatment of non-mutual fixpoint for pretty-printing purpose. *) +(*S Special treatment of non-mutual fixpoint for pretty-printing purpose. *) (* TODO a reecrire plus proprement!! *) @@ -532,19 +580,13 @@ let make_general_fix f ids n args m c = let v = Array.make n 0 in for i=0 to (n-1) do v.(i)<-i done; let aux i = function - MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1) + | MLrel j when v.(j-1)>=0 -> v.(j-1)<-(-i-1) | _ -> raise Impossible - 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 - (normalize (MLapp ((ml_subst new_f c),args))) ids - in MLfix(0,[|f|],[|new_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 + MLfix(0,[|f|],[|new_c|]) let optimize_fix a = if not (optim()) then a @@ -552,28 +594,27 @@ let optimize_fix a = let ids,a' = collect_lams a in let n = List.length ids in if n = 0 then a - else - (match a' with - | MLfix(_,[|f|],[|c|]) -> - let new_f = MLapp (MLrel (n+1),make_eta_args n) in - let new_c = named_lams (ml_subst new_f c) ids - in MLfix(0,[|f|],[|new_c|]) - | MLapp(a',args) -> - let m = List.length args in - (match a' with - | MLfix(_,[|_|],[|_|]) when - (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') - -> a' - | MLfix(_,[|f|],[|c|]) -> - (try - make_general_fix f ids n args m c - with Impossible -> - named_lams (MLapp (MLfix (0,[|f|],[|c|]),args)) ids) - | _ -> a) - | _ -> a) - - -(*s Utility functions used for the decision of expansion. *) + else match a' with + | MLfix(_,[|f|],[|c|]) -> + let new_f = MLapp (MLrel (n+1),eta_args n) in + let new_c = named_lams ids (ml_subst new_f c) + in MLfix(0,[|f|],[|new_c|]) + | MLapp(a',args) -> + let m = List.length args in + (match a' with + | MLfix(_,[|_|],[|_|]) when + (test_eta_args_lift 0 n args) && not (occurs_itvl 1 m a') + -> a' + | MLfix(_,[|f|],[|c|]) -> + (try make_general_fix f ids n args m c + with Impossible -> + named_lams ids (MLapp (MLfix (0,[|f|],[|c|]),args))) + | _ -> a) + | _ -> a + +(*S Inlining. *) + +(* Utility functions used in the decision of inlining. *) let rec ml_size = function | MLapp(t,l) -> List.length l + ml_size t + ml_size_list l @@ -629,9 +670,8 @@ let rec non_stricts add cand = function List.filter ((<>) n) cand | MLapp (MLrel n, _) -> List.filter ((<>) n) cand - (* In [(x y)] we say that only x is strict. Cf [sig_rec]. - We may gain something if x is replaced by a function like - a projection *) + (* In [(x y)] we say that only x is strict. Cf [sig_rec]. We may *) + (* gain something if x is replaced by a function like a projection *) | MLapp (t,l)-> let cand = non_stricts false cand t in List.fold_left (non_stricts false) cand l @@ -646,9 +686,9 @@ let rec non_stricts add cand = function let cand = Array.fold_left (non_stricts false) cand f in pop n cand | MLcase (t,v) -> - (* The only interesting case: for a variable to be non-strict, - it is sufficient that it appears non-strict in at least one branch, - so he make an union (in fact a merge). *) + (* The only interesting case: for a variable to be non-strict, *) + (* it is sufficient that it appears non-strict in at least one branch, *) + (* so he make an union (in fact a merge). *) let cand = non_stricts false cand t in Array.fold_left (fun c (_,i,t)-> @@ -669,63 +709,55 @@ let rec non_stricts add cand = function exception. *) let is_not_strict t = - try - let _ = non_stricts true [] t in false - with - | Toplevel -> true + try let _ = non_stricts true [] t in false + with Toplevel -> true -(*s Expansion decision *) +(*s Inlining decision *) -(* [expansion_test] answers the following question: - If we could expand [t] (the user said nothing special), - should we expand ? +(* [inline_test] answers the following question: + If we could inline [t] (the user said nothing special), + should we inline ? We don't expand fixpoints, but always inductive constructors and small terms. - Last case of expansion is a term with at least one non-strict + Last case of inlining is a term with at least one non-strict variable (i.e. a variable that may not be evaluated). *) -let expansion_test t = - (not (is_fix t)) - && - ((is_constr t) || - (ml_size t < 3) || - ((ml_size t < 12) && (is_not_strict t))) +let inline_test t = + not (is_fix t) + && (is_constr t || ml_size t < 3 || (ml_size t < 12 && is_not_strict t)) -let manual_expand_list = +let manual_inline_list = List.map (fun s -> path_of_string ("Coq.Init."^s)) [ "Specif.sigS_rect" ; "Specif.sigS_rec" ; "Datatypes.prod_rect" ; "Datatypes.prod_rec"; "Wf.Acc_rec" ; "Wf.Acc_rect" ; "Wf.well_founded_induction" ; "Wf.well_founded_induction_type" ] -let manual_expand = function - | ConstRef sp -> List.mem sp manual_expand_list +let manual_inline = function + | ConstRef sp -> List.mem sp manual_inline_list | _ -> false -(* If the user doesn't say he wants to keep [t], we expand in two cases: +(* If the user doesn't say he wants to keep [t], we inline in two cases: \begin{itemize} \item the user explicitly requests it - \item [expansion_test] answers that the expansion is a good idea, and + \item [expansion_test] answers that the inlining is a good idea, and we are free to act (AutoInline is set) \end{itemize} *) -let expand r t = - (not (to_keep r)) (* The user DOES want to keep it *) - && - ((to_inline r) (* The user DOES want to expand it *) - || - (auto_inline () && lang () <> Haskell && - ((manual_expand r) || expansion_test t))) +let inline r t = + not (to_keep r) (* The user DOES want to keep it *) + && (to_inline r (* The user DOES want to inline it *) + || (auto_inline () && lang () <> Haskell + && (manual_inline r || inline_test t))) -(*s Optimization *) +(*S Optimization. *) let subst_glob_ast r m = let rec substrec = function | MLglob r' as t -> if r = r' then m else t | t -> ast_map substrec t - in - substrec + in substrec let subst_glob_decl r m = function | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t') @@ -747,20 +779,14 @@ let rec optimize prm = function Dabbrev(r,_,Tprop) | Dglob(r,MLarity) | Dglob(r,MLprop) ) as d :: l -> - if List.mem r prm.to_appear then - d :: (optimize prm l) + if List.mem r prm.to_appear then d :: (optimize prm l) else optimize prm l | Dglob (r,t) :: l -> let t = normalize t in - let b = expand r t in - let l = if b then - List.map (subst_glob_decl r t) l - else l in - if (not b || prm.modular || List.mem r prm.to_appear) then - let t = optimize_fix t in - Dglob (r,t) :: (optimize prm l) + let b = not (inline r t) in + let l = if b then l else List.map (subst_glob_decl r t) l in + if (b || prm.modular || List.mem r prm.to_appear) then + Dglob (r,optimize_fix t) :: (optimize prm l) else optimize prm l | d :: l -> d :: (optimize prm l) - - diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index 02257be77..b58ee5260 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -18,17 +18,25 @@ open Nametab val anonymous : identifier val prop_name : identifier +val flex_name : identifier +val id_of_name : name -> identifier (*s [collect_lambda MLlam(id1,...MLlam(idn,t)...)] returns 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 named_lams : ml_ast -> identifier list -> ml_ast +val prop_lams : ml_ast -> int -> ml_ast + +val named_lams : identifier list -> ml_ast -> ml_ast (*s Utility functions over ML types. [update_args sp vl t] puts [vl] as arguments behind every inductive types [(sp,_)]. *) @@ -56,7 +64,7 @@ val ml_subst : ml_ast -> ml_ast -> ml_ast (*s Some transformations of ML terms. [normalize] simplify all beta redexes (when the argument does not occur, it is just thrown away; when it occurs exactly once it is substituted; otherwise - a let in redex is created for clarity) and iota redexes, plus some other + a let-in redex is created for clarity) and iota redexes, plus some other optimizations. *) val normalize : ml_ast -> ml_ast @@ -69,7 +77,5 @@ val add_ml_decls : val optimize : extraction_params -> ml_decl list -> ml_decl list -exception Impossible - -val kill_prop_aux : ml_ast -> ml_ast * identifier list * int - +val kill_some_lams : + bool list -> identifier list * ml_ast -> identifier list * ml_ast diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml index 57a198d13..4bd05b03f 100644 --- a/contrib/extraction/ocaml.ml +++ b/contrib/extraction/ocaml.ml @@ -251,13 +251,13 @@ let rec pp_expr par env args = 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 | MLexn s -> - (* an [MLexn] may be applied, but I don't really care *) + (* An [MLexn] may be applied, but I don't really care. *) (open_par par ++ str "assert false" ++ spc () ++ str ("(* "^s^" *)") ++ close_par par) | MLprop -> - assert (args=[]); str "prop" + str "prop" (* An [MLprop] may be applied, but I don't really care. *) | MLarity -> - assert (args=[]); str "arity" + str "arity" (* idem for [MLarity]. *) | MLcast (a,t) -> let tvars = get_tvars t in let _,ren = rename_tvars keywords tvars in diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v index a2a17d20b..406b81953 100644 --- a/contrib/extraction/test_extraction.v +++ b/contrib/extraction/test_extraction.v @@ -28,7 +28,7 @@ Extraction [f:nat->nat][x:nat](f x). (* fun f x -> f x *) Extraction [f:nat->Set->nat][x:nat](f x nat). -(* fun f x -> f x *) +(* fun f x -> f x arity *) Extraction [f:(nat->nat)->nat][x:nat][g:nat->nat](f g). (* fun f x g -> f g *) @@ -46,7 +46,7 @@ Extraction ([X:Set][x:X]x nat). Definition d := [X:Type]X. Extraction d. (* type 'x d = 'x *) Extraction (d Set). (* arity d *) -Extraction [x:(d Set)]O. (* O *) +Extraction [x:(d Set)]O. (* fun _ -> O *) Extraction (d nat). (* nat d *) Extraction ([x:(d Type)]O Type). (* O *) @@ -148,11 +148,11 @@ Extraction eta_c. Eta_c of nat * nat *) Extraction (eta_c O). -(* fun x -> Eta_c (O, x) *) +(* fun _ x _ -> Eta_c (O, x) *) Extraction (eta_c O True). -(* fun x -> Eta_c (O, x) *) +(* fun x _ -> Eta_c (O, x) *) Extraction (eta_c O True O). -(* Eta_c (O, O) *) +(* fun _ -> Eta_c (O, O) *) (** Example of singleton inductive type *) @@ -295,7 +295,6 @@ Extraction [i:(X:Type)X->X](pair ? ? (i nat O) (i bool true)). (* problem: fun f -> (f 0, f true) not legal in ocaml *) (* solution: fun f -> (f 0, Obj.magic f true) *) -(* Prop applied to Prop : impossible ?*) Definition funPropSet:= [b:bool]<[_:bool]Type>if b then (X:Prop)X->X else (X:Set)X->X. @@ -310,3 +309,33 @@ Definition idpropset := Definition funProp := [b:bool][x:True]<natTrue>if b then O else x. +(*s prop and arity can be applied.... *) + +Definition f : (X:Type)(nat->X)->(X->bool)->bool := + [X:Type;x:nat->X;y:X->bool](y (x O)). +Extraction f. +(* let f x y = + y (x O) +*) + +Definition f_prop := (f (O=O) [_](refl_equal ? O) [_]true). +Extraction NoInline f. +Extraction f_prop. +(* let f_prop = + f prop (fun _ -> True) +*) + +Definition f_arity := (f Set [_:nat]nat [_:Set]true). +Extraction f_arity. +(* let f_arity = + f arity (fun _ -> True) +*) + +Definition f_normal := (f nat [x]x [x](Cases x of O => true | _ => false end)). +Extraction f_normal. +(* let f_normal = + f (fun x -> x) (fun x -> match x with + O -> True + | S n -> False) +*) + |