From 0fa422bfaf3931aacff958cb73d44ebfa4191f4a Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Thu, 23 Oct 2008 12:58:35 -0400 Subject: Fix nasty de Bruijn substitution bug; TcSum demo --- demo/prose | 4 ++++ demo/tcSum.ur | 9 +++++++++ demo/tcSum.urp | 2 ++ demo/tcSum.urs | 1 + 4 files changed, 16 insertions(+) create mode 100644 demo/tcSum.ur create mode 100644 demo/tcSum.urp create mode 100644 demo/tcSum.urs (limited to 'demo') diff --git a/demo/prose b/demo/prose index 8fedc557..19e9df0f 100644 --- a/demo/prose +++ b/demo/prose @@ -100,3 +100,7 @@ An unusual part of the third argument is the syntax [t1 ~ t2] within a

The general syntax for constant row types is [Name1 = t1, ..., NameN = tN], and there is a shorthand version [Name1, ..., NameN] for records of Units.

With sum defined, it is easy to make some sample calls. The form of the code for main does not make it apparent, but the compiler must "reverse engineer" the appropriate {Unit} from the {Type} available from the context at each call to sum.

+ +tcSum.urp + +

It's easy to adapt the last example to use type classes, such that we can sum the fields of records based on any numeric type.

diff --git a/demo/tcSum.ur b/demo/tcSum.ur new file mode 100644 index 00000000..53679116 --- /dev/null +++ b/demo/tcSum.ur @@ -0,0 +1,9 @@ +fun sum (t ::: Type) (_ : num t) (fs ::: {Unit}) (x : $(mapUT t fs)) = + foldUR [t] [fn _ => t] + (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] n acc => n + acc) + zero [fs] x + +fun main () = return + {[sum {A = 0, B = 1}]}
+ {[sum {C = 2.1, D = 3.2, E = 4.3}]} + diff --git a/demo/tcSum.urp b/demo/tcSum.urp new file mode 100644 index 00000000..8b36efc0 --- /dev/null +++ b/demo/tcSum.urp @@ -0,0 +1,2 @@ + +tcSum diff --git a/demo/tcSum.urs b/demo/tcSum.urs new file mode 100644 index 00000000..6ac44e0b --- /dev/null +++ b/demo/tcSum.urs @@ -0,0 +1 @@ +val main : unit -> transaction page -- cgit v1.2.3