commit 1b84163cd6506ed3c7efae7a18a656ea382cae49
parent a56d4e7da22851289923593d8fb4751ec4092128
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 29 Jan 2024 19:25:44 -0800
Make tuples inferrable
Diffstat:
5 files changed, 59 insertions(+), 16 deletions(-)
diff --git a/abstract.ml b/abstract.ml
@@ -18,6 +18,7 @@ and term' =
| Fn of abstraction
| FnType of abstraction
| Data of tag_name * term array
+| TupleData of term array (* Can be inferred, unlike regular Data. *)
| DataType of multibinder Name.Tag.Map.t
| Nat of Z.t
| Var of var_name * int
diff --git a/desugar.ml b/desugar.ml
@@ -152,11 +152,14 @@ let rec term
let ctors = Array.fold_left insert Name.Tag.Map.empty ctors in
loc @$ A.DataType ctors
| C.Tuple fields ->
- let tag = synth_tag_name (string_of_int (Array.length fields)) in
- loc @$ A.Data (tag, Array.map term fields)
+ loc @$ A.TupleData (Array.map term fields)
| C.TupleType doms ->
let tag = Name.Tag.Of (string_of_int (Array.length doms)) in
- let binders = array_loc doms @$ Array.map domain doms in
+ let binders =
+ if Array.length doms = 0 then
+ Loc.Nowhere @$ [||]
+ else
+ array_loc doms @$ Array.map domain doms in
loc @$ A.DataType (Name.Tag.Map.singleton tag binders)
| C.Unit -> loc @$ A.Data (synth_tag_name "0", [||])
| C.Nat n -> loc @$ A.Nat n
diff --git a/elab.ml b/elab.ml
@@ -235,6 +235,41 @@ and elaborate'
let typ = quote ctx.env vtyp in
E.abort loc @@ E.ElabExpectedDataType typ
+| A.TupleData args, Infer ->
+ let arity = Array.length args in
+
+ (* Only needed so that the indices in the type are correct. *)
+ let vars = Uniq.fresh arity in
+ let clo = Env.bind ctx.env vars in
+
+ let args' = Array.make arity garbage in
+ let binders = Array.make arity garbage in
+ for i = 0 to arity - 1 do
+ let (arg', vtyp) = infer' ctx args.(i) in
+ args'.(i) <- arg';
+ let typ = quote clo vtyp in
+ binders.(i) <- {
+ I.plicity = Plicity.Ex;
+ I.patt = {
+ names = [||];
+ disc = DWild typ;
+ };
+ }
+ done;
+
+ let tag = Name.Tag.Of (string_of_int arity) in
+ let datatype = {
+ I.ctors = [|{binders; order = Array.init arity Fun.id}|];
+ I.names = Name.Tag.Map.singleton tag 0;
+ } in
+ (I.Data {tag; tagi = 0; args = args'; datatype},
+ V.DataTypeClosure (clo, datatype))
+
+| A.TupleData args, Check vtyp ->
+ (* XXX: Kinda hacky. *)
+ let tag = Name.Tag.Of (string_of_int (Array.length args)) in
+ elaborate' ctx (loc @$ A.Data (Loc.Nowhere @$ tag, args)) (Check vtyp)
+
| A.DataType ctors, Infer ->
let next = ref 0 in
let ctors' = Array.make (Name.Tag.Map.cardinal ctors) garbage in
diff --git a/main.ml b/main.ml
@@ -74,7 +74,7 @@ let buf = Lexing.from_string "\
Opt := fn A: Type => #{@some A; @none};\n\
div: [Nat, Nat] -> Opt Nat := fn m, n =>\n\
if n = 0 then @none else @some (m / n);\n\
- (div 3 0, div 12 3): #(Opt Nat, Opt Nat)\n\
+ (div 3 0, div 12 3)\n\
"
let ctx =
diff --git a/pretty.ml b/pretty.ml
@@ -13,7 +13,7 @@ let rec pp_print_with_parens
F.fprintf ppf
(* TODO: Fix precedences given recent parser changes *)
-and pp_print_term
+let rec pp_print_term
: int -> F.formatter -> term -> unit
= fun m ppf -> function
| Let (definers, body) ->
@@ -28,7 +28,7 @@ and pp_print_term
pp_print_switch switch
| App (fn, args) ->
- pp_print_with_parens m 5 ppf "@[<4>%a%a@]"
+ pp_print_with_parens m 5 ppf "@[<4>%a@ %a@]"
(pp_print_term 6) fn
pp_print_args args
@@ -45,10 +45,17 @@ and pp_print_term
(pp_print_term 3) codomain
| Data {tag; args; datatype; _} ->
- pp_print_with_parens m 2 ppf "@[<hv>@[<4>%a%a@]:@;<1 4>%a@;<0 -4>@]"
- Name.Tag.pp_print tag
- pp_print_args args
- (pp_print_term 2) (DataType datatype)
+ begin match args with
+ | [||] ->
+ pp_print_with_parens m 6 ppf "@[%a@]"
+ Name.Tag.pp_print tag
+ | args ->
+ (*pp_print_with_parens m 2 ppf "@[<hv 4>@[<4>%a%a@]:@ %a@;<0 -4>@]"*)
+ pp_print_with_parens m 2 ppf "@[<4>%a@ %a@]"
+ Name.Tag.pp_print tag
+ pp_print_args args
+ (*(pp_print_term 2) (DataType datatype)*)
+ end
| DataType {ctors; names} ->
pp_print_with_parens m 6 ppf "@[@[<hv 4>#{@,%a%t@]}@]"
@@ -72,7 +79,7 @@ and pp_print_term
and pp_print_definer
: F.formatter -> definer -> unit
= fun ppf {names; rhs; typ} ->
- F.fprintf ppf "@[@[<hv 4>%a:@;<1 4>%a@;<1 -4>@]:=@;<1 4>%a@]"
+ F.fprintf ppf "@[@[<hv 4>%a:@ %a@;<1 -4>@]:=@;<1 4>%a@]"
(pp_print_names 3) names
(pp_print_term 2) typ
(pp_print_term 1) rhs
@@ -143,11 +150,8 @@ and pp_print_subswitches
and pp_print_args
: F.formatter -> term array -> unit
-= fun ppf -> function
-| [||] -> () (* This only happens for Data, not App. *)
-| args ->
- F.fprintf ppf "@ %a"
- (F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_term 6)) args
+= fun ppf args ->
+ F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_term 6) ppf args
and pp_print_binders
: F.formatter -> binder array -> unit
