]> matita.cs.unibo.it Git - helm.git/commitdiff
MutCases that occur in types should be handled with "any type".
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Nov 2007 14:56:16 +0000 (14:56 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 5 Nov 2007 14:56:16 +0000 (14:56 +0000)
Unfortunately, such type does not exists in OCaml. For now I generate
unit with a comment. Applications to arguments will fail and require another
Obj.magic.

helm/software/components/cic_exportation/cicExportation.ml

index 79eab870d2c9a7c421c3f1cdfed5d2b7f61c1946..9296b7bb05d260fd4429147b12c354104070a95c 100644 (file)
@@ -103,12 +103,8 @@ let qualified_name_of_uri current_module_uri ?(capitalize=false) uri =
    String.capitalize filename ^ "." ^ name
 ;;
 
-(* pp t l                                                                  *)
-(* pretty-prints a term t of cic in an environment l where l is a list of  *)
-(* identifier names used to resolve DeBrujin indexes. The head of l is the *)
-(* name associated to the greatest DeBrujin index in t                     *)
-let pp current_module_uri ?metasenv =
-let rec pp t context =
+let pp current_module_uri ?metasenv ~in_type =
+let rec pp ~in_type t context =
  let module C = Cic in
    match t with
       C.Rel n ->
@@ -130,7 +126,10 @@ let rec pp t context =
            None ->
             "?" ^ (string_of_int n) ^ "[" ^ 
              String.concat " ; "
-              (List.rev_map (function None -> "_" | Some t -> pp t context) l1) ^
+              (List.rev_map
+                (function
+                    None -> "_"
+                  | Some t -> pp ~in_type:false t context) l1) ^
              "]"
          | Some metasenv ->
             try
@@ -143,7 +142,7 @@ let rec pp t context =
                       match x,y with
                          _, None
                        | None, _ -> "_"
-                       | Some _, Some t -> pp t context
+                       | Some _, Some t -> pp ~in_type:false t context
                     ) context l1)) ^
                "]"
             with
@@ -151,7 +150,8 @@ let rec pp t context =
             | Invalid_argument _ ->
               "???" ^ (string_of_int n) ^ "[" ^ 
                String.concat " ; "
-                (List.rev_map (function None -> "_" | Some t -> pp t context) l1) ^
+                (List.rev_map (function None -> "_" | Some t ->
+                  pp ~in_type:false t context) l1) ^
                "]"
        )
     | C.Sort s ->
@@ -168,20 +168,25 @@ let rec pp t context =
        (match b with
           C.Name n ->
            let n = "'" ^ String.uncapitalize n in
-            "(" ^ pp s context ^ " -> " ^ pp t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
-        | C.Anonymous -> "(" ^ pp s context ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")"
-       )
-    | C.Cast (v,t) -> pp v context
+            "(" ^ pp ~in_type:true s context ^ " -> " ^
+            pp ~in_type:true t ((Some (Cic.Name n,Cic.Decl s))::context) ^ ")"
+        | C.Anonymous ->
+           "(" ^ pp ~in_type:true s context ^ " -> " ^
+           pp ~in_type:true t ((Some (b,Cic.Decl s))::context) ^ ")")
+    | C.Cast (v,t) -> pp ~in_type v context
     | C.Lambda (b,s,t) ->
        (match analyze_type context s with
            `Sort _
-         | `Statement -> pp t ((Some (b,Cic.Decl s))::context)
-         | `Type -> "(function " ^ ppname b ^ " -> " ^ pp t ((Some (b,Cic.Decl s))::context) ^ ")")
+         | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context)
+         | `Type ->
+            "(function " ^ ppname b ^ " -> " ^
+             pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")")
     | C.LetIn (b,s,t) ->
        let ty,_ = CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph in
-       "(let " ^ ppname b ^ " = " ^ pp s context ^ " in " ^ pp t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
+       "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^
+        pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")"
     | C.Appl (C.MutInd _ as he::tl) ->
