Intégration initiale du Cases

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

6 files changed, 58 insertions, 26 deletions

diff --git a/parsing/ast.ml b/parsing/ast.ml
index f0fed61983..e7c6cb23c7 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -322,6 +322,15 @@ let rec occur_var_ast s = function
   | Id _ | Str _ | Num _ | Path _ -> false
   | Dynamic _ -> (* Hum... what to do here *) false
 
+let rec replace_var_ast s1 s2 = function
+  | Node(loc,op,args) -> Node (loc,op, List.map (replace_var_ast s1 s2) args)
+  | Nvar(loc,s) as a -> if s = s1 then Nvar (loc,s2) else a
+  | Slam(loc,None,body) -> Slam(loc,None,replace_var_ast s1 s2 body)
+  | Slam(loc,Some s,body) as a -> if s=s1 then a else
+      Slam(loc,Some s,replace_var_ast s1 s2 body)
+  | Id _ | Str _ | Num _ | Path _ as a -> a
+  | Dynamic _ as a -> (* Hum... what to do here *) a
+
 exception No_match of string
 
 let no_match_loc (loc,s) = Stdpp.raise_with_loc loc (No_match s)
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 4dacd24536..f40bc78b97 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -90,6 +90,7 @@ val alpha_eq : Coqast.t * Coqast.t -> bool
 val alpha_eq_val : v * v -> bool
 
 val occur_var_ast : string -> Coqast.t -> bool
+val replace_var_ast : string -> string -> Coqast.t -> Coqast.t
 
 val bind_env : env -> string -> v -> env
 val ast_match : env -> pat -> Coqast.t -> env
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 1e7b897ad7..68cd5482d9 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -156,24 +156,38 @@ let destruct_binder = function
   | Node(_,"BINDER",c::idl) ->
       List.map (fun id -> (id_of_string (nvar_of_ast id),c)) idl
   | _ -> anomaly "BINDER is expected"
-	
-let rec dbize_pattern env = function
+
+let merge_aliases p = function
+  | a, Anonymous    -> a, p
+  | Anonymous, a    -> a, p
+  | Name id1, (Name id2 as na) ->
+      let s1 = string_of_id id1 in
+      let s2 = string_of_id id2 in
+      warning ("Alias variable "^s1^" is merged with "^s2);
+      na, replace_var_ast s1 s2 p
+
+let rec dbize_pattern env aliasopt = function
   | Node(_,"PATTAS",[Nvar (loc,s); p]) ->
