From c33019051c716916414320b8b676202b18e2e8e4 Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 12 Jan 2007 23:42:17 +0000 Subject: Suite au mail de Lionel a propos du Makefile: MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 1) Disparition de test_extraction.v rebasculé dans test-suite/success/extraction.v Au passage, remplacement de quelques Set en Type pour ne pas avoir besoin du -impredicative-set. Et ajout de passes d'extraction en Haskell et Scheme. Simplification du Makefile en conséquence (plus de barestate) 2) Au passage, reparation (et embellissement) de extract_env. Depuis le passage de Claudio dans cette portion (il y a 2 ans ?), faire Extraction S (ou tout autre constructeur) echouait. Idem pour un nom d'inductif mutuel autre que le premier du paquet. Etonnant que personne n'ait remarqué ca plus tot... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9484 85f007b7-540e-0410-9357-904b9bb8a0f7 --- Makefile | 3 - contrib/extraction/extract_env.ml | 299 ++++++++++-------- contrib/extraction/test_extraction.v | 552 -------------------------------- test-suite/success/extraction.v | 589 ++++++++++++++++++++++++++++++++++- 4 files changed, 748 insertions(+), 695 deletions(-) delete mode 100644 contrib/extraction/test_extraction.v diff --git a/Makefile b/Makefile index e28032735..776fff914 100644 --- a/Makefile +++ b/Makefile @@ -1129,9 +1129,6 @@ theories/%.vo: theories/%.v states/initial.coq $(VO_TOOLS_DEP) contrib/%.vo: contrib/%.v states/initial.coq $(VO_TOOLS_DEP) $(BOOTCOQTOP) -compile contrib/$* -contrib/extraction/%.vo: contrib/extraction/%.v states/barestate.coq $(VO_TOOLS_DEP) - $(BOOTCOQTOP) -is states/barestate.coq -compile $* - cleantheories: rm -f states/*.coq rm -f theories/*/*.vo diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 549e5e4fd..c231dc4f2 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -53,23 +53,55 @@ let environment_until dir_opt = | _ -> assert false in parse (Library.loaded_libraries ()) -type visit = - { mutable kn : KNset.t; mutable ref : Refset.t; mutable mp : MPset.t } - -let in_kn v kn = KNset.mem kn v.kn -let in_ref v ref = Refset.mem ref v.ref -let in_mp v mp = MPset.mem mp v.mp - -let visit_mp v mp = v.mp <- MPset.union (prefixes_mp mp) v.mp -let visit_kn v kn = v.kn <- KNset.add kn v.kn; visit_mp v (modpath kn) -let visit_ref v r = - let r = - (* if we meet a constructor we must export the inductive definition *) - match r with - ConstructRef (r,_) -> IndRef r - | _ -> r - in - v.ref <- Refset.add r v.ref; visit_mp v (modpath_of_r r) + +(*s Visit: + a structure recording the needed dependencies for the current extraction *) + +module type VISIT = sig + (* Reset the dependencies by emptying the visit lists *) + val reset : unit -> unit + + (* Add the module_path and all its prefixes to the mp visit list *) + val add_mp : module_path -> unit + + (* Add kernel_name / constant / reference / ... in the visit lists. + These functions silently add the mp of their arg in the mp list *) + val add_kn : kernel_name -> unit + val add_con : constant -> unit + val add_ref : global_reference -> unit + val add_decl_deps : ml_decl -> unit + val add_spec_deps : ml_spec -> unit + + (* Test functions: + is a particular object a needed dependency for the current extraction ? *) + val needed_kn : kernel_name -> bool + val needed_con : constant -> bool + val needed_mp : module_path -> bool +end + +module Visit : VISIT = struct + (* Thanks to C.S.C, what used to be in a single KNset should now be split + into a KNset (for inductives and modules names) and a Cset for constants + (and still the remaining MPset) *) + type must_visit = + { mutable kn : KNset.t; mutable con : Cset.t; mutable mp : MPset.t } + (* the imperative internal visit lists *) + let v = { kn = KNset.empty ; con = Cset.empty ; mp = MPset.empty } + (* the accessor functions *) + let reset () = v.kn <- KNset.empty; v.con <- Cset.empty; v.mp <- MPset.empty + let needed_kn kn = KNset.mem kn v.kn + let needed_con c = Cset.mem c v.con + let needed_mp mp = MPset.mem mp v.mp + let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) + let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) + let add_ref = function + | ConstRef c -> add_con c + | IndRef (kn,_) | ConstructRef ((kn,_),_) -> add_kn kn + | VarRef _ -> assert false + let add_decl_deps = decl_iter_references add_ref add_ref add_ref + let add_spec_deps = spec_iter_references add_ref add_ref add_ref +end exception Impossible @@ -104,115 +136,108 @@ let factor_fix env l cb msb = labels, recd, msb'' end -let get_decl_references v d = - let f = visit_ref v in decl_iter_references f f f d - -let get_spec_references v s = - let f = visit_ref v in spec_iter_references f f f s - -let rec extract_msig env v mp = function +let rec extract_msig env mp = function | [] -> [] | (l,SPBconst cb) :: msig -> let kn = make_con mp empty_dirpath l in let s = extract_constant_spec env kn cb in - if logical_spec s then extract_msig env v mp msig + if logical_spec s then extract_msig env mp msig else begin - get_spec_references v s; - (l,Spec s) :: (extract_msig env v mp msig) + Visit.add_spec_deps s; + (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmind cb) :: msig -> let kn = make_kn mp empty_dirpath l in let s = Sind (kn, extract_inductive env kn) in - if logical_spec s then extract_msig env v mp msig + if logical_spec s then extract_msig env mp msig else begin - get_spec_references v s; - (l,Spec s) :: (extract_msig env v mp msig) + Visit.add_spec_deps s; + (l,Spec s) :: (extract_msig env mp msig) end | (l,SPBmodule {msb_modtype=mtb}) :: msig -> -(*i let mpo = Some (MPdot (mp,l)) in i*) - (l,Smodule (extract_mtb env v None (*i mpo i*) mtb)) :: (extract_msig env v mp msig) + (l,Smodule (extract_mtb env None mtb)) :: (extract_msig env mp msig) | (l,SPBmodtype mtb) :: msig -> - (l,Smodtype (extract_mtb env v None mtb)) :: (extract_msig env v mp msig) + (l,Smodtype (extract_mtb env None mtb)) :: (extract_msig env mp msig) -and extract_mtb env v mpo = function - | MTBident kn -> visit_kn v kn; MTident kn +and extract_mtb env mpo = function + | MTBident kn -> Visit.add_kn kn; MTident kn | MTBfunsig (mbid, mtb, mtb') -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MTfunsig (mbid, extract_mtb env v None mtb, - extract_mtb env' v None mtb') + MTfunsig (mbid, extract_mtb env None mtb, + extract_mtb env' None mtb') | MTBsig (msid, msig) -> let mp, msig = match mpo with | None -> MPself msid, msig | Some mp -> mp, Modops.subst_signature_msid msid mp msig in let env' = Modops.add_signature mp msig env in - MTsig (msid, extract_msig env' v mp msig) + MTsig (msid, extract_msig env' mp msig) -let rec extract_msb env v mp all = function +let rec extract_msb env mp all = function | [] -> [] | (l,SEBconst cb) :: msb -> (try let vl,recd,msb = factor_fix env l cb msb in - let vkn = Array.map (fun id -> make_con mp empty_dirpath id) vl in - let ms = extract_msb env v mp all msb in - let b = array_exists (fun con -> in_ref v (ConstRef con)) vkn in + let vc = Array.map (make_con mp empty_dirpath) vl in + let ms = extract_msb env mp all msb in + let b = array_exists Visit.needed_con vc in if all || b then - let d = extract_fixpoint env vkn recd in + let d = extract_fixpoint env vc recd in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms with Impossible -> - let ms = extract_msb env v mp all msb in - let kn = make_con mp empty_dirpath l in - let b = in_ref v (ConstRef kn) in + let ms = extract_msb env mp all msb in + let c = make_con mp empty_dirpath l in + let b = Visit.needed_con c in if all || b then - let d = extract_constant env kn cb in + let d = extract_constant env c cb in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms) | (l,SEBmind mib) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in - let b = in_ref v (IndRef (kn,0)) in (* 0 is dummy *) + let b = Visit.needed_kn kn in if all || b then let d = Dind (kn, extract_inductive env kn) in if (not b) && (logical_decl d) then ms - else begin get_decl_references v d; (l,SEdecl d) :: ms end + else begin Visit.add_decl_deps d; (l,SEdecl d) :: ms end else ms | (l,SEBmodule mb) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let mp = MPdot (mp,l) in - if all || in_mp v mp then - (l,SEmodule (extract_module env v mp true mb)) :: ms + if all || Visit.needed_mp mp then + (l,SEmodule (extract_module env mp true mb)) :: ms else ms | (l,SEBmodtype mtb) :: msb -> - let ms = extract_msb env v mp all msb in + let ms = extract_msb env mp all msb in let kn = make_kn mp empty_dirpath l in - if all || in_kn v kn then - (l,SEmodtype (extract_mtb env v None mtb)) :: ms + if all || Visit.needed_kn kn then + (l,SEmodtype (extract_mtb env None mtb)) :: ms else ms -and extract_meb env v mpo all = function +and extract_meb env mpo all = function | MEBident (MPfile d) -> error_MPfile_as_mod d (* temporary (I hope) *) - | MEBident mp -> visit_mp v mp; MEident mp + | MEBident mp -> Visit.add_mp mp; MEident mp | MEBapply (meb, meb',_) -> - MEapply (extract_meb env v None true meb, - extract_meb env v None true meb') + MEapply (extract_meb env None true meb, + extract_meb env None true meb') | MEBfunctor (mbid, mtb, meb) -> let mp = MPbound mbid in let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in - MEfunctor (mbid, extract_mtb env v None mtb, - extract_meb env' v None true meb) + MEfunctor (mbid, extract_mtb env None mtb, + extract_meb env' None true meb) | MEBstruct (msid, msb) -> let mp,msb = match mpo with | None -> MPself msid, msb | Some mp -> mp, subst_msb (map_msid msid mp) msb in let env' = add_structure mp msb env in - MEstruct (msid, extract_msb env' v mp all msb) + MEstruct (msid, extract_msb env' mp all msb) -and extract_module env v mp all mb = +and extract_module env mp all mb = (* [mb.mod_expr <> None ], since we look at modules from outside. *) (* Example of module with empty [mod_expr] is X inside a Module F [X:SIG]. *) let meb = out_some mb.mod_expr in @@ -220,25 +245,21 @@ and extract_module env v mp all mb = (* Because of the "with" construct, the module type can be [MTBsig] with *) (* a msid different from the one of the module. Here is the patch. *) let mtb = replicate_msid meb mtb in - { ml_mod_expr = extract_meb env v (Some mp) all meb; - ml_mod_type = extract_mtb env v None mtb } + { ml_mod_expr = extract_meb env (Some mp) all meb; + ml_mod_type = extract_mtb env None mtb } let unpack = function MEstruct (_,sel) -> sel | _ -> assert false let mono_environment refs mpl = - let l = environment_until None in - let v = - let add_ref r = Refset.add r in - let refs = List.fold_right add_ref refs Refset.empty in - let add_mp mp = MPset.union (prefixes_mp mp) in - let mps = List.fold_right add_mp mpl MPset.empty in - let mps = Refset.fold (fun k -> add_mp (modpath_of_r k)) refs mps in - { kn = KNset.empty; ref = refs; mp = mps } - in + Visit.reset (); + List.iter Visit.add_ref refs; + List.iter Visit.add_mp mpl; let env = Global.env () in - List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) false m)) - (List.rev l) + let l = List.rev (environment_until None) in + List.rev_map + (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) false m)) l + (*s Recursive extraction in the Coq toplevel. The vernacular command is \verb!Recursive Extraction! [qualid1] ... [qualidn]. We use [extract_env] to get the saturated environment to extract. *) @@ -259,6 +280,7 @@ let mono_extraction (f,m) qualids = let prm = {modular=false; mod_name = m; to_appear= refs} in let struc = optimize_struct prm None (mono_environment refs mps) in print_structure_to_file f prm struc; + Visit.reset (); reset_tables () let extraction_rec = mono_extraction (None,id_of_string "Main") @@ -277,15 +299,15 @@ let extraction qid = let r = Nametab.global qid in if is_custom r then msgnl (str "User defined extraction:" ++ spc () ++ - str (find_custom r) ++ fnl ()) - else begin + str (find_custom r) ++ fnl ()) + else let prm = - { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in + { modular = false; mod_name = id_of_string "Main"; to_appear = [r]} in let struc = optimize_struct prm None (mono_environment [r] []) in let d = get_decl_in_structure r struc in print_one_decl struc (modpath_of_r r) d; - reset_tables () - end + Visit.reset (); + reset_tables () (*s Extraction to a file (necessarily recursive). The vernacular command is @@ -313,32 +335,33 @@ let extraction_file f vl = let extraction_module m = check_inside_section (); check_inside_module (); - match lang () with + begin match lang () with | Toplevel -> error_toplevel () | Scheme -> error_scheme () - | _ -> - let q = snd (qualid_of_reference m) in - let mp = - try Nametab.locate_module q - with Not_found -> error_unknown_module q - in - let b = is_modfile mp in - let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in - let l = environment_until None in - let v={ kn = KNset.empty ; ref = Refset.empty; mp = prefixes_mp mp } in - let env = Global.env () in - let struc = - List.rev_map - (fun (mp,m) -> mp, unpack (extract_meb env v (Some mp) b m)) - (List.rev l) - in - let struc = optimize_struct prm None struc in - let struc = - let bmp = base_mp mp in - try [bmp, List.assoc bmp struc] with Not_found -> assert false - in - print_structure_to_file None prm struc; - reset_tables () + | _ -> () + end; + let q = snd (qualid_of_reference m) in + let mp = + try Nametab.locate_module q with Not_found -> error_unknown_module q + in + let b = is_modfile mp in + let prm = {modular=b; mod_name = id_of_string ""; to_appear= []} in + Visit.reset (); + Visit.add_mp mp; + let env = Global.env () in + let l = List.rev (environment_until None) in + let struc = + List.rev_map (fun (mp,m) -> mp, unpack (extract_meb env (Some mp) b m)) l + in + let struc = optimize_struct prm None struc in + let struc = + let bmp = base_mp mp in + try [bmp, List.assoc bmp struc] with Not_found -> assert false + in + print_structure_to_file None prm struc; + Visit.reset (); + reset_tables () + (*s (Recursive) Extraction of a library. The vernacular command is \verb!(Recursive) Extraction Library! [M]. *) @@ -355,38 +378,38 @@ let dir_module_of_id m = let extraction_library is_rec m = check_inside_section (); check_inside_module (); - match lang () with + begin match lang () with | Toplevel -> error_toplevel () | Scheme -> error_scheme () - | _ -> - let dir_m = dir_module_of_id m in - let v = - { kn = KNset.empty; ref = Refset.empty; - mp = MPset.singleton (MPfile dir_m) } in - let l = environment_until (Some dir_m) in - let struc = - let env = Global.env () in - let select l (mp,meb) = - if in_mp v mp (* [mp] est long -> [in_mp] peut etre sans [long_mp] *) - then (mp, unpack (extract_meb env v (Some mp) true meb)) :: l - else l - in - List.fold_left select [] (List.rev l) - in - let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in - let struc = optimize_struct dummy_prm None struc in - let rec print = function - | [] -> () - | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l - | (MPfile dir, sel) as e :: l -> - let short_m = snd (split_dirpath dir) in - let f = module_file_name short_m in - let prm = {modular=true;mod_name=short_m;to_appear=[]} in - print_structure_to_file (Some f) prm [e]; - print l - | _ -> assert false - in print struc; - reset_tables () + | _ -> () + end; + let dir_m = dir_module_of_id m in + Visit.reset (); + Visit.add_mp (MPfile dir_m); + let env = Global.env () in + let l = List.rev (environment_until (Some dir_m)) in + let select l (mp,meb) = + if Visit.needed_mp mp + then (mp, unpack (extract_meb env (Some mp) true meb)) :: l + else l + in + let struc = List.fold_left select [] l in + let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in + let struc = optimize_struct dummy_prm None struc in + let rec print = function + | [] -> () + | (MPfile dir, _) :: l when not is_rec && dir <> dir_m -> print l + | (MPfile dir, sel) as e :: l -> + let short_m = snd (split_dirpath dir) in + let f = module_file_name short_m in + let prm = {modular=true;mod_name=short_m;to_appear=[]} in + print_structure_to_file (Some f) prm [e]; + print l + | _ -> assert false + in + print struc; + Visit.reset (); + reset_tables () diff --git a/contrib/extraction/test_extraction.v b/contrib/extraction/test_extraction.v deleted file mode 100644 index 0745f62d1..000000000 --- a/contrib/extraction/test_extraction.v +++ /dev/null @@ -1,552 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* nat) (x:nat) := f x. -Extraction test2. -(* let test2 f x = f x *) - -Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat. -Extraction test3. -(* let test3 f x = f x __ *) - -Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g. -Extraction test4. -(* let test4 f x g = f g *) - -Definition test5 := (1, 0). -Extraction test5. -(* let test5 = Pair ((S O), O) *) - -Definition cf (x:nat) (_:x <= 0) := S x. -Extraction NoInline cf. -Definition test6 := cf 0 (le_n 0). -Extraction test6. -(* let test6 = cf O *) - -Definition test7 := (fun (X:Set) (x:X) => x) nat. -Extraction test7. -(* let test7 x = x *) - -Definition d (X:Type) := X. -Extraction d. (* type 'x d = 'x *) -Definition d2 := d Set. -Extraction d2. (* type d2 = __ d *) -Definition d3 (x:d Set) := 0. -Extraction d3. (* let d3 _ = O *) -Definition d4 := d nat. -Extraction d4. (* type d4 = nat d *) -Definition d5 := (fun x:d Type => 0) Type. -Extraction d5. (* let d5 = O *) -Definition d6 (x:d Type) := x. -Extraction d6. (* type 'x d6 = 'x *) - -Definition test8 := (fun (X:Type) (x:X) => x) Set nat. -Extraction test8. (* type test8 = nat *) - -Definition test9 := let t := nat in id Set t. -Extraction test9. (* type test9 = nat *) - -Definition test10 := (fun (X:Type) (x:X) => 0) Type Type. -Extraction test10. (* let test10 = O *) - -Definition test11 := let n := 0 in let p := S n in S p. -Extraction test11. (* let test11 = S (S O) *) - -Definition test12 := forall x:forall X:Type, X -> X, x Type Type. -Extraction test12. -(* type test12 = (__ -> __ -> __) -> __ *) - - -Definition test13 := match left True I with - | left x => 1 - | right x => 0 - end. -Extraction test13. (* let test13 = S O *) - - -(** example with more arguments that given by the type *) - -Definition test19 := - nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0) - (fun (n:nat) (f:nat -> nat) => f) 0 0. -Extraction test19. -(* let test19 = - let rec f = function - | O -> (fun n0 -> O) - | S n0 -> f n0 - in f O O -*) - - -(** casts *) - -Definition test20 := True:Type. -Extraction test20. -(* type test20 = __ *) - - -(** Simple inductive type and recursor. *) - -Extraction nat. -(* -type nat = - | O - | S of nat -*) - -Extraction sumbool_rect. -(* -let sumbool_rect f f0 = function - | Left -> f __ - | Right -> f0 __ -*) - -(** Less simple inductive type. *) - -Inductive c (x:nat) : nat -> Set := - | refl : c x x - | trans : forall y z:nat, c x y -> y <= z -> c x z. -Extraction c. -(* -type c = - | Refl - | Trans of nat * nat * c -*) - -Definition Ensemble (U:Type) := U -> Prop. -Definition Empty_set (U:Type) (x:U) := False. -Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y. - -Inductive Finite (U:Type) : Ensemble U -> Set := - | Empty_is_finite : Finite U (Empty_set U) - | Union_is_finite : - forall A:Ensemble U, - Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x). -Extraction Finite. -(* -type 'u finite = - | Empty_is_finite - | Union_is_finite of 'u finite * 'u -*) - - -(** Mutual Inductive *) - -Inductive tree : Set := - Node : nat -> forest -> tree -with forest : Set := - | Leaf : nat -> forest - | Cons : tree -> forest -> forest. - -Extraction tree. -(* -type tree = - | Node of nat * forest -and forest = - | Leaf of nat - | Cons of tree * forest -*) - -Fixpoint tree_size (t:tree) : nat := - match t with - | Node a f => S (forest_size f) - end - - with forest_size (f:forest) : nat := - match f with - | Leaf b => 1 - | Cons t f' => tree_size t + forest_size f' - end. - -Extraction tree_size. -(* -let rec tree_size = function - | Node (a, f) -> S (forest_size f) -and forest_size = function - | Leaf b -> S O - | Cons (t, f') -> plus (tree_size t) (forest_size f') -*) - - -(** Eta-expansions of inductive constructor *) - -Inductive titi : Set := - tata : nat -> nat -> nat -> nat -> titi. -Definition test14 := tata 0. -Extraction test14. -(* let test14 x x0 x1 = Tata (O, x, x0, x1) *) -Definition test15 := tata 0 1. -Extraction test15. -(* let test15 x x0 = Tata (O, (S O), x, x0) *) - -Inductive eta : Set := - eta_c : nat -> Prop -> nat -> Prop -> eta. -Extraction eta_c. -(* -type eta = - | Eta_c of nat * nat -*) -Definition test16 := eta_c 0. -Extraction test16. -(* let test16 x = Eta_c (O, x) *) -Definition test17 := eta_c 0 True. -Extraction test17. -(* let test17 x = Eta_c (O, x) *) -Definition test18 := eta_c 0 True 0. -Extraction test18. -(* let test18 _ = Eta_c (O, O) *) - - -(** Example of singleton inductive type *) - -Inductive bidon (A:Prop) (B:Type) : Set := - tb : forall (x:A) (y:B), bidon A B. -Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) - (x:A) (y:B) := f x y. -Extraction bidon. -(* type 'b bidon = 'b *) -Extraction tb. -(* tb : singleton inductive constructor *) -Extraction fbidon. -(* let fbidon f x y = - f x y -*) - -Definition fbidon2 := fbidon True nat (tb True nat). -Extraction fbidon2. (* let fbidon2 y = y *) -Extraction NoInline fbidon. -Extraction fbidon2. -(* let fbidon2 y = fbidon (fun _ x -> x) __ y *) - -(* NB: first argument of fbidon2 has type [True], so it disappears. *) - -(** mutual inductive on many sorts *) - -Inductive test_0 : Prop := - ctest0 : test_0 -with test_1 : Set := - ctest1 : test_0 -> test_1. -Extraction test_0. -(* test0 : logical inductive *) -Extraction test_1. -(* -type test1 = - | Ctest1 -*) - -(** logical singleton *) - -Extraction eq. -(* eq : logical inductive *) -Extraction eq_rect. -(* let eq_rect x f y = - f -*) - -(** No more propagation of type parameters. Obj.t instead. *) - -Inductive tp1 : Set := - T : forall (C:Set) (c:C), tp2 -> tp1 -with tp2 : Set := - T' : tp1 -> tp2. -Extraction tp1. -(* -type tp1 = - | T of __ * tp2 -and tp2 = - | T' of tp1 -*) - -Inductive tp1bis : Set := - Tbis : tp2bis -> tp1bis -with tp2bis : Set := - T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis. -Extraction tp1bis. -(* -type tp1bis = - | Tbis of tp2bis -and tp2bis = - | T'bis of __ * tp1bis -*) - - -(** Strange inductive type. *) - -Inductive Truc : Set -> Set := - | chose : forall A:Set, Truc A - | machin : forall A:Set, A -> Truc bool -> Truc A. -Extraction Truc. -(* -type 'x truc = - | Chose - | Machin of 'x * bool truc -*) - - -(** Dependant type over Type *) - -Definition test24 := sigT (fun a:Set => option a). -Extraction test24. -(* type test24 = (__, __ option) sigT *) - - -(** Coq term non strongly-normalizable after extraction *) - -Require Import Gt. -Definition loop (Ax:Acc gt 0) := - (fix F (a:nat) (b:Acc gt a) {struct b} : nat := - F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax. -Extraction loop. -(* let loop _ = - let rec f a = - f (S a) - in f O -*) - -(*** EXAMPLES NEEDING OBJ.MAGIC *) - -(** False conversion of type: *) - -Lemma oups : forall H:nat = list nat, nat -> nat. -intros. -generalize H0; intros. -rewrite H in H1. -case H1. -exact H0. -intros. -exact n. -Qed. -Extraction oups. -(* -let oups h0 = - match Obj.magic h0 with - | Nil -> h0 - | Cons0 (n, l) -> n -*) - - -(** hybrids *) - -Definition horibilis (b:bool) := - if b as b return (if b then Type else nat) then Set else 0. -Extraction horibilis. -(* -let horibilis = function - | True -> Obj.magic __ - | False -> Obj.magic O -*) - -Definition PropSet (b:bool) := if b then Prop else Set. -Extraction PropSet. (* type propSet = __ *) - -Definition natbool (b:bool) := if b then nat else bool. -Extraction natbool. (* type natbool = __ *) - -Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true. -Extraction zerotrue. -(* -let zerotrue = function - | True -> Obj.magic O - | False -> Obj.magic True -*) - -Definition natProp (b:bool) := if b return Type then nat else Prop. - -Definition natTrue (b:bool) := if b return Type then nat else True. - -Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True. -Extraction zeroTrue. -(* -let zeroTrue = function - | True -> Obj.magic O - | False -> Obj.magic __ -*) - -Definition natTrue2 (b:bool) := if b return Type then nat else True. - -Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I. -Extraction zeroprop. -(* -let zeroprop = function - | True -> Obj.magic O - | False -> Obj.magic __ -*) - -(** polymorphic f applied several times *) - -Definition test21 := (id nat 0, id bool true). -Extraction test21. -(* let test21 = Pair ((id O), (id True)) *) - -(** ok *) - -Definition test22 := - (fun f:forall X:Type, X -> X => (f nat 0, f bool true)) - (fun (X:Type) (x:X) => x). -Extraction test22. -(* let test22 = - let f = fun x -> x in Pair ((f O), (f True)) *) - -(* still ok via optim beta -> let *) - -Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true). -Extraction test23. -(* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *) - -(* problem: fun f -> (f 0, f true) not legal in ocaml *) -(* solution: magic ... *) - - -(** Dummy constant __ can be applied.... *) - -Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0). -Extraction f. -(* let f x y = - y (x O) -*) - -Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true). -Extraction NoInline f. -Extraction f_prop. -(* let f_prop = - f (Obj.magic __) (fun _ -> True) -*) - -Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true). -Extraction f_arity. -(* let f_arity = - f (Obj.magic __) (fun _ -> True) -*) - -Definition f_normal := - f nat (fun x => x) (fun x => match x with - | O => true - | _ => false - end). -Extraction f_normal. -(* let f_normal = - f (fun x -> x) (fun x -> match x with - | O -> True - | S n -> False) -*) - - -(* inductive with magic needed *) - -Inductive Boite : Set := - boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. -Extraction Boite. -(* -type boite = - | Boite of bool * __ -*) - - -Definition boite1 := boite true 0. -Extraction boite1. -(* let boite1 = Boite (True, (Obj.magic O)) *) - -Definition boite2 := boite false (0, 0). -Extraction boite2. -(* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *) - -Definition test_boite (B:Boite) := - match B return nat with - | boite true n => n - | boite false n => fst n + snd n - end. -Extraction test_boite. -(* -let test_boite = function - | Boite (b0, n) -> - (match b0 with - | True -> Obj.magic n - | False -> plus (fst (Obj.magic n)) (snd (Obj.magic n))) -*) - -(* singleton inductive with magic needed *) - -Inductive Box : Set := - box : forall A:Set, A -> Box. -Extraction Box. -(* type box = __ *) - -Definition box1 := box nat 0. -Extraction box1. (* let box1 = Obj.magic O *) - -(* applied constant, magic needed *) - -Definition idzarb (b:bool) (x:if b then nat else bool) := x. -Definition zarb := idzarb true 0. -Extraction NoInline idzarb. -Extraction zarb. -(* let zarb = Obj.magic idzarb True (Obj.magic O) *) - -(** function of variable arity. *) -(** Fun n = nat -> nat -> ... -> nat *) - -Fixpoint Fun (n:nat) : Set := - match n with - | O => nat - | S n => nat -> Fun n - end. - -Fixpoint Const (k n:nat) {struct n} : Fun n := - match n as x return Fun x with - | O => k - | S n => fun p:nat => Const k n - end. - -Fixpoint proj (k n:nat) {struct n} : Fun n := - match n as x return Fun x with - | O => 0 (* ou assert false ....*) - | S n => - match k with - | O => fun x => Const x n - | S k => fun x => proj k n - end - end. - -Definition test_proj := proj 2 4 0 1 2 3. - -Eval compute in test_proj. - -Recursive Extraction test_proj. - - - -(*** TO SUM UP: ***) - - -Extraction - "test_extraction.ml" idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. - diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index e7da947b5..0b3060d51 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -1,5 +1,590 @@ -(* Mini extraction test *) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* nat) (x:nat) := f x. +Extraction test2. +(* let test2 f x = f x *) + +Definition test3 (f:nat -> Set -> nat) (x:nat) := f x nat. +Extraction test3. +(* let test3 f x = f x __ *) + +Definition test4 (f:(nat -> nat) -> nat) (x:nat) (g:nat -> nat) := f g. +Extraction test4. +(* let test4 f x g = f g *) + +Definition test5 := (1, 0). +Extraction test5. +(* let test5 = Pair ((S O), O) *) + +Definition cf (x:nat) (_:x <= 0) := S x. +Extraction NoInline cf. +Definition test6 := cf 0 (le_n 0). +Extraction test6. +(* let test6 = cf O *) + +Definition test7 := (fun (X:Set) (x:X) => x) nat. +Extraction test7. +(* let test7 x = x *) + +Definition d (X:Type) := X. +Extraction d. (* type 'x d = 'x *) +Definition d2 := d Set. +Extraction d2. (* type d2 = __ d *) +Definition d3 (x:d Set) := 0. +Extraction d3. (* let d3 _ = O *) +Definition d4 := d nat. +Extraction d4. (* type d4 = nat d *) +Definition d5 := (fun x:d Type => 0) Type. +Extraction d5. (* let d5 = O *) +Definition d6 (x:d Type) := x. +Extraction d6. (* type 'x d6 = 'x *) + +Definition test8 := (fun (X:Type) (x:X) => x) Set nat. +Extraction test8. (* type test8 = nat *) + +Definition test9 := let t := nat in id Set t. +Extraction test9. (* type test9 = nat *) + +Definition test10 := (fun (X:Type) (x:X) => 0) Type Type. +Extraction test10. (* let test10 = O *) + +Definition test11 := let n := 0 in let p := S n in S p. +Extraction test11. (* let test11 = S (S O) *) + +Definition test12 := forall x:forall X:Type, X -> X, x Type Type. +Extraction test12. +(* type test12 = (__ -> __ -> __) -> __ *) + + +Definition test13 := match left True I with + | left x => 1 + | right x => 0 + end. +Extraction test13. (* let test13 = S O *) + + +(** example with more arguments that given by the type *) + +Definition test19 := + nat_rec (fun n:nat => nat -> nat) (fun n:nat => 0) + (fun (n:nat) (f:nat -> nat) => f) 0 0. +Extraction test19. +(* let test19 = + let rec f = function + | O -> (fun n0 -> O) + | S n0 -> f n0 + in f O O +*) + + +(** casts *) + +Definition test20 := True:Type. +Extraction test20. +(* type test20 = __ *) + + +(** Simple inductive type and recursor. *) + +Extraction nat. +(* +type nat = + | O + | S of nat +*) + +Extraction sumbool_rect. +(* +let sumbool_rect f f0 = function + | Left -> f __ + | Right -> f0 __ +*) + +(** Less simple inductive type. *) + +Inductive c (x:nat) : nat -> Set := + | refl : c x x + | trans : forall y z:nat, c x y -> y <= z -> c x z. +Extraction c. +(* +type c = + | Refl + | Trans of nat * nat * c +*) + +Definition Ensemble (U:Type) := U -> Prop. +Definition Empty_set (U:Type) (x:U) := False. +Definition Add (U:Type) (A:Ensemble U) (x y:U) := A y \/ x = y. + +Inductive Finite (U:Type) : Ensemble U -> Type := + | Empty_is_finite : Finite U (Empty_set U) + | Union_is_finite : + forall A:Ensemble U, + Finite U A -> forall x:U, ~ A x -> Finite U (Add U A x). +Extraction Finite. +(* +type 'u finite = + | Empty_is_finite + | Union_is_finite of 'u finite * 'u +*) + + +(** Mutual Inductive *) + +Inductive tree : Set := + Node : nat -> forest -> tree +with forest : Set := + | Leaf : nat -> forest + | Cons : tree -> forest -> forest. + +Extraction tree. +(* +type tree = + | Node of nat * forest +and forest = + | Leaf of nat + | Cons of tree * forest +*) + +Fixpoint tree_size (t:tree) : nat := + match t with + | Node a f => S (forest_size f) + end + + with forest_size (f:forest) : nat := + match f with + | Leaf b => 1 + | Cons t f' => tree_size t + forest_size f' + end. + +Extraction tree_size. +(* +let rec tree_size = function + | Node (a, f) -> S (forest_size f) +and forest_size = function + | Leaf b -> S O + | Cons (t, f') -> plus (tree_size t) (forest_size f') +*) + + +(** Eta-expansions of inductive constructor *) + +Inductive titi : Set := + tata : nat -> nat -> nat -> nat -> titi. +Definition test14 := tata 0. +Extraction test14. +(* let test14 x x0 x1 = Tata (O, x, x0, x1) *) +Definition test15 := tata 0 1. +Extraction test15. +(* let test15 x x0 = Tata (O, (S O), x, x0) *) + +Inductive eta : Type := + eta_c : nat -> Prop -> nat -> Prop -> eta. +Extraction eta_c. +(* +type eta = + | Eta_c of nat * nat +*) +Definition test16 := eta_c 0. +Extraction test16. +(* let test16 x = Eta_c (O, x) *) +Definition test17 := eta_c 0 True. +Extraction test17. +(* let test17 x = Eta_c (O, x) *) +Definition test18 := eta_c 0 True 0. +Extraction test18. +(* let test18 _ = Eta_c (O, O) *) + + +(** Example of singleton inductive type *) + +Inductive bidon (A:Prop) (B:Type) : Type := + tb : forall (x:A) (y:B), bidon A B. +Definition fbidon (A B:Type) (f:A -> B -> bidon True nat) + (x:A) (y:B) := f x y. +Extraction bidon. +(* type 'b bidon = 'b *) +Extraction tb. +(* tb : singleton inductive constructor *) +Extraction fbidon. +(* let fbidon f x y = + f x y +*) + +Definition fbidon2 := fbidon True nat (tb True nat). +Extraction fbidon2. (* let fbidon2 y = y *) +Extraction NoInline fbidon. +Extraction fbidon2. +(* let fbidon2 y = fbidon (fun _ x -> x) __ y *) + +(* NB: first argument of fbidon2 has type [True], so it disappears. *) + +(** mutual inductive on many sorts *) + +Inductive test_0 : Prop := + ctest0 : test_0 +with test_1 : Set := + ctest1 : test_0 -> test_1. +Extraction test_0. +(* test0 : logical inductive *) +Extraction test_1. +(* +type test1 = + | Ctest1 +*) + +(** logical singleton *) + +Extraction eq. +(* eq : logical inductive *) +Extraction eq_rect. +(* let eq_rect x f y = + f +*) + +(** No more propagation of type parameters. Obj.t instead. *) + +Inductive tp1 : Type := + T : forall (C:Set) (c:C), tp2 -> tp1 +with tp2 : Type := + T' : tp1 -> tp2. +Extraction tp1. +(* +type tp1 = + | T of __ * tp2 +and tp2 = + | T' of tp1 +*) + +Inductive tp1bis : Type := + Tbis : tp2bis -> tp1bis +with tp2bis : Type := + T'bis : forall (C:Set) (c:C), tp1bis -> tp2bis. +Extraction tp1bis. +(* +type tp1bis = + | Tbis of tp2bis +and tp2bis = + | T'bis of __ * tp1bis +*) + + +(** Strange inductive type. *) + +Inductive Truc : Set -> Type := + | chose : forall A:Set, Truc A + | machin : forall A:Set, A -> Truc bool -> Truc A. +Extraction Truc. +(* +type 'x truc = + | Chose + | Machin of 'x * bool truc +*) + + +(** Dependant type over Type *) + +Definition test24 := sigT (fun a:Set => option a). +Extraction test24. +(* type test24 = (__, __ option) sigT *) + + +(** Coq term non strongly-normalizable after extraction *) + +Require Import Gt. +Definition loop (Ax:Acc gt 0) := + (fix F (a:nat) (b:Acc gt a) {struct b} : nat := + F (S a) (Acc_inv b (S a) (gt_Sn_n a))) 0 Ax. +Extraction loop. +(* let loop _ = + let rec f a = + f (S a) + in f O +*) + +(*** EXAMPLES NEEDING OBJ.MAGIC *) + +(** False conversion of type: *) + +Lemma oups : forall H:nat = list nat, nat -> nat. +intros. +generalize H0; intros. +rewrite H in H1. +case H1. +exact H0. +intros. +exact n. +Qed. +Extraction oups. +(* +let oups h0 = + match Obj.magic h0 with + | Nil -> h0 + | Cons0 (n, l) -> n +*) + + +(** hybrids *) + +Definition horibilis (b:bool) := + if b as b return (if b then Type else nat) then Set else 0. +Extraction horibilis. +(* +let horibilis = function + | True -> Obj.magic __ + | False -> Obj.magic O +*) + +Definition PropSet (b:bool) := if b then Prop else Set. +Extraction PropSet. (* type propSet = __ *) + +Definition natbool (b:bool) := if b then nat else bool. +Extraction natbool. (* type natbool = __ *) + +Definition zerotrue (b:bool) := if b as x return natbool x then 0 else true. +Extraction zerotrue. +(* +let zerotrue = function + | True -> Obj.magic O + | False -> Obj.magic True +*) + +Definition natProp (b:bool) := if b return Type then nat else Prop. + +Definition natTrue (b:bool) := if b return Type then nat else True. + +Definition zeroTrue (b:bool) := if b as x return natProp x then 0 else True. +Extraction zeroTrue. +(* +let zeroTrue = function + | True -> Obj.magic O + | False -> Obj.magic __ +*) + +Definition natTrue2 (b:bool) := if b return Type then nat else True. + +Definition zeroprop (b:bool) := if b as x return natTrue x then 0 else I. +Extraction zeroprop. +(* +let zeroprop = function + | True -> Obj.magic O + | False -> Obj.magic __ +*) + +(** polymorphic f applied several times *) + +Definition test21 := (id nat 0, id bool true). +Extraction test21. +(* let test21 = Pair ((id O), (id True)) *) + +(** ok *) + +Definition test22 := + (fun f:forall X:Type, X -> X => (f nat 0, f bool true)) + (fun (X:Type) (x:X) => x). +Extraction test22. +(* let test22 = + let f = fun x -> x in Pair ((f O), (f True)) *) + +(* still ok via optim beta -> let *) + +Definition test23 (f:forall X:Type, X -> X) := (f nat 0, f bool true). +Extraction test23. +(* let test23 f = Pair ((Obj.magic f __ O), (Obj.magic f __ True)) *) + +(* problem: fun f -> (f 0, f true) not legal in ocaml *) +(* solution: magic ... *) + + +(** Dummy constant __ can be applied.... *) + +Definition f (X:Type) (x:nat -> X) (y:X -> bool) : bool := y (x 0). +Extraction f. +(* let f x y = + y (x O) +*) + +Definition f_prop := f (0 = 0) (fun _ => refl_equal 0) (fun _ => true). +Extraction NoInline f. +Extraction f_prop. +(* let f_prop = + f (Obj.magic __) (fun _ -> True) +*) + +Definition f_arity := f Set (fun _:nat => nat) (fun _:Set => true). +Extraction f_arity. +(* let f_arity = + f (Obj.magic __) (fun _ -> True) +*) + +Definition f_normal := + f nat (fun x => x) (fun x => match x with + | O => true + | _ => false + end). +Extraction f_normal. +(* let f_normal = + f (fun x -> x) (fun x -> match x with + | O -> True + | S n -> False) +*) + + +(* inductive with magic needed *) + +Inductive Boite : Set := + boite : forall b:bool, (if b then nat else (nat * nat)%type) -> Boite. +Extraction Boite. +(* +type boite = + | Boite of bool * __ +*) + + +Definition boite1 := boite true 0. +Extraction boite1. +(* let boite1 = Boite (True, (Obj.magic O)) *) + +Definition boite2 := boite false (0, 0). +Extraction boite2. +(* let boite2 = Boite (False, (Obj.magic (Pair (O, O)))) *) + +Definition test_boite (B:Boite) := + match B return nat with + | boite true n => n + | boite false n => fst n + snd n + end. +Extraction test_boite. +(* +let test_boite = function + | Boite (b0, n) -> + (match b0 with + | True -> Obj.magic n + | False -> plus (fst (Obj.magic n)) (snd (Obj.magic n))) +*) + +(* singleton inductive with magic needed *) + +Inductive Box : Type := + box : forall A:Set, A -> Box. +Extraction Box. +(* type box = __ *) + +Definition box1 := box nat 0. +Extraction box1. (* let box1 = Obj.magic O *) + +(* applied constant, magic needed *) + +Definition idzarb (b:bool) (x:if b then nat else bool) := x. +Definition zarb := idzarb true 0. +Extraction NoInline idzarb. +Extraction zarb. +(* let zarb = Obj.magic idzarb True (Obj.magic O) *) + +(** function of variable arity. *) +(** Fun n = nat -> nat -> ... -> nat *) + +Fixpoint Fun (n:nat) : Set := + match n with + | O => nat + | S n => nat -> Fun n + end. + +Fixpoint Const (k n:nat) {struct n} : Fun n := + match n as x return Fun x with + | O => k + | S n => fun p:nat => Const k n + end. + +Fixpoint proj (k n:nat) {struct n} : Fun n := + match n as x return Fun x with + | O => 0 (* ou assert false ....*) + | S n => + match k with + | O => fun x => Const x n + | S k => fun x => proj k n + end + end. + +Definition test_proj := proj 2 4 0 1 2 3. + +Eval compute in test_proj. + +Recursive Extraction test_proj. + + + +(*** TO SUM UP: ***) + +(* Was previously producing a "test_extraction.ml" *) +Recursive Extraction + idnat id id' test2 test3 test4 test5 test6 test7 d d2 + d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 + test13 test19 test20 nat sumbool_rect c Finite tree + tree_size test14 test15 eta_c test16 test17 test18 bidon + tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 + tp1bis Truc oups test24 loop horibilis PropSet natbool + zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop + f_arity f_normal Boite boite1 boite2 test_boite Box box1 + zarb test_proj. + +Extraction Language Haskell. +(* Was previously producing a "Test_extraction.hs" *) +Recursive Extraction + idnat id id' test2 test3 test4 test5 test6 test7 d d2 + d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 + test13 test19 test20 nat sumbool_rect c Finite tree + tree_size test14 test15 eta_c test16 test17 test18 bidon + tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 + tp1bis Truc oups test24 loop horibilis PropSet natbool + zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop + f_arity f_normal Boite boite1 boite2 test_boite Box box1 + zarb test_proj. + +Extraction Language Scheme. +(* Was previously producing a "test_extraction.scm" *) +Recursive Extraction + idnat id id' test2 test3 test4 test5 test6 test7 d d2 + d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 + test13 test19 test20 nat sumbool_rect c Finite tree + tree_size test14 test15 eta_c test16 test17 test18 bidon + tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 + tp1bis Truc oups test24 loop horibilis PropSet natbool + zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop + f_arity f_normal Boite boite1 boite2 test_boite Box box1 + zarb test_proj. + + +(*** Finally, a test more focused on everyday's life situations ***) Require Import ZArith. -Extraction "zarith.ml" two_or_two_plus_one Zdiv_eucl_exist. +Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist. -- cgit v1.2.3