From 2a8ac977519aa0c980d2906b60bb8fb258900d28 Mon Sep 17 00:00:00 2001 From: delahaye Date: Fri, 21 Jul 2000 15:29:26 +0000 Subject: Pattern -> parsing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@564 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/pattern.ml | 245 ++++++++++++++++++++++++++++++++++++++++++++++++++++ parsing/pattern.mli | 77 +++++++++++++++++ proofs/pattern.ml | 245 ---------------------------------------------------- proofs/pattern.mli | 77 ----------------- 4 files changed, 322 insertions(+), 322 deletions(-) create mode 100644 parsing/pattern.ml create mode 100644 parsing/pattern.mli delete mode 100644 proofs/pattern.ml delete mode 100644 proofs/pattern.mli diff --git a/parsing/pattern.ml b/parsing/pattern.ml new file mode 100644 index 0000000000..6d3c362d68 --- /dev/null +++ b/parsing/pattern.ml @@ -0,0 +1,245 @@ + +(* $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_pattern 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 _ -> 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. + + *) + +exception PatternMatchingFailure + +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 raise PatternMatchingFailure + 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 + +let matches_core convert pat c = + 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 + | PRel 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)), IsConst (sp2,ctxt2) + when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma + + | 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 + Sort.list (fun (a,_) (b,_) -> a 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,_) -> 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/parsing/pattern.mli b/parsing/pattern.mli new file mode 100644 index 0000000000..b725d90446 --- /dev/null +++ b/parsing/pattern.mli @@ -0,0 +1,77 @@ + +(* $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_pattern 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 + +(* [matches pat c] matches [c] against [pat] and returns the resulting + assignment of metavariables; it raises [PatternMatchingFailure] if + not matchable; bindings are given in increasing order based on the + numbers given in the pattern *) +val matches : + constr_pattern -> constr -> (int * constr) list + +(* [is_matching pat c] just tells if [c] matches against [pat] *) + +val is_matching : + constr_pattern -> constr -> bool + +(* [matches_conv env sigma] matches up to conversion in environment + [(env,sigma)] when constants in pattern are concerned; it raises + [PatternMatchingFailure] if not matchable; bindings are given in + increasing order based on the numbers given in the pattern *) + +val matches_conv : + env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list + +(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] + up to conversion for constants in patterns *) + +val is_matching_conv : + env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool + diff --git a/proofs/pattern.ml b/proofs/pattern.ml deleted file mode 100644 index 6d3c362d68..0000000000 --- a/proofs/pattern.ml +++ /dev/null @@ -1,245 +0,0 @@ - -(* $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_pattern 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 _ -> 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. - - *) - -exception PatternMatchingFailure - -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 raise PatternMatchingFailure - 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 - -let matches_core convert pat c = - 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 - | PRel 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)), IsConst (sp2,ctxt2) - when sp1 = sp2 && eq_context ctxt1 ctxt2 -> sigma - - | 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 - Sort.list (fun (a,_) (b,_) -> a 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,_) -> 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 deleted file mode 100644 index b725d90446..0000000000 --- a/proofs/pattern.mli +++ /dev/null @@ -1,77 +0,0 @@ - -(* $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_pattern 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 - -(* [matches pat c] matches [c] against [pat] and returns the resulting - assignment of metavariables; it raises [PatternMatchingFailure] if - not matchable; bindings are given in increasing order based on the - numbers given in the pattern *) -val matches : - constr_pattern -> constr -> (int * constr) list - -(* [is_matching pat c] just tells if [c] matches against [pat] *) - -val is_matching : - constr_pattern -> constr -> bool - -(* [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) - -val matches_conv : - env -> 'a Evd.evar_map -> constr_pattern -> constr -> (int * constr) list - -(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) - -val is_matching_conv : - env -> 'a Evd.evar_map -> constr_pattern -> constr -> bool - -- cgit v1.2.3