diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2020-05-30 19:49:56 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2020-05-30 19:49:56 -0400 |
commit | c2f1e1096f602b1cbd4531352f3e1ea6d656a186 (patch) | |
tree | ae102982878bb0c31bdfe07209e60bfc14030490 /src/elaborate.sig | |
parent | 095c2640aa2070ed4e2765875238d5e6e6673856 (diff) | |
parent | 5a0b639dfbd7db9d16c6995f72ba17152a1f362d (diff) |
Merge branch 'upstream' into dfsg_clean20200209+dfsgdfsg_clean
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r-- | src/elaborate.sig | 25 |
1 files changed, 24 insertions, 1 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig index d60cff42..d6747241 100644 --- a/src/elaborate.sig +++ b/src/elaborate.sig @@ -29,7 +29,10 @@ signature ELABORATE = sig val elabFile : Source.sgn_item list -> Time.time -> Source.decl list -> Source.sgn_item list -> Time.time - -> ElabEnv.env -> Source.file -> Elab.file + -> ElabEnv.env + -> (ElabEnv.env -> ElabEnv.env) (* Adapt env after stdlib but before elaborate *) + -> Source.file + -> Elab.file val resolveClass : ElabEnv.env -> Elab.con -> Elab.exp option @@ -47,4 +50,24 @@ signature ELABORATE = sig val incremental : bool ref val verbose : bool ref + val dopen: ElabEnv.env + -> { str: int + , strs: string list + , sgn: Elab.sgn } + -> (Elab.decl list * ElabEnv.env) + + val elabSgn: (ElabEnv.env * Disjoint.env) + -> Source.sgn + -> (Elab.sgn * Disjoint.goal list) + + datatype constraint = + Disjoint of Disjoint.goal + | TypeClass of ElabEnv.env * Elab.con * Elab.exp option ref * ErrorMsg.span + + val elabStr: (ElabEnv.env * Disjoint.env) + -> Source.str + -> (Elab.str * Elab.sgn * constraint list) + + val subSgn: ElabEnv.env -> ErrorMsg.span -> Elab.sgn -> Elab.sgn -> unit + end |