diff options
| -rw-r--r-- | proofs/logic.ml | 170 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 1 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 1 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 3 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 1 | ||||
| -rw-r--r-- | tactics/tactics.ml | 45 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldfail/1898.v | 5 |
7 files changed, 179 insertions, 47 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 48ed610b9..391d6f466 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -62,27 +62,14 @@ let rec catchable_exception = function (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true | _ -> false +let error_no_such_hypothesis id = + error ("No such hypothesis: " ^ string_of_id id ^ ".") + (* Tells if the refiner should check that the submitted rules do not produce invalid subgoals *) let check = ref false let with_check = Flags.with_option check -(************************************************************************) -(************************************************************************) -(* Implementation of the structural rules (moving and deleting - hypotheses around) *) - -(* The Clear tactic: it scans the context for hypotheses to be removed - (instead of iterating on the list of identifier to be removed, which - forces the user to give them in order). *) - -let clear_hyps sigma ids sign cl = - let evdref = ref (Evd.create_goal_evar_defs sigma) in - let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in - (hyps,concl,evars_of !evdref) - -(* The ClearBody tactic *) - (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and returns [tail::(f head (id,_,_) (rev tail))] *) let apply_to_hyp sign id f = @@ -100,6 +87,22 @@ let apply_to_hyp_and_dependent_on sign id f g = let check_typability env sigma c = if !check then let _ = type_of env sigma c in () +(************************************************************************) +(************************************************************************) +(* Implementation of the structural rules (moving and deleting + hypotheses around) *) + +(* The Clear tactic: it scans the context for hypotheses to be removed + (instead of iterating on the list of identifier to be removed, which + forces the user to give them in order). *) + +let clear_hyps sigma ids sign cl = + let evdref = ref (Evd.create_goal_evar_defs sigma) in + let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in + (hyps,concl,evars_of !evdref) + +(* The ClearBody tactic *) + let recheck_typability (what,id) env sigma t = try check_typability env sigma t with _ -> @@ -129,6 +132,111 @@ let remove_hyp_body env sigma id = in reset_with_named_context sign env +(* Reordering of the context *) + +(* faire le minimum d'echanges pour que l'ordre donne soit un *) +(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *) +(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *) +(* reculees par rapport aux autres (faire le contraire!) *) + +let mt_q = (Idmap.empty,[]) +let push_val y = function + (_,[] as q) -> q + | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q) +let push_item x v q = + let (m,l) = push_val x q in + (Idmap.add x v m, (x,Idset.empty)::l) +let mem_q x (m,_) = Idmap.mem x m +let rec find_q x (m,q) = + let v = Idmap.find x m in + let m' = Idmap.remove x m in + let rec find accs acc = function + [] -> raise Not_found + | [(x',l)] -> + if x=x' then ((v,Idset.union accs l),(m',List.rev acc)) + else raise Not_found + | (x',l as i)::((x'',l'')::q as itl) -> + if x=x' then + ((v,Idset.union accs l), + (m',List.rev acc@(x'',Idset.union l l'')::q)) + else find (Idset.union l accs) (i::acc) itl in + find Idset.empty [] q + +let occur_vars_in_decl env hyps d = + if Idset.is_empty hyps then false else + let ohyps = global_vars_set_of_decl env d in + Idset.exists (fun h -> Idset.mem h ohyps) hyps + +let reorder_context env sign ord = + let ords = List.fold_right Idset.add ord Idset.empty in + if List.length ord <> Idset.cardinal ords then + error "Order list has duplicates"; + let rec step ord expected ctxt_head moved_hyps ctxt_tail = + match ord with + | [] -> List.rev ctxt_tail @ ctxt_head + | top::ord' when mem_q top moved_hyps -> + let ((d,h),mh) = find_q top moved_hyps in + if occur_vars_in_decl env h d then + errorlabstrm "reorder_context" + (str "Cannot move declaration " ++ pr_id top ++ spc() ++ + str "before " ++ + prlist_with_sep pr_spc pr_id + (Idset.elements (Idset.inter h + (global_vars_set_of_decl env d)))); + step ord' expected ctxt_head mh (d::ctxt_tail) + | _ -> + (match ctxt_head with + | [] -> error_no_such_hypothesis (List.hd ord) + | (x,_,_ as d) :: ctxt -> + if Idset.mem x expected then + step ord (Idset.remove x expected) + ctxt (push_item x d moved_hyps) ctxt_tail + else + step ord expected + ctxt (push_val x moved_hyps) (d::ctxt_tail)) in + step ord ords sign mt_q [] + +let reorder_val_context env sign ord = + val_of_named_context (reorder_context env (named_context_of_val sign) ord) + + +let check_decl_position env sign (x,_,_ as d) = + let needed = global_vars_set_of_decl env d in + let deps = + list_map_filter (fun (id,_,_) -> + if Idset.mem id needed then Some id else None) + (named_context_of_val sign) in + if List.mem x deps then + error ("Cannot create self-referring hypothesis "^string_of_id x); + x::deps + + +(******) +(* older version (performs more swapping) +let reorder_context sign ord = + let ords = List.fold_left Idset.add Idset.empty sign in + let rec step expected moved_hyps ctxt_head ctxt_tail = + if not (Idset.is_empty expected) then + match ctxt_head with + [] -> failwith "some hyps not found" (* those in expected *) + | (x,_,_ as d) :: ctxt -> + if Idset.mem x expected then + step + (Idset.remove x expected) + (Idmap.add x (d,Idset.empty) move_hyps) + ctxt ctxt_tail + else + step expected (push_hyp x moved_hyps) ctxt (d::ctxt_tail) + else begin + (* TODO: check free var constraints *) + let ctxt_mid = + List.map (fun h -> fst (Idmap.find h moved_hyps)) ords + + in List.rev ctxt_tail @ ctxt_mid @ ctxt_head + end in + step ords Idmap.empty sign [] +*) + (* Auxiliary functions for primitive MOVE tactic * * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves @@ -137,9 +245,6 @@ let remove_hyp_body env sigma id = * on the right side [right] if [toleft=false]. * If [with_dep] then dependent hypotheses are moved accordingly. *) -let error_no_such_hypothesis id = - error ("No such hypothesis: " ^ string_of_id id ^ ".") - let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h | (hyp,_,_) :: right -> @@ -360,14 +465,19 @@ and mk_casegoals sigma goal goalacc p c = let convert_hyp sign sigma (id,b,bt as d) = - apply_to_hyp sign id - (fun _ (_,c,ct) _ -> - let env = Global.env_of_context sign in - if !check && not (is_conv env sigma bt ct) then - error ("Incorrect change of the type of "^(string_of_id id)^"."); - if !check && not (Option.Misc.compare (is_conv env sigma) b c) then - error ("Incorrect change of the body of "^(string_of_id id)^"."); - d) + let env = Global.env() in + let reorder = ref [] in + let sign' = + apply_to_hyp sign id + (fun _ (_,c,ct) _ -> + let env = Global.env_of_context sign in + if !check && not (is_conv env sigma bt ct) then + error ("Incorrect change of the type of "^(string_of_id id)^"."); + if !check && not (Option.Misc.compare (is_conv env sigma) b c) then + error ("Incorrect change of the body of "^(string_of_id id)^"."); + if !check then reorder := check_decl_position env sign d; + d) in + reorder_val_context env sign' !reorder (* Normalizing evars in a goal. Called by tactic Local_constraints (i.e. when the sigma of the proof tree changes). Detect if the @@ -522,6 +632,10 @@ let prim_refiner r sigma goal = move_hyp withdep toleft (left,declfrom,right) hto in ([mk_goal hyps' cl], sigma) + | Order ord -> + let hyps' = reorder_val_context env sign ord in + ([mk_goal hyps' cl], sigma) + | Rename (id1,id2) -> if !check & id1 <> id2 && List.mem id2 (ids_of_named_context (named_context_of_val sign)) then @@ -632,7 +746,7 @@ let prim_extractor subfun vl pft = | Some (Prim (ThinBody _),[pf]) -> subfun vl pf - | Some (Prim (Move _),[pf]) -> + | Some (Prim (Move _|Order _),[pf]) -> subfun vl pf | Some (Prim (Rename (id1,id2)),[pf]) -> diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index 6f8aebf0e..dabc84ca3 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -37,6 +37,7 @@ type prim_rule = | Thin of identifier list | ThinBody of identifier list | Move of bool * identifier * identifier move_location + | Order of identifier list | Rename of identifier * identifier | Change_evars diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 2af581a1c..1529a07f3 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -37,6 +37,7 @@ type prim_rule = | Thin of identifier list | ThinBody of identifier list | Move of bool * identifier * identifier move_location + | Order of identifier list | Rename of identifier * identifier | Change_evars diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index bc2cb2b42..45bd0c896 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -202,6 +202,9 @@ let thin_body_no_check ids gl = let move_hyp_no_check with_dep id1 id2 gl = refiner (Prim (Move (with_dep,id1,id2))) gl +let order_hyps idl gl = + refiner (Prim (Order idl)) gl + let rec rename_hyp_no_check l gl = match l with | [] -> tclIDTAC gl | (id1,id2)::l -> diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index a73e79a0c..f57b121db 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -133,6 +133,7 @@ val thin_body_no_check : identifier list -> tactic val move_hyp_no_check : bool -> identifier -> identifier move_location -> tactic val rename_hyp_no_check : (identifier*identifier) list -> tactic +val order_hyps : identifier list -> tactic val mutual_fix : identifier -> int -> (identifier * int * constr) list -> tactic val mutual_cofix : identifier -> (identifier * constr) list -> tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index da4d95eaa..b4371ac23 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -169,6 +169,8 @@ let internal_cut_rev_replace = internal_cut_rev_gen true (* Moving hypotheses *) let move_hyp = Tacmach.move_hyp +let order_hyps = Tacmach.order_hyps + (* Renaming hypotheses *) let rename_hyp = Tacmach.rename_hyp @@ -192,25 +194,28 @@ let cofix = function type tactic_reduction = env -> evar_map -> constr -> constr -(* The following two tactics apply an arbitrary - reduction function either to the conclusion or to a - certain hypothesis *) - -let reduct_in_concl (redfun,sty) gl = - convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl - -let reduct_in_hyp redfun ((_,id),where) gl = - let (_,c, ty) = pf_get_hyp gl id in +let pf_reduce_decl redfun where (id,c,ty) gl = let redfun' = pf_reduce redfun gl in match c with | None -> if where = InHypValueOnly then errorlabstrm "" (pr_id id ++ str "has no value."); - convert_hyp_no_check (id,None,redfun' ty) gl + (id,None,redfun' ty) | Some b -> let b' = if where <> InHypTypeOnly then redfun' b else b in let ty' = if where <> InHypValueOnly then redfun' ty else ty in - convert_hyp_no_check (id,Some b',ty') gl + (id,Some b',ty') + +(* The following two tactics apply an arbitrary + reduction function either to the conclusion or to a + certain hypothesis *) + +let reduct_in_concl (redfun,sty) gl = + convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl + +let reduct_in_hyp redfun ((_,id),where) gl = + convert_hyp_no_check + (pf_reduce_decl redfun where (pf_get_hyp gl id) gl) gl let reduct_option redfun = function | Some id -> reduct_in_hyp (fst redfun) id @@ -238,8 +243,8 @@ let change_on_subterm cv_pb t = function let change_in_concl occl t = reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast) -let change_in_hyp occl t = - reduct_in_hyp (change_on_subterm Reduction.CONV t occl) +let change_in_hyp occl t id = + with_check (reduct_in_hyp (change_on_subterm Reduction.CONV t occl) id) let change_option occl t = function Some id -> change_in_hyp occl t id @@ -276,16 +281,18 @@ let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast) (* A function which reduces accordingly to a reduction expression, as the command Eval does. *) -let needs_check = function +let checking_fun = function (* Expansion is not necessarily well-typed: e.g. expansion of t into x is not well-typed in [H:(P t); x:=t |- G] because x is defined after H *) - | Fold _ -> true - | _ -> false + | Fold _ -> with_check + | Pattern _ -> with_check + | _ -> (fun x -> x) let reduce redexp cl goal = - (if needs_check redexp then with_check else (fun x -> x)) - (redin_combinator (Redexpr.reduction_of_red_expr redexp) cl) - goal + let red = Redexpr.reduction_of_red_expr redexp in + match redexp with + (Fold _|Pattern _) -> with_check (redin_combinator red cl) goal + | _ -> redin_combinator red cl goal (* Unfolding occurrences of a constant *) diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v new file mode 100644 index 000000000..92490eb94 --- /dev/null +++ b/test-suite/bugs/closed/shouldfail/1898.v @@ -0,0 +1,5 @@ +(* folding should not allow circular dependencies *) + +Lemma bug_fold_unfold : True. + set (h := 1). + fold h in h. |