diff options
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/correctness/Correctness.v | 9 | ||||
-rw-r--r-- | contrib/correctness/examples/exp.v | 13 | ||||
-rw-r--r-- | contrib/correctness/examples/exp_int.v | 8 | ||||
-rw-r--r-- | contrib/correctness/pcic.ml | 5 | ||||
-rw-r--r-- | contrib/correctness/pmisc.ml | 8 | ||||
-rw-r--r-- | contrib/correctness/pmisc.mli | 6 | ||||
-rw-r--r-- | contrib/correctness/pmonad.ml | 24 | ||||
-rw-r--r-- | contrib/correctness/psyntax.ml4 | 2 | ||||
-rw-r--r-- | contrib/correctness/ptactic.ml | 22 | ||||
-rw-r--r-- | contrib/extraction/Extraction.v | 8 | ||||
-rw-r--r-- | contrib/extraction/extract_env.ml | 6 | ||||
-rw-r--r-- | contrib/extraction/mlutil.ml | 24 | ||||
-rw-r--r-- | contrib/extraction/mlutil.mli | 2 |
13 files changed, 60 insertions, 77 deletions
diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v index bc12ec755..0c47512ed 100644 --- a/contrib/correctness/Correctness.v +++ b/contrib/correctness/Correctness.v @@ -22,13 +22,4 @@ Require Export ProgWf. Require Export Arrays. -Declare ML Module - "pmisc" "peffect" "prename" - "perror" "penv" "putil" "pdb" "pcic" "pmonad" "pcicenv" - "pred" "ptyping" "pwp" "pmlize" "ptactic" "psyntax". - Token "'". - - - - diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v index 1b6bc0b38..e4aaa49c2 100644 --- a/contrib/correctness/examples/exp.v +++ b/contrib/correctness/examples/exp.v @@ -149,7 +149,7 @@ Correctness i_exp let e = ref n in begin while (notzerop_bool !e) do - { invariant (power x n)=(mult y (power m e)) as I + { invariant (power x n)=(mult y (power m e)) as Inv variant e for lt } (if not (even_odd_bool !e) then y := (mult !y !m)) { (power x n) = (mult y (power m (double (div2 e)))) as Q }; @@ -161,11 +161,10 @@ Correctness i_exp { result=(power x n) } . Proof. -Rewrite (odd_double e0 Test1) in I. Rewrite I. Simpl. Auto with arith. +stop. +Rewrite (odd_double e0 Test1) in Inv. Rewrite Inv. Simpl. Auto with arith. -Rewrite (even_double e0 Test1) in I. Rewrite I. Reflexivity. - -Split. +Rewrite (even_double e0 Test1) in Inv. Rewrite Inv. Reflexivity. Exact (lt_div2 e0 Test2). @@ -177,8 +176,8 @@ Rewrite (power_2n m0 (div2 e0)). Reflexivity. Auto with arith. -Decompose [and] I. -Rewrite H0. Rewrite H1. +Decompose [and] Inv. +Rewrite H. Rewrite H0. Auto with arith. Save. diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v index dc55eafa1..e6beecccf 100644 --- a/contrib/correctness/examples/exp_int.v +++ b/contrib/correctness/examples/exp_int.v @@ -27,7 +27,7 @@ Require Zpower. Require Zcomplements. -Require Programs. +Require Correctness. Require ZArithRing. Require Omega. @@ -52,12 +52,12 @@ Intro. Absurd `0 > 0`; [ Omega | Assumption ]. Destruct p; Auto with zarith. Simpl. -Intro p. +Intro p0. Replace (POS (xI p0)) with `2*(POS p0)+1`. Omega. Simpl. Auto with zarith. -Intro p. +Intro p0. Simpl. Replace (POS (xO p0)) with `2*(POS p0)`. Omega. @@ -120,7 +120,7 @@ Correctness i_exp let e = ref n in begin while !e > 0 do - { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as I + { invariant (Zpower x n)=(Zmult y (Zpower m e)) /\ `e>=0` as Inv variant e } (if not (Zeven_odd_bool !e) then y := (Zmult !y !m)) { (Zpower x n) = (Zmult y (Zpower m (Zdouble (Zdiv2 e)))) as Q }; diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml index cf233a988..4395aa53a 100644 --- a/contrib/correctness/pcic.ml +++ b/contrib/correctness/pcic.ml @@ -185,10 +185,11 @@ let rawconstr_of_prog p = let args = tyl @ cl in RApp (dummy_loc, RRef (dummy_loc, tuple), args) - | CC_case (_,b,el) -> + | CC_case (ty,b,el) -> let c = trad avoid nenv b in let cl = List.map (trad avoid nenv) el in - ROldCase (dummy_loc, false, None, c, Array.of_list cl) + let ty = Detyping.detype avoid nenv ty in + ROldCase (dummy_loc, false, Some ty, c, Array.of_list cl) | CC_expr c -> Detyping.detype avoid nenv c diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml index 77356e17c..d6a15959b 100644 --- a/contrib/correctness/pmisc.ml +++ b/contrib/correctness/pmisc.ml @@ -17,8 +17,6 @@ open Term module SpSet = Set.Make(struct type t = section_path let compare = sp_ord end) -let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI - (* debug *) let debug = ref false @@ -148,6 +146,12 @@ let real_subst_in_constr = replace_vars (* Coq constants *) +let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI + +let bool_sp = coq_constant ["Init"; "Datatypes"] "bool" +let coq_true = mkMutConstruct (((bool_sp,0),1), [||]) +let coq_false = mkMutConstruct (((bool_sp,0),2), [||]) + let constant s = let id = id_of_string s in Declare.global_reference CCI id diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli index 96519ee9f..a4359b6d8 100644 --- a/contrib/correctness/pmisc.mli +++ b/contrib/correctness/pmisc.mli @@ -15,8 +15,6 @@ open Term module SpSet : Set.S with type elt = section_path -val coq_constant : string list -> string -> section_path - (* Some misc. functions *) val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b @@ -57,8 +55,12 @@ val subst_ast_in_ast : (identifier * Coqast.t) list -> Coqast.t -> Coqast.t val real_subst_in_constr : (identifier * constr) list -> constr -> constr val constant : string -> constr +val coq_constant : string list -> string -> section_path val conj : constr -> constr -> constr +val coq_true : constr +val coq_false : constr + val connective_and : identifier val connective_or : identifier val connective_not : identifier diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml index 9d69ecdcb..49d8d9bf7 100644 --- a/contrib/correctness/pmonad.ml +++ b/contrib/correctness/pmonad.ml @@ -402,14 +402,19 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c = *) let make_if_case ren env ty (b,qb) (br1,br2) = - let ty',id_b = match qb with + let id_b,ty',ty1,ty2 = match qb with | Some q -> let q = apply_post ren env (current_date ren) q in let (name,t1,t2) = Term.destLambda q.a_value in - Term.mkLambda (name, t1, (mkArrow t2 ty)), q.a_name + q.a_name, + Term.mkLambda (name, t1, mkArrow t2 ty), + Term.mkApp (q.a_value, [| coq_true |]), + Term.mkApp (q.a_value, [| coq_false |]) | None -> assert false in - CC_app (CC_case (ty', b, [br1;br2]), + let n = test_name Anonymous in + CC_app (CC_case (ty', b, [CC_lam ([n,CC_typed_binder ty1], br1); + CC_lam ([n,CC_typed_binder ty2], br2)]), [CC_var (post_name id_b)]) let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c = @@ -436,17 +441,10 @@ let make_if ren env (tb,cb) ren' (t1,c1) (t2,c2) c = in let t1,ty1 = branch c1 t1 in let t2,ty2 = branch c2 t2 in - let t1,t2 = - let n = test_name Anonymous in - CC_lam ([n,CC_untyped_binder],t1), - CC_lam ([n,CC_untyped_binder],t2) in let ty = ty1 in let qb = force_bool_name qb in let t = make_if_case ren env ty (CC_var resb,qb) (t1,t2) in - let t = - make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) - in - t + make_let_in ren env tb pb (current_vars ren' wb,qb) (resb,tyb) (t,ty) (* [make_while ren env (cphi,r,a) (tb,cb) (te,ce) c] @@ -509,10 +507,6 @@ let make_body_while ren env phi_of a r id_phi0 id_w (tb,cb) tbl (i,c) = (CC_expr (constant "tt"),constant "unit") (ef,is) in - let t1,t2 = - let n = test_name Anonymous in - CC_lam ([n,CC_untyped_binder],t1), - CC_lam ([n,CC_untyped_binder],t2) in let b_al = current_vars ren' (get_reads eb) in let qb = force_bool_name qb in let t = make_if_case ren' env ty (CC_var resb,qb) (t1,t2) in diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4 index 64a291026..80399858c 100644 --- a/contrib/correctness/psyntax.ml4 +++ b/contrib/correctness/psyntax.ml4 @@ -94,7 +94,7 @@ let ast_of_int n = let constr_of_int n = Astterm.interp_constr Evd.empty (Global.env ()) (ast_of_int n) -let ast_constant loc s = <:ast< ($VAR $s) >> +let ast_constant loc s = <:ast< (QUALID ($VAR $s)) >> let conj_assert {a_name=n;a_value=a} {a_value=b} = let loc = Ast.loc a in diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml index 45ab72c38..950ef30b5 100644 --- a/contrib/correctness/ptactic.ml +++ b/contrib/correctness/ptactic.ml @@ -98,7 +98,7 @@ open Equality let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0) let lt = ConstRef (coq_constant ["Init";"Peano"] "lt") let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded") -let z = IndRef (coq_constant ["Init";"fast_integer"] "Z", 0) +let z = IndRef (coq_constant ["Zarith";"fast_integer"] "Z", 0) let and_ = IndRef (coq_constant ["Init";"Logic"] "and", 0) let eq = IndRef (coq_constant ["Init";"Logic"] "eq", 0) @@ -107,7 +107,7 @@ let wf_nat_pattern = PApp (PRef well_founded, [| PRef nat; PRef lt |]) (* ["((well_founded Z (Zwf ?1))"] *) let wf_z_pattern = - let zwf = ConstRef (coq_constant ["correctness";"Zwf"] "Zwf") in + let zwf = ConstRef (coq_constant ["correctness";"ProgWf"] "Zwf") in PApp (PRef well_founded, [| PRef z; PApp (PRef zwf, [| PMeta (Some 1) |]) |]) (* ["(and ?1 ?2)"] *) let and_pattern = @@ -252,14 +252,9 @@ let wrap_save_named b = Command.save_named b; register pf_id None -let wrap_save_anonymous_thm b id = +let wrap_save_anonymous b id = let pf_id = Pfedit.get_current_proof_name () in - Command.save_anonymous_thm b (string_of_id id); - register pf_id (Some id) - -let wrap_save_anonymous_remark b id = - let pf_id = Pfedit.get_current_proof_name () in - Command.save_anonymous_remark b (string_of_id id); + Command.save_anonymous b (string_of_id id); register pf_id (Some id) let _ = add "SaveNamed" @@ -272,14 +267,9 @@ let _ = add "DefinedNamed" wrap_save_named false) | _ -> assert false) -let _ = add "SaveAnonymousThm" +let _ = add "SaveAnonymous" (function [VARG_IDENTIFIER id] -> (fun () -> if not(Options.is_silent()) then show_script(); - wrap_save_anonymous_thm true id) + wrap_save_anonymous true id) | _ -> assert false) -let _ = add "SaveAnonymousRmk" - (function [VARG_IDENTIFIER id] -> - (fun () -> if not(Options.is_silent()) then show_script(); - wrap_save_anonymous_remark true id) - | _ -> assert false) diff --git a/contrib/extraction/Extraction.v b/contrib/extraction/Extraction.v index c4c62b3cb..e909d4511 100644 --- a/contrib/extraction/Extraction.v +++ b/contrib/extraction/Extraction.v @@ -12,10 +12,10 @@ Grammar vernac vernac : ast := | extr_list [ "Recursive" "Extraction" ne_qualidarg_list($l) "." ] -> [ (ExtractionRec ($LIST $l)) ] | extr_list - [ "Extraction" options($o) stringarg($f) ne_qualidarg_list($l) "." ] + [ "Extraction" stringarg($f) options($o) ne_qualidarg_list($l) "." ] -> [ (ExtractionFile $o $f ($LIST $l)) ] | extr_module - [ "Extraction" options($o) "Module" identarg($m) "." ] + [ "Extraction" "Module" options($o) identarg($m) "." ] -> [ (ExtractionModule $o $m) ] | extract_constant @@ -39,7 +39,7 @@ with idorstring : ast := | ids_string [ stringarg($s) ] -> [ $s ] with options : ast := -| ext_opt_noopt [ "noopt" ] -> [ (VERNACARGLIST "noopt") ] -| ext_op_expand [ "expand" "[" ne_qualidarg_list($l) "]" ] -> +| ext_opt_noopt [ "[" "noopt" "]" ] -> [ (VERNACARGLIST "noopt") ] +| ext_op_expand [ "[" "expand" ne_qualidarg_list($l) "]" ] -> [ (VERNACARGLIST "expand" ($LIST $l)) ] | ext_opt_none [ ] -> [ (VERNACARGLIST "nooption") ]. diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index b0bb1ad3a..616591048 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -161,13 +161,13 @@ let _ = let interp_options keep modular = function | [VARG_STRING "noopt"] -> - { no_opt = true; modular = modular; + { optimization = false; modular = modular; to_keep = refs_set_of_list keep; to_expand = Refset.empty } | [VARG_STRING "nooption"] -> - { no_opt = false; modular = modular; + { optimization = not modular; modular = modular; to_keep = refs_set_of_list keep; to_expand = Refset.empty } | VARG_STRING "expand" :: l -> - { no_opt = false; modular = modular; + { optimization = not modular; modular = modular; to_keep = refs_set_of_list keep; to_expand = refs_set_of_list (refs_of_vargl l) } | _ -> diff --git a/contrib/extraction/mlutil.ml b/contrib/extraction/mlutil.ml index 4b04c4dec..b7a07c706 100644 --- a/contrib/extraction/mlutil.ml +++ b/contrib/extraction/mlutil.ml @@ -202,26 +202,29 @@ module Refset = type extraction_params = { modular : bool; (* modular extraction *) - no_opt : bool; (* no optimization at all *) + optimization : bool; (* we need optimization *) to_keep : Refset.t; (* globals to keep *) to_expand : Refset.t; (* globals to expand *) } -let ml_subst_glob r m = +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 -let expand r m = function - | Dglob(r',t') -> Dglob(r', ml_subst_glob r m t') +let subst_glob_decl r m = function + | Dglob(r',t') -> Dglob(r', subst_glob_ast r m t') | d -> d let normalize = betared_ast -let keep prm r t' = true - (* prm.no_opt || Refset.mem r prm.to_keep *) +let expansion_test r t = false + +let expand prm r t = + (not (Refset.mem r prm.to_keep)) && + (Refset.mem r prm.to_expand || (prm.optimization && expansion_test r t)) let warning_expansion r = wARN (hOV 0 [< 'sTR "The constant"; 'sPC; @@ -240,13 +243,12 @@ let rec optimize prm = function let t' = normalize t in [ Dglob(r,t') ] | Dglob(r,t) as d :: l -> let t' = normalize t in - if keep prm r t' then - (Dglob(r,t')) :: (optimize prm l) - else begin + if expand prm r t' then begin warning_expansion r; - let l' = List.map (expand r t') l in + let l' = List.map (subst_glob_decl r t') l in optimize prm l' - end + end else + (Dglob(r,t')) :: (optimize prm l) (*s Table for direct ML extractions. *) diff --git a/contrib/extraction/mlutil.mli b/contrib/extraction/mlutil.mli index af931b648..f4aae3b7f 100644 --- a/contrib/extraction/mlutil.mli +++ b/contrib/extraction/mlutil.mli @@ -45,7 +45,7 @@ module Refset : Set.S with type elt = global_reference type extraction_params = { modular : bool; (* modular extraction *) - no_opt : bool; (* no optimization at all *) + optimization : bool; (* we need optimization *) to_keep : Refset.t; (* globals to keep *) to_expand : Refset.t; (* globals to expand *) } |