summaryrefslogtreecommitdiff
path: root/src/elaborate.sig
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-10 20:21:35 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commit053783525d8365b8a498ac38942d44f4669d6a54 (patch)
tree95bf1dd92ee28c88a03d20c3909eb6906645251b /src/elaborate.sig
parent98ebd4d0b10165693a205d30399149e32954b833 (diff)
First version of calculateFileState
Diffstat (limited to 'src/elaborate.sig')
-rw-r--r--src/elaborate.sig14
1 files changed, 14 insertions, 0 deletions
diff --git a/src/elaborate.sig b/src/elaborate.sig
index 03359814..88ea068f 100644
--- a/src/elaborate.sig
+++ b/src/elaborate.sig
@@ -53,4 +53,18 @@ signature ELABORATE = sig
, 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