Require Import Coq.Lists.List.
Require Import Coq.Init.Specif.
Require Import HaskKinds.
-Require Import HaskLiteralsAndTyCons.
+Require Import HaskLiterals.
+Require Import HaskTyCons.
Require Import HaskWeakTypes.
Require Import HaskWeakVars.
Require Import HaskWeak.
| WTyVarTy ec => return WCodeTy ec t2'
| _ => failM "impossible"
end
- | TyFunApp tfc tls => bind tls' = rawHaskTypeListToWeakType tls
+ | TyFunApp tfc _ _ tls => bind tls' = rawHaskTypeListToWeakType tls
; return WTyFunApp tfc tls'
end
with rawHaskTypeListToWeakType {κ}(rht:RawHaskTypeList κ) : UniqM (list WeakType) :=
-> UniqM WeakExpr :=
match exp as E in @Expr _ _ G D X L return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM WeakExpr with
| EVar Γ' _ ξ' ev => fun ite => match χ ev with OK v => return WEVar v | Error s => failM s end
- | EGlobal Γ' _ ξ' t wev => fun ite => return WEVar wev
+ | EGlobal Γ' _ ξ' g v lev => fun ite => bind tv' = mapM (ilist_to_list (ilmap (fun κ x => typeToWeakType x ite) v))
+ ; return (fold_left (fun x y => WETyApp x y) tv' (WEVar g))
| ELam Γ' _ _ tv _ _ cv e => fun ite => bind tv' = typeToWeakType tv ite
; bind ev' = mkWeakExprVar tv'
; bind e' = exprToWeakExpr (update_χ χ cv ev') e ite
(fun _ => UniqM WeakType) _ (fun _ t => typeToWeakType t ite) atypes))
; return WECase vscrut' escrut' tbranches' tc tys branches'
- | ELetRec _ _ _ _ _ vars elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
+ | ELetRec _ _ _ _ _ vars disti elrb e => fun ite => bind vars' = seqM (map (fun vt:VV * HaskType _ ★
=> bind tleaf = typeToWeakType (snd vt) ite
; bind v' = mkWeakExprVar tleaf
; return ((fst vt),v'))
Fixpoint strongExprToWeakExpr (us:UniqSupply){Γ}{Δ}{ξ}{τ}(exp:@Expr _ eqVV Γ Δ ξ τ)
(ite:InstantiatedTypeEnv (fun _ => WeakTypeVar) Γ)
: ???WeakExpr :=
- match exprToWeakExpr (fun v => Error ("unbound variable " +++ v)) exp ite with
+ match exprToWeakExpr (fun v => Error ("unbound variable " +++ toString v)) exp ite with
uniqM f => f us >>= fun x => OK (snd x)
end.
-End HaskStrongToWeak.
\ No newline at end of file
+End HaskStrongToWeak.