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.
Require Import HaskStrongTypes.
Require Import HaskStrong.
-(* Uniques *)
-Variable UniqSupply : Type. Extract Inlined Constant UniqSupply => "UniqSupply.UniqSupply".
-Variable Unique : Type. Extract Inlined Constant Unique => "Unique.Unique".
-Variable uniqFromSupply : UniqSupply -> Unique. Extract Inlined Constant uniqFromSupply => "UniqSupply.uniqFromSupply".
-Variable splitUniqSupply : UniqSupply -> UniqSupply * UniqSupply.
- Extract Inlined Constant splitUniqSupply => "UniqSupply.splitUniqSupply".
-
-Inductive UniqM {T:Type} : Type :=
- | uniqM : (UniqSupply -> ???(UniqSupply * T)) -> UniqM.
- Implicit Arguments UniqM [ ].
-
-Instance UniqMonad : Monad UniqM :=
-{ returnM := fun T (x:T) => uniqM (fun u => OK (u,x))
-; bindM := fun a b (x:UniqM a) (f:a->UniqM b) =>
- uniqM (fun u =>
- match x with
- | uniqM fa =>
- match fa u with
- | Error s => Error s
- | OK (u',va) => match f va with
- | uniqM fb => fb u'
- end
- end
- end)
-}.
-
-Definition getU : UniqM Unique :=
- uniqM (fun us => let (us1,us2) := splitUniqSupply us in OK (us1,(uniqFromSupply us2))).
-
-Notation "'bind' x = e ; f" := (@bindM _ _ _ _ e (fun x => f)) (x ident, at level 60, right associativity).
-Notation "'return' x" := (returnM x) (at level 100).
-Notation "'failM' x" := (uniqM (fun _ => Error x)) (at level 100).
-
Section HaskStrongToWeak.
Context (hetmet_brak : WeakExprVar).
| 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
; bind tbranches' = @typeToWeakType Γ _ tbranches ite
; bind escrut' = exprToWeakExpr χ escrut ite
; bind branches' =
- ((fix caseBranches (tree:Tree ??{scb : StrongCaseBranchWithVVs VV _ _ _ & Expr _ _ _ _ })
+ ((fix caseBranches (tree:Tree ??{sac : _ & { scb : StrongCaseBranchWithVVs VV _ _ _ sac & Expr _ _ _ _ } })
: UniqM (Tree ??(WeakAltCon*list WeakTypeVar*list WeakCoerVar*list WeakExprVar*WeakExpr)) :=
match tree with
| T_Leaf None => return []
- | T_Leaf (Some x) => let (scb,e) := x in
+ | T_Leaf (Some x) =>
+ let (sac,scb_e) := x in
+ let (scb,e) := scb_e in
let varstypes := vec2list (scbwv_varstypes scb) in
bind evars_ite = mfresh _ ite
; bind exprvars = seqM (map (fun vt:VV * HaskType _ ★
varstypes)
; let χ' := update_χ' χ exprvars in
bind e'' = exprToWeakExpr χ' e (snd evars_ite)
- ; return [(sac_altcon scb, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
+ ; return [(sac_altcon sac, vec2list (fst evars_ite), nil, (map (@snd _ _) exprvars), e'')]
| T_Branch b1 b2 => bind b1' = caseBranches b1
; bind b2' = caseBranches b2
; return (b1',,b2')
(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'))
match elrb as E in ELetRecBindings G D X L V
return InstantiatedTypeEnv (fun _ => WeakTypeVar) G -> UniqM (Tree ??(WeakExprVar * WeakExpr)) with
| ELR_nil _ _ _ _ => fun ite => return []
- | ELR_leaf _ _ ξ' cv v e => fun ite => bind t' = typeToWeakType (unlev (ξ' v)) ite
+ | ELR_leaf _ _ ξ' cv v t e => fun ite => bind t' = typeToWeakType t ite
; bind e' = exprToWeakExpr χ e ite
; bind v' = match χ v with Error s => failM s | OK y => return y end
; return [(v',e')]
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.