correction des transformations, toujours pas de Duse apres applatissement

src/core/transform.ml

@@ -35,7 +35,7 @@ let apply f x = f.all x
 let clear f = f.clear ()
 
 let memo f tag h x =
-  try Hashtbl.find h (tag x:int)
+  try Hashtbl.find h (tag x)
   with Not_found ->
     let r = f x in
     Hashtbl.add h (tag x) r;
@@ -66,7 +66,7 @@ let fold_map_up ?clear f_fold v_empty =
       | Some (decls,ctxt2) -> 
           try 
             let ecdone = Hashtbl.find memo_t ctxt2.ctxt_tag in
-            rewind ecdone todo
+            rewind ecdone ((decls,ctxt)::todo)
           with Not_found -> f ((decls,ctxt)::todo) ctxt2 
   in
   t (f []) clear (fun () -> Hashtbl.clear memo_t)

src/main.ml

@@ -58,6 +58,8 @@ let rec report fmt = function
       fprintf fmt "syntax error"
   | Typing.Error e ->
       Typing.report fmt e
+  | Theory.Context.UnknownIdent i ->
+      fprintf fmt "anomaly: unknownident %s" i.Ident.id_short
   | e ->
       fprintf fmt "anomaly: %s" (Printexc.to_string e)
 

src/transform/simplify_recursive_definition.ml

@@ -146,4 +146,9 @@ let elt d =
         List.map (fun e -> create_type (List.map (Hid.find mem) e)) l
     | Dclone _ | Duse _ -> [d]
 
+let elt d = 
+  let r = elt d in
+(*  Format.printf "srd : %a -> %a@\n" Pretty.print_decl d Pretty.print_decl_list r;*)
+  r
+
 let t = Transform.elt elt