diff --git a/src/haz3lweb/ExerciseSettings_base.re b/src/haz3lweb/ExerciseSettings_base.re index ec657a057..9cff586e9 100644 --- a/src/haz3lweb/ExerciseSettings_base.re +++ b/src/haz3lweb/ExerciseSettings_base.re @@ -4,6 +4,8 @@ let exercises: list(Exercise.spec) = [ Ex_DerivationEmpty.exercise, Ex_DerivationEmpty2.exercise, Ex_DerivationEmpty3.exercise, + Ex_Closed_Substitution.exercise, + Ex_Type_Validation_Derivation.exercise, Ex_PairMap_Derivation.exercise, Ex_Curried_Function_Derivation.exercise, Ex_Shadowing_And_Closures.exercise, diff --git a/src/haz3lweb/exercises/Ex_Closed_Substitution.ml b/src/haz3lweb/exercises/Ex_Closed_Substitution.ml new file mode 100644 index 000000000..b71d6354f --- /dev/null +++ b/src/haz3lweb/exercises/Ex_Closed_Substitution.ml @@ -0,0 +1,493 @@ +let prompt = Ex_Closed_Substitution_prompt.prompt + +let exercise : Exercise.spec = + { + header = + { + title = "Closed Substitution"; + version = 1; + module_name = "Ex_Closed_Substitution"; + prompt; + }; + pos = Proof Prelude; + model = + Proof + { + prelude = + { + selection = { focus = Left; content = []; mode = Normal }; + backpack = []; + relatives = + { + siblings = + ( [ + Grout + { + id = + Option.get + (Haz3lcore.Id.of_string + "31347ee2-fed9-4a06-b029-93c090413a99"); + shape = Convex; + }; + ], + [] ); + ancestors = []; + }; + caret = Outer; + }; + setup = + { + selection = { focus = Left; content = []; mode = Normal }; + backpack = []; + relatives = + { + siblings = + ( [], + [ + Grout + { + id = + Option.get + (Haz3lcore.Id.of_string + "81a3a47c-4cb6-4b7c-975a-99b18190003c"); + shape = Convex; + }; + ] ); + ancestors = []; + }; + caret = Outer; + }; + trees = + [ + Node + ( Just + { + jdmt = + { + selection = + { focus = Left; content = []; mode = Normal }; + backpack = []; + relatives = + { + siblings = + ( [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "a3c0826b-4dd0-44c6-8317-8d5b1902b198"); + label = [ "let"; "="; "in" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Pat; Drv Exp ]; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Concave 17; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1; 2 ]; + children = + [ + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "c21426f3-eaad-4f79-9956-920edebf65d4"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "d83412fc-077d-4b31-a518-be75985d3b5b"); + label = [ "incr" ]; + mold = + { + out = Drv Pat; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Pat; + }, + { + shape = Convex; + sort = Drv Pat; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "87da8e24-4b19-4e21-a084-f11fd26aafcc"); + content = Whitespace " "; + }; + ]; + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "deea7e89-07e9-4d10-8921-dd38d4d91f74"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "a84ae0ce-e862-47d5-9c97-1e6b9c2a88bf"); + label = [ "fun"; "->" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Pat ]; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Concave 14; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id + .of_string + "66b3203e-399c-4dd4-9c94-61c051bb6175"); + content = + Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id + .of_string + "bb7eb7c4-f502-4f86-b46f-9b0620ad5806"); + label = [ "x" ]; + mold = + { + out = Drv Pat; + in_ = []; + nibs = + ( { + shape = + Convex; + sort = + Drv Pat; + }, + { + shape = + Convex; + sort = + Drv Pat; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id + .of_string + "6f6b134b-a561-4edc-9409-c94139a8f69f"); + content = + Whitespace " "; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "e2772ef1-d7b5-4e1c-b7b6-34c87aa4e49e"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "f1bb7e80-f9af-4df2-ba97-a87dc1b26518"); + label = [ "x" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "cd88dcb1-198d-47d7-9644-aeec89991084"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "ae3465cc-7055-4bb0-9391-e59fbd7e5c35"); + label = [ "+" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Concave 6; + sort = Drv Exp; + }, + { + shape = Concave 6; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "604b0f90-8de2-4346-a139-268d1a91d65d"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "3b912307-16ec-402a-b228-fda3d18a0bd1"); + label = [ "1" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "fa84e024-3f6a-400f-8056-0678af4e6f62"); + content = Whitespace " "; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "1288ddd5-a751-40bd-b25c-9f229f0b3c7d"); + content = Whitespace " "; + }; + ], + [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "ebfe86ab-5be0-44f0-812b-642efbd02e51"); + label = [ "incr" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "b7bffab2-038f-4a55-9420-ce69c85049c1"); + label = [ "("; ")" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Exp ]; + nibs = + ( { + shape = Concave 2; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "2eddfac3-7e9b-4620-ace1-2874005749d8"); + label = [ "5" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "94fed024-4c98-4711-b743-f12953f3659d"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "ec2edb1c-a78b-4176-b057-d57ef1220436"); + label = [ "\\=/" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Concave 26; + sort = Drv Exp; + }, + { + shape = Concave 26; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "607a6141-eda2-4659-bbdb-bac9812894eb"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "f91fd96f-d510-4a36-9542-eea8535d2252"); + label = [ "6" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + ] ); + ancestors = []; + }; + caret = Inner (0, 0); + }; + rule = None; + }, + [] ); + ]; + }; + } diff --git a/src/haz3lweb/exercises/Ex_Closed_Substitution_prompt.re b/src/haz3lweb/exercises/Ex_Closed_Substitution_prompt.re new file mode 100644 index 000000000..7a7451878 --- /dev/null +++ b/src/haz3lweb/exercises/Ex_Closed_Substitution_prompt.re @@ -0,0 +1,4 @@ +open Virtual_dom.Vdom; +open Node; + +let prompt = div([]); diff --git a/src/haz3lweb/exercises/Ex_Type_Validation_Derivation.ml b/src/haz3lweb/exercises/Ex_Type_Validation_Derivation.ml new file mode 100644 index 000000000..d6b0ab462 --- /dev/null +++ b/src/haz3lweb/exercises/Ex_Type_Validation_Derivation.ml @@ -0,0 +1,757 @@ +let prompt = Ex_Type_Validation_Derivation_prompt.prompt + +let exercise : Exercise.spec = + { + header = + { + title = "Type Validation Derivation"; + version = 1; + module_name = "Ex_Type_Validation_Derivation"; + prompt; + }; + pos = Proof Prelude; + model = + Proof + { + prelude = + { + selection = { focus = Left; content = []; mode = Normal }; + backpack = []; + relatives = + { + siblings = + ( [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "b533dba4-a7fa-46d1-91a4-4e2b9d611641"); + label = [ "let"; "="; "in" ]; + mold = + { + out = Exp; + in_ = [ Pat; Exp ]; + nibs = + ( { shape = Convex; sort = Exp }, + { shape = Concave 17; sort = Exp } ); + }; + shards = [ 0; 1; 2 ]; + children = + [ + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "bb1c3b18-0d2d-45b9-b67b-77d3709d5397"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "24d4008d-2a18-424d-887f-eae2ab5de29b"); + label = [ "delta" ]; + mold = + { + out = Pat; + in_ = []; + nibs = + ( { shape = Convex; sort = Pat }, + { shape = Convex; sort = Pat } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "b3c26f13-96ad-44bf-85f6-1dec0c472d7c"); + content = Whitespace " "; + }; + ]; + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "22fd0d0e-b81e-49d2-876f-2111469150ac"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "17b70310-333d-4e61-8209-353f36514b67"); + label = [ "of_ctx"; "end" ]; + mold = + { + out = Exp; + in_ = [ Drv Exp ]; + nibs = + ( { shape = Convex; sort = Exp }, + { shape = Convex; sort = Exp } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "a1ab2949-9945-4dd1-92cf-9fadef1653b7"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "cb7a7fdb-8155-4c3b-9d31-decebbb4d5f6"); + label = [ "["; "]" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Exp ]; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Tile + { + id = + Option.get + (Haz3lcore.Id + .of_string + "813229a8-2d88-4d5e-9509-58b7fc3e9ac7"); + label = + [ "valid"; "end" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Typ ]; + nibs = + ( { + shape = + Convex; + sort = + Drv Exp; + }, + { + shape = + Convex; + sort = + Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Secondary + { + id = + Option.get + (Haz3lcore + .Id + .of_string + "2d391623-2177-43a3-ae2c-7b3790b5afeb"); + content = + Whitespace + " "; + }; + Tile + { + id = + Option.get + (Haz3lcore + .Id + .of_string + "a0d9e8e0-1238-4b23-a9d7-92fc744b505c"); + label = + [ "A" ]; + mold = + { + out = + Drv + Typ; + in_ = []; + nibs = + ( { + shape = + Convex; + sort = + Drv + Typ; + }, + { + shape = + Convex; + sort = + Drv + Typ; + } ); + }; + shards = + [ 0 ]; + children = + []; + }; + Secondary + { + id = + Option.get + (Haz3lcore + .Id + .of_string + "fa13eb3d-de40-45ff-aadd-43bc508c0941"); + content = + Whitespace + " "; + }; + ]; + ]; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "a828b61f-2cb5-4598-9acc-b43855c26e4f"); + content = Whitespace " "; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "e1efd65b-b2dd-4022-9b23-18d55f1eb3ad"); + content = Whitespace " "; + }; + ]; + ]; + }; + Grout + { + id = + Option.get + (Haz3lcore.Id.of_string + "150ad291-71cc-43b6-a8aa-5b45dea42978"); + shape = Convex; + }; + ], + [] ); + ancestors = []; + }; + caret = Outer; + }; + setup = + { + selection = { focus = Left; content = []; mode = Normal }; + backpack = []; + relatives = + { + siblings = + ( [], + [ + Grout + { + id = + Option.get + (Haz3lcore.Id.of_string + "2a1817bc-6d54-4a07-9c3b-3c29689ccfc7"); + shape = Convex; + }; + ] ); + ancestors = []; + }; + caret = Outer; + }; + trees = + [ + Node + ( Just + { + jdmt = + { + selection = + { focus = Left; content = []; mode = Normal }; + backpack = []; + relatives = + { + siblings = + ( [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "cd29a546-4616-488f-afb4-d959a990f709"); + label = [ "{"; "}" ]; + mold = + { + out = Drv Exp; + in_ = [ Pat ]; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "c62109a2-2c49-44a6-8e4a-d8856dd418f2"); + label = [ "delta" ]; + mold = + { + out = Pat; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Pat; + }, + { + shape = Convex; + sort = Pat; + } ); + }; + shards = [ 0 ]; + children = []; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "32c6cc78-d990-4a12-a0c1-2f7ed9b83aea"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "1620c2cb-09c4-4d61-80f0-a28963f14694"); + label = [ "|-" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Concave 26; + sort = Drv Exp; + }, + { + shape = Concave 26; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "fc8ba8e3-9b35-4aae-899c-dd09dae9e548"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "5901997d-d506-4493-be38-7490561a7616"); + label = [ "("; ")" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Exp ]; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "561e8a44-5228-4eb8-b288-1f624b5e6101"); + label = [ "fun"; "->" ]; + mold = + { + out = Drv Exp; + in_ = [ Drv Pat ]; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Concave 14; + sort = Drv Exp; + } ); + }; + shards = [ 0; 1 ]; + children = + [ + [ + Secondary + { + id = + Option.get + (Haz3lcore.Id + .of_string + "43462108-e539-429e-9f1a-1969db14bd52"); + content = + Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id + .of_string + "d9e2699f-bcc5-426c-aa5f-a4b64f21ce82"); + label = [ "x" ]; + mold = + { + out = Drv Pat; + in_ = []; + nibs = + ( { + shape = + Convex; + sort = + Drv Pat; + }, + { + shape = + Convex; + sort = + Drv Pat; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id + .of_string + "ff2ac15e-76ad-4ed5-91b5-370655a5be37"); + content = + Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id + .of_string + "76992270-2973-49bb-9cec-02ff67d43f4c"); + label = [ ":" ]; + mold = + { + out = Drv Pat; + in_ = []; + nibs = + ( { + shape = + Concave + 12; + sort = + Drv Pat; + }, + { + shape = + Concave + 12; + sort = + Drv Typ; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id + .of_string + "218c7a2a-a00e-44eb-93f1-4d8a6c0d404c"); + content = + Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id + .of_string + "68585ba6-a584-4212-8464-bc1081550497"); + label = [ "A" ]; + mold = + { + out = Drv Typ; + in_ = []; + nibs = + ( { + shape = + Convex; + sort = + Drv Typ; + }, + { + shape = + Convex; + sort = + Drv Typ; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id + .of_string + "b7c47e34-54b7-4519-a489-ce74976ca98f"); + content = + Whitespace " "; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "c3e2d208-2134-405e-9dfc-ebaf7d9a8ab7"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "a16c9d9a-1167-4749-8074-e0c93dc605a0"); + label = [ "x" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Exp; + }, + { + shape = Convex; + sort = Drv Exp; + } ); + }; + shards = [ 0 ]; + children = []; + }; + ]; + ]; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "4583f952-1a29-4271-84db-d626700bdae3"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "ebe1f8b9-896c-4515-a52a-f15e7554ace5"); + label = [ ":" ]; + mold = + { + out = Drv Exp; + in_ = []; + nibs = + ( { + shape = Concave 12; + sort = Drv Exp; + }, + { + shape = Concave 12; + sort = Drv Typ; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "4d48d124-84f8-4342-893d-1069c0118405"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "7325b8d1-941b-4628-877c-9fdae132597a"); + label = [ "A" ]; + mold = + { + out = Drv Typ; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Typ; + }, + { + shape = Convex; + sort = Drv Typ; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "74123937-04f3-4d8c-bdd6-d2e87ee6828c"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "511a9893-5ed7-4c3c-a168-c7192cfbafa7"); + label = [ "->" ]; + mold = + { + out = Drv Typ; + in_ = []; + nibs = + ( { + shape = Concave 5; + sort = Drv Typ; + }, + { + shape = Concave 5; + sort = Drv Typ; + } ); + }; + shards = [ 0 ]; + children = []; + }; + Secondary + { + id = + Option.get + (Haz3lcore.Id.of_string + "0ed6deb5-0f14-4bdd-9761-41aae97b980a"); + content = Whitespace " "; + }; + Tile + { + id = + Option.get + (Haz3lcore.Id.of_string + "f8b4dd23-f0f6-4cbc-a178-709507db394b"); + label = [ "A" ]; + mold = + { + out = Drv Typ; + in_ = []; + nibs = + ( { + shape = Convex; + sort = Drv Typ; + }, + { + shape = Convex; + sort = Drv Typ; + } ); + }; + shards = [ 0 ]; + children = []; + }; + ], + [] ); + ancestors = []; + }; + caret = Outer; + }; + rule = None; + }, + [] ); + ]; + }; + } diff --git a/src/haz3lweb/exercises/Ex_Type_Validation_Derivation_prompt.re b/src/haz3lweb/exercises/Ex_Type_Validation_Derivation_prompt.re new file mode 100644 index 000000000..7a7451878 --- /dev/null +++ b/src/haz3lweb/exercises/Ex_Type_Validation_Derivation_prompt.re @@ -0,0 +1,4 @@ +open Virtual_dom.Vdom; +open Node; + +let prompt = div([]);