Restructuration et simplification des fonctions d'affichage, de détypage

et d'"externalisation"; standardisation du nom des fonctions d'affichage


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

4 files changed, 46 insertions, 26 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 3ebfde29e5..3707c0f9aa 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -458,6 +458,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
       with
 	  No_match -> extern_symbol_pattern allscopes vars t rules
 
+let extern_cases_pattern vars p = 
+  extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p
+
 (**********************************************************************)
 (* Externalising applications *)
 
@@ -839,15 +842,12 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
       with
 	  No_match -> extern_symbol allscopes vars t rules
 
-let extern_rawconstr vars c = 
+let extern_rawconstr vars c =
   extern false (None,Notation.current_scopes()) vars c
 
 let extern_rawtype vars c =
   extern_typ (None,Notation.current_scopes()) vars c
 
-let extern_cases_pattern vars p = 
-  extern_cases_pattern_in_scope (None,Notation.current_scopes()) vars p
-
 (******************************************************************)
 (* Main translation function from constr -> constr_expr *)
 
@@ -855,7 +855,7 @@ let loc = dummy_loc (* for constr and pattern, locations are lost *)
 
 let extern_constr_gen at_top scopt env t =
   let avoid = if at_top then ids_of_context env else [] in
-  let r = Detyping.detype (at_top,env) avoid (names_of_rel_context env) t in
+  let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   let vars = vars_of_env env in
   extern (not at_top) (scopt,Notation.current_scopes()) vars r
 
@@ -867,16 +867,16 @@ let extern_constr at_top env t =
 
 let extern_type at_top env t =
   let avoid = if at_top then ids_of_context env else [] in
-  let r = Detyping.detype (at_top,env) avoid (names_of_rel_context env) t in
+  let r = Detyping.detype at_top avoid (names_of_rel_context env) t in
   extern_rawtype (vars_of_env env) r
 
 (******************************************************************)
 (* Main translation function from pattern -> constr_expr *)
 
-let rec raw_of_pat tenv env = function
+let rec raw_of_pat env = function
   | PRef ref -> RRef (loc,ref)
   | PVar id -> RVar (loc,id)
-  | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat tenv env) l))
+  | PEvar (n,l) -> REvar (loc,n,Some (array_map_to_list (raw_of_pat env) l))
   | PRel n ->
       let id = try match lookup_name_of_rel n env with
 	| Name id   -> id
@@ -887,32 +887,35 @@ let rec raw_of_pat tenv env = function
   | PMeta None -> RHole (loc,Evd.InternalHole)
   | PMeta (Some n) -> RPatVar (loc,(false,n))
   | PApp (f,args) ->
-      RApp (loc,raw_of_pat tenv env f,array_map_to_list (raw_of_pat tenv env) args)
+      RApp (loc,raw_of_pat env f,array_map_to_list (raw_of_pat env) args)
   | PSoApp (n,args) ->
       RApp (loc,RPatVar (loc,(true,n)),
-        List.map (raw_of_pat tenv env) args)
+        List.map (raw_of_pat env) args)
   | PProd (na,t,c) ->
-      RProd (loc,na,raw_of_pat tenv env t,raw_of_pat tenv (na::env) c)
+      RProd (loc,na,raw_of_pat env t,raw_of_pat (na::env) c)
   | PLetIn (na,t,c) ->
