Amélioration afficheur de Cases pour les constr_pattern

Déplacement traducteur de nom dans Constrextern pour accès aux noms longs
Extension du traducteur de nom
Ajout notation c.(f) en v8 pour les projections de Record


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

2 files changed, 201 insertions, 126 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index d23986def..102754384 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -118,8 +118,93 @@ let raw_string_of_ref = function
   | VarRef id -> 
       "SECVAR("^(string_of_id id)^")"
 
+(* v7->v8 translation *)
+
+let is_coq_root d =
+  let d = repr_dirpath d in d <> [] & string_of_id (list_last d) = "Coq"
+
+let is_module m =
+  let d = repr_dirpath (Lib.library_dp()) in
+  d <> [] & string_of_id (List.hd d) = m
+
+let translate_v7_string = function
+  (* ZArith *)
+  | "double_moins_un" -> "double_minus_one"
+  | "double_moins_deux" -> "double_minus_two"
+  | "entier" -> "N"
+  | "SUPERIEUR" -> "GREATER"
+  | "EGAL" -> "EQUAL"
+  | "INFERIEUR" -> "LESS"
+  | "add" -> "Padd"
+  | "times" when not (is_module "Mapfold") -> "Pmult"
+  | "true_sub" -> "Psub"
+  | "add_un" -> "Padd_one"
+  | "sub_un" -> "Psub_one"
+  | "sub_pos" -> "PNsub"
+  | "sub_neg" -> "PNsub_carry"
+  | "convert_add_un" -> "convert_Padd_one"
+  | "compare_convert_INFERIEUR" -> "compare_convert_LESS"
+  | "compare_convert_SUPERIEUR" -> "compare_convert_GREATER"
+  | "compare_convert_EGAL"      -> "compare_convert_EQUAL"
+  | "convert_compare_INFERIEUR" -> "convert_compare_LESS"
+  | "convert_compare_SUPERIEUR" -> "convert_compare_GREATER"
+  | "convert_compare_EGAL"      -> "convert_compare_EQUAL"
+  | "Zcompare_EGAL"             -> "Zcompare_EQUAL"
+  | "Nul" -> "Null"
+  | "Un_suivi_de" -> "double_plus_one"
+  | "Zero_suivi_de" -> "double"
+  | "is_double_moins_un" -> "is_double_minus_one"
+  | "Zplus_sym" -> "Zplus_comm"
+  | "Zmult_sym" -> "Zmult_comm"
+  | "sub_pos_SUPERIEUR" -> "sub_pos_GREATER"
+  | "inject_nat" -> "INZ"
+  | "convert" -> "IPN"
+  | "anti_convert" -> "INP"
+  | "convert_intro" -> "IPN_inj"
+  | "convert_add" -> "IPN_add"
+  | "convert_add_carry" -> "IPN_add_carry"
+  | "compare_convert_O" -> "lt_O_IPN"
+  | "Zopp_intro" -> "Zopp_inj"
+  (* Arith *)
+  | "plus_sym" -> "plus_comm"
+  | "mult_sym" -> "mult_comm"
+  | "max_sym" -> "max_comm"
+  | "min_sym" -> "min_comm"
+  | "gt_not_sym" -> "gt_asym"
+  | "fact_growing" -> "fact_le"
+  (* Lists *)
+  | "idempot_rev" -> "involutive_rev"
+  (* Bool *)
+  | "orb_sym" -> "orb_comm"
+  | "andb_sym" -> "andb_comm"
+  (* Reals *)
+    (* redundant *)
+  | "Rle_sym1" -> "Rle_ge"
+  | "Rmin_sym" -> "Rmin_comm"
+  | s when String.length s >= 7 & 
+      let s' = String.sub s 0 7 in
+      (s' = "unicite" or s' = "unicity") ->
+      "uniqueness"^(String.sub s 7 (String.length s - 7))
+  (* Default *)
+  | x -> x
+
+let id_of_v7_string s =
+  id_of_string (if !Options.v7 then s else translate_v7_string s)
+
+let v7_to_v8_dir_id dir id =
+  if Options.do_translate()
+    & (is_coq_root (Lib.library_dp()) or is_coq_root dir)
+  then id_of_string (translate_v7_string (string_of_id id)) else id
+
+let v7_to_v8_id = v7_to_v8_dir_id empty_dirpath
+
+let shortest_qualid_of_v7_global ctx ref =
+  let fulldir,_ = repr_path (sp_of_global ref) in
+  let dir,id = repr_qualid (shortest_qualid_of_global ctx ref) in
+  make_qualid dir (v7_to_v8_dir_id fulldir id)
+
 let extern_reference loc vars r =
