commit 680d5ffc27c92e9f504ced9ebd714f403d9174a6
parent cf53b44cb71672987ab0f078f94b0645eb646398
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Tue, 19 Dec 2023 22:34:37 -0800
Return to working condition
Diffstat:
| M | Makefile | | | 20 | ++++++++++++++++++-- |
| M | common.ml | | | 5 | ----- |
| M | elab.ml | | | 69 | +++++++++++++++++++++++++++++++++++++-------------------------------- |
| M | eval.ml | | | 34 | +++++++++++++++++----------------- |
| M | main.ml | | | 11 | ++++------- |
| M | value.ml | | | 10 | +++++----- |
6 files changed, 81 insertions(+), 68 deletions(-)
diff --git a/Makefile b/Makefile
@@ -1,4 +1,20 @@
-main: loc.ml node.ml common.ml field.ml concrete.ml parser.ml lexer.ml abstract.ml cnctoabs.ml main.ml #core.ml value.ml eval.ml elab.ml main.ml
+SRC = \
+ loc.ml \
+ node.ml \
+ common.ml \
+ field.ml \
+ concrete.ml \
+ parser.ml \
+ lexer.ml \
+ abstract.ml \
+ cnctoabs.ml \
+ internal.ml \
+ value.ml \
+ eval.ml \
+ elab.ml \
+ main.ml
+
+main: $(SRC)
ocamlfind ocamlopt -o $@ -g -linkpkg -package zarith $^
lexer.ml: lexer.mll
@@ -6,7 +22,7 @@ lexer.ml: lexer.mll
parser.ml: parser.mly
ocamlyacc -v parser.mly
- rm parser.mli # Hack
+ @rm parser.mli # Hack
.PHONY: clean
clean:
diff --git a/common.ml b/common.ml
@@ -2,11 +2,6 @@ type ident = string
type index = int
type level = int
-(*
-exception Error of loc * msg
-let error loc msg = raise (TypeError)
-*)
-
(* Short-circuiting AND fold_left. *)
let rec all2 f xs ys = match xs, ys with
| x :: xs, y :: ys -> f x y && all2 f xs ys
diff --git a/elab.ml b/elab.ml
@@ -4,6 +4,10 @@ module A = Abstract
module I = Internal
module V = Value
+exception ElabError of Loc.t * string
+
+let error loc msg = raise (ElabError (loc, msg))
+
(* TODO: use a hashtable or map for ident -> level lookups *)
type context = {
len: int;
@@ -47,8 +51,8 @@ let bind_def ctx x v a = {
(* Add `x : a` to ctx. *)
let bind_arb ctx x a = bind_def ctx x (V.Arb ctx.len) a
-let rec infer ctx = function
-| A.Let (A.PAnnot (p, a), scrutinee, body) ->
+let rec infer ctx (Node.Of (loc, t)) = match t with
+| A.Let (Node.Of (_, A.PAnnot (p, a)), scrutinee, body) ->
let a = check ctx a (V.Intrin I.Type) in
let va = eval ctx.values a in
let x = check_patt ctx p va in
@@ -63,17 +67,17 @@ let rec infer ctx = function
let (body, vb) = infer (bind_def ctx x vscrutinee va) body in
(I.Let (scrutinee, body), vb)
| A.Match _ -> failwith "no impl: match"
-| A.Annot (tm, a) ->
+| A.Annot (t, a) ->
let a = check ctx a (V.Intrin I.Type) in
let va = eval ctx.values a in
- let tm = check ctx tm va in
- (tm, va)
+ let t = check ctx t va in
+ (t, va)
| A.App (f, args) ->
let (f, fty) = infer ctx f in
begin match fty with
| V.FnType (env, arity, doms, cod) ->
if List.length args <> arity then
- failwith "type error: arity mismatch in application"
+ error loc "arity mismatch in application"
else
let rec go env args doms = match args, doms with
| arg :: args, dom :: doms ->
@@ -86,21 +90,18 @@ let rec infer ctx = function
| _, _ -> failwith "impossible" in
let (args, vcod) = go env args doms in
(I.App (f, args), vcod)
- | _ -> failwith "type error: expected function type in application"
+ | _ -> error loc "expected function in application"
end
-| A.Access _ -> failwith "no impl: access"
-| A.Index _ -> failwith "no impl: index"
-| A.Deref _ -> failwith "no impl: deref"
| A.Fn (ps, body) ->
let rec go ctx = function
- | A.PAnnot (p, dom) :: ps ->
+ | Node.Of (_, A.PAnnot (p, dom)) :: ps ->
let dom = check ctx dom (V.Intrin I.Type) in
let vdom = eval ctx.values dom in
let x = check_patt ctx p vdom in
let (body, doms, vcod) = go (bind_arb ctx x vdom) ps in
(body, dom :: doms, vcod)
- | _ :: ps ->
- failwith "type error: can not infer type for unannotated function parameter"
+ | Node.Of (loc, _) :: _ ->
+ error loc "can not infer type for unannotated function parameter"
| [] ->
let (body, vcod) = infer ctx body in
(body, [], vcod) in
@@ -111,15 +112,18 @@ let rec infer ctx = function
| A.FnType (anns, cod) ->
let arity = List.length anns in
let rec go ctx = function
- | (p, dom) :: anns ->
- let cdom = check ctx dom (V.Intrin I.Type) in
- let vdom = eval ctx.values cdom in
+ | Node.Of (_, ann) :: anns ->
+ let (p, dom) = match ann with
+ | A.AType dom -> (Loc.None @$ A.PWild, dom)
+ | A.APatt (p, dom) -> (p, dom) in
+ let dom = check ctx dom (V.Intrin I.Type) in
+ let vdom = eval ctx.values dom in
let x = check_patt ctx p vdom in
- let (cdoms, ccod) = go (bind_arb ctx x vdom) anns in
- (cdom :: cdoms, ccod)
+ let (doms, cod) = go (bind_arb ctx x vdom) anns in
+ (dom :: doms, cod)
| [] -> ([], check ctx cod (V.Intrin I.Type)) in
- let (cdoms, ccod) = go ctx anns in
- (I.FnType (arity, cdoms, ccod), V.Intrin I.Type)
+ let (doms, cod) = go ctx anns in
+ (I.FnType (arity, doms, cod), V.Intrin I.Type)
| A.Data _ -> failwith "no impl: data"
| A.DataType _ -> failwith "no impl: data type"
| A.Nat n -> (I.Nat n, V.Intrin I.NatType)
@@ -127,13 +131,13 @@ let rec infer ctx = function
let rec go i ys ts = match ys, ts with
| Some y :: ys, t :: ts -> if x = y then (I.Var i, t) else go (i + 1) ys ts
| None :: ys, _ :: ts -> go (i + 1) ys ts
- | [], [] -> failwith ("unbound identifier: " ^ x)
+ | [], [] -> error loc ("unbound identifier: " ^ x)
| _, _ -> failwith "impossible" in
go 0 ctx.names ctx.types
-and check ctx tm vty = match tm, vty with
+and check ctx (Node.Of (loc, t') as t) va = match t', va with
(* TODO: Match, Data *)
-| A.Let (A.PAnnot (p, a), scrutinee, body), vb ->
+| A.Let (Node.Of (_, A.PAnnot (p, a)), scrutinee, body), vb ->
let a = check ctx a (V.Intrin I.Type) in
let va = eval ctx.values a in
let x = check_patt ctx p va in
@@ -149,7 +153,7 @@ and check ctx tm vty = match tm, vty with
I.Let (scrutinee, body)
| A.Fn (ps, body), V.FnType (env, arity, doms, cod) ->
if List.length ps <> arity then
- failwith "type error: arity mismatch"
+ error loc "arity mismatch"
else
let rec go ctx ps env doms = match ps, doms with
| p :: ps, dom :: doms ->
@@ -164,24 +168,25 @@ and check ctx tm vty = match tm, vty with
| _, _ -> failwith "impossible" in
let cbody = go ctx ps env doms in
I.Fn (arity, cbody)
-| tm, vexpected ->
- let (tm, vinferred) = infer ctx tm in
+| _, vexpected ->
+ let (t, vinferred) = infer ctx t in
if conv ctx.len vexpected vinferred then
- tm
+ t
else
- failwith "type error: expected/inferred mismatch"
+ (* TODO: pretty-print types *)
+ error loc "expected/inferred mismatch"
-and check_patt ctx {loc; x = p} va = match p with
+and check_patt ctx (Node.Of (loc, p)) va = match p with
| A.PWild -> None
| A.PBind x -> Some x
-| A.PAssign _ -> failwith "no impl: assign pattern"
| A.PAnnot (p, b) ->
let b = check ctx b (V.Intrin I.Type) in
- let vb = eval ctx.values cb in
+ let vb = eval ctx.values b in
if conv ctx.len va vb then
check_patt ctx p va
else
- failwith "pattern does not unify with inferred type"
+ (* TODO: pretty-print types *)
+ error loc "pattern does not unify with inferred type"
| A.PData _ -> failwith "no impl: data pattern"
| A.PNat _ -> failwith "no impl: nat pattern"
| A.PAnd _ -> failwith "no impl: and pattern"
diff --git a/eval.ml b/eval.ml
@@ -1,5 +1,5 @@
open Common
-module C = Core
+module I = Internal
module V = Value
(* Extend env with values Arb l, Arb (l+1), ..., Arb (l+n-1). *)
@@ -9,31 +9,31 @@ let weaken env l n =
go env l
let rec eval env = function
-| C.Let (scrutinee, body) -> eval (eval env scrutinee :: env) body
-| C.Case _ -> failwith "no impl: case"
-| C.App (f, args) ->
+| I.Let (scrutinee, body) -> eval (eval env scrutinee :: env) body
+| I.Case _ -> failwith "no impl: case"
+| I.App (f, args) ->
begin match eval env f, List.map (eval env) args with
(* β-reduction *)
| V.Fn (cap, _, body), vargs -> eval (List.rev_append vargs cap) body
- | V.Intrin C.NatOpAdd, [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
- | V.Intrin C.NatOpMul, [V.Nat m; V.Nat n] -> V.Nat (Z.mul m n)
+ | V.Intrin I.NatOpAdd, [V.Nat m; V.Nat n] -> V.Nat (Z.add m n)
+ | V.Intrin I.NatOpMul, [V.Nat m; V.Nat n] -> V.Nat (Z.mul m n)
(* neutral application *)
| vf, vargs -> V.App (vf, vargs)
end
-| C.Fn (arity, body) -> V.Fn (env, arity, body)
-| C.FnType (arity, doms, cod) -> V.FnType (env, arity, doms, cod)
-| C.Nat n -> V.Nat n
-| C.Var i -> List.nth env i
-| C.Intrin a -> V.Intrin a
+| I.Fn (arity, body) -> V.Fn (env, arity, body)
+| I.FnType (arity, doms, cod) -> V.FnType (env, arity, doms, cod)
+| I.Nat n -> V.Nat n
+| I.Var i -> List.nth env i
+| I.Intrin a -> V.Intrin a
(* TODO: quote of eval normalizes terms; in some cases below, we probabaly
* don't need to eval before quoting *)
let rec quote l = function
| V.Case _ -> failwith "no impl: case"
-| V.App (f, args) -> C.App (quote l f, List.map (quote l) args)
+| V.App (f, args) -> I.App (quote l f, List.map (quote l) args)
| V.Fn (env, arity, body) ->
let vbody = eval (weaken env l arity) body in
- C.Fn (arity, quote (l + arity) vbody)
+ I.Fn (arity, quote (l + arity) vbody)
| V.FnType (env, arity, doms, cod) ->
let rec go l env = function
| dom :: doms ->
@@ -42,10 +42,10 @@ let rec quote l = function
(cdom :: cdoms, ccod)
| [] -> ([], quote l (eval env cod)) in
let (cdoms, ccod) = go l env doms in
- C.FnType (arity, cdoms, ccod)
-| V.Nat n -> C.Nat n
-| V.Arb i -> C.Var (l - i - 1)
-| V.Intrin a -> C.Intrin a
+ I.FnType (arity, cdoms, ccod)
+| V.Nat n -> I.Nat n
+| V.Arb i -> I.Var (l - i - 1)
+| V.Intrin a -> I.Intrin a
let rec quote_telescope l = function
| t :: ts -> quote l t :: quote_telescope (l + 1) ts
diff --git a/main.ml b/main.ml
@@ -7,14 +7,11 @@ let buf = Lexing.from_string "\
three: N := fn A, z, s => s (s (s z));\
five := add two three;\
five Nat 0 (fn n => n + 1)\
- ≈
"
let concrete = Parser.start Lexer.token buf
let abstract = Cnctoabs.term concrete
-(*
let ctx = Elab.default_ctx
-let (core, core_type) = Elab.infer ctx abstract
-let norm = Eval.quote ctx.len (Eval.eval ctx.values core)
-let () = print_endline (Core.to_string 0 core)
-let () = print_endline (Core.to_string 0 norm)
-*)
+let (internal, ty) = Elab.infer ctx abstract
+let internal' = Eval.quote ctx.len (Eval.eval ctx.values internal)
+let () = print_endline (Internal.to_string 0 internal)
+let () = print_endline (Internal.to_string 0 internal')
diff --git a/value.ml b/value.ml
@@ -1,12 +1,12 @@
open Common
-module C = Core
+module I = Internal
type value =
-| Case of value * environ * C.case list
+| Case of value * environ * I.case list
| App of value * value list
-| Fn of environ * int * C.term
-| FnType of environ * int * C.term list * C.term
+| Fn of environ * int * I.term
+| FnType of environ * int * I.term list * I.term
| Nat of Z.t
| Arb of level
-| Intrin of C.intrin
+| Intrin of I.intrin
and environ = value list
