Pattern sera mieux dans Pretyping; relâchement head_pattern_bound

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 0 insertions, 411 deletions

diff --git a/parsing/pattern.ml b/parsing/pattern.ml
deleted file mode 100644
index 3dd339d46..000000000
--- a/parsing/pattern.ml
+++ /dev/null
@@ -1,325 +0,0 @@
-
-(* $Id$ *)
-
-open Util
-open Names
-open Term
-open Reduction
-open Rawterm
-open Environ
-
-type constr_pattern =
-  | PRef of global_reference
-  | PVar of identifier
-  | 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
-  | PSort of rawsort
-  | PMeta of int option
-  | PCase of constr_pattern option * constr_pattern * constr_pattern array
-  | PFix of fixpoint
-  | PCoFix of cofixpoint
-
-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)
-  | PMeta _ | PSoApp _ -> true
-  | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
-
-type constr_label =
-  | ConstNode of section_path
-  | IndNode of inductive_path
-  | CstrNode of constructor_path
-  | VarNode of identifier
-  | SectionVarNode of section_path
-(*
-  | ... 
-*)
-
-exception BoundPattern;;
-
-let label_of_ref = function
-  | ConstRef sp     -> ConstNode sp
-  | IndRef sp       -> IndNode sp
-  | ConstructRef sp -> CstrNode sp
-  | VarRef sp       -> SectionVarNode sp
-  | EvarRef n          -> raise BoundPattern
-
-let rec head_pattern_bound t =
-  match t with
-    | PBinder ((BProd|BLetIn),_,_,b) -> head_pattern_bound b 
-    | PApp (c,args)         -> head_pattern_bound c
-    | PCase (p,c,br)        -> head_pattern_bound c
-    | PRef r                -> label_of_ref r
-    | PVar id               -> VarNode id
-    | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _ -> raise BoundPattern
-    | PBinder(BLambda,_,_,_) | PCoFix _ ->
-      anomaly "head_pattern_bound: not a type"
-
-let head_of_constr_reference c = match kind_of_term c with
-  | IsConst (sp,_) -> ConstNode sp
-  | IsMutConstruct (sp,_) -> CstrNode sp
-  | IsMutInd (sp,_) -> IndNode sp
-  | IsVar 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 [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 LAMBDA 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_lambda toabstract stk (m : constr) = 
-  let rec buildrec m p_0 p_1 = match p_0,p_1 with 
-    | (_, []) -> m
-    | (n, (na,t)::tl) -> 
-	if List.mem n toabstract then
-          buildrec (mkLambda (na,t,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 = strip_outer_cast 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_lambda 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 (VarRef sp1), IsVar v2 when basename sp1 = v2 -> sigma
-
-      | PVar v1, IsVar v2 when v1 = v2 -> sigma
-
-      | PRef ref, _ when Declare.constr_of_reference Evd.empty (Global.env()) ref = cT -> 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), IsApp (c2,arg2) ->
-        (try array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
-         with Invalid_argument _ -> raise PatternMatchingFailure)
-
-      | PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
-
-      | PBinder(BLambda,na1,c1,d1), IsLambda(na2,c2,d2) ->
-	  sorec ((na2,c2)::stk) (sorec stk sigma c1 c2) d1 d2
-
-      | PBinder(BLetIn,na1,c1,d1), IsLetIn(na2,c2,t2,d2) ->
-	  sorec ((na2,t2)::stk) (sorec stk sigma c1 c2) d1 d2
-
-      | PRef (ConstRef _ as ref), _ when convert <> None ->
-	  let (env,evars) = out_some convert in
-	  let c = Declare.constr_of_reference Evd.empty env ref in
-	  if is_conv env evars c cT then sigma
-	  else raise PatternMatchingFailure
-
-      | PCase (_,a1,br1), IsMutCase (_,_,a2,br2) ->
-	  (* On ne teste pas le prédicat *)
-	  array_fold_left2 (sorec stk) (sorec stk sigma a1 a2)
-	    br1 br2
-      (* À faire *)
-      |	PFix f0, IsFix f1 when f0 = f1 -> sigma
-      |	PCoFix c0, IsCoFix c1 when c0 = c1 -> sigma
-      | _ -> raise PatternMatchingFailure
-
-  in 
-  Sort.list (fun (a,_) (b,_) -> a<b) (sorec [] [] pat c)
-
-let matches = matches_core None
-
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
-
-(* Tells if it is an authorized occurrence *)
-let authorized_occ nocc mres =
-  if nocc = 0 then mres
-  else raise (NextOccurrence nocc)
-
-(* Tries matches according to the occurrence *)
-let rec try_matches nocc pat = function
-  | [] -> raise (NextOccurrence nocc)
-  | c::tl ->
-    (try authorized_occ nocc (matches pat c) with
-    | PatternMatchingFailure -> (try_matches nocc pat tl)
-    | NextOccurrence nocc -> (try_matches (nocc - 1) pat tl))
-
-(* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match nocc pat c =
-  match kind_of_term c with
-  | IsCast (c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1] in
-      (lm,mkCast (List.hd lc, c2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
-      (lm,mkCast (List.hd lc, c2)))
-  | IsLambda (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,mkLambda (x,List.hd lc,List.nth lc 1))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,mkLambda (x,List.hd lc,List.nth lc 1)))
-  | IsProd (x,c1,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;c2] in
-      (lm,mkProd (x,List.hd lc,List.nth lc 1))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
-      (lm,mkProd (x,List.hd lc,List.nth lc 1)))
-  | IsLetIn (x,c1,t2,c2) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
-      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
-    | NextOccurrence nocc ->
-      let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
-      (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
-  | IsApp (c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
-      (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
-    | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
-      (lm,mkApp (List.hd le, Array.of_list (List.tl le))))
-  | IsMutCase (ci,hd,c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
-    | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
-      (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le))
-    | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::Array.to_list lc) in
-      (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)))
-  | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
-  | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ ->
-    (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
-    | PatternMatchingFailure -> raise (NextOccurrence nocc)
-    | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
-
-(* Tries [sub_match] for all terms in the list *)
-and try_sub_match nocc pat lc =
-  let rec try_sub_match_rec nocc pat lacc = function
-    | [] -> raise (NextOccurrence nocc)
-    | c::tl ->
-      (try 
-         let (lm,ce) = sub_match nocc pat c in
-         (lm,lacc@(ce::tl))
-       with
-      | NextOccurrence nocc -> try_sub_match_rec nocc pat (lacc@[c]) tl) in
-  try_sub_match_rec nocc pat [] lc
-
-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 -> PVar id
-    | IsSort (Prop c) -> PSort (RProp c)
-    | IsSort (Type _) -> PSort RType
-    | IsCast (c,_)      -> pattern_of_constr c
-    | IsLetIn (na,c,_,b)   ->
-	PBinder (BLetIn,na,pattern_of_constr c,pattern_of_constr b)
-    | 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)
-    | IsApp (f,args)   ->
-	PApp (pattern_of_constr f, Array.map pattern_of_constr args)
-    | IsConst (sp,ctxt)         ->
-	pattern_of_ref (ConstRef sp) ctxt
-    | IsMutInd (sp,ctxt)        ->
-	pattern_of_ref (IndRef sp) ctxt
-    | IsMutConstruct (sp,ctxt) ->
-	pattern_of_ref (ConstructRef sp) ctxt
-    | IsEvar (n,ctxt) ->
-	pattern_of_ref (EvarRef n) ctxt
-    | IsMutCase (ci,p,a,br) ->
-	PCase (Some (pattern_of_constr p),pattern_of_constr a,
-	       Array.map pattern_of_constr br)
-    | IsFix f -> PFix f
-    | IsCoFix _ ->
-	error "pattern_of_constr: (co)fix currently not supported"
-    | IsXtra _   -> anomaly "No longer supported"
-
-and pattern_of_ref ref inst =
-  let args = Declare.extract_instance ref inst in
-  let f = PRef ref in
-  if args = [||] then f else PApp (f, Array.map pattern_of_constr args)
diff --git a/parsing/pattern.mli b/parsing/pattern.mli
deleted file mode 100644
index 5c5c28ba1..000000000
--- a/parsing/pattern.mli
+++ /dev/null
@@ -1,86 +0,0 @@
-
-(*i $Id$ i*)
-
-(*i*)
-open Names
-open Sign
-open Term
-open Environ
-(*i*)
-
-type constr_pattern =
-  | PRef of global_reference
-  | PVar of identifier
-  | PRel of int
-  | PApp of constr_pattern * constr_pattern array
-  | PSoApp of int * constr_pattern list
-  | PBinder of Rawterm.binder_kind * name * constr_pattern * constr_pattern
-  | PSort of Rawterm.rawsort
-  | PMeta of int option
-  | PCase of constr_pattern option * constr_pattern * constr_pattern array
-  | PFix of fixpoint
-  | PCoFix of cofixpoint
-
-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
-  | SectionVarNode of section_path
-
-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
-
-(* To skip to the next occurrence *)
-exception NextOccurrence of int
-
-(* Tries to match a subterm of [c] with [pat] *)
-val sub_match :
-  int -> constr_pattern -> constr -> ((int * constr) list * constr)
-
-(* [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