comparison src/elab_util.sig @ 1732:4a03aa3251cb

Initial support for reusing elaboration results
author Adam Chlipala <adam@chlipala.net>
date Sun, 29 Apr 2012 13:17:31 -0400
parents 6c00d8af6239
children d28adceef22a
comparison
equal deleted inserted replaced
1731:27e731a65934 1732:4a03aa3251cb
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2010, 2012, Adam Chlipala
2 * All rights reserved. 2 * All rights reserved.
3 * 3 *
4 * Redistribution and use in source and binary forms, with or without 4 * Redistribution and use in source and binary forms, with or without
5 * modification, are permitted provided that the following conditions are met: 5 * modification, are permitted provided that the following conditions are met:
6 * 6 *
227 sgn : 'context -> Elab.sgn' -> Elab.sgn', 227 sgn : 'context -> Elab.sgn' -> Elab.sgn',
228 str : 'context -> Elab.str' -> Elab.str', 228 str : 'context -> Elab.str' -> Elab.str',
229 decl : 'context -> Elab.decl' -> Elab.decl', 229 decl : 'context -> Elab.decl' -> Elab.decl',
230 bind : 'context * binder -> 'context} 230 bind : 'context * binder -> 'context}
231 -> 'context -> Elab.decl -> Elab.decl 231 -> 'context -> Elab.decl -> Elab.decl
232
233 val fold : {kind : Elab.kind' * 'state -> 'state,
234 con : Elab.con' * 'state -> 'state,
235 exp : Elab.exp' * 'state -> 'state,
236 sgn_item : Elab.sgn_item' * 'state -> 'state,
237 sgn : Elab.sgn' * 'state -> 'state,
238 str : Elab.str' * 'state -> 'state,
239 decl : Elab.decl' * 'state -> 'state}
240 -> 'state -> Elab.decl -> 'state
232 end 241 end
233 242
234 structure File : sig 243 structure File : sig
235 val maxName : Elab.file -> int 244 val maxName : Elab.file -> int
236 245