-  try Qualid (loc,shortest_qualid_of_global vars r)
+  try Qualid (loc,shortest_qualid_of_v7_global vars r)
   with Not_found ->
     (* happens in debugger *)
     Ident (loc,id_of_string (raw_string_of_ref r))
@@ -127,11 +212,13 @@ let extern_reference loc vars r =
 (**********************************************************************)
 (* conversion of terms and cases patterns                             *)
 
+let make_current_scope (scopt,scopes) = option_cons scopt scopes
+
 let rec extern_cases_pattern_in_scope scopes vars pat =
   try 
     if !print_no_symbol then raise No_match;
     let (sc,n) = Symbols.uninterp_cases_numeral pat in
-    match Symbols.availability_of_numeral sc scopes with
+    match Symbols.availability_of_numeral sc (make_current_scope scopes) with
     | None -> raise No_match
     | Some key ->
         let loc = pattern_loc pat in
@@ -153,9 +240,16 @@ let occur_name na aty =
     | Name id -> occur_var_constr_expr id aty
     | Anonymous -> false
 
+let is_projection nargs = function
+  | Some r -> 
+      (try Recordops.find_projection_nparams r + 1 = nargs
+       with Not_found -> false)
+  | None ->
+      false
+
 (* Implicit args indexes are in ascending order *)
 (* inctx is useful only if there is a last argument to be deduced from ctxt *)
-let explicitize loc inctx impl f args =
+let explicitize loc inctx impl (cf,f) args =
   let n = List.length args in
   let rec exprec q = function
     | a::args, imp::impl when is_status_implicit imp ->
@@ -169,8 +263,9 @@ let explicitize loc inctx impl f args =
     | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
     | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
     | [], _ -> [] in
+  let isproj = is_projection (List.length args) cf in
   let args = exprec 1 (args,impl) in
-  if args = [] then f else CApp (loc, f, args)
+  if args = [] then f else CApp (loc, (isproj, f), args)
 
 let rec skip_coercion dest_ref (f,args as app) =
   if !print_coercions or Options.do_translate () then app
@@ -188,23 +283,23 @@ let rec skip_coercion dest_ref (f,args as app) =
 	| None -> app
     with Not_found -> app
 
-let extern_app loc inctx impl f args =
+let extern_app loc inctx impl (cf,f) args =
   if !print_implicits &
     not !print_implicits_explicit_args &
     List.exists is_status_implicit impl
   then 
     if args = [] (* maybe caused by a hidden coercion *) then CRef f 
-    else CAppExpl (loc, f, args)
+    else CAppExpl (loc, (is_projection (List.length args) cf, f), args)
   else
-    explicitize loc inctx impl (CRef f) args
+    explicitize loc inctx impl (cf,CRef f) args
 
 let rec extern_args extern scopes env args subscopes =
   match args with
     | [] -> []
     | a::args ->
 	let argscopes, subscopes = match subscopes with
-	  | [] -> scopes, []
-	  | scopt::subscopes -> option_cons scopt scopes, subscopes in
+	  | [] -> (None,scopes), []
+	  | scopt::subscopes -> (scopt,scopes), subscopes in
 	extern argscopes env a :: extern_args extern scopes env args subscopes
 
 let rec extern inctx scopes vars r =
@@ -219,7 +314,7 @@ let rec extern inctx scopes vars r =
   with No_match -> match r with
   | RRef (loc,ref) -> CRef (extern_reference loc vars ref)
 
-  | RVar (loc,id) -> CRef (Ident (loc,id))
+  | RVar (loc,id) -> CRef (Ident (loc,v7_to_v8_id id))
 
   | REvar (loc,n) -> extern_evar loc n
 
@@ -235,39 +330,40 @@ let rec extern inctx scopes vars r =
 	 | REvar (loc,ev) -> extern_evar loc ev (* we drop args *)
 	 | RRef (loc,ref) ->
 	     let subscopes = Symbols.find_arguments_scope ref in
-	     let args = extern_args (extern true) scopes vars args subscopes in
+	     let args =
+	       extern_args (extern true) (snd scopes) vars args subscopes in
 	     extern_app loc inctx (implicits_of_global_out ref)
-               (extern_reference loc vars ref)
+               (Some ref,extern_reference loc vars ref)
 	       args
 	 | RVar (loc,id) -> (* useful for translation of inductive *)
 	     let args = List.map (extern true scopes vars) args in
 	     extern_app loc inctx (get_temporary_implicits_out id)
