# HG changeset patch # User Adam Chlipala # Date 1224784992 14400 # Node ID ad7e854a518c0a4d5f73e23b0a164f905da71566 # Parent e0e9e9eca1cbd5414f1d45ccbea61309695fc9c7 Metaform demos, minus prose diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform.ur Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,28 @@ +functor Make (M : sig + con fs :: {Unit} + val names : $(mapUT string fs) + end) = struct + + fun handler values = return + {foldURX2 [string] [string] [body] + (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name value => +
  • {[name]} = {[value]}
    • +     ) + [M.fs] M.names values} +     + + fun main () = return +
    + {foldUR [string] [fn cols :: {Unit} => xml form [] (mapUT string cols)] + (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] name + (acc : xml form [] (mapUT string rest)) => +
  • {[name]}:
    • + {useMore acc} +     ) + + [M.fs] M.names} + + +
    + +end diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform.urs Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,6 @@ +functor Make (M : sig + con fs :: {Unit} + val names : $(mapUT string fs) + end) : sig + val main : unit -> transaction page +end diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform1.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform1.ur Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,3 @@ +open Metaform.Make(struct + val names = {A = "Tic", B = "Tac", C = "Toe"} + end) diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform1.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform1.urp Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,3 @@ + +metaform +metaform1 diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform1.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform1.urs Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform2.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform2.ur Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,12 @@ +structure MM = Metaform.Make(struct + val names = {X = "x", Y = "y"} + end) + +fun diversion () = return + Welcome to the diversion. + + +fun main () = return +
  • See something shiny!
    • +
  • Fill out a form!
    • +     diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform2.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform2.urp Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,3 @@ + +metaform +metaform2 diff -r e0e9e9eca1cb -r ad7e854a518c demo/metaform2.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/metaform2.urs Thu Oct 23 14:03:12 2008 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page diff -r e0e9e9eca1cb -r ad7e854a518c demo/prose --- a/demo/prose Thu Oct 23 12:58:35 2008 -0400 +++ b/demo/prose Thu Oct 23 14:03:12 2008 -0400 @@ -104,3 +104,7 @@ 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.

    + +metaform1.urp + +metaform2.urp diff -r e0e9e9eca1cb -r ad7e854a518c lib/top.ur --- a/lib/top.ur Thu Oct 23 12:58:35 2008 -0400 +++ b/lib/top.ur Thu Oct 23 14:03:12 2008 -0400 @@ -36,6 +36,26 @@ f [nm] [rest] r.nm (acc (r -- nm))) (fn _ => i) +fun foldUR2 (tf1 :: Type) (tf2 :: Type) (tr :: {Unit} -> Type) + (f : nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) + (i : tr []) = + fold [fn r :: {Unit} => $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r] + (fn (nm :: Name) (t :: Unit) (rest :: {Unit}) acc + [[nm] ~ rest] r1 r2 => + f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + (fn _ _ => i) + +fun foldURX2 (tf1 :: Type) (tf2 :: Type) (ctx :: {Unit}) + (f : nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> xml ctx [] []) = + foldUR2 [tf1] [tf2] [fn _ => xml ctx [] []] + (fn (nm :: Name) (rest :: {Unit}) [[nm] ~ rest] v1 v2 acc => + {f [nm] [rest] v1 v2}{acc}) + + fun foldTR (tf :: Type -> Type) (tr :: {Type} -> Type) (f : nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => diff -r e0e9e9eca1cb -r ad7e854a518c lib/top.urs --- a/lib/top.urs Thu Oct 23 12:58:35 2008 -0400 +++ b/lib/top.urs Thu Oct 23 14:03:12 2008 -0400 @@ -29,6 +29,18 @@ tf -> tr rest -> tr ([nm] ++ rest)) -> tr [] -> r :: {Unit} -> $(mapUT tf r) -> tr r +val foldUR2 : tf1 :: Type -> tf2 :: Type -> tr :: ({Unit} -> Type) + -> (nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> tr rest -> tr ([nm] ++ rest)) + -> tr [] -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> tr r + +val foldURX2: tf1 :: Type -> tf2 :: Type -> ctx :: {Unit} + -> (nm :: Name -> rest :: {Unit} + -> fn [[nm] ~ rest] => + tf1 -> tf2 -> xml ctx [] []) + -> r :: {Unit} -> $(mapUT tf1 r) -> $(mapUT tf2 r) -> xml ctx [] [] + val foldTR : tf :: (Type -> Type) -> tr :: ({Type} -> Type) -> (nm :: Name -> t :: Type -> rest :: {Type} -> fn [[nm] ~ rest] => diff -r e0e9e9eca1cb -r ad7e854a518c src/cjr_print.sml --- a/src/cjr_print.sml Thu Oct 23 12:58:35 2008 -0400 +++ b/src/cjr_print.sml Thu Oct 23 14:03:12 2008 -0400 @@ -1466,7 +1466,8 @@ let fun unurlify' rf t = case t of - TFfi (m, t) => string ("uw_" ^ ident m ^ "_unurlify" ^ capitalize t ^ "(ctx, &request)") + TFfi ("Basis", "unit") => string ("uw_unit_v") + | TFfi (m, t) => string ("uw_" ^ ident m ^ "_unurlify" ^ capitalize t ^ "(ctx, &request)") | TRecord 0 => string "uw_unit_v" | TRecord i =>