Handling of left parameters of constructors/indutive type definitions improved.

Bug fixed: arguments of sort Prop were not dropped from MutCase branches.

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index dbb7194a998e69ade2bd60d166712e39754e449f..7be9ea3d9f0e30b566fb67e1e6b793b86b76d9f5 100644 (file)
--- a/helm/software/components/cic_exportation/cicExportation.ml
+++ b/helm/software/components/cic_exportation/cicExportation.ml
@@ -184,12 +184,16 @@ let rec pp t context =
        let hes = pp he context in
        let stl = String.concat "," (clean_args_for_ty context tl) in
         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
-    | C.Appl (C.MutConstruct _ as he::tl) ->
+    | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
+       let nparams =
+        match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+           C.InductiveDefinition (_,_,nparams,_) -> nparams
+         | _ -> assert false in
        let hes = pp he context in
-       let stl = String.concat "," (clean_args context tl) in
+       let stl = String.concat "," (clean_args nparams context tl) in
         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
     | C.Appl li ->
-       "(" ^ String.concat " " (clean_args context li) ^ ")"
+       "(" ^ String.concat " " (clean_args 0 context li) ^ ")"
     | C.Const (uri,exp_named_subst) ->
        qualified_name_of_uri current_module_uri uri ^
         pp_exp_named_subst exp_named_subst context
@@ -225,6 +229,10 @@ let rec pp t context =
            string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
+       let paramsno =
+        match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+           C.InductiveDefinition (_,_,paramsno,_) -> paramsno
+         | _ -> assert false in
        (match analyze_term context te with
            `Type -> assert false
          | `Proof ->
@@ -263,9 +271,8 @@ let rec pp t context =
                 let rec combine =
                    function
                       [],[] -> []
-                    | [],l -> List.map (fun x -> "???",0,Some x) l
-                    | l,[] -> List.map (fun (x,no) -> x,no,None) l
-                    | (x,no)::tlx,y::tly -> (x,no,Some y)::(combine (tlx,tly))
+                    | (x,no)::tlx,y::tly -> (x,no,y)::(combine (tlx,tly))
+                    | _,_ -> assert false
                 in
                  combine (connames_and_argsno,patterns)
                in
@@ -280,23 +287,25 @@ let rec pp t context =
                            aux (argsno - 1) (Some (name,Cic.Decl ty)::context)
                             bo
                           in
-                           (match name with C.Anonymous -> "_" | C.Name s -> s)
-                           ::args,
-                           res
+                           (match analyze_type context ty with
+                               `Statement
+                             | `Sort _ -> args,res
+                             | `Type ->
+                                 (match name with
+                                     C.Anonymous -> "_"
+                                   | C.Name s -> s)::args,res)
                        | t when argsno = 0 -> [],pp t context
                        | t ->
                           ["{" ^ string_of_int argsno ^ " args missing}"],
                            pp t context
                      in
                       let pattern,body =
-                       match y with
-                          None -> x,""
-                        | Some y when argsno = 0 -> x,pp y context
-                        | Some y ->
-                           let args,body = aux argsno context y in
-                           let sargs = String.concat "," args in
-                            x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
-                             body
+                       if argsno = 0 then x,pp y context
+                       else
+                        let args,body = aux argsno context y in
+                        let sargs = String.concat "," args in
+                         x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"),
+                          body
                       in
                        pattern ^ " -> " ^ body
                    ) connames_and_argsno_and_patterns)) ^
@@ -339,13 +348,16 @@ and pp_exp_named_subst exp_named_subst context =
      (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t context)
      exp_named_subst
    ) ^ "]"
-and clean_args context =
+and clean_args nparams context =
+ let nparams = ref nparams in
  HExtlib.filter_map
   (function t ->
+    decr nparams;
     match analyze_term context t with
-       `Type -> None
-     | `Proof -> None
-     | `Term -> Some pp t context)
+       `Term when !nparams < 0 -> Some pp t context
+     | `Term
+     | `Type
+     | `Proof -> None)
 and clean_args_for_ty context =
  HExtlib.filter_map
   (function t ->
@@ -358,7 +370,9 @@ in
 ;;
 
 let ppty current_module_uri =
- let rec args context =
+ (* nparams is the number of left arguments
+    left arguments should either become parameters or be skipped altogether *)
+ let rec args nparams context =
   function
      Cic.Prod (n,s,t) ->
       let n =
@@ -367,21 +381,27 @@ let ppty current_module_uri =
         | Cic.Name n -> Cic.Name (String.uncapitalize n)
       in
        (match analyze_type context s with
-           `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t
-         | `Statement
+           `Statement
+         | `Sort Cic.Prop ->
+             args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+         | `Type when nparams > 0 ->
+             args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+         | `Type ->
+             let abstr,args =
+              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
+               abstr,pp current_module_uri s context::args
          | `Sort _ ->
              let n =
               match n with
                  Cic.Anonymous -> Cic.Anonymous
                | Cic.Name name -> Cic.Name ("'" ^ name) in
-             let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
+             let abstr,args =
+              args (nparams - 1) ((Some (n,Cic.Decl s))::context) t
+             in
               (match n with
                   Cic.Anonymous -> abstr
                 | Cic.Name name -> name::abstr),
-              args
-         | `Type ->
-             let abstr,args = args ((Some (n,Cic.Decl s))::context) t in
-              abstr,pp current_module_uri s context::args)
+              args)
    | _ -> [],[]
  in
   args
@@ -403,7 +423,7 @@ let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons
      let abstr,scons =
       List.fold_right
        (fun (id,ty) (_abstr,i) -> (* we should verify _abstr = abstr' *)
-          let abstr',sargs = ppty current_module_uri [] ty in
+          let abstr',sargs = ppty current_module_uri nparams [] ty in
           let sargs = String.concat " * " sargs in
            abstr',
            String.capitalize id ^
@@ -432,7 +452,7 @@ let ppobj current_module_uri obj =
             match analyze_type [] t1 with
                `Sort Cic.Prop -> ""
              | _ ->
-               let abstr,args = ppty current_module_uri [] t1 in
+               let abstr,args = ppty current_module_uri 0 [] t1 in
                let abstr =
                 let s = String.concat "," abstr in
                 if s = "" then "" else "(" ^ s ^ ") "