Elsa L. Gunter

2016-07-27 13:44:27 UTC

Permalink

Dear Isabelle community,Raw Message

I am having difficulty building records they way I want. I may well

have forgotten something, but the behavior I am see with extending

polymorphic records is surprising to me. First I define:

record ('instr,'dir) generalized_control_flow_graph_context =

Instructions :: "'instr set"

Directions :: "'dir set"

edgeTyping :: "'instr ⇒ ('dir ⇒ nat)set"

If I then enter

declare [[show_types = true]]

term "⦇Instructions =a,

Directions = b,

edgeTyping =c⦈"

I get

"⦇Instructions = a::'a set, Directions = b::'b set,

edgeTyping = c::'a ⇒ ('b ⇒ nat) set⦈"

:: "('a, 'b) generalized_control_flow_graph_context"

as output, which is what I would expect. Now I wish to extend this

record to a new record with additional fields, introducing some new

type variables, but also sharing the type variables already used in

generalized_control_flow_graph_context. So I enter the following:

record ('instr,'dir,'node) generalized_control_flow_graph =

"('instr,'dir) generalized_control_flow_graph_context" +

Nodes :: "'node set"

Edges :: "'node ⇒ ('dir × 'node)set"

labeling :: "'node ⇒ 'instr"

The intent is that the types of 'dir and 'instr are shared between

Instructions, Directions, edgeTyping, Edges and labeling. When I

create at element of this extended record type as follows I get the

given results:

term "⦇Instructions =a,

Directions = b,

edgeTyping =c,

Nodes = d,

Edges = e,

labeling = f⦈"

"⦇Instructions = a::'a set, Directions = b::'b set,

edgeTyping = c::'a ⇒ ('b ⇒ nat) set, Nodes = d::'e set,

Edges = e::'e ⇒ ('d × 'e) set, labeling = f::'e ⇒ 'c⦈"

:: "⦇Instructions :: 'a set, Directions :: 'b set,

edgeTyping :: 'a ⇒ ('b ⇒ nat) set, Nodes :: 'e set,

Edges :: 'e ⇒ ('d × 'e) set, labeling :: 'e ⇒ 'c⦈"

Note that the types of Nodes, Edges, labeling are completely

independent of those for Instructions, Directions and edgeTyping,

despite the same types being used in both parts of the

generalized_control_flow_graph record definition. I know each type

gets separately parsed separately, but it seems plausible that the

whole record extension package could infer that the types used in one

part of the definition where to be the same as those of the same name

in other parts. These extra degrees of freedom present problems where

type variables can end up buried on the right-hand side of a definition

without being captured by the left hand side, where they would if the

desired type constraints had been enforced. I have found a number of

crufty ways around the difficulty, but I would appreciate help with

learning how to do this record extension definition correctly. I've

not been able to find it in the documentation.

---Elsa