Mercurial > urweb
comparison src/elaborate.sml @ 1912:006633a0039a
Sneaky still-in-today's-release update of 'table' signature item handling
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Sun, 24 Nov 2013 09:56:50 -0500 |
parents | b7cd3c7c7edd |
children | 072656016dfa |
comparison
equal
deleted
inserted
replaced
1911:7d26b96370af | 1912:006633a0039a |
---|---|
2627 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); | 2627 checkKind env c' ck (L'.KRecord (L'.KType, loc), loc); |
2628 checkCon env' pe' pet pst; | 2628 checkCon env' pe' pet pst; |
2629 checkCon env' ce' cet cst; | 2629 checkCon env' ce' cet cst; |
2630 | 2630 |
2631 ([(L'.SgiConAbs (x', hidden_n, cstK), loc), | 2631 ([(L'.SgiConAbs (x', hidden_n, cstK), loc), |
2632 (L'.SgiConstraint (visible, hidden), loc), | 2632 (L'.SgiConstraint ((L'.CConcat (pkey, visible), loc), hidden), loc), |
2633 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) | 2633 (L'.SgiVal (x, n, ct), loc)], (env', denv, gs''' @ gs'' @ gs' @ gs)) |
2634 end | 2634 end |
2635 | 2635 |
2636 | L.SgiStr (x, sgn) => | 2636 | L.SgiStr (x, sgn) => |
2637 let | 2637 let |
3629 | L'.TRecord c => | 3629 | L'.TRecord c => |
3630 (case decompileCon env c of | 3630 (case decompileCon env c of |
3631 NONE => NONE | 3631 NONE => NONE |
3632 | SOME c' => SOME (L.TRecord c', loc)) | 3632 | SOME c' => SOME (L.TRecord c', loc)) |
3633 | 3633 |
3634 | c => (Print.preface ("WTF?", p_con env (c, loc)); NONE) | 3634 | c => ((*Print.preface ("WTF?", p_con env (c, loc));*) NONE) |
3635 | 3635 |
3636 fun buildNeeded env sgis = | 3636 fun buildNeeded env sgis = |
3637 #1 (foldl (fn ((sgi, loc), (nd, env')) => | 3637 #1 (foldl (fn ((sgi, loc), (nd, env')) => |
3638 (case sgi of | 3638 (case sgi of |
3639 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k) | 3639 L'.SgiCon (x, _, k, _) => naddCon (nd, x, k) |
4858 | 4858 |
4859 if ErrorMsg.anyErrors () then | 4859 if ErrorMsg.anyErrors () then |
4860 ModDb.revert () | 4860 ModDb.revert () |
4861 else | 4861 else |
4862 (); | 4862 (); |
4863 | |
4864 (*Print.preface("File", ElabPrint.p_file env file);*) | |
4863 | 4865 |
4864 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) | 4866 (L'.DFfiStr ("Basis", basis_n, sgn), ErrorMsg.dummySpan) |
4865 :: ds | 4867 :: ds |
4866 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) | 4868 @ (L'.DStr ("Top", top_n, topSgn, topStr), ErrorMsg.dummySpan) |
4867 :: ds' @ file | 4869 :: ds' @ file |