Overloading formal relation

2 files changed, 20 insertions, 3 deletions

diff --git a/language/l2_rules.ott b/language/l2_rules.ott
index 44b74ef0..1beb4702 100644
--- a/language/l2_rules.ott
+++ b/language/l2_rules.ott
@@ -425,10 +425,21 @@ E_d, K_Typ |- t ~= t'
 E_d, K_Nat |- ne ~= ne'
 
 defn
-select ( conformsto ( t , t' ) ) of tinflist gives tinf' :: :: selectoverload :: so_
-{{ tex [[select]]_{(\textbf{conformsto} ([[t]],[[t']]))} ([[tinflist]]) [[gives]] [[tinf']] }}
+E_d |- select ( conformsto ( t , t' ) ) of tinflist gives tinflist' :: :: selectoverload :: so_
+{{ tex [[select]]_{[[conformsto]] ([[t]],[[t']])} ([[tinflist]]) [[gives]] [[tinflist']] }}
 by
 
+E_d |- ti ~= ti'
+E_d |- tj' ~= tj
+E_d |- select (full(ti,tj)) of tinf0 .. tinfm tinf'0 .. tinf'n gives empty
+--------------------------------------------------------- :: full
+E_d |- select (full( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag, ti' -> tj' effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> tj'
+
+E_d |- ti ~= ti'
+E_d |- select (parm(ti,tj)) of tinf0 .. tinfm gives empty
+-------------------------------------------------------- :: parm
+E_d |- select (parm( ti, tj)) of tinf0 .. tinfm E_k,S_N,tag,ti' -> t effect tinf'0 .. tinf'n gives E_k,S_N,tag,ti' -> t
+
 defn
 E_d |- t ~< t' , S_N :: :: consistent_typ :: consistent_typ_
 by
diff --git a/language/l2_typ.ott b/language/l2_typ.ott
index d55499e0..12baa059 100644
--- a/language/l2_typ.ott
+++ b/language/l2_typ.ott
@@ -201,8 +201,14 @@ S_N {{ tex {\Sigma^{\textsc{N} } } }} :: '' ::= {{ phantom }}
 
 tinflist :: 'tinfs_' ::=
   {{ com In place so that a list of tinfs can be referred to without the dot form }}
+  | empty :: :: empty
   | tinf1 ... tinfn  :: :: ls
 
+conformsto :: 'conformsto_' ::=
+  {{ com how much conformance does overloading need }}
+ | full :: :: full
+ | parm :: :: parm
+
  E_a {{ tex \ottnt{E}^{\textsc{a} } }} :: 'E_a_' ::=   {{ phantom }}
                                                                             {{ hol tid |-> tinf}}
                                                                             {{ lem map tid tinf }} 
@@ -258,7 +264,7 @@ grammar
    | { id1 |-> tinf1 , .. , idn |-> tinfn }                    :: :: base
      {{ hol (FOLDR (\x E. E |+ x) FEMPTY [[id1 tinf1 .. idn tinfn]]) }}
      {{ lem (List.foldr (fun (x,f) m -> Map.insert x f m) Map.empty [[id1 tinf1 .. idn tinfn]]) }} 
-   | { id |-> overload tinf : tinf1 , ... , tinfn }        :: :: overload
+   | { id |-> overload tinf conformsto : tinf1 , ... , tinfn }        :: :: overload
    | ( E_t1 u+ .... u+ E_tn )                                         :: M :: union
      {{ hol (FOLDR FUNION FEMPTY [[E_t1....E_tn]]) }}
      {{ lem (List.foldr (union) Map.empty [[E_t1....E_tn]]) }}