Version préliminaire d'inversion de la compilation du filtrage

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

3 files changed, 143 insertions, 58 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 40d0465741..ff494c7825 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -899,7 +899,7 @@ let rec raw_of_pat env = function
       let k = mip.Declarations.mind_nrealargs in
       let nparams = mib.Declarations.mind_nparams in
       let cstrnargs = mip.Declarations.mind_consnrealargs in
-      Detyping.detype_case false (raw_of_pat env)(raw_of_eqn env)
+      Detyping.detype_case false (raw_of_pat env) (raw_of_eqns env)
 	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
 	avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv
   | PCase _ -> error "Unsupported case-analysis while printing pattern"
@@ -907,6 +907,9 @@ let rec raw_of_pat env = function
   | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
 
+and raw_of_eqns env constructs consnargsl bl =
+  Array.to_list (array_map3 (raw_of_eqn env) constructs consnargsl bl)
+
 and raw_of_eqn env constr construct_nargs branch =
   let make_pat x env b ids =
     let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 5b26eaec5f..38675da786 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -26,6 +26,8 @@ open Nametab
 open Evd
 open Mod_subst
 
+let dl = dummy_loc
+
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
@@ -132,11 +134,21 @@ let synthetize_type () = !synth_type_value
 
 let _ = declare_bool_option 
 	  { optsync  = true;
-	    optname  = "synthesizability";
+	    optname  = "pattern matching return type synthesizability";
 	    optkey   = SecondaryTable ("Printing","Synth");
 	    optread  = synthetize_type;
 	    optwrite = (:=) synth_type_value }
 
+let reverse_matching_value = ref true
+let reverse_matching () = !reverse_matching_value
+
+let _ = declare_bool_option 
+	  { optsync  = true;
+	    optname  = "pattern-matching reversibility";
+	    optkey   = SecondaryTable ("Printing","Matching");
+	    optread  = reverse_matching;
+	    optwrite = (:=) reverse_matching_value }
+
 (* Auxiliary function for MutCase printing *)
 (* [computable] tries to tell if the predicate typing the result is inferable*)
 
@@ -195,6 +207,61 @@ let lookup_index_as_renamed env t n =
     | _ -> None
   in lookup n 1 t
 
