From 6b4797fcd33290122bdde9cd89f8dfe65e90b307 Mon Sep 17 00:00:00 2001 From: Josh Brown Date: Thu, 02 Apr 2026 04:04:03 +0000 Subject: [PATCH] simplify coercions --- src/AtomDef.res | 51 ++++++++------------------------------------------- src/Coercible.res | 44 +++++++++++++++++++------------------------- src/SExp.res | 4 ++-- src/StringA.res | 5 ----- src/Symbolic.res | 5 ----- 5 file(s) changed, 29 insertion(s)(+), 80 deletion(s)(-) diff --git a/src/AtomDef.res b/src/AtomDef.res --- a/src/AtomDef.res +++ b/src/AtomDef.res @@ -1,12 +1,10 @@ // type level stuff to enable well-typed coercions type atomTag<_> = .. -type rec eq<_, _> = Refl: eq<'a, 'a> module type ATOM = { type t type subst = Map.t type atomTag<_> += Tag: atomTag - let tagEq: atomTag<'a> => option> let unify: (t, t, ~gen: ref=?) => Seq.t let prettyPrint: (t, ~scope: array) => string let parse: (string, ~scope: array, ~gen: ref=?) => result<(t, string), string> @@ -19,41 +17,12 @@ type rec hValue = HValue(atomTag<'a>, 'a): hValue module type COERCIBLE_ATOM = { include ATOM - let liftHValue: hValue => option - let getHValue: t => hValue + let coerce: hValue => option } type loweredSExp = Var({idx: int}) | Schematic({schematic: int, allowed: array}) type atomTag<_> += SExpTag: atomTag -let tagEqSExp = (type a, tag: atomTag): option> => - switch tag { - | SExpTag => Some(Refl) - | _ => None - } -// coercion represents a coercion from some type 'a to t, -// along with a function that effectively checks whether its argument is -// an instance of the coerced type. see usage in MakeCoercible.liftHValue -type rec coercion<_> = - Coercion({tagEq: 'c. atomTag<'c> => option>, coerce: 'a => option<'b>}): coercion<'b> -module MakeCoercible = ( - Atom: ATOM, - Coercions: { - let coercions: array> - }, -): (COERCIBLE_ATOM with type t = Atom.t) => { - include Atom - let liftHValue = (HValue(tag, val)) => - Array.findMap(Coercions.coercions, (Coercion(c)) => - switch c.tagEq(tag) { - | Some(Refl) => c.coerce(val) - | None => None - } - ) - let getHValue = t => HValue(Atom.Tag, t) -} - -exception MatchCombineAtomBoth exception MatchCombineAtomForeign module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): { @@ -75,19 +44,15 @@ type subst = Map.t type gen = ref type atomTag<_> += Tag: atomTag - let tagEq = (type a, tag: atomTag): option> => - switch tag { - | Tag => Some(Refl) - | _ => None - } - let liftHValue = v => Some(Foreign(v)) + let coerce = v => Some(Foreign(v)) let match = (t, leftBranch: Left.t => 'a, rightBranch: Right.t => 'a): 'a => switch t { | Left(s) => leftBranch(s) | Right(s) => rightBranch(s) | Foreign(_) => throw(MatchCombineAtomForeign) } - let getHValue = t => t->match(Left.getHValue, Right.getHValue) + let wrapLeft = left => HValue(Left.Tag, left) + let wrapRight = right => HValue(Right.Tag, right) let parse = (s, ~scope, ~gen: option=?) => { Left.parse(s, ~scope, ~gen?) ->Result.map(((r, rest)) => (Left(r), rest)) @@ -108,14 +73,14 @@ let coerceToLeft = (t): option => switch t { | Left(s) => Some(s) - | Right(s) => s->Right.getHValue->Left.liftHValue - | Foreign(v) => Left.liftHValue(v) + | Right(s) => s->wrapRight->Left.coerce + | Foreign(v) => Left.coerce(v) } let coerceToRight = (t): option => switch t { | Right(s) => Some(s) - | Left(s) => s->Left.getHValue->Right.liftHValue - | Foreign(v) => Right.liftHValue(v) + | Left(s) => s->wrapLeft->Right.coerce + | Foreign(v) => Right.coerce(v) } let substitute = (s, subst: subst) => { s->match( diff --git a/src/Coercible.res b/src/Coercible.res --- a/src/Coercible.res +++ b/src/Coercible.res @@ -1,28 +1,22 @@ open AtomDef -module StringA = MakeCoercible( - StringA.Atom, - { - let coercions = [ - Coercion({ - tagEq: Symbolic.Atom.tagEq, - coerce: s => Some([StringA.String(s)]), - }), - Coercion({ - tagEq: tagEqSExp, - coerce: t => - switch t { - | Var({idx}) => Some([StringA.Var({idx: idx})]) - | Schematic({schematic, allowed}) => Some([StringA.Schematic({schematic, allowed})]) - }, - }), - ] - }, -) +module StringA: COERCIBLE_ATOM with type t = StringA.t = { + include StringA.Atom + let coerce = (HValue(tag, a)) => + switch tag { + | Symbolic.Atom.Tag => Some([StringA.String(a)]) + | AtomDef.SExpTag => + Some([ + switch a { + | Var({idx}) => StringA.Var({idx: idx}) + | Schematic({schematic, allowed}) => StringA.Schematic({schematic, allowed}) + }, + ]) + | _ => None + } +} -module Symbolic = MakeCoercible( - Symbolic.Atom, - { - let coercions = [] - }, -) +module Symbolic: COERCIBLE_ATOM with type t = Symbolic.Atom.t = { + include Symbolic.Atom + let coerce = _ => None +} diff --git a/src/SExp.res b/src/SExp.res --- a/src/SExp.res +++ b/src/SExp.res @@ -150,9 +150,9 @@ let rec lower = (term: t): option => switch term { | Atom(s) => Some(s) - | Var({idx}) => Atom.liftHValue(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx}))) + | Var({idx}) => Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Var({idx: idx}))) | Schematic({schematic, allowed}) => - Atom.liftHValue(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed}))) + Atom.coerce(HValue(AtomDef.SExpTag, AtomDef.Schematic({schematic, allowed}))) | Compound({subexps: [e1]}) => lower(e1) | _ => None } diff --git a/src/StringA.res b/src/StringA.res --- a/src/StringA.res +++ b/src/StringA.res @@ -15,11 +15,6 @@ type t = t type subst = Map.t type AtomDef.atomTag<_> += Tag: AtomDef.atomTag - let tagEq = (type a, tag: AtomDef.atomTag): option> => - switch tag { - | Tag => Some(Refl) - | _ => None - } let substitute = (term: t, subst: subst) => Array.flatMap(term, piece => { switch piece { diff --git a/src/Symbolic.res b/src/Symbolic.res --- a/src/Symbolic.res +++ b/src/Symbolic.res @@ -4,11 +4,6 @@ type t = string type subst = Map.t type atomTag<_> += Tag: atomTag - let tagEq = (type a, tag: atomTag): option> => - switch tag { - | Tag => Some(Refl) - | _ => None - } let unify = (a, b, ~gen as _=?) => if a == b { Seq.once(Map.make()) -- tangled.sh