diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 57 | ||||
| -rw-r--r-- | proofs/proof_trees.ml | 6 | ||||
| -rw-r--r-- | proofs/proof_type.ml | 8 | ||||
| -rw-r--r-- | proofs/proof_type.mli | 8 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 17 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 18 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 9 |
7 files changed, 103 insertions, 20 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 3f22a6f8ba..a5fe2d5962 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -266,13 +266,37 @@ let check_forward_dependencies id tail = ^ (string_of_id id'))) tail -let convert_hyp sign sigma id ty = +let convert_hyp sign sigma id b = apply_to_hyp sign id (fun sign (idc,c,ct) _ -> let env = Global.env_of_context sign in - if !check && not (is_conv env sigma ty (body_of_type ct)) then - error "convert-hyp rule passed non-converting term"; - add_named_decl (idc,c,ty) sign) + match c with + | None -> (* Change the type *) + if !check && not (is_conv env sigma b ct) then + error "convert-hyp rule passed non-converting term"; + add_named_decl (idc,c,b) sign + | Some c -> (* Change the body *) + if !check && not (is_conv env sigma b c) then + error "convert-hyp rule passed non-converting term"; + add_named_decl (idc,Some b,ct) sign) + +let convert_def inbody sign sigma id c = + apply_to_hyp sign id + (fun sign (idc,b,t) _ -> + let env = Global.env_of_context sign in + match b with + | None -> error "convert-deftype rule passed to an hyp without body" + | Some b -> + let b,t = + if inbody then + (if !check && not (is_conv env sigma c b) then + error "convert-deftype rule passed non-converting type"; + (c,t)) + else + (if !check && not (is_conv env sigma c t) then + error "convert-deftype rule passed non-converting type"; + (b,c)) in + add_named_decl (idc,Some b,t) sign) let replace_hyp sign id d = apply_to_hyp sign id @@ -445,8 +469,14 @@ let prim_refiner r sigma goal = else error "convert-concl rule passed non-converting term" - | { name = Convert_hyp; hypspecs = [id]; terms = [ty'] } -> - [mk_goal info (convert_hyp sign sigma id ty') cl] + | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } -> + [mk_goal info (convert_hyp sign sigma id ty) cl] + + | { name = Convert_defbody; hypspecs = [id]; terms = [c] } -> + [mk_goal info (convert_def true sign sigma id c) cl] + + | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } -> + [mk_goal info (convert_def false sign sigma id ty) cl] | { name = Thin; hypspecs = ids } -> let clear_aux sign id = @@ -537,7 +567,13 @@ let prim_extractor subfun vl pft = | {ref=Some(Prim{name=Convert_concl;terms=[c]},[pf])} -> subfun vl pf - | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[c]},[pf])} -> + | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[_]},[pf])} -> + subfun vl pf + + | {ref=Some(Prim{name=Convert_defbody;hypspecs=[id];terms=[_]},[pf])} -> + subfun vl pf + + | {ref=Some(Prim{name=Convert_deftype;hypspecs=[id];terms=[_]},[pf])} -> subfun vl pf | {ref=Some(Prim{name=Thin;hypspecs=ids},[pf])} -> @@ -600,6 +636,13 @@ let pr_prim_rule = function | {name=Convert_hyp;hypspecs=[id];terms=[c]} -> [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >] + | {name=Convert_defbody;hypspecs=[id];terms=[c]} -> + [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >] + + | {name=Convert_deftype;hypspecs=[id];terms=[c]} -> + [< 'sTR"Change " ; prterm c ; 'sPC ; + 'sTR"in (Type of " ; pr_id id; 'sTR ")" >] + | {name=Thin;hypspecs=ids} -> [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >] diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 18cd475cde..45fe9e5a47 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -407,7 +407,11 @@ let ast_of_cvt_arg = function | Constr_context _ -> anomalylabstrm "ast_of_cvt_arg" [<'sTR "Constr_context argument could not be used">] - | Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl) + | Clause idl -> + let transl = function + | InHyp id -> ope ("INHYP", [nvar (string_of_id id)]) + | InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in + ope ("CLAUSE", List.map transl idl) | Bindings bl -> ope ("BINDINGS", List.map (ast_of_cvt_bind (fun x -> x)) bl) | Cbindings bl -> diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index bf8deb53a5..363dd09645 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -28,6 +28,10 @@ type pf_status = | Complete_proof | Incomplete_proof +type hyp_location = (* To distinguish body and type of local defs *) + | InHyp of identifier + | InHypType of identifier + type prim_rule_name = | Intro | Intro_after @@ -37,6 +41,8 @@ type prim_rule_name = | Refine | Convert_concl | Convert_hyp + | Convert_defbody + | Convert_deftype | Thin | Move of bool @@ -97,7 +103,7 @@ and tactic_arg = | Identifier of identifier | Qualid of Nametab.qualid | Integer of int - | Clause of identifier list + | Clause of hyp_location list | Bindings of Coqast.t substitution | Cbindings of constr substitution | Quoted_string of string diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index de2c155f07..5d415d5a08 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -31,6 +31,10 @@ type pf_status = | Complete_proof | Incomplete_proof +type hyp_location = (* To distinguish body and type of local defs *) + | InHyp of identifier + | InHypType of identifier + type prim_rule_name = | Intro | Intro_after @@ -40,6 +44,8 @@ type prim_rule_name = | Refine | Convert_concl | Convert_hyp + | Convert_defbody + | Convert_deftype | Thin | Move of bool @@ -129,7 +135,7 @@ and tactic_arg = | Identifier of identifier | Qualid of Nametab.qualid | Integer of int - | Clause of identifier list + | Clause of hyp_location list | Bindings of Coqast.t substitution | Cbindings of constr substitution | Quoted_string of string diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index 4b45132455..35435f7a70 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -529,6 +529,10 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = | Invalid_argument "destVar" -> user_err_loc (loc, "Tacinterp.val_interp",[<'sTR "Metavariable "; 'iNT n; 'sTR " must be an identifier" >]))*) + | Node(loc,"QUALIDARG",p) -> VArg (Qualid (interp_qualid p)) + | Node(loc,"QUALIDMETA",[Num(_,n)]) -> + VArg + (Qualid (Nametab.qualid_of_sp (path_of_const (List.assoc n lmatch)))) | Str(_,s) -> VArg (Quoted_string s) | Num(_,n) -> VArg (Integer n) | Node(_,"COMMAND",[c]) -> @@ -544,8 +548,8 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast = VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug) (redname,args))) | Node(_,"CLAUSE",cl) -> - VArg (Clause (List.map (fun ast -> make_ids ast (unvarg (val_interp - (evc,env,lfun,lmatch,goalopt,debug) ast))) cl)) + VArg (Clause (List.map (clause_interp + (evc,env,lfun,lmatch,goalopt,debug)) cl)) | Node(_,"TACTIC",[ast]) -> VArg (Tac ((tac_interp lfun lmatch debug ast),ast)) (*Remains to treat*) @@ -1170,7 +1174,14 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function error "\"Goal\" occurs twice" else (Some (List.map num_of_ast nums), l) - | arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern") + | arg -> invalid_arg_loc (Ast.loc arg,"cvt_letpattern") + +(* Interprets an hypothesis name *) +and clause_interp info = function + | Node(_,("INHYP"|"INHYPTYPE" as where),[ast]) -> + let id = make_ids ast (unvarg (val_interp info ast)) in + if where = "INHYP" then InHyp id else InHypType id + | arg -> invalid_arg_loc (Ast.loc arg,"clause_interp") (* Interprets tactic arguments *) let interp_tacarg sign ast = unvarg (val_interp sign ast) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index b68196ff3b..d63325cd85 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -58,12 +58,14 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id let pf_last_hyp gl = List.hd (pf_hyps gl) -let pf_get_hyp_typ gls id = +let pf_get_hyp gls id = try - body_of_type (snd (lookup_id id (pf_hyps gls))) + lookup_id id (pf_hyps gls) with Not_found -> error ("No such hypothesis : " ^ (string_of_id id)) +let pf_get_hyp_typ gls id = snd (pf_get_hyp gls id) + let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) let pf_ctxt gls = get_ctxt (sig_it gls) @@ -229,9 +231,17 @@ let convert_concl c pf = refiner (Prim { name = Convert_concl; terms = [c]; hypspecs = []; newids = []; params = [] }) pf -let convert_hyp id c pf = +let convert_hyp id t pf = refiner (Prim { name = Convert_hyp; hypspecs = [id]; - terms = [c]; newids = []; params = []}) pf + terms = [t]; newids = []; params = []}) pf + +let convert_defbody id t pf = + refiner (Prim { name = Convert_defbody; hypspecs = [id]; + terms = [t]; newids = []; params = []}) pf + +let convert_deftype id t pf = + refiner (Prim { name = Convert_deftype; hypspecs = [id]; + terms = [t]; newids = []; params = []}) pf let thin ids gl = refiner (Prim { name = Thin; hypspecs = ids; diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 5481491d53..e7742f2ecd 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -56,7 +56,8 @@ val hnf_type_of : goal sigma -> constr -> constr val pf_interp_constr : goal sigma -> Coqast.t -> constr val pf_interp_type : goal sigma -> Coqast.t -> constr -val pf_get_hyp_typ : goal sigma -> identifier -> constr +val pf_get_hyp : goal sigma -> identifier -> constr option * types +val pf_get_hyp_typ : goal sigma -> identifier -> types val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr @@ -162,7 +163,9 @@ val introduction : identifier -> tactic val intro_replacing : identifier -> tactic val refine : constr -> tactic val convert_concl : constr -> tactic -val convert_hyp : identifier -> constr -> tactic +val convert_hyp : identifier -> types -> tactic +val convert_deftype : identifier -> types -> tactic +val convert_defbody : identifier -> constr -> tactic val thin : identifier list -> tactic val move_hyp : bool -> identifier -> identifier -> tactic val mutual_fix : identifier list -> int list -> constr list -> tactic @@ -228,7 +231,7 @@ val hide_openconstr_tactic : Pretyping.open_constr hide_combinator val hide_constrl_tactic : (constr list) hide_combinator val hide_numarg_tactic : int hide_combinator val hide_ident_tactic : identifier hide_combinator -val hide_identl_tactic : (identifier list) hide_combinator +val hide_identl_tactic : hyp_location list hide_combinator val hide_string_tactic : string hide_combinator val hide_bindl_tactic : ((bindOcc * constr) list) hide_combinator val hide_cbindl_tactic : (constr * (bindOcc * constr) list) hide_combinator |