move 'tag' to the outside

Author: squell

proofs/sudoers.mlw

@@ -17,19 +17,22 @@ function last_match (pred: 'a -> bool) (a: seq 'a): 'a
       a[last_index]
 
 (* loose models for the types in sudoers::Ast *)
-type name = H.key
-type metavar 'a = All | Only 'a | Alias name
+type metavar 'a = All | Only 'a | Alias H.key
 type qualified 'a = Allow 'a | Forbid 'a
-type spec 'tag 'a = { inner: qualified (metavar 'a); info: 'tag }
+type spec 'a = qualified (metavar 'a)
+
+type tagged 'tag 'a = { inner: 'a; info: 'tag }
+type tagged_spec 'tag 'a = tagged 'tag (spec 'a)
+
 type found_aliases = H.t bool
 
-function who (item: spec 'tag 'a): metavar 'a
-  = match item.inner with
+function who (item: spec 'a): metavar 'a
+  = match item with
     | Allow x -> x
     | Forbid x -> x
     end
 
-function condition (aliases: found_aliases) (item: spec 'tag 'a): option (qualified 'tag)
+function condition (aliases: found_aliases) (item: tagged_spec 'tag 'a): option (qualified 'tag)
   = match item with
     | { inner = Allow (Alias name);  info = tag } -> Some(if H.find name aliases then Allow tag else Forbid tag)
     | { inner = Forbid (Alias name); info = tag } -> Some(if H.find name aliases then Forbid tag else Allow tag)
@@ -38,8 +41,8 @@ function condition (aliases: found_aliases) (item: spec 'tag 'a): option (qualif
     | _ -> None
     end
 
-function matched_by (pred: 'a -> bool) (aliases: found_aliases) (item: spec 'tag 'a): bool
-  = match who item with
+function matched_by (pred: 'a -> bool) (aliases: found_aliases) (item: tagged_spec 'tag 'a): bool
+  = match who item.inner with
     | All -> true
     | Only x -> pred x
     | Alias name -> H.mem name aliases
@@ -48,20 +51,20 @@ function matched_by (pred: 'a -> bool) (aliases: found_aliases) (item: spec 'tag
 let function bool_then (b: bool) (x: 'a): option 'a
   = if b then Some x else None
 
-function rule (pred: 'a -> bool) (aliases: found_aliases) (items: seq (spec 'tag 'a)): option (qualified 'tag)
+function rule (pred: 'a -> bool) (aliases: found_aliases) (items: seq (tagged_spec 'tag 'a)): option (qualified 'tag)
   = if contains (matched_by pred aliases) items then
       condition aliases (last_match (matched_by pred aliases) items)
     else
       None
 
-function judgement (pred: 'a -> bool) (aliases: found_aliases) (items: seq (spec 'tag 'a)): option 'tag
+function judgement (pred: 'a -> bool) (aliases: found_aliases) (items: seq (tagged_spec 'tag 'a)): option 'tag
   = match rule pred aliases items with
     | Some (Allow tag) -> Some tag
     | _ -> None
     end
 
 (* Why3 model of the sudoers::find_item function *)
-let find_item (items: seq (spec 'tag 'a)) (pred: 'a -> bool) (aliases: found_aliases): option 'tag
+let find_item (items: seq (tagged_spec 'tag 'a)) (pred: 'a -> bool) (aliases: found_aliases): option 'tag
     ensures { result = judgement pred aliases items }
 
 = let result = ref None in