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