summaryrefslogtreecommitdiff
path: root/src/elab_env.sml
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simon.van.casteren@gmail.com>2020-01-10 02:25:45 +0100
committerGravatar Simon Van Casteren <simon.van.casteren@gmail.com>2020-01-10 02:25:45 +0100
commitce6bae891c6d1e22e61a1fb54ce3ecd08ca31891 (patch)
treee6681735be997d9d6e2c34d6adb327638fcc2ee1 /src/elab_env.sml
parent028f15cce127360f29afa41754aab3816718492f (diff)
Refactor to do all matching on strings, more precise and faster
Diffstat (limited to 'src/elab_env.sml')
-rw-r--r--src/elab_env.sml28
1 files changed, 11 insertions, 17 deletions
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f492bc94..5fa32cd2 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -404,14 +404,6 @@ fun lookupC (env : env) x =
| SOME (Rel' x) => Rel x
| SOME (Named' x) => Named x
-fun matchCByPrefix (env: env) (prefix: string): (string * kind) list =
- List.mapPartial (fn (name, value) => if String.isPrefix prefix name
- then case value of
- Rel' (_, x) => SOME (name, x)
- | Named' (_, x) => SOME (name, x)
- else NONE)
- (SM.listItemsi (#renameC env))
-
fun pushDatatype (env : env) n xs xncs =
let
val dk = U.classifyDatatype xncs
@@ -940,13 +932,6 @@ fun lookupENamed (env : env) n =
NONE => raise UnboundNamed n
| SOME x => x
-(* TODO Why does this work better than using #renameE? *)
-fun matchEByPrefix (env: env) (prefix: string): (string * con) list =
- List.mapPartial (fn (name, value) => if String.isPrefix prefix name
- then SOME (name, value)
- else NONE)
- (#relE env @ IM.listItems (#namedE env))
-
fun checkENamed (env : env) n =
Option.isSome (IM.find (#namedE env, n))
@@ -1000,8 +985,17 @@ fun lookupStrNamed (env : env) n =
| SOME x => x
fun lookupStr (env : env) x = SM.find (#renameStr env, x)
-fun matchStrByPrefix (env: env) prefix =
- List.filter (fn (name,_) => String.isPrefix prefix name) (SM.listItemsi (#renameStr env))
+
+fun dumpCs (env: env): (string * kind) list =
+ List.map (fn (name, value) => case value of
+ Rel' (_, x) => (name, x)
+ | Named' (_, x) => (name, x))
+ (SM.listItemsi (#renameC env))
+(* TODO try again with #renameE *)
+fun dumpEs (env: env): (string * con) list =
+ #relE env @ IM.listItems (#namedE env)
+fun dumpStrs (env: env) =
+ SM.listItemsi (#renameStr env)
fun sgiSeek (sgi, (sgns, strs, cons)) =
case sgi of