From: Claudio Sacerdoti Coen Date: Mon, 5 Nov 2007 14:56:16 +0000 (+0000) Subject: MutCases that occur in types should be handled with "any type". X-Git-Tag: make_still_working~5897 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=991427cc0c77549103c07318963259c9148508f3;p=helm.git MutCases that occur in types should be handled with "any type". 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. --- diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 79eab870d..9296b7bb0 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -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 ""