-      (match name_of_nvar s with
-	 | Anonymous -> dbize_pattern env p
-	 | Name id   -> 
-	     let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p')))
+      let aliasopt',p' = merge_aliases p (aliasopt,name_of_nvar s) in
+      dbize_pattern env aliasopt' p'
+  | Nvar(loc,s) ->
+      (match maybe_constructor env s with
+	 | Some c ->
+	     let ids = match aliasopt with Anonymous -> [] | Name id -> [id] in
+	     (ids,PatCstr (loc,c,[],aliasopt))
+	 | None ->
+	     (match name_of_nvar s with
+		| Anonymous -> ([], PatVar (loc,Anonymous))
+		| Name id as name -> ([id], PatVar (loc,name))))
   | Node(_,"PATTCONSTRUCT", Nvar(loc,s)::((_::_) as pl)) ->
       (match maybe_constructor env s with
 	 | Some c ->
-	     let (idsl,pl') = List.split (List.map (dbize_pattern env) pl) in
-	     (List.flatten idsl,PatCstr (loc,c,pl'))
+	     let ids = match aliasopt with Anonymous -> [] | Name id -> [id] in
+	     let (idsl,pl') = 
+	       List.split (List.map (dbize_pattern env Anonymous) pl) in
+	     (List.flatten (ids::idsl),PatCstr (loc,c,pl',aliasopt))
 	 | None ->
 	     user_err_loc (loc,"dbize_pattern",mssg_hd_is_not_constructor s))
-  | Nvar(loc,s) ->
-      (match name_of_nvar s with
-	 | Anonymous -> ([], PatVar (loc,Anonymous))
-	 | Name id as name -> ([id], PatVar (loc,name)))
   | _ -> anomaly "dbize: badly-formed ast for Cases pattern"
 
 let rec dbize_fix = function
@@ -309,7 +323,8 @@ let dbize k sigma =
 
   and dbize_eqn n env = function
     | Node(loc,"EQN",rhs::lhs) ->
-	let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in
+	let (idsl,pl) =
+	  List.split (List.map (dbize_pattern env Anonymous) lhs) in
 	let ids = List.flatten idsl in
 	(* Linearity implies the order in ids is irrelevant *)
 	check_linearity loc ids;
diff --git a/parsing/g_cases.ml4 b/parsing/g_cases.ml4
index 0b45dd3e47..a6dcbffe71 100644
--- a/parsing/g_cases.ml4
+++ b/parsing/g_cases.ml4
@@ -9,10 +9,12 @@ GEXTEND Gram
     [ [  -> []
       | p = pattern; pl = pattern_list -> p :: pl ] ]
   ;
+(*
   lsimple_pattern:
     [ [ c = simple_pattern2 -> c ] ]
   ;
-  simple_pattern:
+*)
+  pattern:
     [ [ id = ident -> id
       | "("; p = lsimple_pattern; ")" -> p ] ]
   ;
@@ -21,18 +23,19 @@ GEXTEND Gram
       | p = simple_pattern; pl = simple_pattern_list ->
 	   p :: pl ] ]
   ;
-  (* The XTRA"!" means we want to override the implicit arg mecanism of bdize,
-     since params are not given in patterns *)
-  simple_pattern2:
-    [ [ p = simple_pattern; lp = pattern_list ->
-          <:ast< (PATTCONSTRUCT $p ($LIST $lp)) >>
-      | p = simple_pattern; "as"; id = ident -> <:ast< (PATTAS $id $p) >>
+  lsimple_pattern:
+    [ [ id = ident; lp = ne_pattern_list ->
+	  <:ast< (PATTCONSTRUCT $id ($LIST $lp)) >>
+      | p = pattern; "as"; id = ident -> <:ast< (PATTAS $id $p)>>
       | c1 = simple_pattern; ","; c2 = simple_pattern ->
-          <:ast< (PATTCONSTRUCT pair $c1 $c2) >> ] ]
+          <:ast< (PATTCONSTRUCT pair $c1 $c2) >>
+      | "("; p = lsimple_pattern; ")" -> p ] ]
   ;
+(*
   pattern:
     [ [ p = simple_pattern -> p ] ]
   ;
+*)
   ne_pattern_list:
     [ [ c1 = pattern; cl = ne_pattern_list -> c1 :: cl
       | c1 = pattern -> [c1] ] ]
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 848a2132ec..e0277761d0 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -452,8 +452,8 @@ let print_opaque_name name =
 	    anomaly "print_opaque_name"
       | DOPN(MutInd (sp,_),_) as x ->
           print_mutual sp (Global.lookup_mind sp)
-      | DOPN(MutConstruct _,_) as x -> 
-	  let ty = Typeops.type_of_constructor env sigma x in
+      | DOPN(MutConstruct cstr_sp,a) as x -> 
+	  let ty = Typeops.type_of_constructor env sigma (cstr_sp,a) in
 	  print_typed_value(x, ty)
       | VAR id ->
           let a = snd(lookup_sign id sign) in 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index bbc9e368cc..cfe85f7fda 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -68,10 +68,14 @@ let ast_of_ref = function
 let rec ast_of_pattern = function   (* loc is thrown away for printing *)
   | PatVar (loc,Name id) -> nvar (string_of_id id)
   | PatVar (loc,Anonymous) -> nvar "_"
-  | PatCstr(loc,cstr,args) ->
+  | PatCstr(loc,cstr,args,Name id) ->
+      ope("PATTAS",
+	  [nvar (string_of_id id);
+	   ope("PATTCONSTRUCT",
+	       (ast_of_constructor cstr)::List.map ast_of_pattern args)])
+  | PatCstr(loc,cstr,args,Anonymous) ->
       ope("PATTCONSTRUCT",
 	  (ast_of_constructor cstr)::List.map ast_of_pattern args)
-  | PatAs(loc,id,p) -> ope("PATTAS",[nvar (string_of_id id); ast_of_pattern p])
 	
 (* Nouvelle version de renommage des variables (DEC 98) *)
 (* This is the algorithm to display distinct bound variables 
@@ -800,7 +804,7 @@ and detype_eqn avoid env constr_id construct_params branch =
 	buildrec new_ids (pat::patlist) new_avoid new_env (l,new_b)
 	  
     | []  , rhs	-> 
-	(ids, [PatCstr(dummy_loc, constr_id, List.rev patlist)],
+	(ids, [PatCstr(dummy_loc, constr_id, List.rev patlist,Anonymous)],
 	 detype avoid env rhs)
   in 
   buildrec [] [] avoid env (construct_params,branch)