+(**********************************************************************)
+(* Fragile algorithm to reverse pattern-matching compilation          *)
+
+let update_name na ((_,e),c) =
+  match na with
+  | Name _ when force_wildcard () & noccurn (list_index na e) c ->
+      Anonymous
+  | _ ->
+      na
+
+let rec decomp_branch n nal b (avoid,env as e) c =
+  if n=0 then (List.rev nal,(e,c))
+  else
+    let na,c,f =
+      match kind_of_term (strip_outer_cast c) with
+	| Lambda (na,_,c) -> na,c,concrete_let_name
+	| LetIn (na,_,_,c) -> na,c,concrete_name
+	| _ -> 
+	    Name (id_of_string "x"),(applist (lift 1 c, [mkRel 1])), 
+	    concrete_name in
+    let na',avoid' = f b avoid env na c in
+    decomp_branch (n-1) (na'::nal) b (avoid',add_name na' env) c
+
+let rec build_tree na isgoal e ci cl =
+  let mkpat n rhs pl = PatCstr(dl,(ci.ci_ind,n+1),pl,update_name na rhs) in
+  let cnl = ci.ci_cstr_nargs in
+  List.flatten
+    (list_tabulate (fun i -> contract_branch isgoal e (cnl.(i),mkpat i,cl.(i)))
+       (Array.length cl))
+
+and align_tree nal isgoal (e,c as rhs) = match nal with
+  | [] -> [[],rhs]
+  | na::nal ->
+    match kind_of_term c with
+    | Case (ci,_,c,cl) when c = mkRel (list_index na (snd e)) ->
+	let clauses = build_tree na isgoal e ci cl in
+	List.flatten
+          (List.map (fun (pat,rhs) ->
+	      let lines = align_tree nal isgoal rhs in
+	      List.map (fun (hd,rest) -> pat::hd,rest) lines) 
+	    clauses)
+    | _ ->
+	let pat = PatVar(dl,update_name na rhs) in
+	let mat = align_tree nal isgoal rhs in
+	List.map (fun (hd,rest) -> pat::hd,rest) mat
+
+and contract_branch isgoal e (cn,mkpat,b) =
+  let nal,rhs = decomp_branch cn [] isgoal e b in
+  let mat = align_tree nal isgoal rhs in
+  List.map (fun (hd,rhs) -> (mkpat rhs hd,rhs)) mat
+
+(**********************************************************************)
+(* Transform internal representation of pattern-matching into list of *)
+(* clauses                                                            *)
+
 let is_nondep_branch c n =
   try
     let _,ccl = decompose_lam_n_assum n c in
@@ -210,7 +277,7 @@ let extract_nondep_branches test c b n =
       | _ -> assert false in
   if test c n then Some (strip n b) else None
 
-let detype_case computable detype detype_eqn testdep avoid data p c bl =
+let detype_case computable detype detype_eqns testdep avoid data p c bl =
   let (indsp,st,nparams,consnargsl,k) = data in
   let synth_type = synthetize_type () in
   let tomatch = detype c in
@@ -230,10 +297,10 @@ let detype_case computable detype detype_eqn testdep avoid data p c bl =
                   | c -> 
                       let x = next_ident_away (id_of_string "x") avoid in
                       lamdec_rec ((Name x)::l) (x::avoid) (k-1)
-                        (let a = RVar (dummy_loc,x) in
+                        (let a = RVar (dl,x) in
                           match c with
                           | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                          | _ -> (RApp (dummy_loc,c,[a])))
+                          | _ -> (RApp (dl,c,[a])))
               in 
               lamdec_rec [] [] k c in
             let nl,typ = decompose_lam k p in
@@ -244,12 +311,11 @@ let detype_case computable detype detype_eqn testdep avoid data p c bl =
 	      if List.for_all ((=) Anonymous) nl then None
 	      else 
 		let pars = list_tabulate (fun _ -> Anonymous) nparams in
-		Some (dummy_loc,indsp,pars@nl) in
+		Some (dl,indsp,pars@nl) in
             n, aliastyp, Some typ
   in
   let constructs = Array.init (Array.length bl) (fun i -> (indsp,i+1)) in
-  let eqnv = array_map3 detype_eqn constructs consnargsl bl in
-  let eqnl = Array.to_list eqnv in
+  let eqnl = detype_eqns constructs consnargsl bl in
   let tag =
     try 
       if !Options.raw_print then
@@ -261,12 +327,10 @@ let detype_case computable detype detype_eqn testdep avoid data p c bl =
       else 
 	st
     with Not_found -> st
-  in 
-  if tag = RegularStyle then
-    RCases (dummy_loc,pred,[tomatch,(alias,aliastyp)],eqnl)
-  else
-    let bl' = Array.map detype bl in
-    if tag = LetStyle && aliastyp = None then
+  in
+  match tag with
+  | LetStyle when aliastyp = None -> 
+      let bl' = Array.map detype bl in
       let rec decomp_lam_force n avoid l p =
 	if n = 0 then (List.rev l,p) else
           match p with
@@ -278,66 +342,70 @@ let detype_case computable detype detype_eqn testdep avoid data p c bl =
 		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
+                  (let a = RVar (dl,x) in
                   match p with
                     | RApp (loc,p,l) -> RApp (loc,p,l@[a])
-                    | _ -> (RApp (dummy_loc,p,[a]))) in
+                    | _ -> (RApp (dl,p,[a]))) in
       let (nal,d) = decomp_lam_force consnargsl.(0) avoid [] bl'.(0) in
