Mercurial > urweb

comparison src/elaborate.sml @ 29:537db4ee89f4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Translation to Cjr
author Adam Chlipala <adamc@hcoop.net>
date Tue, 10 Jun 2008 18:28:43 -0400
parents 4ab19c19665f
children e6ccf961d8a3
comparison
equal deleted inserted replaced
28:104d43266b33 29:537db4ee89f4
702 (case #1 (typeof env e1) of 702 (case #1 (typeof env e1) of
703 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1 703 L'.TCFun (_, _, _, c1) => subConInCon (0, c) c1
704 | _ => raise Fail "typeof: Bad ECApp") 704 | _ => raise Fail "typeof: Bad ECApp")
705 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc) 705 | L'.ECAbs (expl, x, k, e1) => (L'.TCFun (expl, x, k, typeof (E.pushCRel env x k) e1), loc)
706 706
707 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, e) => (x, typeof env e)) xes), loc), loc) 707 | L'.ERecord xes => (L'.TRecord (L'.CRecord (ktype, map (fn (x, _, t) => (x, t)) xes), loc), loc)
708 | L'.EField (_, _, {field, ...}) => field 708 | L'.EField (_, _, {field, ...}) => field
709 709
710 | L'.EError => cerror 710 | L'.EError => cerror
711 711
712 fun elabHead env (e as (_, loc)) t = 712 fun elabHead env (e as (_, loc)) t =
819 in 819 in
820 checkKind env x' xk kname; 820 checkKind env x' xk kname;
821 (x', e', et) 821 (x', e', et)
822 end) xes 822 end) xes
823 in 823 in
824 ((L'.ERecord (map (fn (x', e', _) => (x', e')) xes'), loc), 824 ((L'.ERecord xes', loc),
825 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc)) 825 (L'.TRecord (L'.CRecord (ktype, map (fn (x', _, et) => (x', et)) xes'), loc), loc))
826 end 826 end
827 827
828 | L.EField (e, c) => 828 | L.EField (e, c) =>
829 let 829 let