+15

index.html

reviewed

··· 418 418 419 419 |- ? 420 420 </hol-proof> 421 421 + <hol-proof id="index.html/constructor-neq-test" deps="index.html/myconfig index.html/baz index.html/nat"> 422 422 + x. y. 423 423 + -------------------- neq-constructors 424 424 + (not (= (@Z x) (@S y))) 425 425 + 426 426 + x. y. |- ? 427 427 + </hol-proof> 428 428 + <hol-proof id="index.html/constructor-inj-test" deps="index.html/myconfig index.html/baz index.html/nat"> 429 429 + x. y. 430 430 + (= (@S x) (@S y)) 431 431 + -------------- S-inj 432 432 + (= x y) 433 433 + 434 434 + x. y. eq |- ? 435 435 + </hol-proof> 421 436 <hol-proof id="index.html/fcu-test" deps="index.html/myconfig"> 422 437 x. 423 438 [P. (P (fst x))]

+1 -1

package.json

reviewed

··· 10 10 "preview": "vite preview", 11 11 "res:build": "rescript", 12 12 "res:clean": "rescript clean", 13 13 - "res:dev": "rescript -w", 13 13 + "res:dev": "rescript watch", 14 14 "res:format": "rescript format", 15 15 "test": "npm run res:build && pta 'tests/*.mjs'", 16 16 "test-watch": "onchange --initial '{tests,src}/*.mjs' -- pta 'tests/*.mjs'",

+209

src/Method.res

reviewed

