diff options
Diffstat (limited to 'contrib/subtac')
-rw-r--r-- | contrib/subtac/eterm.ml | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_command.ml | 50 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.ml | 116 | ||||
-rw-r--r-- | contrib/subtac/subtac_obligations.mli | 2 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.ml | 3 | ||||
-rw-r--r-- | contrib/subtac/subtac_utils.mli | 1 | ||||
-rw-r--r-- | contrib/subtac/test/Mutind.v | 25 | ||||
-rw-r--r-- | contrib/subtac/test/euclid.v | 82 |
8 files changed, 125 insertions, 157 deletions
diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index 790e61a0a..8ec173630 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -141,7 +141,8 @@ let eterm_obligations name nclen evm t tycon = let hyps = trunc_named_context nclen hyps in trace (str "Named context is: " ++ Printer.pr_named_context (Global.env ()) hyps); let evtyp, deps = etype_of_evar l ev hyps in - trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp); + trace (str "Evar " ++ str (string_of_int n) ++ str "'s type is: " ++ Termops.print_constr_env (Global.env ()) evtyp ++ + str " depends on evars : " ++ str (Subtac_utils.string_of_intset deps)); let y' = (id, ((n, nstr), hyps, evtyp, deps)) in y' :: l) evn [] diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 955ee8ac2..43d6fcdec 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -364,52 +364,6 @@ let build_mutrec l boxed = let (lnonrec,(namerec,defrec,arrec,nvrec)) = collect_non_rec env lrecnames recdef arityl nv in - let declare arrec defrec = - let recvec = - Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in - let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in - let rec declare i fi = - (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ - my_print_constr env (recvec.(i))); - with _ -> ()); - let ce = - { const_entry_body = mkFix ((nvrec,i),recdecls); - const_entry_type = Some arrec.(i); - const_entry_opaque = false; - const_entry_boxed = boxed} in - let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) - in (ConstRef kn) - in - (* declare the recursive definitions *) - let lrefrec = Array.mapi declare namerec in - Options.if_verbose ppnl (recursive_message lrefrec); - - - (*(* The others are declared as normal definitions *) - let var_subst id = (id, Constrintern.global_reference id) in - let _ = - List.fold_left - (fun subst (f,def,t) -> - let ce = { const_entry_body = replace_vars subst def; - const_entry_type = Some t; - const_entry_opaque = false; - const_entry_boxed = boxed } in - let _ = - Declare.declare_constant f (DefinitionEntry ce,IsDefinition Definition) - in - warning ((string_of_id f)^" is non-recursively defined"); - (var_subst f) :: subst) - (List.map var_subst (Array.to_list namerec)) - lnonrec - in*) - List.iter (fun (df,c,scope) -> - Metasyntax.add_notation_interpretation df [] c scope) notations - in - let declare l = - let recvec = Array.of_list l - and arrec = Array.map pi3 arrec - in declare arrec recvec - in let recdefs = Array.length defrec in trace (int recdefs ++ str " recursive definitions"); (* Solve remaining evars *) @@ -430,11 +384,11 @@ let build_mutrec l boxed = Termops.it_mkNamedProd_or_LetIn typ (Environ.named_context rec_sign) in let evars, def = Eterm.eterm_obligations id nc_len evm def (Some typ) in - collect_evars (succ i) ((id, def, typ, evars) :: acc) + collect_evars (succ i) ((id, nvrec.(i), def, typ, evars) :: acc) else acc in let defs = collect_evars 0 [] in - Subtac_obligations.add_mutual_definitions defs + Subtac_obligations.add_mutual_definitions (List.rev defs) let out_n = function Some n -> n diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index 8bb79a785..e2192f28d 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -28,7 +28,7 @@ type program_info = { prg_body: constr; prg_type: constr; prg_obligations: obligations; - prg_deps : identifier list; + prg_deps : (identifier * int) list; } let evar_of_obligation o = { evar_hyps = Environ.empty_named_context_val ; @@ -40,7 +40,13 @@ let subst_deps obls deps t = Intset.fold (fun x acc -> let xobl = obls.(x) in - let oblb = out_some xobl.obl_body in + debug 3 (str "Trying to get body of obligation " ++ int x); + let oblb = + try out_some xobl.obl_body + with _ -> + debug 3 (str "Couldn't get body of obligation " ++ int x); + assert(false) + in Term.subst1 oblb (Term.subst_var xobl.obl_name acc)) deps t @@ -108,41 +114,49 @@ let declare_definition prg = in Subtac_utils.definition_message prg.prg_name -let declare_mutual_definition l = assert(false) - (*let len = List.length l in - let namerec = List.map (fun x -> x.prg_name) l in - let arrrec = - Array.of_list (List.map (fun x -> x.prg_type) l) +open Pp +open Ppconstr + +let declare_mutual_definition l = + let len = List.length l in + let l, nvlist = List.split l in + let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in + let arrec = + Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) in - let defrec = - Array.of_list (List.map (fun x -> subst_body x) l) + let recvec = + Array.of_list + (List.map (fun x -> + let subs = (subst_body x) in + snd (decompose_lam_n len subs)) l) in - let recvec = Array.map (subst_vars (List.rev namerec)) defrec in - let recdecls = (Array.of_list (List.map (fun id -> Name id) namerec), arrec, recvec) in + let nvrec = Array.of_list nvlist in + let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = (try trace (str "Declaring: " ++ pr_id fi ++ spc () ++ - my_print_constr env (recvec.(i))); + my_print_constr (Global.env()) (recvec.(i))); with _ -> ()); let ce = { const_entry_body = mkFix ((nvrec,i),recdecls); const_entry_type = Some arrec.(i); const_entry_opaque = false; - const_entry_boxed = boxed} in + const_entry_boxed = true} in let kn = Declare.declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint) in ConstRef kn in let lrefrec = Array.mapi declare namerec in Options.if_verbose ppnl (recursive_message lrefrec) - *) + let declare_obligation obl body = let ce = { const_entry_body = body; const_entry_type = Some obl.obl_type; - const_entry_opaque = true; + const_entry_opaque = false; const_entry_boxed = false} in - let constant = Declare.declare_constant obl.obl_name (DefinitionEntry ce,IsProof Property) + let constant = Declare.declare_constant obl.obl_name + (DefinitionEntry ce,IsProof Property) in Subtac_utils.definition_message obl.obl_name; { obl with obl_body = Some (mkConst constant) } @@ -163,36 +177,17 @@ let try_tactics obls = let init_prog_info n b t deps obls = let obls' = - Array.map - (fun (n, t, d) -> + Array.mapi + (fun i (n, t, d) -> + debug 2 (str "Adding obligation " ++ int i ++ str " with deps : " ++ str (string_of_intset d)); { obl_name = n ; obl_body = None; obl_type = t; obl_deps = d }) obls in { prg_name = n ; prg_body = b; prg_type = t; prg_obligations = (obls', Array.length obls'); prg_deps = deps } - -let add_definition n b t obls = - Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n b t [] obls in - let obls,_ = prg.prg_obligations in - if Array.length obls = 0 then ( - Options.if_verbose ppnl (str "."); - declare_definition prg) - else ( - let len = Array.length obls in - let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in - from_prg := ProgMap.add n prg !from_prg) - -let add_mutual_definitions l = - let deps = List.map (fun (n, b, t, obls) -> n) l in - let upd = List.fold_left - (fun acc (n, b, t, obls) -> - let prg = init_prog_info n b t deps obls in - ProgMap.add n prg acc) - !from_prg l - in from_prg := upd -let error s = Util.error s +let pperror cmd = Util.errorlabstrm "Subtac" cmd +let error s = pperror (str s) let get_prog name = let prg_infos = !from_prg in @@ -209,18 +204,45 @@ let obligations_solved prg = (snd prg.prg_obligations) = 0 let update_obls prg obls rem = let prg' = { prg with prg_obligations = (obls, rem) } in - if rem > 1 then ( - debug 2 (int rem ++ str " obligations remaining"); - from_prg := map_replace prg.prg_name prg' !from_prg) + from_prg := map_replace prg.prg_name prg' !from_prg; + if rem > 0 then ( + Options.if_verbose ppnl (int rem ++ str " obligation(s) remaining"); + ) else ( + debug 2 (str "No more obligations remaining"); match prg'.prg_deps with [] -> declare_definition prg'; from_prg := ProgMap.remove prg.prg_name !from_prg | l -> - if List.for_all (fun x -> obligations_solved (ProgMap.find x !from_prg)) prg'.prg_deps then - declare_mutual_definition (List.map (fun x -> ProgMap.find x !from_prg) prg'.prg_deps) - ) + let progs = List.map (fun (x,y) -> ProgMap.find x !from_prg, y) prg'.prg_deps in + if List.for_all (fun x -> obligations_solved (fst x)) progs then + declare_mutual_definition progs) + +let add_definition n b t obls = + Options.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); + let prg = init_prog_info n b t [] obls in + let obls,_ = prg.prg_obligations in + if Array.length obls = 0 then ( + Options.if_verbose ppnl (str "."); + declare_definition prg) + else ( + let len = Array.length obls in + let _ = Options.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in + from_prg := ProgMap.add n prg !from_prg) + +let add_mutual_definitions l = + let deps = List.map (fun (n, nclen, b, t, obls) -> n, nclen) l in + let upd = List.fold_left + (fun acc (n, nclen, b, t, obls) -> + let prg = init_prog_info n b t deps obls in + ProgMap.add n prg acc) + !from_prg l + in + from_prg := upd; + let prg = (ProgMap.find (fst (List.hd deps)) !from_prg) in + let o, r = prg.prg_obligations in + update_obls prg o r let is_defined obls x = obls.(x).obl_body <> None @@ -251,7 +273,7 @@ let subtac_obligation (user_num, name) = let _ = obls.(num) <- obl in update_obls prg obls (pred rem)); trace (str "Started obligation " ++ int user_num ++ str " proof") - | l -> msgnl (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " + | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l))) | Some r -> error "Obligation already solved" else error (sprintf "Unknown obligation number %i" (succ num)) diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index a8039300a..6ba479764 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -6,7 +6,7 @@ val add_definition : Names.identifier -> Term.constr -> Term.types -> obligation_info -> unit val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * obligation_info) list -> unit + (Names.identifier * int * Term.constr * Term.types * obligation_info) list -> unit val subtac_obligation : int * Names.identifier option -> unit diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index b196bf913..8164910f2 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -591,3 +591,6 @@ let rec string_of_list sep f = function [] -> "" | x :: [] -> f x | x :: ((y :: _) as tl) -> f x ^ sep ^ string_of_list sep f tl + +let string_of_intset d = + string_of_list "," string_of_int (Intset.elements d) diff --git a/contrib/subtac/subtac_utils.mli b/contrib/subtac/subtac_utils.mli index ebfc51232..86662c478 100644 --- a/contrib/subtac/subtac_utils.mli +++ b/contrib/subtac/subtac_utils.mli @@ -98,3 +98,4 @@ val recursive_message : global_reference array -> std_ppcmds val solve_by_tac : evar_info -> Tacmach.tactic -> constr val string_of_list : string -> ('a -> string) -> 'a list -> string +val string_of_intset : Intset.t -> string diff --git a/contrib/subtac/test/Mutind.v b/contrib/subtac/test/Mutind.v index 0b40ef82a..8a9bec52f 100644 --- a/contrib/subtac/test/Mutind.v +++ b/contrib/subtac/test/Mutind.v @@ -1,13 +1,28 @@ -Program Fixpoint f (a : nat) : nat := +Program Fixpoint f (a : nat) : { x : nat | x > 0 } := match a with - | 0 => 0 + | 0 => 1 | S a' => g a a' end -with g (a b : nat) { struct b } : nat := +with g (a b : nat) { struct b } : { x : nat | x > 0 } := match b with - | 0 => 0 + | 0 => 1 | S b' => f b' end. +Obligations of f. + +Obligation 1 of f. + simpl ; intros ; auto with arith. +Defined. + +Obligation 1 of g. + simpl ; intros ; auto with arith. +Defined. + Check f. -Check g.
\ No newline at end of file +Check g. + + + + + diff --git a/contrib/subtac/test/euclid.v b/contrib/subtac/test/euclid.v index c14edad55..7fa80fbd0 100644 --- a/contrib/subtac/test/euclid.v +++ b/contrib/subtac/test/euclid.v @@ -11,71 +11,43 @@ Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : Obligations. -Definition t := fun (Evar46 : forall a : nat, (fun y : nat => @eq nat a y) a) (a : nat) => -@existS nat (fun x : nat => @sig nat (fun y : nat => @eq nat x y)) a - (@exist nat (fun y : nat => @eq nat a y) a (Evar46 a)). - -Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } := - (a & a). +Require Import Coq.subtac.Utils. +Require Import Coq.subtac.FixSub. +Require Import Omega. Obligation 1. -intros ; simpl ; auto. + simpl ; intros. + destruct_exists ; simpl in * ; auto with arith. + omega. Qed. -Solve Obligations using auto. -reflexivity. -Defined. - -Extraction testsig. -Extraction sig. -Extract Inductive sig => "" [ "" ]. -Extraction testsig. - -Require Import Coq.Arith.Compare_dec. +Obligation 2 of euclid. + simpl ; intros. + destruct_exists ; simpl in * ; auto with arith. + assert(x0 * S q' = x0 * q' + x0) by auto with arith ; omega. +Qed. -Require Import Omega. +Obligation 4 of euclid. + exact Wf_nat.lt_wf. +Qed. -Lemma minus_eq_add : forall x y z w, y <= x -> x - y = y * z + w -> x = y * S z + w. -intros. -assert(y * S z = y * z + y). -auto. -rewrite H1. -omega. +Obligation 3 of euclid. + simpl ; intros. + destruct_exists ; simpl in *. + omega. Qed. -Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : - { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in - (S q' & r) - else (O & a). -intro euclid. -simpl ; intros. -Print euclid_evars. -eapply euclid_evars with euclid. -refine (euclid_evars _ _ _ euclid a Acc_a b). -; simpl ; intros. -Show Existentials. +Extraction Inline Fix_sub Fix_F_sub. +Extract Inductive sigT => "pair" [ "" ]. +Extract Inductive sumbool => "bool" [ "true" "false" ]. +Extraction le_lt_dec. +Extraction euclid. -induction b0 ; induction r. -simpl in H. -simpl. -simpl in p0. -destruct p0. -split. -apply minus_eq_add. -omega. -auto with arith. -auto. -simpl. -induction b0 ; simpl. -split ; auto. -omega. -exact (euclid a0 Acc_a0 b0). +Program Definition testsig (a : nat) : { x : nat & { y : nat | x = y } } := + (a & a). -exact (Acc_a). -auto. -auto. -Focus 1. +Solve Obligations using simpl ; auto. +Extraction testsig. |