-Fixpoint weakTypeToCoreType (wt:WeakType) : CoreType :=
- match wt with
- | WTyVarTy (weakTypeVar v _) => TyVarTy v
- | WAppTy (WAppTy WFunTyCon t1) t2 => FunTy (weakTypeToCoreType t1) (weakTypeToCoreType t2)
- | WAppTy t1 t2 => match (weakTypeToCoreType t1) with
- | TyConApp tc tys => TyConApp tc (app tys ((weakTypeToCoreType t2)::nil))
- | t1' => AppTy t1' (weakTypeToCoreType t2)
- end
- | WTyCon tc => TyConApp tc nil
- | WTyFunApp tf lt => TyConApp tf (map weakTypeToCoreType lt)
- | WClassP c lt => PredTy (ClassP c (map weakTypeToCoreType lt))
- | WIParam n ty => PredTy (IParam n (weakTypeToCoreType ty))
- | WForAllTy (weakTypeVar wtv _) t => ForAllTy wtv (weakTypeToCoreType t)
- | WFunTyCon => TyConApp ArrowTyCon nil
- | WCodeTy (weakTypeVar ec _) t => TyConApp ModalBoxTyCon ((TyVarTy ec)::(weakTypeToCoreType t)::nil)
- | WCoFunTy t1 t2 t3 => FunTy (PredTy (EqPred (weakTypeToCoreType t1) (weakTypeToCoreType t2)))
- (weakTypeToCoreType t3)
- end.
-
-Instance WeakTypeToString : ToString WeakType :=
- { toString := coreTypeToString ○ weakTypeToCoreType }.
+(* this is a trick to allow circular definitions, post-extraction *)
+Variable weakTypeToString : WeakType -> string.
+ Extract Inlined Constant weakTypeToString => "(coreTypeToString . weakTypeToCoreType)".
+Instance WeakTypeToString : ToString WeakType := { toString := weakTypeToString }.