# HG changeset patch # User Adam Chlipala # Date 1354121146 18000 # Node ID 373e2c3f03b2b64fad87f0f7f9a34694cbbd1da1 # Parent 36428d853c975e4a409f6b10c4856538dc30bc6d Rename Basis.exp to Basis.pow, to avoid confusion with 'expression'; add a test case for it diff -r 36428d853c97 -r 373e2c3f03b2 lib/ur/basis.urs --- a/lib/ur/basis.urs Wed Nov 28 11:41:54 2012 -0500 +++ b/lib/ur/basis.urs Wed Nov 28 11:45:46 2012 -0500 @@ -42,7 +42,7 @@ val times : t ::: Type -> num t -> t -> t -> t val divide : t ::: Type -> num t -> t -> t -> t val mod : t ::: Type -> num t -> t -> t -> t -val exp : t ::: Type -> num t -> t -> t -> t +val pow : t ::: Type -> num t -> t -> t -> t val num_int : num int val num_float : num float diff -r 36428d853c97 -r 373e2c3f03b2 src/monoize.sml --- a/src/monoize.sml Wed Nov 28 11:41:54 2012 -0500 +++ b/src/monoize.sml Wed Nov 28 11:45:46 2012 -0500 @@ -192,7 +192,7 @@ ("Times", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), ("Div", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), ("Mod", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), - ("Exp", (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], + ("Pow", (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc) end | L.CApp ((L.CFfi ("Basis", "ord"), _), t) => @@ -793,7 +793,7 @@ ("Times", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), ("Div", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), ("Mod", (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), - ("Exp", (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc) + ("Pow", (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc) fun numEx (t, zero, neg, plus, minus, times, dv, md, ex) = ((L'.ERecord [("Zero", (L'.EPrim zero, loc), t), ("Neg", neg, (L'.TFun (t, t), loc)), @@ -802,7 +802,7 @@ ("Times", times, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), ("Div", dv, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), ("Mod", md, (L'.TFun (t, (L'.TFun (t, t), loc)), loc)), - ("Exp", ex, (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc), fm) + ("Pow", ex, (L'.TFun (t, (L'.TFun (t, t), loc)), loc))], loc), fm) fun ordTy t = (L'.TRecord [("Lt", (L'.TFun (t, (L'.TFun (t, (L'.TFfi ("Basis", "bool"), loc)), loc)), loc)), @@ -1032,12 +1032,12 @@ ((L'.EAbs ("r", numTy t, (L'.TFun (t, (L'.TFun (t, t), loc)), loc), (L'.EField ((L'.ERel 0, loc), "Mod"), loc)), loc), fm) end - | L.ECApp ((L.EFfi ("Basis", "exp"), _), t) => + | L.ECApp ((L.EFfi ("Basis", "pow"), _), t) => let val t = monoType env t in ((L'.EAbs ("r", numTy t, (L'.TFun (t, (L'.TFun (t, t), loc)), loc), - (L'.EField ((L'.ERel 0, loc), "Exp"), loc)), loc), fm) + (L'.EField ((L'.ERel 0, loc), "Pow"), loc)), loc), fm) end | L.EFfi ("Basis", "num_int") => let diff -r 36428d853c97 -r 373e2c3f03b2 tests/pow.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/tests/pow.ur Wed Nov 28 11:45:46 2012 -0500 @@ -0,0 +1,4 @@ +fun main () : transaction page = return +
  • 2^4 = {[pow 2 4]}
  • +
  • 3.4^5.6 = {[pow 3.4 5.6]}
  • +