Mercurial > urweb
comparison src/elab_env.sig @ 191:aa54250f58ac
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 |