··· 763 763 let reversed = true 764 764 }, 765 765 ) 766 766 + 767 767 + module ConstructorNeq = ( 768 768 + Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 769 769 + ) => { 770 770 + module Term = HOTerm 771 771 + module Rule = Rule.Make(HOTerm, Judgment) 772 772 + module Context = Context(HOTerm, Judgment) 773 773 + 774 774 + type t<'a> = unit 775 775 + 776 776 + type constructorHead = {name: string, args: array<HOTerm.t>} 777 777 + 778 778 + let constructorHead = (term: HOTerm.t): option<constructorHead> => { 779 779 + let (head, args) = HOTerm.strip(term) 780 780 + switch head { 781 781 + | HOTerm.Symbol({name, constructor: true}) => Some({name, args}) 782 782 + | _ => None 783 783 + } 784 784 + } 785 785 + 786 786 + type constructorComparison = {lhs: constructorHead, rhs: constructorHead, negated: bool} 787 787 + 788 788 + let extractConstructorEqualityFrom = (term: HOTerm.t): option<( 789 789 + constructorHead, 790 790 + constructorHead, 791 791 + )> => { 792 792 + let (head, args) = HOTerm.strip(term) 793 793 + switch head { 794 794 + | HOTerm.Symbol({name: "="}) if Array.length(args) == 2 => 795 795 + switch ( 796 796 + constructorHead(args->Array.getUnsafe(0)), 797 797 + constructorHead(args->Array.getUnsafe(1)), 798 798 + ) { 799 799 + | (Some(lhs), Some(rhs)) => Some((lhs, rhs)) 800 800 + | _ => None 801 801 + } 802 802 + | _ => None 803 803 + } 804 804 + } 805 805 + 806 806 + let extractConstructorEquality = (judgment: Judgment.t): option<constructorComparison> => { 807 807 + let reduced = judgment->Judgment.reduce 808 808 + switch extractConstructorEqualityFrom(reduced) { 809 809 + | Some((lhs, rhs)) => Some({lhs, rhs, negated: false}) 810 810 + | None => 811 811 + switch HOTerm.strip(reduced) { 812 812 + | (HOTerm.Symbol({name: "not"}), [inner]) => 813 813 + extractConstructorEqualityFrom(inner)->Option.map(((lhs, rhs)) => {lhs, rhs, negated: true}) 814 814 + | _ => None 815 815 + } 816 816 + } 817 817 + } 818 818 + 819 819 + let keywords = ["constructor_neq"] 820 820 + 821 821 + let map = (it: t<'a>, _f: 'a => 'b): t<'b> => it 822 822 + 823 823 + let substitute = (it: t<'a>, _subst: Judgment.subst) => it 824 824 + 825 825 + let prettyPrint = (_it: t<'a>, ~scope as _, ~indentation=0, ~subprinter as _) => 826 826 + String.repeat(" ", indentation)->String.concat("constructor_neq") 827 827 + 828 828 + let parse = (input, ~keyword as _, ~scope as _, ~gen as _, ~subparser as _) => Ok(( 829 829 + (), 830 830 + String.trim(input), 831 831 + )) 832 832 + 833 833 + let apply = (_ctx: Context.t, j: Judgment.t, _gen: HOTerm.gen, _f: Rule.t => 'a) => { 834 834 + let ret = Dict.make() 835 835 + switch extractConstructorEquality(j) { 836 836 + | Some({lhs: {name: lhs}, rhs: {name: rhs}}) if lhs != rhs => 837 837 + ret->Dict.set(`constructor_neq ${lhs} ${rhs}`, ((), HOTerm.makeSubst())) 838 838 + | _ => () 839 839 + } 840 840 + ret 841 841 + } 842 842 + 843 843 + let check = (_it: t<'a>, _ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => 844 844 + switch extractConstructorEquality(goal) { 845 845 + | Some({lhs: {name: lhs}, rhs: {name: rhs}}) => 846 846 + if lhs == rhs { 847 847 + Error("constructor_neq expects different constructor symbols") 848 848 + } else { 849 849 + Ok() 850 850 + } 851 851 + | None => Error("constructor_neq applies only to equalities between constructors") 852 852 + } 853 853 + } 854 854 + 855 855 + module ConstructorInj = ( 856 856 + Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 857 857 + ) => { 858 858 + module Rule = Rule.Make(HOTerm, Judgment) 859 859 + module Context = Context(HOTerm, Judgment) 860 860 + 861 861 + // we need to define this to workaround a type error for map 862 862 + type inner = { 863 863 + source: string, 864 864 + argIndex: int, 865 865 + } 866 866 + type t<'a> = inner 867 867 + 868 868 + let keywords = ["constructor_inj"] 869 869 + 870 870 + let map = (it: t<'a>, _f: 'a => 'b): t<'b> => it 871 871 + 872 872 + let substitute = (it: t<'a>, _subst: Judgment.subst) => it 873 873 + 874 874 + let prettyPrint = (it: t<'a>, ~scope as _, ~indentation=0, ~subprinter as _) => 875 875 + String.repeat(" ", indentation)->String.concat( 876 876 + `constructor_inj ${it.source} ${Int.toString(it.argIndex)}`, 877 877 + ) 878 878 + 879 879 + let parseIntPrefix = (input: string): option<(int, string)> => { 880 880 + let cur = input->String.trimStart 881 881 + let re = RegExp.fromStringWithFlags("^(-?[0-9]+)", ~flags="y") 882 882 + switch re->RegExp.exec(cur) { 883 883 + | None => None 884 884 + | Some(res) => 885 885 + switch RegExp.Result.matches(res) { 886 886 + | [n] => 887 887 + Some(( 888 888 + n->Int.fromString->Option.getExn, 889 889 + cur->String.sliceToEnd(~start=RegExp.lastIndex(re)), 890 890 + )) 891 891 + | _ => None 892 892 + } 893 893 + } 894 894 + } 895 895 + 896 896 + let parse = (input, ~keyword as _, ~scope as _, ~gen as _, ~subparser as _) => { 897 897 + let cur = String.trim(input) 898 898 + switch Rule.parseRuleName(cur) { 899 899 + | Error(e) => Error(e) 900 900 + | Ok((source, rest)) => 901 901 + let rest = String.trim(rest) 902 902 + switch parseIntPrefix(rest) { 903 903 + | Some((argIndex, remainder)) => Ok(({source, argIndex}, remainder->String.trim)) 904 904 + | None => Ok(({source, argIndex: 0}, rest)) 905 905 + } 906 906 + } 907 907 + } 908 908 + 909 909 + let extractConstructorEquality = (term: HOTerm.t): option<( 910 910 + string, 911 911 + array<HOTerm.t>, 912 912 + array<HOTerm.t>, 913 913 + )> => { 914 914 + let (_head, args) = term->HOTerm.strip 915 915 + if Array.length(args) != 2 { 916 916 + None 917 917 + } else { 918 918 + let (lHead, lArgs) = args->Array.getUnsafe(0)->HOTerm.strip 919 919 + let (rHead, rArgs) = args->Array.getUnsafe(1)->HOTerm.strip 920 920 + switch (lHead, rHead) { 921 921 + | (HOTerm.Symbol({name: ln, constructor: true}), HOTerm.Symbol({name: rn, constructor: true})) 922 922 + if ln == rn && lArgs->Array.length == rArgs->Array.length => 923 923 + Some((ln, lArgs, rArgs)) 924 924 + | _ => None 925 925 + } 926 926 + } 927 927 + } 928 928 + 929 929 + let apply = (ctx: Context.t, j: Judgment.t, _gen: HOTerm.gen, _f: Rule.t => 'a) => { 930 930 + let ret = Dict.make() 931 931 + switch j->Judgment.reduce->HOTerm.strip { 932 932 + | (HOTerm.Symbol({name: "="}), [lhs, rhs]) => 933 933 + ctx.facts->Dict.forEachWithKey((fact, name) => { 934 934 + switch extractConstructorEquality(fact.conclusion) { 935 935 + | Some((_cName, lArgs, rArgs)) => 936 936 + Belt.Array.zip(lArgs, rArgs)->Array.forEachWithIndex(((la, ra), idx) => 937 937 + if HOTerm.equivalent(la, lhs) && HOTerm.equivalent(ra, rhs) { 938 938 + ret->Dict.set( 939 939 + `constructor_inj ${name} ${Int.toString(idx)}`, 940 940 + ({source: name, argIndex: idx}, HOTerm.makeSubst()), 941 941 + ) 942 942 + } 943 943 + ) 944 944 + | None => () 945 945 + } 946 946 + }) 947 947 + | _ => () 948 948 + } 949 949 + ret 950 950 + } 951 951 + 952 952 + let check = (it: t<'a>, ctx: Context.t, goal: Judgment.t, _f: ('a, Rule.t) => 'b) => { 953 953 + switch (ctx.facts->Dict.get(it.source), goal->Judgment.reduce->HOTerm.strip) { 954 954 + | (None, _) => Error(`Cannot find equality '${it.source}'`) 955 955 + | (Some(fact), (HOTerm.Symbol({name: "="}), [lhs, rhs])) => 956 956 + switch extractConstructorEquality(fact.conclusion) { 957 957 + | None => Error(`'${it.source}' is not a constructor equality`) 958 958 + | Some((_cName, lArgs, rArgs)) => 959 959 + if it.argIndex < 0 || it.argIndex >= Array.length(lArgs) { 960 960 + Error("constructor_inj index out of range") 961 961 + } else { 962 962 + let la = lArgs->Array.getUnsafe(it.argIndex) 963 963 + let ra = rArgs->Array.getUnsafe(it.argIndex) 964 964 + if HOTerm.equivalent(la, lhs) && HOTerm.equivalent(ra, rhs) { 965 965 + Ok({source: it.source, argIndex: it.argIndex}) 966 966 + } else { 967 967 + Error("constructor_inj target does not match goal") 968 968 + } 969 969 + } 970 970 + } 971 971 + | (_, _) => Error("constructor_inj applies to equality goals") 972 972 + } 973 973 + } 974 974 + }

+56

src/MethodView.res

reviewed

··· 245 245 } 246 246 } 247 247 248 248 + module ConstructorNeqView = ( 249 249 + Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 250 250 + ) => { 251 251 + module Method = Method.ConstructorNeq(Judgment) 252 252 + type props<'a> = { 253 253 + method: Method.t<'a>, 254 254 + scope: array<HOTerm.meta>, 255 255 + ruleStyle: RuleView.style, 256 256 + gen: HOTerm.gen, 257 257 + onChange: (Method.t<'a>, Judgment.subst) => unit, 258 258 + } 259 259 + type srProps<'a> = { 260 260 + "proof": 'a, 261 261 + "scope": array<HOTerm.meta>, 262 262 + "ruleStyle": RuleView.style, 263 263 + "gen": HOTerm.gen, 264 264 + "onChange": ('a, Judgment.subst) => unit, 265 265 + } 266 266 + let make = (_subRender: srProps<'a> => React.element) => 267 267 + _props => { 268 268 + <div> 269 269 + <b> {React.string("constructor_neq")} </b> 270 270 + </div> 271 271 + } 272 272 + } 273 273 + 274 274 + module ConstructorInjView = ( 275 275 + Judgment: JUDGMENT with module Term := HOTerm and type subst = HOTerm.subst and type t = HOTerm.t, 276 276 + ) => { 277 277 + module Method = Method.ConstructorInj(Judgment) 278 278 + type props<'a> = { 279 279 + method: Method.t<'a>, 280 280 + scope: array<HOTerm.meta>, 281 281 + ruleStyle: RuleView.style, 282 282 + gen: HOTerm.gen, 283 283 + onChange: (Method.t<'a>, Judgment.subst) => unit, 284 284 + } 285 285 + type srProps<'a> = { 286 286 + "proof": 'a, 287 287 + "scope": array<HOTerm.meta>, 288 288 + "ruleStyle": RuleView.style, 289 289 + "gen": HOTerm.gen, 290 290 + "onChange": ('a, Judgment.subst) => unit, 291 291 + } 292 292 + let make = (_subRender: srProps<'a> => React.element) => 293 293 + props => { 294 294 + <div> 295 295 + <b> 296 296 + {React.string( 297 297 + `constructor_inj ${props.method.source} ${Int.toString(props.method.argIndex)}`, 298 298 + )} 299 299 + </b> 300 300 + </div> 301 301 + } 302 302 + } 303 303 + 248 304 module CombineMethodView = ( 249 305 Term: TERM, 250 306 Judgment: JUDGMENT with module Term := Term,

+13 -1

src/Scratch.res

reviewed

··· 3 3 module AxiomS = Editable.TextArea(AxiomSet.Make(HOTerm, HOTermJ, HOTermJView)) 4 4 module InductiveS = Editable.TextArea(InductiveSet.Make(HOTerm, HOTermJ, HOTermJView)) 5 5 6 6 - module RewritesView = MethodView.CombineMethodView( 6 6 + module EqualityViews = MethodView.CombineMethodView( 7 7 HOTerm, 8 8 HOTermJ, 9 9 MethodView.RewriteView(HOTermJ), 10 10 MethodView.RewriteReverseView(HOTermJ), 11 11 + ) 12 12 + module ConstructorEqualityViews = MethodView.CombineMethodView( 13 13 + HOTerm, 14 14 + HOTermJ, 15 15 + EqualityViews, 16 16 + MethodView.ConstructorNeqView(HOTermJ), 17 17 + ) 18 18 + module RewritesView = MethodView.CombineMethodView( 19 19 + HOTerm, 20 20 + HOTermJ, 21 21 + ConstructorEqualityViews, 22 22 + MethodView.ConstructorInjView(HOTermJ), 11 23 ) 12 24 module DerivationsOrLemmasView = MethodView.CombineMethodView( 13 25 HOTerm,