diff --git a/index.html b/index.html
index 58ce0cb..c326915 100644
--- a/index.html
+++ b/index.html
@@ -452,156 +452,145 @@
Basic
---- M-Empty
- "" M
+ ("" M)
s.
- "$s" M
+ ("$s" M)
------- M-Surround
- "($s)" M
+ ("($s)" M)
s1. s2.
- "$s1" M "$s2" M
+ ("$s1" M) ("$s2" M)
------- M-Juxtapose
- "$s1 $s2" M
+ ("$s1 $s2" M)
- -------- paren
- "()(())" M
- |- by (Concat "()" "(())") {
- |- by (Surround "") {
- |- by (Empty) {}
- }
- |- by (Surround "()") {
- |- by (Surround "") {
- |- by (Empty) {}
- }
- }
- }
-
-
- ------- T-Atom
- "T" Atom
- ------- F-Atom
- "F" Atom
-
- e.
- "$e" Atom
- --------- Atom-AE
- "$e" AE
-
- e1.e2.
- "$e1" Atom "$e2" AE
- -------------------- And
- "$e1 /\\ $e2" AE
-
- e.
- "$e" AE
- --------- AE-B
- "$e" B
-
- e1.e2.
- "$e1" AE "$e2" B
- ----------------- Or
- "$e1 \\/ $e2" B
+ ---- paren
+ ("( ) ( ( ) )" M)
- e.
- "$e" B
- ----------- Paren
- "($e)" Atom
-
-
- ------------- bool
- "T/\\(T\\/F)" AE
- |- by (And "T" "(T\\/F)") {
- |- by (T-Atom) {}
- |- by (Atom-AE "(T\\/F)") {
- |- by (Paren "T\\/F") {
- |- by (Or "T" "F") {
- |- by (Atom-AE "T") {
- |- by (T-Atom) {}
- }
- |- by (AE-B "F") {
- |- by (Atom-AE "F") {
- |- by (F-Atom) {}
- }
- }
- }
- }
- }
- }
+ |- by (M-Juxtapose "( )" "( ( ) )") {
+ |- by (M-Surround "") {
+ |- by (M-Empty) {}}
+ |- by (M-Surround "( )") {
+ |- by (M-Surround "") {
+ |- by (M-Empty) {}}}}
- With first-order term judgments
-
- ---- MParse-Empty
- "" (MP emp)
-
- s1. p1.
- "$s1" (MP p1)
- ------------- MParse-Surround
- "($s1)" (MP (p1))
-
- s1. s2. p1. p2.
- "$s1" p1
- "$s1" p2
- ------------------- MParse-Juxtapose
- "$s1 $s2" (MP (p1 p2))
-
-
- ---- Expr-e
- "e" (Expr e)
-
- s1.
- s2. e2.
- "$s2" (Expr e2)
- ------------- Stmt-Let
- "let $s1 = $s2" (Let (ID "$s1") e2)
-
-
- s. p.
- "$s" M "" p [s1. "$s1" p |- "($s1)" p] [s1. s2. "$s1" p "$s2" p |- "$s1 $s2" p]
- ---------------------------------- M-Induct
- "$s" p
-
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
- s. "$s" L
+ s. ("$s" L)
-----N-Surr
- "($s)" N
+ ("($s)" N)
-----L-Empty
- "" L
+ ("" L)
s1. s2.
- "$s1" N "$s2" L
+ ("$s1" N) ("$s2" L)
-----L-Juxtapose
- "$s1 $s2" L
+ ("$s1 $s2" L)
-
-
- s. "$s" N
+
+ s. ("$s" N)
--------N-L
- "$s" L
+ ("$s" L)
s. sn |- by (L-Juxtapose s "") {
|- by (sn) {}
|- by (L-Empty) {}
}
-
- s1.s2. "$s1" L "$s2" L
+
+ s1.s2. ("$s1" L) ("$s2" L)
--------------------- lexp-juxt
- "$s1 $s2" L
+ ("$s1 $s2" L)
s1. s2. s1L s2L |- ?
-
- s. "$s" M
+
+ s. ("$s" M)
----------- mexp-lexp
- "$s" L
+ ("$s" L)
s. sM |- ?
-
- s. "$s" L
+
+ s. ("$s" L)
----------- mexp-lexp
- "$s" M
- s. sL |- elim (L_mutualInduct sL "" "$s" "" "M" "M") {
+ ("$s" M)
+ s. sL |- elim (L_mutualInduct sL "" "$s" "" M M) {
|- by (M-Empty) {}
s1.s2. 0 1 2 3 |- elim (M-Juxtapose 2 "$s1" "$s2") {
|- by (3) {}}
diff --git a/src/SExp.res b/src/SExp.res
index 204e828..f714d71 100644
--- a/src/SExp.res
+++ b/src/SExp.res
@@ -8,8 +8,17 @@ module ConstSymbol: SExpFunc.SYMBOL with type t = string = {
Seq.empty
}
let prettyPrint = (name, ~scope as _: array) => name
- let parse = (string, ~scope as _: array, ~gen as _=?) => Ok((string, ""))
+ let symbolRegex = /^([^\s()\[\]]+)/
+ let parse = (string, ~scope as _: array, ~gen as _=?) =>
+ switch Util.execRe(symbolRegex, string) {
+ | Some(([res], l)) => Ok((res, string->String.substringToEnd(~start=l)))
+ | _ => Error("constant symbol parse error")
+ }
let substitute = (name, _) => name
+ let lowerVar = _ => ""
+ let lowerSchematic = (_, _) => ""
+ let ghost = ""
+ let substDeBruijn = (name, _, ~from as _) => name
let constSymbol = name => Some(name)
}
diff --git a/src/SExpFunc.res b/src/SExpFunc.res
index d04e8e1..904e1e0 100644
--- a/src/SExpFunc.res
+++ b/src/SExpFunc.res
@@ -5,6 +5,11 @@ module type SYMBOL = {
let prettyPrint: (t, ~scope: array) => string
let parse: (string, ~scope: array, ~gen: ref=?) => result<(t, string), string>
let substitute: (t, subst) => t
+ // used for when trying to substitute a variable of the wrong type
+ let lowerVar: int => t
+ let lowerSchematic: (int, array) => t
+ let ghost: t
+ let substDeBruijn: (t, array, ~from: int) => t
// used for grouping judgments together for rule induction
let constSymbol: t => option
}
@@ -147,9 +152,21 @@ module Make = (Symbol: SYMBOL): {
}
let unify = (a: t, b: t, ~gen as _=?) => unifyTerm(a, b)
+ let rec lower = (term: t): Symbol.t =>
+ switch term {
+ | Symbol(s) => s
+ | Var({idx}) => Symbol.lowerVar(idx)
+ | Schematic({schematic, allowed}) => Symbol.lowerSchematic(schematic, allowed)
+ | Compound({subexps: [e1]}) => lower(e1)
+ | _ => Symbol.ghost
+ }
let rec substDeBruijn = (term: t, substs: array, ~from: int=0) =>
switch term {
- | Symbol(_) => term
+ | Symbol(s) => {
+ let symbolSubsts = substs->Array.map(lower)
+ Symbol(Symbol.substDeBruijn(s, symbolSubsts, ~from))
+ }
+
| Compound({subexps}) =>
Compound({subexps: Array.map(subexps, x => substDeBruijn(x, substs, ~from))})
| Var({idx: var}) =>
@@ -295,26 +312,31 @@ module Make = (Symbol: SYMBOL): {
| Some(res) =>
switch RegExp.Result.matches(res) {
| [symb] => {
- cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
- let parseSymb = () => {
+ let specialSymb = tok => {
+ cur := String.sliceToEnd(str, ~start=RegExp.lastIndex(symbolRegexp))
+ Some(tok)
+ }
+ let regularSymb = () => {
// FIX: not ideal to throw away symbol error message
- Symbol.parse(symb, ~scope)
+ Console.log(("current", cur.contents))
+ Symbol.parse(cur.contents, ~scope)
->Util.Result.ok
->Option.map(((s, rest)) => {
- cur := rest->String.concat(cur.contents)
+ cur := rest
+ Console.log(("parsed", s, cur.contents))
SymbolT(s)
})
}
switch checkVariable(symb) {
- | Some(idx) => Some(VarT(idx))
+ | Some(idx) => specialSymb(VarT(idx))
| None => {
let schematicRegexp = RegExp.fromString(schematicRegexpString)
switch schematicRegexp->RegExp.exec(symb) {
- | None => parseSymb()
+ | None => regularSymb()
| Some(res') =>
switch RegExp.Result.matches(res') {
- | [s] => Some(SchematicT(s->Int.fromString->Option.getUnsafe))
- | _ => parseSymb()
+ | [s] => specialSymb(SchematicT(s->Int.fromString->Option.getUnsafe))
+ | _ => regularSymb()
}
}
}
diff --git a/src/StringTermJudgment.res b/src/StringTermJudgment.res
index f56e954..d3cc167 100644
--- a/src/StringTermJudgment.res
+++ b/src/StringTermJudgment.res
@@ -30,13 +30,29 @@ module StringSymbol: SExpFunc.SYMBOL with type t = stringSymbol = {
let stringSubs = subst->Util.mapMapValues(v =>
switch v {
| StringS(s) => s
- | _ => throw(Util.Unreachable("const should not have map values"))
+ | _ => [StringTerm.Ghost]
}
)
StringS(StringTerm.substitute(s, stringSubs))
}
| ConstS(s) => ConstS(s)
}
+ let lowerVar = idx => StringS([StringTerm.Var({idx: idx})])
+ let lowerSchematic = (schematic, allowed) => StringS([StringTerm.Schematic({schematic, allowed})])
+ let ghost = StringS([StringTerm.Ghost])
+ let substDeBruijn = (s, substs: array, ~from) =>
+ switch s {
+ | StringS(s) => {
+ let stringSubs = substs->Array.map(v =>
+ switch v {
+ | StringS(s) => s
+ | _ => [StringTerm.String("AYAYAYSLKDJFLSKDJ")]
+ }
+ )
+ StringS(StringTerm.substDeBruijn(s, stringSubs, ~from))
+ }
+ | ConstS(s) => ConstS(s)
+ }
let constSymbol = s =>
switch s {
| StringS(_) => None