- | None => coreExprToWeakExpr e1 >>= fun e1' =>
- match e2 with
- | CoreEType t =>
- coreTypeToWeakType t >>= fun t' =>
- OK (WETyApp e1' t')
- | _ => coreExprToWeakExpr e2
- >>= fun e2' => OK (WEApp e1' e2')
- end
- end
- end
+ | None =>
+ (*
+ if isKappa e1
+ then match e2 with
+ | CoreELam v e => match coreVarToWeakVar' v with
+ | OK (WExprVar ev) =>
+ coreExprToWeakExpr e >>= fun e' =>
+ OK (WEKappa ev e')
+ | _ => Error "bogus"
+ end
+ | _ => Error "bogus"
+ end
+ else if isKappaApp e1
+ then match e1 with
+ | (CoreEApp (CoreEApp (CoreEApp (CoreEApp _ _) _) _) e1') =>
+ coreExprToWeakExpr e1' >>= fun e1'' =>
+ coreExprToWeakExpr e2 >>= fun e2'' =>
+ OK (WEKappaApp e1'' e2'')
+ | _ => Error "bogus"
+ end
+ else
+ *)
+ coreExprToWeakExpr e1 >>= fun e1' =>
+ match e2 with
+ | CoreEType t =>
+ coreTypeToWeakType t >>= fun t' =>
+ OK (WETyApp e1' t')
+ | _ => coreExprToWeakExpr e2
+ >>= fun e2' => OK (WEApp e1' e2')
+ end
+ end
+ end