equal.}}%
-equal: tp -> tp -> type.
-e_ref: equal T T.
+LF equal: tp -> tp -> type =
+| e_ref: equal T T;
%{{## Schema
The schema txG describes a context containing assumptions x:tm, each associated with a typing assumption hastype x t for some type t. Formally, we are using a dependent product &Eta (used only in contexts) to tie x to hastype x t. We thus do not need to establish separately that for every variable there is a unique typing assumption: this is inherent in the definition of txG. The schema classifies well-formed contexts and checking whether a context satisfies a schema will be part of type checking. As a consequence, type checking will ensure that we are manipulating only well-formed contexts, that later declarations overshadow previous declarations, and that all declarations are of the specified form.}}%
@@ -47,15 +47,15 @@ The schema txG describes a context containing assumptions x:t
schema xtG = some [t:tp] block x:term, _t:hastype x t;
%{{## Typing uniqueness proof
-Our final proof of type uniqueness rec unique proceeds by case analysis on the first derivation. Accordingly, the recursive function pattern-matches on the first derivation d which has type [g |- hastype (M[..]) T].}}%
+Our final proof of type uniqueness rec unique proceeds by case analysis on the first derivation. Accordingly, the recursive function pattern-matches on the first derivation d which has type [g |- hastype M T].}}%
-% induction on [g |- hastype (M[..]) T]
+% induction on [g |- hastype M T]
rec unique : (g:xtG)[g |- hastype M T[]] -> [g |- hastype M T'[]]
-> [ |- equal T T'] =
fn d => fn f => case d of
-| [g |- h_app (D1[..]) (D2[..])] =>
- let [g |- h_app (F1[..]) (F2[..])] = f in
- let [ |- e_ref] = unique [g |- D1[..]] [g |- F1[..]] in
+| [g |- h_app D1 D2] =>
+ let [g |- h_app F1 F2] = f in
+ let [ |- e_ref] = unique [g |- D1] [g |- F1] in
[ |- e_ref]
| [g |- h_lam (\x.\u. D)] =>
@@ -63,18 +63,18 @@ fn d => fn f => case d of
let [ |- e_ref] = unique [g,b: block x:term, u:hastype x _ |- D[..,b.x,b.u]] [g,b |- F[..,b.x,b.u]] in
[ |- e_ref]
-| [g |- #q.2[..]] => % d : hastype #p.1 T
- let [g |- #r.2[..]] = f in % f : hastype #p.1 T'
+| [g |- #q.2] => % d : hastype #p.1 T
+ let [g |- #r.2] = f in % f : hastype #p.1 T'
[ |- e_ref]
;
%{{
Consider each case individually.
- Application case.
-If the first derivation d concludes with
h_app, it matches the pattern [g |- h_app (D1[..]) (D2[..])], and forms a contextual object in the context g of type [g |- hastype (M[..]) T']. D1 corresponds to the first premise of the typing rule for applications with contextual type [g |- hastype (M1[..]) (arr T' T)]. Using a let-binding, we invert the second argument, the derivation f which must have type [g |- hastype (app (M1[..]) (M2[..])) T]. F1 corresponds to the first premise of the typing rule for applications and has the contextual type [g |- hastype (M1[..]) (arr S' S)]. The appeal to the induction hypothesis using D1 and F1 in the on-paper proof corresponds to the recursive call unique [g |- D1[..]] [g |- F1[..]]. Note that while unique’s type says it takes a context variable (g:xtG), we do not pass it explicitly; Beluga infers it from the context in the first argument passed. The result of the recursive call is a contextual object of type [ |- eq (arr T1 T2) (arr S1 S2)]. The only rule that could derive such an object is e_ref, and pattern matching establishes that arr T T' = arr S S’ and hence T = S and T' = S’.
-Lambda case. If the first derivation d concludes with h_lam, it matches the pattern [g |- h_lam (\x.\u. D u)], and is a contextual object in the context g of type hastype (lam T M) (arr T T'). Pattern matching—through a let-binding—serves to invert the second derivation f, which must have been by h_lam with a subderivation F u to reach hastype (M) S that can use x, _t:hastype x T, and assumptions from g.
+If the first derivation d concludes with h_app, it matches the pattern [g |- h_app D1 D2], and forms a contextual object in the context g of type [g |- hastype M T']. D1 corresponds to the first premise of the typing rule for applications with contextual type [g |- hastype M1 (arr T' T)]. Using a let-binding, we invert the second argument, the derivation f which must have type [g |- hastype (app M1 M2) T]. F1 corresponds to the first premise of the typing rule for applications and has the contextual type [g |- hastype M1 (arr S' S)]. The appeal to the induction hypothesis using D1 and F1 in the on-paper proof corresponds to the recursive call unique [g |- D1] [g |- F1]. Note that while unique’s type says it takes a context variable (g:xtG), we do not pass it explicitly; Beluga infers it from the context in the first argument passed. The result of the recursive call is a contextual object of type [ |- eq (arr T1 T2) (arr S1 S2)]. The only rule that could derive such an object is e_ref, and pattern matching establishes that arr T T' = arr S S’ and hence T = S and T' = S’.Lambda case. If the first derivation d concludes with h_lam, it matches the pattern [g |- h_lam (\x.\u. D u)], and is a contextual object in the context g of type hastype (lam T M) (arr T T'). Pattern matching—through a let-binding—serves to invert the second derivation f, which must have been by h_lam with a subderivation F to reach hastype M S that can use x, _t:hastype x T, and assumptions from g.
The use of the induction hypothesis on D and F in a paper proof corresponds to the recursive call to unique. To appeal to the induction hypothesis, we need to extend the context by pairing up x and the typing assumption hastype x T. This is accomplished by creating the declaration b: block x:term, u:hastype x T. In the code, we wrote an underscore _ instead of T, which tells Beluga to reconstruct it since we cannot write T there without binding it by explicitly giving the type of D. To retrieve x we take the first projection b.x, and to retrieve x’s typing assumption we take the second projection b.u.
-Now we can appeal to the induction hypothesis using D1[..] b.x b.u and F1[..] b.x b.u in the context g,b: block x:term, u:hastype x S. From the i.h. we get a contextual object, a closed derivation of (eq (arr T T') (arr S S’))[ ]. The only rule that could derive this is ref, and pattern matching establishes that S must equal S’, since we must have arr T S = arr T1 S’. Therefore, there is a proof of [ |- equal S S’], and we can finish with the reflexivity rule e_ref.
- Variable case. Since our context consists of blocks containing variables of type
tm and assumptions hastype x T, we pattern match on [g |- #p.2[..]], i.e., we project out the second argument of the block. By the given assumptions, we know that [g |- #p.2[..]] has type [g |- hastype (#p.1[..]) T], because #p has type [g |- block x:tm , u:hastype x T]. We also know that the second input, called f, to the function unique has type [g |- hastype (#p.1[..]) T']. By inversion on f, we know that the only possible object that can inhabit this type is [g |- #p.2[..]] and therefore T' must be identical to T. Moreover, #r denotes the same block as #p.
+Now we can appeal to the induction hypothesis using D1[.., b.x, b.u] and F1[.., b.x, b.u] in the context g,b: block x:term, u:hastype x S. From the i.h. we get a contextual object, a closed derivation of (eq (arr T T') (arr S S’))[ ]. The only rule that could derive this is ref, and pattern matching establishes that S must equal S’, since we must have arr T S = arr T1 S’. Therefore, there is a proof of [ |- equal S S’], and we can finish with the reflexivity rule e_ref.
+- Variable case. Since our context consists of blocks containing variables of type
tm and assumptions hastype x T, we pattern match on [g |- #p.2], i.e., we project out the second argument of the block. By the given assumptions, we know that [g |- #p.2] has type [g |- hastype (#p.1) T], because #p has type [g |- block x:tm , u:hastype x T]. We also know that the second input, called f, to the function unique has type [g |- hastype (#p.1) T']. By inversion on f, we know that the only possible object that can inhabit this type is [g |- #p.2] and therefore T' must be identical to T. Moreover, #r denotes the same block as #p.
}}%
diff --git a/src/core/prettyext.ml b/src/core/prettyext.ml
index 6eefc5c2e..715289204 100644
--- a/src/core/prettyext.ml
+++ b/src/core/prettyext.ml
@@ -224,13 +224,11 @@ module Ext = struct
fprintf ppf "%s" name
| LF.Atom (_, a, ms) ->
- let cond = lvl > 1 in
let name = to_html (Id.render_name a) Link in
- fprintf ppf "%s%s%a%s"
- (l_paren_if cond)
+ fprintf ppf "%s%a"
name
(fmt_ppr_lf_spine cD cPsi 2) ms
- (r_paren_if cond)
+
| LF.PiTyp (_,LF.TypDecl (x, a), (LF.ArrTyp _ as b)) ->
let cond = lvl > 1 in
let x = fresh_name_dctx cPsi x in
@@ -348,13 +346,11 @@ module Ext = struct
let paren s = not (Control.db()) && lvl > 0 && true
in begin match head with
| LF.MVar (_, x, LF.EmptySub _) ->
- fprintf ppf "%s" (Id.render_name x)
+ fprintf ppf "%s[^]" (Id.render_name x)
| LF.MVar (_, x, s) ->
- fprintf ppf "%s%s%a%s"
- (l_paren_if (paren s))
+ fprintf ppf "%s%a"
(Id.render_name x)
(fmt_ppr_lf_sub cD cPsi lvl) s
- (r_paren_if (paren s))
(* | LF.SVar (_, x, s) -> *)
(* fprintf ppf "%s%s%a%s" *)
@@ -400,39 +396,40 @@ module Ext = struct
| Control.Natural -> fmt_ppr_lf_sub_natural cD cPsi lvl ppf s
| Control.DeBruijn -> fmt_ppr_lf_sub_deBruijn cD cPsi lvl ppf s
- and fmt_ppr_lf_sub_natural cD cPsi lvl ppf s=
- let print_front = fmt_ppr_lf_front cD cPsi 1 in
- let hasCtxVar = has_ctx_var cPsi in
- let rec self lvl ppf = function
- (* Print ".." for a Shift when there is a context variable present,
+ and fmt_ppr_lf_sub_natural cD cPsi lvl ppf s =
+ let print_front = fmt_ppr_lf_front cD cPsi 1 in
+ let hasCtxVar = has_ctx_var cPsi in
+ let rec self lvl ppf = (function
+ (* Print ".." for a Shift when there is a context variable present,
and nothing otherwise *)
- (* above is WRONG *)
- | LF.Dot (_, f, s) when hasCtxVar ->
- fprintf ppf "%a %a"
- (self lvl) f
- print_front s
-
- | LF.Dot (_, f, s) when not hasCtxVar ->
- fprintf ppf "%a %a"
+ (* above is WRONG *)
+ | LF.Dot (_, f, s) when hasCtxVar ->
+ fprintf ppf "%a, %a" (self lvl) f
+ print_front s
+
+ | LF.Dot (_, f, s) when not hasCtxVar ->
+ fprintf ppf "%a, %a"
(self lvl) f
print_front s
- | LF.Id _ ->
+ | LF.Id _ ->
fprintf ppf "%s" (symbol_to_html Dots)
- | LF.RealId -> ()
- | LF.EmptySub _ ->
+ | LF.RealId -> ()
+
+ | LF.EmptySub _ ->
fprintf ppf ""
- | LF.SVar(_, s, LF.EmptySub _) ->
+ | LF.SVar(_, s, LF.EmptySub _) ->
fprintf ppf "#%s[^]"
(Id.render_name s)
- | LF.SVar (_, s, f) ->
+ | LF.SVar (_, s, f) ->
fprintf ppf "#%s[%a]"
(Id.render_name s)
- (self lvl) f
+ (self lvl) f)
in
- fprintf ppf " %a"
- (self lvl) s
+ (match s with
+ | LF.RealId -> fprintf ppf ""
+ | _ -> fprintf ppf "[%a]" (self lvl) s)
and fmt_ppr_lf_sub_deBruijn cD cPsi lvl ppf s =
let rec self lvl ppf = function
@@ -715,7 +712,7 @@ module Ext = struct
fprintf ppf "[%a %s %a]"
(fmt_ppr_lf_dctx cD 0) cPsi
(symbol_to_html Turnstile)
- (fmt_ppr_lf_typ cD cPsi 1) tA
+ (fmt_ppr_lf_typ cD cPsi 0) tA
| Comp.TypBox (_, (_,LF.ClTyp (LF.PTyp tA, cPsi))) ->
fprintf ppf "#[%a %s %a]"
@@ -863,11 +860,9 @@ module Ext = struct
(r_paren_if cond)
| Comp.Box (_ , m) ->
- let cond = lvl > 1 in
- fprintf ppf "%s%a%s"
- (l_paren_if cond)
+ fprintf ppf "%a"
(fmt_ppr_meta_obj cD 0) m
- (r_paren_if cond)
+
| Comp.Case (_, Pragma.RegularCase, i, [b]) ->
begin match b with
@@ -1074,11 +1069,11 @@ module Ext = struct
fprintf ppf "%s %s : %a = "
(to_html prefix Keyword)
(to_html (Id.render_name n) (ID Typ))
- (fmt_ppr_lf_kind LF.Null 1) kA
+ (fmt_ppr_lf_kind LF.Null 0) kA
| Sgn.Const(_, n, tA) ->
fprintf ppf "@\n| %s : %a"
(to_html (Id.render_name n) (ID Constructor))
- (fmt_ppr_lf_typ LF.Empty LF.Null 1) tA
+ (fmt_ppr_lf_typ LF.Empty LF.Null 0) tA
| Sgn.CompTyp(_, n, kA, _)
| Sgn.CompCotyp(_, n, kA) ->
fprintf ppf "%s %s : %a = "