-      RLetIn (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c)
+      RLetIn (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
   | PLambda (na,t,c) ->
-      RLambda (loc,na,raw_of_pat tenv env t, raw_of_pat tenv (na::env) c)
+      RLambda (loc,na,raw_of_pat env t, raw_of_pat (na::env) c)
   | PCase ((_,cs),typopt,tm,[||]) ->
       if typopt <> None then failwith "TODO: PCase to RCases";
-      RCases (loc,(*(option_app (raw_of_pat tenv env) typopt,*)None,
-         [raw_of_pat tenv env tm,(Anonymous,None)],[])
+      RCases (loc,(*(option_app (raw_of_pat env) typopt,*)None,
+         [raw_of_pat env tm,(Anonymous,None)],[])
   | PCase ((Some ind,cs),typopt,tm,bv) ->
       let avoid = List.fold_right (name_fold (fun x l -> x::l)) env [] in
-      let k = (snd (lookup_mind_specif (Global.env()) ind)).Declarations.mind_nrealargs in
-      Detyping.detype_case false (raw_of_pat tenv env)(raw_of_eqn tenv env)
+      let mib,mip = lookup_mind_specif (Global.env()) ind in
+      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)
 	(fun _ _ -> false (* lazy: don't try to display pattern with "if" *))
-	tenv avoid ind cs typopt k tm bv
+	avoid (ind,cs,nparams,cstrnargs,k) typopt tm bv
   | PCase _ -> error "Unsupported case-analysis while printing pattern"
-  | PFix f -> Detyping.detype (false,tenv) [] env (mkFix f)
-  | PCoFix c -> Detyping.detype (false,tenv) [] env (mkCoFix c)
+  | PFix f -> Detyping.detype false [] env (mkFix f)
+  | PCoFix c -> Detyping.detype false [] env (mkCoFix c)
   | PSort s -> RSort (loc,s)
 
-and raw_of_eqn tenv env constr construct_nargs branch =
+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
     let id = next_name_away_with_default "x" x avoid in
@@ -922,7 +925,7 @@ and raw_of_eqn tenv env constr construct_nargs branch =
     if n=0 then
       (dummy_loc, ids, 
        [PatCstr(dummy_loc, constr, List.rev patlist,Anonymous)],
-       raw_of_pat tenv env b)
+       raw_of_pat env b)
     else
       match b with
 	| PLambda (x,_,b) -> 
@@ -938,6 +941,6 @@ and raw_of_eqn tenv env constr construct_nargs branch =
   in 
   buildrec [] [] env construct_nargs branch
 
-let extern_pattern tenv env pat =
+let extern_constr_pattern env pat =
   extern true (None,Notation.current_scopes()) Idset.empty
-    (raw_of_pat tenv env pat)
+    (raw_of_pat env pat)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index e97d778c33..37f7369ad6 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -32,7 +32,7 @@ val check_same_type : constr_expr -> constr_expr -> unit
 val extern_cases_pattern : Idset.t -> cases_pattern -> cases_pattern_expr
 val extern_rawconstr : Idset.t -> rawconstr -> constr_expr
 val extern_rawtype : Idset.t -> rawconstr -> constr_expr
-val extern_pattern : env -> names_context -> constr_pattern -> constr_expr
+val extern_constr_pattern : names_context -> constr_pattern -> constr_expr
 
 (* If [b=true] in [extern_constr b env c] then the variables in the first 
    level of quantification clashing with the variables in [env] are renamed *)
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 771c5716b2..da67c9f3ff 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -247,7 +247,7 @@ let aconstr_of_rawconstr vars a =
   a
 
 let aconstr_of_constr avoiding t =
- aconstr_of_rawconstr [] (Detyping.detype (false,Global.env()) avoiding [] t)
+ aconstr_of_rawconstr [] (Detyping.detype false avoiding [] t)
 
 let rec subst_aconstr subst bound raw =
   match raw with
@@ -630,6 +630,20 @@ let mkLambdaC (idl,a,b) = CLambdaN (dummy_loc,[idl,a],b)
 let mkLetInC (id,a,b)   = CLetIn (dummy_loc,id,a,b)
 let mkProdC (idl,a,b)   = CProdN (dummy_loc,[idl,a],b)
 
+let rec abstract_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
+      (abstract_constr_expr c bl)
+      
+let rec prod_constr_expr c = function
+  | [] -> c
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,prod_constr_expr c bl)
+  | LocalRawAssum (idl,t)::bl ->
+      List.fold_right (fun x b -> mkProdC([x],t,b)) idl
+      (prod_constr_expr c bl)
+
 let coerce_to_id = function
   | CRef (Ident (loc,id)) -> (loc,id)
   | a -> user_err_loc
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 5b9d69cd67..d6f7dbd037 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -144,6 +144,9 @@ val mkProdC : name located list * constr_expr * constr_expr -> constr_expr
 
 val coerce_to_id : constr_expr -> identifier located
 
+val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
+val prod_constr_expr : constr_expr -> local_binder list -> constr_expr
+
 (* For binders parsing *)
 
 (* Includes let binders *)