Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)

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

1 files changed, 0 insertions, 389 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 0baaa9819..193d0a161 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -462,201 +462,6 @@ let rec pretype tycon env isevars lvar = function
 	     in
 	     { uj_val = v; uj_type = ccl })
 
-  (* Special Case for let constructions to avoid exponential behavior *)      
-  | ROrderedCase (loc,st,po,c,[|f|],xx) when st <> MatchStyle ->
-      let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs) as indt) = 
-	try find_rectype env (evars_of !isevars) cj.uj_type
-	with Not_found ->
-	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj 
-      in
-      let j = match po with
-	 | Some p ->
-             let pj = pretype empty_tycon env isevars lvar p in
-             let dep = is_dependent_elimination env pj.uj_type indf in
-             let ar =
-               arity_of_case_predicate env indf dep (Type (new_univ())) in
-             let _ = e_cumul env isevars pj.uj_type ar in
-	     let pj = j_nf_evar (evars_of !isevars) pj in
-	     let pj = if dep then pj else make_dep_of_undep env indt pj in
-	     let (bty,rsty) = 
-	       Indrec.type_rec_branches 
-		 false env (evars_of !isevars) indt pj.uj_val cj.uj_val 
-	     in
-	     if Array.length bty <> 1 then
-	       error_number_branches_loc 
-		 loc env (evars_of !isevars) cj (Array.length bty);
-	     let fj = 
-	       let tyc = bty.(0) in 
-	       pretype (mk_tycon tyc) env isevars lvar f 
-	     in
-	     let fv = j_val fj in
-	     let ft = fj.uj_type in
-	     check_branches_message loc env isevars cj.uj_val (bty,[|ft|]);
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env st mis in
-	       mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|])
-	     in 
-	     { uj_val = v;  uj_type = rsty }
-
-	 | None -> 
-             (* get type information from type of branches *)
-	     let expbr = Cases.branch_scheme env isevars false indf in
-	     if Array.length expbr <> 1 then
-	       error_number_branches_loc loc env (evars_of !isevars) 
-		 cj (Array.length expbr);
-             let expti = expbr.(0) in
-	     let fj = pretype (mk_tycon expti) env isevars lvar f in
-	     let use_constraint () =
-               (* get type information from constraint *)
-               (* warning: if the constraint comes from an evar type, it *)
-               (* may be Type while Prop or Set would be expected *)
-	       match tycon with
-		 | Some pred ->
-		     let arsgn = make_arity_signature env true indf in
-                     let pred = lift (List.length arsgn) pred in
-  		     let pred = 
-                       it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
-			 arsgn in
-                     false, pred
-	         | None ->
-                     let sigma = evars_of !isevars in
-                     error_cant_find_case_type_loc loc env sigma cj.uj_val
-	     in
-             let ok, p =
-	       try
-		 let pred = 
-		   Cases.pred_case_ml 
-		     env (evars_of !isevars) false indt (0,fj.uj_type) 
-		 in 
-		 if is_ground_term !isevars pred then
-		   true, pred
-		 else
-		   use_constraint ()
-	       with Cases.NotInferable _ ->
-		 use_constraint ()
-	     in 
-	     let p = nf_evar (evars_of !isevars) p in
-	     let (bty,rsty) =
-	       Indrec.type_rec_branches
-		 false env (evars_of !isevars) indt p cj.uj_val 
-	     in
-	     let _ = option_app (e_cumul env isevars rsty) tycon in
-	     let fj = 
-	       if ok then fj 
-	       else pretype (mk_tycon bty.(0)) env isevars lvar f 
-	     in
-	     let fv = fj.uj_val in
-	     let v =
-	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env st mis in
-	       mkCase (ci, (nf_betaiota p), cj.uj_val,[|fv|] ) 
-	     in
-	     { uj_val = v; uj_type = rsty } in
-
-      (* Build the LetTuple form for v8 *)
-      let c =
-        let (ind,params) = dest_ind_family indf in
-        let rtntypopt, indnalopt = match po with
-          | None -> None, (Anonymous,None)
-          | Some p ->
-              let pj = pretype empty_tycon env isevars lvar p in
-              let dep = is_dependent_elimination env pj.uj_type indf in
-              let rec decomp_lam_force n avoid l p =
-                (* avoid is not exhaustive ! *)
-                if n = 0 then (List.rev l,p,avoid) else
-                  match p with
-                    | RLambda (_,(Name id as na),_,c) -> 
-                        decomp_lam_force (n-1) (id::avoid) (na::l) c
-                    | RLambda (_,(Anonymous as na),_,c) ->
-                        decomp_lam_force (n-1) avoid (na::l) c
-                    | _ ->
-                        let x = Nameops.next_ident_away (id_of_string "x") avoid in
-                        decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-                          (* eta-expansion *)
-                          (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in
-              let (nal,p,avoid) = 
-                decomp_lam_force (List.length realargs) [] [] p in
-              let na,rtntyp,_ = 
-                if dep then decomp_lam_force 1 avoid [] p
-                else [Anonymous],p,[] in
-              let intyp =
-                if List.for_all
-                  (function
-                    | Anonymous -> true
-                    | Name id -> not (occur_rawconstr id rtntyp)) nal
-                then (* No dependency in realargs *)
-                  None
-                else
-                  let args = List.map (fun _ -> Anonymous) params @ nal in
-                  Some (dummy_loc,ind,args) in
-              (Some rtntyp,(List.hd na,intyp)) in
-        let cs = (get_constructors env indf).(0) in
-        match indnalopt with
-          | (na,None) -> (* Represented as a let *)
-              let rec decomp_lam_force n avoid l p =
-                if n = 0 then (List.rev l,p) else
-                  match p with
-                    | RLambda (_,(Name id as na),_,c) -> 
-                        decomp_lam_force (n-1) (id::avoid) (na::l) c
-                    | RLambda (_,(Anonymous as na),_,c) -> 
-                        decomp_lam_force (n-1) avoid (na::l) c
-                    | _ ->
-                        let x = Nameops.next_ident_away (id_of_string "x") avoid in
-                        decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-                          (* eta-expansion *)
-                          (let a = RVar (dummy_loc,x) in
-                          match p with
-                            | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                            | _ -> (RApp (dummy_loc,p,[a]))) in
-              let (nal,d) = decomp_lam_force cs.cs_nargs [] [] f in
-              RLetTuple (loc,nal,(na,rtntypopt),c,d)
-          | _ -> (* Represented as a match *)
-            let detype_eqn constr construct_nargs branch =
-              let name_cons = function 
-                | Anonymous -> fun l -> l
-                | Name id -> fun l -> id::l in
-              let make_pat na avoid b ids =
-                PatVar (dummy_loc,na),
-                name_cons na avoid,name_cons na ids
-              in
-              let rec buildrec ids patlist avoid n b =
-                if n=0 then
-                  (dummy_loc, ids, 
-                  [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
-                  b)
-                else
-                  match b with
-	            | RLambda (_,x,_,b) -> 
-	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
-                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
-                          
-	            | RLetIn (_,x,_,b) -> 
-	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
-                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
-                          
-	            | RCast (_,c,_,_) ->    (* Oui, il y a parfois des cast *)
-	                buildrec ids patlist avoid n c
-                        
-	            | _ -> (* eta-expansion *)
-                        (* nommage de la nouvelle variable *)
-                        let id = Nameops.next_ident_away (id_of_string "x") avoid in
-	                let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in
-                        let pat,new_avoid,new_ids =
-	                  make_pat (Name id) avoid new_b ids in
-	                buildrec new_ids (pat::patlist) new_avoid (n-1) new_b
-	                  
-              in 
-              buildrec [] [] [] construct_nargs branch in
-            let eqn = detype_eqn (ind,1) cs.cs_nargs f in
-            RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],[eqn])
-      in
-      xx := Some c;
-      (* End building the v8 syntax *)
-      j
-
   | RIf (loc,c,(na,po),b1,b2) ->
       let cj = pretype empty_tycon env isevars lvar c in
       let (IndType (indf,realargs)) = 
