diff options
| -rw-r--r-- | proofs/pattern.ml | 241 | ||||
| -rw-r--r-- | proofs/pattern.mli | 60 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 229 | ||||
| -rw-r--r-- | tactics/hipattern.mli (renamed from tactics/pattern.mli) | 15 | ||||
| -rw-r--r-- | tactics/pattern.ml | 384 |
5 files changed, 532 insertions, 397 deletions
diff --git a/proofs/pattern.ml b/proofs/pattern.ml new file mode 100644 index 000000000..56a9db7f2 --- /dev/null +++ b/proofs/pattern.ml @@ -0,0 +1,241 @@ + +(* $Id$ *) + +open Util +open Generic +open Names +open Term +open Reduction +open Rawterm + +type constr_pattern = + | PRef of Term.constr array reference + | PRel of int + | PApp of constr_pattern * constr_pattern array + | PSoApp of int * constr list + | PBinder of binder_kind * name * constr_pattern * constr_pattern + | PLet of identifier * constr_pattern * constr_pattern * constr_pattern + | PSort of rawsort + | PMeta of int option + | PCase of constr_pattern option * constr_pattern * constr_pattern array +(*i + | Prec of loc * fix_kind * identifier array * + constr_pattern array * constr_pattern array +i*) + +let rec occur_meta_pattern = function + | PApp (f,args) -> + (occur_meta_pattern f) or (array_exists occur_meta_pattern args) + | PBinder(_,na,t,c) -> (occur_meta_pattern t) or (occur_meta_pattern c) + | PCase(None,c,br) -> + (occur_meta_pattern c) or (array_exists occur_meta_pattern br) + | PCase(Some p,c,br) -> + (occur_meta_pattern p) or + (occur_meta_pattern c) or (array_exists occur_meta_pattern br) + | PLet(id,a,t,c) -> + (occur_meta_pattern a) or (occur_meta_pattern t) + or (occur_meta_pattern c) + | PMeta _ | PSoApp _ -> true + | PRel _ | PSort _ -> false + + (* On suppose que les ctxt des cstes ne contient pas de meta *) + | PRef _ -> false + +type constr_label = + | ConstNode of section_path + | IndNode of inductive_path + | CstrNode of constructor_path + | VarNode of identifier +(* + | ... +*) + +exception BoundPattern;; + +let label_of_ref = function + | RConst (sp,_) -> ConstNode sp + | RInd (sp,_) -> IndNode sp + | RConstruct (sp,_) -> CstrNode sp + | RVar id -> VarNode id + | RAbst _ -> error "Obsolète" + | REVar _ | RMeta _ -> raise BoundPattern + +let rec head_pattern_bound t = + match t with + | PBinder (BProd,_,_,b) -> head_pattern_bound b + | PApp (c,args) -> head_pattern_bound c + | PCase (p,c,br) -> head_pattern_bound c + | PLet (id,a,t,c) -> head_pattern_bound c + | PRef r -> label_of_ref r + | PRel _ | PMeta _ | PSoApp _ | PSort _ -> raise BoundPattern + | PBinder(BLambda,_,_,_) -> anomaly "head_pattern_bound: not a type" + +let head_of_constr_reference = function + | DOPN (Const sp,_) -> ConstNode sp + | DOPN (MutConstruct sp,_) -> CstrNode sp + | DOPN (MutInd sp,_) -> IndNode sp + | VAR id -> VarNode id + | _ -> anomaly "Not a rigid reference" + + +(* 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, + matching, in the case where the pattern is a pattern in the sense + of Dale Miller. + + ALGORITHM: + + Given a pattern, we decompose it, flattening Cast's and apply's, + recursing on all operators, and pushing the name of the binder each + time we descend a binder. + + When we reach a first-order variable, we ask that the corresponding + term's free-rels all be higher than the depth of the current stack. + + When we reach a second-order application, we ask that the + intersection of the free-rels of the term and the current stack be + contained in the arguments of the application, and in that case, we + construct a DLAM with the names on the stack. + + *) + +let constrain ((n : int),(m : constr)) sigma = + if List.mem_assoc n sigma then + if eq_constr m (List.assoc n sigma) then sigma else error "somatch" + else + (n,m)::sigma + +let build_dlam toabstract stk (m : constr) = + let rec buildrec m p_0 p_1 = match p_0,p_1 with + | (_, []) -> m + | (n, (na::tl)) -> + if List.mem n toabstract then + buildrec (DLAM(na,m)) (n+1) tl + else + buildrec (pop m) (n+1) tl + in + buildrec m 1 stk + +let memb_metavars m n = + match (m,n) with + | (None, _) -> true + | (Some mvs, n) -> List.mem n mvs + +let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 + +exception PatternMatchingFailure + +let matches_core convert = + let rec sorec stk sigma p t = + let cT = whd_castapp t in + match p,kind_of_term cT with + | PSoApp (n,args),m -> + let relargs = + List.map + (function + | Rel n -> n + | _ -> error "Only bound indices are currently allowed in second order pattern matching") + args in + 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 (Some n), m -> + 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 + + | PMeta None, m -> sigma + + | PRef (RVar v1), IsVar v2 when v1 = v2 -> sigma + + | PRef (RConst (sp1,ctxt1)), IsConst (sp2,ctxt2) + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma + + | PRef (RInd (sp1,ctxt1)), IsMutInd (sp2,ctxt2) + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma + + | PRef (RConstruct (sp1,ctxt1)), IsMutConstruct (sp2,ctxt2) + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma + + | 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 + + | PRef (RConst (sp1,ctxt1)), _ when convert <> None -> + let (env,evars) = out_some convert in + if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma + else raise PatternMatchingFailure + + | PCase (_,a1,br1), IsMutCase (ci,p2,a2,br2) -> + (* On ne teste pas le prédicat *) + array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) + br1 br2 + + | (PLet _,_) | _,(IsFix _ | IsCoFix _) -> + error "somatch: not implemented" + + | _ -> raise PatternMatchingFailure + + in + sorec [] [] + +let matches = matches_core None + +let is_matching pat n = + try let _ = matches pat n in true + with PatternMatchingFailure -> false + +let matches_conv env sigma = matches_core (Some (env,sigma)) + +let is_matching_conv env sigma pat n = + try let _ = matches_conv env sigma pat n in true + with PatternMatchingFailure -> false + +let rec pattern_of_constr t = + match kind_of_term t with + | IsRel n -> PRel n + | IsMeta n -> PMeta (Some 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, ctxt)) + | IsMutInd (ind_sp,ctxt) -> + PRef (RInd (ind_sp, ctxt)) + | IsMutConstruct (cstr_sp,ctxt) -> + PRef (RConstruct (cstr_sp, ctxt)) + | IsEvar (n,ctxt) -> + PRef (REVar (n,ctxt)) + | IsMutCase (ci,p,a,br) -> + PCase (Some (pattern_of_constr p),pattern_of_constr a, + Array.map pattern_of_constr br) + | IsFix _ | IsCoFix _ -> + error "pattern_of_constr: (co)fix currently not supported" + | IsAbst _ | IsXtra _ -> anomaly "No longer supported" diff --git a/proofs/pattern.mli b/proofs/pattern.mli new file mode 100644 index 000000000..a4685a468 --- /dev/null +++ b/proofs/pattern.mli @@ -0,0 +1,60 @@ + +(* $Id$ *) + +(*i*) +open Names +open Sign +open Term +open Environ +(*i*) + +type constr_pattern = + | PRef of constr array reference + | PRel of int + | PApp of constr_pattern * constr_pattern array + | PSoApp of int * constr list + | PBinder of binder_kind * name * constr_pattern * constr_pattern + | PLet of identifier * constr_pattern * constr_pattern * constr_pattern + | PSort of Rawterm.rawsort + | PMeta of int option + | PCase of constr_pattern option * constr_pattern * constr_pattern array + +val occur_meta_pattern : constr_pattern -> bool + +type constr_label = + | ConstNode of section_path + | IndNode of inductive_path + | CstrNode of constructor_path + | VarNode of identifier + +exception BoundPattern + +(* [head_pattern_bound t] extracts the head variable/constant of the + type [t] or raises [BoundPattern] (even if a sort); it raises an anomaly + if [t] is an abstraction *) + +val head_pattern_bound : constr_pattern -> constr_label + +(* [head_of_constr_reference c] assumes [r] denotes a reference and + returns its label; raises an anomaly otherwise *) + +val head_of_constr_reference : Term.constr -> constr_label + +(* [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 -> constr_pattern + + +exception PatternMatchingFailure + +val matches : + constr_pattern -> constr -> (int * constr) list +val matches_conv : + env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list +val is_matching : + constr_pattern -> constr -> bool +val is_matching_conv : + env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool + diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml new file mode 100644 index 000000000..70297f586 --- /dev/null +++ b/tactics/hipattern.ml @@ -0,0 +1,229 @@ + +(* $Id$ *) + +open Pp +open Util +open Names +open Generic +open Term +open Reduction +open Evd +open Environ +open Proof_trees +open Stock +open Clenv +open Pattern + +(* The pattern table for tactics. *) + +(* Description: see the interface. *) + +(* First part : introduction of term patterns *) + +type module_mark = Stock.module_mark + +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 = + Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_constr s) + +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 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 = + let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) in + (collect_metas c, c) + +type marked_term = (int list * constr) Stock.stocked + +let (squeleton_stock : (int list * constr) Stock.stock) = + Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton } + +let put_squel = Stock.stock squeleton_stock +let get_squel_core = Stock.retrieve squeleton_stock + + +let dest_somatch n pat = + let _,m = get_pat pat in + matches m n + +let somatches n pat = + let _,m = get_pat pat in + is_matching m n + +let dest_somatch_conv env sigma n pat = + let _,m = get_pat pat in + matches_conv env sigma m n + +let somatches_conv env sigma n pat = + let _,m = get_pat pat in + is_matching_conv env sigma m n + +let soinstance squel arglist = + let mvs,c = get_squel_core squel in + let mvb = List.combine mvs arglist in + Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) + empty_env Evd.empty c) + +let get_squel m = + let mvs, c = get_squel_core m in + if mvs = [] then c + else errorlabstrm "get_squel" + [< Printer.prterm c; + 'sPC; 'sTR "is not a closed squeleton, use 'soinstance'" >] + +(* I implemented the following functions which test whether a term t + is an inductive but non-recursive type, a general conjuction, a + general disjunction, or a type with no constructors. + + They are more general than matching with or_term, and_term, etc, + since they do not depend on the name of the type. Hence, they + also work on ad-hoc disjunctions introduced by the user. + + -- Eduardo (6/8/97). *) + +let mmk = make_module_marker ["Prelude"] + +type 'a matching_function = constr -> 'a option + +type testing_function = constr -> bool + +let op2bool = function Some _ -> true | None -> false + +let match_with_non_recursive_type t = + match kind_of_term t with + | IsAppL _ -> + let (hdapp,args) = decomp_app t in + (match kind_of_term hdapp with + | IsMutInd ind -> + if not (Global.mind_is_recursive ind) then + Some (hdapp,args) + else + None + | _ -> None) + | _ -> None + +let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) + +(* A general conjunction type is a non-recursive inductive type with + only one constructor. *) + +let match_with_conjunction t = + let (hdapp,args) = decomp_app t in + match kind_of_term hdapp with + | IsMutInd ind -> + let nconstr = Global.mind_nconstr ind in + if (nconstr = 1) && + (not (Global.mind_is_recursive ind)) && + (nb_prod (Global.mind_arity ind)) = (Global.mind_nparams ind) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_conjunction t = op2bool (match_with_conjunction t) + +(* A general disjunction type is a non-recursive inductive type all + whose constructors have a single argument. *) + +let match_with_disjunction 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 only_one_arg c = + ((nb_prod c) - (Global.mind_nparams ind)) = 1 in + if (array_for_all only_one_arg constr_types) && + (not (Global.mind_is_recursive ind)) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_disjunction t = op2bool (match_with_disjunction t) + +let match_with_empty_type t = + let (hdapp,args) = decomp_app t in + match (kind_of_term hdapp) with + | IsMutInd ind -> + let nconstr = Global.mind_nconstr ind in + if nconstr = 0 then Some hdapp else None + | _ -> None + +let is_empty_type t = op2bool (match_with_empty_type t) + +let match_with_unit_type 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 nconstr = Global.mind_nconstr ind in + let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in + if nconstr = 1 && (array_for_all zero_args constr_types) then + Some hdapp + else + None + | _ -> None + +let is_unit_type t = op2bool (match_with_unit_type t) + + +(* Checks if a given term is an application of an + 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 nconstr = Global.mind_nconstr ind in + if nconstr = 1 && + (somatches constr_types.(0) refl_rel_pat1 || + somatches constr_types.(0) refl_rel_pat2) + then + Some (hdapp,args) + else + None + | _ -> None + +let is_equation t = op2bool (match_with_equation t) + +let arrow_pat = put_pat mmk "(?1 -> ?2)" + +let match_with_nottype t = + try + let sigma = dest_somatch t arrow_pat in + let arg = List.assoc 1 sigma in + let mind = List.assoc 2 sigma in + if is_empty_type mind then Some (mind,arg) else None + with PatternMatchingFailure -> None + +let is_nottype t = op2bool (match_with_nottype t) + +let is_imp_term = function + | DOP2(Prod,_,DLAM(_,b)) -> not (dependent (Rel 1) b) + | _ -> false + + + diff --git a/tactics/pattern.mli b/tactics/hipattern.mli index e16a8ea77..0235fa79f 100644 --- a/tactics/pattern.mli +++ b/tactics/hipattern.mli @@ -58,12 +58,6 @@ 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] *) @@ -95,22 +89,17 @@ i*) contained in the arguments of the application, and in that case, we construct a [DLAM] with the names on the stack. *) -(*i Devrait être une fonction de filtrage externe i*) -val somatch : int list option -> Rawterm.constr_pattern -> constr -> (int * constr) list - - -exception PatternMatchingFailure (* [dest_somatch c pat] matches [c] against [pat] and returns the resulting assignment of metavariables; it raises [PatternMatchingFailure] if not matchable *) - +(* val dest_somatch : constr -> marked_pattern -> constr list (* [somatches c pat] just tells if [c] matches against [pat] *) val somatches : constr -> marked_pattern -> bool - +*) (* [dest_somatch_conv env sigma] matches up to conversion in environment [(env,sgima)] when constants in pattern are concerned; diff --git a/tactics/pattern.ml b/tactics/pattern.ml deleted file mode 100644 index 04f845adc..000000000 --- a/tactics/pattern.ml +++ /dev/null @@ -1,384 +0,0 @@ - -(* $Id$ *) - -open Pp -open Util -open Names -open Generic -open Term -open Reduction -open Evd -open Environ -open Proof_trees -open Stock -open Clenv -open Rawterm - -(* The pattern table for tactics. *) - -(* Description: see the interface. *) - -(* First part : introduction of term patterns *) - -type module_mark = Stock.module_mark - -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 = - Astterm.interp_constrpattern Evd.empty (Global.env()) (parse_constr s) - -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 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 = - let c = Astterm.interp_constr Evd.empty (Global.env()) (parse_constr s) in - (collect_metas c, c) - -type marked_term = (int list * constr) Stock.stocked - -let (squeleton_stock : (int list * constr) Stock.stock) = - Stock.make_stock { name = "SQUELETON"; proc = parse_squeleton } - -let put_squel = Stock.stock squeleton_stock -let get_squel_core = 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, - matching, in the case where the pattern is a pattern in the sense - of Dale Miller. - - ALGORITHM: - - Given a pattern, we decompose it, flattening Cast's and apply's, - recursing on all operators, and pushing the name of the binder each - time we descend a binder. - - When we reach a first-order variable, we ask that the corresponding - term's free-rels all be higher than the depth of the current stack. - - When we reach a second-order application, we ask that the - intersection of the free-rels of the term and the current stack be - contained in the arguments of the application, and in that case, we - construct a DLAM with the names on the stack. - - *) - -let dest_soapp_operator = function - | DOPN(XTRA("$SOAPP"),v) -> - (match Array.to_list v with - | (DOP0(Meta n))::l -> - let l' = - List.map (function (Rel i) -> i | _ -> error "somatch") l in - Some (n, list_uniquize l') - | _ -> error "somatch") - | (DOP2(XTRA("$SOAPP"),DOP0(Meta n),Rel p)) -> - Some (n,list_uniquize [p]) - | _ -> None - -let constrain ((n : int),(m : constr)) sigma = - if List.mem_assoc n sigma then - if eq_constr m (List.assoc n sigma) then sigma else error "somatch" - else - (n,m)::sigma - -let build_dlam toabstract stk (m : constr) = - let rec buildrec m p_0 p_1 = match p_0,p_1 with - | (_, []) -> m - | (n, (na::tl)) -> - if List.mem n toabstract then - buildrec (DLAM(na,m)) (n+1) tl - else - buildrec (pop m) (n+1) tl - in - buildrec m 1 stk - -let memb_metavars m n = - match (m,n) with - | (None, _) -> true - | (Some mvs, n) -> List.mem n mvs - -let eq_context ctxt1 ctxt2 = array_for_all2 eq_constr ctxt1 ctxt2 - -exception PatternMatchingFailure - -let somatch_core convert 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 && eq_context ctxt1 ctxt2 -> sigma - - | PRef (RInd (sp1,ctxt1)), IsMutInd (sp2,ctxt2) - when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma - - | PRef (RConstruct (sp1,ctxt1)), IsMutConstruct (sp2,ctxt2) - when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma - - | 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 - - | PRef (RConst (sp1,ctxt1)), _ when convert <> None -> - let (env,evars) = out_some convert in - if is_conv env evars (mkConst (sp1,ctxt1)) cT then sigma - else raise PatternMatchingFailure - - | _, (IsFix _ | IsMutCase _ | IsCoFix _) -> - error "somatch: not implemented" - - | _ -> raise PatternMatchingFailure - - in - sorec [] [] - -let somatch = somatch_core None - -let dest_somatch n pat = - 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 somatches n pat = - 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_conv env sigma n pat = - let mvs,m = get_pat pat in - somatch_core (Some (env,sigma)) (Some (list_uniquize mvs)) m n - -let somatches_conv env sigma n pat = - try - let _ = dest_somatch_conv env sigma n pat in true - with e when Logic.catchable_exception e -> - false - -let soinstance squel arglist = - let mvs,c = get_squel_core squel in - let mvb = List.combine mvs arglist in - Sosub.soexecute (Reduction.strong (fun _ _ -> Reduction.whd_meta mvb) - empty_env Evd.empty c) - -let get_squel m = - let mvs, c = get_squel_core m in - if mvs = [] then c else error "Not a closed squeleton, use 'soinstance'" - -(* I implemented the following functions which test whether a term t - is an inductive but non-recursive type, a general conjuction, a - general disjunction, or a type with no constructors. - - They are more general than matching with or_term, and_term, etc, - since they do not depend on the name of the type. Hence, they - also work on ad-hoc disjunctions introduced by the user. - - -- Eduardo (6/8/97). *) - -let mmk = make_module_marker ["Prelude"] - -type 'a matching_function = constr -> 'a option - -type testing_function = constr -> bool - -let op2bool = function Some _ -> true | None -> false - -let match_with_non_recursive_type t = - match kind_of_term t with - | IsAppL _ -> - let (hdapp,args) = decomp_app t in - (match kind_of_term hdapp with - | IsMutInd ind -> - if not (Global.mind_is_recursive ind) then - Some (hdapp,args) - else - None - | _ -> None) - | _ -> None - -let is_non_recursive_type t = op2bool (match_with_non_recursive_type t) - -(* A general conjunction type is a non-recursive inductive type with - only one constructor. *) - -let match_with_conjunction t = - let (hdapp,args) = decomp_app t in - match kind_of_term hdapp with - | IsMutInd ind -> - let nconstr = Global.mind_nconstr ind in - if (nconstr = 1) && - (not (Global.mind_is_recursive ind)) && - (nb_prod (Global.mind_arity ind)) = (Global.mind_nparams ind) - then - Some (hdapp,args) - else - None - | _ -> None - -let is_conjunction t = op2bool (match_with_conjunction t) - -(* A general disjunction type is a non-recursive inductive type all - whose constructors have a single argument. *) - -let match_with_disjunction 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 only_one_arg c = - ((nb_prod c) - (Global.mind_nparams ind)) = 1 in - if (array_for_all only_one_arg constr_types) && - (not (Global.mind_is_recursive ind)) - then - Some (hdapp,args) - else - None - | _ -> None - -let is_disjunction t = op2bool (match_with_disjunction t) - -let match_with_empty_type t = - let (hdapp,args) = decomp_app t in - match (kind_of_term hdapp) with - | IsMutInd ind -> - let nconstr = Global.mind_nconstr ind in - if nconstr = 0 then Some hdapp else None - | _ -> None - -let is_empty_type t = op2bool (match_with_empty_type t) - -let match_with_unit_type 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 nconstr = Global.mind_nconstr ind in - let zero_args c = ((nb_prod c) - (Global.mind_nparams ind)) = 0 in - if nconstr = 1 && (array_for_all zero_args constr_types) then - Some hdapp - else - None - | _ -> None - -let is_unit_type t = op2bool (match_with_unit_type t) - - -(* Checks if a given term is an application of an - 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 nconstr = Global.mind_nconstr ind in - if nconstr = 1 && - (somatches constr_types.(0) refl_rel_pat1 || - somatches constr_types.(0) refl_rel_pat2) - then - Some (hdapp,args) - else - None - | _ -> None - -let is_equation t = op2bool (match_with_equation t) - -let match_with_nottype t = - let notpat = put_pat mmk "(?1 -> ?2)" in - try - (match dest_somatch t notpat with - | [arg;mind] when is_empty_type mind -> Some (mind,arg) - | [arg;mind] -> None - | _ -> anomaly "match_with_nottype") - with UserError ("somatches",_) -> - None - -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, ctxt)) - | IsMutInd (ind_sp,ctxt) -> - PRef (RInd (ind_sp, ctxt)) - | IsMutConstruct (cstr_sp,ctxt) -> - PRef (RConstruct (cstr_sp, 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" - - |