Suppression de Abst

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

5 files changed, 9 insertions, 399 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 5415d819cf..72b7e1cf55 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -153,8 +153,6 @@ let dbize_global loc = function
       RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt))
   | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) ->
       RRef (loc,RConstruct (((dbize_sp sp,ti),n),dbize_ctxt ctxt))
-  (* | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp) *)
-  (* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *)
   | _ -> anomaly_loc (loc,"dbize_global",
 		      [< 'sTR "Bad ast for this global a reference">])
 
@@ -595,7 +593,6 @@ let rec pat_of_ref metas vars = function
   | RInd (ip,ctxt) -> RInd (ip, dbize_rawconstr_ctxt ctxt)
   | RConstruct(cp,ctxt) ->RConstruct(cp, dbize_rawconstr_ctxt ctxt)
   | REVar (n,ctxt) -> REVar (n, dbize_rawconstr_ctxt ctxt)
-  | RAbst _ -> error "pattern_of_rawconstr: not implemented"
   | RVar _ -> assert false (* Capturé dans pattern_of_raw *)
 
 and pat_of_raw metas vars lvar = function
diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 2a7f5ac8e6..fac13a4e08 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -86,7 +86,6 @@ GEXTEND Gram
                    ($SLAM $b $c1))) >>
       | IDENT "let"; id1 = IDENT ; "="; c = constr; "in"; c1 = constr -> 
 	  <:ast< (LETIN $c [$id1]$c1) >>
-(* <:ast< (ABST #Core#let.cci $c [$id1]$c1) >>*)
       | IDENT "if"; c1 = constr; IDENT "then"; c2 = constr;
         IDENT "else"; c3 = constr ->
         <:ast< ( CASE "NOREC" "SYNTH" $c1 $c2 $c3) >>
diff --git a/parsing/g_minicoq.ml4 b/parsing/g_minicoq.ml4
index 21163804ec..f3aaa4e2a7 100644
--- a/parsing/g_minicoq.ml4
+++ b/parsing/g_minicoq.ml4
@@ -5,7 +5,7 @@ open Pp
 open Util
 open Names
 open Univ
-open Generic
+(*i open Generic i*)
 open Term
 open Environ
 
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index ff747d4e35..17a4535a4d 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -53,7 +53,6 @@ let label_of_ref = function
   | 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 =
@@ -265,12 +264,12 @@ let rec sub_match nocc pat c =
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure ->
       let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
-      (lm,mkMutCase (ci,hd,List.hd le,List.tl le))
+      (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,mkMutCase (ci,hd,List.hd le,List.tl le)))
+      (lm,mkMutCaseL (ci,hd,List.hd le,List.tl le)))
   | IsMutConstruct _ | IsFix _ | IsMutInd _|IsCoFix _ |IsEvar _|IsConst _
-  | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _|IsAbst (_, _) ->
+  | IsRel _|IsMeta _|IsVar _|IsXtra _|IsSort _ ->
     (try authorized_occ nocc ((matches pat c),DOP0 (Meta (-1))) with
     | PatternMatchingFailure -> raise (NextOccurrence nocc)
     | NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
@@ -327,4 +326,4 @@ let rec pattern_of_constr t =
 	       Array.map pattern_of_constr br)
     | IsFix _ | IsCoFix _ ->
 	error "pattern_of_constr: (co)fix currently not supported"
-    | IsAbst _ | IsXtra _   -> anomaly "No longer supported"
+    | IsXtra _   -> anomaly "No longer supported"
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 98aed4f567..0d04bd2b21 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -110,9 +110,6 @@ let ast_of_inductive_ref pr  ((sp,tyi) as ind_sp,ids) =
 
 let ast_of_ref pr = function
   | RConst (sp,ctxt) -> ast_of_constant_ref pr (sp,ctxt)
-  | RAbst (sp) ->
-      ope("ABST", (path_section dummy_loc sp)
-	    ::(List.map ast_of_ident (* on triche *) []))
   | RInd (ind,ctxt) -> ast_of_inductive_ref pr (ind,ctxt)
   | RConstruct (cstr,ctxt) -> ast_of_constructor_ref pr (cstr,ctxt)
   | RVar id -> ast_of_ident id
@@ -310,399 +307,17 @@ and factorize_binder n oper na aty c =
 
 let ast_of_rawconstr = ast_of_raw
 
