diff --git a/src/AtomDef.res b/src/AtomDef.res index c41cd07..3c74ed4 100644 --- a/src/AtomDef.res +++ b/src/AtomDef.res @@ -1,8 +1,6 @@ // type level stuff to enable well-typed coercions type typeTag<_> = .. type rec eq<_, _> = Refl: eq<'a, 'a> -// coercion represents a coercion from some type 'a to t -type rec coercion<_> = Coercion(typeTag<'a>, 'a => option<'b>): coercion<'b> module type ATOM = { type t @@ -21,6 +19,8 @@ module type ATOM = { let concrete: t => bool } +// coercion represents a coercion from some type 'a to t +type rec coercion<_> = Coercion(typeTag<'a>, 'a => option<'b>): coercion<'b> module type COERCIBLE_ATOM = { include ATOM let coercions: array> @@ -36,7 +36,9 @@ module MakeCoercible = ( let coercions = Coercions.coercions } -exception RawVarOrSchematic +exception MatchCombineAtomVar +exception MatchCombineAtomSchematic + module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): { type base = | Left(Left.t) @@ -80,7 +82,8 @@ module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): { switch t { | Left(s) => leftBranch(s) | Right(s) => rightBranch(s) - | _ => throw(RawVarOrSchematic) + | Var(_) => throw(MatchCombineAtomVar) + | Schematic(_) => throw(MatchCombineAtomSchematic) } let parse = (s, ~scope, ~gen: option=?) => { Left.parse(s, ~scope, ~gen?) @@ -166,3 +169,36 @@ module CombineAtom = (Left: COERCIBLE_ATOM, Right: COERCIBLE_ATOM): { ) let concrete = s => s->match(Left.concrete, Right.concrete) } + +module type ATOM_VIEW = { + module Atom: ATOM + type props = {name: Atom.t, scope: array} + let make: props => React.element +} + +module MakeAtomView = ( + Left: COERCIBLE_ATOM, + LeftView: ATOM_VIEW with module Atom := Left, + Right: COERCIBLE_ATOM, + RightView: ATOM_VIEW with module Atom := Right, + Combined: module type of CombineAtom(Left, Right), +): { + include ATOM_VIEW with module Atom := Combined +} => { + type props = {name: Combined.t, scope: array} + let make = ({name, scope}: props) => + name->Combined.match( + left => , + right => , + ) +} + +module MakeAtomAndView = ( + Left: COERCIBLE_ATOM, + LeftView: ATOM_VIEW with module Atom := Left, + Right: COERCIBLE_ATOM, + RightView: ATOM_VIEW with module Atom := Right, +) => { + module Atom = CombineAtom(Left, Right) + module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom) +} diff --git a/src/CombinedAtom.res b/src/CombinedAtom.res deleted file mode 100644 index 2e7a6da..0000000 --- a/src/CombinedAtom.res +++ /dev/null @@ -1,42 +0,0 @@ -module type ATOM = SExpFunc.ATOM -exception RawVarOrSchematic - -module MakeAtom = (Left: AtomDef.COERCIBLE_ATOM, Right: AtomDef.COERCIBLE_ATOM): { - type base = - | Left(Left.t) - | Right(Right.t) - // neither of the below should appear organically. they're purely so we can lower - // substitutions to both Left.t and Right.t - | Var({idx: int}) - | Schematic({schematic: int, allowed: array}) - include ATOM with type t = base - let match: (t, Left.t => 'a, Right.t => 'a) => 'a -} => AtomDef.CombineAtom(Left, Right) - -module type ATOM_VIEW = SExpViewFunc.ATOM_VIEW -module MakeAtomView = ( - Left: AtomDef.COERCIBLE_ATOM, - LeftView: ATOM_VIEW with module Atom := Left, - Right: AtomDef.COERCIBLE_ATOM, - RightView: ATOM_VIEW with module Atom := Right, - Combined: module type of MakeAtom(Left, Right), -): { - include ATOM_VIEW with module Atom := Combined -} => { - type props = {name: Combined.t, scope: array} - let make = ({name, scope}: props) => - name->Combined.match( - left => , - right => , - ) -} - -module MakeAtomAndView = ( - Left: AtomDef.COERCIBLE_ATOM, - LeftView: ATOM_VIEW with module Atom := Left, - Right: AtomDef.COERCIBLE_ATOM, - RightView: ATOM_VIEW with module Atom := Right, -) => { - module Atom = MakeAtom(Left, Right) - module AtomView = MakeAtomView(Left, LeftView, Right, RightView, Atom) -} diff --git a/src/SExpFunc.res b/src/SExp.res similarity index 100% rename from src/SExpFunc.res rename to src/SExp.res diff --git a/src/SExpViewFunc.res b/src/SExpView.res similarity index 90% rename from src/SExpViewFunc.res rename to src/SExpView.res index 77c29b0..32d38fc 100644 --- a/src/SExpViewFunc.res +++ b/src/SExpView.res @@ -1,13 +1,9 @@ -module type ATOM_VIEW = { - module Atom: SExpFunc.ATOM - type props = {name: Atom.t, scope: array} - let make: props => React.element -} +module type ATOM_VIEW = AtomDef.ATOM_VIEW module Make = ( - Atom: SExpFunc.ATOM, + Atom: AtomDef.ATOM, AtomView: ATOM_VIEW with module Atom := Atom, - SExp: module type of SExpFunc.Make(Atom), + SExp: module type of SExp.Make(Atom), ): { include Signatures.TERM_VIEW with module Term := SExp } => { diff --git a/src/Scratch.res b/src/Scratch.res index 94ea949..c3f1a3a 100644 --- a/src/Scratch.res +++ b/src/Scratch.res @@ -42,14 +42,14 @@ module DLREView = MethodView.CombineMethodView( module TheoremS = Editable.TextArea(Theorem.Make(HOTerm, HOTerm, HOTermJView, DLRView)) module ConfS = ConfigBlock.Make(HOTerm, HOTerm) -module StringSymbol = CombinedAtom.MakeAtomAndView( +module StringSymbol = AtomDef.MakeAtomAndView( Coercible.StringA, StringA.AtomView, Coercible.Symbolic, Symbolic.AtomView, ) -module StringSExp = SExpFunc.Make(StringSymbol.Atom) -module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) +module StringSExp = SExp.Make(StringSymbol.Atom) +module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) module StringSExpJView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) module AxiomStr = Editable.TextArea(StringAxiomSet) diff --git a/src/StringA.res b/src/StringA.res index 23c7128..72cf47d 100644 --- a/src/StringA.res +++ b/src/StringA.res @@ -291,7 +291,7 @@ module Atom = { | Some(v) => v | None => throw( - SExpFunc.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`), + SExp.SubstNotCompatible(`index ${Int.toString(var - from)} not of sort string`), ) } } else { diff --git a/src/StringA.resi b/src/StringA.resi index a6492c6..48e60c7 100644 --- a/src/StringA.resi +++ b/src/StringA.resi @@ -5,4 +5,4 @@ type rec piece = type t = array module Atom: AtomDef.ATOM with type t = t -module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom +module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom diff --git a/src/StringAxiomSet.res b/src/StringAxiomSet.res index f455d97..f3b6391 100644 --- a/src/StringAxiomSet.res +++ b/src/StringAxiomSet.res @@ -1,13 +1,13 @@ open Component -module StringSymbol = CombinedAtom.MakeAtomAndView( +module StringSymbol = AtomDef.MakeAtomAndView( Coercible.StringA, StringA.AtomView, Coercible.Symbolic, Symbolic.AtomView, ) -module StringSExp = SExpFunc.Make(StringSymbol.Atom) -module TermView = SExpViewFunc.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) +module StringSExp = SExp.Make(StringSymbol.Atom) +module TermView = SExpView.Make(StringSymbol.Atom, StringSymbol.AtomView, StringSExp) module JudgmentView = TermViewAsJudgmentView.Make(StringSExp, StringSExp, TermView) module Rule = Rule.Make(StringSExp, StringSExp) diff --git a/src/Symbolic.resi b/src/Symbolic.resi index 1a2ca55..a6a1779 100644 --- a/src/Symbolic.resi +++ b/src/Symbolic.resi @@ -1,3 +1,3 @@ type t = string module Atom: AtomDef.ATOM with type t = t -module AtomView: SExpViewFunc.ATOM_VIEW with module Atom := Atom +module AtomView: AtomDef.ATOM_VIEW with module Atom := Atom diff --git a/src/Theorem.res b/src/Theorem.res index 12d3074..af200a1 100644 --- a/src/Theorem.res +++ b/src/Theorem.res @@ -63,7 +63,7 @@ module Make = ( Proof.check(ctx, proof, props.content.rule)->ignore {...props.content, proof, substFailed: None} } catch { - | SExpFunc.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)} + | SExp.SubstNotCompatible(s) => {...props.content, substFailed: Some(s)} }, ~exports={ Ports.facts: Dict.fromArray([(props.content.name, props.content.rule)]), diff --git a/tests/SExpTest.res b/tests/SExpTest.res index 740d636..733283f 100644 --- a/tests/SExpTest.res +++ b/tests/SExpTest.res @@ -1,6 +1,6 @@ open Zora -module SExp = SExpFunc.Make(Symbolic.Atom) +module SExp = SExp.Make(Symbolic.Atom) open SExp module Util = TestUtil.MakeTerm(SExp) diff --git a/tests/TestUtil.res b/tests/TestUtil.res index 3e4f3e5..93e5cab 100644 --- a/tests/TestUtil.res +++ b/tests/TestUtil.res @@ -124,7 +124,7 @@ module MakeUnifyTester = (Subj: CAN_UNIFY) => { } } -module MakeAtomTester = (Atom: SExpFunc.ATOM) => { +module MakeAtomTester = (Atom: SExp.ATOM) => { module ParseWrapper: CAN_PARSE with type t = Atom.t and type meta = string