# HG changeset patch # User Adam Chlipala # Date 1276452786 14400 # Node ID cd8d2c73ccf4d7daab06e62ec687c11497a2da1e # Parent 1e6a4f9d3e4a3e82d23e89a08adf92fa06120a50 Catch a missed ReduceLocal of field projection annotations diff -r 1e6a4f9d3e4a -r cd8d2c73ccf4 src/expl_env.sig --- a/src/expl_env.sig Sun Jun 13 10:55:20 2010 -0400 +++ b/src/expl_env.sig Sun Jun 13 14:13:06 2010 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -66,4 +66,6 @@ val declBinds : env -> Expl.decl -> env val sgiBinds : env -> Expl.sgn_item -> env + val patBinds : env -> Expl.pat -> env + end diff -r 1e6a4f9d3e4a -r cd8d2c73ccf4 src/expl_env.sml --- a/src/expl_env.sml Sun Jun 13 10:55:20 2010 -0400 +++ b/src/expl_env.sml Sun Jun 13 14:13:06 2010 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -400,4 +400,13 @@ | SgiSgn (x, n, sgn) => pushSgnNamed env x n sgn | SgiStr (x, n, sgn) => pushStrNamed env x n sgn +fun patBinds env (p, loc) = + case p of + PWild => env + | PVar (x, t) => pushERel env x t + | PPrim _ => env + | PCon (_, _, _, NONE) => env + | PCon (_, _, _, SOME p) => patBinds env p + | PRecord xps => foldl (fn ((_, p, _), env) => patBinds env p) env xps + end diff -r 1e6a4f9d3e4a -r cd8d2c73ccf4 src/expl_print.sml --- a/src/expl_print.sml Sun Jun 13 10:55:20 2010 -0400 +++ b/src/expl_print.sml Sun Jun 13 14:13:06 2010 -0400 @@ -1,4 +1,4 @@ -(* Copyright (c) 2008, Adam Chlipala +(* Copyright (c) 2008-2010, Adam Chlipala * All rights reserved. * * Redistribution and use in source and binary forms, with or without @@ -422,7 +422,7 @@ space, string "=>", space, - p_exp env e]) pes]) + p_exp (E.patBinds env p) e]) pes]) | ELet (x, t, e1, e2) => box [string "let", space, diff -r 1e6a4f9d3e4a -r cd8d2c73ccf4 src/reduce_local.sml --- a/src/reduce_local.sml Sun Jun 13 10:55:20 2010 -0400 +++ b/src/reduce_local.sml Sun Jun 13 14:13:06 2010 -0400 @@ -286,12 +286,12 @@ | EKAbs (x, e) => (EKAbs (x, exp env e), loc) | ERecord xcs => (ERecord (map (fn (x, e, t) => (con env x, exp env e, con env t)) xcs), loc) - | EField (e, c, others) => + | EField (e, c, {field = f, rest = r}) => let val e = exp env e val c = con env c - fun default () = (EField (e, c, others), loc) + fun default () = (EField (e, c, {field = con env f, rest = con env r}), loc) in case (#1 e, #1 c) of (ERecord xcs, CName x) =>