-(*****************************************************************)
-(* TO EJECT ... REPRIS DANS detyping *)
-
-
-(* Nouvelle version de renommage des variables (DEC 98) *)
-(* This is the algorithm to display distinct bound variables 
-
-    - Règle 1 : un nom non anonyme, même non affiché, contribue à la liste
-      des noms à éviter 
-    - Règle 2 : c'est la dépendance qui décide si on affiche ou pas
-
-    Exemple : 
-    si bool_ind = (P:bool->Prop)(f:(P true))(f:(P false))(b:bool)(P b), alors
-    il est affiché (P:bool->Prop)(P true)->(P false)->(b:bool)(P b)
-    mais f et f0 contribue à la liste des variables à éviter (en supposant 
-    que les noms f et f0 ne sont pas déjà pris)
-    Intérêt : noms homogènes dans un but avant et après Intro
-*)
-
-type used_idents = identifier list
-
-(* This avoids var names, const/ind/construct names but also names of
-   de Bruijn variables bound in env *)
-
-let occur_id env id0 c =
-  let rec occur n = function
-    | VAR id             -> id=id0
-    | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
-    | DOPN (Abst sp,cl)  -> (basename sp = id0) or (array_exists (occur n) cl)
-    | DOPN (MutInd ind_sp, cl) as t -> 
-  	(basename (path_of_inductive_path ind_sp) = id0)
-	or (array_exists (occur n) cl)
-    | DOPN (MutConstruct cstr_sp, cl) as t -> 
-    	(basename (path_of_constructor_path cstr_sp) = id0)
-	or (array_exists (occur n) cl)
-    | DOPN(_,cl)         -> array_exists (occur n) cl
-    | DOP1(_,c)          -> occur n c
-    | DOP2(_,c1,c2)      -> (occur n c1) or (occur n c2)
-    | DLAM(_,c)          -> occur (n+1) c
-    | DLAMV(_,v)         -> array_exists (occur (n+1)) v
-    | CLam (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
-    | CPrd (_,t,c)   -> occur n (body_of_type t) or occur (n+1) c
-    | CLet (_,b,t,c) -> occur n b or occur n (body_of_type t) or occur (n+1) c
-    | Rel p              ->
-    	p>n &
-    	(try lookup_name_of_rel (p-n) env = Name id0
-	 with Not_found -> false) (* Unbound indice : may happen in debug *)
-    | DOP0 _             -> false
-  in 
-  occur 1 c
-
-let next_name_not_occuring name l env t =
-  let rec next id =
-    if List.mem id l or occur_id env id t then next (lift_ident id) else id
-  in 
-  match name with
-    | Name id   -> next id
-    | Anonymous -> id_of_string "_"
-
-(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let concrete_name islam l env n c =
-  if n = Anonymous & not (dependent (mkRel 1) c) then
-    (None,l)
-  else
-    let fresh_id = next_name_not_occuring n l env c in
-    let idopt =
-      if islam or dependent (mkRel 1) c then (Some fresh_id) else None in
-    (idopt, fresh_id::l)
-
-    (* Returns the list of global variables and constants in a term *)
-let global_vars_and_consts t =
-  let rec collect acc c =
-    let op, cl = splay_constr c in
-    let acc' = Array.fold_left collect acc cl in
-    match op with
-    | OpVar id -> id::acc'
-    | OpConst sp -> (basename sp)::acc'
-    | OpAbst sp  -> (basename sp)::acc'
-    | OpMutInd ind_sp -> (basename (path_of_inductive_path ind_sp))::acc'
-    | OpMutConstruct csp -> (basename (path_of_constructor_path csp))::acc'
-    | _ -> acc'
-  in
-  list_uniquize (collect [] t)
-    
-let used_of = global_vars_and_consts
-
-(****************************************************************************)
-(* Tools for printing of Cases                                              *)
-(* These functions implement a light form of Termenv.mind_specif_of_mind    *)
-(* specially for handle Cases printing; they respect arities but not typing *)
-
-let bdize_app c al =
-  let impl =
-    match c with
-      | DOPN(MutConstruct constr_sp,_) -> constructor_implicits_list constr_sp
-      | DOPN(MutInd ind_sp,_) -> inductive_implicits_list ind_sp
-      | DOPN(Const sp,_) -> constant_implicits_list sp
-      | VAR id -> (try implicits_of_var id with _ -> []) (* et FW? *)
-      | _ -> []
-  in
-  if !print_implicits then 
-    ope("APPLISTEXPL", al)
-  else
-    ope("APPLIST", explicitize impl al)
-
-(* Auxiliary function for MutCase printing *)
-(* [computable] tries to tell if the predicate typing the result is inferable*)
-
-let computable p k =
-    (* We first remove as many lambda as the arity, then we look
-       if it remains a lambda for a dependent elimination. This function
-       works for normal eta-expanded term. For non eta-expanded or
-       non-normal terms, it may affirm the pred is synthetisable
-       because of an undetected ultimate dependent variable in the second
-       clause, or else, it may affirms the pred non synthetisable
-       because of a non normal term in the fourth clause.
-       A solution could be to store, in the MutCase, the eta-expanded
-       normal form of pred to decide if it depends on its variables
-
-       Lorsque le prédicat est dépendant de manière certaine, on
-       ne déclare pas le prédicat synthétisable (même si la
-       variable dépendante ne l'est pas effectivement) parce que
-       sinon on perd la réciprocité de la synthèse (qui, lui,
-       engendrera un prédicat non dépendant) *)
-
-  let rec striprec n c = match n,kind_of_term c with
-    | (0,IsLambda (_,_,d)) -> false
-    | (0,_)                -> noccur_between 1 k c
-    | (n,IsLambda (_,_,d)) -> striprec (n-1) d
-    |  _                   -> false
-  in 
-  striprec k p
-
-let ids_of_var cl =
-  List.map
-    (function 
-       | RRef (_,RVar id) -> id
-       | _-> anomaly "ids_of_var")
-    (Array.to_list cl)
-
-(* Main translation function from constr -> ast *)
-
-let old_bdize at_top env t =
-  let init_avoid = if at_top then ids_of_context env else [] in
-  let rec bdrec avoid env t = match collapse_appl t with
-    (* Not well-formed constructions *)
-    | DLAM(na,c) ->
-	(match concrete_name true (*On ne sait pas si prod*)avoid env na c with
-           | (Some id,avoid') -> 
-	       slam(Some (string_of_id id),
-                    bdrec avoid' (add_name (Name id) env) c)
-           | (None,avoid') -> 
-	       slam(None,bdrec avoid' env (pop c)))
-    | DLAMV(na,cl) ->
-	if not(array_exists (dependent (mkRel 1)) cl) then
-	  slam(None,ope("V$",array_map_to_list
-			  (fun c -> bdrec avoid env (pop c)) cl))
-	else
-	  let id = next_name_away na avoid in 
-	  slam(Some (string_of_id id),
-	       ope("V$", array_map_to_list
-		     (bdrec (id::avoid) (add_name (Name id) env)) cl))
-	    
-    (* Well-formed constructions *)
-    | regular_constr -> 
-	(match kind_of_term regular_constr with
-	   | IsRel n ->
-	       (try 
-		  match lookup_name_of_rel n env with
-		    | Name id   -> nvar (string_of_id id)
-		    | Anonymous -> raise Not_found
-		with Not_found -> 
-		  ope("REL",[num n]))
-	     (* TODO: Change this to subtract the current depth *)
-	   | IsMeta n -> ope("META",[num n])
-	   | IsVar id -> nvar (string_of_id id)
-	   | IsXtra s -> ope("XTRA",[str s])
-	   | IsSort s ->
-	       (match s with
-		  | Prop Null -> ope("PROP",[])
-		  | Prop Pos -> ope("SET",[])
-		  | Type u -> 
-		      ope("TYPE",
-			  [path_section dummy_loc u.u_sp; num u.u_num]))
-	   | IsCast (c1,c2) ->
-	       if !print_casts then 
-		 bdrec avoid env c1 
-	       else 
-		 ope("CAST",[bdrec avoid env c1;bdrec avoid env c2])
-	   | IsLetIn (na,b,_,c) ->
-	       ope("LETIN",[bdrec [] env b;
-			   slam(stringopt_of_name na,bdrec avoid env (pop c))])
-	   | IsProd (Anonymous,ty,c) ->
-                    (* Anonymous product are never factorized *)
-	       ope("PROD",[bdrec [] env ty;
-			   slam(None,bdrec avoid env (pop c))])
-	   | IsProd (Name _ as na,ty,c) ->
-	       let (n,a) = factorize_binder 1 avoid env Prod na ty c in
-               (* PROD et PRODLIST doivent être distingués à cause du cas
-                  non dépendant, pour isoler l'implication; peut-être 
-	          un constructeur ARROW serait-il plus justifié ? *)
-	       let oper = if n=1 then "PROD" else "PRODLIST" in
-	       ope(oper,[bdrec [] env ty;a])
-	   | IsLambda (na,ty,c) ->
-	       let (n,a) = factorize_binder 1 avoid env Lambda na ty c in
-               (* LAMBDA et LAMBDALIST se comportent pareil *)
-	       let oper = if n=1 then "LAMBDA" else "LAMBDALIST" in
-	       ope(oper,[bdrec [] env ty;a])
-	   | IsAppL (f,args) ->
-	       bdize_app f (List.map (bdrec avoid env) (f::args))
-	   | IsConst (sp,cl) ->
-	       ope("CONST",((path_section dummy_loc sp)::
-			    (array_map_to_list (bdrec avoid env) cl)))
-	   | IsEvar (ev,cl) ->
-	       ope("EVAR",((num ev)::
-			   (array_map_to_list (bdrec avoid env) cl)))
-	   | IsAbst (sp,cl) ->
-	       ope("ABST",((path_section dummy_loc sp)::
-			   (array_map_to_list (bdrec avoid env) cl)))
-	   | IsMutInd ((sp,tyi),cl) ->
-	       ope("MUTIND",((path_section dummy_loc sp)::(num tyi)::
-			     (array_map_to_list (bdrec avoid env) cl)))
-	   | IsMutConstruct (((sp,tyi),n),cl) ->
-	       ope("MUTCONSTRUCT",
-		   ((path_section dummy_loc sp)::(num tyi)::(num n)::
-		    (array_map_to_list (bdrec avoid env) cl)))
-	   | IsMutCase (annot,p,c,bl) ->
-	       let synth_type = Detyping.synthetize_type () in
-	       let tomatch = bdrec avoid env c in
-	       begin 
-		 match annot with
-(*		 | None -> 
-	             (* Pas d'annotation --> affichage avec vieux Case *)
-		     let pred = bdrec avoid env p in
-		     let bl' = array_map_to_list (bdrec avoid env) bl in
-		     ope("MUTCASE",pred::tomatch::bl')
-		 | Some *) (consnargsl,(_,considl,k,style,tags) as ci) ->
-		     let pred = 
-		       if synth_type & computable p k & considl <> [||] then
-			 (str "SYNTH")
-		       else 
-			 bdrec avoid env p 
-		     in
-		     if Detyping.force_if ci then 
-		       ope("FORCEIF", [ pred; tomatch;
-					bdrec avoid env bl.(0); 
-					bdrec avoid env bl.(1) ])
-		     else
-		       let asttomatch = ope("TOMATCH", [tomatch]) in
-		       let eqnv =
-			 array_map3 (bdize_eqn avoid env)
-			   considl consnargsl bl in
-		       let eqnl = Array.to_list eqnv in
-		       let tag =
-			 if Detyping.force_let ci then 
-			   "FORCELET" 
-			 else 
-			   "CASES"
-		       in 
-		       ope(tag,pred::asttomatch::eqnl)
-	       end
-	       
-	   | IsFix ((nv,n),(cl,lfn,vt)) ->
-	       let lfi = List.map (fun na -> next_name_away na avoid) lfn in
-	       let def_env = 
-		 List.fold_left
-		   (fun env id -> add_name (Name id) env) env lfi in
-	       let def_avoid = lfi@avoid in
-	       let f = List.nth lfi n in
-	       let rec split_lambda binds env avoid n t =
-		 match (n,kind_of_term t) with
-		 | (0, _) -> (binds,bdrec avoid env t)
-		 | (n, IsCast (t,_)) -> split_lambda binds env avoid n t
-		 | (n, IsLambda (na,t,b)) ->
-		     let ast = bdrec avoid env t in
-		     let id = next_name_away na avoid in
-		     let ast_of_bind = 
-		       ope("BINDER",[ast;nvar (string_of_id id)]) in
-		     let new_env = add_name (Name id) env in
-		     split_lambda (ast_of_bind::binds) 
-		       new_env (id::avoid) (n-1) b
-		 | _ -> error "split_lambda" 
-	       in
-	       let rec split_product env avoid n t =
-		 match (n,kind_of_term t) with
-		 | (0, _) -> bdrec avoid env t
-		 | (n, IsCast (t,_)) -> split_product env avoid n t
-		 | (n, IsProd (na,t,b)) ->
-		     let ast = bdrec avoid env t in
-		     let id = next_name_away na avoid in
-		     let new_env = add_name (Name id) env in
-		     split_product new_env (id::avoid) (n-1) b
-		 | _ -> error "split_product" 
-	       in
-	       let listdecl = 
-		 list_map_i
-		   (fun i fi ->
-		      let (lparams,ast_of_def) =
-			split_lambda [] def_env def_avoid (nv.(i)+1) vt.(i) in
-		      let ast_of_typ = 
-			split_product env avoid (nv.(i)+1) cl.(i) in
-		      ope("FDECL",
-			  [nvar (string_of_id fi); 
-			   ope ("BINDERS",List.rev lparams);
-			   ast_of_typ; ast_of_def ]))
-		   0 lfi 
-	       in 
-	       ope("FIX", (nvar (string_of_id f))::listdecl)
-
-	   | IsCoFix (n,(cl,lfn,vt)) ->
-	       let lfi = List.map (fun na -> next_name_away na avoid) lfn in
-	       let def_env =
-		 List.fold_left 
-		   (fun env id -> add_name (Name id) env) env lfi in
-	       let def_avoid = lfi@avoid in
-	       let f = List.nth lfi n in
-	       let listdecl =
-		 list_map_i (fun i fi -> ope("CFDECL",
-					     [nvar (string_of_id fi);
-					      bdrec avoid env cl.(i);
-					      bdrec def_avoid def_env vt.(i)]))
-		   0 lfi
-	       in 
-	       ope("COFIX", (nvar (string_of_id f))::listdecl))
-
-  and bdize_eqn avoid env constructid nargs branch =
-    let print_underscore = Detyping.force_wildcard () in
-    let cnvar = nvar (string_of_id constructid) in
-    let rec buildrec nvarlist avoid env = function
-
-      | 0, b
-	-> let pattern =
-          if nvarlist = [] then cnvar
-          else ope ("PATTCONSTRUCT", cnvar::(List.rev nvarlist)) in
-	   let action = bdrec avoid env b in
-	     ope("EQN", [action; pattern])
-
-      | n, DOP2(Lambda,_,DLAM(x,b))
-	-> let x'=
-          if not print_underscore or (dependent (mkRel 1) b) then x 
-          else Anonymous in
-           let id = next_name_away x' avoid in
-           let new_env = (add_name (Name id) env) in
-           let new_avoid = id::avoid in
-           let new_nvarlist = (nvar (string_of_id id))::nvarlist in
-             buildrec new_nvarlist new_avoid new_env (n-1,b)
-	       
-      | n, DOP2(Cast,b,_)     (* Oui, il y a parfois des cast *)
-	-> buildrec nvarlist avoid env (n,b)
-	  
-      | n, b (* eta-expansion : n'arrivera plus lorsque tous les
-                   termes seront construits à partir de la syntaxe Cases *)
-	-> (* nommage de la nouvelle variable *)
-          let id = next_ident_away (id_of_string "x") avoid in
-	  let new_nvarlist = (nvar (string_of_id id))::nvarlist in
-          let new_env = (add_name (Name id) env) in
-          let new_avoid = id::avoid in
-          let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
-            buildrec new_nvarlist new_avoid new_env (n-1,new_b)
-
-    in buildrec [] avoid env (nargs,branch)
-
-  and factorize_binder n avoid env oper na ty c =
-    let (env2, avoid2,na2) =
-      match concrete_name (oper=Lambda) avoid env na c with
-	  (Some id,l') -> add_name (Name id) env, l', Some (string_of_id id) 
-	| (None,l')    -> add_name Anonymous env, l', None
-    in
-    let (p,body) = match c with
-	DOP2(oper',ty',DLAM(na',c')) 
-	  when (oper = oper')
-	    & eq_constr (lift 1 ty) ty'
-	    & not (na' = Anonymous & oper = Prod)
-	    -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
-      | _ -> (n,bdrec avoid2 env2 c)
-    in (p,slam(na2, body))
-
-  in
-    bdrec init_avoid (names_of_rel_context env) t
-(* FIN TO EJECT *)
 (******************************************************************)
+(* Main translation function from constr -> ast *)
        
 let ast_of_constr at_top env t =
   let t' =
     if !print_casts then t
     else Reduction.strong (fun _ _ -> strip_outer_cast)
       empty_env Evd.empty t in
-  try
-    let avoid = if at_top then ids_of_context env else [] in
-    ast_of_raw 
-      (Detyping.detype avoid (names_of_rel_context env) t')
-  with Detyping.StillDLAM ->
-    old_bdize at_top env t'
+  let avoid = if at_top then ids_of_context env else [] in
+  ast_of_raw 
+    (Detyping.detype avoid (names_of_rel_context env) t')
 
 let ast_of_constant env    = ast_of_constant_ref (ast_of_constr false env)