X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fcic_exportation%2FcicExportation.ml;h=8af058f9692d3bb8590fac15264d8236893c859b;hb=24dd4569daf1d35bffaa813b8164058d8643f14d;hp=7be9ea3d9f0e30b566fb67e1e6b793b86b76d9f5;hpb=0831e5dbfb2ca0424c7273477506a505f7c3262d;p=helm.git diff --git a/components/cic_exportation/cicExportation.ml b/components/cic_exportation/cicExportation.ml index 7be9ea3d9..8af058f96 100644 --- a/components/cic_exportation/cicExportation.ml +++ b/components/cic_exportation/cicExportation.ml @@ -45,8 +45,7 @@ let analyze_type context t = let rec aux = function Cic.Sort s -> `Sort s - | Cic.Prod (_,_,t) - | Cic.Lambda (_,_,t) -> aux t + | Cic.Prod (_,_,t) -> aux t | _ -> `SomethingElse in match aux t with @@ -63,7 +62,9 @@ let ppid = let reserved = [ "to"; "mod"; - "val" + "val"; + "in"; + "function" ] in function n -> @@ -103,12 +104,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 +127,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 +143,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 +151,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 +169,29 @@ 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 ty,_ = CicTypeChecker.type_of_aux' [] context s CicUniv.oblivion_ugraph in + "(let " ^ ppname b ^ " = " ^ pp ~in_type:false s context ^ " in " ^ + pp ~in_type t ((Some (b,Cic.Def (s,Some ty)))::context) ^ ")" + | C.Appl (he::tl) when in_type -> + 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.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 +199,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,16 +239,22 @@ 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 + if in_type then + "unit (* TOO POLYMORPHIC TYPE *)" + else ( + let needs_obj_magic = + (* BUG HERE: we should consider also the right parameters *) + match CicReduction.whd context ty with + Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t) + | _ -> false (* it can be a Rel, e.g. in *_rec *) + 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" @@ -276,13 +292,17 @@ 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) -> let rec aux argsno context = function Cic.Lambda (name,ty,bo) when argsno > 0 -> + let name = + match name with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name n -> Cic.Name (ppid n) in let args,res = aux (argsno - 1) (Some (name,Cic.Decl ty)::context) bo @@ -294,50 +314,56 @@ 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 x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"), body in - pattern ^ " -> " ^ body + pattern ^ " -> " ^ + if needs_obj_magic then + "Obj.magic (" ^ body ^ ")" + else + body ) connames_and_argsno_and_patterns)) ^ - ")\n")) + ")\n"))) | C.Fix (no, funs) -> - let names = - List.rev - (List.map - (function (name,_,ty,_) -> - Some (C.Name name,Cic.Decl ty)) funs) + let names,_ = + List.fold_left + (fun (types,len) (n,_,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in "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 Some (Cic.Name n,_) -> n | _ -> assert false) | C.CoFix (no,funs) -> - let names = - List.rev - (List.map - (function (name,ty,_) -> - Some (C.Name name,Cic.Decl ty)) funs) + let names,_ = + List.fold_left + (fun (types,len) (n,ty,_) -> + (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types, + len+1) + ) ([],0) funs in "\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 = @@ -345,7 +371,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 = @@ -354,7 +380,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) @@ -362,11 +388,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 = @@ -389,7 +415,10 @@ 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 _ when nparams <= 0 -> + let n = Cic.Name "unit (* EXISTENTIAL TYPE *)" in + args (nparams - 1) ((Some (n,Cic.Decl s))::context) t | `Sort _ -> let n = match n with @@ -407,6 +436,47 @@ let ppty current_module_uri = args ;; +exception DoNotExtract;; + +let pp_abstracted_ty current_module_uri = + let rec args context = + function + Cic.Lambda (n,s,t) -> + let n = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name n -> Cic.Name (String.uncapitalize n) + in + (match analyze_type context s with + `Statement + | `Type + | `Sort Cic.Prop -> + args ((Some (n,Cic.Decl s))::context) t + | `Sort _ -> + let n = + match n with + Cic.Anonymous -> Cic.Anonymous + | Cic.Name name -> Cic.Name ("'" ^ name) in + let abstr,res = + args ((Some (n,Cic.Decl s))::context) t + in + (match n with + Cic.Anonymous -> abstr + | Cic.Name name -> name::abstr), + res) + | ty -> + match analyze_type context ty with + ` Sort _ + | `Statement -> raise DoNotExtract + | `Type -> + (* BUG HERE: this can be a real System F type *) + let head = pp ~in_type:true current_module_uri ty context in + [],head + in + args +;; + + (* ppinductiveType (typename, inductive, arity, cons) *) (* pretty-prints a single inductive definition *) (* (typename, inductive, arity, cons) *) @@ -441,24 +511,26 @@ 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 -> "" | _ -> - let abstr,args = ppty current_module_uri 0 [] t1 in - let abstr = - let s = String.concat "," abstr in - if s = "" then "" else "(" ^ s ^ ") " - in - "type " ^ abstr ^ ppid name ^ " = " ^ String.concat "->" args ^ - "\n") + (try + let abstr,res = pp_abstracted_ty current_module_uri [] t1 in + let abstr = + let s = String.concat "," abstr in + if s = "" then "" else "(" ^ s ^ ") " + in + "type " ^ abstr ^ ppid name ^ " = " ^ res ^ "\n" + with + DoNotExtract -> "")) | C.Constant (name, None, ty, params, _) -> (match analyze_type [] ty with `Sort Cic.Prop @@ -469,8 +541,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) ^ @@ -485,12 +557,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 @@ -498,10 +571,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 ""