[CakeML] Behaviour of evaluate_dec

[Scott Owens]

The c field is for new data constructors. let rec doesn’t make any new data constructors, so it is empty. The result for each declaration (for both variables and constructors) is not cumulative, but just the definitions that that declaration makes.

Scott

> On 2017/05/25, at 08:18, Lars Hupel <hupel at in.tum.de> wrote:
> 
> Dear CakeML developers,
> 
> I am wondering about the "dletrec1" rule in the big step semantics:
> 
> dletrec1 : forall ck mn env funs s locs.
> List.allDistinct (List.map (fun (x,y,z) -> x) funs)
> ==>
> evaluate_dec ck mn env s (Dletrec locs funs) (s, Rval <| v =
> build_rec_env funs env nsEmpty; c = nsEmpty |>)
> 
> Why is it that the "c" field of the result semantic environment is left
> empty? Isn't that necessary for determining the welltypedness of pattern
> matching?
> 
> This seems to be the same for the functional semantics.
> 
> Cheers
> Lars
> 
> _______________________________________________
> Users mailing list
> Users at cakeml.org
> https://lists.cakeml.org/listinfo/users