-      RLetTuple (dummy_loc,nal,(alias,pred),tomatch,d)
-    else
-    let nondepbrs =
-      array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
-    if tag = IfStyle && aliastyp = None
-      && array_for_all ((<>) None) nondepbrs then
-      RIf (dummy_loc,tomatch,(alias,pred),
-           out_some nondepbrs.(0),out_some nondepbrs.(1))
-    else 
-      RCases(dummy_loc,pred,[tomatch,(alias,aliastyp)],eqnl)
-
+      RLetTuple (dl,nal,(alias,pred),tomatch,d)
+  | IfStyle when aliastyp = None ->
+      let bl' = Array.map detype bl in
+      let nondepbrs =
+	array_map3 (extract_nondep_branches testdep) bl bl' consnargsl in
+      if array_for_all ((<>) None) nondepbrs then
+	RIf (dl,tomatch,(alias,pred),
+             out_some nondepbrs.(0),out_some nondepbrs.(1))
+      else
+	RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+  | _ ->
+      RCases (dl,pred,[tomatch,(alias,aliastyp)],eqnl)
+
+(**********************************************************************)
+(* Main detyping function                                             *)
 
 let rec detype isgoal avoid env t =
   match kind_of_term (collapse_appl t) with
     | Rel n ->
       (try match lookup_name_of_rel n env with
-	 | Name id   -> RVar (dummy_loc, id)
+	 | Name id   -> RVar (dl, id)
 	 | Anonymous -> anomaly "detype: index to an anonymous variable"
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
-	 in RVar (dummy_loc, id_of_string s))
+	 in RVar (dl, id_of_string s))
     | Meta n ->
 	(* Meta in constr are not user-parsable and are mapped to Evar *)
-	REvar (dummy_loc, n, None)
+	REvar (dl, n, None)
     | Var id ->
 	(try
-	  let _ = Global.lookup_named id in RRef (dummy_loc, VarRef id)
+	  let _ = Global.lookup_named id in RRef (dl, VarRef id)
 	 with _ ->
-	  RVar (dummy_loc, id))
-    | Sort (Prop c) -> RSort (dummy_loc,RProp c)
-    | Sort (Type u) -> RSort (dummy_loc,RType (Some u))
+	  RVar (dl, id))
+    | Sort (Prop c) -> RSort (dl,RProp c)
+    | Sort (Type u) -> RSort (dl,RType (Some u))
     | Cast (c1,k,c2) ->
