commit 0f8ed905de3ec4f365268a8b523933f55945185c
parent 796bd77fe16a3575fa41d22b26510dbd470f4acd
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Mon, 8 Jan 2024 18:30:27 -0800
Test data and datatypes
Diffstat:
6 files changed, 26 insertions(+), 5 deletions(-)
diff --git a/.gitignore b/.gitignore
@@ -7,3 +7,4 @@ parser.output
test
test2
main
+*.out
diff --git a/Makefile b/Makefile
@@ -23,7 +23,7 @@ SRC = \
main.ml
main: $(SRC)
- ocamlfind ocamlopt -o $@ -g -linkpkg -package zarith $^
+ ocamlfind ocamlc -o $@ -g -linkpkg -package zarith $^
lexer.ml: lexer.mll
ocamllex lexer.mll
diff --git a/internal.ml b/internal.ml
@@ -81,8 +81,16 @@ let rec write_term buf = function
P.at 3 P.fold_left buf ", " write_binder binders;
P.string buf "] -> ";
P.at 3 write_term buf codomain
-| Data _ -> no_impl "write data"
-| DataType _ -> no_impl "write datatype"
+| Data (tag, args) ->
+ P.parens buf 6 @@ fun () ->
+ P.at 7 P.string buf (Tag.to_string tag);
+ P.string buf " ";
+ P.at 7 P.fold_left buf " " write_term args
+| DataType ctors ->
+ P.parens buf 7 @@ fun () ->
+ P.string buf "#{";
+ P.at 3 P.fold_left buf "; " write_ctor (Array.of_list (Tag.Map.to_list ctors));
+ P.string buf "}"
| Nat n ->
P.parens buf 7 @@ fun () ->
P.string buf (Z.to_string n)
@@ -115,6 +123,13 @@ and write_binder buf = function
| {plicity = Plicity.Ex; typ} ->
write_term buf typ
+and write_ctor buf (tag, {binders; _}) =
+ P.string buf (Tag.to_string tag);
+ begin if Array.length binders > 0 then
+ P.string buf " ";
+ P.at 3 P.fold_left buf ", " write_binder binders
+ end
+
let to_string t =
let buf = P.make 128 in
write_term buf t;
diff --git a/main.ml b/main.ml
@@ -1,6 +1,7 @@
module I = Internal
module V = Value
+(*
let buf = Lexing.from_string "\
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\
@@ -9,7 +10,9 @@ let buf = Lexing.from_string "\
five := add two three;\n\
five Nat 0 (fn n => n + 1)\n\
"
-(*let buf = Lexing.from_string "T := #[@a Nat; @b #()]; @a 3 : T"*)
+*)
+let buf = Lexing.from_string "\
+T := #{@a Nat; @b #()}; @a 3 : T"
let concrete =
try Parser.start Lexer.token buf with
diff --git a/parser.mly b/parser.mly
@@ -56,7 +56,7 @@ let rec term {loc; data = e} = loc @$ match e with
| Match (scrutinee, len, cases) -> C.Match (term scrutinee, to_array len cases)
| If (c, t, f) -> C.If (term c, term t, term f)
| Iff (c, t) -> C.Iff (term c, term t)
-| Annot (a, b) -> C.Iff (term a, term b)
+| Annot (a, b) -> C.Annot (term a, term b)
| Add (a, b) -> C.Add (term a, term b)
| Mul (a, b) -> C.Mul (term a, term b)
| Or _ -> error loc "'|' can not appear in terms (yet)"
diff --git a/tag.ml b/tag.ml
@@ -1,6 +1,8 @@
type tag = Of of string
type t = tag
+let to_string (Of x) = "@" ^ x
+
module Map = Map.Make(struct
type t = tag
let compare (Of x) (Of y) = String.compare x y