@@ -707,200 +512,6 @@ let rec pretype tycon env isevars lvar = function
       in
       { uj_val = v; uj_type = p }
 
-  | ROrderedCase (loc,st,po,c,lf,x) ->
-      let isrec = (st = MatchStyle) in
-      let cj = pretype empty_tycon env isevars lvar c in
-      let (IndType (indf,realargs) as indt) = 
-	try find_rectype env (evars_of !isevars) cj.uj_type
-	with Not_found ->
-	  let cloc = loc_of_rawconstr c in
-	  error_case_not_inductive_loc cloc env (evars_of !isevars) cj in
-      let (dep,pj) = match po with
-	| Some p ->
-            let pj = pretype empty_tycon env isevars lvar p in
-            let dep = is_dependent_elimination env pj.uj_type indf in
-            let ar =
-              arity_of_case_predicate env indf dep (Type (new_univ())) in
-            let _ = e_cumul env isevars pj.uj_type ar in
-            (dep, pj)
-	| None -> 
-            (* get type information from type of branches *)
-	    let expbr = Cases.branch_scheme env isevars isrec indf in
-	    let rec findtype i =
-	      if i >= Array.length lf
-	      then
-                (* get type information from constraint *)
-                (* warning: if the constraint comes from an evar type, it *)
-                (* may be Type while Prop or Set would be expected *)
-	        match tycon with
-		  | Some pred ->
-		      let arsgn = make_arity_signature env true indf in
-                      let pred = lift (List.length arsgn) pred in
-  		      let pred = 
-			it_mkLambda_or_LetIn (nf_evar (evars_of !isevars) pred)
-			  arsgn in
-                      (true, 
-                       Retyping.get_judgment_of env (evars_of !isevars) pred)
-	          | None ->
-                      let sigma = evars_of !isevars in
-                      error_cant_find_case_type_loc loc env sigma cj.uj_val
-	      else
-		try
-		  let expti = expbr.(i) in
-		  let fj =
-		    pretype (mk_tycon expti) env isevars lvar lf.(i) in
-		  let pred = 
-		    Cases.pred_case_ml (* eta-expanse *)
-                      env (evars_of !isevars) isrec indt (i,fj.uj_type) in
-		  if not (is_ground_term !isevars pred) then findtype (i+1)
-		  else 
-		    let pty =
-                      Retyping.get_type_of env (evars_of !isevars) pred in
-		    let pj = { uj_val = pred; uj_type = pty } in
-(*
-                    let _ = option_app (the_conv_x_leq env isevars pred) tycon
-                    in
-*)
-                    (true,pj)
-		with Cases.NotInferable _ -> findtype (i+1) in
-	    findtype 0 
-      in
-      let pj = j_nf_evar (evars_of !isevars) pj in
-      let pj = if dep then pj else make_dep_of_undep env indt pj in
-      let (bty,rsty) =
-	Indrec.type_rec_branches
-          isrec env (evars_of !isevars) indt pj.uj_val cj.uj_val in
-      let _ = option_app (e_cumul env isevars rsty) tycon in
-      if Array.length bty <> Array.length lf then
-	error_number_branches_loc loc env (evars_of !isevars) 
-	  cj (Array.length bty)
-      else
-	let lfj =
-	  array_map2
-            (fun tyc f -> pretype (mk_tycon tyc) env isevars lvar f) bty
-            lf in
-	let lfv = Array.map j_val lfj in
-	let lft = Array.map (fun j -> j.uj_type) lfj in
-	check_branches_message loc env isevars cj.uj_val (bty,lft);
-	let v =
-	  if isrec
-	  then 
-	    transform_rec loc env (evars_of !isevars)(pj,cj.uj_val,lfv) indt
-	  else
-	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info env st mis in
-	    mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,
-                       Array.map (fun j-> j.uj_val) lfj)
-	in
-        (* Build the Cases form for v8 *)
-        let c =
-          let (ind,params) = dest_ind_family indf in
-          let (mib,mip) = lookup_mind_specif env ind in
-          let recargs = mip.mind_recargs in
-          let tyi = snd ind in
-          if isrec && mis_is_recursive_subset [tyi] recargs then
-            Some (Detyping.detype (false,env)
-	      (ids_of_context env) (names_of_rel_context env)
-              (nf_evar (evars_of !isevars) v))
-	  else
-	    (* Translate into a "match ... with" *)
-            let rtntypopt, indnalopt = match po with
-              | None -> None, (Anonymous,None)
-              | Some p ->
-                  let rec decomp_lam_force n avoid l p =
-                    (* avoid is not exhaustive ! *)
-                    if n = 0 then (List.rev l,p,avoid) else
-                      match p with
-                        | RLambda (_,(Name id as na),_,c) -> 
-                            decomp_lam_force (n-1) (id::avoid) (na::l) c
-                        | RLambda (_,(Anonymous as na),_,c) ->
-                            decomp_lam_force (n-1) avoid (na::l) c
-                        | _ ->
-                            let x = Nameops.next_ident_away (id_of_string "x") avoid in
-                            decomp_lam_force (n-1) (x::avoid) (Name x :: l) 
-                              (* eta-expansion *)
-                              (RApp (dummy_loc,p, [RVar (dummy_loc,x)])) in
-                  let (nal,p,avoid) = 
-                    decomp_lam_force (List.length realargs) [] [] p in
-                  let na,rtntyopt,_ = 
-                    if dep then decomp_lam_force 1 avoid [] p
-                    else [Anonymous],p,[] in
-		  let intyp =
-		    if nal=[] then None else
-                      let args = List.map (fun _ -> Anonymous) params @ nal in
-		      Some (dummy_loc,ind,args) in
-                  (Some rtntyopt,(List.hd na,intyp)) in
-	    let rawbranches =
-	      array_map3 (fun bj b cstr ->
-		let rec strip n r = if n=0 then r else
-		  match r with
-		    | RLambda (_,_,_,t) -> strip (n-1) t
-		    | RLetIn (_,_,_,t) -> strip (n-1) t
-		    | _ -> assert false in
-		let n = rel_context_length cstr.cs_args in
-		try
-		  let _,ccl = decompose_lam_n_assum n bj.uj_val in
-		  if noccur_between 1 n ccl then Some (strip n b) else None
-		with _ -> (* Not eta-expanded or not reduced *) None)
-		lfj lf (get_constructors env indf) in
-	    if st = IfStyle & snd indnalopt = None 
-	       & rawbranches.(0) <> None && rawbranches.(1) <> None then
-	      (* Translate into a "if ... then ... else" *)
-	      (* TODO: translate into a "if" even if po is dependent *)
-	      Some (RIf (loc,c,(fst indnalopt,rtntypopt),
-	          out_some rawbranches.(0),out_some rawbranches.(1)))
-	    else
-            let detype_eqn constr construct_nargs branch =
-              let name_cons = function 
-                | Anonymous -> fun l -> l
-                | Name id -> fun l -> id::l in
-              let make_pat na avoid b ids =
-                PatVar (dummy_loc,na),
-                name_cons na avoid,name_cons na ids
-              in
-              let rec buildrec ids patlist avoid n b =
-                if n=0 then
-                  (dummy_loc, ids, 
-                  [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
-                  b)
-                else
-                  match b with
-	            | RLambda (_,x,_,b) -> 
-	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
-                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
-                          
-	            | RLetIn (_,x,_,b) -> 
-	                let pat,new_avoid,new_ids = make_pat x avoid b ids in
-                        buildrec new_ids (pat::patlist) new_avoid (n-1) b
-                          
-	            | RCast (_,c,_,_) ->    (* Oui, il y a parfois des cast *)
-	                buildrec ids patlist avoid n c
-                        
-	            | _ -> (* eta-expansion *)
-                        (* nommage de la nouvelle variable *)
-                        let id = Nameops.next_ident_away (id_of_string "x") avoid in
-	                let new_b = RApp (dummy_loc, b, [RVar(dummy_loc,id)])in
-                        let pat,new_avoid,new_ids =
-	                  make_pat (Name id) avoid new_b ids in
-	                buildrec new_ids (pat::patlist) new_avoid (n-1) new_b
-	                  
-              in 
-              buildrec [] [] [] construct_nargs branch in
-            let (mib,mip) = Inductive.lookup_mind_specif (Global.env()) ind in
-            let get_consnarg j = 
-              let typi = mis_nf_constructor_type (ind,mib,mip) (j+1) in
-              let _,t = decompose_prod_n_assum mib.mind_nparams typi in
-              List.rev (fst (decompose_prod_assum t)) in
-            let consnargs = Array.init (Array.length mip.mind_consnames) get_consnarg in
-            let consnargsl = Array.map List.length consnargs in
-            let constructs = Array.init (Array.length lf) (fun i -> (ind,i+1)) in
-            let eqns = array_map3 detype_eqn constructs consnargsl lf in
-            Some (RCases (loc,(po,ref rtntypopt),[c,ref indnalopt],Array.to_list eqns)) in
-        x := c;
-        (* End build the Cases form for v8 *)
-	{ uj_val = v;
-	  uj_type = rsty }
-
   | RCases (loc,po,tml,eqns) ->
       Cases.compile_cases loc
 	((fun vtyc env -> pretype vtyc env isevars lvar),isevars)