From 0dfcbb8be78db7bee20f7ac8c909179ccffbaa6c Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 25 Mar 2008 15:37:01 +0000 Subject: [PATCH] this patch is a shit, the part that fixes the heuristic about Obj.magic should be really adopted, the rest is metaocaml specific --- .../cic_exportation/cicExportation.ml | 43 +++++++++++++------ 1 file changed, 30 insertions(+), 13 deletions(-) diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml index 83b775eae..69c949c63 100644 --- a/helm/software/components/cic_exportation/cicExportation.ml +++ b/helm/software/components/cic_exportation/cicExportation.ml @@ -113,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 @@ -194,9 +206,9 @@ let rec pp ~in_type t context = pp ~in_type t ((Some (b,Cic.Decl s))::context) ^ ")") | C.LetIn (b,s,ty,t) -> (match analyze_term context s with - | `Optimize -> prerr_endline "XXX letin";assert false | `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 " ^ @@ -257,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 -> @@ -299,7 +312,7 @@ let rec pp ~in_type t context = ) cons in if not (is_mcu_type uri) then rc, "","","","" - else rc, "(.~(", "))", "( .< (", " ) >.)" + else rc, !current_go_up, "))", "( .< (", " ) >.)" | _ -> raise CicExportationInternalError ) in @@ -414,7 +427,7 @@ and clean_args context = let head_arg1, rest = match analyze_term context arg1 with | `Optimize -> - "(.~(" :: pp ~in_type:false he context :: + !current_go_up :: pp ~in_type:false he context :: pp ~in_type:false arg1 context :: ["))"], tl | _ -> [], l in @@ -564,24 +577,28 @@ let ppobj current_module_uri obj = match obj with C.Constant (name, Some t1, t2, params, _) -> (match analyze_type [] t2 with - | `Optimize -> prerr_endline "XXX definition of an l2 term"; assert false | `Sort Cic.Prop | `Statement -> "" + | `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 - ^ " -> .< " ^ pp ~in_type:false t [Some (Cic.Name arg, Cic.Decl s)] + ^ " -> .< " ^ + at_level2 (pp ~in_type:false t) [Some (Cic.Name arg, Cic.Decl s)] ^ " >. ;;\n" - ^ "let " ^ ppid name ^ "__2 = ref ([] : (unit*unit) list);;\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 := (" - ^ ppid arg^",Obj.magic (.! ("^ppid name^"__1 "^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" + ^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") -- 2.39.2