diff options
Diffstat (limited to 'language')
| -rw-r--r-- | language/l2_rules.ott | 15 | ||||
| -rw-r--r-- | language/l2_typ.ott | 8 |
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]]) }} |