From 215f42dae466bbbdb865303af05c7e70b5fb3d15 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 21 May 2003 13:11:15 +0000 Subject: Fusion à l'essai de lmatch et lfun dans tacinterp; utilisation de noms pour les metavariables de patterns; fusion NoHypId et Hyp git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4043 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tacinterp.ml | 197 ++++++++++++++++++++------------------------------- tactics/tauto.ml4 | 15 ++-- 2 files changed, 87 insertions(+), 125 deletions(-) (limited to 'tactics') diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index ea7765cd62..b065aac186 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -348,7 +348,8 @@ let error_unbound_metanum loc n = (loc,"intern_qualid_or_metanum", str "?" ++ pr_patvar n ++ str " is unbound") let intern_metanum sign loc n = - if List.mem n sign.metavars then n else error_unbound_metanum loc n + if List.mem n sign.metavars or find_var n sign then n + else error_unbound_metanum loc n let intern_hyp_or_metanum ist = function | AN id -> AN (intern_hyp ist (loc,id)) @@ -524,14 +525,10 @@ let intern_constr_may_eval ist = function (* Reads the hypotheses of a Match Context rule *) let rec intern_match_context_hyps evc env lfun = function - | (NoHypId mp)::tl -> + | (Hyp ((_,na) as locna,mp))::tl -> let metas1, pat = intern_pattern evc env lfun mp in let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in - lfun, metas1@metas2, (NoHypId pat)::hyps - | (Hyp ((_,s) as locs,mp))::tl -> - let metas1, pat = intern_pattern evc env lfun mp in - let lfun, metas2, hyps = intern_match_context_hyps evc env lfun tl in - s::lfun, metas1@metas2, Hyp (locs,pat)::hyps + name_fold (fun a l -> a::l) na lfun, metas1@metas2, Hyp (locna,pat)::hyps | [] -> lfun, [], [] (* Utilities *) @@ -753,7 +750,7 @@ and intern_match_rule ist = function let lfun',metas1,hyps = intern_match_context_hyps sigma env lfun rl in let metas2,pat = intern_pattern sigma env lfun mp in let metas = list_uniquize (metas1@metas2@lmeta) in - let ist' = { ist with ltacvars = (lfun',l2); metavars = metas } in + let ist' = { ist with ltacvars = (metas@lfun',l2); metavars = [] } in Pat (hyps,pat,intern_tactic ist' tc) :: (intern_match_rule ist tl) | [] -> [] @@ -834,18 +831,18 @@ let read_pattern evc env lfun = function | Term pc -> Term (eval_pattern lfun pc) (* Reads the hypotheses of a Match Context rule *) -let rec read_match_context_hyps evc env lfun lidh = function - | (NoHypId mp)::tl -> - (NoHypId (read_pattern evc env lfun mp)):: - (read_match_context_hyps evc env lfun lidh tl) - | (Hyp ((loc,id) as locid,mp))::tl -> - if List.mem id lidh then - user_err_loc (loc,"Tacinterp.read_match_context_hyps", +let cons_and_check_name id l = + if List.mem id l then + user_err_loc (loc,"read_match_context_hyps", str ("Hypothesis pattern-matching variable "^(string_of_id id)^ - " used twice in the same pattern")) - else - (Hyp (locid,read_pattern evc env lfun mp)):: - (read_match_context_hyps evc env lfun (id::lidh) tl) + " used twice in the same pattern")) + else id::l + +let rec read_match_context_hyps evc env lfun lidh = function + | (Hyp ((loc,na) as locna,mp))::tl -> + let lidh' = name_fold cons_and_check_name na lidh in + Hyp (locna,read_pattern evc env lfun mp):: + (read_match_context_hyps evc env lfun lidh' tl) | [] -> [] (* Reads the rules of a Match Context or a Match *) @@ -887,69 +884,40 @@ let apply_matching pat csr = PatternMatchingFailure -> raise No_match (* Tries to match one hypothesis pattern with a list of hypotheses *) -let apply_one_mhyp_context ist env gl lmatch mhyp lhyps noccopt = - let get_pattern = function - | Hyp (_,pat) -> pat - | NoHypId pat -> pat - and get_id_couple id = function - | Hyp((_,idpat),_) -> [idpat,VIdentifier id] - | NoHypId _ -> [] - and get_info_pattern = function - | Hyp((_,idpat),pat) -> (Some idpat,pat) - | NoHypId pat -> (None,pat) in - let rec apply_one_mhyp_context_rec ist env mhyp lhyps_acc nocc = function - | (id,hyp)::tl -> - (match (get_pattern mhyp) with +let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) = + let get_id_couple id = function + | Name idpat -> [idpat,VIdentifier id] + | Anonymous -> [] in + let rec apply_one_mhyp_context_rec nocc = function + | (id,hyp)::tl as hyps -> + (match pat with | Term t -> (try - let lmeta = - verify_metas_coherence gl lmatch (matches t hyp) in - (get_id_couple id mhyp,[],lmeta,tl,(id,hyp),None) - with | PatternMatchingFailure | Not_coherent_metas -> - apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl) + let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in + (get_id_couple id hypname,lmeta,(id,hyp),(tl,0)) + with + | PatternMatchingFailure | Not_coherent_metas -> + apply_one_mhyp_context_rec 0 tl) | Subterm (ic,t) -> (try let (lm,ctxt) = sub_match nocc t hyp in let lmeta = verify_metas_coherence gl lmatch lm in - (get_id_couple id mhyp,give_context ctxt - ic,lmeta,tl,(id,hyp),Some nocc) + ((get_id_couple id hypname)@(give_context ctxt ic), + lmeta,(id,hyp),(hyps,nocc + 1)) with - | NextOccurrence _ -> - apply_one_mhyp_context_rec ist env mhyp (lhyps_acc@[id,hyp]) 0 tl - | Not_coherent_metas -> - apply_one_mhyp_context_rec ist env mhyp lhyps_acc (nocc + 1) - ((id,hyp)::tl))) + | NextOccurrence _ -> + apply_one_mhyp_context_rec 0 tl + | Not_coherent_metas -> + apply_one_mhyp_context_rec (nocc + 1) hyps)) | [] -> - begin - db_hyp_pattern_failure ist.debug env (get_info_pattern mhyp); + db_hyp_pattern_failure ist.debug env (hypname,pat); raise No_match - end in - let nocc = - match noccopt with - | None -> 0 - | Some n -> n in - apply_one_mhyp_context_rec ist env mhyp [] nocc lhyps - -(* Gets the identifier of the pattern if it exists *) -let get_id_pattern = function - | [] -> None - | [(id,_)] -> Some id - | _ -> assert false - -(* -let coerce_to_qualid loc = function - | Constr c when isVar c -> make_short_qualid (destVar c) - | Constr c -> - (try qualid_of_sp (sp_of_global (Global.env()) (reference_of_constr c)) - with Not_found -> invalid_arg_loc (loc, "Not a reference")) - | Identifier id -> make_short_qualid id - | Qualid qid -> qid - | _ -> invalid_arg_loc (loc, "Not a reference") -*) + in + apply_one_mhyp_context_rec nocc lhyps -let constr_to_id loc c = - if isVar c then destVar c - else invalid_arg_loc (loc, "Not an identifier") +let constr_to_id loc = function + | VConstr c when isVar c -> destVar c + | _ -> invalid_arg_loc (loc, "Not an identifier") let constr_to_qid loc c = try shortest_qualid_of_global Idset.empty (reference_of_constr c) @@ -1038,7 +1006,7 @@ let eval_name ist = function let interp_hyp_or_metanum ist gl = function | AN id -> eval_variable ist gl (dummy_loc,id) - | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lmatch) + | MetaNum (loc,n) -> constr_to_id loc (List.assoc n ist.lfun) (* To avoid to move to much simple functions in the big recursive block *) let forward_vcontext_interp = ref (fun ist v -> failwith "not implemented") @@ -1065,7 +1033,7 @@ let pf_interp_reference ist gl = interp_reference ist (pf_env gl) let interp_inductive_or_metanum ist = function | MetaNum (loc,n) -> - coerce_to_inductive (VConstr (List.assoc n ist.lmatch)) + coerce_to_inductive (List.assoc n ist.lfun) | AN r -> match r with | ArgArg r -> r | ArgVar (_,id) -> @@ -1073,7 +1041,7 @@ let interp_inductive_or_metanum ist = function let interp_evaluable_or_metanum ist env = function | MetaNum (loc,n) -> - coerce_to_evaluable_ref env (VConstr (List.assoc n ist.lmatch)) + coerce_to_evaluable_ref env (List.assoc n ist.lfun) | AN r -> match r with | ArgArg (r,Some (loc,id)) -> (* Maybe [id] has been introduced by Intro-like tactics *) @@ -1434,7 +1402,8 @@ and match_context_interp ist g lr lmr = let (lgoal,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in if mhyps = [] then - eval_with_fail {ist with lfun=lctxt@ist.lfun; lmatch=lgoal@ist.lmatch} + let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in + eval_with_fail {ist with lfun=lgoal@lctxt@ist.lfun; lmatch=ist.lmatch} mt goal else apply_hyps_context ist env goal mt lgoal mhyps hyps @@ -1468,7 +1437,8 @@ and match_context_interp ist g lr lmr = if mhyps = [] then begin db_mc_pattern_success ist.debug; - eval_with_fail {ist with lmatch=lgoal@ist.lmatch} mt goal + let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in + eval_with_fail {ist with lfun=lgoal@ist.lfun} mt goal end else apply_hyps_context ist env goal mt lgoal mhyps hyps @@ -1499,44 +1469,29 @@ and match_context_interp ist g lr lmr = (read_match_rule (project g) env (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) -and apply_hyps_context ist env goal mt lgmatch mhyps hyps = - let rec apply_hyps_context_rec ist mt lfun lmatch mhyps lhyps_mhyp - lhyps_rest noccopt = - match mhyps with - | hd::tl -> - let (lid,lc,lm,newlhyps,hyp_match,noccopt) = - apply_one_mhyp_context ist env goal lmatch hd lhyps_mhyp noccopt in - begin - db_matched_hyp ist.debug (pf_env goal) hyp_match - (get_id_pattern lid); - (try - if tl = [] then - begin - db_mc_pattern_success ist.debug; - eval_with_fail {ist with lfun=lfun@lid@lc@ist.lfun; - lmatch=lmatch@lm@ist.lmatch} mt goal - end - else - let nextlhyps = - List.fold_left (fun l e -> if e = hyp_match then l else l@[e]) [] - lhyps_rest in - apply_hyps_context_rec ist mt - (lfun@lid@lc) (lmatch@lm) tl nextlhyps nextlhyps None - with - | e when is_failure e -> raise e - | e when is_match_catchable e -> - (match noccopt with - | None -> - apply_hyps_context_rec ist mt lfun - lmatch mhyps newlhyps lhyps_rest None - | Some nocc -> - apply_hyps_context_rec ist mt ist.lfun ist.lmatch mhyps - (hyp_match::newlhyps) lhyps_rest (Some (nocc + 1)))) +and apply_hyps_context ist env goal mt (lgmatch:(Rawterm.patvar * Term.constr) list) mhyps hyps = + let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function + | Hyp ((_,hypname),mhyp)::tl -> + let (lids,lm,hyp_match,next) = + apply_one_mhyp_context ist env goal lmatch (hypname,mhyp) current in + db_matched_hyp ist.debug (pf_env goal) hyp_match hypname; + begin + try + let nextlhyps = list_except hyp_match lhyps_rest in + apply_hyps_context_rec (lfun@lids) (lmatch@lm) nextlhyps + (nextlhyps,0) tl + with + | e when is_failure e -> raise e + | e when is_match_catchable e -> + apply_hyps_context_rec lfun lmatch lhyps_rest next mhyps end - | [] -> - anomalylabstrm "apply_hyps_context_rec" (str - "Empty list should not occur") in - apply_hyps_context_rec ist mt [] lgmatch mhyps hyps hyps None + | [] -> + let lmatch = List.map (fun (id,c) -> (id,VConstr c)) lmatch in + db_mc_pattern_success ist.debug; + eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun; + lmatch=ist.lmatch} mt goal + in + apply_hyps_context_rec [] lgmatch hyps (hyps,0) mhyps (* Interprets extended tactic generic arguments *) and interp_genarg ist goal x = @@ -1589,7 +1544,8 @@ and match_interp ist g constr lmr = try let (lm,ctxt) = sub_match nocc c csr in let lctxt = give_context ctxt id in - val_interp {ist with lfun=lctxt@ist.lfun; lmatch=lm@ist.lmatch} g mt + let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in + val_interp {ist with lfun=lm@lctxt@ist.lfun; lmatch=ist.lmatch} g mt with | NextOccurrence _ -> raise No_match in let rec apply_match ist csr = function @@ -1598,8 +1554,10 @@ and match_interp ist g constr lmr = with e when is_match_catchable e -> apply_match ist csr []) | (Pat ([],Term c,mt))::tl -> (try + let lm = apply_matching c csr in + let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in val_interp - { ist with lmatch=(apply_matching c csr)@ist.lmatch } g mt + { ist with lfun=lm@ist.lfun } g mt with e when is_match_catchable e -> apply_match ist csr tl) | (Pat ([],Subterm (id,c),mt))::tl -> (try @@ -1853,9 +1811,6 @@ let subst_match_pattern subst = function | Term pc -> Term (subst_pattern subst pc) let rec subst_match_context_hyps subst = function - | NoHypId mp :: tl -> - NoHypId (subst_match_pattern subst mp) - :: subst_match_context_hyps subst tl | Hyp (locs,mp) :: tl -> Hyp (locs,subst_match_pattern subst mp) :: subst_match_context_hyps subst tl @@ -2115,7 +2070,9 @@ let interp_redexp env evc r = (* Backwarding recursive needs of tactic glob/interp/eval functions *) let _ = Auto.set_extern_interp - (fun l -> interp_tactic {lfun=[];lmatch=l;debug=get_debug()}) + (fun l -> + let l = List.map (fun (id,c) -> (id,VConstr c)) l in + interp_tactic {lfun=l;lmatch=[];debug=get_debug()}) let _ = Auto.set_extern_intern_tac (fun l -> intern_tactic {(make_empty_glob_sign()) with metavars=l}) let _ = Auto.set_extern_subst_tactic subst_tactic diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4 index 5a03b08413..bc746094a8 100644 --- a/tactics/tauto.ml4 +++ b/tactics/tauto.ml4 @@ -21,28 +21,33 @@ open Tacticals open Tacinterp open Tactics open Util - + +let assoc_last ist = + match List.assoc (Pattern.patvar_of_int 1) ist.lfun with + | VConstr c -> c + | _ -> failwith "Tauto: anomaly" + let is_empty ist = - if (is_empty_type (List.assoc (id_of_string "1") ist.lmatch)) then + if is_empty_type (assoc_last ist) then <:tactic> else <:tactic> let is_unit ist = - if (is_unit_type (List.assoc (id_of_string "1") ist.lmatch)) then + if is_unit_type (assoc_last ist) then <:tactic> else <:tactic> let is_conj ist = - let ind=(List.assoc (id_of_string "1") ist.lmatch) in + let ind = assoc_last ist in if (is_conjunction ind) && (is_nodep_ind ind) then <:tactic> else <:tactic> let is_disj ist = - if (is_disjunction (List.assoc (id_of_string "1") ist.lmatch)) then + if is_disjunction (assoc_last ist) then <:tactic> else <:tactic> -- cgit v1.2.3