# HG changeset patch # User Adam Chlipala # Date 1241366515 14400 # Node ID 74a090ff296ea9aa7de2a60aaf51062cd2325af5 # Parent 8ed1261f838c8722b3cee46c29d4cd2ff16f7452 constraints demo diff -r 8ed1261f838c -r 74a090ff296e demo/constraints.ur --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/constraints.ur Sun May 03 12:01:55 2009 -0400 @@ -0,0 +1,38 @@ +table t : { Id : int, Nam : string, Parent : option int } + PRIMARY KEY Id, + CONSTRAINT Nam UNIQUE Nam, + CONSTRAINT Id CHECK Id >= 0, + CONSTRAINT Parent FOREIGN KEY Parent REFERENCES t(Id) + +fun main () = + list <- queryX (SELECT * FROM t) + (fn r => + {[r.T.Id]} + {[r.T.Nam]} + {case r.T.Parent of + None => NULL + | Some id => {[id]}} + ); + return + + + {list} +
Id Name Parent
+ +
+ + + + + +
Id:
Name:
Parent:
+
+ + +and add r = + dml (INSERT INTO t (Id, Nam, Parent) + VALUES ({[readError r.Id]}, {[r.Nam]}, + {[case r.Parent of + "" => None + | s => Some (readError s)]})); + main () diff -r 8ed1261f838c -r 74a090ff296e demo/constraints.urp --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/constraints.urp Sun May 03 12:01:55 2009 -0400 @@ -0,0 +1,4 @@ +database dbname=test +sql constraints.sql + +constraints diff -r 8ed1261f838c -r 74a090ff296e demo/constraints.urs --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/demo/constraints.urs Sun May 03 12:01:55 2009 -0400 @@ -0,0 +1,1 @@ +val main : unit -> transaction page diff -r 8ed1261f838c -r 74a090ff296e demo/prose --- a/demo/prose Sat May 02 18:46:00 2009 -0400 +++ b/demo/prose Sun May 03 12:01:55 2009 -0400 @@ -100,12 +100,23 @@

The signature of TreeFun.Make tells us that, to instantiate the functor, we must provide

    -
  1. A primary key type key
    2. -
  2. SQL field names id (for primary keys) and parent (for parent links)
    3. -
  3. A type-level record cols of field names besides id and parent
    4. -
  4. "Proofs" that id is distinct from parent and that neither of id and parent appears in cols
    5. -
  5. A witness that key belongs to the type class sql_injectable_prim, which indicates that both key and option key are fair game to use with SQL
    6. -
  6. An SQL table tab, containing a field id of type key, a field parent of type option key, and every field of cols
    7. +
  7. A primary key type key
    8. +
  8. SQL field names id (for primary keys) and parent (for parent links)
    9. +
  9. A type-level record cols of field names besides id and parent
    10. +
  10. "Proofs" that id is distinct from parent and that neither of id and parent appears in cols
    11. +
  11. A witness that key belongs to the type class sql_injectable_prim, which indicates that both key and option key are fair game to use with SQL
    12. +
  12. An SQL table tab, containing a field id of type key, a field parent of type option key, and every field of cols
    13. +
+ +constraints.urp + +

Ur/Web supports attaching SQL table constraints to table definitions. We've sprinkled a few such constraints throughout our examples so far, without mentioning them. This example shows a table with all four of the supported kinds of constraints. An application would generally try to avoid inserting data that violates constraints, but, in this example, we let you insert arbitrary data, so that you can see each of the constraints failing.

+ +
    +
  1. The PRIMARY KEY constraint establishes the field of the table that we expect to use as a key in looking up specific rows. It is an error for two rows to share the same primary key.
    2. +
  2. The UNIQUE constraint is like PRIMARY KEY, with the difference being that a table may have many UNIQUE constraints but no more than one primary key.
    3. +
  3. The CHECK constraint declares a boolean assertion that must hold for every row of the table.
    4. +
  4. The FOREIGN KEY constraint declares that a row of the table references a particular column of another table, or of the same table, as we see in this example. It's a static type error to reference a foreign key column that has no PRIMARY KEY or UNIQUE constraint.
sum.urp @@ -121,13 +132,13 @@

