Tree demo working (and other assorted regressions fixed)

6 files changed, 71 insertions, 8 deletions

diff --git a/src/cjr_print.sml b/src/cjr_print.sml
index 2485e317..3941fdd9 100644
--- a/src/cjr_print.sml
+++ b/src/cjr_print.sml
@@ -799,6 +799,43 @@ fun unurlify env (t, loc) =
                              string "})"]
                     end
 
+              | TOption t =>
+                box [string "(request[0] == '/' ? ++request : request, ",
+                     string "((!strncmp(request, \"None\", 4) ",
+                     string "&& (request[4] == 0 || request[4] == '/')) ",
+                     string "? (request += 4, NULL) ",
+                     string ": ((!strncmp(request, \"Some\", 4) ",
+                     string "&& request[4] == '/') ",
+                     string "? (request += 5, ",
+                     if isUnboxable  t then
+                         unurlify' rf (#1 t)
+                     else
+                         box [string "({",
+                              newline,
+                              p_typ env t,
+                              space,
+                              string "*tmp",
+                              space,
+                              string "=",
+                              space,
+                              string "uw_malloc(ctx, sizeof(",
+                              p_typ env t,
+                              string "));",
+                              newline,
+                              string "*tmp",
+                              space,
+                              string "=",
+                              space,
+                              unurlify' rf (#1 t),
+                              string ";",
+                              newline,
+                              string "tmp;",
+                              newline,
+                              string "})"],
+                     string ") :",
+                     space,
+                     string "(uw_error(ctx, FATAL, \"Error unurlifying option type\"), NULL))))"]
+
               | _ => (ErrorMsg.errorAt loc "Unable to choose a URL decoding function";
                       space)
     in
diff --git a/src/elab_env.sig b/src/elab_env.sig
index 90cf8153..926837e1 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -74,6 +74,7 @@ signature ELAB_ENV = sig
     val pushENamed : env -> string -> Elab.con -> env * int
     val pushENamedAs : env -> string -> int -> Elab.con -> env
     val lookupENamed : env -> int -> string * Elab.con
+    val checkENamed : env -> int -> bool
 
     val lookupE : env -> string -> Elab.con var
 
diff --git a/src/elab_env.sml b/src/elab_env.sml
index 46f62727..05da56db 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -542,6 +542,9 @@ fun lookupENamed (env : env) n =
         NONE => raise UnboundNamed n
       | SOME x => x
 
+fun checkENamed (env : env) n =
+    Option.isSome (IM.find (#namedE env, n))
+
 fun lookupE (env : env) x =
     case SM.find (#renameE env, x) of
         NONE => NotBound
diff --git a/src/elaborate.sml b/src/elaborate.sml
index f0beecdd..e84f5307 100644
--- a/src/elaborate.sml
+++ b/src/elaborate.sml
@@ -2282,9 +2282,15 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
                                         let
                                             val env = case #1 h of
                                                           L'.SgiCon (x, n, k, c) =>
-                                                          E.pushCNamedAs env x n k (SOME c)
+                                                          if E.checkENamed env n then
+                                                              env
+                                                          else
+                                                              E.pushCNamedAs env x n k (SOME c)
                                                         | L'.SgiConAbs (x, n, k) =>
-                                                          E.pushCNamedAs env x n k NONE
+                                                          if E.checkENamed env n then
+                                                              env
+                                                          else
+                                                              E.pushCNamedAs env x n k NONE
                                                         | _ => env
                                         in
                                             seek (E.sgiBinds env h, sgiBindsD (env, denv) h) t
@@ -2391,12 +2397,12 @@ fun subSgn (env, denv) sgn1 (sgn2 as (_, loc2)) =
 
                                              fun good () =
                                                  let
-                                                     val env = E.sgiBinds env sgi2All
+                                                     val env = E.sgiBinds env sgi1All
                                                      val env = if n1 = n2 then
                                                                    env
                                                                else
-                                                                   E.pushCNamedAs env x n1 k'
-                                                                                  (SOME (L'.CNamed n2, loc))
+                                                                   E.pushCNamedAs env x n2 k'
+                                                                                  (SOME (L'.CNamed n1, loc))
                                                  in
                                                      SOME (env, denv)
                                                  end
diff --git a/src/monoize.sml b/src/monoize.sml
index 9e1a4d22..ee509f52 100644
--- a/src/monoize.sml
+++ b/src/monoize.sml
@@ -390,6 +390,22 @@ fun fooifyExp fk env =
                         ((L'.EApp ((L'.ENamed n, loc), e), loc), fm)
                     end
 
+                  | L'.TOption t =>
+                    let
+                        val (body, fm) = fooify fm ((L'.ERel 0, loc), t)
+                    in
+                        ((L'.ECase (e,
+                                    [((L'.PNone t, loc),
+                                      (L'.EPrim (Prim.String "None"), loc)),
+                                     
+                                     ((L'.PSome (t, (L'.PVar ("x", t), loc)), loc),
+                                      (L'.EStrcat ((L'.EPrim (Prim.String "Some/"), loc),
+                                                   body), loc))],
+                                    {disc = tAll,
+                                     result = (L'.TFfi ("Basis", "string"), loc)}), loc),
+                         fm)
+                    end
+
                   | _ => (E.errorAt loc "Don't know how to encode attribute type";
                           Print.eprefaces' [("Type", MonoPrint.p_typ MonoEnv.empty tAll)];
                           (dummyExp, fm))
diff --git a/src/urweb.grm b/src/urweb.grm
index 4ac14450..b49cd793 100644
--- a/src/urweb.grm
+++ b/src/urweb.grm
@@ -1236,7 +1236,7 @@ sqlexp : TRUE                           (sql_inject (EVar (["Basis"], "True", In
                                                   end
                                           end)
 
-       | LBRACE LBRACK eexp RBRACK RBRACE       (eexp)
+       | LBRACE eexp RBRACE             (eexp)
 
        | sqlexp EQ sqlexp               (sql_compare ("eq", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
        | sqlexp NE sqlexp               (sql_compare ("ne", sqlexp1, sqlexp2, s (sqlexp1left, sqlexp2right)))
@@ -1256,8 +1256,8 @@ sqlexp : TRUE                           (sql_inject (EVar (["Basis"], "True", In
                                                     sqlexp), loc)
                                          end)
 
-       | LBRACE eexp RBRACE             (sql_inject (#1 eexp,
-                                                     s (LBRACEleft, RBRACEright)))
+       | LBRACE LBRACK eexp RBRACK RBRACE  (sql_inject (#1 eexp,
+                                                        s (LBRACEleft, RBRACEright)))
        | LPAREN sqlexp RPAREN           (sqlexp)
 
        | NULL                           (sql_inject ((EVar (["Basis"], "None", Infer),