This commit is contained in:
Olivier 2020-07-10 14:10:43 +02:00
parent f59d28cd1c
commit a1a844901e
3 changed files with 211 additions and 3 deletions

View File

@ -170,3 +170,200 @@ and print_pattern_atom = function
print_tuple print_pattern ps
| PInj _ as pat ->
group (parens (print_pattern pat))
(* De Bruijn *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* -------------------------------------------------------------------------- *)
(* Types. *)
let print_tyvar x =
OCaml.int x (* TEMPORARY *)
let rec print_debruijn_type (ty:debruijn_type) =
print_type_quant ty
and print_type_quant = function
| TyMu ((), ty) ->
string "mu " ^^
lparen ^^ rparen ^^
dot ^^ space ^^
print_type_quant ty
| TyForall ((), ty) ->
lbracket ^^
lparen ^^ rparen ^^
rbracket ^^ space ^^
print_type_quant ty
| ty ->
print_type_arrow ty
and print_type_arrow = function
| TyArrow (ty1, ty2) ->
print_type_atom ty1 ^^
string " -> " ^^
print_type_arrow ty2
| ty ->
print_type_atom ty
and print_type_atom = function
| TyVar x ->
print_tyvar x
| TyProduct tys ->
surround_separate_map 2 0 (lbrace ^^ rbrace)
lbrace star rbrace print_debruijn_type tys
| TySum tys ->
surround_separate_map 2 0 (lbracket ^^ rbracket)
lbracket plus rbracket print_debruijn_type tys
| TyMu _ | TyForall _ | TyArrow _ as ty ->
group (parens (print_debruijn_type ty))
let print_angle_type ty =
surround 2 0 langle (print_debruijn_type ty) rangle
(* -------------------------------------------------------------------------- *)
(* Terms. *)
let print_inj tys i t =
string "inj" ^^
print_angle_type (TySum tys) ^^ space ^^
OCaml.int i ^^ space ^^
t
let print_tuple print_elem elems =
let contents =
match elems with
| [elem] -> print_elem elem ^^ comma
| _ -> separate_map (comma ^^ space) print_elem elems in
surround 2 0 lparen contents rparen
let print_let_in lhs rhs body =
string "let " ^^ lhs
^^ string " = " ^^ rhs
^^ string " in " ^^ body
let rec print_debruijn_term (t:debruijn_term) =
print_term_abs t
and print_term_abs = function
| TyAbs ((), t1) ->
string "FUN " ^^
lparen ^^ rparen ^^
string " = " ^^
print_term_abs t1
| Let (x, t1, t2) ->
print_let_in
(string x)
(print_debruijn_term t1)
(print_term_abs t2)
| LetProd (xs, t1, t2) ->
print_let_in
(print_tuple string xs)
(print_debruijn_term t1)
(print_term_abs t2)
| Abs (x, ty1, t2) ->
string "fun " ^^
string x ^^
string " : " ^^
print_debruijn_type ty1 ^^
string " = " ^^
print_term_abs t2
| t ->
print_term_proj t
and print_term_proj = function
| Proj (i, t) ->
string "proj" ^^
langle ^^
OCaml.int i ^^
rangle ^^
space ^^
print_term_app t
| Inj (ty1, i, t2) ->
print_inj ty1 i (print_term_app t2)
| t ->
print_term_app t
and print_term_app = function
| TyApp (t1, ty2) ->
print_term_app t1 ^^
space ^^ lbracket ^^
print_debruijn_type ty2 ^^
rbracket
| App (t1, t2) ->
print_term_app t1 ^^
space ^^
print_term_atom t2
| t ->
print_term_atom t
and print_term_atom = function
| Var x ->
string x
| Tuple ts ->
print_tuple print_debruijn_term ts
| Match (ty, t, brs) ->
string "match" ^^ print_angle_type ty ^^ space ^^
print_debruijn_term t ^^ space ^^
string "with" ^^ hardline ^^
print_branches brs ^^ space ^^
string "end"
| TyAbs _ | Let _ | LetProd _ | Abs _
| Proj _ | Inj _ | TyApp _ | App _ as t ->
group (parens (print_debruijn_term t))
and print_branches brs =
separate_map hardline print_branch brs
and print_branch (pat,t) =
bar ^^ space ^^
print_pattern pat ^^
string " -> " ^^
print_debruijn_term t
and print_pattern pat =
print_pattern_inj pat
and print_pattern_inj = function
| PInj (tys, i, pat) ->
print_inj tys i (print_pattern_atom pat)
| pat ->
print_pattern_atom pat
and print_pattern_atom = function
| PVar x ->
string x
| PWildcard ->
underscore
| PTuple ps ->
print_tuple print_pattern ps
| PInj _ as pat ->
group (parens (print_pattern pat))

View File

@ -6,3 +6,5 @@ open F
val print_type: nominal_type -> document
val print_term: nominal_term -> document
val print_debruijn_type: debruijn_type -> document
val print_debruijn_term: debruijn_term -> document

View File

@ -171,9 +171,18 @@ let rec equal budget ty1 ty2 =
let budget =
4
let print_type ty =
PPrint.(ToChannel.pretty 0.9 80 stdout (FPrinter.print_debruijn_type ty ^^ hardline))
let (--) ty1 ty2 =
if not (equal budget ty1 ty2) then
raise (TypeError (TypeMismatch (ty1, ty2)))
if not (equal budget ty1 ty2) then begin
print_endline "foo";
print_type ty1;
print_type ty2;
print_endline "bar";
flush_all ();
raise (TypeError (TypeMismatch (ty1, ty2)))
end
let nth_type complete_ty tys i =
if i < 0 || i >= List.length tys then
@ -220,7 +229,7 @@ let rec typeof env (t : debruijn_term) : debruijn_type =
let ty = typeof env t in
ty -- nth_type (TySum tys) tys i;
TySum tys
| Match (ty, t, brs) ->
let scrutinee_ty = typeof env t in
let tys = List.map (typeof_branch env scrutinee_ty) brs in