Mercurial > urweb
comparison src/elab_env.sig @ 188:8e9f97508f0d
Datatype representation optimization
author | Adam Chlipala <adamc@hcoop.net> |
---|---|
date | Sun, 03 Aug 2008 19:49:21 -0400 |
parents | 7ee424760d2f |
children | aa54250f58ac |
comparison
equal
deleted
inserted
replaced
187:fb6ed259f5bd | 188:8e9f97508f0d |
---|---|
55 type datatyp | 55 type datatyp |
56 val lookupDatatype : env -> int -> datatyp | 56 val lookupDatatype : env -> int -> datatyp |
57 val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option | 57 val lookupDatatypeConstructor : datatyp -> int -> string * Elab.con option |
58 val constructors : datatyp -> (string * int * Elab.con option) list | 58 val constructors : datatyp -> (string * int * Elab.con option) list |
59 | 59 |
60 val lookupConstructor : env -> string -> (int * Elab.con option * int) option | 60 val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option |
61 | 61 |
62 val pushERel : env -> string -> Elab.con -> env | 62 val pushERel : env -> string -> Elab.con -> env |
63 val lookupERel : env -> int -> string * Elab.con | 63 val lookupERel : env -> int -> string * Elab.con |
64 | 64 |
65 val pushENamed : env -> string -> Elab.con -> env * int | 65 val pushENamed : env -> string -> Elab.con -> env * int |
87 | 87 |
88 val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option | 88 val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option |
89 val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string } | 89 val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string } |
90 -> (string * int * Elab.con option) list option | 90 -> (string * int * Elab.con option) list option |
91 val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string } | 91 val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string } |
92 -> (int * Elab.con option * Elab.con) option | 92 -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option |
93 val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option | 93 val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option |
94 val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option | 94 val projectSgn : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option |
95 val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option | 95 val projectStr : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.sgn option |
96 val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option | 96 val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option |
97 | 97 |