Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 36 insertions, 109 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a32aaf45..b0fe83a3 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cases.ml 8693 2006-04-10 12:05:05Z msozeau $ *)
+(* $Id: cases.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Util
 open Names
@@ -66,13 +66,10 @@ let error_needs_inversion env x t =
 module type S = sig
   val compile_cases :
     loc ->
-    (type_constraint -> env -> rawconstr -> unsafe_judgment) *    
+    (type_constraint -> env -> rawconstr -> unsafe_judgment) *
       Evd.evar_defs ref ->
     type_constraint -> 
-    env ->
-    rawconstr option *
-      (rawconstr * (name * (loc * inductive * name list) option)) list *
-      (loc * identifier list * cases_pattern list * rawconstr) list ->
+    env -> rawconstr option * tomatch_tuple * cases_clauses ->
     unsafe_judgment
 end
 
@@ -138,14 +135,9 @@ type 'a lifted = int * 'a
 
 let insert_lifted a = (0,a);;
 
-(* The pattern variables for [it] are in [user_ids] and the variables
-   to avoid are in [other_ids]. 
-*)
-
 type rhs =
     { rhs_env    : env;
-      other_ids  : identifier list;
-      user_ids   : identifier list;
+      avoid_ids  : identifier list;
       rhs_lift   : int;
       it         : rawconstr }
 
@@ -321,16 +313,21 @@ let rec find_row_ind = function
   | PatCstr(loc,c,_,_) :: _ -> Some (loc,c)
 
 let inductive_template isevars env tmloc ind =
-  let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  let (ntys,_) = splay_prod env (Evd.evars_of !isevars) mip.mind_nf_arity in
+  let arsign = get_full_arity_sign env ind in
   let hole_source = match tmloc with 
     | Some loc -> fun i -> (loc, Evd.TomatchTypeParameter (ind,i))
     | None -> fun _ -> (dummy_loc, Evd.InternalHole) in
-   let (evarl,_) =
+   let (_,evarl,_) =
     List.fold_right
-      (fun (na,ty) (evl,n) ->
-	(e_new_evar isevars env ~src:(hole_source n) (substl evl ty))::evl,n+1)
-      ntys ([],1) in
+      (fun (na,b,ty) (subst,evarl,n) ->
+	match b with
+        | None ->
+	    let ty' = substl subst ty in
+	    let e = e_new_evar isevars env ~src:(hole_source n) ty' in
+	    (e::subst,e::evarl,n+1) 
+	| Some b ->
+	    (b::subst,evarl,n+1))
+      arsign ([],[],1) in
    applist (mkInd ind,List.rev evarl)
 
 let inh_coerce_to_ind isevars env ty tyi =
@@ -349,7 +346,7 @@ let unify_tomatch_with_patterns isevars env typ tm =
 
 let find_tomatch_tycon isevars env loc = function
   (* Try first if some 'in I ...' is present and can be used as a constraint *)
-  | Some (_,ind,_),_ 
+  | Some (_,ind,_,_),_ 
   (* Otherwise try to get constraints from (the 1st) constructor in clauses *)
   | None, Some (_,(ind,_)) ->
       mk_tycon (inductive_template isevars env loc ind)
@@ -434,7 +431,7 @@ let mkDeclTomatch na = function
 
 let map_tomatch_type f = function
   | IsInd (t,ind) -> IsInd (f t,map_inductive_type f ind)
-  | NotInd (c,t) -> NotInd (option_app f c, f t)
+  | NotInd (c,t) -> NotInd (option_map f c, f t)
 
 let liftn_tomatch_type n depth = map_tomatch_type (liftn n depth)
 let lift_tomatch_type n = liftn_tomatch_type n 1
@@ -701,7 +698,7 @@ let get_names env sign eqns =
   (* Otherwise, we take names from the parameters of the constructor but
      avoiding conflicts with user ids *)
   let allvars =
-    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.other_ids) [] eqns in
+    List.fold_left (fun l (_,eqn) -> list_union l eqn.rhs.avoid_ids) [] eqns in
   let names4,_ =
     List.fold_left2
       (fun (l,avoid) d na ->
@@ -793,7 +790,7 @@ let prepare_unif_pb typ cs =
   let typ' =
     if noccur_between_without_evar 1 n typ then lift (-n) typ
     else (* TODO4-1 *)
-      error "Inference of annotation not yet implemented in this case" in
+      error "Unable to infer return clause of this pattern-matching problem" in
   let args = extended_rel_list (-n) cs.cs_args in
   let ci = applist (mkConstruct cs.cs_cstr, cs.cs_params@args) in
 
@@ -1172,7 +1169,7 @@ let rec generalize_problem pb current = function
       let tomatch = regeneralize_index_tomatch (i+1) tomatch in
       { pb with
 	  tomatch = Abstract d :: tomatch;
-          pred = option_app (generalize_predicate current i d) pb'.pred }
+          pred = option_map (generalize_predicate current i d) pb'.pred }
 
 (* No more patterns: typing the right-hand-side of equations *)
 let build_leaf pb =
@@ -1187,7 +1184,7 @@ let build_leaf pb =
 let shift_problem (current,t) pb =
   {pb with
      tomatch = Alias (current,current,NonDepAlias,type_of_tomatch t)::pb.tomatch;
-     pred = option_app (specialize_predicate_var (current,t)) pb.pred;
+     pred = option_map (specialize_predicate_var (current,t)) pb.pred;
      history = push_history_pattern 0 AliasLeaf pb.history;
      mat = List.map remove_current_pattern pb.mat }
 
@@ -1257,7 +1254,7 @@ let build_branch current deps pb eqns const_info =
   { pb with
       env = push_rels sign pb.env;
       tomatch = List.rev_append currents tomatch;
-      pred = option_app (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
+      pred = option_map (specialize_predicate (List.rev typs') dep_sign const_info) pb.pred;
       history = history;
       mat = List.map (push_rels_eqn_with_names sign) submat }
 
@@ -1329,7 +1326,7 @@ and compile_generalization pb d rest =
     { pb with
        env = push_rel d pb.env;
        tomatch = rest;
-       pred = option_app ungeneralize_predicate pb.pred;
+       pred = option_map ungeneralize_predicate pb.pred;
        mat = List.map (push_rels_eqn [d]) pb.mat } in
   let patstat,j = compile pb in
   patstat, 
@@ -1355,7 +1352,7 @@ and compile_alias pb (deppat,nondeppat,d,t) rest =
     {pb with
        env = newenv;
        tomatch = tomatch;
-       pred = option_app (lift_predicate n) pb.pred;
+       pred = option_map (lift_predicate n) pb.pred;
        history = history;
        mat = mat } in
   let patstat,j = compile pb in
@@ -1368,78 +1365,16 @@ substituer après par les initiaux *)
 (**************************************************************************)
 (* Preparation of the pattern-matching problem                            *)
 
-(* Qu'est-ce qui faut pas faire pour traiter les alias ... *)
-
-(* On ne veut pas ajouter de primitive à Environ et le problème, c'est
-   donc de faire un renommage en se contraignant à parcourir l'env
-   dans le sens croissant. Ici, subst renomme des variables repérées
-   par leur numéro et seen_ids collecte celles dont on sait que les
-   variables de subst annule le scope *)
-let rename_env subst env =
-  let n = ref (rel_context_length (rel_context env)) in
-  let seen_ids = ref [] in
-  process_rel_context
-    (fun (na,c,t as d) env ->
-       let d =
-	 try
-	   let id = List.assoc !n subst in
-	   seen_ids := id :: !seen_ids;
-	   (Name id,c,t)
-	 with Not_found ->
-	   match na with
-	     | Name id when List.mem id !seen_ids -> (Anonymous,c,t)
-	     | _ -> d in
-       decr n;
-       push_rel d env) env
-
-let is_dependent_indtype = function
-  | NotInd _ -> false
-  | IsInd (_, IndType(_,realargs)) -> realargs <> []
-
-let prepare_initial_alias_eqn isdep tomatchl eqn =
-  let (subst, pats) = 
-  List.fold_right2
-    (fun pat (tm,tmtyp) (subst, stripped_pats) ->
-       match alias_of_pat pat with
-	 | Anonymous -> (subst, pat::stripped_pats)
-	 | Name idpat ->
-	     match kind_of_term tm with
-	       | Rel n when not (is_dependent_indtype tmtyp) & not isdep
-		   -> (n, idpat)::subst, (unalias_pat pat::stripped_pats)
-	       | _ -> (subst, pat::stripped_pats))
-    eqn.patterns tomatchl ([], []) in
-  let env = rename_env subst eqn.rhs.rhs_env in
-  { eqn with patterns = pats; rhs = { eqn.rhs with rhs_env = env } }
-
-let prepare_initial_aliases isdep tomatchl mat = mat
-(*  List.map (prepare_initial_alias_eqn isdep tomatchl) mat*)
-
-(*
-let prepare_initial_alias lpat tomatchl rhs =
-  List.fold_right2
-    (fun pat tm (stripped_pats, rhs) ->
-       match alias_of_pat pat with
-	 | Anonymous -> (pat::stripped_pats, rhs)
-	 | Name _ as na ->
-	     match tm with
-	       | RVar _ -> 
-		   (unalias_pat pat::stripped_pats, 
-		    RLetIn (dummy_loc, na, tm, rhs))
-	       | _ -> (pat::stripped_pats, rhs))
-    lpat tomatchl ([], rhs)
-*)
 (* builds the matrix of equations testing that each eqn has n patterns
  * and linearizing the _ patterns.
  * Syntactic correctness has already been done in astterm *)
 let matx_of_eqns env tomatchl eqns =
   let build_eqn (loc,ids,lpat,rhs) =
-(*    let initial_lpat,initial_rhs = prepare_initial_alias lpat tomatchl rhs in*)
     let initial_lpat,initial_rhs = lpat,rhs in
     let initial_rhs = rhs in
     let rhs =
       { rhs_env = env;
-	other_ids = ids@(ids_of_named_context (named_context env));
-	user_ids = ids;
+	avoid_ids = ids@(ids_of_named_context (named_context env));
 	rhs_lift = 0;
 	it = initial_rhs } in
     { dependencies = [];
@@ -1547,7 +1482,7 @@ let set_arity_signature dep n arsign tomatchl pred x =
   in
   decomp_block [] pred (tomatchl,arsign)
 
-let prepare_predicate_from_tycon loc dep env isevars tomatchs c =
+let prepare_predicate_from_tycon loc dep env isevars tomatchs sign c =
   let cook (n, l, env, signs) = function
     | c,IsInd (_,IndType(indf,realargs)) ->
 	let indf' = lift_inductive_family n indf in
@@ -1605,8 +1540,8 @@ let extract_arity_signature env0 tomatchl tmsign =
     match tm with
       | NotInd (bo,typ) -> 
 	  (match t with
-	    | None -> [na,option_app (lift n) bo,lift n typ]
-	    | Some (loc,_,_) -> 
+	    | None -> [na,option_map (lift n) bo,lift n typ]
+	    | Some (loc,_,_,_) -> 
  	    user_err_loc (loc,"",
 	    str "Unexpected type annotation for a term of non inductive type"))
       | IsInd (_,IndType(indf,realargs)) ->
@@ -1615,18 +1550,12 @@ let extract_arity_signature env0 tomatchl tmsign =
 	  let nrealargs = List.length realargs in
 	  let realnal =
 	    match t with
-	      | Some (loc,ind',nal) ->
-		  let nparams = List.length params in
+	      | Some (loc,ind',nparams,realnal) ->
 		  if ind <> ind' then
 		    user_err_loc (loc,"",str "Wrong inductive type");
-		  let nindargs = nparams + nrealargs in
-		  (* Normally done at interning time *)
-		  if List.length nal <> nindargs then
-		    error_wrong_numarg_inductive_loc loc env0 ind' nindargs;
-		  let parnal,realnal = list_chop nparams nal in
-		  if List.exists ((<>) Anonymous) parnal then
-		    user_err_loc (loc,"",
-		    str "The parameters of inductive type must be implicit");
+		  if List.length params <> nparams
+		    or nrealargs <> List.length realnal then
+		      anomaly "Ill-formed 'in' clause in cases";
 		  List.rev realnal
 	      | None -> list_tabulate (fun _ -> Anonymous) nrealargs in
 	  let arsign = fst (get_arity env0 indf') in
@@ -1665,7 +1594,7 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       (match tycon with
        | Some (None, t) ->
 	   let names,pred = 
-	     prepare_predicate_from_tycon loc false env isevars tomatchs t 
+	     prepare_predicate_from_tycon loc false env isevars tomatchs sign t 
 	   in Some (build_initial_predicate false names pred)
        | _ -> None)
 
@@ -1677,8 +1606,9 @@ let prepare_predicate loc typing_fun isevars env tomatchs sign tycon = function
       let allnames = List.rev (List.map (List.map pi1) arsign) in
       let predcclj = typing_fun (mk_tycon (new_Type ())) env rtntyp in
       let _ = 
-	option_app (fun tycon -> 
-		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val tycon)
+	option_map (fun tycon -> 
+		      isevars := Coercion.inh_conv_coerces_to loc env !isevars predcclj.uj_val 
+		      (lift_tycon_type (List.length arsign) tycon))
 	  tycon
       in
       let predccl = (j_nf_isevar !isevars predcclj).uj_val in      
@@ -1701,9 +1631,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e
   let tmsign = List.map snd tomatchl in
   let pred = prepare_predicate loc typing_fun isevars env tomatchs tmsign tycon predopt in
     
-  (* We deal with initial aliases *)
-  let matx = prepare_initial_aliases (known_dependent pred) tomatchs matx in 
-    
   (* We push the initial terms to match and push their alias to rhs' envs *)
   (* names of aliases will be recovered from patterns (hence Anonymous here) *)
   let initial_pushed = List.map (fun tm -> Pushed (tm,[])) tomatchs in