Decoupage de tactics/pattern en proofs/pattern et tactics/hipattern

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

1 files changed, 241 insertions, 0 deletions

diff --git a/proofs/pattern.ml b/proofs/pattern.ml
new file mode 100644
index 0000000000..56a9db7f28
--- /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"