this patch is a shit, the part that fixes the heuristic about Obj.magic should be...

diff --git a/helm/software/components/cic_exportation/cicExportation.ml b/helm/software/components/cic_exportation/cicExportation.ml
index 83b775eaea26f6ae6036463b53abc6cb4b8ade53..69c949c6325044044414012e62094805ffd7fa96 100644 (file)
--- 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")