Another library function foldUR is defined at the level of expressions, while mapU is a type-level function. foldUR takes 7 arguments, some of them types and some values. Type arguments are distinguished by being written within brackets. The arguments to foldUR respectively tell us:

    -
  1. The type we will assign to each record field
    2. -
  2. The type of the final and all intermediate results of the fold, expressed as a function over the portion of the {Unit} that has been traversed so far
    3. -
  3. A function that updates the accumulator based on the current record field name, the rest of the input record type, the current record field value, and the current accumulator
    4. -
  4. The initial accumulator value
    5. -
  5. The input record type
    6. -
  6. A folder for that type
    7. -
  7. The input record value
    8. +
  8. The type we will assign to each record field
    9. +
  9. The type of the final and all intermediate results of the fold, expressed as a function over the portion of the {Unit} that has been traversed so far
    10. +
  10. A function that updates the accumulator based on the current record field name, the rest of the input record type, the current record field value, and the current accumulator
    11. +
  11. The initial accumulator value
    12. +
  12. The input record type
    13. +
  13. A folder for that type
    14. +
  14. The input record value
An unusual part of the third argument is the syntax [t1 ~ t2] within a multi-argument fn. This syntax denotes a proof that row types t1 and t2 have no field names in common. The proof is not named, because it is applied automatically as needed. Indeed, the proof appears unused in this case, though it is actually needed to ensure the validity of some inferred types, as well as to unify with the type of foldUR.

@@ -158,12 +169,12 @@

The signature of Crud.Make is based around a type function colMeta, which describes which supporting values we need for each column. This function is declared with the keyword con, which stands for "constructor," the general class of "compile-time things" that includes types. An argument to colMeta has kind (Type * Type), which means that it must be a type-level tuple. The first type is how the column is represented in SQL, and the second is how we represent it in HTML forms. In order, the components of the resulting record give:

    -
  1. A display name
    2. -
  2. A way of pretty-printing values of the column
    3. -
  3. A way of generating an HTML form widget to input this column
    4. -
  4. A way of generating an HTML form widget with an initial value specified
    5. -
  5. A way of parsing values of the column from strings
    6. -
  6. A type class witness, showing that the SQL representation can really be included in SQL
    7. +
  7. A display name
    8. +
  8. A way of pretty-printing values of the column
    9. +
  9. A way of generating an HTML form widget to input this column
    10. +
  10. A way of generating an HTML form widget with an initial value specified
    11. +
  11. A way of parsing values of the column from strings
    12. +
  12. A type class witness, showing that the SQL representation can really be included in SQL

The function colsMeta lifts colMeta over type-level records of type pairs. The Crud module also defines reasonable default colMeta values for some primitive types.

@@ -171,11 +182,11 @@

The functor signature tells us (in order) that an input must contain:

    -
  1. A type pair record cols
    2. -
  2. A proof that cols does not contain a field named Id
    3. -
  3. A SQL table tab with an Id field of type int and other fields whose names and types are read off of cols
    4. -
  4. A display title for the admin interface
    5. -
  5. A record of meta-data for the columns
    6. +
  6. A type pair record cols
    7. +
  7. A proof that cols does not contain a field named Id
    8. +
  8. A SQL table tab with an Id field of type int and other fields whose names and types are read off of cols
    9. +
  9. A display title for the admin interface
    10. +
  10. A record of meta-data for the columns

Looking at crud1.ur, we see that a use of the functor is almost trivial. Only the value components of the argument structure must be provided. The column row type is inferred, and the disjointness constraint is proved automatically.

@@ -226,9 +237,9 @@

The first three fields of a colMeta record are the same as for Crud. The rest of the fields are:

    -
  1. NewState, which allocates some new widget local state
    2. -
  2. Widget, which produces a reactive widget from some state
    3. -
  3. ReadState, which reads the current value of some state to determine which SQL value it encodes
    4. +
  4. NewState, which allocates some new widget local state
    5. +
  5. Widget, which produces a reactive widget from some state
    6. +
  6. ReadState, which reads the current value of some state to determine which SQL value it encodes

BatchFun.Make handles the plumbing of allocating the local state, using it to create widgets, and reading the state values when the user clicks "Batch it."

diff -r 8ed1261f838c -r 74a090ff296e src/demo.sml --- a/src/demo.sml Sat May 02 18:46:00 2009 -0400 +++ b/src/demo.sml Sun May 03 12:01:55 2009 -0400 @@ -44,7 +44,7 @@ file = "index.html"} val out = TextIO.openOut fname - val () = (TextIO.output (out, "\n"); + val () = (TextIO.output (out, "\n"); TextIO.output (out, "\n"); TextIO.output (out, "\n"); TextIO.output (out, "\n");