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