-       let hes = pp he context in
+       let hes = pp ~in_type he context in
        let stl = String.concat "," (clean_args_for_ty context tl) in
         (if stl = "" then "" else "(" ^ stl ^ ") ") ^ hes
     | C.Appl (C.MutConstruct (uri,n,_,_) as he::tl) ->
@@ -189,7 +194,7 @@ let rec pp t context =
         match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
            C.InductiveDefinition (_,_,nparams,_) -> nparams
          | _ -> assert false in
-       let hes = pp he context in
+       let hes = pp ~in_type he context in
        let stl = String.concat "," (clean_args nparams context tl) in
         "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")"
     | C.Appl li ->
@@ -229,21 +234,21 @@ let rec pp t context =
            string_of_int n2
        )
     | C.MutCase (uri,n1,ty,te,patterns) ->
+       if in_type then
+        "unit (* TOO POLYMORPHIC TYPE *)"
+       else (
        let needs_obj_magic =
         match ty with
            Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t)
          | _ -> assert false
        in
-       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 ->
              (match patterns with
                  [] -> "assert false"   (* empty type elimination *)
-               | [he] -> pp he context  (* singleton elimination *)
+               | [he] ->
+                  pp ~in_type:false he context  (* singleton elimination *)
                | _ -> assert false)
          | `Term ->
             if patterns = [] then "assert false"
@@ -281,7 +286,7 @@ let rec pp t context =
                 in
                  combine (connames_and_argsno,patterns)
                in
-                "\n(match " ^ pp te context ^ " with \n   " ^
+                "\n(match " ^ pp ~in_type:false te context ^ " with \n   " ^
                  (String.concat "\n | "
                   (List.map
                    (fun (x,argsno,y) ->
@@ -299,13 +304,13 @@ let rec pp t context =
                                  (match name with
                                      C.Anonymous -> "_"
                                    | C.Name s -> s)::args,res)
-                       | t when argsno = 0 -> [],pp t context
+                       | t when argsno = 0 -> [],pp ~in_type:false t context
                        | t ->
                           ["{" ^ string_of_int argsno ^ " args missing}"],
-                           pp t context
+                           pp ~in_type:false t context
                      in
                       let pattern,body =
-                       if argsno = 0 then x,pp y context
+                       if argsno = 0 then x,pp ~in_type:false y context
                        else
                         let args,body = aux argsno context y in
                         let sargs = String.concat "," args in
@@ -318,7 +323,7 @@ let rec pp t context =
                         else
                          body
                    ) connames_and_argsno_and_patterns)) ^
-                 ")\n"))
+                 ")\n")))
     | C.Fix (no, funs) ->
        let names =
         List.rev
@@ -329,7 +334,7 @@ let rec pp t context =
          "let rec " ^
          List.fold_right
           (fun (name,ind,ty,bo) i -> name ^ " = \n" ^
-            pp bo (names@context) ^ i)
+            pp ~in_type:false bo (names@context) ^ i)
           funs "" ^
          " in " ^
          (match get_nth names (no + 1) with
@@ -345,8 +350,8 @@ let rec pp t context =
          "\nCoFix " ^ " {" ^
          List.fold_right
           (fun (name,ty,bo) i -> "\n" ^ name ^ 
-            " : " ^ pp ty context ^ " := \n" ^
-            pp bo (names@context) ^ i)
+            " : " ^ pp ~in_type:true ty context ^ " := \n" ^
+            pp ~in_type:false bo (names@context) ^ i)
           funs "" ^
          "}\n"
 and pp_exp_named_subst exp_named_subst context =
@@ -354,7 +359,7 @@ and pp_exp_named_subst exp_named_subst context =
   "\\subst[" ^
    String.concat " ; " (
     List.map
-     (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp t context)
+     (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context)
      exp_named_subst
    ) ^ "]"
 and clean_args nparams context =
@@ -363,7 +368,7 @@ and clean_args nparams context =
   (function t ->
     decr nparams;
     match analyze_term context t with
-       `Term when !nparams < 0 -> Some pp t context
+       `Term when !nparams < 0 -> Some (pp ~in_type:false t context)
      | `Term
      | `Type
      | `Proof -> None)
