commit cc623dfe6e5bf45199824c718b939516a7b2285e
parent 8e0a0d1522a4cca7ee6d239085e9e7f05a48d14b
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 29 Jan 2024 03:11:00 -0800
Cleanup builtins, check new ones with factorial example
Diffstat:
15 files changed, 248 insertions(+), 131 deletions(-)
diff --git a/Makefile b/Makefile
@@ -10,12 +10,14 @@ SRC = \
node.ml \
env.ml \
ctx.ml \
+ builtin.ml \
concrete.ml \
abstract.ml \
internal.ml \
value.ml \
pretty.ml \
error.ml \
+ std.ml \
parser.ml \
lexer.ml \
desugar.ml \
diff --git a/abstract.ml b/abstract.ml
@@ -1,6 +1,7 @@
(* Abstract syntax is "desugared" concrete syntax. See desugar.ml. *)
open Node
+module B = Builtin
type var_name = var_name' node
and var_name' = Name.Var.t
@@ -20,7 +21,7 @@ and term' =
| DataType of multibinder Name.Tag.Map.t
| Nat of Z.t
| Var of var_name * int
-| Type (* Impossible to write in concrete syntax. Arises during desugaring. *)
+| Builtin of B.builtin (* Only arises during desugaring. *)
and definer = definer' node
and definer' = {
diff --git a/builtin.ml b/builtin.ml
@@ -0,0 +1,16 @@
+(* See also std.ml. *)
+
+type builtin =
+| Type
+| NatType
+| NatOpAdd
+| NatOpSub (* n < m => n - m = 0 *)
+| NatOpMul
+| NatOpDiv (* n / 0 = 0 *)
+| NatOpMod (* n % 0 = 0 *)
+| NatOpLt
+| NatOpLe
+| NatOpEq
+| NatOpGe
+| NatOpGt
+| NatOpNe
diff --git a/desugar.ml b/desugar.ml
@@ -1,8 +1,9 @@
open Util
open Node
-module E = Error
+module B = Builtin
module C = Concrete
module A = Abstract
+module E = Error
let add2 (x0, y0) (x1, y1) = (x0 + x1, y0 + y1)
@@ -86,17 +87,17 @@ let binop
= function
| C.LOr | C.LAnd ->
impossible "Desugar.binop: LOr and Land are handled specially"
-| C.Lt -> "`<"
-| C.Le -> "`<="
-| C.Eq -> "`="
-| C.Ge -> "`>`"
-| C.Gt -> "`>"
-| C.Ne -> "`<>"
-| C.Add -> "`+"
-| C.Sub -> "`-"
-| C.Mul -> "`*"
-| C.Div -> "`/"
-| C.Mod -> "`%"
+| C.Lt -> "<"
+| C.Le -> "<="
+| C.Eq -> "="
+| C.Ge -> ">"
+| C.Gt -> ">"
+| C.Ne -> "<>"
+| C.Add -> "+"
+| C.Sub -> "-"
+| C.Mul -> "*"
+| C.Div -> "/"
+| C.Mod -> "%"
let rec term
: C.term -> A.term
@@ -203,7 +204,7 @@ and domain
let p = patt p in
let p = p.loc @$ {
A.names = p.data.names;
- A.typs = Array.append [|Loc.Nowhere @$ A.Type|] p.data.typs;
+ A.typs = Array.append [|Loc.Nowhere @$ A.Builtin B.Type|] p.data.typs;
A.disc = p.data.disc;
} in
{A.plicity = Plicity.Im; A.patt = p}
diff --git a/elab.ml b/elab.ml
@@ -12,8 +12,6 @@ module V = Value
exception BlockedOnFuture of Uniq.uniq * int * Name.Var.t
-type context = V.value Ctx.context
-
type mode =
| Infer
| Check of V.value
@@ -40,7 +38,7 @@ let add_name'
(Name.Var.Set.add name name_set, name)
let rec assign_patt
-: context -> I.patt -> V.value -> Uniq.uniq -> context
+: V.context -> I.patt -> V.value -> Uniq.uniq -> V.context
= fun ctx {names; disc} vtyp var ->
let (ctx, _) = Ctx.assign ctx names vtyp (V.Arb var) in
@@ -105,35 +103,35 @@ let elaborate_args'
args
let rec infer
-: context -> A.term -> (I.term * V.value, E.error) result
+: V.context -> A.term -> (I.term * V.value, E.error) result
= fun ctx t ->
try Ok (infer' ctx t) with
| E.Exn e -> Error e
and infer'
-: context -> A.term -> I.term * V.value
+: V.context -> A.term -> I.term * V.value
= fun ctx t -> elaborate' ctx t Infer
and check
-: context -> A.term -> V.value -> (I.term, E.error) result
+: V.context -> A.term -> V.value -> (I.term, E.error) result
= fun ctx t vtyp ->
try Ok (check' ctx t vtyp) with
| E.Exn e -> Error e
and check'
-: context -> A.term -> V.value -> I.term
+: V.context -> A.term -> V.value -> I.term
= fun ctx t vtyp ->
let (t, _) = elaborate' ctx t (Check (force ctx.env vtyp)) in
t
and elaborate
-: context -> A.term -> mode -> (I.term * V.value, E.error) result
+: V.context -> A.term -> mode -> (I.term * V.value, E.error) result
= fun ctx t mode ->
try Ok (elaborate' ctx t mode) with
| E.Exn e -> Error e
and elaborate'
-: context -> A.term -> mode -> I.term * V.value
+: V.context -> A.term -> mode -> I.term * V.value
= fun ctx {loc; data = t} mode -> match t, mode with
| A.Let (definers, body), mode ->
let (ctx, definers) = infer_definers' ctx definers in
@@ -146,7 +144,7 @@ and elaborate'
(elaborate_match' ctx loc scrutinee cases vtyp, vtyp)
| A.Annot (tm, typ), Infer ->
- let typ = check' ctx typ V.Type in
+ let typ = check' ctx typ Std.v_Type in
let vtyp = eval ctx.env typ in
let tm = check' ctx tm vtyp in
(tm, vtyp)
@@ -215,8 +213,8 @@ and elaborate'
| A.FnType {data = {multibinder = domains; term = codomain}; _}, Infer ->
let (ctx, multibinder) = infer_multibinder' ctx loc domains in
- let codomain = check' ctx codomain V.Type in
- (I.FnType {multibinder; term = codomain}, V.Type)
+ let codomain = check' ctx codomain Std.v_Type in
+ (I.FnType {multibinder; term = codomain}, Std.v_Type)
| A.Data _, Infer -> E.abort loc E.ElabCantInferData
@@ -243,9 +241,9 @@ and elaborate'
ctors'.(i) <- multibinder;
i in
let names = Name.Tag.Map.map go ctors in
- (I.DataType {ctors = ctors'; names}, V.Type)
+ (I.DataType {ctors = ctors'; names}, Std.v_Type)
-| A.Nat n, Infer -> (I.Nat n, V.Builtin I.NatType)
+| A.Nat n, Infer -> (I.Nat n, Std.v_Nat)
| A.Var ({data = name; _}, i), Infer ->
begin match Ctx.lookup ctx name i with
@@ -254,10 +252,10 @@ and elaborate'
| None -> E.abort loc @@ E.ElabUnboundVar (name, i)
end
-| A.Type, Infer -> (I.Type, V.Type)
+| A.Builtin b, Infer -> (I.Builtin b, Std.infer b)
| (A.Annot _ | A.App _ | A.Fn _ | A.FnType _ | A.Data _ | A.DataType _
- | A.Nat _ | A.Var _ | A.Type) as t, Check vexpected ->
+ | A.Nat _ | A.Var _ | A.Builtin _) as t, Check vexpected ->
let (t, vinferred) = infer' ctx {loc; data = t} in
begin try unify ctx.env vexpected vinferred with
| UnifyFail ->
@@ -271,7 +269,7 @@ and elaborate'
* Return the elaborated terms and the multibinder's closure extended with
* fresh variables defined to the arguments' values. *)
and check_args'
-: context -> Loc.t -> A.term array -> V.environment -> I.multibinder
+: V.context -> Loc.t -> A.term array -> V.environment -> I.multibinder
-> I.term array * V.environment
= fun ctx loc explicit_args clo {binders; order} ->
let arity = Array.length binders in
@@ -304,7 +302,7 @@ and check_args'
* their delay + 1, and a β-redex uses the variables in the lambda with their
* delay - 1. *)
and infer_definers'
-: context -> A.definer array -> context * I.definer array
+: V.context -> A.definer array -> V.context * I.definer array
= fun ctx definers ->
let ndefiners = Array.length definers in
@@ -411,7 +409,7 @@ and infer_definers'
({ctx with env = !env}, definers')
and elaborate_match'
-: context -> Loc.t -> A.term -> A.case array -> V.value -> I.term
+: V.context -> Loc.t -> A.term -> A.case array -> V.value -> I.term
= fun ctx loc scrutinee cases body_vtyp ->
let (scrutinee, scrutinee_vtyp) = infer' ctx scrutinee in
let vars = Uniq.fresh 1 in
@@ -548,7 +546,7 @@ and elaborate_subswitch'
(* TODO: This has evolved into a complete disaster. Rewrite it. *)
and infer_multibinder'
-: context -> Loc.t -> A.multibinder -> context * I.multibinder
+: V.context -> Loc.t -> A.multibinder -> V.context * I.multibinder
= fun ctx loc {data = binders; _} ->
(* We generate a globally unique id for this multibinder so that we can
* determine which BlockedOnFuture exceptions belong to us (see below).
@@ -676,13 +674,14 @@ and infer_multibinder'
(ctx, {binders = binders'; order})
and infer_binder'
-: context -> A.binder -> Name.Var.t array * V.value
+: V.context -> A.binder -> Name.Var.t array * V.value
= fun ctx {loc; data = {plicity; patt}} ->
match infer_irrefutable_patt ctx Name.Var.Set.empty patt, plicity with
| Ok (_, names, vtyp), _ -> (names, vtyp)
| Error {data = E.ElabNonInferablePatt; _}, Plicity.Im ->
- begin match check_irrefutable_patt ctx Name.Var.Set.empty patt V.Type with
- | Ok (_, names) -> (names, V.Type)
+ begin match check_irrefutable_patt ctx Name.Var.Set.empty patt
+ Std.v_Type with
+ | Ok (_, names) -> (names, Std.v_Type)
| Error root -> E.abort loc @@ E.ElabUnannotImplicitIsType root
end
| Error ({data = E.ElabNonInferablePatt; _} as root), Plicity.Ex ->
@@ -692,10 +691,10 @@ and infer_binder'
(* Check that each term in the array starting at the given index is a type
* convertible to the given value. *)
and check_types'
-: context -> A.term array -> int -> V.value -> unit
+: V.context -> A.term array -> int -> V.value -> unit
= fun ctx typs start vtyp ->
for i = start to Array.length typs - 1 do
- let typ' = check' ctx typs.(i) V.Type in
+ let typ' = check' ctx typs.(i) Std.v_Type in
let vtyp' = eval ctx.env typ' in
try unify ctx.env vtyp vtyp' with
| UnifyFail ->
@@ -704,14 +703,14 @@ and check_types'
done
and infer_irrefutable_patt
-: context -> Name.Var.Set.t -> A.patt
+: V.context -> Name.Var.Set.t -> A.patt
-> (Name.Var.Set.t * Name.Var.t array * V.value, E.error) result
= fun ctx name_set patt ->
try Ok (infer_irrefutable_patt' ctx name_set patt) with
| E.Exn e -> Error e
and infer_irrefutable_patt'
-: context -> Name.Var.Set.t -> A.patt
+: V.context -> Name.Var.Set.t -> A.patt
-> Name.Var.Set.t * Name.Var.t array * V.value
= fun ctx name_set ({loc; _} as patt) ->
let (name_set, patt, vtyp) = infer_patt' ctx name_set patt in
@@ -720,14 +719,14 @@ and infer_irrefutable_patt'
| {names; disc = I.DWild _} -> (name_set, names, vtyp)
and check_irrefutable_patt
-: context -> Name.Var.Set.t -> A.patt -> V.value
+: V.context -> Name.Var.Set.t -> A.patt -> V.value
-> (Name.Var.Set.t * Name.Var.t array, E.error) result
= fun ctx name_set patt vtyp ->
try Ok (check_irrefutable_patt' ctx name_set patt vtyp) with
| E.Exn e -> Error e
and check_irrefutable_patt'
-: context -> Name.Var.Set.t -> A.patt -> V.value
+: V.context -> Name.Var.Set.t -> A.patt -> V.value
-> Name.Var.Set.t * Name.Var.t array
= fun ctx name_set ({loc; _} as patt) vtyp ->
let (name_set, patt) = check_patt' ctx name_set patt vtyp in
@@ -736,19 +735,19 @@ and check_irrefutable_patt'
| {names; disc = I.DWild _} -> (name_set, names)
and infer_patt'
-: context -> Name.Var.Set.t -> A.patt -> Name.Var.Set.t * I.patt * V.value
+: V.context -> Name.Var.Set.t -> A.patt -> Name.Var.Set.t * I.patt * V.value
= fun ctx name_set {loc; data = patt} -> match patt with
| {typs = [||]; _} -> E.abort loc E.ElabNonInferablePatt
| {names; typs; disc} ->
let (name_set, names) = Array.fold_left_map add_name' name_set names in
- let typ = check' ctx typs.(0) V.Type in
+ let typ = check' ctx typs.(0) Std.v_Type in
let vtyp = eval ctx.env typ in
check_types' ctx typs 1 vtyp;
let (names_set, disc) = check_disc' ctx name_set disc vtyp in
(name_set, {names; disc}, vtyp)
and check_patt'
-: context -> Name.Var.Set.t -> A.patt -> V.value -> Name.Var.Set.t * I.patt
+: V.context -> Name.Var.Set.t -> A.patt -> V.value -> Name.Var.Set.t * I.patt
= fun ctx name_set {loc; data = {names; typs; disc}} vtyp ->
let (name_set, names) = Array.fold_left_map add_name' name_set names in
check_types' ctx typs 0 vtyp;
@@ -756,7 +755,7 @@ and check_patt'
(name_set, {names; disc})
and check_disc'
-: context -> Name.Var.Set.t -> A.discriminant -> V.value
+: V.context -> Name.Var.Set.t -> A.discriminant -> V.value
-> Name.Var.Set.t * I.discriminant
= fun ctx name_set {loc; data = disc} vtyp -> match disc, force ctx.env vtyp with
| A.DWild, vtyp -> (name_set, I.DWild (quote ctx.env vtyp))
diff --git a/eval.ml b/eval.ml
@@ -1,4 +1,5 @@
open Util
+module B = Builtin
module I = Internal
module V = Value
@@ -42,6 +43,10 @@ let rec define_data_args
| _, I.DData _ ->
impossible "Eval.define_data_args: value is not data, but disc is"
+let lower_bool
+: bool -> V.value
+= fun b -> if b then Std.v_true else Std.v_false
+
let rec eval
: V.environment -> I.term -> V.value
= fun env -> function
@@ -75,7 +80,6 @@ let rec eval
| Some v -> v
| None -> Arb var
end
-| I.Type -> V.Type
| I.Builtin b -> V.Builtin b
and do_match
@@ -127,8 +131,20 @@ and apply
clo := Env.define !clo (Uniq.get vars i) args.(i)
done;
eval !clo body
-| V.Builtin I.NatOpAdd, [|V.Nat m; V.Nat n|] -> V.Nat (Z.add m n)
-| V.Builtin I.NatOpMul, [|V.Nat m; V.Nat n|] -> V.Nat (Z.mul m n)
+| V.Builtin B.NatOpAdd, [|V.Nat m; V.Nat n|] -> V.Nat (Z.add m n)
+| V.Builtin B.NatOpSub, [|V.Nat m; V.Nat n|] ->
+ V.Nat (if Z.lt m n then Z.zero else Z.sub m n)
+| V.Builtin B.NatOpMul, [|V.Nat m; V.Nat n|] -> V.Nat (Z.mul m n)
+| V.Builtin B.NatOpDiv, [|V.Nat m; V.Nat n|] ->
+ V.Nat (if Z.equal n Z.zero then Z.zero else Z.div m n)
+| V.Builtin B.NatOpMod, [|V.Nat m; V.Nat n|] ->
+ V.Nat (if Z.equal n Z.zero then Z.zero else Z.rem m n)
+| V.Builtin B.NatOpLt, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.lt m n
+| V.Builtin B.NatOpLe, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.leq m n
+| V.Builtin B.NatOpEq, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.equal m n
+| V.Builtin B.NatOpGe, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.geq m n
+| V.Builtin B.NatOpGt, [|V.Nat m; V.Nat n|] -> lower_bool @@ Z.gt m n
+| V.Builtin B.NatOpNe, [|V.Nat m; V.Nat n|] -> lower_bool @@ not (Z.equal m n)
| fn, args -> V.NeutralApp (fn, args)
(* TODO: This is inefficient. We should do something smarter, like lifting
diff --git a/internal.ml b/internal.ml
@@ -1,4 +1,5 @@
open Node
+module B = Builtin
(* Ideas for implicit args/metavariables/unification: Unlike in Andras's
* elaboration-zoo, we use globally fresh names in the semantic domain, so
@@ -32,11 +33,6 @@ open Node
(* TODO: When we actually start compiling to low-level code, we need to
* consider where types should be stored on internal terms. *)
-type builtin =
-| NatType
-| NatOpAdd
-| NatOpMul
-
type term =
| Let of definer array * term
| Match of {
@@ -56,8 +52,7 @@ type term =
| DataType of datatype
| Nat of Z.t
| Var of Index.t
-| Type
-| Builtin of builtin
+| Builtin of B.builtin
and definer = {
names: Name.Var.t array;
diff --git a/lexer.mll b/lexer.mll
@@ -29,7 +29,7 @@ let lgreek = "α" | "β" | "γ" | "δ" | "ε" | "ζ" | "η" | "θ" | "ι" | "κ"
let lgreekalt = "ϵ" | "ϑ" | "ϰ" | "ϖ" | "ϱ" | "ς" | "ϕ"
let greek = ugreek | lgreek | lgreekalt
-let comment = '\\' '\\' (ascii_horizontal | greek)*
+let comment = '\\' (ascii_horizontal | greek)*
(* Keep in sync with non_start and non_cont in name.ml. *)
let ident_start = latin | greek | '_'
diff --git a/main.ml b/main.ml
@@ -1,26 +1,28 @@
open Node
+module B = Builtin
module I = Internal
module V = Value
-(*
let buf = Lexing.from_string "\
+ \\comment :)\n\
N := [A: Type, A, A -> A] -> A;\n\
add: [N, N] -> N := fn m, n => fn A, z, s => m A (n A z s) s;\n\
two: N := fn A, z, s => s (s z);\n\
three: N := fn A, z, s => s (s (s z));\n\
- five := add two three;\n\
- five Nat 0 (fn n => n + 1)\n\
+ `f i v e` := add two three;\n\
+ `f i v e` Nat 0 (fn n => n + 1)\n\
"
-*)
+(*
let buf = Lexing.from_string "\
Bool := #{@false; @true};\n\
T := #(b: Bool, (if b then Nat else Type));\n\
- ((@true, 3): T match {\n\
+ ((@true, 3): T) match {\n\
(@true, n) => n,\n\
(@false, _) => 2,\n\
- }): Nat\n\
+ }: Nat\n\
"
+*)
(*
let buf = Lexing.from_string "\
@@ -61,33 +63,30 @@ let buf = Lexing.from_string "\
(*
let buf = Lexing.from_string "\
fact: Nat -> Nat := rec fn n =>\n\
- if eq n 0 then 1 else n * fact (n + 1);\n\
- fact 3\n\
+ if n = 0 then 1 else n * fact (n - 1);\n\
+ fact 6\n\
"
*)
let ctx =
- let nat_binder = {
- I.plicity = Plicity.Ex;
- I.patt = {
- I.names = [|Name.Var.Of "a"|];
- I.disc = I.DWild (I.Builtin I.NatType);
- };
- } in
- let nat_op_typ = V.FnTypeClosure (Env.empty, {
- multibinder = {binders = [|nat_binder; nat_binder|]; order = [|0; 1|]};
- term = I.Builtin I.NatType;
- }) in
- let ctx = Ctx.empty in
- let (ctx, _) = Ctx.assign ctx
- [|Name.Var.Of "Type"|] V.Type V.Type in
- let (ctx, _) = Ctx.assign ctx
- [|Name.Var.Of "Nat"|] V.Type (V.Builtin I.NatType) in
- let (ctx, _) = Ctx.assign ctx
- [|Name.Var.Of "`+"|] nat_op_typ (V.Builtin I.NatOpAdd) in
- let (ctx, _) = Ctx.assign ctx
- [|Name.Var.Of "`*"|] nat_op_typ (V.Builtin I.NatOpMul) in
- ctx
+ let ctx = ref Ctx.empty in
+ let assign s t v =
+ let (ctx', _) = Ctx.assign !ctx [|Name.Var.Of s|] t v in
+ ctx := ctx' in
+ assign "Type" Std.v_Type @@ V.Builtin B.Type;
+ assign "Nat" Std.v_Type @@ V.Builtin B.NatType;
+ assign "+" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpAdd;
+ assign "-" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpSub;
+ assign "*" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpMul;
+ assign "/" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpDiv;
+ assign "%" Std.v_Nat_Nat_arrow_Nat @@ V.Builtin B.NatOpMod;
+ assign "<" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpLt;
+ assign "<=" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpLe;
+ assign "=" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpEq;
+ assign ">=" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpGe;
+ assign ">" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpGt;
+ assign "<>" Std.v_Nat_Nat_arrow_Bool @@ V.Builtin B.NatOpNe;
+ !ctx
let print fmt a =
Format.set_margin 80;
diff --git a/parser.mly b/parser.mly
@@ -125,12 +125,17 @@ let loc () =
(* TODO: Syntactic sugar: Allow application in patterns, with the following
* interpretation:
- * p p1 ... pn := b ---> p := rec fn p1, ..., pn => b
+ * p p1 ... pn := rec? b ---> p := rec? fn p1, ..., pn => b
* fn ..., p(p1 ... pn), ... => b ---> fn ..., p1, ..., pn, ... => b
* The pattern p in the second rule is restricted to being a composition of
* PParen and PAnnot. Note that application of the first rule may make the
* second rule applicable, and application of the second rule may need to be
* iterated until we reach a "normal form". *)
+(* TODO: Probably we should change the match syntax when staging is added,
+ * so that we can write something like `$match x ...` instead of
+ * `$(x match ...)` for conditional compilation. *)
+(* TODO: Chaining relations? I.e., ability to write x < y < z instead of
+ * x < y && y < z. *)
start: expr0 EOF { term $1 }
@@ -142,25 +147,34 @@ expr0: (* Definitions and sequencing *)
| expr1 SEMICOLON expr0 { loc () @$ Seq ($1, $3) }
| expr1 { $1 }
-expr1: (* Control flow and functions *)
- (* TODO: Probably we should change the match syntax when staging is added,
- * so that we can write something like `$match x ...` instead of
- * `$(x match ...)` for conditional compilation. *)
- | expr2 MATCH LBRACE case_list RBRACE {
- let (len, lst) = $4 in
- loc () @$ Match($1, len, lst)
- }
- | IF cond THEN expr1 ELSE expr1 { loc () @$ If ($2, $4, $6) }
- | IFF cond DO expr1 { loc () @$ Iff ($2, $4) }
+expr1:
+ | expr1r COLON expr1l { loc () @$ Annot ($1, $3) }
+ | expr1ll { $1 }
+ | expr1rr { $1 }
+ | expr2 { $1 }
+
+expr1l: (* Prec 1 with a terminal to the left, OR prec >1 *)
+ | expr1ll { $1 }
+ | expr2 { $1 }
+expr1ll: (* Prec 1 with a terminal to the left *)
+ | IF cond THEN expr1 ELSE expr1l { loc () @$ If ($2, $4, $6) }
+ | IFF cond DO expr1l { loc () @$ Iff ($2, $4) }
| FN param_list DOUBLE_ARROW expr1 {
let (len, lst) = $2 in
loc () @$ Fn (len, lst, $4)
}
+
+expr1r: (* Prec 1 with a terminal to the right, OR prec >1 *)
+ | expr1rr { $1 }
| expr2 { $1 }
+expr1rr: (* Prec 1 with a terminal to the right *)
+ | expr1r MATCH LBRACE case_list RBRACE {
+ let (len, lst) = $4 in
+ loc () @$ Match($1, len, lst)
+ }
-expr2: (* Type annotations (right-associative) *)
- | expr3 COLON expr2 { loc () @$ Annot ($1, $3) }
- | expr3 { $1 }
+(* TODO: Remove this and shift all precedences? Ughh. *)
+expr2: expr3 { $1 }
expr3: (* Function arrow (right-associative) *)
| expr5 SINGLE_ARROW expr3 {
@@ -187,8 +201,6 @@ expr4b: (* Logical AND (left-associative) *)
| expr4c { $1 }
expr4c: (* Relations (non-associative) *)
- (* TODO: Chaining relations? I.e., ability to write x < y < z instead of
- * x < y && y < z. *)
| expr4d rel expr4d { loc () @$ BinOp ($1, $2, $3) }
| expr4d { $1 }
rel:
@@ -275,14 +287,14 @@ expr6_apposition_list:
| { (0, []) }
definer:
- | expr2 COLON_EQ expr1 { loc () @$ C.Definer (patt $1, term $3) }
- | expr2 COLON_EQ REC expr1 { loc () @$ C.RecDefiner (patt $1, term $4) }
+ | expr1 COLON_EQ expr1 { loc () @$ C.Definer (patt $1, term $3) }
+ | expr1 COLON_EQ REC expr1 { loc () @$ C.RecDefiner (patt $1, term $4) }
definer_list:
| definer COMMA definer_list { cons $1 $3 }
| definer { (1, [$1]) }
case:
- | expr2 DOUBLE_ARROW expr1 { loc () @$ C.Case (patt $1, term $3) }
+ | expr1 DOUBLE_ARROW expr1 { loc () @$ C.Case (patt $1, term $3) }
case_list:
| case COMMA case_list { cons $1 $3 }
| case { (1, [$1]) }
@@ -290,11 +302,11 @@ case_list:
cond:
| expr1 { loc () @$ C.TrueCond (term $1) }
- | expr2 COLON_EQ expr1 { loc () @$ C.PattCond (patt $1, term $3) }
+ | expr1 COLON_EQ expr1 { loc () @$ C.PattCond (patt $1, term $3) }
param:
- | expr2 { loc () @$ C.Param (Plicity.Ex, patt $1) }
- | QUESTION expr2 { loc () @$ C.Param (Plicity.Im, patt $2) }
+ | expr1 { loc () @$ C.Param (Plicity.Ex, patt $1) }
+ | QUESTION expr1 { loc () @$ C.Param (Plicity.Im, patt $2) }
param_list:
| param COMMA param_list { cons $1 $3 }
| param { (1, [$1]) }
@@ -306,7 +318,7 @@ domain:
| Annot (p, t) -> loc () @$ C.AnnotDomain (Plicity.Ex, patt p, term t)
| _ -> loc () @$ C.ExplicitDomain (term $1)
}
- | QUESTION expr2 {
+ | QUESTION expr1 {
match $2.data with
| Annot (p, t) -> loc () @$ C.AnnotDomain (Plicity.Im, patt p, term t)
| _ -> loc () @$ C.ImplicitTypeDomain (patt $2)
diff --git a/pretty.ml b/pretty.ml
@@ -1,5 +1,6 @@
module F = Format
open Node
+module B = Builtin
open Internal
let rec pp_print_with_parens
@@ -11,6 +12,7 @@ let rec pp_print_with_parens
end else
F.fprintf ppf
+(* TODO: Fix precedences given recent parser changes *)
and pp_print_term
: int -> F.formatter -> term -> unit
= fun m ppf -> function
@@ -43,10 +45,9 @@ and pp_print_term
(pp_print_term 3) codomain
| Data {tag; args; datatype; _} ->
- pp_print_with_parens m 2 ppf "@[@[<4>%a%a@]%t%a@]"
+ 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
- (F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
(pp_print_term 2) (DataType datatype)
| DataType {ctors; names} ->
@@ -64,10 +65,6 @@ and pp_print_term
pp_print_with_parens m 6 ppf "%a"
Index.pp_print ij
-| Type ->
- pp_print_with_parens m 6 ppf "%s"
- "~Type"
-
| Builtin b ->
pp_print_with_parens m 6 ppf "%a"
pp_print_builtin b
@@ -75,9 +72,8 @@ and pp_print_term
and pp_print_definer
: F.formatter -> definer -> unit
= fun ppf {names; rhs; typ} ->
- F.fprintf ppf "@[@[<hv 4>%a%t%a@;<1 -4>@]:=@;<1 4>%a@]"
+ F.fprintf ppf "@[@[<hv 4>%a:@;<1 4>%a@;<1 -4>@]:=@;<1 4>%a@]"
(pp_print_names 3) names
- (F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 0, ""))
(pp_print_term 2) typ
(pp_print_term 1) rhs
@@ -139,7 +135,7 @@ and pp_print_subswitches
let names = Array.of_list (Name.Tag.Map.to_list names) in
for i = 0 to Array.length subswitches - 1 do
let (tag, _) = names.(i) in
- F.fprintf ppf "@,@[%a =>@;<1 4>%a@],"
+ F.fprintf ppf "@,@[<v 4>@[%a@] => %a@],"
Name.Tag.pp_print tag
pp_print_switch subswitches.(i)
done;
@@ -161,10 +157,9 @@ and pp_print_binders
and pp_print_binder
: F.formatter -> binder -> unit
= fun ppf {plicity; patt = {names; disc}} ->
- F.fprintf ppf "@[%a%a%t%a@]"
+ F.fprintf ppf "@[%a%a:@;<1 4>%a@]"
pp_print_plicity plicity
(pp_print_names 3) names
- (F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
(pp_print_term 2) (disc_type disc)
and pp_print_plicity
@@ -191,11 +186,21 @@ and pp_print_ctors
) names
and pp_print_builtin
-: F.formatter -> builtin -> unit
+: F.formatter -> B.builtin -> unit
= fun ppf -> function
-| NatType -> F.fprintf ppf "~Nat"
-| NatOpAdd -> F.fprintf ppf "~+"
-| NatOpMul -> F.fprintf ppf "~*"
+| B.Type -> F.fprintf ppf "~Type"
+| B.NatType -> F.fprintf ppf "~Nat"
+| B.NatOpAdd -> F.fprintf ppf "~+"
+| B.NatOpSub -> F.fprintf ppf "~-"
+| B.NatOpMul -> F.fprintf ppf "~*"
+| B.NatOpDiv -> F.fprintf ppf "~/"
+| B.NatOpMod -> F.fprintf ppf "~%%"
+| B.NatOpLt -> F.fprintf ppf "~<"
+| B.NatOpLe -> F.fprintf ppf "~<="
+| B.NatOpEq -> F.fprintf ppf "~="
+| B.NatOpGe -> F.fprintf ppf "~>="
+| B.NatOpGt -> F.fprintf ppf "~>"
+| B.NatOpNe -> F.fprintf ppf "~<>"
and pp_print_names
: int -> F.formatter -> Name.Var.t array -> unit
diff --git a/quote.ml b/quote.ml
@@ -49,7 +49,6 @@ let rec quote
| Some ij -> I.Var ij
| None -> impossible "Eval.quote: env does not bind variable"
end
-| V.Type -> I.Type
| V.Builtin b -> I.Builtin b
| V.Future _ -> impossible "Eval.quote: can not quote future"
diff --git a/std.ml b/std.ml
@@ -0,0 +1,71 @@
+module B = Builtin
+module I = Internal
+module V = Value
+
+let t_Nat: I.term = I.Builtin B.NatType
+let v_Nat: V.value = V.Builtin B.NatType
+
+let t_Type: I.term = I.Builtin B.Type
+let v_Type: V.value = V.Builtin B.Type
+
+let dt_Bool: I.datatype =
+ {
+ ctors = [|
+ {binders = [||]; order = [||]};
+ {binders = [||]; order = [||]};
+ |];
+ names = Name.Tag.Map.add (Name.Tag.Of "false") 0
+ @@ Name.Tag.Map.add (Name.Tag.Of "true") 1 Name.Tag.Map.empty;
+ }
+let t_Bool: I.term = I.DataType dt_Bool
+let v_Bool: V.value = V.DataTypeClosure (Env.empty, dt_Bool)
+
+let v_false: V.value =
+ V.Data {
+ tag = Name.Tag.Of "false";
+ tagi = 0;
+ args = [||];
+ datatype_clo = (Env.empty, dt_Bool);
+ }
+
+let v_true: V.value =
+ V.Data {
+ tag = Name.Tag.Of "true";
+ tagi = 1;
+ args = [||];
+ datatype_clo = (Env.empty, dt_Bool);
+ }
+
+let v_Nat_Nat_arrow
+: I.term -> V.value
+= fun cod ->
+ let nat_binder = {
+ I.plicity = Plicity.Ex;
+ I.patt = {
+ I.names = [||];
+ I.disc = I.DWild t_Nat;
+ };
+ } in
+ V.FnTypeClosure (Env.empty, {
+ multibinder = {binders = [|nat_binder; nat_binder|]; order = [|0; 1|]};
+ term = cod;
+ })
+let v_Nat_Nat_arrow_Nat: V.value = v_Nat_Nat_arrow t_Nat
+let v_Nat_Nat_arrow_Bool: V.value = v_Nat_Nat_arrow t_Bool
+
+let infer
+: B.builtin -> V.value
+= function
+| B.Type -> v_Type
+| B.NatType -> v_Type
+| B.NatOpAdd -> v_Nat_Nat_arrow_Nat
+| B.NatOpSub -> v_Nat_Nat_arrow_Nat
+| B.NatOpMul -> v_Nat_Nat_arrow_Nat
+| B.NatOpDiv -> v_Nat_Nat_arrow_Nat
+| B.NatOpMod -> v_Nat_Nat_arrow_Nat
+| B.NatOpLt -> v_Nat_Nat_arrow_Bool
+| B.NatOpLe -> v_Nat_Nat_arrow_Bool
+| B.NatOpEq -> v_Nat_Nat_arrow_Bool
+| B.NatOpGe -> v_Nat_Nat_arrow_Bool
+| B.NatOpGt -> v_Nat_Nat_arrow_Bool
+| B.NatOpNe -> v_Nat_Nat_arrow_Bool
diff --git a/unify.ml b/unify.ml
@@ -42,13 +42,11 @@ let rec unify
conv_datatype env clo0 clo1 datatype0 datatype1
| V.Nat n, V.Nat m -> if not @@ Z.equal n m then raise UnifyFail
| V.Arb var0, V.Arb var1 -> if var0 <> var1 then raise UnifyFail
-| V.Type, V.Type -> ()
| V.Builtin b0, V.Builtin b1 -> if b0 <> b1 then raise UnifyFail
| V.Future _, _ -> impossible "Unify.unify: Futures do not unify"
| _, V.Future _ -> impossible "Unify.unify: Futures do not unify"
| (V.NeutralMatch _ | V.NeutralApp _ | V.FnClosure _ | V.FnTypeClosure _
- | V.Data _ | V.DataTypeClosure _ | V.Nat _ | V.Arb _ | V.Type
- | V.Builtin _), _ ->
+ | V.Data _ | V.DataTypeClosure _ | V.Nat _ | V.Arb _ | V.Builtin _), _ ->
raise UnifyFail
and conv
diff --git a/value.ml b/value.ml
@@ -1,3 +1,4 @@
+module B = Builtin
module I = Internal
type value =
@@ -20,10 +21,12 @@ type value =
| Nat of Z.t
| Arb of Uniq.uniq
(*| Meta of ...*)
-| Type
-| Builtin of I.builtin
+| Builtin of B.builtin
| Future of Uniq.uniq * int
and environment = value Env.environment
and 'a closure = environment * 'a
+
+type context = value Ctx.context
+