-	RCast(dummy_loc,detype isgoal avoid env c1, k,
+	RCast(dl,detype isgoal avoid env c1, k,
               detype isgoal avoid env c2)
     | Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
     | Lambda (na,ty,c) -> detype_binder isgoal BLambda avoid env na ty c
     | LetIn (na,b,_,c) -> detype_binder isgoal BLetIn avoid env na b c
     | App (f,args) ->
-	RApp (dummy_loc,detype isgoal avoid env f,
+	RApp (dl,detype isgoal avoid env f,
               array_map_to_list (detype isgoal avoid env) args)
-    | Const sp -> RRef (dummy_loc, ConstRef sp)
+    | Const sp -> RRef (dl, ConstRef sp)
     | Evar (ev,cl) ->
-        REvar (dummy_loc, ev, 
+        REvar (dl, ev, 
                Some (List.map (detype isgoal avoid env) (Array.to_list cl)))
     | Ind ind_sp ->
-	RRef (dummy_loc, IndRef ind_sp)
+	RRef (dl, IndRef ind_sp)
     | Construct cstr_sp ->
-	RRef (dummy_loc, ConstructRef cstr_sp)
-    | Case (annot,p,c,bl) ->
-	let comp = computable p (annot.ci_pp_info.ind_nargs) in
-	let ind = annot.ci_ind in
-	let st = annot.ci_pp_info.style in
-	detype_case comp (detype isgoal avoid env) (detype_eqn isgoal avoid env)
-	  is_nondep_branch avoid
-	  (ind,st,annot.ci_npar,annot.ci_cstr_nargs,annot.ci_pp_info.ind_nargs)
+	RRef (dl, ConstructRef cstr_sp)
+    | Case (ci,p,c,bl) ->
+	let comp = computable p (ci.ci_pp_info.ind_nargs) in
+	detype_case comp (detype isgoal avoid env)
+	  (detype_eqns isgoal avoid env ci comp)
+	  is_nondep_branch avoid 
+	  (ci.ci_ind,ci.ci_pp_info.style,ci.ci_npar,
+	   ci.ci_cstr_nargs,ci.ci_pp_info.ind_nargs)
 	  (Some p) c bl
     | Fix (nvn,recdef) -> detype_fix isgoal avoid env nvn recdef
     | CoFix (n,recdef) -> detype_cofix isgoal avoid env n recdef
@@ -353,7 +421,7 @@ and detype_fix isgoal avoid env (vn,_ as nvn) (names,tys,bodies) =
   let v = array_map3
     (fun c t i -> share_names isgoal (i+1) [] def_avoid def_env c (lift n t))
     bodies tys vn in
-  RRec(dummy_loc,RFix nvn,Array.of_list (List.rev lfi),
+  RRec(dl,RFix nvn,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -369,7 +437,7 @@ and detype_cofix isgoal avoid env n (names,tys,bodies) =
   let v = array_map2
     (fun c t -> share_names isgoal 0 [] def_avoid def_env c (lift ntys t))
     bodies tys in
-  RRec(dummy_loc,RCoFix n,Array.of_list (List.rev lfi),
+  RRec(dl,RCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
@@ -410,18 +478,28 @@ and share_names isgoal n l avoid env c t =
         let t = detype isgoal avoid env t in
         (List.rev l,c,t)
 
+and detype_eqns isgoal avoid env ci computable constructs consnargsl bl =
+  try
+    if !Options.raw_print or not (reverse_matching ()) then raise Exit;
+    let mat = build_tree Anonymous isgoal (avoid,env) ci bl in
+    List.map (fun (pat,((avoid,env),c)) -> (dl,[],[pat],detype isgoal avoid env c))
+      mat
+  with _ ->
+    Array.to_list
+      (array_map3 (detype_eqn isgoal avoid env) constructs consnargsl bl)
+
 and detype_eqn isgoal avoid env constr construct_nargs branch =
   let make_pat x avoid env b ids =
     if force_wildcard () & noccurn 1 b then
-      PatVar (dummy_loc,Anonymous),avoid,(add_name Anonymous env),ids
+      PatVar (dl,Anonymous),avoid,(add_name Anonymous env),ids
     else 
       let id = next_name_away_with_default "x" x avoid in
-      PatVar (dummy_loc,Name id),id::avoid,(add_name (Name id) env),id::ids
+      PatVar (dl,Name id),id::avoid,(add_name (Name id) env),id::ids
   in
   let rec buildrec ids patlist avoid env n b =
     if n=0 then
-      (dummy_loc, ids, 
-       [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
+      (dl, ids, 
+       [PatCstr(dl, constr, List.rev patlist,Anonymous)],
        detype isgoal avoid env b)
     else
       match kind_of_term b with
@@ -455,9 +533,12 @@ and detype_binder isgoal bk avoid env na ty c =
       concrete_name isgoal avoid env na c in
   let r =  detype isgoal avoid' (add_name na' env) c in
   match bk with
-    | BProd -> RProd (dummy_loc, na',detype isgoal avoid env ty, r)
-    | BLambda -> RLambda (dummy_loc, na',detype isgoal avoid env ty, r)
-    | BLetIn -> RLetIn (dummy_loc, na',detype isgoal avoid env ty, r)
+  | BProd -> RProd (dl, na',detype isgoal avoid env ty, r)
+  | BLambda -> RLambda (dl, na',detype isgoal avoid env ty, r)
+  | BLetIn -> RLetIn (dl, na',detype isgoal avoid env ty, r)
+
+(**********************************************************************)
+(* Module substitution: relies on detyping                            *)
 
 let rec subst_cases_pattern subst pat = 
   match pat with
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 2a16b9e7ee..71aed93737 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -32,8 +32,9 @@ val detype : bool -> identifier list -> names_context -> constr -> rawconstr
 
 val detype_case : 
   bool -> ('a -> rawconstr) ->
-  (constructor -> int -> 'a -> loc * identifier list * cases_pattern list *
-    rawconstr) -> ('a -> int -> bool) ->
+  (constructor array -> int array -> 'a array -> 
+    (loc * identifier list * cases_pattern list * rawconstr) list) ->
+  ('a -> int -> bool) ->
   identifier list -> inductive * case_style * int * int array * int ->
     'a option -> 'a -> 'a array -> rawconstr