From c5455f79a56b00af66a980cf0469290fa9c62f96 Mon Sep 17 00:00:00 2001 From: Adam Megacz Date: Wed, 11 May 2011 19:32:34 -0700 Subject: [PATCH] HaskFlattener: represent first-order abstraction using GArrows --- src/HaskFlattener.v | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/HaskFlattener.v b/src/HaskFlattener.v index 47315bb..cd5bd57 100644 --- a/src/HaskFlattener.v +++ b/src/HaskFlattener.v @@ -204,8 +204,10 @@ Section HaskFlattener. Definition ga_mk_tree {Γ}(ec:HaskType Γ ECKind)(tr:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := fun TV ite => ga_mk_tree' (ec TV ite) (mapOptionTree (fun x => x TV ite) tr). - Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind )(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ := - gaTy TV ec (ga_mk_tree' ec ant) (ga_mk_tree' ec suc). + Definition ga_mk_raw {TV}(ec:RawHaskType TV ECKind)(ant suc:Tree ??(RawHaskType TV ★)) : RawHaskType TV ★ := + gaTy TV ec + (ga_mk_tree' ec (ant,,(mapOptionTreeAndFlatten (unleaves ○ take_arg_types) suc))) + (ga_mk_tree' ec ( mapOptionTree drop_arg_types suc) ). Definition ga_mk {Γ}(ec:HaskType Γ ECKind )(ant suc:Tree ??(HaskType Γ ★)) : HaskType Γ ★ := fun TV ite => ga_mk_raw (ec TV ite) (mapOptionTree (fun x => x TV ite) ant) (mapOptionTree (fun x => x TV ite) suc). -- 1.7.10.4