-	       (Ident (loc,id))
+	       (None,Ident (loc,v7_to_v8_id id))
 	       args
 	 | _       -> 
-	     explicitize loc inctx [] (extern false scopes vars f)
+	     explicitize loc inctx [] (None,extern false scopes vars f)
                (List.map (extern true scopes vars) args))
 
   | RProd (loc,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
-      CArrow (loc,extern true scopes vars t, extern true scopes vars c)
+      CArrow (loc,extern_type scopes vars t, extern_type scopes vars c)
 
   | RLetIn (loc,na,t,c) ->
       CLetIn (loc,(loc,na),extern false scopes vars t,
               extern inctx scopes (add_vname vars na) c)
 
   | RProd (loc,na,t,c) ->
-      let t = extern true scopes vars (anonymize_if_reserved na t) in
+      let t = extern_type scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_prod scopes (add_vname vars na) t c in
       CProdN (loc,[(dummy_loc,na)::idl,t],c)
 
   | RLambda (loc,na,t,c) ->
-      let t = extern true scopes vars (anonymize_if_reserved na t) in
+      let t = extern_type scopes vars (anonymize_if_reserved na t) in
       let (idl,c) = factorize_lambda inctx scopes (add_vname vars na) t c in
       CLambdaN (loc,[(dummy_loc,na)::idl,t],c)
 
   | RCases (loc,typopt,tml,eqns) ->
-      let pred = option_app (extern true scopes vars) typopt in
+      let pred = option_app (extern_type scopes vars) typopt in
       let tml = List.map (extern false scopes vars) tml in
       let eqns = List.map (extern_eqn (typopt<>None) scopes vars) eqns in 
       CCases (loc,pred,tml,eqns)
@@ -276,7 +372,7 @@ let rec extern inctx scopes vars r =
       let bv = Array.to_list (Array.map (extern (typopt<>None) scopes vars) bv)
       in
       COrderedCase
-	(loc,cs,option_app (extern true scopes vars) typopt,
+	(loc,cs,option_app (extern_type scopes vars) typopt,
          extern false scopes vars tm,bv)
 
   | RRec (loc,fk,idv,tyv,bv) ->
@@ -307,10 +403,12 @@ let rec extern inctx scopes vars r =
   | RHole (loc,e) -> CHole loc
 
   | RCast (loc,c,t) ->
-      CCast (loc,extern false scopes vars c,extern false scopes vars t)
+      CCast (loc,extern false scopes vars c,extern_type scopes vars t)
 
   | RDynamic (loc,d) -> CDynamic (loc,d)
-	
+
+and extern_type (_,scopes) = extern true (Some Symbols.type_scope,scopes)
+
 and factorize_prod scopes vars aty = function
   | RProd (loc,(Name id as na),ty,c)
       when aty = extern true scopes vars (anonymize_if_reserved na ty)
@@ -333,11 +431,11 @@ and extern_eqn inctx scopes vars (loc,ids,pl,c) =
    extern inctx scopes vars c)
 
 and extern_numeral loc scopes (sc,n) =
-  match Symbols.availability_of_numeral sc scopes with
+  match Symbols.availability_of_numeral sc (make_current_scope scopes) with
     | None -> raise No_match
     | Some key -> insert_delimiters (CNumeral (loc,n)) key
 
-and extern_symbol scopes vars t = function
+and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
   | [] -> raise No_match
   | (keyrule,pat,n as rule)::rules ->
       let loc = Rawterm.loc t in
@@ -354,31 +452,34 @@ and extern_symbol scopes vars t = function
         let e =
           match keyrule with
           | NotationRule (sc,ntn) ->
-	      (match Symbols.availability_of_notation (sc,ntn) scopes with
+	      let scopes' = option_cons tmp_scope scopes in
+	      (match Symbols.availability_of_notation (sc,ntn) scopes' with
                   (* Uninterpretation is not allowed in current context *)
               | None -> raise No_match
                   (* Uninterpretation is allowed in current context *)
 	      | Some (scopt,key) ->
 	          let scopes = option_cons scopt scopes in
 	          let l =
-		    List.map (fun (c,scl) ->
+		    List.map (fun (c,(scopt,scl)) ->
 		      extern (* assuming no overloading: *) true
-		        (scl@scopes) vars c)
+		        (scopt,scl@scopes) vars c)
                       subst in
 	          insert_delimiters (CNotation (loc,ntn,l)) key)
           | SynDefRule kn ->
               CRef (Qualid (loc, shortest_qualid_of_syndef kn)) in
  	if args = [] then e 
-	else explicitize loc false [] e 
-	  (List.map (extern true scopes vars) args)
+	else
+	  (* TODO: compute scopt for the extra args, in case, head is a ref *)
+	  explicitize loc false [] (None,e)
+	  (List.map (extern true allscopes vars) args)
       with
-	  No_match -> extern_symbol scopes vars t rules
+	  No_match -> extern_symbol allscopes vars t rules
 
 let extern_rawconstr vars c = 
-  extern false (Symbols.current_scopes()) vars c
+  extern false (None,Symbols.current_scopes()) vars c
 
 let extern_cases_pattern vars p = 
-  extern_cases_pattern_in_scope (Symbols.current_scopes()) vars p
+  extern_cases_pattern_in_scope (None,Symbols.current_scopes()) vars p
 
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
@@ -388,110 +489,79 @@ let loc = dummy_loc (* for constr and pattern, locations are lost *)
 let extern_constr at_top env t =
   let vars = vars_of_env env in
   let avoid = if at_top then ids_of_context env else [] in
-  extern (not at_top) (Symbols.current_scopes()) vars
+  extern (not at_top) (None,Symbols.current_scopes()) vars
     (Detyping.detype env avoid (names_of_rel_context env) t)
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
-let rec extern_pattern tenv vars env = function
-  | PRef ref -> CRef (extern_reference loc vars ref)
-
-  | PVar id -> CRef (Ident (loc,id))
-
-  | PEvar n -> extern_evar loc n
-
+let rec raw_of_pat tenv env = function
+  | PRef ref -> RRef (loc,ref)
+  | PVar id -> RVar (loc,id)
+  | PEvar n -> REvar (loc,n)
   | PRel n ->
-      CRef (Ident (loc,
-        try match lookup_name_of_rel n env with
-	 | Name id   -> id
-	 | Anonymous ->
-	     anomaly "ast_of_pattern: index to an anonymous variable"
-       with Not_found ->
-	 id_of_string ("[REL "^(string_of_int n)^"]")))
-
-  | PMeta None -> CHole loc
-
-  | PMeta (Some n) -> CPatVar (loc,(false,n))
-
+      let id = try match lookup_name_of_rel n env with
+	| Name id   -> id
+	| Anonymous ->
+	    anomaly "rawconstr_of_pattern: index to an anonymous variable"
+      with Not_found -> id_of_string ("[REL "^(string_of_int n)^"]") in
+      RVar (loc,id)
+  | PMeta None -> RHole (loc,InternalHole)
+  | PMeta (Some n) -> RPatVar (loc,(false,n))
   | PApp (f,args) ->
-      let (f,args) = 
-	skip_coercion (function PRef r -> Some r | _ -> None)
-	  (f,Array.to_list args) in
-      let args = List.map (extern_pattern tenv vars env) args in
-      (match f with
-	 | PRef ref ->
-	     extern_app loc false (implicits_of_global ref)
-               (extern_reference loc vars ref)
-	       args
-	 | _       ->
-	     explicitize loc false [] (extern_pattern tenv vars env f) args)
-
+      RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args)
   | PSoApp (n,args) ->
-      let args = List.map (extern_pattern tenv vars env) args in
-      (* [-n] is the trick to embed a so patten into a regular application *)
-      (* see constrintern.ml and g_constr.ml4 *)
-      explicitize loc false [] (CPatVar (loc,(true,n))) args
-
-  | PProd (Anonymous,t,c) ->
-      (* Anonymous product are never factorized *)
-      CArrow (loc,extern_pattern tenv vars env t,
-              extern_pattern tenv vars env c)
-
-  | PLetIn (na,t,c) ->
-      CLetIn (loc,(loc,na),extern_pattern tenv vars env t,
-              extern_pattern tenv (add_vname vars na) (na::env) c)
-
+      RApp (loc,RPatVar (loc,(true,n)),
+        List.map (raw_of_pat tenv env) args)
   | PProd (na,t,c) ->
-      let t = extern_pattern tenv vars env t in
-      let (idl,c) =
-        factorize_prod_pattern tenv (add_vname vars na) (na::env) t c in
-      CProdN (loc,[(loc,na)::idl,t],c)
-
+      RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c)
+  | PLetIn (na,t,c) ->
+      RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c)
   | PLambda (na,t,c) ->
