From 262d2831a751e4fb4c3eef6fbfaaf7146b793aac Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 30 Aug 2007 16:24:31 +0000 Subject: [PATCH] bugfix in computation of src and tgt for coercions with arity > 0 --- .../components/library/librarySync.ml | 23 ++++++++++--------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/helm/software/components/library/librarySync.ml b/helm/software/components/library/librarySync.ml index cbc45e6a9..5897d62ba 100644 --- a/helm/software/components/library/librarySync.ml +++ b/helm/software/components/library/librarySync.ml @@ -259,18 +259,19 @@ let add_coercion ~add_composites refinement_toolkit uri arity saturations in let src_carr, tgt_carr = let get_classes arity saturations l = - let rec aux target = function - 0,0,tgt::src::_ when target = None -> src,Some (`Class tgt) - | 0,0,src::_ when target <> None -> src,target - | 0,saturations,tgt::tl when target = None -> - aux (Some (`Class tgt)) (0,saturations,tl) - | 0,saturations,_::tl -> - aux target (0,saturations - 1,tl) - | arity,saturations,_::tl -> - aux (Some `Funclass) (arity - 1, saturations, tl) - | _,_,_ -> assert false + (* this is the ackerman's function revisited *) + let rec aux = function + 0,0,None,tgt::src::_ -> src,Some (`Class tgt) + | 0,0,target,src::_ -> src,target + | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl) + | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl) + | arity,saturations,None,_::tl -> + aux (arity, saturations, Some `Funclass, tl) + | arity,saturations,target,_::tl -> + aux (arity - 1, saturations, target, tl) + | _ -> assert false in - aux None (arity,saturations,List.rev l) + aux (arity,saturations,None,List.rev l) in let types = spine2list coer_ty in let src,tgt = get_classes arity saturations types in -- 2.39.2