diff options
| -rw-r--r-- | contrib/xml/proof2aproof.ml | 2 | ||||
| -rw-r--r-- | proofs/logic.ml | 75 | ||||
| -rw-r--r-- | proofs/logic.mli | 8 | ||||
| -rw-r--r-- | proofs/refiner.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/Rename.v | 13 |
5 files changed, 72 insertions, 28 deletions
diff --git a/contrib/xml/proof2aproof.ml b/contrib/xml/proof2aproof.ml index f78df74789..dff546c948 100644 --- a/contrib/xml/proof2aproof.ml +++ b/contrib/xml/proof2aproof.ml @@ -117,7 +117,7 @@ let extract_open_proof sigma pf = (fun id -> (* Section variables are in the [id] list but are not *) (* lambda abstracted in the term [vl] *) - try let n = Util.list_index id vl in (n,id) + try let n = Logic.proof_variable_index id vl in (n,id) with Not_found -> failwith "caught") (*CSC: the above function must be modified such that when it is found *) (*CSC: it becomes a Rel; otherwise a Var. Then it can be already used *) diff --git a/proofs/logic.ml b/proofs/logic.ml index ee9959a695..071e44b5be 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -535,15 +535,39 @@ let prim_refiner r sigma goal = (* Extracting a proof term from the proof tree *) (* Util *) + +type variable_proof_status = ProofVar | SectionVar of identifier + +type proof_variable = name * variable_proof_status + +let subst_proof_vars = + let rec aux p vars = + let _,subst = + List.fold_left (fun (n,l) var -> + let t = match var with + | Anonymous,_ -> l + | Name id, ProofVar -> (id,mkRel n)::l + | Name id, SectionVar id' -> (id,mkVar id')::l in + (n+1,t)) (p,[]) vars + in replace_vars (List.rev subst) + in aux 1 + let rec rebind id1 id2 = function - | [] -> [] - | id::l -> - if id = id1 then id2::l else + | [] -> [Name id2,SectionVar id1] + | (na,_ as x)::l -> + if na = Name id1 then (Name id2,ProofVar)::l else let l' = rebind id1 id2 l in - if id = id2 then - (* TODO: find a more elegant way to hide a variable *) - (id_of_string "_@")::l' - else id::l' + if na = Name id2 then (Anonymous,ProofVar)::l' else x::l' + +let add_proof_var id vl = (Name id,ProofVar)::vl + +let proof_variable_index x = + let rec aux n = function + | (Name id,ProofVar)::l when x = id -> n + | _::l -> aux (n+1) l + | [] -> raise Not_found + in + aux 1 let prim_extractor subfun vl pft = let cl = pft.goal.evar_concl in @@ -551,50 +575,53 @@ let prim_extractor subfun vl pft = | Some (Prim (Intro id), [spf]) -> (match kind_of_term (strip_outer_cast cl) with | Prod (_,ty,_) -> - let cty = subst_vars vl ty in - mkLambda (Name id, cty, subfun (id::vl) spf) + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) | LetIn (_,b,ty,_) -> - let cb = subst_vars vl b in - let cty = subst_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (id::vl) spf) + let cb = subst_proof_vars vl b in + let cty = subst_proof_vars vl ty in + mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "incomplete proof!") | Some (Prim (Intro_replacing id),[spf]) -> (match kind_of_term (strip_outer_cast cl) with | Prod (_,ty,_) -> - let cty = subst_vars vl ty in - mkLambda (Name id, cty, subfun (id::vl) spf) + let cty = subst_proof_vars vl ty in + mkLambda (Name id, cty, subfun (add_proof_var id vl) spf) | LetIn (_,b,ty,_) -> - let cb = subst_vars vl b in - let cty = subst_vars vl ty in - mkLetIn (Name id, cb, cty, subfun (id::vl) spf) + let cb = subst_proof_vars vl b in + let cty = subst_proof_vars vl ty in + mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf) | _ -> error "incomplete proof!") | Some (Prim (Cut (b,id,t)),[spf1;spf2]) -> let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in - mkLetIn (Name id,subfun vl spf1,subst_vars vl t,subfun (id::vl) spf2) + mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t, + subfun (add_proof_var id vl) spf2) | Some (Prim (FixRule (f,n,others)),spfl) -> let all = Array.of_list ((f,n,cl)::others) in - let lcty = Array.map (fun (_,_,ar) -> subst_vars vl ar) all in + let lcty = Array.map (fun (_,_,ar) -> subst_proof_vars vl ar) all in let names = Array.map (fun (f,_,_) -> Name f) all in let vn = Array.map (fun (_,n,_) -> n-1) all in - let newvl = List.fold_left (fun vl (id,_,_)->(id::vl)) (f::vl)others in + let newvl = List.fold_left (fun vl (id,_,_) -> add_proof_var id vl) + (add_proof_var f vl) others in let lfix = Array.map (subfun newvl) (Array.of_list spfl) in mkFix ((vn,0),(names,lcty,lfix)) | Some (Prim (Cofix (f,others)),spfl) -> let all = Array.of_list ((f,cl)::others) in - let lcty = Array.map (fun (_,ar) -> subst_vars vl ar) all in + let lcty = Array.map (fun (_,ar) -> subst_proof_vars vl ar) all in let names = Array.map (fun (f,_) -> Name f) all in - let newvl = List.fold_left (fun vl (id,_)->(id::vl)) (f::vl) others in + let newvl = List.fold_left (fun vl (id,_)-> add_proof_var id vl) + (add_proof_var f vl) others in let lfix = Array.map (subfun newvl) (Array.of_list spfl) in mkCoFix (0,(names,lcty,lfix)) | Some (Prim (Refine c),spfl) -> let mvl = collect_meta_variables c in let metamap = List.combine mvl (List.map (subfun vl) spfl) in - let cc = subst_vars vl c in + let cc = subst_proof_vars vl c in plain_instance metamap cc (* Structural and conversion rules do not produce any proof *) @@ -605,7 +632,7 @@ let prim_extractor subfun vl pft = subfun vl pf | Some (Prim (Thin _),[pf]) -> - (* No need to make ids Anonymous in vl: subst_vars take the more recent *) + (* No need to make ids Anon in vl: subst_proof_vars take the most recent*) subfun vl pf | Some (Prim (ThinBody _),[pf]) -> diff --git a/proofs/logic.mli b/proofs/logic.mli index 906fef0171..4af70cfb72 100644 --- a/proofs/logic.mli +++ b/proofs/logic.mli @@ -36,9 +36,13 @@ val with_check : tactic -> tactic val prim_refiner : prim_rule -> evar_map -> goal -> goal list +type proof_variable + val prim_extractor : - (identifier list -> proof_tree -> constr) - -> identifier list -> proof_tree -> constr + (proof_variable list -> proof_tree -> constr) + -> proof_variable list -> proof_tree -> constr + +val proof_variable_index : identifier -> proof_variable list -> int (*s Refiner errors. *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index dd719e48e4..f4ed6694e5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -282,7 +282,7 @@ let extract_open_proof sigma pf = let visible_rels = map_succeed (fun id -> - try let n = list_index id vl in (n,id) + try let n = proof_variable_index id vl in (n,id) with Not_found -> failwith "caught") (ids_of_named_context (named_context_of_val goal.evar_hyps)) in let sorted_rels = diff --git a/test-suite/success/Rename.v b/test-suite/success/Rename.v index 8a5db157c0..0576f3c68f 100644 --- a/test-suite/success/Rename.v +++ b/test-suite/success/Rename.v @@ -3,3 +3,16 @@ intros. rename n into p. induction p; auto. Qed. + +(* Submitted by Iris Loeb (#842) *) + +Section rename. + +Variable A:Prop. + +Lemma Tauto: A->A. +rename A into B. +tauto. +Qed. + +End rename. |