diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2008-08-08 10:28:32 -0400 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2008-08-08 10:28:32 -0400 |
| commit | baf22271ef6e646c97ddfa1e4193a8857816c67d (patch) | |
| tree | 1d34bf6404d3e94e6862c5fedbc4e53ed6bab883 /src/expl_print.sml | |
| parent | 51fd5b1af6b2af7706c0c8604129d99e504a2d36 (diff) | |
Parametrized datatypes through explify
Diffstat (limited to 'src/expl_print.sml')
| -rw-r--r-- | src/expl_print.sml | 19 |
1 files changed, 11 insertions, 8 deletions
diff --git a/src/expl_print.sml b/src/expl_print.sml index 1056dfe4..60075a70 100644 --- a/src/expl_print.sml +++ b/src/expl_print.sml @@ -181,10 +181,10 @@ fun p_pat' par env (p, _) = PWild => string "_" | PVar (s, _) => string s | PPrim p => Prim.p_t p - | PCon (_, pc, NONE) => p_patCon env pc - | PCon (_, pc, SOME p) => parenIf par (box [p_patCon env pc, - space, - p_pat' true env p]) + | PCon (_, pc, _, NONE) => p_patCon env pc + | PCon (_, pc, _, SOME p) => parenIf par (box [p_patCon env pc, + space, + p_pat' true env p]) | PRecord xps => box [string "{", p_list_sep (box [string ",", space]) (fn (x, p, _) => @@ -329,13 +329,16 @@ fun p_named x n = else string x -fun p_datatype env (x, n, cons) = +fun p_datatype env (x, n, xs, cons) = let - val env = E.pushCNamed env x n (KType, ErrorMsg.dummySpan) NONE + val k = (KType, ErrorMsg.dummySpan) + val env = E.pushCNamed env x n k NONE + val env = foldl (fn (x, env) => E.pushCRel env x k) env xs in box [string "datatype", space, string x, + p_list_sep (box []) (fn x => box [space, string x]) xs, space, string "=", space, @@ -368,7 +371,7 @@ fun p_sgn_item env (sgi, _) = space, p_con env c] | SgiDatatype x => p_datatype env x - | SgiDatatypeImp (x, _, m1, ms, x', _) => + | SgiDatatypeImp (x, _, m1, ms, x', _, _) => let val m1x = #1 (E.lookupStrNamed env m1) handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 @@ -482,7 +485,7 @@ fun p_decl env (dAll as (d, _) : decl) = space, p_con env c] | DDatatype x => p_datatype env x - | DDatatypeImp (x, _, m1, ms, x', _) => + | DDatatypeImp (x, _, m1, ms, x', _, _) => let val m1x = #1 (E.lookupStrNamed env m1) handle E.UnboundNamed _ => "UNBOUND_STR_" ^ Int.toString m1 |