Mercurial > urweb

comparison src/elab_env.sig @ 191:aa54250f58ac

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Parametrized datatypes through explify
author Adam Chlipala <adamc@hcoop.net>
date Fri, 08 Aug 2008 10:28:32 -0400
parents 8e9f97508f0d
children e86411f647c6
comparison
equal deleted inserted replaced
190:3eb53c957d10 191:aa54250f58ac
49 val pushCNamedAs : env -> string -> int -> Elab.kind -> Elab.con option -> env 49 val pushCNamedAs : env -> string -> int -> Elab.kind -> Elab.con option -> env
50 val lookupCNamed : env -> int -> string * Elab.kind * Elab.con option 50 val lookupCNamed : env -> int -> string * Elab.kind * Elab.con option
51 51
52 val lookupC : env -> string -> Elab.kind var 52 val lookupC : env -> string -> Elab.kind var
53 53
54 val pushDatatype : env -> int -> (string * int * Elab.con option) list -> env 54 val pushDatatype : env -> int -> string list -> (string * int * Elab.con option) list -> env
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 datatypeArgs : datatyp -> string list
58 val constructors : datatyp -> (string * int * Elab.con option) list 59 val constructors : datatyp -> (string * int * Elab.con option) list
59 60
60 val lookupConstructor : env -> string -> (Elab.datatype_kind * int * Elab.con option * int) option 61 val lookupConstructor : env -> string -> (Elab.datatype_kind * int * string list * Elab.con option * int) option
61 62
62 val pushERel : env -> string -> Elab.con -> env 63 val pushERel : env -> string -> Elab.con -> env
63 val lookupERel : env -> int -> string * Elab.con 64 val lookupERel : env -> int -> string * Elab.con
64 65
65 val pushENamed : env -> string -> Elab.con -> env * int 66 val pushENamed : env -> string -> Elab.con -> env * int
85 86
86 val hnormSgn : env -> Elab.sgn -> Elab.sgn 87 val hnormSgn : env -> Elab.sgn -> Elab.sgn
87 88
88 val projectCon : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> (Elab.kind * Elab.con option) option 89 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 } 90 val projectDatatype : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
90 -> (string * int * Elab.con option) list option 91 -> (string list * (string * int * Elab.con option) list) option
91 val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string } 92 val projectConstructor : env -> { sgn : Elab.sgn, str : Elab.str, field : string }
92 -> (Elab.datatype_kind * int * Elab.con option * Elab.con) option 93 -> (Elab.datatype_kind * int * string list * Elab.con option * Elab.con) option
93 val projectVal : env -> { sgn : Elab.sgn, str : Elab.str, field : string } -> Elab.con option 94 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 95 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 96 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 97 val projectConstraints : env -> { sgn : Elab.sgn, str : Elab.str } -> (Elab.con * Elab.con) list option
97 98