Email Gateway (Aug 22 2022 at 14:38): Email Gateway (Aug 22 2022 at 14:38):From: scott constable <sdconsta@syr.edu>
Hi All,
I'm writing a portable implementation of access control logic (ACL) for
Isabelle, Coq, and HOL4. In broad terms, ACL describes relationships
between principals (e.g. people, organizations, devices, etc.) and commands
which principals can execute. For example, the ACL statement
Alice says <Fetch>
indicates that Alice is executing the command "Fetch." The logic itself is
implemented in terms of inference rules. Ideally, such a theory would be
parameterized on two types: the type of principals and the type of
commands. For example, one interpretation of ACL could represent each
principal as a natural number, another interpretation could make principals
explicit:
datatype MyPrincipal = Alice | Bob
In Coq, I can do this with a module parameterized by some "Principal" and
"Command" each in the universe of types, e.g.
Module Type ACL.
Parameters Principal Command : Type.
...
End ACL.
What is the best practice for doing this in Isabelle?
Thanks in advance,
Scott Constable
Email Gateway (Aug 22 2022 at 14:38):From: Peter Lammich <lammich@in.tum.de>
Hi,
A locale fixes all polymorphic types of its parameters. If you have a type
variable not in the type of a fixed term variable, you can fix a variable of
type itself: fixes t :: 'a itself
Peter
\-------- Originalnachricht --------
Email Gateway (Aug 22 2022 at 14:38):From: scott constable <sdconsta@syr.edu>
Hi Peter,
First of all, thank you for your speedy response. I was able to use
"itself" to fix a type variable, but now I'm not sure how to actually use
it. For example, I now have:
locale ACL =
fixes principal :: "'a itself" and command :: "'b itself"
begin
datatype "princ" = -- {* Principal Expressions *}
p_PrincName "'a" -- {* Principal Name *}
| p_ConjWith "princ" "princ" -- {* Conjunction With *}
| p_Quoting "princ" "princ" -- {* Quoting *}
but now Isabelle reports an error: "Extra type variables on right-hand side
"'a"".
Scott
Email Gateway (Aug 22 2022 at 14:38):From: Lars Hupel <hupel@in.tum.de>
Dear Scott,
this is not possible in Isabelle/HOL.
Instead, you can define the "princ" datatype, parameterized on 'a (and
maybe 'b) outside of the locale. You can then use "('a, 'b) princ"
inside the locale.
Cheers
Lars
Email Gateway (Aug 22 2022 at 14:38):From: scott constable <sdconsta@syr.edu>
I don't think this will work for me. I'm generating the ACL grammar and
inference rules from a .ott file, and it seems that generating a
parameterized grammar is not supported by the ott tool. My planned
workaround was to wrap the ott output in a locale to fill in the missing
types.
Scott
Last updated: Apr 16 2024 at 20:15 UTC