diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-10-21 16:41:11 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-10-21 16:41:11 -0400 |
| commit | 1a5acb4732536e4be288895eb89d139b19aebc94 (patch) | |
| tree | e4856ac916556022e401a21e2ff722af1b472aa1 /src/elab_env.sml | |
| parent | a3418cf924752accf2f68fc2673da2a661276ae5 (diff) | |
New implicit argument handling
Diffstat (limited to 'src/elab_env.sml')
| -rw-r--r-- | src/elab_env.sml | 65 |
1 files changed, 42 insertions, 23 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml index 4ff026f1..958d369c 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -358,7 +358,7 @@ fun pushClass (env : env) n = sgn = #sgn env, renameStr = #renameStr env, - str = #str env} + str = #str env} fun class_name_in (c, _) = case c of @@ -367,6 +367,14 @@ fun class_name_in (c, _) = | CUnif (_, _, _, ref (SOME c)) => class_name_in c | _ => NONE +fun isClass (env : env) c = + let + fun find NONE = false + | find (SOME c) = Option.isSome (CM.find (#classes env, c)) + in + find (class_name_in c) + end + fun class_key_in (c, _) = case c of CRel n => SOME (CkRel n) @@ -405,14 +413,16 @@ fun pushERel (env : env) x t = val classes = case class_pair_in t of NONE => classes | SOME (f, x) => - let - val class = Option.getOpt (CM.find (classes, f), empty_class) - val class = { - ground = KM.insert (#ground class, x, (ERel 0, #2 t)) - } - in - CM.insert (classes, f, class) - end + case CM.find (classes, f) of + NONE => classes + | SOME class => + let + val class = { + ground = KM.insert (#ground class, x, (ERel 0, #2 t)) + } + in + CM.insert (classes, f, class) + end in {renameC = #renameC env, relC = #relC env, @@ -444,14 +454,16 @@ fun pushENamedAs (env : env) x n t = val classes = case class_pair_in t of NONE => classes | SOME (f, x) => - let - val class = Option.getOpt (CM.find (classes, f), empty_class) - val class = { - ground = KM.insert (#ground class, x, (ENamed n, #2 t)) - } - in - CM.insert (classes, f, class) - end + case CM.find (classes, f) of + NONE => classes + | SOME class => + let + val class = { + ground = KM.insert (#ground class, x, (ENamed n, #2 t)) + } + in + CM.insert (classes, f, class) + end in {renameC = #renameC env, relC = #relC env, @@ -740,14 +752,21 @@ fun enrichClasses env classes (m1, ms) sgn = | SOME ck => let val cn = ClProj (m1, ms, fx) - val class = Option.getOpt (CM.find (classes, cn), empty_class) - val class = { - ground = KM.insert (#ground class, ck, - (EModProj (m1, ms, x), #2 sgn)) - } + val classes = + case CM.find (classes, cn) of + NONE => classes + | SOME class => + let + val class = { + ground = KM.insert (#ground class, ck, + (EModProj (m1, ms, x), #2 sgn)) + } + in + CM.insert (classes, cn, class) + end in - (CM.insert (classes, cn, class), + (classes, newClasses, fmap, env) |