@@ -371,11 +376,11 @@ and clean_args_for_ty context =
  HExtlib.filter_map
   (function t ->
     match analyze_term context t with
-       `Type -> Some pp t context
+       `Type -> Some (pp ~in_type:true t context)
      | `Proof -> None
      | `Term -> None)
 in
- pp
+ pp ~in_type
 ;;
 
 let ppty current_module_uri =
@@ -398,7 +403,7 @@ let ppty current_module_uri =
          | `Type ->
              let abstr,args =
               args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in
-               abstr,pp current_module_uri s context::args
+               abstr,pp ~in_type:true current_module_uri s context::args
          | `Sort _ ->
              let n =
               match n with
@@ -450,13 +455,13 @@ let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons
 let ppobj current_module_uri obj =
  let module C = Cic in
  let module U = UriManager in
-  let pp = pp current_module_uri in
+  let pp ~in_type = pp ~in_type current_module_uri in
   match obj with
     C.Constant (name, Some t1, t2, params, _) ->
       (match analyze_type [] t2 with
           `Sort Cic.Prop
         | `Statement -> ""
-        | `Type -> "let " ^ ppid name ^ " =\n" ^ pp t1 [] ^ "\n"
+        | `Type -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n"
         | `Sort _ ->
             match analyze_type [] t1 with
                `Sort Cic.Prop -> ""
@@ -478,8 +483,8 @@ let ppobj current_module_uri obj =
       "Variable " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
        ")" ^ ":\n" ^
-       pp ty [] ^ "\n" ^
-       (match bo with None -> "" | Some bo -> ":= " ^ pp bo [])
+       pp ~in_type:true ty [] ^ "\n" ^
+       (match bo with None -> "" | Some bo -> ":= " ^ pp ~in_type:false bo [])
    | C.CurrentProof (name, conjectures, value, ty, params, _) ->
       "Current Proof of " ^ name ^
        "(" ^ String.concat ";" (List.map UriManager.string_of_uri params) ^
@@ -494,12 +499,13 @@ let ppobj current_module_uri obj =
                        Some (n,C.Decl at) ->
                          (separate i) ^
                            ppname n ^ ":" ^
-                            pp ~metasenv:conjectures at name_context ^ " ",
+                            pp ~in_type:true ~metasenv:conjectures
+                            at name_context ^ " ",
                             context_entry::name_context
                      | Some (n,C.Def (at,None)) ->
                          (separate i) ^
-                           ppname n ^ ":= " ^ pp ~metasenv:conjectures
-                            at name_context ^ " ",
+                           ppname n ^ ":= " ^ pp ~in_type:false
+                            ~metasenv:conjectures at name_context ^ " ",
                             context_entry::name_context
                       | None ->
                          (separate i) ^ "_ :? _ ", context_entry::name_context
@@ -507,10 +513,10 @@ let ppobj current_module_uri obj =
             ) context ("",[])
           in
            conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^
-            pp ~metasenv:conjectures t name_context ^ "\n" ^ i
+            pp ~in_type:true ~metasenv:conjectures t name_context ^ "\n" ^ i
         ) conjectures "" ^
-        "\n" ^ pp ~metasenv:conjectures value [] ^ " : " ^
-          pp ~metasenv:conjectures ty [] 
+        "\n" ^ pp ~in_type:false ~metasenv:conjectures value [] ^ " : " ^
+          pp ~in_type:true ~metasenv:conjectures ty [] 
    | C.InductiveDefinition (l, params, nparams, _) ->
       List.fold_right
        (fun x i -> ppinductiveType current_module_uri nparams x ^ i) l ""