MinMLToMinHaskell

Translation from MinML (unencapsulated effects) to MiniHaskell (monadic effects). Uses third-order coverage checking.

MiniHaskell

%sort tp %.
%term unit tp %.
%term arr %pi tp %-> tp %-> tp %.
%term plus %pi tp %-> tp %-> tp %.
%term circ %pi tp %-> tp %.
%sort conc %.
%term true %pi tp %-> conc %.
%term lax %pi tp %-> conc %.
%sort | {_ conc} %.
%prec %prefix 0 | %.
%term <> | true unit %.
%term lam %pi (%pi (| true A) %-> (| true B)) %-> (| true (arr A B)) %.
%term app %pi (| true (arr A B)) %-> (| true A) %-> (| true B) %.
%term inl %pi (| true A) %-> (| true (plus A B)) %.
%term inr %pi (| true B) %-> (| true (plus A B)) %.
%term case
  %pi (| true (plus A B))
  %-> (%pi (| true A) %-> (| J))
  %-> (%pi (| true B) %-> (| J))
  %-> (| J) %.
%term comp %pi (| lax A) %-> (| true (circ A)) %.
%term return %pi (| true A) %-> (| lax A) %.
%term let %pi (| true (circ A)) %-> (%pi (| true A) %-> (| lax C)) %-> (| lax C) %.
%term print %pi (| lax C) %-> (| lax C) %.
%block trueb [A _] {x | true A}%.
%worlds (trueb) (| _) %.

MinML

%sort mtp %.
%term munit mtp %.
%term marr %pi mtp %-> mtp %-> mtp %.
%term mplus %pi mtp %-> mtp %-> mtp %.
%sort mtrue {_ mtp} %.
%term m<> mtrue munit %.
%term mlam %pi (%pi (mtrue A) %-> (mtrue B)) %-> (mtrue (marr A B)) %.
%term mapp %pi (mtrue (marr A B)) %-> (mtrue A) %-> (mtrue B) %.
%term minl %pi (mtrue A) %-> (mtrue (mplus A B)) %.
%term minr %pi (mtrue B) %-> (mtrue (mplus A B)) %.
%term mcase
  %pi (mtrue (mplus A B))
  %-> (%pi (mtrue A) %-> (mtrue C))
  %-> (%pi (mtrue B) %-> (mtrue C))
  %-> (mtrue C) %.
%term mprint %pi (mtrue C) %-> (mtrue C) %.

Translation

%sort tptrans {_ mtp} {_ tp} %.
%mode tptrans %in %out %.
%term tptrans/unit tptrans munit unit %.
%term tptrans/arr %pi (tptrans (marr A B) (arr A' (circ B'))) %<- (tptrans A A') %<- (tptrans B B') %.
%term tptrans/plus %pi (tptrans (mplus A B) (plus A' B')) %<- (tptrans A A') %<- (tptrans B B') %.
%worlds () (tptrans _ _) %.
%total A (tptrans A _) %.
%unique tptrans %in %out %.
%sort id-tp {_ tp} {_ tp} %.
%term id-tp/refl id-tp A A %.
%sort trueresp {_ | true A} {_ id-tp A A'} {_ | true A'} %.
%mode trueresp %in %in %out %.
%term _ trueresp E id-tp/refl E %.
%worlds (trueb) (trueresp _ _ _) %.
%total {} (trueresp _ _ _) %.
%sort laxresp {_ | lax A} {_ id-tp A A'} {_ | lax A'} %.
%mode laxresp %in %in %out %.
%term _ laxresp E id-tp/refl E %.
%worlds (trueb) (laxresp _ _ _) %.
%total {} (laxresp _ _ _) %.
%sort can-tptrans {A} {_ tptrans A A'} %.
%mode can-tptrans %in %out %.
%worlds () (can-tptrans _ _) %.
%total A (can-tptrans A _) %.
%sort tptrans-unique {_ tptrans A A'} {_ tptrans A A''} {_ id-tp A' A''} %.
%mode tptrans-unique %in %in %out %.
%worlds () (tptrans-unique _ _ _) %.
%total D (tptrans-unique D _ _) %.
%sort trans {_ mtrue A} {_ tptrans A A'} {_ | lax A'} %.
%mode trans %in %in %out %.
%term _ trans m<> tptrans/unit (return <>) %.
%term _
  %pi (trans (mlam E) (tptrans/arr (%the (tptrans B B') DB) DA) (return (lam ([x] comp (E' x)))))
  %<- ({x mtrue A} {x' | true A'} {_ {A'' _} {DA'' tptrans A A''} {Did id-tp A' A''} {E'' | lax A''}
  %pi (trans x DA'' E'')
  %<- (tptrans-unique DA DA'' Did)
  %<- (laxresp (return x') Did E'')} trans (E x) DB (E' x')) %.
%term _
  %pi (trans (mapp (%the (mtrue (marr A B)) E1) E2) DB (let (comp E1') ([x1] let (comp E2') ([x2] let (app x1 x2) ([r] return r)))))
  %<- (can-tptrans A DA)
  %<- (trans E1 (tptrans/arr DB DA) E1')
  %<- (trans E2 DA E2') %.
%term _
  %pi (trans (minl E) (tptrans/plus DB DA) (let (comp E') ([x] return (inl x))))
  %<- (trans E DA E') %.
%term _
  %pi (trans (minr E) (tptrans/plus DB DA) (let (comp E') ([x] return (inr x))))
  %<- (trans E DB E') %.
%term _
  %pi (trans (mcase (%the (mtrue (mplus A B)) E) E1 E2) DC (let (comp E') ([x] case x E1' E2')))
  %<- (can-tptrans A DA)
  %<- (can-tptrans B DB)
  %<- (trans E (tptrans/plus DB DA) E')
  %<- ({x mtrue A} {x' | true A'} {_ {A'' _} {DA'' tptrans A A''} {Did id-tp A' A''} {E'' | lax A''}
  %pi (trans x DA'' E'')
  %<- (tptrans-unique DA DA'' Did)
  %<- (laxresp (return x') Did E'')} trans (E1 x) DC (E1' x'))
  %<- ({x mtrue B} {x' | true B'} {_ {B'' _} {DB'' tptrans B B''} {Did id-tp B' B''} {E'' | lax B''}
  %pi (trans x DB'' E'')
  %<- (tptrans-unique DB DB'' Did)
  %<- (laxresp (return x') Did E'')} trans (E2 x) DC (E2' x')) %.
%term _ %pi (trans (mprint E) DC (print E')) %<- (trans E DC E') %.
%block transb [A _] [A' _] [DA tptrans A A'] {x mtrue A} {x' | true A'} {_ {A'' _} {DA'' tptrans A A''} {Did id-tp A' A''} {E'' | lax A''}
  %pi (trans x DA'' E'')
  %<- (tptrans-unique DA DA'' Did)
  %<- (laxresp (return x') Did E'')}%.
%worlds (transb) (trans _ _ _) %.
%total E (trans E _ _) %.