commit 5bb93471b62efc8ce1f7cc6cd9b9e0c10e34c93a
parent ca5579829cd533e5a88e9859b25cb5fe20def135
Author: Robert Russell <robertrussell.72001@gmail.com>
Date: Tue, 23 Jan 2024 22:06:56 -0800
Back to an ostensibly working state
Diffstat:
| M | abstract.ml | | | 25 | +++++++++++++++---------- |
| M | concrete.ml | | | 10 | +++++----- |
| M | ctx.ml | | | 38 | ++++++++++++++++++++++++++------------ |
| M | desugar.ml | | | 204 | +++++++++++++++++++++++++++++++++++++++++++++++++++---------------------------- |
| M | elab.ml | | | 304 | +++++++++++++++++++++++++++++++++++++++---------------------------------------- |
| M | env.ml | | | 38 | +++++++++++++++++++++++++++----------- |
| M | error.ml | | | 15 | +++++---------- |
| M | eval.ml | | | 42 | +++++++++++++++++++++++++++--------------- |
| M | inc_array.ml | | | 12 | +++++++++--- |
| M | index.ml | | | 4 | +++- |
| M | internal.ml | | | 87 | ++++++++++++++++++++++++++++++------------------------------------------------- |
| M | loc.ml | | | 20 | ++++++++++++++++++-- |
| M | main.ml | | | 19 | +++++++++---------- |
| M | name.ml | | | 35 | ++++++++++++++++++++++------------- |
| M | parser.mly | | | 36 | +++++++++++++++++++++--------------- |
| M | porig.ml | | | 3 | ++- |
| M | pretty.ml | | | 45 | ++++++++++++++++++++------------------------- |
| M | quote.ml | | | 173 | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++-------------------- |
| M | unify.ml | | | 193 | +++++++++++++++++++++++++++++++++++++++++++++++++++---------------------------- |
| M | uniq.ml | | | 23 | ++++++++++++++++++----- |
| M | util.ml | | | 15 | +++++++++++---- |
| M | value.ml | | | 25 | +++++++++++-------------- |
22 files changed, 819 insertions(+), 547 deletions(-)
diff --git a/abstract.ml b/abstract.ml
@@ -5,8 +5,8 @@ open Node
type var_name = var_name' node
and var_name' = Name.Var.t
-type ctor_name = ctor_name' node
-and ctor_name' = Name.Ctor.t
+type tag_name = tag_name' node
+and tag_name' = Name.Tag.t
type term = term' node
and term' =
@@ -14,10 +14,10 @@ and term' =
| Match of term * case array
| Annot of term * term
| App of term * term array
-| Fn of binder array * term
-| FnType of binder array * term
-| Data of ctor_name * term array
-| DataType of ctor Name.Ctor.Map.t
+| Fn of abstraction
+| FnType of abstraction
+| Data of tag_name * term array
+| 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. *)
@@ -39,11 +39,16 @@ and binder = binder' node
and binder' = {
plicity: Plicity.t;
patt: patt;
- typ: term option;
}
-and ctor = ctor' node
-and ctor' = Ctor of binder array
+and multibinder = multibinder' node
+and multibinder' = binder array
+
+and abstraction = abstraction' node
+and abstraction' = {
+ multibinder: multibinder;
+ term: term;
+}
and patt = patt' node
and patt' = {
@@ -56,6 +61,6 @@ and discriminant = discriminant' node
and discriminant' =
| DWild
| DData of {
- tag: ctor_name;
+ tag: tag_name;
subpatts: patt array;
}
diff --git a/concrete.ml b/concrete.ml
@@ -8,8 +8,8 @@ type binop =
type var_name = var_name' node
and var_name' = Name.Var.t
-type ctor_name = ctor_name' node
-and ctor_name' = Name.Ctor.t
+type tag_name = tag_name' node
+and tag_name' = Name.Tag.t
type term = term' node
and term' =
@@ -23,7 +23,7 @@ and term' =
| App of term * term array
| Fn of param array * term
| FnType of domain array * term
-| Variant of ctor_name * term array
+| Variant of tag_name * term array
| VariantType of ctor array
| Tuple of term array
| TupleType of domain array
@@ -56,14 +56,14 @@ and domain' =
| AnnotDomain of Plicity.t * patt * term
and ctor = ctor' node
-and ctor' = Ctor of ctor_name * domain array
+and ctor' = Ctor of tag_name * domain array
and patt = patt' node
and patt' =
| PWild
| PBind of var_name
| PAnnot of patt * term
-| PVariant of ctor_name * patt array
+| PVariant of tag_name * patt array
| PTuple of patt array
| PUnit
| PNat of Z.t
diff --git a/ctx.ml b/ctx.ml
@@ -1,27 +1,29 @@
open Node
-(* TODO: Somewhere we need to forbid multi-binders and multi-definers from
- * declaring the same name twice. *)
-
type 'a assignment = {
mutable typ: 'a;
mutable value: 'a;
mutable active: bool;
}
+(* The "assignments" part of a context can be (and is) mutable, because it does
+ * not get stored on core terms or semantic values after elaboration, but the
+ * "env" part must not be mutable, because it gets saved on values. *)
type 'a context = {
assignments: 'a assignment Tsil.t Name.Var.Map.t; (* XXX: tsil! Yuck! *)
env: 'a Env.environment;
}
-let empty = {
+let empty: 'a. 'a context = {
assignments = Name.Var.Map.empty;
env = Env.empty;
}
-let assign ctx names typ value =
+let assign
+: 'a. 'a context -> Name.Var.t array -> 'a -> 'a -> 'a context * 'a assignment
+= fun ctx names typ value ->
let asn = {typ; value; active = true} in
- let shadow ctx {data = name; _} =
+ let shadow ctx name =
let add_to_tsil = function
| None -> Some (Tsil.Snoc (Tsil.Lin, asn))
| Some t -> Some (Tsil.Snoc (t, asn)) in
@@ -29,11 +31,17 @@ let assign ctx names typ value =
{ctx with assignments} in
(Array.fold_left shadow ctx names, asn)
-let bind ctx vars = {ctx with env = Env.bind ctx.env vars}
+let bind
+: 'a. 'a context -> Uniq.range -> 'a context
+= fun ctx vars -> {ctx with env = Env.bind ctx.env vars}
-let define ctx var value = {ctx with env = Env.define ctx.env var value}
+let define
+: 'a. 'a context -> Uniq.uniq -> 'a -> 'a context
+= fun ctx var value -> {ctx with env = Env.define ctx.env var value}
-let lookup ctx name i =
+let lookup
+: 'a. 'a context -> Name.Var.t -> int -> 'a assignment option
+= fun ctx name i ->
match Name.Var.Map.find_opt name ctx.assignments with
| Some t ->
let rec go i t = match i, t with
@@ -44,8 +52,14 @@ let lookup ctx name i =
go i t
| None -> None
-let index ctx ij = Env.index ctx.env ij
+let index
+: 'a. 'a context -> Index.t -> Uniq.uniq
+= fun ctx ij -> Env.index ctx.env ij
-let quote ctx var = Env.quote ctx.env var
+let quote
+: 'a. 'a context -> Uniq.uniq -> Index.t option
+= fun ctx var -> Env.quote ctx.env var
-let eval ctx var = Env.eval ctx.env var
+let eval
+: 'a. 'a context -> Uniq.uniq -> 'a option
+= fun ctx var -> Env.eval ctx.env var
diff --git a/desugar.ml b/desugar.ml
@@ -4,17 +4,11 @@ module E = Error
module C = Concrete
module A = Abstract
-let ensure_distinct names =
- let declare name_set {loc; data = name} =
- if Name.Var.Set.mem name name_set then
- E.abort loc (E.DesugarDuplicateBinderName name)
- else
- Name.Var.Set.add name name_set in
- ignore @@ Array.fold_left declare Name.Var.Set.empty names
-
let add2 (x0, y0) (x1, y1) = (x0 + x1, y0 + y1)
-let rec bind_and_annot_count {data = p; _} = match p with
+let rec bind_and_annot_count
+: C.patt -> int * int
+= fun p -> match p.data with
| C.PWild -> (0, 0)
| C.PBind _ -> (1, 0)
| C.PAnnot (p, _) -> add2 (bind_and_annot_count p) (0, 1)
@@ -26,38 +20,70 @@ let rec bind_and_annot_count {data = p; _} = match p with
| C.POr _ -> no_impl "or patterns"
| C.PParen p -> bind_and_annot_count p
-let synth_var_name name = Loc.Nowhere @$ Name.Var.Of name
+let array_loc
+: 'a. 'a node array -> Loc.t
+= function
+| [||] -> invalid_arg "Desugar.array_loc: empty node array"
+| nodes -> Loc.of_locs nodes.(0).loc nodes.(Array.length nodes - 1).loc
-let synth_ctor_name name = Loc.Nowhere @$ Name.Ctor.Of name
+let synth_var_name
+: string -> A.var_name
+= fun name -> Loc.Nowhere @$ Name.Var.Of name
-let synth_ctor binders = Loc.Nowhere @$ A.Ctor binders
+let synth_tag_name
+: string -> A.tag_name
+= fun name -> Loc.Nowhere @$ Name.Tag.Of name
-let synth_term_var name i = Loc.Nowhere @$ A.Var (synth_var_name name, i)
-let synth_term_unit_type =
- let ctor = synth_ctor [||] in
- let ctors = Name.Ctor.Map.singleton (Name.Ctor.Of "0") ctor in
+let synth_term_data
+: string -> A.term
+= fun tag -> Loc.Nowhere @$ A.Data (synth_tag_name tag, [||])
+
+let synth_term_datatype_unit: A.term =
+ let ctor = Loc.Nowhere @$ [||] in
+ let ctors = Name.Tag.Map.singleton (Name.Tag.Of "0") ctor in
Loc.Nowhere @$ A.DataType ctors
-let synth_term_unit = Loc.Nowhere @$ A.Data (synth_ctor_name "0", [||])
-let synth_term_true = Loc.Nowhere @$ A.Data (synth_ctor_name "true", [||])
-let synth_term_false = Loc.Nowhere @$ A.Data (synth_ctor_name "false", [||])
-
-let synth_case patt body = Loc.Nowhere @$ {A.patt; A.body}
-
-let synth_binder plicity patt typ = Loc.Nowhere @$ {A.plicity; A.patt; A.typ}
-
-let synth_patt names typs disc =
- Loc.Nowhere @$ {A.names; A.typs; A.disc = Loc.Nowhere @$ disc}
-let synth_patt_wild = synth_patt [||] [||] A.DWild
-let synth_patt_wild_unit = synth_patt [||] [|synth_term_unit_type|] A.DWild
-let synth_patt_data names typs tag subpatts =
- synth_patt [||] [||] @@ A.DData {
- tag = synth_ctor_name tag;
- subpatts;
+
+let synth_term_var
+: string -> int -> A.term
+= fun name i -> Loc.Nowhere @$ A.Var (synth_var_name name, i)
+
+let synth_case
+: A.patt -> A.term -> A.case
+= fun patt body -> Loc.Nowhere @$ {A.patt; A.body}
+
+let synth_binder
+: Plicity.t -> A.patt -> A.binder
+= fun plicity patt -> Loc.Nowhere @$ {A.plicity; A.patt}
+
+let synth_patt_wild: A.patt =
+ Loc.Nowhere @$ {
+ A.names = [||];
+ A.typs = [||];
+ A.disc = Loc.Nowhere @$ A.DWild;
}
-let synth_patt_true = synth_patt_data [||] [||] "true" [||]
-let synth_patt_false = synth_patt_data [||] [||] "false" [||]
-let binop = function
+let synth_patt_wild_unit: A.patt =
+ Loc.Nowhere @$ {
+ A.names = [||];
+ A.typs = [|synth_term_datatype_unit|];
+ A.disc = Loc.Nowhere @$ A.DWild;
+ }
+
+let synth_patt_data
+: string -> A.patt
+= fun tag ->
+ Loc.Nowhere @$ {
+ A.names = [||];
+ A.typs = [||];
+ A.disc = Loc.Nowhere @$ A.DData {
+ tag = synth_tag_name tag;
+ subpatts = [||];
+ };
+ }
+
+let binop
+: C.binop -> string
+= function
| C.LOr | C.LAnd ->
impossible "Desugar.binop: LOr and Land are handled specially"
| C.Lt -> "`<"
@@ -72,7 +98,9 @@ let binop = function
| C.Div -> "`/"
| C.Mod -> "`%"
-let rec term {loc; data = t} = match t with
+let rec term
+: C.term -> A.term
+= fun {loc; data = t} -> match t with
| C.Let (definers, body) ->
loc @$ A.Let (Array.map definer definers, term body)
| C.Seq (t, u) ->
@@ -85,89 +113,123 @@ let rec term {loc; data = t} = match t with
| C.Match (scrutinee, cases) ->
loc @$ A.Match (term scrutinee, Array.map case cases)
| C.If ({data = C.TrueCond s; _}, t, f) ->
- loc @$ term_if synth_patt_true (term s) (term t) (term f)
+ loc @$ term_if (synth_patt_data "true") (term s) (term t) (term f)
| C.If ({data = C.PattCond (p, s); _}, t, f) ->
loc @$ term_if (patt p) (term s) (term t) (term f)
| C.Iff ({data = C.TrueCond s; _ }, t) ->
- loc @$ term_if synth_patt_true (term s) (term t) synth_term_unit
+ loc @$ term_if (synth_patt_data "true") (term s) (term t) (synth_term_data "0")
| C.Iff ({data = C.PattCond (p, s); _}, t) ->
- loc @$ term_if (patt p) (term s) (term t) synth_term_unit
+ loc @$ term_if (patt p) (term s) (term t) (synth_term_data "0")
| C.Annot (t, u) -> loc @$ A.Annot (term t, term u)
| C.BinOp (t, C.LOr, u) ->
- loc @$ term_if synth_patt_true (term t) synth_term_true (term u)
+ loc @$ term_if (synth_patt_data "true") (term t) (synth_term_data "true") (term u)
| C.BinOp (t, C.LAnd, u) ->
- loc @$ term_if synth_patt_true (term t) (term u) synth_term_false
+ loc @$ term_if (synth_patt_data "true") (term t) (term u) (synth_term_data "false")
| C.BinOp (t, o, u) ->
loc @$ A.App (synth_term_var (binop o) 0, [|term t; term u|])
| C.App (fn, args) -> loc @$ A.App (term fn, Array.map term args)
| C.Fn (params, body) ->
- let params =
+ let multibinder =
if Array.length params = 0 then
- [|synth_binder Plicity.Ex synth_patt_wild_unit None|]
- else
- Array.map param params in
- loc @$ A.Fn (params, term body)
-| C.FnType (doms, cod) -> loc @$ A.FnType (Array.map domain doms, term cod)
+ Loc.Nowhere @$ [|synth_binder Plicity.Ex synth_patt_wild_unit|]
+ else
+ array_loc params @$ Array.map param params in
+ let abstraction = loc @$ {A.multibinder; A.term = term body} in
+ loc @$ A.Fn abstraction
+| C.FnType (doms, cod) ->
+ let multibinder = array_loc doms @$ Array.map domain doms in
+ let abstraction = loc @$ {A.multibinder; A.term = term cod} in
+ loc @$ A.FnType abstraction
| C.Variant (tag, fields) -> loc @$ A.Data (tag, Array.map term fields)
| C.VariantType ctors ->
let insert m {loc = ctor_loc; data = C.Ctor (tag, doms)} =
- if Name.Ctor.Map.mem tag.data m then
- E.abort tag.loc (E.DesugarDuplicateCtor tag.data)
+ if Name.Tag.Map.mem tag.data m then
+ E.abort tag.loc (E.DesugarDuplicateTag tag.data)
else
- let ctor = ctor_loc @$ A.Ctor (Array.map domain doms) in
- Name.Ctor.Map.add tag.data ctor m in
- let ctors = Array.fold_left insert Name.Ctor.Map.empty ctors in
+ let binders = ctor_loc @$ Array.map domain doms in
+ Name.Tag.Map.add tag.data binders m in
+ let ctors = Array.fold_left insert Name.Tag.Map.empty ctors in
loc @$ A.DataType ctors
| C.Tuple fields ->
- let tag = synth_ctor_name (string_of_int (Array.length fields)) in
+ let tag = synth_tag_name (string_of_int (Array.length fields)) in
loc @$ A.Data (tag, Array.map term fields)
| C.TupleType doms ->
- let tag = Name.Ctor.Of (string_of_int (Array.length doms)) in
- let ctor = synth_ctor (Array.map domain doms) in
- loc @$ A.DataType (Name.Ctor.Map.singleton tag ctor)
-| C.Unit -> loc @$ A.Data (synth_ctor_name "0", [||])
+ let tag = Name.Tag.Of (string_of_int (Array.length doms)) in
+ let binders = 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
| C.IndexedVar (x, i) -> loc @$ A.Var (x, i)
| C.Var x -> loc @$ A.Var (x, 0)
| C.Paren t -> term t
-and term_if p s t f =
+and term_if
+: A.patt -> A.term -> A.term -> A.term -> A.term'
+= fun p s t f ->
A.Match (s, [|
synth_case p t;
synth_case synth_patt_wild f;
|])
-and definer {loc; data = d} = loc @$ match d with
+and definer
+: C.definer -> A.definer
+= fun {loc; data = d} -> loc @$ match d with
| C.Definer (lhs, rhs) ->
{A.recursive = false; A.lhs = patt lhs; A.rhs = term rhs}
| C.RecDefiner (lhs, rhs) ->
{A.recursive = true; A.lhs = patt lhs; A.rhs = term rhs}
-and case {loc; data = C.Case (p, t)} =
+and case
+: C.case -> A.case
+= fun {loc; data = C.Case (p, t)} ->
loc @$ {A.patt = patt p; A.body = term t}
-and param {loc; data = C.Param (plicity, p)} =
- loc @$ {A.plicity; A.patt = patt p; A.typ = None}
+and param
+: C.param -> A.binder
+= fun {loc; data = C.Param (plicity, p)} ->
+ loc @$ {A.plicity; A.patt = patt p}
-and domain {loc; data = dom} = loc @$ match dom with
+and domain
+: C.domain -> A.binder
+= fun {loc; data = dom} -> loc @$ match dom with
| C.ExplicitDomain t ->
- {A.plicity = Plicity.Ex; A.patt = synth_patt_wild; A.typ = Some (term t)}
+ let p = Loc.Nowhere @$ {
+ A.names = [||];
+ A.typs = [|term t|];
+ A.disc = Loc.Nowhere @$ A.DWild;
+ } in
+ {A.plicity = Plicity.Ex; A.patt = p}
| C.ImplicitTypeDomain p ->
- {A.plicity = Plicity.Im; A.patt = patt p; A.typ = Some (Loc.Nowhere @$ A.Type)}
+ 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.disc = p.data.disc;
+ } in
+ {A.plicity = Plicity.Im; A.patt = p}
| C.AnnotDomain (plicity, p, t) ->
- {A.plicity; A.patt = patt p; A.typ = Some (term t)}
+ let p = patt p in
+ let p = p.loc @$ {
+ A.names = p.data.names;
+ A.typs = Array.append [|term t|] p.data.typs;
+ A.disc = p.data.disc;
+ } in
+ {A.plicity; A.patt = p}
-and patt p =
+and patt
+: C.patt -> A.patt
+= fun p ->
let (bind_count, annot_count) = bind_and_annot_count p in
let names = Inc_array.make bind_count in
let typs = Inc_array.make annot_count in
let disc = discriminant names typs p in
let names = Inc_array.to_array names in
let typs = Inc_array.to_array typs in
- ensure_distinct names;
p.loc @$ {A.names; A.typs; A.disc}
-and discriminant names typs {loc; data = p} = match p with
+and discriminant
+: A.var_name Inc_array.t -> A.term Inc_array.t -> C.patt -> A.discriminant
+= fun names typs {loc; data = p} -> match p with
| C.PWild -> loc @$ A.DWild
| C.PBind name ->
Inc_array.add names name;
@@ -177,9 +239,9 @@ and discriminant names typs {loc; data = p} = match p with
discriminant names typs p
| C.PVariant (tag, ps) -> loc @$ A.DData {tag; subpatts = Array.map patt ps}
| C.PTuple ps ->
- let tag = synth_ctor_name (string_of_int (Array.length ps)) in
+ let tag = synth_tag_name (string_of_int (Array.length ps)) in
loc @$ A.DData {tag; subpatts = Array.map patt ps}
-| C.PUnit -> loc @$ A.DData {tag = synth_ctor_name "0"; subpatts = [||]}
+| C.PUnit -> loc @$ A.DData {tag = synth_tag_name "0"; subpatts = [||]}
| C.PNat _ -> no_impl "nat patterns"
| C.PAnd (p, q) ->
let pdisc = discriminant names typs p in
diff --git a/elab.ml b/elab.ml
@@ -31,42 +31,59 @@ type clause = {
* not end with a prime, which returns in the result monad.
* TODO: Make sure every function has both versions, even if unused? *)
-(* TODO: We check for name distinctness in two places; unify them. *)
-let declare_name'
-: Name.Var.Set.t -> Name.Var.t node -> Name.Var.Set.t
+let add_name'
+: Name.Var.Set.t -> Name.Var.t node -> Name.Var.Set.t * Name.Var.t
= fun name_set {loc; data = name} ->
if Name.Var.Set.mem name name_set then
E.abort loc @@ E.ElabDuplicateName name
else
- Name.Var.Set.add name name_set
+ (Name.Var.Set.add name name_set, name)
+
+(*
+let ensure_distinct'
+: Name.Var.t node array -> Name.Var.t array
+= fun names ->
+ let nnames = Array.length names in
+ let name_set = ref Name.Var.Set.empty in
+ let names' = Array.make nnames garbage in
+ for i = 0 to nnames - 1 do
+ let {loc; data = name} = names.(i) in
+ name_set := add_name' loc !name_set name;
+ names'.(i) <- names.(i).data
+ done;
+ names'
+*)
-(* XXX: Misleading name. This also binds and defines things. *)
let rec assign_patt
: context -> I.patt -> V.value -> Uniq.uniq -> context
-= fun ctx {names; disc} vtyp var ->
+= fun ctx {names; disc} vtyp var ->
let (ctx, _) = Ctx.assign ctx names vtyp (V.Arb var) in
match disc with
- | I.DWild -> ctx
+ | I.DWild _ -> ctx
| I.DData {tag; tagi; subpatts; datatype} ->
+ let {I.binders; I.order} = datatype.ctors.(tagi) in
let arity = Array.length subpatts in
let subvars = Uniq.fresh arity in
let data = V.Data {
tag;
tagi;
args = Array.init arity (fun i -> V.Arb (Uniq.get subvars i));
- clo = ctx.env; (* Environment before binding *)
- datatype;
+ (* datatype is formed in a context without subvars bound. *)
+ datatype_clo = (ctx.env, datatype);
} in
let ctx = Ctx.bind ctx subvars in
let ctx = Ctx.define ctx var data in
+ (* Assign each subpattern in type-dependency order, because that's the
+ * order that check_disc' elaborates subpatterns in. The order matters
+ * here, because assign_patt binds variables. *)
let ctx = ref ctx in
for i = 0 to arity - 1 do
- (* XXX: Do we need to do this in type-checking order? *)
- let subtyp = datatype.ctors.(tagi).binders.(i).typ in
+ let j = order.(i) in
+ let subtyp = I.disc_type binders.(j).patt.disc in
let vsubtyp = eval !ctx.env subtyp in
- ctx := assign_patt !ctx subpatts.(i) vsubtyp (Uniq.get subvars i)
+ ctx := assign_patt !ctx subpatts.(j) vsubtyp (Uniq.get subvars j)
done;
!ctx
@@ -152,23 +169,24 @@ and elaborate'
| A.App (fn, explicit_args), Infer ->
let (fn, vtyp) = infer' ctx fn in
begin match force ctx.env vtyp with
- | V.FnTypeClosure (clo, {multibinder; codomain}) ->
+ | V.FnTypeClosure (clo, {multibinder; term = codomain}) ->
let (args, clo) = check_args' ctx loc explicit_args clo multibinder in
let vcodomain = eval clo codomain in
(I.App (fn, args), vcodomain)
| vtyp -> E.abort loc @@ E.ElabApplyNonFunction (quote ctx.env vtyp)
end
-| A.Fn (params, body), Infer ->
+| A.Fn {data = {multibinder = params; term = body}; _}, Infer ->
let (ctx', multibinder) = infer_multibinder' ctx loc params in
let (body, vcodomain) = infer' ctx' body in
let codomain = quote ctx'.env vcodomain in
- let fn = I.Fn {multibinder; body; codomain} in
- let vfntype = V.FnTypeClosure (ctx.env, {multibinder; codomain}) in
+ let fn = I.Fn {multibinder; term = body} in
+ let vfntype = V.FnTypeClosure (ctx.env, {multibinder; term = codomain}) in
(fn, vfntype)
-| A.Fn (params, body), Check (V.FnTypeClosure (clo, fntype) as vfntype) ->
- let {I.multibinder = {binders = domains; order}; I.codomain} = fntype in
+| A.Fn {data = {multibinder = {data = params; _}; term = body}; _},
+ Check (V.FnTypeClosure (clo, fntype) as vfntype) ->
+ let {I.multibinder = {binders = domains; order}; I.term = codomain} = fntype in
begin if Array.length params <> Array.length domains then
E.abort loc E.ElabFnArityMismatch
@@ -180,69 +198,66 @@ and elaborate'
let clo = Env.bind clo vars in
let ctx = ref ctx in
+ let name_set = ref Name.Var.Set.empty in
let params' = Array.make arity garbage in
for i = 0 to arity - 1 do
let j = order.(i) in
let param = params.(j).data in
let domain = domains.(j) in
- begin if Option.is_some param.typ then
- impossible "Elab.elaborate': params shouldn't have guaranteed \
- type annotations";
- end;
-
begin if param.plicity <> domain.plicity then
E.abort loc E.ElabFnPlicityMismatch
end;
let plicity = param.plicity in
- let vtyp = eval clo domain.typ in
+ let vtyp = eval clo (I.disc_type domain.patt.disc) in
let typ = quote !ctx.env vtyp in
- let names = check_irrefutable_patt' !ctx param.patt vtyp in
+ let (name_set', names) = check_irrefutable_patt'
+ !ctx !name_set param.patt vtyp in
+ name_set := name_set';
let (ctx', _) = Ctx.assign !ctx names vtyp (V.Arb (Uniq.get vars j)) in
ctx := ctx';
- params'.(j) <- {I.plicity; I.names; I.typ}
+ params'.(j) <- {I.plicity; I.patt = {names; disc = I.DWild typ}}
done;
let vcodomain = eval clo codomain in
- let codomain = quote !ctx.env vcodomain in
let body = check' !ctx body vcodomain in
- (I.Fn {multibinder = {binders = params'; order}; body; codomain}, vfntype)
+ (I.Fn {multibinder = {binders = params'; order}; term = body}, vfntype)
(*| A.Fn _, Check vtyp -> E.abort loc @@ ErrExpectedFnType vtyp*)
-| A.FnType (domains, codomain), Infer ->
+| 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; codomain}, V.Type)
+ (I.FnType {multibinder; term = codomain}, V.Type)
| A.Data _, Infer -> E.abort loc E.ElabCantInferData
| A.Data ({data = tag; _}, explicit_args),
Check (V.DataTypeClosure (clo, datatype) as vdatatype) ->
- begin match Name.Ctor.Map.find_opt tag datatype.names with
+ begin match Name.Tag.Map.find_opt tag datatype.names with
| Some tagi ->
let (args, _) = check_args' ctx loc explicit_args clo
datatype.ctors.(tagi) in
- let datatype = quote_datatype ctx.env clo datatype in
+ let datatype = shift_datatype ctx.env clo datatype in
(I.Data {tag; tagi; args; datatype}, vdatatype)
- | None -> E.abort loc @@ E.ElabUnexpectedCtor tag
+ | None -> E.abort loc @@ E.ElabUnexpectedTag tag
end
(*| A.Data _, Check vtyp -> E.abort loc @@ ErrExpectedDataType vtyp*)
| A.DataType ctors, Infer ->
let next = ref 0 in
- let ctors' = Array.make (Name.Ctor.Map.cardinal ctors) garbage in
- let go {data = A.Ctor binders; _} =
+ let ctors' = Array.make (Name.Tag.Map.cardinal ctors) garbage in
+ let go binders =
let i = !next in
incr next;
let (_, multibinder) = infer_multibinder' ctx loc binders in
ctors'.(i) <- multibinder;
i in
- let names = Name.Ctor.Map.map go ctors in
+ let names = Name.Tag.Map.map go ctors in
(I.DataType {ctors = ctors'; names}, V.Type)
| A.Nat n, Infer -> (I.Nat n, V.Builtin I.NatType)
@@ -259,12 +274,13 @@ and elaborate'
| (A.Annot _ | A.App _ | A.Fn _ | A.FnType _ | A.Data _ | A.DataType _
| A.Nat _ | A.Var _ | A.Type) as t, Check vexpected ->
let (t, vinferred) = infer' ctx {loc; data = t} in
- if conv ctx.env vexpected vinferred then
- (t, vexpected)
- else
+ begin try unify ctx.env vexpected vinferred with
+ | UnifyFail ->
let expected = quote ctx.env vexpected in
let inferred = quote ctx.env vinferred in
E.abort loc @@ E.ElabUnifyFail (expected, inferred)
+ end;
+ (t, vexpected)
(* Check the given explicit arguments against the given multibinder.
* Return the elaborated terms and the multibinder's closure extended with
@@ -283,7 +299,7 @@ and check_args'
let clo = ref clo in
for i = 0 to arity - 1 do
let j = order.(i) in
- let vtyp = eval !clo binders.(j).typ in
+ let vtyp = eval !clo (I.disc_type binders.(j).patt.disc) in
let arg = match args.(j) with
| Some arg -> check' ctx arg vtyp
| None -> no_impl "implicit args" in
@@ -321,20 +337,21 @@ and infer_definers'
| [|{loc; data = {recursive = false; lhs; rhs}}|] ->
let (names, rhs, vtyp) =
(* First try to infer from lhs (and check rhs). *)
- match infer_irrefutable_patt ctx lhs with
- | Ok (names, vtyp) ->
+ match infer_irrefutable_patt ctx Name.Var.Set.empty lhs with
+ | Ok (_, names, vtyp) ->
let rhs = check' ctx rhs vtyp in
(names, rhs, vtyp)
| Error {data = E.ElabNonInferablePatt; _} ->
(* Next try to infer from rhs (and check lhs). *)
let (rhs, vtyp) = infer' ctx rhs in
- let names = check_irrefutable_patt' ctx lhs vtyp in
+ let (_, names) = check_irrefutable_patt'
+ ctx Name.Var.Set.empty lhs vtyp in
(names, rhs, vtyp)
| Error e -> E.abort e.loc e.data in
let typ = quote ctx.env vtyp in
- (* XXX: vrhs doesn't need to be a Rec. We could eagerly evaluate it, or
- * add some other mechanism for laziness (like glued eval). *)
- let vrhs = V.Rec {env = ref ctx.env; rhs} in
+ (* XXX: vrhs doesn't need to be a RefClo. We could eagerly evaluate it,
+ * or add some other mechanism for laziness (like glued eval). *)
+ let vrhs = V.RefClo (ref ctx.env, rhs) in
let (ctx, _) = Ctx.assign ctx names vtyp (V.Arb (Uniq.get vars 0)) in
let ctx = Ctx.define ctx (Uniq.get vars 0) vrhs in
(ctx, [|{names; rhs; typ}|])
@@ -351,17 +368,19 @@ and infer_definers'
* assignments. We later set the active flag to false on assignments
* for non-recusive definers, so that the rhs of non-recursive definers
* can not access their own assignment. *)
- let name_set = ref Name.Var.Set.empty in
let ctx_with_asns = ref ctx in
+ let name_set = ref Name.Var.Set.empty in
+ let namess = Array.make ndefiners garbage in
let asns = Array.make ndefiners garbage in
for i = 0 to ndefiners - 1 do
let {loc; data = {A.lhs; _}} = definers.(i) in
- match infer_irrefutable_patt ctx lhs with
- | Ok (names, vtyp) ->
- name_set := Array.fold_left declare_name' !name_set names;
- let (ctx', asn) = Ctx.assign !ctx_with_asns
+ match infer_irrefutable_patt ctx !name_set lhs with
+ | Ok (name_set', names, vtyp) ->
+ name_set := name_set';
+ namess.(i) <- names;
+ let (ctx_with_asns', asn) = Ctx.assign !ctx_with_asns
names vtyp (V.Arb (Uniq.get vars i)) in
- ctx_with_asns := ctx';
+ ctx_with_asns := ctx_with_asns';
asns.(i) <- asn
| Error ({data = E.ElabNonInferablePatt; _} as root) ->
E.abort loc @@ E.ElabNoLetAnnot root
@@ -395,11 +414,10 @@ and infer_definers'
asns.(i).active <- true;
rhs
end in
- let vrhs = V.Rec {env; rhs} in
+ let vrhs = V.RefClo (env, rhs) in
env := Env.define !env (Uniq.get vars i) vrhs;
- let names = definers.(i).data.lhs.data.names in
- definers'.(i) <- {I.names; I.rhs; I.typ}
+ definers'.(i) <- {I.names = namess.(i); I.rhs; I.typ}
done;
(* TODO: For this situation, it might be nice to abstract the surface
@@ -417,7 +435,8 @@ and elaborate_match'
for i = 0 to ncases - 1 do
let {data = {A.patt; A.body}; _} = cases.(i) in
- let patt = check_patt' ctx patt scrutinee_vtyp in
+ let (_, patt) = check_patt'
+ ctx Name.Var.Set.empty patt scrutinee_vtyp in
let vars = Uniq.fresh 1 in
let var = Uniq.get vars 0 in
@@ -435,7 +454,7 @@ and elaborate_match'
: int -> I.case -> clause
= fun casei case ->
let tests = match case.patt.disc with
- | I.DWild -> Uniq.UniqMap.empty
+ | I.DWild _ -> Uniq.UniqMap.empty
| I.DData data_disc -> Uniq.UniqMap.singleton var data_disc in
{tests; casei} in
let clauses = Array.mapi to_clause cases' in
@@ -525,7 +544,7 @@ and elaborate_subswitch'
let tests = ref tests in
for j = 0 to Array.length subpatts - 1 do
match subpatts.(j).disc with
- | I.DWild -> ()
+ | I.DWild _ -> ()
| I.DData data_disc ->
let subvar = Uniq.get subvars j in
tests := Uniq.UniqMap.add subvar data_disc !tests
@@ -545,65 +564,28 @@ and elaborate_subswitch'
let env = Env.bind env subvars in
elaborate_switch' match_loc used_cases env subclauses
+(* TODO: This has evolved into a complete disaster. Rewrite it. *)
and infer_multibinder'
-: context -> Loc.t -> A.binder array -> context * I.multibinder
-= fun ctx loc binders ->
- (* We associate two different orders on the variables of a multibinder.
- * The *type dependency ordering* is the order where x <T y iff the type of
- * y depends on x. The *representation dependency ordering* is the order
- * where x <R y iff the representation of y depends on x. Note that x <R y
- * implies x <T y, but these two orders needn't coincide; for instance,
- * (A: Type) <T (p: Ptr A), but not A <R p. We type check multibinders
- * along a topological sorting of the variables with respect to the type
- * dependency order. There may be multiple such sortings, but the
- * programmer has no reason to care which one we choose. On the other hand,
- * the representation dependency order comes in to play when laying out
- * arguments of a function or fields of a data structure in memory.
- * Specifically, arguments/fields must be topologically sorted in memory
- * with respect to the representation dependency order. Again, there may
- * be multiple such sortings, but this time, the programmer might actually
- * care which one we use. For maximum flexibility, we let the source code
- * ordering of arguments/fields determine which topological sorting of <R
- * we use for memory layout, and we permit this sorting to NOT be a
- * topological sorting of <T, in contrast to existing implementations of
- * dependent types. (In practice, it is desirable to have the source code
- * order of arguments/fields be completely irrelevant by default, and have
- * the compiler automatically pick a reasonable memory layout (e.g., a
- * memory layout that minimizes padding). However, it is crucial for
- * low-level applications (e.g., modelling network packets) that there is
- * some way to request a particular memory layout.) This flexibility leads
- * to some difficulties here in the implementation, because we can't know
- * <T until we try elaborating each binder. To solve the problem, we
- * introduce a new kind of value, namely a *future*, which is the type of
- * a binder that we haven't elaborated yet. Whenever a future is
- * encountered, we raise the BlockedOnFuture exception, and indictate which
- * (multibinder, binder) pair we got stuck on. This exception is caught by
- * the associated multibinder, which updates a graph-like data structure
- * that tracks dependencies between binders. Every time a binder
- * successfully elaborates, we retry elaborating each of its dependents.
- * This means that, after trying to elaborate each binder at least once,
- * we're guaranteed to have found a topological sorting of <T if there is
- * one, and otherwise there is a cycle, which we report as an error. *)
-
+: context -> Loc.t -> A.multibinder -> 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).
* This uniq is not a variable. *)
let id = Uniq.get (Uniq.fresh 1) 0 in
let arity = Array.length binders in
-
let vars = Uniq.fresh arity in
let ctx = Ctx.bind ctx vars in
(* Add future assignments to ctx. *)
- let name_set = ref Name.Var.Set.empty in
let ctx = ref ctx in
+ let name_set = ref Name.Var.Set.empty in
let asns = Array.make arity garbage in
for i = 0 to arity - 1 do
(* TODO: We should probably check that the pattern is irrefutable
* here. *)
let names = binders.(i).data.patt.data.names in
- name_set := Array.fold_left declare_name' !name_set names;
+ let (name_set, names) = Array.fold_left_map add_name' !name_set names in
let typ = V.Future (id, i) in
let value = V.Arb (Uniq.get vars i) in
let (ctx', asn) = Ctx.assign !ctx names typ value in
@@ -645,6 +627,7 @@ and infer_multibinder'
end in
let states = Array.make arity start_state in
+ let namess = Array.make arity garbage in
(* Next index in the topological sorting of <T. *)
let next = ref 0 in
@@ -659,7 +642,8 @@ and infer_multibinder'
impossible "Elab.infer_multibinder': try_binder called with \
elaborated binder" in
match infer_binder' ctx binders.(i) with
- | vtyp ->
+ | (names, vtyp) ->
+ namess.(i) <- names;
asns.(i).typ <- vtyp;
states.(i) <- Elaborated !next;
incr next;
@@ -697,8 +681,10 @@ and infer_multibinder'
let typ = quote ctx.env asns.(i).typ in
binders'.(i) <- {
I.plicity = binders.(i).data.plicity;
- I.names = binders.(i).data.patt.data.names;
- I.typ;
+ I.patt = {
+ names = namess.(i);
+ disc = I.DWild typ;
+ };
};
order.(j) <- i
| Pending _ ->
@@ -708,19 +694,13 @@ and infer_multibinder'
(ctx, {binders = binders'; order})
and infer_binder'
-: context -> A.binder -> V.value
-= fun ctx {loc; data = {plicity; patt; typ}} -> match typ with
-| Some typ ->
- let typ = check' ctx typ V.Type in
- let vtyp = eval ctx.env typ in
- ignore @@ check_irrefutable_patt' ctx patt vtyp;
- vtyp
-| None ->
- match infer_irrefutable_patt ctx patt, plicity with
- | Ok (_, vtyp), _ -> vtyp
+: 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 patt V.Type with
- | Ok _ -> V.Type
+ begin match check_irrefutable_patt ctx Name.Var.Set.empty patt V.Type with
+ | Ok (_, names) -> (names, V.Type)
| Error root -> E.abort loc @@ E.ElabUnannotImplicitIsType root
end
| Error ({data = E.ElabNonInferablePatt; _} as root), Plicity.Ex ->
@@ -735,93 +715,107 @@ and check_types'
for i = start to Array.length typs - 1 do
let typ' = check' ctx typs.(i) V.Type in
let vtyp' = eval ctx.env typ' in
- begin if not (conv ctx.env vtyp vtyp') then
+ try unify ctx.env vtyp vtyp' with
+ | UnifyFail ->
let typ = quote ctx.env vtyp in
- let typ' = quote ctx.env vtyp' in
E.abort typs.(i).loc @@ E.ElabUnifyFail (typ, typ')
- end
done
and infer_irrefutable_patt
-: context -> A.patt -> (Name.Var.t node array * V.value, E.error) result
-= fun ctx patt ->
- try Ok (infer_irrefutable_patt' ctx patt) with
+: 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 -> A.patt -> Name.Var.t node array * V.value
-= fun ctx ({loc; _} as patt) ->
- let (patt, vtyp) = infer_patt' ctx patt in
+: 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
match patt with
| {disc = I.DData _; _} -> E.abort loc E.ElabDataPattRefutable
- | {names; disc = I.DWild} -> (names, vtyp)
+ | {names; disc = I.DWild _} -> (name_set, names, vtyp)
and check_irrefutable_patt
-: context -> A.patt -> V.value -> (Name.Var.t node array, E.error) result
-= fun ctx patt vtyp ->
- try Ok (check_irrefutable_patt' ctx patt vtyp) with
+: 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 -> A.patt -> V.value -> Name.Var.t node array
-= fun ctx ({loc; _} as patt) vtyp ->
- let patt = check_patt' ctx patt vtyp in
+: 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
match patt with
| {disc = I.DData _; _} -> E.abort loc E.ElabDataPattRefutable
- | {names; disc = I.DWild} -> names
+ | {names; disc = I.DWild _} -> (name_set, names)
and infer_patt'
-: context -> A.patt -> I.patt * V.value
-= fun ctx {loc; data = patt} -> match patt with
+: 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 vtyp = eval ctx.env typ in
check_types' ctx typs 1 vtyp;
- let disc = check_disc' ctx disc vtyp in
- ({names; disc}, vtyp)
+ let (names_set, disc) = check_disc' ctx name_set disc vtyp in
+ (name_set, {names; disc}, vtyp)
and check_patt'
-: context -> A.patt -> V.value -> I.patt
-= fun ctx {loc; data = {names; typs; disc}} vtyp ->
+: 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;
- let disc = check_disc' ctx disc vtyp in
- {names; disc}
+ let (name_set, disc) = check_disc' ctx name_set disc vtyp in
+ (name_set, {names; disc})
and check_disc'
-: context -> A.discriminant -> V.value -> I.discriminant
-= fun ctx {loc; data = disc} vtyp -> match disc, force ctx.env vtyp with
-| A.DWild, _ -> I.DWild
+: 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))
| A.DData {tag = {data = tag; _}; subpatts = explicit_subpatts},
- V.DataTypeClosure (clo, vdatatype) ->
- begin match Name.Ctor.Map.find_opt tag vdatatype.names with
+ V.DataTypeClosure (clo, datatype) ->
+ begin match Name.Tag.Map.find_opt tag datatype.names with
| Some tagi -> (* XXX: This is very similar to check_args'. *)
- let datatype = quote_datatype ctx.env clo vdatatype in
- let {I.binders; I.order} = vdatatype.ctors.(tagi) in
+ let datatype' = shift_datatype ctx.env clo datatype in
+ let {I.binders; I.order} = datatype.ctors.(tagi) in
let arity = Array.length binders in
-
let vars = Uniq.fresh arity in
let ctx = Ctx.bind ctx vars in
let clo = Env.bind clo vars in
+ let name_set = ref name_set in
let subpatts = elaborate_args' loc explicit_subpatts binders in
let subpatts' = Array.make arity garbage in
let ctx = ref ctx in
for i = 0 to arity - 1 do
let j = order.(i) in
- let vtyp = eval clo binders.(j).typ in
- let subpatt = match subpatts.(j) with
- | Some patt -> check_patt' !ctx patt vtyp
+ let typ = I.disc_type binders.(j).patt.disc in
+ let vtyp = eval clo typ in
+ let (name_set', subpatt') = match subpatts.(j) with
+ | Some patt -> check_patt' !ctx !name_set patt vtyp
| None -> no_impl "implict args" in
- subpatts'.(j) <- subpatt;
+ name_set := name_set';
+ subpatts'.(j) <- subpatt';
(* XXX: I think this is a quadratic time algorithm. We should
* thread a context through the check_disc calls instead of
* repeatedly reassigning/rebinding/redefining stuff. *)
- ctx := assign_patt !ctx subpatt vtyp (Uniq.get vars j)
+ ctx := assign_patt !ctx subpatt' vtyp (Uniq.get vars j)
done;
- I.DData {tag; tagi; subpatts = subpatts'; datatype}
+ let disc = I.DData {
+ tag;
+ tagi;
+ subpatts = subpatts';
+ datatype = datatype';
+ } in
+ (!name_set, disc)
- | None -> E.abort loc @@ E.ElabUnexpectedCtor tag
+ | None -> E.abort loc @@ E.ElabUnexpectedTag tag
end
| A.DData _, vtyp -> E.abort loc @@ E.ElabExpectedDataType (quote ctx.env vtyp)
diff --git a/env.ml b/env.ml
@@ -15,24 +15,30 @@ module UniqTsil = struct
var_to_index: VarMap.t;
}
- let lin = {
+ let lin: t = {
length = 0;
index_to_var = IndexMap.empty;
var_to_index = VarMap.empty;
}
- let snoc {length; index_to_var; var_to_index} vars = {
+ let snoc
+ : t -> Uniq.range -> t
+ = fun {length; index_to_var; var_to_index} vars -> {
length = length + 1;
index_to_var = IndexMap.add length vars index_to_var;
var_to_index = VarMap.add vars length var_to_index;
}
- let var_of {length; index_to_var; _} (Index.Of (i, j)) =
+ let var_of
+ : t -> Index.t -> Uniq.uniq
+ = fun {length; index_to_var; _} (Index.Of (i, j)) ->
let l = length - i - 1 in (* Convert index i to level l. *)
Uniq.get (IndexMap.find l index_to_var) j
- let index_of {length; var_to_index; _} var =
- match VarMap.find_opt var var_to_index with
+ let index_of
+ : t -> Uniq.uniq -> Index.t option
+ = fun {length; var_to_index; _} var ->
+ match VarMap.find_opt var var_to_index with
| Some (l, j) ->
let i = length - l - 1 in (* Convert level l to index i. *)
Some (Index.Of (i, j))
@@ -44,19 +50,29 @@ type 'a environment = {
definitions: 'a UniqMap.t;
}
-let empty = {
+let empty: 'a. 'a environment = {
bindings = UniqTsil.lin;
definitions = UniqMap.empty;
}
-let bind env vars =
+let bind
+: 'a. 'a environment -> Uniq.range -> 'a environment
+= fun env vars ->
{env with bindings = UniqTsil.snoc env.bindings vars}
-let define env var value =
+let define
+: 'a. 'a environment -> Uniq.uniq -> 'a -> 'a environment
+= fun env var value ->
{env with definitions = UniqMap.add var value env.definitions}
-let index env ij = UniqTsil.var_of env.bindings ij
+let index
+: 'a. 'a environment -> Index.t -> Uniq.uniq
+= fun env ij -> UniqTsil.var_of env.bindings ij
-let quote env var = UniqTsil.index_of env.bindings var
+let quote
+: 'a. 'a environment -> Uniq.uniq -> Index.t option
+= fun env var -> UniqTsil.index_of env.bindings var
-let eval env var = UniqMap.find_opt var env.definitions
+let eval
+: 'a. 'a environment -> Uniq.uniq -> 'a option
+= fun env var -> UniqMap.find_opt var env.definitions
diff --git a/error.ml b/error.ml
@@ -12,14 +12,13 @@ and error' =
| ParserInvalidPatt
| ParserEmptyDomain
-| DesugarDuplicateCtor of Name.Ctor.t
-| DesugarDuplicateBinderName of Name.Var.t
+| DesugarDuplicateTag of Name.Tag.t
| DesugarDataAndData
| ElabApplyNonFunction of I.term
| ElabNonInferablePatt
| ElabUnifyFail of I.term * I.term
-| ElabUnexpectedCtor of Name.Ctor.t
+| ElabUnexpectedTag of Name.Tag.t
| ElabExpectedDataType of I.term
| ElabNoLetAnnot of error
| ElabBinderCycle of Name.Var.t list
@@ -57,14 +56,10 @@ and pp_print' ppf = function
| ParserEmptyDomain ->
F.pp_print_string ppf "empty domain"
-| DesugarDuplicateCtor tag ->
+| DesugarDuplicateTag tag ->
F.fprintf ppf "%s: %a"
"duplicate constructor: "
- Name.Ctor.pp_print tag
-| DesugarDuplicateBinderName name ->
- F.fprintf ppf "%s: %a"
- "duplicate binder name: "
- Name.Var.pp_print name
+ Name.Tag.pp_print tag
| DesugarDataAndData ->
F.pp_print_string ppf "conjunction of two data patterns"
@@ -88,7 +83,7 @@ and pp_print' ppf = function
| ElabExpectedDataType _ -> F.pp_print_string ppf "ErrExpectedDataType"
| ElabFnArityMismatch -> F.pp_print_string ppf "ErrFnArityMismatch"
| ElabFnPlicityMismatch -> F.pp_print_string ppf "ErrFnPlicityMismatch"
-| ElabUnexpectedCtor _ -> F.pp_print_string ppf "ErrUnexpectedCtor"
+| ElabUnexpectedTag _ -> F.pp_print_string ppf "ErrUnexpectedTag"
| ElabDuplicateName _ -> F.pp_print_string ppf "ErrDuplicateName"
| ElabNonExhaustiveMatch -> F.pp_print_string ppf "ElabNonExhaustiveMatch"
| ElabRedundantCase -> F.pp_print_string ppf "ElabRedundantCase"
diff --git a/eval.ml b/eval.ml
@@ -6,6 +6,7 @@ module V = Value
* cases? *)
(* TODO: Lazily evaluate args? *)
+(*
let rec define_data_args
: V.environment -> V.value -> I.patt -> V.environment
= fun env value {disc; _} -> match value, disc with
@@ -31,22 +32,25 @@ let rec define_data_args
!env
| _, I.DData _ ->
impossible "Eval.define_along_patt: value is not data, but disc is"
+*)
-let rec eval env = function
+let rec eval
+: V.environment -> I.term -> V.value
+= fun env -> function
| I.Let (definers, body) ->
let ndefiners = Array.length definers in
-
let vars = Uniq.fresh ndefiners in
let env = Env.bind env vars in
-
let env = ref env in
for i = 0 to ndefiners - 1 do
- let vrhs = V.Rec {env; rhs = definers.(i).rhs} in
+ let vrhs = V.RefClo (env, definers.(i).rhs) in
env := Env.define !env (Uniq.get vars i) vrhs
done;
eval !env body
| I.Match {scrutinee; cases; switch} ->
+ no_impl "eval match"
+(*
let scrutinee = eval env scrutinee in
let vars = Uniq.fresh 1 in
let var = Uniq.get vars 0 in
@@ -62,6 +66,7 @@ let rec eval env = function
eval env body
| None -> V.Match {scrutinee; clo = env; cases; switch}
end
+*)
| I.App (fn, args) -> apply (eval env fn) (Array.map (eval env) args)
@@ -74,8 +79,7 @@ let rec eval env = function
tag;
tagi;
args = Array.map (eval env) args;
- clo = env;
- datatype;
+ datatype_clo = (env, datatype);
}
| I.DataType datatype -> V.DataTypeClosure (env, datatype)
@@ -93,6 +97,7 @@ let rec eval env = function
| I.Builtin b -> V.Builtin b
+(*
and do_switch env ij = function
| Switch {index = ij'; subswitches; _} ->
let var = Env.index env ij in
@@ -111,30 +116,37 @@ and do_switch env ij = function
| None -> impossible "Eval.switch: undefined variable"
end
| Goto casei -> Some casei
+*)
-and apply fn args = match fn, args with
-| V.Rec {env; rhs}, args -> apply (eval !env rhs) args
-| V.FnClosure (clo, {multibinder = {binders; _}; body; _}), args ->
+and apply
+: V.value -> V.value array -> V.value
+= fun fn args -> match fn, args with
+| V.RefClo (env, t), args -> apply (eval !env t) args
+| V.FnClosure (clo, {multibinder = {binders; _}; term = body}), args ->
let arity = Array.length binders in
let vars = Uniq.fresh arity in
- let clo = ref (Env.bind clo vars) in
+ let clo = Env.bind clo vars in
+ let clo = ref clo in
for i = 0 to arity - 1 do
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)
-| fn, args -> V.App (fn, args)
+| fn, args -> V.NeutralApp (fn, args)
(* TODO: This is inefficient. We should do something smarter, like lifting
* stuck variables to the outside of neutral terms so we can force them without
- * needing to recurse. *)
-and force env = function
-| V.Rec {env = env'; rhs} -> force env (eval !env' rhs)
+ * needing to recurse (i.e., use spine form). *)
+and force
+: V.environment -> V.value -> V.value
+= fun env -> function
+| V.RefClo (env', t) -> force env (eval !env' t)
+| V.NeutralMatch _ -> no_impl "force neutral match"
(* XXX: There's no reason to force the arguments for "CbNeed redexes" (i.e.,
* when fn is a lambda), but we do need to force args in a "CbValue redex"
* (i.e., when fn is a builtin with builtin reduction rules). *)
-| V.App (fn, args) -> apply (force env fn) (Array.map (force env) args)
+| V.NeutralApp (fn, args) -> apply (force env fn) (Array.map (force env) args)
| V.Arb var ->
begin match Env.eval env var with
| Some v -> force env v
diff --git a/inc_array.ml b/inc_array.ml
@@ -7,10 +7,16 @@ type 'a t = {
data: 'a array;
}
-let make n = {length = 0; data = Array.make n garbage}
+let make
+: 'a. int -> 'a t
+= fun n -> {length = 0; data = Array.make n garbage}
-let add a v =
+let add
+: 'a. 'a t -> 'a -> unit
+= fun a v ->
a.data.(a.length) <- v;
a.length <- a.length + 1
-let to_array a = a.data
+let to_array
+: 'a. 'a t -> 'a array
+= fun a -> a.data
diff --git a/index.ml b/index.ml
@@ -8,5 +8,7 @@
type index = Of of int * int
type t = index
-let pp_print ppf (Of (i, j)) =
+let pp_print
+: Format.formatter -> index -> unit
+= fun ppf (Of (i, j)) ->
Format.fprintf ppf "%d.%d" i j
diff --git a/internal.ml b/internal.ml
@@ -45,22 +45,22 @@ type term =
switch: switch;
}
| App of term * term array
-| Fn of fn
-| FnType of fntype
+| Fn of abstraction
+| FnType of abstraction
| Data of {
- tag: Name.Ctor.t;
+ tag: Name.Tag.t;
tagi: int;
args: term array;
datatype: datatype;
}
| DataType of datatype
| Nat of Z.t
-| Var of Index.t (* TODO: Store type on here or in env? *)
+| Var of Index.t
| Type
| Builtin of builtin
and definer = {
- names: Name.Var.t node array;
+ names: Name.Var.t array;
rhs: term;
typ: term;
}
@@ -70,41 +70,9 @@ and case = {
body: term;
}
-(* Decision tree of match. Switch is an internal node that switches on a
- * non-empty datatype, and Goto is a leaf node that jumps to the indicated
- * case. *)
-and switch =
-| Switch of {
- index: Index.t;
- subswitches: switch array;
- names: int Name.Ctor.Map.t; (* For pretty-printing. *)
-}
-| Goto of int
-
-(* TODO: Generalize binders/multibinders to include discriminants, i.e.,
- * generalize from linear to tree structure. When we bind such a binder,
- * we also establish some definitions according to the tree structure.
-
and binder = {
plicity: Plicity.t;
- names: Name.Var.t node array;
- disc: discriminant;
- typ: term;
-}
-
-and discriminant =
-| DWild
-| DData of {
- tag: Name.Ctor.t;
- tagi: int;
- sub: multibinder;
-}
-*)
-
-and binder = {
- plicity: Plicity.t;
- names: Name.Var.t node array;
- typ: term;
+ patt: patt;
}
and multibinder = {
@@ -112,34 +80,45 @@ and multibinder = {
order: int array;
}
-and fn = {
+and abstraction = {
multibinder: multibinder;
- body: term;
- codomain: term;
-}
-
-and fntype = {
- multibinder: multibinder;
- codomain: term;
-}
-
-and datatype = {
- ctors: multibinder array;
- names: int Name.Ctor.Map.t; (* TODO: Rename to "tagis" for consistency *)
+ term: term;
}
and patt = {
- names: Name.Var.t node array;
+ names: Name.Var.t array;
disc: discriminant;
}
and discriminant =
-| DWild
+| DWild of term
| DData of data_discriminant
and data_discriminant = {
- tag: Name.Ctor.t;
+ tag: Name.Tag.t;
tagi: int;
subpatts: patt array;
datatype: datatype;
}
+
+(* Decision tree of match. Switch is an internal node that switches on a
+ * non-empty datatype, and Goto is a leaf node that jumps to the indicated
+ * case. *)
+and switch =
+| Switch of {
+ index: Index.t;
+ subswitches: switch array;
+ names: int Name.Tag.Map.t; (* For pretty-printing. *)
+}
+| Goto of int
+
+and datatype = {
+ ctors: multibinder array;
+ names: int Name.Tag.Map.t; (* TODO: Rename to "tagis" for consistency *)
+}
+
+let disc_type
+: discriminant -> term
+= function
+| DWild typ -> typ
+| DData {datatype; _} -> DataType datatype
diff --git a/loc.ml b/loc.ml
@@ -10,7 +10,9 @@ type loc =
}
type t = loc
-let of_positions beg_pos end_pos =
+let of_positions
+: position -> position -> loc
+= fun beg_pos end_pos ->
Loc {
beg_row = beg_pos.pos_lnum;
beg_col = beg_pos.pos_cnum - beg_pos.pos_bol;
@@ -18,7 +20,21 @@ let of_positions beg_pos end_pos =
end_col = end_pos.pos_cnum - end_pos.pos_bol;
}
-let pp_print ppf = function
+let of_locs
+: loc -> loc -> loc
+= fun beg_loc end_loc -> match beg_loc, end_loc with
+| Loc b, Loc e ->
+ Loc {
+ beg_row = b.beg_row;
+ beg_col = b.beg_col;
+ end_row = e.end_row;
+ end_col = e.end_col;
+ }
+| Nowhere, _ | _, Nowhere -> Nowhere
+
+let pp_print
+: Format.formatter -> loc -> unit
+= fun ppf -> function
| Nowhere -> Format.pp_print_string ppf "?"
| Loc {beg_row; beg_col; end_row; end_col} ->
Format.fprintf ppf "%d:%d-%d:%d" beg_row beg_col end_row end_col
diff --git a/main.ml b/main.ml
@@ -69,25 +69,24 @@ let buf = Lexing.from_string "\
let ctx =
let nat_binder = {
I.plicity = Plicity.Ex;
- I.names = [|
- Loc.Nowhere @$ Name.Var.Of "a";
- Loc.Nowhere @$ Name.Var.Of "b";
- |];
- I.typ = I.Builtin I.NatType;
+ 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|]};
- codomain = I.Builtin I.NatType;
+ term = I.Builtin I.NatType;
}) in
let ctx = Ctx.empty in
let (ctx, _) = Ctx.assign ctx
- [|Loc.Nowhere @$ Name.Var.Of "Type"|] V.Type V.Type in
+ [|Name.Var.Of "Type"|] V.Type V.Type in
let (ctx, _) = Ctx.assign ctx
- [|Loc.Nowhere @$ Name.Var.Of "Nat"|] V.Type (V.Builtin I.NatType) in
+ [|Name.Var.Of "Nat"|] V.Type (V.Builtin I.NatType) in
let (ctx, _) = Ctx.assign ctx
- [|Loc.Nowhere @$ Name.Var.Of "`+"|] nat_op_typ (V.Builtin I.NatOpAdd) in
+ [|Name.Var.Of "`+"|] nat_op_typ (V.Builtin I.NatOpAdd) in
let (ctx, _) = Ctx.assign ctx
- [|Loc.Nowhere @$ Name.Var.Of "`*"|] nat_op_typ (V.Builtin I.NatOpMul) in
+ [|Name.Var.Of "`*"|] nat_op_typ (V.Builtin I.NatOpMul) in
ctx
let print fmt a =
diff --git a/name.ml b/name.ml
@@ -1,9 +1,13 @@
-let non_start c = false
+let non_start
+: char -> bool
+= fun c -> false
|| ('0' <= c && c <= '9')
|| c = '\''
|| c = '"'
-let non_cont c = false
+let non_cont
+: char -> bool
+= fun c -> false
|| c < '\''
|| ('\'' < c && c < '0')
|| ('9' < c && c < 'A')
@@ -23,39 +27,44 @@ module Var = struct
module Set = Set.Make(Ord)
- let requires_quotes (Of s) = false
+ let requires_quotes
+ : var -> bool
+ = fun (Of s) -> false
|| String.length s = 0
|| non_start s.[0]
|| String.exists non_cont s
- let pp_print ppf (Of s as name) =
+ let pp_print
+ : Format.formatter -> var -> unit
+ = fun ppf (Of s as name) ->
if requires_quotes name then
Format.fprintf ppf "`%s`" s
else
Format.fprintf ppf "%s" s
end
-module Ctor = struct
- type ctor = Of of string
- type t = ctor
+module Tag = struct
+ type tag = Of of string
+ type t = tag
module Ord = struct
- type t = ctor
+ type t = tag
let compare (Of x) (Of y) = String.compare x y
end
module Map = Map.Make(Ord)
- let equal (Of x) (Of y) = String.equal x y
-
- let requires_quotes (Of s) = false
+ let requires_quotes
+ : tag -> bool
+ = fun (Of s) -> false
|| String.length s = 0
|| String.exists non_cont s
- let pp_print ppf (Of s as name) =
+ let pp_print
+ : Format.formatter -> tag -> unit
+ = fun ppf (Of s as name) ->
if requires_quotes name then
Format.fprintf ppf "%@`%s`" s
else
Format.fprintf ppf "%@%s" s
end
-
diff --git a/parser.mly b/parser.mly
@@ -27,7 +27,7 @@ and expr' =
| App of expr * int * expr list
| Fn of int * C.param list * expr
| FnType of int * C.domain list * expr
-| Variant of C.ctor_name * int * expr list
+| Variant of C.tag_name * int * expr list
| VariantType of int * ctor list
| Tuple of int * expr list
| TupleType of int * C.domain list
@@ -39,7 +39,7 @@ and expr' =
| Paren of expr
and ctor = ctor' node
-and ctor' = Ctor of C.ctor_name * int * C.domain list
+and ctor' = Ctor of C.tag_name * int * C.domain list
let cons a (len, lst) = (len + 1, a :: lst)
@@ -163,7 +163,7 @@ expr2: (* Type annotations (right-associative) *)
| expr3 { $1 }
expr3: (* Function arrow (right-associative) *)
- | expr6 SINGLE_ARROW expr3 {
+ | expr5 SINGLE_ARROW expr3 {
let dom = loc_of 1 @$ C.ExplicitDomain (term $1) in
loc () @$ FnType (1, [dom], $3)
}
@@ -242,7 +242,6 @@ expr5:
| expr6 { $1 }
expr6:
- | ctor_name { loc () @$ Variant ($1, 0, []) }
| UNDERSCORE { loc () @$ Underscore }
| indexed_var_name {
let (x, i) = $1 in
@@ -250,18 +249,19 @@ expr6:
}
| var_name { loc () @$ Var $1 }
| NAT { loc () @$ Nat $1 }
+ | tag_name { loc () @$ Variant ($1, 0, []) }
| HASH_LBRACE ctor_list RBRACE {
let (len, lst) = $2 in
loc () @$ VariantType (len, lst)
}
- | HASH_LPAREN domain_list RPAREN {
- let (len, lst) = $2 in
- loc () @$ TupleType (len, lst)
- }
| LPAREN expr1 COMMA expr1_comma_list RPAREN {
let (len, lst) = $4 in
loc () @$ Tuple (len + 1, $2 :: lst)
}
+ | HASH_LPAREN domain_list RPAREN {
+ let (len, lst) = $2 in
+ loc () @$ TupleType (len, lst)
+ }
| LPAREN RPAREN { loc () @$ Unit }
| LPAREN expr0 RPAREN { loc () @$ Paren $2 }
@@ -301,17 +301,23 @@ param_list:
| { (0, []) }
domain:
- | expr3 { loc () @$ C.ExplicitDomain (term $1) }
- | QUESTION expr3 { loc () @$ C.ImplicitTypeDomain (patt $2) }
- | expr3 COLON expr2 { loc () @$ C.AnnotDomain (Plicity.Ex, patt $1, term $3) }
- | QUESTION expr3 COLON expr2 { loc () @$ C.AnnotDomain (Plicity.Im, patt $2, term $4) }
+ | expr1 {
+ match $1.data with
+ | Annot (p, t) -> loc () @$ C.AnnotDomain (Plicity.Ex, patt p, term t)
+ | _ -> loc () @$ C.ExplicitDomain (term $1)
+ }
+ | QUESTION expr2 {
+ match $2.data with
+ | Annot (p, t) -> loc () @$ C.AnnotDomain (Plicity.Im, patt p, term t)
+ | _ -> loc () @$ C.ImplicitTypeDomain (patt $2)
+ }
domain_list:
| domain COMMA domain_list { cons $1 $3 }
| domain { (1, [$1]) }
| { (0, []) }
-ctor_name:
- | TAG { loc () @$ Name.Ctor.Of $1 }
+tag_name:
+ | TAG { loc () @$ Name.Tag.Of $1 }
indexed_var_name:
| INDEXED_NAME {
@@ -323,7 +329,7 @@ var_name:
| NAME { loc () @$ Name.Var.Of $1 }
ctor:
- | ctor_name domain_list {
+ | tag_name domain_list {
let (len, lst) = $2 in
loc () @$ Ctor ($1, len, lst)
}
diff --git a/porig.ml b/porig.ml
@@ -30,7 +30,8 @@ module Intuitionistic: Porig = struct
let to_string Zero = "0"
end
-(* TODO: discrete boolean porig and total boolean porig *)
+(* TODO: module DiscreteBoolean: Porig = struct ... end*)
+(* TODO: module TotalBoolean: Porig = struct ... end*)
module NoneOneTons: Porig = struct
type t = Zero | One | Omega
diff --git a/pretty.ml b/pretty.ml
@@ -30,14 +30,13 @@ and pp_print_term
(pp_print_term 6) fn
pp_print_args args
-| Fn {multibinder = {binders; _}; body; codomain} ->
- pp_print_with_parens m 1 ppf "@[@[<hv 4>fn@ %a%t::@ %a@;<1 -4>@]=>@;<1 4>%a@]"
+| Fn {multibinder = {binders; _}; term = body} ->
+ pp_print_with_parens m 1 ppf "@[@[<hv 4>fn@ %a%t@]=>@;<1 4>%a@]"
pp_print_binders binders
(F.pp_print_custom_break ~fits:(" ", 0, "") ~breaks:(",", -4, ""))
- (pp_print_term 2) codomain
(pp_print_term 1) body
-| FnType {multibinder = {binders; _}; codomain} ->
+| FnType {multibinder = {binders; _}; term = codomain} ->
pp_print_with_parens m 3 ppf "@[@[<hv 4>[@,%a%t@]] ->@;<1 4>%a@]"
pp_print_binders binders
(F.pp_print_custom_break ~fits:("", 0, "") ~breaks:(",", -4, ""))
@@ -45,7 +44,7 @@ and pp_print_term
| Data {tag; args; datatype; _} ->
pp_print_with_parens m 2 ppf "@[@[<4>%a%a@]%t%a@]"
- Name.Ctor.pp_print tag
+ Name.Tag.pp_print tag
pp_print_args args
(F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
(pp_print_term 2) (DataType datatype)
@@ -99,7 +98,7 @@ and pp_print_patt
= fun m ppf -> function
| {names = [||]; disc} ->
pp_print_disc m ppf disc
-| {names; disc = DWild} ->
+| {names; disc = DWild _} ->
pp_print_names m ppf names
| {names; disc = DData _ as disc} ->
(* XXX: The grammar uses precdence 4 for all binops. *)
@@ -110,14 +109,14 @@ and pp_print_patt
and pp_print_disc
: int -> F.formatter -> discriminant -> unit
= fun m ppf -> function
-| DWild ->
+| DWild _ ->
pp_print_with_parens m 6 ppf "_"
| DData {tag; subpatts = [||]; _} ->
pp_print_with_parens m 6 ppf "%a"
- Name.Ctor.pp_print tag
+ Name.Tag.pp_print tag
| DData {tag; subpatts; _} ->
pp_print_with_parens m 5 ppf "%a %a"
- Name.Ctor.pp_print tag
+ Name.Tag.pp_print tag
(F.pp_print_array ~pp_sep:F.pp_print_space (pp_print_patt 6)) subpatts
and pp_print_switch
@@ -132,16 +131,16 @@ and pp_print_switch
casei
and pp_print_subswitches
-: F.formatter -> switch array * int Name.Ctor.Map.t -> unit
+: F.formatter -> switch array * int Name.Tag.Map.t -> unit
= fun ppf -> function
| ([||], _) -> ()
| (subswitches, names) ->
(* TODO: Doing this conversion sucks. *)
- let names = Array.of_list (Name.Ctor.Map.to_list names) in
+ 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@],"
- Name.Ctor.pp_print tag
+ Name.Tag.pp_print tag
pp_print_switch subswitches.(i)
done;
F.fprintf ppf "@;<0 -4>"
@@ -161,12 +160,12 @@ and pp_print_binders
and pp_print_binder
: F.formatter -> binder -> unit
-= fun ppf {plicity; names; typ} ->
+= fun ppf {plicity; patt = {names; disc}} ->
F.fprintf ppf "@[%a%a%t%a@]"
pp_print_plicity plicity
(pp_print_names 3) names
(F.pp_print_custom_break ~fits:(": ", 0, "") ~breaks:(" :", 4, ""))
- (pp_print_term 2) typ
+ (pp_print_term 2) (disc_type disc)
and pp_print_plicity
: F.formatter -> Plicity.t -> unit
@@ -175,19 +174,19 @@ and pp_print_plicity
| Plicity.Ex -> ()
and pp_print_ctors
-: F.formatter -> multibinder array * int Name.Ctor.Map.t -> unit
+: F.formatter -> multibinder array * int Name.Tag.Map.t -> unit
= fun ppf (ctors, names) ->
let first = ref true in
- Name.Ctor.Map.iter (fun tag tagi ->
+ Name.Tag.Map.iter (fun tag tagi ->
begin if not !first then
F.fprintf ppf ";@ ";
first := false
end;
match ctors.(tagi).binders with
- | [||] -> Name.Ctor.pp_print ppf tag
+ | [||] -> Name.Tag.pp_print ppf tag
| binders ->
F.fprintf ppf "@[<4>%a@ %a@]"
- Name.Ctor.pp_print tag
+ Name.Tag.pp_print tag
pp_print_binders binders
) names
@@ -199,21 +198,17 @@ and pp_print_builtin
| NatOpMul -> F.fprintf ppf "~*"
and pp_print_names
-: int -> F.formatter -> Name.Var.t node array -> unit
+: int -> F.formatter -> Name.Var.t array -> unit
= fun m ppf -> function
| [||] ->
pp_print_with_parens m 6 ppf "_"
| [|name|] ->
pp_print_with_parens m 6 ppf "%a"
- pp_print_name name
+ Name.Var.pp_print name
| names ->
(* XXX: The grammar uses precdence 4 for all binops. *)
pp_print_with_parens m 4 ppf "%a"
- (F.pp_print_array ~pp_sep:pp_print_and pp_print_name) names
-
-and pp_print_name
-: F.formatter -> Name.Var.t node -> unit
-= fun ppf {data = name; _} -> Name.Var.pp_print ppf name
+ (F.pp_print_array ~pp_sep:pp_print_and Name.Var.pp_print) names
and pp_print_comma
: F.formatter -> unit -> unit
diff --git a/quote.ml b/quote.ml
@@ -3,42 +3,72 @@ open Eval
module I = Internal
module V = Value
-let rec quote env = function
-| V.Rec {env = env'; rhs} -> quote env (eval !env' rhs)
(*
-| V.Match {scrutinee; clo; cases; switch} ->
- let scrutinee = quote env scrutinee in
- let ncases = Array.length cases in
- let cases' = Array.make ncases garbage in
- for i = 0 to ncases - 1 do
- let {I.patt; I.body} = cases.(i) in
- let vars = Uniq.fresh 1 in
- let env = Env.bind env vars in
- let env = define_data_args env scrutinee patt in
+let rec bind_and_define_subpatts
+: V.environment -> Uniq.uniq -> I.patt -> V.environment
+= fun env var {disc; _} -> match disc with
+| I.DWild -> env
+| I.DData {tag; tagi; subpatts; datatype} ->
+ let arity = Array.length subpatts in
+ let subvars = Uniq.fresh arity in
+ let data = V.Data {
+ tag;
+ tagi;
+ args = Array.init arity (fun i -> V.Arb (Uniq.get subvars i));
+ datatype_clo = (env, datatype);
+ } in
+ let env = Env.bind env subvars in
+ let env = Env.define env var data in
+
+ let env = ref env in
+ for i = 0 to arity - 1 do
+ let subvar = Uniq.get subvars i in
+ env := bind_and_define_subpatts !env subvar subpatts.(i)
done;
- I.Match {scrutinee; ; switch}
+
+ !env
*)
-| V.App (fn, args) -> I.App (quote env fn, Array.map (quote env) args)
-| V.FnClosure (clo, {multibinder; body; codomain}) ->
- let (env, clo, multibinder) =
- bind_and_quote_multibinder env clo multibinder in
- let body = quote env (eval clo body) in
- let codomain = quote env (eval clo codomain) in
- I.Fn {multibinder; body; codomain}
-| V.FnTypeClosure (clo, {multibinder; codomain}) ->
- let (env, clo, multibinder) =
- bind_and_quote_multibinder env clo multibinder in
- let codomain = quote env (eval clo codomain) in
- I.FnType {multibinder; codomain}
-| V.Data {tag; tagi; args; clo; datatype} ->
+
+let rec bind_patt_twice
+: V.environment * V.environment -> I.patt -> V.environment * V.environment
+= fun (env0, env1) {disc; _} ->
+ let vars = Uniq.fresh 1 in
+ let env0 = Env.bind env0 vars in
+ let env1 = Env.bind env1 vars in
+ match disc with
+ | I.DWild _ -> (env0, env1)
+ | I.DData {subpatts; _} ->
+ let arity = Array.length subpatts in
+ let subvars = Uniq.fresh arity in
+ let env0 = Env.bind env0 subvars in
+ let env1 = Env.bind env1 subvars in
+ Array.fold_left bind_patt_twice (env0, env1) subpatts
+
+let rec quote
+: V.environment -> V.value -> I.term
+= fun env -> function
+| V.RefClo (env', t) -> shift env !env' t
+| V.NeutralMatch {scrutinee; cases_clo = (clo, cases); switch} ->
+ I.Match {
+ scrutinee = quote env scrutinee;
+ cases = Array.map (shift_case env clo) cases;
+ switch;
+ }
+| V.NeutralApp (fn, args) ->
+ I.App (quote env fn, Array.map (quote env) args)
+| V.FnClosure (clo, abs) ->
+ I.Fn (shift_abstraction env clo abs)
+| V.FnTypeClosure (clo, abs) ->
+ I.FnType (shift_abstraction env clo abs)
+| V.Data {tag; tagi; args; datatype_clo = (clo, datatype)} ->
I.Data {
tag;
tagi;
args = Array.map (quote env) args;
- datatype = quote_datatype env clo datatype;
+ datatype = shift_datatype env clo datatype;
}
| V.DataTypeClosure (clo, datatype) ->
- I.DataType (quote_datatype env clo datatype)
+ I.DataType (shift_datatype env clo datatype)
| V.Nat n -> I.Nat n
| V.Arb var ->
begin match Env.quote env var with
@@ -49,26 +79,81 @@ let rec quote env = function
| V.Builtin b -> I.Builtin b
| V.Future _ -> impossible "Eval.quote: can not quote future"
-and quote_datatype env clo {ctors; names} = {
- ctors = Array.map (quote_multibinder env clo) ctors;
- names;
-}
+and shift
+: V.environment -> V.environment -> I.term -> I.term
+= fun dst src t -> quote dst (eval src t)
+
+and shift_case
+: V.environment -> V.environment -> I.case -> I.case
+= fun dst src {patt; body} ->
+ let patt = shift_patt dst src patt in
+ let (dst, src) = bind_patt_twice (dst, src) patt in
+ let body = shift dst src body in
+ {patt; body}
-and bind_and_quote_multibinder env clo {binders; order} =
+and shift_binder
+: V.environment -> V.environment -> I.binder -> I.binder
+= fun dst src {plicity; patt} ->
+ {
+ plicity;
+ patt = shift_patt dst src patt;
+ }
+
+and bind_and_shift_multibinder
+: V.environment -> V.environment -> I.multibinder
+ -> V.environment * V.environment * I.multibinder
+= fun dst src {binders; order} ->
let arity = Array.length binders in
let vars = Uniq.fresh arity in
- let env = Env.bind env vars in
- let clo = Env.bind clo vars in
- let binders' = Array.make arity garbage in
- for i = 0 to arity - 1 do
- (* TODO: This does not need to be done in order. *)
- let j = order.(i) in
- let typ = quote env (eval clo binders.(j).typ) in
- binders'.(j) <- {binders.(j) with typ}
- done;
- (env, clo, {binders = binders'; order})
+ let dst = Env.bind dst vars in
+ let src = Env.bind src vars in
+ let multibinder = {
+ I.binders = Array.map (shift_binder dst src) binders;
+ I.order;
+ } in
+ (dst, src, multibinder)
-and quote_multibinder env clo multibinder =
+and shift_multibinder
+: V.environment -> V.environment -> I.multibinder -> I.multibinder
+= fun dst src multibinder ->
let (_, _, multibinder) =
- bind_and_quote_multibinder env clo multibinder in
+ bind_and_shift_multibinder dst src multibinder in
multibinder
+
+and shift_abstraction
+: V.environment -> V.environment -> I.abstraction -> I.abstraction
+= fun dst src {multibinder; term} ->
+ let (dst, src, multibinder) =
+ bind_and_shift_multibinder dst src multibinder in
+ {
+ multibinder;
+ term = shift dst src term;
+ }
+
+and shift_patt
+: V.environment -> V.environment -> I.patt -> I.patt
+= fun dst src {names; disc} ->
+ {
+ names;
+ disc = shift_disc dst src disc;
+ }
+
+and shift_disc
+: V.environment -> V.environment -> I.discriminant -> I.discriminant
+= fun dst src -> function
+| I.DWild typ -> I.DWild (shift dst src typ)
+| I.DData {tag; tagi; subpatts; datatype} ->
+ I.DData {
+ tag;
+ tagi;
+ subpatts = Array.map (shift_patt dst src) subpatts;
+ datatype = shift_datatype dst src datatype;
+ }
+
+and shift_datatype
+: V.environment -> V.environment -> I.datatype -> I.datatype
+= fun dst src {ctors; names} ->
+ {
+ ctors = Array.map (shift_multibinder dst src) ctors;
+ names;
+ }
diff --git a/unify.ml b/unify.ml
@@ -3,74 +3,133 @@ open Eval
module I = Internal
module V = Value
-(* TODO: Actually make this perform unification, not conversion checking *)
-let rec conv env v0 v1 = match force env v0, force env v1 with
+exception UnifyFail
+
+(* TODO: Make this actually solve metas *)
(* TODO: η-equality? *)
-(* TODO: Switch *)
-| V.Rec _, _ -> impossible "Unify.conv: Rec's are removed during forcing"
-| _, V.Rec _ -> impossible "Unify.conv: Rec's are removed during forcing"
-| V.App (fn0, args0), V.App (fn1, args1) ->
- (* Note that aargs and bargs aren't necessarily the same length, but they
- * are if fn0 and fn1 are convertible, so the short-circuiting of (&&)
- * ensures that for_all2 can't fail. *)
- conv env fn0 fn1 && Array.for_all2 (conv env) args0 args1
-| V.FnClosure (clo0, fn0), V.FnClosure (clo1, fn1) ->
- let arity = Array.length fn0.multibinder.binders in
- let vars = Uniq.fresh arity in
- let env = Env.bind env vars in
- let clo0, clo1 = Env.bind clo0 vars, Env.bind clo1 vars in
- let vbody0, vbody1 = eval clo0 fn0.body, eval clo1 fn1.body in
- conv env vbody0 vbody1
-| V.FnTypeClosure (clo0, fntype0), V.FnTypeClosure (clo1, fntype1) ->
- let {I.multibinder = multibinder0; I.codomain = codomain0} = fntype0 in
- let {I.multibinder = multibinder1; I.codomain = codomain1} = fntype1 in
- begin match bind_and_conv_multibinder env clo0 clo1
- multibinder0 multibinder1 with
- | Some (env, clo0, clo1) ->
- let vcodomain0 = eval clo0 codomain0 in
- let vcodomain1 = eval clo1 codomain1 in
- conv env vcodomain0 vcodomain1
- | None -> false
- end
-| V.Data {tag = tag0; args = args0; _}, V.Data {tag = tag1; args = args1; _} ->
- tag0 = tag1 && Array.for_all2 (conv env) args0 args1
+(* Precondition: Both values have the same type. *)
+let rec unify
+: V.environment -> V.value -> V.value -> unit
+= fun env v0 v1 -> match force env v0, force env v1 with
+| V.RefClo _, _ -> impossible "Unify.unify: RefClo's are removed during forcing"
+| _, V.RefClo _ -> impossible "Unify.unify: RefClo's are removed during forcing"
+| V.NeutralMatch _, V.NeutralMatch _ -> no_impl "unify neutral match"
+| V.NeutralApp (fn0, args0), V.NeutralApp (fn1, args1) ->
+ (* Note that args0 and args1 aren't necessarily the same length, but they
+ * are if fn0 and fn1 unify, so the short-circuiting of (&&) ensures that
+ * for_all2 can't fail. *)
+ (* XXX: fn0 and fn1 needn't have the same type, so we are technically not
+ * obeying the precondition of unify here. However, it's ok in this case,
+ * because fn0 and fn1 can't be Fn's. Rather, fn0 and fn1 are either
+ * variables or builtins, which will fail to unify if they have different
+ * types. *)
+ unify env fn0 fn1;
+ Array.iter2 (unify env) args0 args1
+| V.FnClosure (clo0, abs0), V.FnClosure (clo1, abs1) ->
+ (* XXX: Testing the entire abstraction for conversion is overkill: Since
+ * both Fn's are assumed to have the same type, we know both multibinders
+ * are convertible, so it suffices to bind fresh variables in the envs and
+ * then test the bodies for conversion. *)
+ conv_abstraction env clo0 clo1 abs0 abs1
+| V.FnTypeClosure (clo0, abs0), V.FnTypeClosure (clo1, abs1) ->
+ conv_abstraction env clo0 clo1 abs0 abs1
+| V.Data {tagi = tagi0; args = args0; _}, V.Data {tagi = tagi1; args = args1; _} ->
+ begin if tagi0 <> tagi1 then
+ raise UnifyFail
+ end;
+ Array.iter2 (unify env) args0 args1
| V.DataTypeClosure (clo0, datatype0), V.DataTypeClosure (clo1, datatype1) ->
- let {I.ctors = ctors0; I.names = names0} = datatype0 in
- let {I.ctors = ctors1; I.names = names1} = datatype1 in
- Array.for_all2 (conv_multibinder env clo0 clo1) ctors0 ctors1 &&
- Name.Ctor.Map.equal Int.equal names0 names1
-| V.Nat n, V.Nat m -> Z.equal n m
-| V.Arb var0, V.Arb var1 -> var0 = var1
-| V.Type, V.Type -> true
-| V.Builtin b0, V.Builtin b1 -> b0 = b1
-| V.Future _, _ -> impossible "Unify.conv: Future tested for conversion"
-| _, V.Future _ -> impossible "Unify.conv: Future tested for conversion"
-| _, _ -> false
+ 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 _), _ ->
+ raise UnifyFail
+
+and conv
+: V.environment -> V.environment -> V.environment -> I.term -> I.term -> unit
+= fun env clo0 clo1 t0 t1 ->
+ let v0 = eval clo0 t0 in
+ let v1 = eval clo1 t1 in
+ unify env v0 v1
+
+and conv_binder
+: V.environment -> V.environment -> V.environment
+ -> I.binder -> I.binder -> unit
+= fun env clo0 clo1 binder0 binder1 ->
+ begin if binder0.plicity <> binder1.plicity then
+ raise UnifyFail
+ end;
+ conv_patt env clo0 clo1 binder0.patt binder1.patt
+
+and bind_and_conv_multibinder
+: V.environment -> V.environment -> V.environment
+ -> I.multibinder -> I.multibinder
+ -> V.environment * V.environment * V.environment
+= fun env clo0 clo1 multibinder0 multibinder1 ->
+ let arity0 = Array.length multibinder0.binders in
+ let arity1 = Array.length multibinder1.binders in
+ begin if arity0 <> arity1 then
+ raise UnifyFail
+ end;
+
+ begin if not @@ Array.for_all2 Int.equal
+ multibinder0.order multibinder1.order then
+ raise UnifyFail
+ end;
+
+ let vars = Uniq.fresh arity0 in
+ let env = Env.bind env vars in
+ let clo0 = Env.bind clo0 vars in
+ let clo1 = Env.bind clo1 vars in
+ Array.iter2 (conv_binder env clo0 clo1)
+ multibinder0.binders multibinder1.binders;
+
+ (env, clo0, clo1)
+
+and conv_multibinder
+: V.environment -> V.environment -> V.environment
+ -> I.multibinder -> I.multibinder -> unit
+= fun env clo0 clo1 multibinder0 multibinder1 ->
+ ignore @@ bind_and_conv_multibinder env clo0 clo1 multibinder0 multibinder1
+
+and conv_abstraction
+: V.environment -> V.environment -> V.environment
+ -> I.abstraction -> I.abstraction -> unit
+= fun env clo0 clo1 abs0 abs1 ->
+ let (env, clo0, clo1) = bind_and_conv_multibinder env clo0 clo1
+ abs0.multibinder abs1.multibinder in
+ conv env clo0 clo1 abs0.term abs1.term
+
+and conv_patt
+: V.environment -> V.environment -> V.environment -> I.patt -> I.patt -> unit
+= fun env clo0 clo1 patt0 patt1 ->
+ conv_disc env clo0 clo1 patt0.disc patt1.disc
-and bind_and_conv_multibinder env clo0 clo1 multibinder0 multibinder1 =
- let {I.binders = binders0; I.order = order0} = multibinder0 in
- let {I.binders = binders1; I.order = order1} = multibinder1 in
- let arity0 = Array.length binders0 in
- let arity1 = Array.length binders1 in
- if arity0 = arity1 then
- let vars = Uniq.fresh arity0 in
- let env = Env.bind env vars in
- let clo0 = Env.bind clo0 vars in
- let clo1 = Env.bind clo1 vars in
- let domain_conv i0 i1 =
- i0 = i1 && binders0.(i0).plicity = binders1.(i1).plicity &&
- let vtyp0 = eval clo0 binders0.(i0).typ in
- let vtyp1 = eval clo1 binders1.(i1).typ in
- conv env vtyp0 vtyp1 in
- if Array.for_all2 domain_conv order0 order1 then
- Some (env, clo0, clo1)
- else
- None
- else
- None
+and conv_disc
+: V.environment -> V.environment -> V.environment
+ -> I.discriminant -> I.discriminant -> unit
+= fun env clo0 clo1 disc0 disc1 -> match disc0, disc1 with
+| I.DWild typ0, I.DWild typ1 ->
+ conv env clo0 clo1 typ0 typ1
+| I.DData data0, I.DData data1 ->
+ conv_datatype env clo0 clo1 data0.datatype data1.datatype;
+ begin if data0.tagi <> data1.tagi then
+ raise UnifyFail
+ end;
+ Array.iter2 (conv_patt env clo0 clo1) data0.subpatts data1.subpatts
+| I.DWild _, I.DData _ -> raise UnifyFail
+| I.DData _, I.DWild _ -> raise UnifyFail
-and conv_multibinder env clo0 clo1 multibinder0 multibinder1 =
- match bind_and_conv_multibinder env clo0 clo1
- multibinder0 multibinder1 with
- | Some _ -> true
- | None -> false
+and conv_datatype
+: V.environment -> V.environment -> V.environment
+ -> I.datatype -> I.datatype -> unit
+= fun env clo0 clo1 datatype0 datatype1 ->
+ Array.iter2 (conv_multibinder env clo0 clo1) datatype0.ctors datatype1.ctors;
+ if not @@ Name.Tag.Map.equal Int.equal datatype0.names datatype1.names then
+ raise UnifyFail
diff --git a/uniq.ml b/uniq.ml
@@ -2,6 +2,9 @@
* the semantic domain, but they can be used any time we need a unique
* identifier. *)
+(* TODO: Separate uniq and range? Having them in the same module is not really
+ * consistent with what we do elsewhere. *)
+
open Util
type uniq = Uniq of int
@@ -9,7 +12,9 @@ type range = Range of int * int
exception Exhaustion
-let fresh =
+let fresh
+: int -> range
+=
let next = ref 0 in
fun n ->
if !next > max_int - n then
@@ -19,9 +24,13 @@ let fresh =
next := !next + n;
r
-let length (Range (_, l)) = l
+let length
+: range -> int
+= fun (Range (_, l)) -> l
-let get (Range (b, l)) i =
+let get
+: range -> int -> uniq
+= fun (Range (b, l)) i ->
if i < 0 || i >= l then
invalid_arg "Uniq.get"
else
@@ -69,9 +78,13 @@ module RangeMap = struct
let empty: t = M.empty
- let add (Range (b, l)) v m = M.add (K.Key (b, l)) (v, b) m
+ let add
+ : range -> V.v -> t -> t
+ = fun (Range (b, l)) v m -> M.add (K.Key (b, l)) (v, b) m
- let find_opt (Uniq x) m =
+ let find_opt
+ : uniq -> t -> V.v' option
+ = fun (Uniq x) m ->
match M.find_opt (K.Query x) m with
| Some (v, b) -> Some (V.offset v (x - b))
| None -> None
diff --git a/util.ml b/util.ml
@@ -1,11 +1,18 @@
-let impossible reason = failwith ("impossible: " ^ reason)
-let no_impl feature = failwith ("no impl: " ^ feature)
+let impossible
+: 'a. string -> 'a
+= fun reason -> failwith ("impossible: " ^ reason)
+
+let no_impl
+: 'a. string -> 'a
+= fun feature -> failwith ("no impl: " ^ feature)
(* For creating uninitialized arrays *)
-let garbage = Obj.magic 0
+let garbage: 'a. 'a = Obj.magic 0
(* For some reason this isn't in the standard Array module... *)
-let fold_left2 f acc xs ys =
+let fold_left2
+: 'acc 'a 'b. ('acc -> 'a -> 'b -> 'acc) -> 'acc -> 'a array -> 'b array -> 'acc
+= fun f acc xs ys ->
begin if Array.length xs <> Array.length ys then
invalid_arg "Util.fold_left2"
end;
diff --git a/value.ml b/value.ml
@@ -1,27 +1,22 @@
module I = Internal
type value =
-| Rec of {
- env: environment ref;
- rhs: I.term;
-}
-| Match of {
+| RefClo of environment ref * I.term
+| NeutralMatch of {
scrutinee: value;
- clo: environment;
- cases: I.case array;
+ cases_clo: I.case array closure;
switch: I.switch;
}
-| App of value * value array
-| FnClosure of environment * I.fn
-| FnTypeClosure of environment * I.fntype
+| NeutralApp of value * value array
+| FnClosure of I.abstraction closure
+| FnTypeClosure of I.abstraction closure
| Data of {
- tag: Name.Ctor.t;
+ tag: Name.Tag.t;
tagi: int;
args: value array;
- clo: environment;
- datatype: I.datatype;
+ datatype_clo: I.datatype closure;
}
-| DataTypeClosure of environment * I.datatype
+| DataTypeClosure of I.datatype closure
| Nat of Z.t
| Arb of Uniq.uniq
(*| Meta of ...*)
@@ -30,3 +25,5 @@ type value =
| Future of Uniq.uniq * int
and environment = value Env.environment
+
+and 'a closure = environment * 'a
