X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_exportation%2FcicExportation.ml;h=c595c6d7dfc03bb9564908be5293994a5249215d;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;hp=dd3be75721a55eb7f18705b89e586b5132945877;hpb=cc23f034c9419186602d9250456241f2eba90d7c;p=helm.git diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index dd3be7572..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,11 +53,12 @@ let analyze_type context t = let rec aux = function Cic.Sort s -> `Sort s + | 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) @@ -104,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 @@ -161,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 _ -> "?" @@ -179,15 +200,17 @@ 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,ty,t) -> (match analyze_term context s with - `Type + | `Type | `Proof -> pp ~in_type t ((Some (b,Cic.Def (s,ty)))::context) + | `Optimize | `Term -> - "(let " ^ ppname b ^ " : " ^ pp ~in_type:true ty context ^ + "(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 -> @@ -200,20 +223,20 @@ let rec pp ~in_type t context = (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 @@ -227,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 @@ -246,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 -> @@ -260,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 @@ -284,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 @@ -296,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 @@ -312,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 @@ -331,13 +362,13 @@ 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.fold_left @@ -378,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 @@ -411,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 -> @@ -452,7 +506,8 @@ let pp_abstracted_ty current_module_uri = | Cic.Name n -> Cic.Name (String.uncapitalize n) in (match analyze_type context s with - `Statement + | `Optimize + | `Statement | `Type | `Sort Cic.Prop -> args ((Some (n,Cic.Decl s))::context) t @@ -470,7 +525,9 @@ let pp_abstracted_ty current_module_uri = res) | ty -> match analyze_type context ty with - ` Sort _ + | `Optimize -> + prerr_endline "XXX abstracted l2 ty"; assert false + | `Sort _ | `Statement -> raise DoNotExtract | `Type -> (* BUG HERE: this can be a real System F type *) @@ -488,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 _ -> @@ -519,12 +577,35 @@ 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 | _ -> (try let abstr,res = pp_abstracted_ty current_module_uri [] t1 in @@ -538,6 +619,7 @@ let ppobj current_module_uri obj = | 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")