# HG changeset patch # User Adam Chlipala # Date 1308056085 14400 # Node ID 18d18a70821e5b959c5a11ca17f2a092f5960db8 # Parent 67ebd30a2283ffe29b758a69fd7c9777b2af4ba6 Implicit argument insertion for local variables diff -r 67ebd30a2283 -r 18d18a70821e doc/manual.tex --- a/doc/manual.tex Sun Jun 12 17:44:34 2011 -0400 +++ b/doc/manual.tex Tue Jun 14 08:54:45 2011 -0400 @@ -527,7 +527,7 @@ A signature item or declaration $\mt{class} \; x = \lambda y \Rightarrow c$ may be abbreviated $\mt{class} \; x \; y = c$. -Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all type class instance and disjointness arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments. The default is that implicit arguments are inserted automatically after any reference to a non-local variable, or after any application of a non-local variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). +Handling of implicit and explicit constructor arguments may be tweaked with some prefixes to variable references. An expression $@x$ is a version of $x$ where all type class instance and disjointness arguments have been made explicit. An expression $@@x$ achieves the same effect, additionally making explicit all implicit constructor arguments. The default is that implicit arguments are inserted automatically after any reference to a variable, or after any application of a variable to one or more arguments. For such an expression, implicit wildcard arguments are added for the longest prefix of the expression's type consisting only of implicit polymorphism, type class instances, and disjointness obligations. The same syntax works for variables projected out of modules and for capitalized variables (datatype constructors). At the expression level, an analogue is available of the composite $\lambda$ form for constructors. We define the language of binders as $b ::= p \mid [x] \mid [x \; ? \; \kappa] \mid X \mid [c \sim c]$. A lone variable $[x]$ stands for an implicit constructor variable of unspecified kind. The standard value-level function binder is recovered as the type-annotated pattern form $x : \tau$. It is a compile-time error to include a pattern $p$ that does not match every value of the appropriate type. diff -r 67ebd30a2283 -r 18d18a70821e lib/ur/monad.ur --- a/lib/ur/monad.ur Sun Jun 12 17:44:34 2011 -0400 +++ b/lib/ur/monad.ur Tue Jun 14 08:54:45 2011 -0400 @@ -21,7 +21,7 @@ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> m (tr rest)) r => acc' <- acc (r -- nm); - f [nm] [t] [rest] ! r.nm acc') + f [nm] [t] [rest] r.nm acc') (fn _ => return i) fl @@ -34,7 +34,7 @@ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> _ -> m (tr rest)) r1 r2 => acc' <- acc (r1 -- nm) (r2 -- nm); - f [nm] [t] [rest] ! r1.nm r2.nm acc') + f [nm] [t] [rest] r1.nm r2.nm acc') (fn _ _ => return i) fl @@ -47,7 +47,7 @@ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> _ -> _ -> m (tr rest)) r1 r2 r3 => acc' <- acc (r1 -- nm) (r2 -- nm) (r3 -- nm); - f [nm] [t] [rest] ! r1.nm r2.nm r3.nm acc') + f [nm] [t] [rest] r1.nm r2.nm r3.nm acc') (fn _ _ _ => return i) fl @@ -88,7 +88,7 @@ (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> m ($(map tf' rest) * tr rest)) r => p <- acc (r -- nm); - p' <- f [nm] [t] [rest] ! r.nm p.2; + p' <- f [nm] [t] [rest] r.nm p.2; return ({nm = p'.1} ++ p.1, p'.2)) (fn _ => return ({}, i)) fl diff -r 67ebd30a2283 -r 18d18a70821e lib/ur/top.ur --- a/lib/ur/top.ur Sun Jun 12 17:44:34 2011 -0400 +++ b/lib/ur/top.ur Tue Jun 14 08:54:45 2011 -0400 @@ -21,7 +21,7 @@ [tf :: {K} -> Type] (f : nm :: Name -> v :: K -> r :: {K} -> [[nm] ~ r] => tf r -> tf ([nm = v] ++ r)) - (i : tf []) = f [nm] [v] [r] ! (fold [tf] f i) + (i : tf []) = f [nm] [v] [r] (fold [tf] f i) fun concat [K] [r1 ::: {K}] [r2 ::: {K}] [r1 ~ r2] (f1 : folder r1) (f2 : folder r2) @@ -33,8 +33,8 @@ (fn [nm :: Name] [v :: K] [r1' :: {K}] [[nm] ~ r1'] (acc : [r1' ~ r2] => tf (r1' ++ r2)) [[nm = v] ++ r1' ~ r2] => - f [nm] [v] [r1' ++ r2] ! acc) - (fn [[] ~ r2] => f2 [tf] f i) ! + f [nm] [v] [r1' ++ r2] acc) + (fn [[] ~ r2] => f2 [tf] f i) fun mp [K1] [K2] [f ::: K1 -> K2] [r ::: {K1}] (fold : folder r) @@ -44,7 +44,7 @@ (i : tf []) = fold [fn r => tf (map f r)] (fn [nm :: Name] [v :: K1] [rest :: {K1}] [[nm] ~ rest] (acc : tf (map f rest)) => - f [nm] [f v] [map f rest] ! acc) + f [nm] [f v] [map f rest] acc) i end @@ -127,7 +127,7 @@ (i : tr []) [r ::: {Unit}] (fl : folder r) = fl [fn r :: {Unit} => $(mapU tf r) -> tr r] (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r => - f [nm] [rest] ! r.nm (acc (r -- nm))) + f [nm] [rest] r.nm (acc (r -- nm))) (fn _ => i) fun foldUR2 [tf1 :: Type] [tf2 :: Type] [tr :: {Unit} -> Type] @@ -137,7 +137,7 @@ (i : tr []) [r ::: {Unit}] (fl : folder r) = fl [fn r :: {Unit} => $(mapU tf1 r) -> $(mapU tf2 r) -> tr r] (fn [nm :: Name] [t :: Unit] [rest :: {Unit}] [[nm] ~ rest] acc r1 r2 => - f [nm] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + f [nm] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) (fn _ _ => i) fun foldR [K] [tf :: K -> Type] [tr :: {K} -> Type] @@ -147,7 +147,7 @@ (i : tr []) [r ::: {K}] (fl : folder r) = fl [fn r :: {K} => $(map tf r) -> tr r] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> tr rest) r => - f [nm] [t] [rest] ! r.nm (acc (r -- nm))) + f [nm] [t] [rest] r.nm (acc (r -- nm))) (fn _ => i) fun foldR2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tr :: {K} -> Type] @@ -158,7 +158,7 @@ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> tr r] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> _ -> tr rest) r1 r2 => - f [nm] [t] [rest] ! r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) + f [nm] [t] [rest] r1.nm r2.nm (acc (r1 -- nm) (r2 -- nm))) (fn _ _ => i) fun foldR3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [tr :: {K} -> Type] @@ -169,14 +169,14 @@ fl [fn r :: {K} => $(map tf1 r) -> $(map tf2 r) -> $(map tf3 r) -> tr r] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] (acc : _ -> _ -> _ -> tr rest) r1 r2 r3 => - f [nm] [t] [rest] ! r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) + f [nm] [t] [rest] r1.nm r2.nm r3.nm (acc (r1 -- nm) (r2 -- nm) (r3 -- nm))) (fn _ _ _ => i) fun mapUX [tf :: Type] [ctx :: {Unit}] (f : nm :: Name -> rest :: {Unit} -> [[nm] ~ rest] => tf -> xml ctx [] []) = @@foldR [fn _ => tf] [fn _ => xml ctx [] []] (fn [nm :: Name] [u :: Unit] [rest :: {Unit}] [[nm] ~ rest] r acc => - {f [nm] [rest] ! r}{acc}) + {f [nm] [rest] r}{acc}) fun mapX [K] [tf :: K -> Type] [ctx :: {Unit}] @@ -185,7 +185,7 @@ tf t -> xml ctx [] []) = @@foldR [tf] [fn _ => xml ctx [] []] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r acc => - {f [nm] [t] [rest] ! r}{acc}) + {f [nm] [t] [rest] r}{acc}) fun mapUX2 [tf1 :: Type] [tf2 :: Type] [ctx :: {Unit}] @@ -194,7 +194,7 @@ 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}) + {f [nm] [rest] v1 v2}{acc}) fun mapX2 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [ctx :: {Unit}] @@ -204,7 +204,7 @@ @@foldR2 [tf1] [tf2] [fn _ => xml ctx [] []] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r1 r2 acc => - {f [nm] [t] [rest] ! r1 r2}{acc}) + {f [nm] [t] [rest] r1 r2}{acc}) fun mapX3 [K] [tf1 :: K -> Type] [tf2 :: K -> Type] [tf3 :: K -> Type] [ctx :: {Unit}] @@ -214,7 +214,7 @@ @@foldR3 [tf1] [tf2] [tf3] [fn _ => xml ctx [] []] (fn [nm :: Name] [t :: K] [rest :: {K}] [[nm] ~ rest] r1 r2 r3 acc => - {f [nm] [t] [rest] ! r1 r2 r3}{acc}) + {f [nm] [t] [rest] r1 r2 r3}{acc}) fun query1 [t ::: Name] [fs ::: {Type}] [state ::: Type] (q : sql_query [] [] [t = fs] []) diff -r 67ebd30a2283 -r 18d18a70821e src/elaborate.sml --- a/src/elaborate.sml Sun Jun 12 17:44:34 2011 -0400 +++ b/src/elaborate.sml Tue Jun 14 08:54:45 2011 -0400 @@ -1751,6 +1751,7 @@ case e of L'.ENamed _ => true | L'.EModProj _ => true + | L'.ERel _ => true | L'.EApp (e, _) => findHead' e | L'.ECApp (e, _) => findHead' e | L'.EKApp (e, _) => findHead' e