X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=c595c6d7dfc03bb9564908be5293994a5249215d;hb=ffdd3ddd6ce10a5fa0729ab407647bd46c44b9d8;hp=813e65c298bf9c5c9281597088dadf655b7db3e6;hpb=aa8e74a3f9b16a2fc2521b58a2413534bfb2641e;p=helm.git diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 813e65c29..c595c6d7d 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -28,16 +28,24 @@ exception CicExportationInternalError;; exception NotEnoughElements;; +(* *) + +let is_mcu_type u = + UriManager.eq (UriManager.uri_of_string + "cic:/matita/freescale/opcode/mcu_type.ind") u +;; + (* Utility functions *) let analyze_term context t = match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph)with - Cic.Sort _ -> `Type + | Cic.Sort _ -> `Type + | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize | ty -> match fst (CicTypeChecker.type_of_aux' [] context ty CicUniv.oblivion_ugraph) with - Cic.Sort Cic.Prop -> `Proof + | Cic.Sort Cic.Prop -> `Proof | _ -> `Term ;; @@ -45,12 +53,12 @@ let analyze_type context t = let rec aux = function Cic.Sort s -> `Sort s - | Cic.Prod (_,_,t) - | Cic.Lambda (_,_,t) -> aux t + | Cic.MutInd (u,0,_) when is_mcu_type u -> `Optimize + | Cic.Prod (_,_,t) -> aux t | _ -> `SomethingElse in match aux t with - `Sort _ as res -> res + `Sort _ | `Optimize as res -> res | `SomethingElse -> match fst(CicTypeChecker.type_of_aux' [] context t CicUniv.oblivion_ugraph) @@ -63,7 +71,9 @@ let ppid = let reserved = [ "to"; "mod"; - "val" + "val"; + "in"; + "function" ] in function n -> @@ -103,6 +113,18 @@ let qualified_name_of_uri current_module_uri ?(capitalize=false) uri = String.capitalize filename ^ "." ^ name ;; +let current_go_up = ref "(.!(";; +let at_level2 f x = + try + current_go_up := "(.~("; + let rc = f x in + current_go_up := "(.!("; + rc + with exn -> + current_go_up := "(.!("; + raise exn +;; + let pp current_module_uri ?metasenv ~in_type = let rec pp ~in_type t context = let module C = Cic in @@ -160,7 +182,7 @@ let rec pp ~in_type t context = | C.Set -> "Set" | C.Type _ -> "Type" (*| C.Type u -> ("Type" ^ CicUniv.string_of_universe u)*) - | C.CProp -> "CProp" + | C.CProp _ -> "CProp" ) | C.Implicit (Some `Hole) -> "%" | C.Implicit _ -> "?" @@ -178,33 +200,43 @@ let rec pp ~in_type t context = (match analyze_type context s with `Sort _ | `Statement -> pp ~in_type t ((Some (b,Cic.Decl s))::context) + | `Optimize -> prerr_endline "XXX lambda";assert false | `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 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.LetIn (b,s,ty,t) -> + (match analyze_term context s with + | `Type + | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) + | `Optimize + | `Term -> + "(let " ^ ppname b ^ (*" : " ^ pp ~in_type:true ty context ^*) + " = " ^ pp ~in_type:false s context ^ " in " ^ + pp ~in_type t ((Some (b,Cic.Def (s,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 ~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) -> let nparams = - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (_,_,nparams,_) -> nparams | _ -> assert false in let hes = pp ~in_type he context in - let stl = String.concat "," (clean_args nparams context tl) in + let stl = String.concat "," (clean_args_for_constr nparams context tl) in "(" ^ hes ^ (if stl = "" then "" else "(" ^ stl ^ ")") ^ ")" | C.Appl li -> - "(" ^ String.concat " " (clean_args 0 context li) ^ ")" + "(" ^ String.concat " " (clean_args context li) ^ ")" | C.Const (uri,exp_named_subst) -> qualified_name_of_uri current_module_uri uri ^ pp_exp_named_subst exp_named_subst context | C.MutInd (uri,n,exp_named_subst) -> (try - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (dl,_,_,_) -> let (name,_,_,_) = get_nth dl (n+1) in qualified_name_of_uri current_module_uri @@ -218,7 +250,7 @@ let rec pp ~in_type t context = ) | C.MutConstruct (uri,n1,n2,exp_named_subst) -> (try - match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (dl,_,_,_) -> let _,_,_,cons = get_nth dl (n1+1) in let id,_ = get_nth cons n2 in @@ -237,12 +269,13 @@ let rec pp ~in_type t context = if in_type then "unit (* TOO POLYMORPHIC TYPE *)" else ( - let needs_obj_magic = - (* BUG HERE: we should consider also the right parameters *) + let rec needs_obj_magic ty = match CicReduction.whd context ty with - Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t) + | Cic.Lambda (_,_,(Cic.Lambda(_,_,_) as t)) -> needs_obj_magic t + | Cic.Lambda (_,_,t) -> not (DoubleTypeInference.does_not_occur 1 t) | _ -> false (* it can be a Rel, e.g. in *_rec *) in + let needs_obj_magic = needs_obj_magic ty in (match analyze_term context te with `Type -> assert false | `Proof -> @@ -251,13 +284,15 @@ let rec pp ~in_type t context = | [he] -> pp ~in_type:false he context (* singleton elimination *) | _ -> assert false) + | `Optimize | `Term -> if patterns = [] then "assert false" else - (let connames_and_argsno = - (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph uri) with + (let connames_and_argsno, go_up, go_pu, go_down, go_nwod = + (match fst(CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with C.InductiveDefinition (dl,_,paramsno,_) -> let (_,_,_,cons) = get_nth dl (n1+1) in + let rc = List.map (fun (id,ty) -> (* this is just an approximation since we do not have @@ -275,6 +310,9 @@ let rec pp ~in_type t context = (UriManager.buri_of_uri uri ^ "/" ^ id ^ ".con")), count_prods paramsno ty ) cons + in + if not (is_mcu_type uri) then rc, "","","","" + else rc, !current_go_up, "))", "( .< (", " ) >.)" | _ -> raise CicExportationInternalError ) in @@ -287,6 +325,7 @@ let rec pp ~in_type t context = in combine (connames_and_argsno,patterns) in + go_up ^ "\n(match " ^ pp ~in_type:false te context ^ " with \n " ^ (String.concat "\n | " (List.map @@ -303,7 +342,8 @@ let rec pp ~in_type t context = bo in (match analyze_type context ty with - `Statement + | `Optimize -> prerr_endline "XXX contructor with l2 arg"; assert false + | `Statement | `Sort _ -> args,res | `Type -> (match name with @@ -322,19 +362,20 @@ let rec pp ~in_type t context = x ^ (if sargs = "" then "" else "(" ^ sargs^ ")"), body in - pattern ^ " -> " ^ - if needs_obj_magic then + pattern ^ " -> " ^ go_down ^ + (if needs_obj_magic then "Obj.magic (" ^ body ^ ")" else - body + body) ^ go_nwod ) connames_and_argsno_and_patterns)) ^ - ")\n"))) + ")\n"^go_pu))) | 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 @@ -346,11 +387,12 @@ let rec pp ~in_type t context = 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 @@ -367,21 +409,43 @@ and pp_exp_named_subst exp_named_subst context = (function (uri,t) -> UriManager.name_of_uri uri ^ " \\Assign " ^ pp ~in_type:false t context) exp_named_subst ) ^ "]" -and clean_args nparams context = +and clean_args_for_constr nparams context = let nparams = ref nparams in HExtlib.filter_map (function t -> decr nparams; match analyze_term context t with `Term when !nparams < 0 -> Some (pp ~in_type:false t context) + | `Optimize | `Term | `Type | `Proof -> None) +and clean_args context = + function + | [] | [_] -> assert false + | he::arg1::tl as l -> + let head_arg1, rest = + match analyze_term context arg1 with + | `Optimize -> + !current_go_up :: pp ~in_type:false he context :: + pp ~in_type:false arg1 context :: ["))"], tl + | _ -> [], l + in + head_arg1 @ + HExtlib.filter_map + (function t -> + match analyze_term context t with + | `Term -> Some (pp ~in_type:false t context) + | `Optimize -> + prerr_endline "XXX function taking twice (or not as first) a l2 term"; assert false + | `Type + | `Proof -> None) rest and clean_args_for_ty context = HExtlib.filter_map (function t -> match analyze_term context t with `Type -> Some (pp ~in_type:true t context) + | `Optimize -> None | `Proof -> None | `Term -> None) in @@ -400,7 +464,8 @@ let ppty current_module_uri = | Cic.Name n -> Cic.Name (String.uncapitalize n) in (match analyze_type context s with - `Statement + | `Optimize + | `Statement | `Sort Cic.Prop -> args (nparams - 1) ((Some (n,Cic.Decl s))::context) t | `Type when nparams > 0 -> @@ -409,6 +474,9 @@ let ppty current_module_uri = let abstr,args = args (nparams - 1) ((Some (n,Cic.Decl s))::context) t in 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 @@ -426,6 +494,50 @@ 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 + | `Optimize + | `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 + | `Optimize -> + prerr_endline "XXX abstracted l2 ty"; assert false + | `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) *) @@ -433,6 +545,7 @@ let ppinductiveType current_module_uri nparams (typename, inductive, arity, cons = match analyze_type [] arity with `Sort Cic.Prop -> "" + | `Optimize | `Statement | `Type -> assert false | `Sort _ -> @@ -464,23 +577,49 @@ let ppobj current_module_uri obj = match obj with C.Constant (name, Some t1, t2, params, _) -> (match analyze_type [] t2 with - `Sort Cic.Prop + | `Sort Cic.Prop | `Statement -> "" - | `Type -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n" + | `Optimize + | `Type -> + (match t1 with + | Cic.Lambda (Cic.Name arg, s, t) -> + (match analyze_type [] s with + | `Optimize -> + + "let " ^ ppid name ^ "__1 = function " ^ ppid arg + ^ " -> .< " ^ + at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)] + ^ " >. ;;\n" + ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit list*unit list) list);;\n" + ^ "let " ^ ppid name ^ " = function " ^ ppid arg + ^ " -> (try ignore (List.assoc "^ppid arg^" (Obj.magic !"^ppid name + ^"__2)) with Not_found -> "^ppid name^"__2 := (Obj.magic (" + ^ ppid arg^",.! ("^ppid name^"__1 "^ppid arg^")))::!" + ^ppid name^"__2); .< List.assoc "^ppid arg^" (Obj.magic (!" + ^ppid name^"__2)) >.\n;;\n" + ^" let xxx = prerr_endline \""^ppid name^"\"; .!("^ppid + name^" Matita_freescale_opcode.HCS08)" + | _ -> + "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n") + | _ -> "let " ^ ppid name ^ " =\n" ^ pp ~in_type:false t1 [] ^ "\n") | `Sort _ -> match analyze_type [] t1 with `Sort Cic.Prop -> "" + | `Optimize -> prerr_endline "XXX aliasing l2 type"; assert false | _ -> - 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 + | `Optimize -> prerr_endline "XXX axiom l2"; assert false | `Statement -> "" | `Sort _ -> "type " ^ ppid name ^ "\n" | `Type -> "let " ^ ppid name ^ " = assert false\n") @@ -507,14 +646,16 @@ let ppobj current_module_uri obj = pp ~in_type:true ~metasenv:conjectures at name_context ^ " ", context_entry::name_context - | Some (n,C.Def (at,None)) -> + | Some (n,C.Def (at,aty)) -> (separate i) ^ - ppname n ^ ":= " ^ pp ~in_type:false + ppname n ^ ":" ^ + pp ~in_type:true ~metasenv:conjectures + aty name_context ^ + ":= " ^ pp ~in_type:false ~metasenv:conjectures at name_context ^ " ", context_entry::name_context | None -> - (separate i) ^ "_ :? _ ", context_entry::name_context - | _ -> assert false) + (separate i) ^ "_ :? _ ", context_entry::name_context) ) context ("",[]) in conjectures' ^ " |- " ^ "?" ^ (string_of_int n) ^ ": " ^