diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-26 14:04:45 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-26 14:04:45 +0000 |
commit | d488b3bff54732a8e05f9bd48c66695b461ef3af (patch) | |
tree | 68043a36b8fc3cc5c1d9389de5b39351f0f63b6a /tactics | |
parent | 80297f53a4a43aff327426a08ffd58236ec4d56d (diff) |
Introduction d'un type constr_pattern pour les différents filtrages
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@368 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/auto.ml | 68 | ||||
-rw-r--r-- | tactics/auto.mli | 37 | ||||
-rw-r--r-- | tactics/btermdn.ml | 3 | ||||
-rw-r--r-- | tactics/btermdn.mli | 9 | ||||
-rw-r--r-- | tactics/dhyp.ml | 18 | ||||
-rw-r--r-- | tactics/equality.ml | 33 | ||||
-rw-r--r-- | tactics/nbtermdn.ml | 7 | ||||
-rw-r--r-- | tactics/nbtermdn.mli | 13 | ||||
-rw-r--r-- | tactics/pattern.ml | 169 | ||||
-rw-r--r-- | tactics/pattern.mli | 47 | ||||
-rw-r--r-- | tactics/stock.ml | 2 | ||||
-rw-r--r-- | tactics/stock.mli | 2 | ||||
-rw-r--r-- | tactics/tacticals.ml | 6 | ||||
-rw-r--r-- | tactics/tacticals.mli | 7 | ||||
-rw-r--r-- | tactics/tauto.ml | 7 | ||||
-rw-r--r-- | tactics/termdn.ml | 36 | ||||
-rw-r--r-- | tactics/termdn.mli | 20 |
17 files changed, 320 insertions, 164 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 97222bd35..7d9d3530a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -14,6 +14,7 @@ open Typing open Tacmach open Proof_trees open Pfedit +open Rawterm open Tacred open Tactics open Tacticals @@ -39,7 +40,7 @@ type auto_tactic = type pri_auto_tactic = { hname : identifier; (* name of the hint *) pri : int; (* A number between 0 and 4, 4 = lower priority *) - pat : constr option; (* A pattern for the concl of the Goal *) + pat : constr_pattern option; (* A pattern for the concl of the Goal *) code : auto_tactic (* the tactic to apply when the concl matches pat *) } @@ -88,7 +89,7 @@ let lookup_tacs (hdc,c) (l,l',dn) = module Constr_map = Map.Make(struct - type t = constr + type t = constr_label let compare = Pervasives.compare end) @@ -182,20 +183,25 @@ let rec nb_hyp = function (* adding and removing tactics in the search table *) +let try_head_pattern c = + try head_pattern_bound c + with BoundPattern -> error "Bound head variable" + let make_exact_entry name (c,cty) = match strip_outer_cast cty with | DOP2(Prod,_,_) -> failwith "make_exact_entry" - | cty -> - (List.hd (head_constr cty), - { hname=name; pri=0; pat=None; code=Give_exact c }) + | cty -> + (head_of_constr_reference (List.hd (head_constr cty)), + { hname=name; pri=0; pat=None; code=Give_exact c }) let make_apply_entry (eapply,verbose) name (c,cty) = match hnf_constr (Global.env()) Evd.empty cty with | DOP2(Prod,_,_) as cty -> - let hdconstr = (try List.hd (head_constr_bound cty []) - with Bound -> failwith "make_apply_entry") in - let ce = mk_clenv_from () (c,cty) in + let ce = mk_clenv_from () (c,cty) in + let pat = Pattern.pattern_of_constr (clenv_template_type ce).rebus in + let hd = (try head_pattern_bound pat + with BoundPattern -> failwith "make_apply_entry") in let nmiss = List.length (clenv_missing ce (clenv_template ce,clenv_template_type ce)) @@ -204,16 +210,16 @@ let make_apply_entry (eapply,verbose) name (c,cty) = if verbose then wARN [< 'sTR "the hint: EApply "; prterm c; 'sTR " will only be used by EAuto" >]; - (hdconstr, + (hd, { hname = name; pri = nb_hyp cty + nmiss; - pat = Some (clenv_template_type ce).rebus; + pat = Some pat; code = ERes_pf(c,ce) }) end else - (hdconstr, + (hd, { hname = name; pri = nb_hyp cty; - pat = Some (clenv_template_type ce).rebus; + pat = Some pat; code = Res_pf(c,ce) }) | _ -> failwith "make_apply_entry" @@ -263,7 +269,7 @@ let make_unfold (hintname, id) = with Not_found -> errorlabstrm "make_unfold" [<print_id id; 'sTR " not declared" >]) in - (hdconstr, + (head_of_constr_reference hdconstr, { hname = hintname; pri = 4; pat = None; @@ -276,18 +282,17 @@ let add_unfolds l dbnames = dbnames let make_extern name pri pat tacast = - let hdconstr = List.hd (head_constr pat) in + let hdconstr = try_head_pattern pat in (hdconstr, { hname = name; pri=pri; pat = Some pat; code= Extern tacast }) -let add_extern name pri pat tacast dbname = +let add_extern name pri (patmetas,pat) tacast dbname = (* We check that all metas that appear in tacast have at least one occurence in the left pattern pat *) let tacmetas = Coqast.collect_metas tacast in - let patmetas = Clenv.collect_metas pat in match (list_subtract tacmetas patmetas) with | i::_ -> errorlabstrm "add_extern" @@ -302,11 +307,11 @@ let add_externs name pri pat tacast dbnames = let make_trivial (name,c) = let sigma = Evd.empty and env = Global.env() in let t = type_of env sigma c in - let hdconstr = List.hd (head_constr t) in + let hd = head_of_constr_reference (List.hd (head_constr t)) in let ce = mk_clenv_from () (c,hnf_constr env sigma t) in - (hdconstr, { hname = name; + (hd, { hname = name; pri=1; - pat = Some(clenv_template_type ce).rebus; + pat = Some (Pattern.pattern_of_constr (clenv_template_type ce).rebus); code=Res_pf_THEN_trivial_fail(c,ce) }) let add_trivials l dbnames = @@ -378,8 +383,8 @@ let _ = (function | [VARG_IDENTIFIER hintname; VARG_VARGLIST l; VARG_NUMBER pri; VARG_CONSTR patcom; VARG_TACTIC tacexp] -> - let pat = Pattern.raw_sopattern_of_compattern - (Global.env()) patcom in + let pat = + Astterm.interp_constrpattern Evd.empty (Global.env()) patcom in let dbnames = if l = [] then ["core"] else List.map (function VARG_IDENTIFIER i -> string_of_id i | _ -> bad_vernac_args "HintConstructors") l in @@ -464,10 +469,10 @@ let fmt_hint_list_for_head c = dbs in if valid_dbs = [] then - [<'sTR "No hint declared for :"; prterm c >] + [<'sTR "No hint declared for :"; pr_ref_label c >] else hOV 0 - [< 'sTR"For "; prterm c; 'sTR" -> "; + [< 'sTR"For "; pr_ref_label c; 'sTR" -> "; prlist (fun (name,db,hintlist) -> [< 'sTR " In the database "; 'sTR name; 'sTR " :"; 'fNL; fmt_hint_list hintlist >]) @@ -475,7 +480,8 @@ let fmt_hint_list_for_head c = let fmt_hint_id id = try - let c = Declare.global_reference CCI id in fmt_hint_list_for_head c + let c = Declare.global_reference CCI id in + fmt_hint_list_for_head (head_of_constr_reference c) with Not_found -> [< print_id id; 'sTR " not declared" >] @@ -488,16 +494,17 @@ let fmt_hint_term cl = | hdc::args -> (hdc,args) | [] -> assert false in + let hd = head_of_constr_reference hdc in let dbs = stringmap_to_list !searchtable in let valid_dbs = if occur_existential cl then map_succeed - (fun (name, db) -> (name, db, Hint_db.map_all hdc db)) + (fun (name, db) -> (name, db, Hint_db.map_all hd db)) dbs else map_succeed (fun (name, db) -> - (name, db, Hint_db.map_auto (hdc,applist(hdc,args)) db)) + (name, db, Hint_db.map_auto (hd,applist(hdc,args)) db)) dbs in if valid_dbs = [] then @@ -525,7 +532,7 @@ let print_hint_db db = Hint_db.iter (fun head hintlist -> mSG (hOV 0 - [< 'sTR "For "; prterm head; 'sTR " -> "; + [< 'sTR "For "; pr_ref_label head; 'sTR " -> "; fmt_hint_list hintlist; 'fNL >])) db @@ -644,8 +651,9 @@ and my_find_search db_list local_db hdc concl = and trivial_resolve db_list local_db cl = try + let hdconstr = List.hd (head_constr_bound cl []) in priority - (my_find_search db_list local_db (List.hd (head_constr_bound cl [])) cl) + (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) with Bound | Not_found -> [] @@ -685,9 +693,9 @@ let h_trivial = hide_tactic "Trivial" dyn_trivial let possible_resolve db_list local_db cl = try + let hdconstr = List.hd (head_constr_bound cl []) in List.map snd - (my_find_search db_list local_db - (List.hd (head_constr_bound cl [])) cl) + (my_find_search db_list local_db (head_of_constr_reference hdconstr) cl) with Bound | Not_found -> [] diff --git a/tactics/auto.mli b/tactics/auto.mli index 82a8ee792..fce449c02 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -12,17 +12,19 @@ open Clenv (*i*) type auto_tactic = - | Res_pf of constr * unit clausenv (* Hint Apply *) - | ERes_pf of constr * unit clausenv (* Hint EApply *) + | Res_pf of constr * unit clausenv (* Hint Apply *) + | ERes_pf of constr * unit clausenv (* Hint EApply *) | Give_exact of constr | Res_pf_THEN_trivial_fail of constr * unit clausenv (* Hint Immediate *) - | Unfold_nth of constr (* Hint Unfold *) - | Extern of Coqast.t (* Hint Extern *) + | Unfold_nth of constr (* Hint Unfold *) + | Extern of Coqast.t (* Hint Extern *) + +open Rawterm type pri_auto_tactic = { hname : identifier; (* name of the hint *) pri : int; (* A number between 0 and 4, 4 = lower priority *) - pat : constr option; (* A pattern for the concl of the Goal *) + pat : constr_pattern option; (* A pattern for the concl of the Goal *) code : auto_tactic; (* the tactic to apply when the concl matches pat *) } @@ -34,12 +36,12 @@ module Hint_db : sig type t val empty : t - val find : constr -> t -> search_entry - val map_all : constr -> t -> pri_auto_tactic list - val map_auto : constr * constr -> t -> pri_auto_tactic list - val add_one : constr * pri_auto_tactic -> t -> t - val add_list : (constr * pri_auto_tactic) list -> t -> t - val iter : (constr -> stored_data list -> unit) -> t -> unit + val find : constr_label -> t -> search_entry + val map_all : constr_label -> t -> pri_auto_tactic list + val map_auto : constr_label * constr -> t -> pri_auto_tactic list + val add_one : constr_label * pri_auto_tactic -> t -> t + val add_list : (constr_label * pri_auto_tactic) list -> t -> t + val iter : (constr_label -> stored_data list -> unit) -> t -> unit end type frozen_hint_db_table = Hint_db.t Stringmap.t @@ -54,7 +56,7 @@ val searchtable : hint_db_table [ctyp] is the type of [hc]. *) val make_exact_entry : - identifier -> constr * constr -> constr * pri_auto_tactic + identifier -> constr * constr -> constr_label * pri_auto_tactic (* [make_apply_entry (eapply,verbose) name (c,cty)]. [eapply] is true if this hint will be used only with EApply; @@ -63,7 +65,8 @@ val make_exact_entry : [cty] is the type of [hc]. *) val make_apply_entry : - bool * bool -> identifier -> constr * constr -> constr * pri_auto_tactic + bool * bool -> identifier -> constr * constr + -> constr_label * pri_auto_tactic (* A constr which is Hint'ed will be: (1) used as an Exact, if it does not start with a product @@ -74,19 +77,21 @@ val make_apply_entry : val make_resolves : identifier -> bool * bool -> constr * constr -> - (constr * pri_auto_tactic) list + (constr_label * pri_auto_tactic) list (* [make_resolve_hyp hname htyp]. used to add an hypothesis to the local hint database; Never raises an User_exception; If the hyp cannot be used as a Hint, the empty list is returned. *) -val make_resolve_hyp : identifier -> constr -> (constr * pri_auto_tactic) list +val make_resolve_hyp : identifier -> constr + -> (constr_label * pri_auto_tactic) list (* [make_extern name pri pattern tactic_ast] *) val make_extern : - identifier -> int -> constr -> Coqast.t -> constr * pri_auto_tactic + identifier -> int -> constr_pattern -> Coqast.t + -> constr_label * pri_auto_tactic (* Create a Hint database from the pairs (name, constr). Useful to take the current goal hypotheses as hints *) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index e6a4b43dd..3dbbacea6 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -3,6 +3,7 @@ open Term open Termdn +open Rawterm (* Discrimination nets with bounded depth. See the module dn.ml for further explanations. @@ -26,7 +27,7 @@ let bounded_constr_val_discr (t,depth) = | None -> None | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) -type 'a t = (lbl,constr * int,'a) Dn.t +type 'a t = (constr_label,constr_pattern * int,'a) Dn.t let create = Dn.create diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 882f0bbb9..2d0b2f106 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -4,6 +4,7 @@ (*i*) open Generic open Term +open Rawterm (*i*) (* Discrimination nets with bounded depth. *) @@ -12,10 +13,10 @@ type 'a t val create : unit -> 'a t -val add : 'a t -> (constr * 'a) -> 'a t -val rmv : 'a t -> (constr * 'a) -> 'a t +val add : 'a t -> (constr_pattern * 'a) -> 'a t +val rmv : 'a t -> (constr_pattern * 'a) -> 'a t -val lookup : 'a t -> constr -> (constr * 'a) list -val app : ((constr * 'a) -> unit) -> 'a t -> unit +val lookup : 'a t -> constr -> (constr_pattern * 'a) list +val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit val dnet_depth : int ref diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml index 5969cebbb..0ca3f6b2a 100644 --- a/tactics/dhyp.ml +++ b/tactics/dhyp.ml @@ -8,7 +8,7 @@ The idea here is that we are going to store patterns. These patterns look like: - TYP=<patern> + TYP=<pattern> SORT=<pattern> and from these patterns, we will be able to decide which tactic to @@ -111,6 +111,7 @@ open Generic open Term open Environ open Reduction +open Rawterm open Proof_trees open Tacmach open Tactics @@ -127,8 +128,8 @@ open Pcoq (* two patterns - one for the type, and one for the type of the type *) type destructor_pattern = { - d_typ: constr; - d_sort: constr } + d_typ: Rawterm.constr_pattern; + d_sort: Rawterm.constr_pattern } type ('a,'b) location = Hyp of 'a | Concl of 'b @@ -215,16 +216,17 @@ let _ = | _ -> assert false in fun () -> - let pat = raw_sopattern_of_compattern (Global.env()) patcom in + let (_,pat) = Astterm.interp_constrpattern + Evd.empty (Global.env()) patcom in let code = Ast.to_act_check_vars ["$0",ETast] ETast tacexp in add_destructor_hint na (match loc with | Hyp b -> - Hyp(b,{d_typ=pat;d_sort=DOP0(Meta(new_meta()))}, - { d_typ=DOP0(Meta(new_meta())); - d_sort=DOP0(Meta(new_meta())) }) + Hyp(b,{d_typ=pat;d_sort=PMeta(new_meta())}, + { d_typ=PMeta(new_meta()); + d_sort=PMeta(new_meta()) }) | Concl () -> - Concl({d_typ=pat;d_sort=DOP0(Meta(new_meta()))})) + Concl({d_typ=pat;d_sort=PMeta(new_meta())})) pri code | _ -> bad_vernac_args "HintDestruct") diff --git a/tactics/equality.ml b/tactics/equality.ml index 9f207d27d..1880b5a09 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -173,15 +173,16 @@ let find_constructor env sigma c = | _ -> error "find_constructor" type leibniz_eq = { - eq : marked_term; - ind : marked_term; - rrec : marked_term option; - rect : marked_term option; - congr: marked_term; - sym : marked_term } + eq : marked_pattern; + ind : marked_pattern; + rrec : marked_pattern option; + rect : marked_pattern option; + congr: marked_pattern; + sym : marked_pattern } let mmk = make_module_marker [ "Prelude"; "Logic_Type"; "Specif"; "Logic" ] +(* Patterns *) let eq_pattern = put_pat mmk "(eq ? ? ?)" let not_pattern = put_pat mmk "(not ?)" let imp_False_pattern = put_pat mmk "? -> False" @@ -1119,12 +1120,12 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls = *) +(* squeletons *) +let comp_carS_squeleton = put_pat mmk "<<x>>(projS1 ? ? (?)@[x])" +let comp_cdrS_squeleton = put_pat mmk "<<x>>(projS2 ? ? (?)@[x])" -let comp_carS_pattern = put_pat mmk "<<x>>(projS1 ? ? (?)@[x])" -let comp_cdrS_pattern = put_pat mmk "<<x>>(projS2 ? ? (?)@[x])" - -let comp_carT_pattern = put_pat mmk "<<x>>(projT1 ? ? (?)@[x])" -let comp_cdrT_pattern = put_pat mmk "<<x>>(projT2 ? ? (?)@[x])" +let comp_carT_squeleton = put_pat mmk "<<x>>(projT1 ? ? (?)@[x])" +let comp_cdrT_squeleton = put_pat mmk "<<x>>(projT2 ? ? (?)@[x])" let dest_somatch_sigma ex ex_pat = match dest_somatch ex ex_pat with @@ -1133,11 +1134,11 @@ let dest_somatch_sigma ex ex_pat = let find_sigma_data_decompose ex = try - (comp_carS_pattern, comp_cdrS_pattern, + (comp_carS_squeleton, comp_cdrS_squeleton, dest_somatch_sigma ex existS_pattern) with _ -> (try - (comp_carT_pattern,comp_cdrT_pattern, + (comp_carT_squeleton,comp_cdrT_squeleton, dest_somatch_sigma ex existT_pattern) with _ -> errorlabstrm "find_sigma_data_decompose" [< >]) @@ -1145,10 +1146,10 @@ let find_sigma_data_decompose ex = let decomp_tuple_term env = let rec decomprec to_here_fun ex = try - let (comp_car_pattern,comp_cdr_pattern,(a,p,car,cdr)) = + let (comp_car_squeleton,comp_cdr_squeleton,(a,p,car,cdr)) = find_sigma_data_decompose ex in - let car_code = soinstance comp_car_pattern [a;p;to_here_fun] - and cdr_code = soinstance comp_cdr_pattern [a;p;to_here_fun] in + let car_code = soinstance comp_car_squeleton [a;p;to_here_fun] + and cdr_code = soinstance comp_cdr_squeleton [a;p;to_here_fun] in (car,named_hd env a Anonymous,car_code)::(decomprec cdr_code cdr) with e when catchable_exception e -> [(ex,named_hd env ex Anonymous,to_here_fun)] diff --git a/tactics/nbtermdn.ml b/tactics/nbtermdn.ml index ec5de39c0..e762531d4 100644 --- a/tactics/nbtermdn.ml +++ b/tactics/nbtermdn.ml @@ -20,11 +20,12 @@ open Library Eduardo (5/8/97) *) type ('na,'a) t = { - mutable table : ('na,constr * 'a) Gmap.t; - mutable patterns : (Termdn.lbl option,'a Btermdn.t) Gmap.t } + mutable table : ('na,Rawterm.constr_pattern * 'a) Gmap.t; + mutable patterns : (Rawterm.constr_label option,'a Btermdn.t) Gmap.t } type ('na,'a) frozen_t = - ('na,constr * 'a) Gmap.t * (Termdn.lbl option,'a Btermdn.t) Gmap.t + ('na,Rawterm.constr_pattern * 'a) Gmap.t + * (Rawterm.constr_label option,'a Btermdn.t) Gmap.t let create () = { table = Gmap.empty; diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli index e94a21e9d..527580523 100644 --- a/tactics/nbtermdn.mli +++ b/tactics/nbtermdn.mli @@ -4,6 +4,7 @@ (*i*) open Generic open Term +open Rawterm (*i*) (* Named, bounded-depth, term-discrimination nets. *) @@ -13,18 +14,18 @@ type ('na,'a) frozen_t val create : unit -> ('na,'a) t -val add : ('na,'a) t -> ('na * (constr * 'a)) -> unit +val add : ('na,'a) t -> ('na * (constr_pattern * 'a)) -> unit val rmv : ('na,'a) t -> 'na -> unit val in_dn : ('na,'a) t -> 'na -> bool -val remap : ('na,'a) t -> 'na -> (constr * 'a) -> unit +val remap : ('na,'a) t -> 'na -> (constr_pattern * 'a) -> unit -val lookup : ('na,'a) t -> constr -> (constr * 'a) list -val app : ('na -> (constr * 'a) -> unit) -> ('na,'a) t -> unit +val lookup : ('na,'a) t -> constr -> (constr_pattern * 'a) list +val app : ('na -> (constr_pattern * 'a) -> unit) -> ('na,'a) t -> unit val dnet_depth : int ref val freeze : ('na,'a) t -> ('na,'a) frozen_t val unfreeze : ('na,'a) frozen_t -> ('na,'a) t -> unit val empty : ('na,'a) t -> unit -val to2lists : ('na,'a) t -> ('na * (Term.constr * 'a)) list * - (Termdn.lbl option * 'a Btermdn.t) list +val to2lists : ('na,'a) t -> ('na * (Rawterm.constr_pattern * 'a)) list * + (Rawterm.constr_label option * 'a Btermdn.t) list diff --git a/tactics/pattern.ml b/tactics/pattern.ml index 23b6da6e4..19d020729 100644 --- a/tactics/pattern.ml +++ b/tactics/pattern.ml @@ -12,6 +12,7 @@ open Environ open Proof_trees open Stock open Clenv +open Rawterm (* The pattern table for tactics. *) @@ -21,33 +22,38 @@ open Clenv type module_mark = Stock.module_mark -type marked_term = constr Stock.stocked - -let rec whd_replmeta = function - | DOP0(XTRA("ISEVAR")) -> DOP0(Meta (new_meta())) - | DOP2(Cast,c,_) -> whd_replmeta c - | c -> c - -let raw_sopattern_of_compattern env com = - let c = Astterm.constr_of_com_pattern Evd.empty env com in - strong (fun _ _ -> whd_replmeta) env Evd.empty c +let parse_constr s = + try + Pcoq.parse_string Pcoq.Constr.constr_eoi s + with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> + error "Syntax error : not a construction" +(* Patterns *) let parse_pattern s = - let com = - try - Pcoq.parse_string Pcoq.Constr.constr_eoi s - with Stdpp.Exc_located (_ , (Stream.Failure | Stream.Error _)) -> - error "Malformed pattern" - in - raw_sopattern_of_compattern (Global.env()) com + Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_constr s) -let (pattern_stock : constr Stock.stock) = +type marked_pattern = (int list * constr_pattern) Stock.stocked + +let (pattern_stock : (int list * constr_pattern) Stock.stock) = Stock.make_stock { name = "PATTERN"; proc = parse_pattern } -let make_module_marker = Stock.make_module_marker pattern_stock let put_pat = Stock.stock pattern_stock let get_pat = Stock.retrieve pattern_stock +let make_module_marker = Stock.make_module_marker + +(* Squeletons *) +let parse_squeleton s = + Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) + +type marked_term = constr Stock.stocked + +let (squeleton_stock : constr Stock.stock) = + Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton } + +let put_squel = Stock.stock squeleton_stock +let get_squel = Stock.retrieve squeleton_stock + (* Second part : Given a term with second-order variables in it, represented by Meta's, and possibly applied using XTRA[$SOAPP] to terms, this function will perform second-order, binding-preserving, @@ -103,7 +109,73 @@ let memb_metavars m n = match (m,n) with | (None, _) -> true | (Some mvs, n) -> List.mem n mvs - + +exception PatternMatchingFailure + +let somatch metavars = + let rec sorec stk sigma p t = + let cT = whd_castapp t in + match p,kind_of_term cT with + | PSoApp (n,relargs),m -> + assert (memb_metavars metavars n); + let frels = Intset.elements (free_rels cT) in + if list_subset frels relargs then + constrain (n,build_dlam relargs stk cT) sigma + else + raise PatternMatchingFailure + + | PMeta n, m -> + if not (memb_metavars metavars n) then + (*Ce cas est bizarre : comment les numéros pourraient-ils coincider*) + match m with + | IsMeta m0 when n=m0 -> sigma + | _ -> raise PatternMatchingFailure + else + let depth = List.length stk in + let frels = Intset.elements (free_rels cT) in + if List.for_all (fun i -> i > depth) frels then + constrain (n,lift (-depth) cT) sigma + else + raise PatternMatchingFailure + + | PRef (RVar v1), IsVar v2 when v1 = v2 -> sigma + + | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) + when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> + array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + + | PRef (RInd (sp1,ctxt1)), IsMutInd (sp2,ctxt2) + when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> + array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + + | PRef (RConstruct (sp1,ctxt1)), IsMutConstruct (sp2,ctxt2) + when sp1 = sp2 && Array.length ctxt1 = Array.length ctxt2 -> + array_fold_left2 (sorec stk) sigma ctxt1 ctxt2 + + | PRel n1, IsRel n2 when n1 = n2 -> sigma + + | PSort (RProp c1), IsSort (Prop c2) when c1 = c2 -> sigma + + | PSort RType, IsSort (Type _) -> sigma + + | PApp (c1,arg1), IsAppL (c2,arg2) -> + array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) + arg1 (Array.of_list arg2) + + | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) -> + sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + + | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) -> + sorec (na2::stk) (sorec stk sigma c1 c2) d1 d2 + + | _, (IsFix _ | IsMutCase _ | IsCoFix _) -> + error "somatch: not implemented" + + | _ -> raise PatternMatchingFailure + + in + sorec [] [] +(* let somatch metavars = let rec sorec stk sigma p t = let cP = whd_castapp p @@ -175,26 +247,27 @@ let somatch metavars = | _ -> error "somatch" in sorec [] [] - +*) let somatches n pat = - let m = get_pat pat in + let (_,m) = get_pat pat in try let _ = somatch None m n in true with e when Logic.catchable_exception e -> false let dest_somatch n pat = - let m = get_pat pat in - let mvs = collect_metas m in + let mvs,m = get_pat pat in let mvb = somatch (Some (list_uniquize mvs)) m n in List.map (fun b -> List.assoc b mvb) mvs -let soinstance pat arglist = - let m = get_pat pat in - let mvs = collect_metas m in +let newsomatch n pat = let _,m = get_pat pat in somatch None m n + +let soinstance squel arglist = + let c = get_squel squel in + let mvs = collect_metas c in let mvb = List.combine mvs arglist in Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) - empty_env Evd.empty m) + empty_env Evd.empty c) (* I implemented the following functions which test whether a term t is an inductive but non-recursive type, a general conjuction, a @@ -300,18 +373,18 @@ let is_unit_type t = op2bool (match_with_unit_type t) inductive binary relation R, so that R has only one constructor stablishing its reflexivity. *) +let refl_rel_pat1 = put_pat mmk "(A : ?)(x:A)(? A x x)" +let refl_rel_pat2 = put_pat mmk "(x : ?)(? x x)" + let match_with_equation t = let (hdapp,args) = decomp_app t in match (kind_of_term hdapp) with | IsMutInd ind -> - let constr_types = - Global.mind_lc_without_abstractions ind in - let refl_rel_term1 = put_pat mmk "(A : ?)(x:A)(? A x x)" in - let refl_rel_term2 = put_pat mmk "(x : ?)(? x x)" in + let constr_types = Global.mind_lc_without_abstractions ind in let nconstr = Global.mind_nconstr ind in if nconstr = 1 && - (somatches constr_types.(0) refl_rel_term1 || - somatches constr_types.(0) refl_rel_term2) + (somatches constr_types.(0) refl_rel_pat1 || + somatches constr_types.(0) refl_rel_pat2) then Some (hdapp,args) else @@ -335,3 +408,31 @@ let is_nottype t = op2bool (match_with_nottype t) let is_imp_term = function | DOP2(Prod,_,DLAM(_,b)) -> not (dependent (Rel 1) b) | _ -> false + +let rec pattern_of_constr t = + match kind_of_term t with + | IsRel n -> PRel n + | IsMeta n -> PMeta n + | IsVar id -> PRef (RVar id) + | IsSort (Prop c) -> PSort (RProp c) + | IsSort (Type _) -> PSort RType + | IsCast (c,t) -> pattern_of_constr c + | IsProd (na,c,b) -> + PBinder (BProd,na,pattern_of_constr c,pattern_of_constr b) + | IsLambda (na,c,b) -> + PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b) + | IsAppL (f,args) -> + PApp (pattern_of_constr f, + Array.of_list (List.map pattern_of_constr args)) + | IsConst (cst_sp,ctxt) -> + PRef (RConst (cst_sp,Array.map pattern_of_constr ctxt)) + | IsMutInd (ind_sp,ctxt) -> + PRef (RInd (ind_sp,Array.map pattern_of_constr ctxt)) + | IsMutConstruct (cstr_sp,ctxt) -> + PRef (RConstruct (cstr_sp,Array.map pattern_of_constr ctxt)) + | IsMutCase _ | IsFix _ | IsCoFix _ -> + error "pattern_of_constr: destructors currently not supported" + | IsEvar _ -> error "pattern_of_constr: an existential variable remains" + | IsAbst _ | IsXtra _ -> anomaly "No longer supported" + + diff --git a/tactics/pattern.mli b/tactics/pattern.mli index afe1ec848..ae59ddef3 100644 --- a/tactics/pattern.mli +++ b/tactics/pattern.mli @@ -37,17 +37,43 @@ open Proof_trees at tactic-application time. The ONLY difference will be that no implicit syntax resolution will happen. *) -(*s First part : introduction of term patterns *) +(* A pattern is intented to be pattern-matched (using functions + [somatch] and co), while a squeleton is a term with holes intented to + be substituted by [soinstance] *) -type module_mark = Stock.module_mark -type marked_term +(*s First part : introduction of term patterns and term squeletons *) +(* [make_module_marker modl] makes a key from the list of + vernacular modules [modl] where names in a pattern or squeleton has + to be searched *) + +type module_mark = Stock.module_mark val make_module_marker : string list -> module_mark -val put_pat : module_mark -> string -> marked_term -val get_pat : marked_term -> constr -val pattern_stock : constr Stock.stock +(* [put_pat mmk s] declares a pattern [s] to be parsed using the + definitions in the modules associated to the key [mmk] *) + +type marked_pattern +val put_pat : module_mark -> string -> marked_pattern +(*val get_pat : marked_pattern -> constr*) + + +(* [pattern_of_constr c] translates a term [c] with metavariables into + a pattern; currently, no destructor (Cases, Fix, Cofix) and no + existential variable are allowed in [c] *) + +val pattern_of_constr : constr -> Rawterm.constr_pattern + +(* [put_squel mmk s] declares an open term [s] to be parsed using the + definitions in the modules associated to the key [mmk] *) + +type marked_term +val put_squel : module_mark -> string -> marked_term +(*val get_squel : marked_term -> constr*) + +(*i Remplacé par Astterm.interp_constrpattern val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr +i*) (*s Second part : Given a term with second-order variables in it, represented by Meta's, and possibly applied using \verb!XTRA[$SOAPP]! to @@ -69,9 +95,12 @@ val raw_sopattern_of_compattern : Environ.env -> Coqast.t -> constr contained in the arguments of the application, and in that case, we construct a [DLAM] with the names on the stack. *) -val somatch : int list option -> constr -> constr -> (int * constr) list -val somatches : constr -> marked_term -> bool -val dest_somatch : constr -> marked_term -> constr list +(*i Devrait être une fonction de filtrage externe i*) +val somatch : int list option -> Rawterm.constr_pattern -> constr -> (int * constr) list + +val somatches : constr -> marked_pattern -> bool +val dest_somatch : constr -> marked_pattern -> constr list + val soinstance : marked_term -> constr list -> constr val is_imp_term : constr -> bool diff --git a/tactics/stock.ml b/tactics/stock.ml index b0fa6d0e8..ef0feec95 100644 --- a/tactics/stock.ml +++ b/tactics/stock.ml @@ -59,7 +59,7 @@ let mmk_ctr = ref 0 let new_mmk () = (incr mmk_ctr; !mmk_ctr) -let make_module_marker stock sl = +let make_module_marker sl = let sorted_sl = Sort.list (<) sl in try Bij.map !path_mark_bij sorted_sl diff --git a/tactics/stock.mli b/tactics/stock.mli index bbc919514..c0cd43c7d 100644 --- a/tactics/stock.mli +++ b/tactics/stock.mli @@ -18,7 +18,7 @@ type 'a stock_args = { proc : string -> 'a } val make_stock : 'a stock_args -> 'a stock -val make_module_marker : 'a stock -> string list -> module_mark +val make_module_marker : string list -> module_mark val stock : 'a stock -> module_mark -> string -> 'a stocked val retrieve : 'a stock -> 'a stocked -> 'a diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 54d04def0..baae41399 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -118,16 +118,14 @@ let clause_type cls gl = (* Functions concerning matching of clausal environments *) -let matches gls n pat = - let m = get_pat pat in +let matches gls n m = let (wc,_) = startWalk gls in try let _ = Clenv.unify_0 [] wc m n in true with e when Logic.catchable_exception e -> false -let dest_match gls n pat = - let m = get_pat pat in +let dest_match gls n m = let mvs = collect_metas m in let (wc,_) = startWalk gls in let (mvb,_) = Clenv.unify_0 [] wc m n in diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 7884ba02e..e7d8cff25 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -48,8 +48,13 @@ val tclTHEN_i1 : tactic -> (int -> tactic) -> tactic val nth_clause : int -> goal sigma -> clause val clause_type : clause -> goal sigma -> constr +(* val matches : goal sigma -> constr -> marked_term -> bool val dest_match : goal sigma -> constr -> marked_term -> constr list +*) +(* The second argument is the pattern *) +val matches : goal sigma -> constr -> constr -> bool +val dest_match : goal sigma -> constr -> constr -> constr list val allHyps : goal sigma -> clause list val afterHyp : identifier -> goal sigma -> clause list @@ -78,7 +83,7 @@ val ifOnClause : [Pattern.somatches], then replace [?1] [?2] metavars in tacast by the right values to build a tactic *) -val conclPattern : constr -> constr -> Coqast.t -> tactic +val conclPattern : constr -> Rawterm.constr_pattern -> Coqast.t -> tactic (*s Elimination tacticals. *) diff --git a/tactics/tauto.ml b/tactics/tauto.ml index 4fcfc0264..334eb304e 100644 --- a/tactics/tauto.ml +++ b/tactics/tauto.ml @@ -46,6 +46,7 @@ let classically cltac = function let somatch m pat = somatch None (get_pat pat) m let module_mark = ["Logic"] +(* patterns *) let mmk = make_module_marker ["Prelude"] let false_pattern = put_pat mmk "False" let true_pattern = put_pat mmk "True" @@ -54,9 +55,12 @@ let or_pattern = put_pat mmk "(or ? ?)" let eq_pattern = put_pat mmk "(eq ? ? ?)" let pi_pattern = put_pat mmk "(x : ?)((?)@[x])" let imply_pattern = put_pat mmk "?1 -> ?2" +let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2" let iff_pattern = put_pat mmk "(iff ? ?)" let not_pattern = put_pat mmk "(not ?1)" -let mkIMP a b = soinstance imply_pattern [a;b] +(* squeletons *) +let imply_squeleton = put_pat mmk "?1 -> ?2" +let mkIMP a b = soinstance imply_squeleton [a;b] let is_atomic m = (not (is_conjunction m) || @@ -120,7 +124,6 @@ let dyck_imply_intro = (dImp None) -------------- A->B,A,Gamma |- G (A Atomique) *) -let atomic_imply_bot_pattern = put_pat mmk "?1 -> ?2" let atomic_imply_step cls gls = let mvb = somatch (clause_type cls gls) atomic_imply_bot_pattern in diff --git a/tactics/termdn.ml b/tactics/termdn.ml index fda033f26..957543e16 100644 --- a/tactics/termdn.ml +++ b/tactics/termdn.ml @@ -3,18 +3,15 @@ open Util open Generic +open Names open Term +open Rawterm (* Discrimination nets of terms. See the module dn.ml for further explanations. Eduardo (5/8/97) *) -type lbl = - | TERM of constr - | DOPER of sorts oper - | DLAMBDA - -type 'a t = (lbl,constr,'a) Dn.t +type 'a t = (constr_label,constr_pattern,'a) Dn.t (*If we have: f a b c ..., decomp gives: (f,[a;b;c;...])*) @@ -24,26 +21,31 @@ let decomp = | DOP2(Cast,c1,_) -> decrec acc c1 | c -> (c,acc) in - decrec [] + decrec [] +let decomp_pat = + let rec decrec acc = function + | PApp (f,args) -> decrec (Array.to_list args @ acc) f + | c -> (c,acc) + in + decrec [] let constr_pat_discr t = - if not(occur_meta t) then + if not (occur_meta_pattern t) then None else - match decomp t with - (* | DOPN(Const _,_) as c,l -> Some(TERM c,l) *) - | DOPN(MutInd _,_) as c,l -> Some(TERM c,l) - | DOPN(MutConstruct _,_) as c,l -> Some(TERM c,l) - | VAR _ as c,l -> Some(TERM c,l) - | c -> None + match decomp_pat t with + | PRef (RInd (ind_sp,_)), args -> Some(IndNode ind_sp,args) + | PRef (RConstruct (cstr_sp,_)), args -> Some(CstrNode cstr_sp,args) + | PRef (RVar id), args -> Some(VarNode id,args) + | _ -> None let constr_val_discr t = match decomp t with (* DOPN(Const _,_) as c,l -> Some(TERM c,l) *) - | DOPN(MutInd _,_) as c,l -> Some(TERM c,l) - | DOPN(MutConstruct _,_) as c,l -> Some(TERM c,l) - | VAR _ as c,l -> Some(TERM c,l) + | DOPN(MutInd ind_sp,_) as c,l -> Some(IndNode ind_sp,l) + | DOPN(MutConstruct cstr_sp,_) as c,l -> Some(CstrNode cstr_sp,l) + | VAR id as c,l -> Some(VarNode id,l) | c -> None (* Les deux fonctions suivantes ecrasaient les precedentes, diff --git a/tactics/termdn.mli b/tactics/termdn.mli index 62066f604..1b8a132ab 100644 --- a/tactics/termdn.mli +++ b/tactics/termdn.mli @@ -4,6 +4,7 @@ (*i*) open Generic open Term +open Rawterm (*i*) (* Discrimination nets of terms. *) @@ -22,26 +23,23 @@ val create : unit -> 'a t (* [add t (c,a)] adds to table [t] pattern [c] associated to action [act] *) -val add : 'a t -> (constr * 'a) -> 'a t +val add : 'a t -> (constr_pattern * 'a) -> 'a t -val rmv : 'a t -> (constr * 'a) -> 'a t +val rmv : 'a t -> (constr_pattern * 'a) -> 'a t (* [lookup t c] looks for patterns (with their action) matching term [c] *) -val lookup : 'a t -> constr -> (constr * 'a) list +val lookup : 'a t -> constr -> (constr_pattern * 'a) list -val app : ((constr * 'a) -> unit) -> 'a t -> unit +val app : ((constr_pattern * 'a) -> unit) -> 'a t -> unit (*i*) (* These are for Nbtermdn *) -type lbl = - | TERM of constr - | DOPER of sorts oper - | DLAMBDA - -val constr_pat_discr : constr -> (lbl * constr list) option -val constr_val_discr : constr -> (lbl * constr list) option +val constr_pat_discr : + constr_pattern -> (constr_label * constr_pattern list) option +val constr_val_discr : + constr -> (constr_label * constr list) option (*i*) |