-      let t = extern_pattern tenv vars env t in
-      let (idl,c) =
-        factorize_lambda_pattern tenv (add_vname vars na) (na::env) t c in
-      CLambdaN (loc,[(loc,na)::idl,t],c)
-
-  | PCase (cs,typopt,tm,bv) ->
-      let bv = Array.to_list (Array.map (extern_pattern tenv vars env) bv) in
-      COrderedCase
-	(loc,cs,option_app (extern_pattern tenv vars env) typopt,
-	 extern_pattern tenv vars env tm,bv)
-
-  | PFix f ->
-      extern true (Symbols.current_scopes()) vars
-        (Detyping.detype tenv [] env (mkFix f))
-
-  | PCoFix c ->
-      extern true (Symbols.current_scopes()) vars
-        (Detyping.detype tenv [] env (mkCoFix c))
-
-  | PSort s ->
-      let s = match s with
-	 | RProp _ -> s
-	 | RType (Some _) when !print_universes -> s
-	 | RType _ -> RType None in
-      CSort (loc,s)
-
-and factorize_prod_pattern tenv vars env aty = function
-  | PProd (Name id as na,ty,c)
-      when aty = extern_pattern tenv vars env ty
-      & not (occur_var_constr_expr id aty) (*To avoid na in ty escapes scope*)
-	-> let (nal,c) =
-          factorize_prod_pattern tenv (add_vname vars na) (na::env) aty c in
-	   ((loc,Name id)::nal,c)
-  | c -> ([],extern_pattern tenv vars env c)
-
-and factorize_lambda_pattern tenv vars env aty = function
-  | PLambda (na,ty,c)
-      when aty = extern_pattern tenv vars env ty
-	& not (occur_name na aty) (* To avoid na in ty' escapes scope *)
-	-> let (nal,c) =
-          factorize_lambda_pattern tenv (add_vname vars na) (na::env) aty c
-        in ((loc,na)::nal,c)
-  | c -> ([],extern_pattern tenv vars env c)
+      RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c)
+  | PCase ((_,(IfStyle|LetStyle as cs)),typopt,tm,bv) ->
+      ROrderedCase (loc,cs,option_app (raw_of_pat tenv env) typopt,
+         raw_of_pat tenv env tm,Array.map (raw_of_pat tenv env) bv)
+  | PCase ((_,cs),typopt,tm,[||]) ->
+      RCases (loc,option_app (raw_of_pat tenv env) typopt,
+         [raw_of_pat tenv env tm],[])
+  | PCase ((Some ind,cs),typopt,tm,bv) ->
+      let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
+      Detyping.detype_case false
+	(fun tenv _ -> raw_of_pat tenv)
+	(fun tenv _ -> raw_of_eqn tenv)
+	tenv avoid env ind cs typopt tm bv
+  | PCase _ -> error "Unsupported case-analysis while printing pattern"
+  | PFix f -> Detyping.detype tenv [] env (mkFix f)
+  | PCoFix c -> Detyping.detype tenv [] env (mkCoFix c)
+  | PSort s -> RSort (loc,s)
+
+and raw_of_eqn tenv 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
+    let id = next_name_away_with_default "x" x avoid in
+    PatVar (dummy_loc,Name id),(Name id)::env,id::ids
+  in
+  let rec buildrec ids patlist env n b =
+    if n=0 then
+      (dummy_loc, ids, 
+       [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
+       raw_of_pat tenv env b)
+    else
+      match b with
+	| PLambda (x,_,b) -> 
+	    let pat,new_env,new_ids = make_pat x env b ids in
+            buildrec new_ids (pat::patlist) new_env (n-1) b
+
+	| PLetIn (x,_,b) -> 
+	    let pat,new_env,new_ids = make_pat x env b ids in
+            buildrec new_ids (pat::patlist) new_env (n-1) b
+
+	| _ ->
+	    error "Unsupported branch in case-analysis while printing pattern"
+  in 
+  buildrec [] [] env construct_nargs branch
 
 let extern_pattern tenv env pat =
-  extern_pattern tenv (vars_of_env tenv) env pat
+  extern true (None,Symbols.current_scopes()) Idset.empty
+    (raw_of_pat tenv env pat)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index cb58ca58e..e5cfd0190 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -22,6 +22,11 @@ open Topconstr
 open Symbols
 (*i*)
 
+(* v7->v8 translation *)
+val id_of_v7_string : string -> identifier
+val v7_to_v8_id : identifier -> identifier (* v7->v8 translation *)
+val shortest_qualid_of_v7_global : Idset.t -> global_reference -> qualid
+
 (* Translation of pattern, cases pattern, rawterm and term into syntax
    trees for printing *)