Skip to content

Commit b97afd5

Browse files
bobatkeybobatkey
committed
[ slakemoth ] slim down the checking code
1 parent 4b677d6 commit b97afd5

File tree

7 files changed

+34
-350
lines changed

7 files changed

+34
-350
lines changed

‎slakemoth/bin/main.ml

-42
Original file line numberDiff line numberDiff line change
@@ -38,55 +38,13 @@ let pretty_print filename =
3838
(Format.pp_print_list Slakemoth_pp.Ast.pp_declaration) decls;
3939
Result.ok ()
4040

41-
module SimpleDoc = struct
42-
type block = string
43-
44-
type inline = string
45-
46-
let txt s = s
47-
let p = String.concat ""
48-
let code_bl s = s
49-
50-
let to_string = String.concat "\n\n"
51-
52-
end
53-
54-
let compare filename1 filename2 =
55-
let* file1 = Reader.parse (In_channel.with_open_bin filename1 In_channel.input_all) in
56-
let* file2 = Reader.parse (In_channel.with_open_bin filename2 In_channel.input_all) in
57-
let* commands1 = Type_checker.check_declarations file1 in
58-
let* commands2 = Type_checker.check_declarations file2 in
59-
match Compare.do_question commands1 commands2 with
60-
| Ok () ->
61-
Printf.printf "Equivalent!\n";
62-
exit 0
63-
| Error difference ->
64-
let doc = Compare.print_err (module SimpleDoc) difference in
65-
print_endline (SimpleDoc.to_string doc);
66-
exit 1
67-
68-
let mark marking_script submitted_script =
69-
let* marking_script = Reader.parse_marking_script (In_channel.with_open_bin marking_script In_channel.input_all) in
70-
let* submitted_script = Reader.parse (In_channel.with_open_bin submitted_script In_channel.input_all) in
71-
match Marker.check marking_script submitted_script with
72-
| Ok () ->
73-
print_endline "OK";
74-
exit 0
75-
| Error err ->
76-
print_endline (Marker.string_of_error err);
77-
exit 1
78-
7941
let () =
8042
handle_errors @@
8143
match Sys.argv with
8244
| [| _; "execute"; filename |] ->
8345
execute filename
8446
| [| _; "prettyprint"; filename |] ->
8547
pretty_print filename
86-
| [| _; "compare"; filename1; filename2 |] ->
87-
compare filename1 filename2
88-
| [| _; "mark"; filename1; filename2 |] ->
89-
mark filename1 filename2
9048
| _ ->
9149
Error (`Usage (Printf.sprintf "Usage: %s (execute|prettyprint) FILE\n"
9250
Sys.argv.(0)))

‎slakemoth/lib/core/ast.ml

-6
Original file line numberDiff line numberDiff line change
@@ -65,9 +65,3 @@ type declaration =
6565
| Print of term
6666

6767
type script = declaration list
68-
69-
type marking_script =
70-
{ domains : (name * constructor_name list) list
71-
; atoms : (name * name list) list
72-
; definitions : (name * term * term) list
73-
}

‎slakemoth/lib/core/compare.ml

+29-87
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,4 @@
1-
open Generalities
2-
open Result_ext.Syntax
1+
open! Generalities
32

43
let add_negated_clauses solver clauses =
54
let x =
@@ -31,6 +30,7 @@ let check_contains env constraint1 constraint2 =
3130
let assignment = Evaluator.assignment_of_vals atom_table vals in
3231
`EXTRA assignment
3332

33+
(*
3434
let rec rename_term rho term =
3535
let open Ast in
3636
match term.detail with
@@ -75,6 +75,10 @@ let rec rename_term rho term =
7575
| Next _ | The _ ->
7676
failwith "RENAME NEW STUFF"
7777
78+
exception Missing_atom of string
79+
exception Changed_Atom of string * (string * string) list * (string * string) list
80+
exception Atom_became_defn of string
81+
7882
let merge_environments (env1 : Environment.environment) (env2 : Environment.environment) =
7983
(* 1. Check that all the domains are the same *)
8084
(* 2. Check that all the atoms are the same *)
@@ -97,20 +101,22 @@ let merge_environments (env1 : Environment.environment) (env2 : Environment.envi
97101
|> Seq.map (fun (nm, _) -> nm, nm ^ "#2")
98102
|> NameMap.of_seq
99103
in
100-
let merged, defns2 =
101-
NameMap.fold
104+
let* merged, defns2 =
105+
try
106+
Result.ok @@ NameMap.fold
102107
(fun name defn (merged, env2) ->
103108
match defn with
104109
| Atom { args } ->
105110
(match NameMap.find_opt name env2 with
106-
| None -> failwith "Missing atom in env2"
111+
| None ->
112+
raise (Missing_atom name)
107113
| Some (Atom { args = args2 }) ->
108-
if args = args2 then
109-
(NameMap.add name (Atom { args}) merged, NameMap.remove name env2)
114+
if List.map snd args = List.map snd args2 then
115+
(NameMap.add name (Atom { args }) merged, NameMap.remove name env2)
110116
else
111-
failwith "Changed atom declaration"
117+
raise (Changed_Atom (name, args, args2))
112118
| Some (Defined _ | Table _) ->
113-
failwith "atom has become definition")
119+
raise (Atom_became_defn name))
114120
| Table _ ->
115121
failwith "TABLES"
116122
| Defined { args; body; kind } ->
@@ -121,6 +127,11 @@ let merge_environments (env1 : Environment.environment) (env2 : Environment.envi
121127
(NameMap.add name defn merged, env2))
122128
env1.defns
123129
(NameMap.empty, env2.defns)
130+
with
131+
| Atom_became_defn name -> Error (`Atom_become_defn name)
132+
| Missing_atom name -> Error (`Missing_atom name)
133+
| Changed_Atom (name, expected, given) ->
134+
Error (`Changed_atom (name, expected, given))
124135
in
125136
let defns =
126137
NameMap.fold
@@ -138,82 +149,13 @@ let merge_environments (env1 : Environment.environment) (env2 : Environment.envi
138149
merged
139150
in
140151
Ok ({ env1 with defns }, rename1, rename2)
152+
*)
141153

142-
143-
let do_question expected submitted =
144-
match expected, submitted with
145-
| [ Environment.AllSat (expected_env, expected_constraint, expected_json) ],
146-
[ Environment.AllSat (sub_env, sub_constraint, sub_json) ] ->
147-
let* (env, rename1, rename2) = merge_environments expected_env sub_env in
148-
let expected = rename_term rename1 expected_constraint in
149-
let submitted = rename_term rename2 sub_constraint in
150-
(match check_contains env expected submitted,
151-
check_contains env submitted expected with
152-
| `CONTAINED, `CONTAINED -> Ok ()
153-
| `EXTRA assgn, `CONTAINED ->
154-
let module E2 = Evaluator.Eval (val assgn) in
155-
let json = E2.to_json (E2.eval env E2.empty_local_env expected_json) in
156-
Error (`Not_enough_solutions json)
157-
| `CONTAINED, `EXTRA assgn ->
158-
let module E2 = Evaluator.Eval (val assgn) in
159-
let json = E2.to_json (E2.eval env E2.empty_local_env sub_json) in
160-
Error (`Too_many_solutions json)
161-
| `EXTRA expected, `EXTRA submitted ->
162-
let expected_json =
163-
let module E = Evaluator.Eval (val expected) in
164-
E.to_json (E.eval env E.empty_local_env expected_json)
165-
and submitted_json =
166-
let module E = Evaluator.Eval (val submitted) in
167-
E.to_json (E.eval env E.empty_local_env sub_json)
168-
in
169-
Error (`Solution_mismatch (expected_json, submitted_json)))
170-
| _, _ ->
171-
Error `Unexpected_commands
172-
173-
module type DOCUMENT = sig
174-
type block
175-
type inline
176-
177-
val txt : string -> inline
178-
val p : inline list -> block
179-
val code_bl : string -> block
180-
181-
end
182-
183-
let print_err (type block) (module D : DOCUMENT with type block = block) : _ -> block list =
184-
let open D in
185-
function
186-
(* | `Parse err -> *)
187-
(* [p [txt (Printf.sprintf "I was unable to parse your submission: %s" *)
188-
(* (Parser_util.Driver.string_of_error err))] *)
189-
(* ] *)
190-
(* | `Type_error (_loc, msg) -> *)
191-
(* [p [txt (Printf.sprintf "There was an error trying to interpret \ *)
192-
(* your submission: %s" msg)] *)
193-
(* ] *)
194-
| `Unexpected_commands ->
195-
[p [txt (Printf.sprintf "Your submission had unexpected commands in it.")]]
196-
| `Domain_mismatch ->
197-
[p [txt "There was a mismatch in the domain definitions, so I was \
198-
unable to mark this submission automatically."]]
199-
| `Not_enough_solutions expected_json ->
200-
[p [txt "Your code does not produce enough solutions. The \
201-
following solution is not generated by your constraints:"]
202-
; code_bl (Generalities.Json.to_string expected_json)
203-
]
204-
| `Too_many_solutions unwanted_json ->
205-
[p [txt "Your code produces too many solutions. The following \
206-
solution is generated by your constraints, but is not \
207-
required by the solution:"]
208-
; code_bl (Generalities.Json.to_string unwanted_json)
209-
]
210-
| `Solution_mismatch (expected, submitted) ->
211-
[ p [txt "Your code produces solutions that are not required, and \
212-
misses solutions that are required. The following is an \
213-
example of a solution that your code should produce but \
214-
does not:"]
215-
; code_bl (Generalities.Json.to_string expected)
216-
; p [txt "This is an example of a solution that you code produces \
217-
but should not:"]
218-
; code_bl (Generalities.Json.to_string submitted)
219-
]
154+
let implies env phi psi json =
155+
match check_contains env phi psi with
156+
| `CONTAINED ->
157+
`Contained
158+
| `EXTRA assgn ->
159+
let module E2 = Evaluator.Eval (val assgn) in
160+
let json = E2.to_json (E2.eval env E2.empty_local_env json) in
161+
`Extra json

‎slakemoth/lib/core/evaluator.ml

+1-1
Original file line numberDiff line numberDiff line change
@@ -177,7 +177,7 @@ module Eval (Assignment : ASSIGNMENT) = struct
177177
| exception Not_found ->
178178
(match NameMap.find name.detail env.defns with
179179
| exception Not_found ->
180-
raise (Evaluation_error "Definition not found") (* FIXME: say what *)
180+
raise (Evaluation_error (Printf.sprintf "Definition not found: %S" name.detail))
181181
| Atom _ ->
182182
let values =
183183
List.map (fun term -> to_constructor (eval local_env term)) terms

0 commit comments

Comments
 (0)