From 873172ae58cf8011d632b637003b02b845eadfd2 Mon Sep 17 00:00:00 2001 From: Henry Till Date: Wed, 28 Feb 2024 21:02:14 -0800 Subject: [PATCH] clean up whitespace --- src/boa/boa.ml | 2 +- src/boa/eval.ml | 8 +- src/boa/example.boa | 2 +- src/boa/lexer.mll | 2 +- src/boa/parser.mly | 22 ++--- src/boa/syntax.ml | 2 +- src/calc/eval.ml | 2 +- src/calc/syntax.ml | 2 +- src/comm/README.md | 2 +- src/lambda/README.md | 2 +- src/levy/eval.ml | 38 ++++---- src/levy/lexer.mll | 2 +- src/levy/parser.mly | 4 +- src/levy/syntax.ml | 32 +++---- src/levy/type_check.ml | 18 ++-- src/minihaskell/README.md | 4 +- src/minihaskell/example.minihaskell | 42 ++++----- src/minihaskell/interpret.ml | 64 +++++++------- src/minihaskell/lexer.mll | 2 +- src/minihaskell/parser.mly | 28 +++--- src/minihaskell/syntax.ml | 66 +++++++------- src/minihaskell/type_check.ml | 22 ++--- src/miniml/lexer.mll | 2 +- src/miniml/machine.ml | 30 +++---- src/miniml/miniml.ml | 2 +- src/miniml/parser.mly | 8 +- src/miniml/syntax.ml | 20 ++--- src/miniml/type_check.ml | 10 +-- src/miniml_error/lexer.mll | 2 +- src/miniml_error/machine.ml | 30 +++---- src/miniml_error/parser.mly | 8 +- src/miniml_error/syntax.ml | 20 ++--- src/miniprolog/README.md | 2 +- src/miniprolog/solve.ml | 44 +++++----- src/miniprolog/syntax.ml | 10 +-- src/miniprolog/unify.ml | 8 +- src/poly/example.poly | 14 +-- src/poly/interpret.ml | 96 ++++++++++---------- src/poly/lexer.mll | 2 +- src/poly/parser.mly | 22 ++--- src/poly/syntax.ml | 94 ++++++++++---------- src/poly/type_infer.ml | 132 ++++++++++++++-------------- src/sub/eval.ml | 52 +++++------ src/sub/lexer.mll | 2 +- src/sub/parser.mly | 24 ++--- src/sub/syntax.ml | 20 ++--- src/sub/type_check.ml | 34 +++---- 47 files changed, 528 insertions(+), 528 deletions(-) diff --git a/src/boa/boa.ml b/src/boa/boa.ml index 6e8bf35..e3e9f2a 100644 --- a/src/boa/boa.ml +++ b/src/boa/boa.ml @@ -20,7 +20,7 @@ let exec env = function (* evaluate [e] *) let v = Eval.eval env e in Format.printf "%t@." (Eval.print_value v) ; - env + env | Syntax.Def (x, e) -> (* define a new global value *) diff --git a/src/boa/eval.ml b/src/boa/eval.ml index 4e16451..b1f0f5f 100644 --- a/src/boa/eval.ml +++ b/src/boa/eval.ml @@ -122,9 +122,9 @@ let eval env e = | Syntax.If (e1, e2, e3) -> if get_bool (eval th env e1) then - eval th env e2 + eval th env e2 else - eval th env e3 + eval th env e3 | Syntax.Skip -> unit_obj @@ -145,8 +145,8 @@ let eval env e = | Syntax.This -> (match th with - | Some v -> v - | None -> Zoo.error "invalid use of 'this'") + | Some v -> v + | None -> Zoo.error "invalid use of 'this'") | Syntax.Object lst -> mk_obj (List.map (fun (x,e) -> (x, ref (eval th env e))) lst) diff --git a/src/boa/example.boa b/src/boa/example.boa index c0bfa67..1309e56 100644 --- a/src/boa/example.boa +++ b/src/boa/example.boa @@ -88,7 +88,7 @@ let list = { isEmpty = fun _ -> this.empty, getHead = fun _ -> this.head, getTail = fun _ -> this.tail, - + # constructors nil = fun _ -> this with { empty = true }, cons = fun x -> fun xs -> this with { empty = false, head = x, tail = xs }, diff --git a/src/boa/lexer.mll b/src/boa/lexer.mll index c584de7..dd3cdf3 100644 --- a/src/boa/lexer.mll +++ b/src/boa/lexer.mll @@ -17,7 +17,7 @@ rule token = parse | "fun" { FUN } | "if" { IF } | "in" { IN } - | "let" { LET } + | "let" { LET } | "not" { NOT } | "or" { OR } | "skip" { SKIP } diff --git a/src/boa/parser.mly b/src/boa/parser.mly index abfd38a..0f9c308 100644 --- a/src/boa/parser.mly +++ b/src/boa/parser.mly @@ -58,7 +58,7 @@ expr: | app { $1 } | arith { $1 } | boolean { $1 } - | IF expr THEN expr ELSE expr { If ($2, $4, $6) } + | IF expr THEN expr ELSE expr { If ($2, $4, $6) } | FUN VAR ARROW expr { Fun ($2, $4) } | LET VAR EQUAL expr IN expr { Let ($2, $4, $6) } | non_app PERIOD VAR ASSIGN expr { Assign ($1, $3, $5) } @@ -69,24 +69,24 @@ app: | non_app non_app { App ($1, $2) } non_app: - VAR { Var $1 } + VAR { Var $1 } | THIS { This } - | TRUE { Bool true } - | FALSE { Bool false } - | INT { Int $1 } + | TRUE { Bool true } + | FALSE { Bool false } + | INT { Int $1 } | SKIP { Skip } - | LPAREN expr RPAREN { $2 } + | LPAREN expr RPAREN { $2 } | non_app PERIOD VAR { Project ($1, $3) } | LBRACE fields RBRACE { Object $2 } | COPY non_app { Copy $2 } | non_app WITH non_app { With ($1, $3) } arith: - | expr PLUS expr { ArithOp (Plus, $1, $3) } - | expr MINUS expr { ArithOp (Minus, $1, $3) } - | expr TIMES expr { ArithOp (Times, $1, $3) } - | expr DIVIDE expr { ArithOp (Divide, $1, $3) } - | expr REMAINDER expr { ArithOp (Remainder, $1, $3) } + | expr PLUS expr { ArithOp (Plus, $1, $3) } + | expr MINUS expr { ArithOp (Minus, $1, $3) } + | expr TIMES expr { ArithOp (Times, $1, $3) } + | expr DIVIDE expr { ArithOp (Divide, $1, $3) } + | expr REMAINDER expr { ArithOp (Remainder, $1, $3) } boolean: | NOT expr { Not $2 } diff --git a/src/boa/syntax.ml b/src/boa/syntax.ml index 67faf40..38e7799 100644 --- a/src/boa/syntax.ml +++ b/src/boa/syntax.ml @@ -15,7 +15,7 @@ type boolop = And | Or (** Expressions *) type expr = | Var of name (** variable *) - | Bool of bool (** boolean constant [true] or [false] *) + | Bool of bool (** boolean constant [true] or [false] *) | Int of int (** integer constant *) | ArithOp of arithop * expr * expr (** arithmetical operation [e1 op e2] *) | Not of expr (** logical negation [not e] *) diff --git a/src/calc/eval.ml b/src/calc/eval.ml index f33b79c..ed97609 100644 --- a/src/calc/eval.ml +++ b/src/calc/eval.ml @@ -9,5 +9,5 @@ let rec eval = function | Syntax.Times (e1, e2) -> eval e1 * eval e2 | Syntax.Divide (e1, e2) -> let n2 = eval e2 in - if n2 <> 0 then eval e1 / n2 else Zoo.error "division by zero" + if n2 <> 0 then eval e1 / n2 else Zoo.error "division by zero" | Syntax.Negate e -> - (eval e) diff --git a/src/calc/syntax.ml b/src/calc/syntax.ml index 3914de8..e59e5cf 100644 --- a/src/calc/syntax.ml +++ b/src/calc/syntax.ml @@ -13,7 +13,7 @@ type expression = let string_of_expression e = let rec to_str n e = let (m, str) = match e with - Numeral n -> (3, string_of_int n) + Numeral n -> (3, string_of_int n) | Negate e -> (2, "-" ^ (to_str 2 e)) | Times (e1, e2) -> (1, (to_str 1 e1) ^ " * " ^ (to_str 2 e2)) | Divide (e1, e2) -> (1, (to_str 1 e1) ^ " / " ^ (to_str 2 e2)) diff --git a/src/comm/README.md b/src/comm/README.md index 79b778a..3df8102 100644 --- a/src/comm/README.md +++ b/src/comm/README.md @@ -18,7 +18,7 @@ Boolean expression `b`: * boolean constants `true` and `false` * conjunction `b₁ and b₂` -* disjunction `b₁ or b₂` +* disjunction `b₁ or b₂` * negation `not b` Command `c`: diff --git a/src/lambda/README.md b/src/lambda/README.md index aee7c13..a7fa20a 100644 --- a/src/lambda/README.md +++ b/src/lambda/README.md @@ -24,7 +24,7 @@ to call by value and the weak head normal form to call by name. The file `example.lambda` contains an example session which defines booleans, numbers, and lists. You can use it as follows: - $ ./lambda.native -l example.lambda + $ ./lambda.native -l example.lambda pair is defined. first is defined. second is defined. diff --git a/src/levy/eval.ml b/src/levy/eval.ml index 5639ce7..8f0eb80 100644 --- a/src/levy/eval.ml +++ b/src/levy/eval.ml @@ -26,16 +26,16 @@ let rec comp env e = | Syntax.If (e1, e2, e3) -> (match expr env e1 with - | VBool true -> comp env e2 - | VBool false -> comp env e3 - | _ -> runtime_error ~loc:(e1.Zoo.loc) "boolean expected") + | VBool true -> comp env e2 + | VBool false -> comp env e3 + | _ -> runtime_error ~loc:(e1.Zoo.loc) "boolean expected") | Syntax.Apply (e1, e2) -> (match comp env e1 with - | VFun (env', x, e) -> + | VFun (env', x, e) -> let v2 = expr env e2 in comp ((x,v2)::env') e - | _ -> runtime_error ~loc:(e1.Zoo.loc) "function expected") + | _ -> runtime_error ~loc:(e1.Zoo.loc) "function expected") | Syntax.Let (x, e1, e2) -> let v = expr env e1 in @@ -50,8 +50,8 @@ let rec comp env e = | Syntax.Force e -> (match expr env e with - | VThunk (env, e) -> comp env e - | _ -> runtime_error ~loc:(e.Zoo.loc) "thunk expected in force") + | VThunk (env, e) -> comp env e + | _ -> runtime_error ~loc:(e.Zoo.loc) "thunk expected in force") | Syntax.Rec (x, _, e') -> comp ((x, VThunk (env, e)) :: env) e' @@ -71,9 +71,9 @@ and expr env {Zoo.data=e; loc} = | Syntax.Var x -> (try - List.assoc x env + List.assoc x env with - Not_found -> runtime_error ~loc "unknown variable %s" x) + Not_found -> runtime_error ~loc "unknown variable %s" x) | Syntax.Int k -> VInt k @@ -83,27 +83,27 @@ and expr env {Zoo.data=e; loc} = | Syntax.Times (e1, e2) -> (match (expr env e1), (expr env e2) with - | VInt k1, VInt k2 -> VInt (k1 * k2) - | _ -> runtime_error ~loc "integers expected in multiplication") + | VInt k1, VInt k2 -> VInt (k1 * k2) + | _ -> runtime_error ~loc "integers expected in multiplication") | Syntax.Plus (e1, e2) -> (match (expr env e1), (expr env e2) with - | VInt k1, VInt k2 -> VInt (k1 + k2) - | _ -> runtime_error ~loc "integers expected in addition") + | VInt k1, VInt k2 -> VInt (k1 + k2) + | _ -> runtime_error ~loc "integers expected in addition") | Syntax.Minus (e1, e2) -> (match (expr env e1), (expr env e2) with - | VInt k1, VInt k2 -> VInt (k1 - k2) - | _ -> runtime_error ~loc "integers expected in subtraction") + | VInt k1, VInt k2 -> VInt (k1 - k2) + | _ -> runtime_error ~loc "integers expected in subtraction") | Syntax.Equal (e1, e2) -> (match (expr env e1), (expr env e2) with - | VInt k1, VInt k2 -> VBool (k1 = k2) - | _ -> runtime_error ~loc "integers expected in =") + | VInt k1, VInt k2 -> VBool (k1 = k2) + | _ -> runtime_error ~loc "integers expected in =") | Syntax.Less (e1, e2) -> (match (expr env e1), (expr env e2) with - | VInt k1, VInt k2 -> VBool (k1 < k2) - | _ -> runtime_error ~loc "integers expected in <") + | VInt k1, VInt k2 -> VBool (k1 < k2) + | _ -> runtime_error ~loc "integers expected in <") | Syntax.Force _ | Syntax.Return _ diff --git a/src/levy/lexer.mll b/src/levy/lexer.mll index 9b23013..69afcfd 100644 --- a/src/levy/lexer.mll +++ b/src/levy/lexer.mll @@ -25,7 +25,7 @@ rule token = parse | "if" { IF } | "in" { IN } | "is" { IS } - | "let" { LET } + | "let" { LET } | "rec" { REC } | "return" { RETURN } | "then" { THEN } diff --git a/src/levy/parser.mly b/src/levy/parser.mly index 45503b4..e6b989d 100644 --- a/src/levy/parser.mly +++ b/src/levy/parser.mly @@ -62,7 +62,7 @@ plain_expr: | IF expr THEN expr ELSE expr { If ($2, $4, $6) } | FUN VAR COLON ty DARROW expr { Fun ($2, $4, $6) } | REC VAR COLON ty IS expr { Rec ($2, $4, $6) } - + (* boolean: mark_position(plain_boolean) { $1 } *) plain_boolean: | plain_arith { $1 } @@ -94,7 +94,7 @@ plain_simple: | INT { Int $1 } | TRUE { Bool true } | FALSE { Bool false } - | LPAREN plain_expr RPAREN { $2 } + | LPAREN plain_expr RPAREN { $2 } ty: mark_position(plain_ty) { $1 } plain_ty: diff --git a/src/levy/syntax.ml b/src/levy/syntax.ml index 7e89d7e..afbc4e1 100644 --- a/src/levy/syntax.ml +++ b/src/levy/syntax.ml @@ -25,23 +25,23 @@ type value = expr and expr = expr' Zoo.located and expr' = - | Var of name (** variable *) - | Int of int (** integer constant *) - | Bool of bool (** boolean constant *) - | Times of value * value (** product [v1 * v2] *) - | Plus of value * value (** sum [v1 + v2] *) - | Minus of value * value (** difference [v1 - v2] *) - | Equal of value * value (** integer equality [v1 = v2] *) - | Less of value * value (** integer comparison [v1 < v2] *) - | Thunk of expr (** thunk [thunk e] *) - | Force of value (** [force v] *) - | Return of value (** [return v] *) - | Do of name * expr * expr (** sequencing [do x <- e1 in e2] *) + | Var of name (** variable *) + | Int of int (** integer constant *) + | Bool of bool (** boolean constant *) + | Times of value * value (** product [v1 * v2] *) + | Plus of value * value (** sum [v1 + v2] *) + | Minus of value * value (** difference [v1 - v2] *) + | Equal of value * value (** integer equality [v1 = v2] *) + | Less of value * value (** integer comparison [v1 < v2] *) + | Thunk of expr (** thunk [thunk e] *) + | Force of value (** [force v] *) + | Return of value (** [return v] *) + | Do of name * expr * expr (** sequencing [do x <- e1 in e2] *) | Let of name * value * expr (** let-binding [let x = v in e] *) - | If of value * expr * expr (** conditional [if v then e1 else e2] *) - | Fun of name * ltype * expr (** function [fun x:s -> e] *) - | Apply of expr * value (** application [e v] *) - | Rec of name * ltype * expr (** recursion [rec x : t is e] *) + | If of value * expr * expr (** conditional [if v then e1 else e2] *) + | Fun of name * ltype * expr (** function [fun x:s -> e] *) + | Apply of expr * value (** application [e v] *) + | Rec of name * ltype * expr (** recursion [rec x : t is e] *) (** Toplevel commands *) type toplevel = diff --git a/src/levy/type_check.ml b/src/levy/type_check.ml index 971bf54..b08c267 100644 --- a/src/levy/type_check.ml +++ b/src/levy/type_check.ml @@ -15,7 +15,7 @@ let rec print_vtype ?max_level vty ppf = match vty with | VInt -> Format.fprintf ppf "int" | VBool -> Format.fprintf ppf "bool" - | VForget cty -> + | VForget cty -> Zoo.print_parens ?max_level ~at_level:2 ppf "U@ %t" (print_ctype ~max_level:1 cty) @@ -24,7 +24,7 @@ and print_ctype ?max_level cty ppf = match cty with | CFree vty -> Zoo.print_parens ?max_level ~at_level:2 ppf - "F@ %t" + "F@ %t" (print_vtype ~max_level:1 vty) | CArrow (vty, cty) -> Zoo.print_parens ?max_level ~at_level:1 ppf @@ -44,7 +44,7 @@ and as_vtype {Zoo.data=ty; loc} = | Syntax.VInt -> VInt | Syntax.VBool -> VBool | Syntax.VForget ty -> VForget (as_ctype ty) - | Syntax.CFree _ | Syntax.CArrow _ -> + | Syntax.CFree _ | Syntax.CArrow _ -> type_error ~loc "this is not a value type" (** [check ctx ty e] checks that expression [e] has computation @@ -71,10 +71,10 @@ and check_ctype ctx cty e = and vtype_of ctx {Zoo.data=e; loc} = match e with | Syntax.Var x -> - (try - List.assoc x ctx + (try + List.assoc x ctx with - Not_found -> type_error ~loc "unknown identifier %s" x) + Not_found -> type_error ~loc "unknown identifier %s" x) | Syntax.Int _ -> VInt @@ -140,7 +140,7 @@ and ctype_of ctx {Zoo.data=e; loc} = check_vtype ctx ty1 e2 ; ty2 | ty -> - type_error ~loc:(e1.Zoo.loc) + type_error ~loc:(e1.Zoo.loc) "this expression is used as a function but its type is %t" (print_ctype ty)) @@ -148,7 +148,7 @@ and ctype_of ctx {Zoo.data=e; loc} = (match ctype_of ctx e1 with | CFree ty1 -> ctype_of ((x,ty1)::ctx) e2 | ty -> type_error ~loc:(e1.Zoo.loc) - "this expression is sequenced but its type is %t" + "this expression is sequenced but its type is %t" (print_ctype ty)) | Syntax.Let (x, e1, e2) -> @@ -178,7 +178,7 @@ and ctype_of ctx {Zoo.data=e; loc} = | Syntax.Minus _ | Syntax.Times _ | Syntax.Equal _ - | Syntax.Less _ + | Syntax.Less _ | Syntax.Thunk _ -> type_error ~loc "a computation was expected but a value was encountered" diff --git a/src/minihaskell/README.md b/src/minihaskell/README.md index a87a5d7..b3814d1 100644 --- a/src/minihaskell/README.md +++ b/src/minihaskell/README.md @@ -12,7 +12,7 @@ A lazy functional language with following features: The file primes.minhs defines the infinite list of prime numbers. You can load it and try it as follows: - $ ./minihaskell.byte prime.minhs + $ ./minihaskell.byte prime.minhs val not : bool -> bool val div : int -> int -> int val mod : int -> int -> int @@ -37,5 +37,5 @@ can load it and try it as follows: :: 383 :: 389 :: 397 :: 401 :: 409 :: 419 :: 421 :: 431 :: 433 :: 439 :: 443 :: 449 :: 457 :: 461 :: 463 :: 467 :: 479 :: 487 :: 491 :: 499 :: 503 :: 509 :: 521 :: 523 :: ... :: ... - MiniHaskell> + MiniHaskell> Good bye. diff --git a/src/minihaskell/example.minihaskell b/src/minihaskell/example.minihaskell index 9009b84..0d4dc40 100644 --- a/src/minihaskell/example.minihaskell +++ b/src/minihaskell/example.minihaskell @@ -10,54 +10,54 @@ let append = rec append : int list -> int list -> int list is fun lst1 : int list => fun lst2 : int list => match lst1 with - [int] => lst2 - | x::xs => x :: (append xs lst2) + [int] => lst2 + | x::xs => x :: (append xs lst2) ;; let fold_left = rec fold_left : (int -> int -> int) -> int -> int list -> int is fun f : (int -> int -> int) => fun x0 : int => - fun lst : int list => - match lst with - [int] => x0 - | x::xs => fold_left f (f x0 x) xs + fun lst : int list => + match lst with + [int] => x0 + | x::xs => fold_left f (f x0 x) xs ;; let flatten = rec flatten : int list list -> int list is fun lsts : int list list => match lsts with - [int list] => [int] - | l :: ls => append l (flatten ls) + [int list] => [int] + | l :: ls => append l (flatten ls) ;; let zip2 = rec zip2 : int list -> int list -> int list is fun l1 : int list => fun l2 : int list => - match l1 with - [int] => l2 - | x::xs => - x :: (match l2 with - [int] => xs - | y::ys => y::(zip2 xs ys)) + match l1 with + [int] => l2 + | x::xs => + x :: (match l2 with + [int] => xs + | y::ys => y::(zip2 xs ys)) ;; let zip = rec zip : int list list -> int list is fun lsts : int list list => match lsts with - [int list] => [int] - | l::ls => zip2 l (zip ls) + [int list] => [int] + | l::ls => zip2 l (zip ls) + - let map = rec map : (int -> int) -> int list -> int list is fun f : (int -> int) => fun l : int list => match l with - [int] => [int] - | x::xs => (f x) :: (map f xs) + [int] => [int] + | x::xs => (f x) :: (map f xs) ;; let filter = @@ -94,7 +94,7 @@ let notmultiple = fun m : int => fun n : int => let nth = rec nth : int list -> int -> int is fun l : int list => fun n : int => match l with - [int] => 0 + [int] => 0 | x::xs => if n = 0 then x else nth xs (n-1) ;; @@ -108,7 +108,7 @@ let sieve = rec sieve : int list -> int list is fun l : int list => match l with [int] => [int] - | n::ns => n :: (sieve (filter (notmultiple n) ns)) + | n::ns => n :: (sieve (filter (notmultiple n) ns)) ;; -- the infinite list of primes diff --git a/src/minihaskell/interpret.ml b/src/minihaskell/interpret.ml index a88f130..f243f1e 100644 --- a/src/minihaskell/interpret.ml +++ b/src/minihaskell/interpret.ml @@ -15,36 +15,36 @@ let runtime_error msg = raise (Runtime_error msg) let rec interp env = function | Syntax.Var x -> (try - let r = List.assoc x env in - match !r with - VClosure (env', e) -> let v = interp env' e in r := v ; v - | v -> v + let r = List.assoc x env in + match !r with + VClosure (env', e) -> let v = interp env' e in r := v ; v + | v -> v with - Not_found -> runtime_error ("Unknown variable " ^ x)) + Not_found -> runtime_error ("Unknown variable " ^ x)) | Syntax.Int k -> VInt k | Syntax.Bool b -> VBool b | Syntax.Times (e1, e2) -> (match (interp env e1), (interp env e2) with - VInt k1, VInt k2 -> VInt (k1 * k2) - | _ -> runtime_error "Integers expected in multiplication") + VInt k1, VInt k2 -> VInt (k1 * k2) + | _ -> runtime_error "Integers expected in multiplication") | Syntax.Divide (e1, e2) -> (match (interp env e1), (interp env e2) with - VInt _, VInt 0 -> runtime_error ("Division by 0") - | VInt k1, VInt k2 -> VInt (k1 / k2) - | _ -> runtime_error "Integers expected in division") + VInt _, VInt 0 -> runtime_error ("Division by 0") + | VInt k1, VInt k2 -> VInt (k1 / k2) + | _ -> runtime_error "Integers expected in division") | Syntax.Mod (e1, e2) -> (match (interp env e1), (interp env e2) with - VInt _, VInt 0 -> runtime_error ("Division by 0") - | VInt k1, VInt k2 -> VInt (k1 mod k2) - | _ -> runtime_error "Integers expected in remainder") + VInt _, VInt 0 -> runtime_error ("Division by 0") + | VInt k1, VInt k2 -> VInt (k1 mod k2) + | _ -> runtime_error "Integers expected in remainder") | Syntax.Plus (e1, e2) -> (match (interp env e1), (interp env e2) with - VInt k1, VInt k2 -> VInt (k1 + k2) - | _ -> runtime_error "Integers expected in addition") + VInt k1, VInt k2 -> VInt (k1 + k2) + | _ -> runtime_error "Integers expected in addition") | Syntax.Minus (e1, e2) -> (match (interp env e1), (interp env e2) with - VInt k1, VInt k2 -> VInt (k1 - k2) - | _ -> runtime_error "Integers expected in subtraction") + VInt k1, VInt k2 -> VInt (k1 - k2) + | _ -> runtime_error "Integers expected in subtraction") | Syntax.Equal (e1, e2) -> (match (interp env e1), (interp env e2) with | VInt k1, VInt k2 -> VBool (k1 = k2) @@ -62,7 +62,7 @@ let rec interp env = function | Syntax.Apply (e1, e2) -> (match interp env e1 with | VClosure (env', Syntax.Fun (x, _, e)) -> - interp ((x, ref (VClosure (env, e2)))::env') e + interp ((x, ref (VClosure (env, e2)))::env') e | _ -> runtime_error "Function expected in application") | Syntax.Pair _ as e -> VClosure (env, e) | Syntax.Fst e -> @@ -75,14 +75,14 @@ let rec interp env = function | _ -> runtime_error "Pair expected in snd") | Syntax.Rec (x, _, e) -> let rec env' = (x,ref (VClosure (env',e))) :: env in - interp env' e + interp env' e | Syntax.Nil ty -> VNil ty | Syntax.Cons _ as e -> VClosure (env, e) | Syntax.Match (e1, _, e2, x, y, e3) -> (match interp env e1 with | VNil _ -> interp env e2 | VClosure (env', Syntax.Cons (d1, d2)) -> - interp ((x,ref (VClosure(env',d1)))::(y,ref (VClosure(env',d2)))::env) e3 + interp ((x,ref (VClosure(env',d1)))::(y,ref (VClosure(env',d2)))::env) e3 | _ -> runtime_error "List expected in match") @@ -96,19 +96,19 @@ let rec print_result n v = | VBool b -> print_string (string_of_bool b) | VNil ty -> print_string ("[" ^ Syntax.string_of_type ty ^ "]") | VClosure (env, Syntax.Pair (e1, e2)) -> - print_char '(' ; - print_result (n/2) (interp env e1) ; - print_string ", " ; - print_result (n/2) (interp env e2) ; - print_char ')' + print_char '(' ; + print_result (n/2) (interp env e1) ; + print_string ", " ; + print_result (n/2) (interp env e2) ; + print_char ')' | VClosure (env, Syntax.Cons (e1, e2)) -> - let v1 = interp env e1 in - (match v1 with - | VClosure (_, Syntax.Cons _) -> - print_char '(' ; print_result (n/2) v1 ; print_char ')' - | _ -> print_result (n/2) v1) ; - print_string " :: " ; - print_result (n-1) (interp env e2) + let v1 = interp env e1 in + (match v1 with + | VClosure (_, Syntax.Cons _) -> + print_char '(' ; print_result (n/2) v1 ; print_char ')' + | _ -> print_result (n/2) v1) ; + print_string " :: " ; + print_result (n-1) (interp env e2) | VClosure (_, Syntax.Fun _) -> print_string "" | _ -> print_string "?" ) ; diff --git a/src/minihaskell/lexer.mll b/src/minihaskell/lexer.mll index ad9c713..3839d9b 100644 --- a/src/minihaskell/lexer.mll +++ b/src/minihaskell/lexer.mll @@ -18,7 +18,7 @@ rule token = parse | "if" { IF } | "int" { TINT } | "is" { IS } - | "let" { LET } + | "let" { LET } | "list" { TLIST } | "match" { MATCH } | "rec" { REC } diff --git a/src/minihaskell/parser.mly b/src/minihaskell/parser.mly index 530b430..a21e944 100644 --- a/src/minihaskell/parser.mly +++ b/src/minihaskell/parser.mly @@ -77,7 +77,7 @@ expr: | arith { $1 } | boolean { $1 } | expr CONS expr { Cons ($1, $3) } - | IF expr THEN expr ELSE expr { If ($2, $4, $6) } + | IF expr THEN expr ELSE expr { If ($2, $4, $6) } | FUN VAR COLON ty DARROW expr { Fun ($2, $4, $6) } | REC VAR COLON ty IS expr { Rec ($2, $4, $6) } | MATCH expr WITH nil DARROW expr ALTERNATIVE VAR CONS VAR DARROW expr @@ -90,21 +90,21 @@ app: | non_app non_app { Apply ($1, $2) } non_app: - VAR { Var $1 } - | TRUE { Bool true } - | FALSE { Bool false } - | INT { Int $1 } + VAR { Var $1 } + | TRUE { Bool true } + | FALSE { Bool false } + | INT { Int $1 } | nil { Nil $1 } - | LPAREN expr RPAREN { $2 } + | LPAREN expr RPAREN { $2 } | LPAREN expr COMMA expr RPAREN { Pair ($2, $4) } arith: | MINUS INT { Int (-$2) } - | expr PLUS expr { Plus ($1, $3) } - | expr MINUS expr { Minus ($1, $3) } - | expr TIMES expr { Times ($1, $3) } - | expr DIVIDE expr { Divide ($1, $3) } - | expr MOD expr { Mod ($1, $3) } + | expr PLUS expr { Plus ($1, $3) } + | expr MINUS expr { Minus ($1, $3) } + | expr TIMES expr { Times ($1, $3) } + | expr DIVIDE expr { Divide ($1, $3) } + | expr MOD expr { Mod ($1, $3) } nil: LBRACK ty RBRACK { $2 } @@ -119,15 +119,15 @@ ty: ty_times : | ty_list { $1 } | ty_times TIMES ty_list { TTimes ($1, $3) } - + ty_list : | ty_simple { $1 } | ty_list TLIST { TList $1 } ty_simple : - | TBOOL { TBool } - | TINT { TInt } + | TBOOL { TBool } + | TINT { TInt } | LPAREN ty RPAREN { $2 } %% diff --git a/src/minihaskell/syntax.ml b/src/minihaskell/syntax.ml index c93cd5e..b85a965 100644 --- a/src/minihaskell/syntax.ml +++ b/src/minihaskell/syntax.ml @@ -46,11 +46,11 @@ let string_of_type ty = let rec to_str n ty = let (m, str) = match ty with - TInt -> (4, "int") - | TBool -> (4, "bool") - | TList ty -> (3, to_str 3 ty ^ " list") - | TTimes (ty1, ty2) -> (2, (to_str 2 ty1) ^ " * " ^ (to_str 2 ty2)) - | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2)) + TInt -> (4, "int") + | TBool -> (4, "bool") + | TList ty -> (3, to_str 3 ty ^ " list") + | TTimes (ty1, ty2) -> (2, (to_str 2 ty1) ^ " * " ^ (to_str 2 ty2)) + | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2)) in if m > n then str else "(" ^ str ^ ")" in @@ -61,33 +61,33 @@ let string_of_expr e = let rec to_str n e = let (m, str) = match e with - Int n -> (10, string_of_int n) - | Bool b -> (10, string_of_bool b) - | Var x -> (10, x) - | Pair (e1, e2) -> (10, "(" ^ (to_str 0 e1) ^ ", " ^ (to_str 0 e2) ^ ")") - | Nil ty -> (10, "[" ^ (string_of_type ty) ^ "]") - | Fst e -> (9, "fst " ^ (to_str 9 e)) - | Snd e -> (9, "snd " ^ (to_str 9 e)) - | Apply (_, _) -> (10, "") - (* (9, (to_str 8 e1) ^ " " ^ (to_str 9 e2)) *) - | Times (e1, e2) -> (8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2)) - | Divide (e1, e2) -> (8, (to_str 7 e1) ^ " / " ^ (to_str 8 e2)) - | Mod (e1, e2) -> (8, (to_str 7 e1) ^ " % " ^ (to_str 8 e2)) - | Plus (e1, e2) -> (7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2)) - | Minus (e1, e2) -> (7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2)) - | Cons (e1, e2) -> (6, (to_str 6 e1) ^ " :: " ^ (to_str 5 e2)) - | Equal (e1, e2) -> (5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2)) - | Less (e1, e2) -> (5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2)) - | If (e1, e2, e3) -> (4, "if " ^ (to_str 4 e1) ^ " then " ^ - (to_str 4 e2) ^ " else " ^ (to_str 4 e3)) - | Match (e1, ty, e2, x, y, e3) -> - (3, "match " ^ (to_str 3 e1) ^ " with " ^ - "[" ^ (string_of_type ty) ^ "] -> " ^ (to_str 3 e2) ^ " | " ^ - x ^ "::" ^ y ^ " -> " ^ (to_str 3 e3)) - | Fun (_, _, _) -> (10, "") - (* (2, "fun " ^ x ^ " : " ^ (string_of_type ty) ^ " -> " ^ (to_str 0 e)) *) - | Rec (_, _, _) -> (10, "") - (* (1, "rec " ^ x ^ " : " ^ (string_of_type ty) ^ " is " ^ (to_str 0 e)) *) + Int n -> (10, string_of_int n) + | Bool b -> (10, string_of_bool b) + | Var x -> (10, x) + | Pair (e1, e2) -> (10, "(" ^ (to_str 0 e1) ^ ", " ^ (to_str 0 e2) ^ ")") + | Nil ty -> (10, "[" ^ (string_of_type ty) ^ "]") + | Fst e -> (9, "fst " ^ (to_str 9 e)) + | Snd e -> (9, "snd " ^ (to_str 9 e)) + | Apply (_, _) -> (10, "") + (* (9, (to_str 8 e1) ^ " " ^ (to_str 9 e2)) *) + | Times (e1, e2) -> (8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2)) + | Divide (e1, e2) -> (8, (to_str 7 e1) ^ " / " ^ (to_str 8 e2)) + | Mod (e1, e2) -> (8, (to_str 7 e1) ^ " % " ^ (to_str 8 e2)) + | Plus (e1, e2) -> (7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2)) + | Minus (e1, e2) -> (7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2)) + | Cons (e1, e2) -> (6, (to_str 6 e1) ^ " :: " ^ (to_str 5 e2)) + | Equal (e1, e2) -> (5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2)) + | Less (e1, e2) -> (5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2)) + | If (e1, e2, e3) -> (4, "if " ^ (to_str 4 e1) ^ " then " ^ + (to_str 4 e2) ^ " else " ^ (to_str 4 e3)) + | Match (e1, ty, e2, x, y, e3) -> + (3, "match " ^ (to_str 3 e1) ^ " with " ^ + "[" ^ (string_of_type ty) ^ "] -> " ^ (to_str 3 e2) ^ " | " ^ + x ^ "::" ^ y ^ " -> " ^ (to_str 3 e3)) + | Fun (_, _, _) -> (10, "") + (* (2, "fun " ^ x ^ " : " ^ (string_of_type ty) ^ " -> " ^ (to_str 0 e)) *) + | Rec (_, _, _) -> (10, "") + (* (1, "rec " ^ x ^ " : " ^ (string_of_type ty) ^ " is " ^ (to_str 0 e)) *) in if m > n then str else "(" ^ str ^ ")" @@ -112,7 +112,7 @@ let rec subst s = function | Rec (x, ty, e) -> let s' = List.remove_assoc x s in Rec (x, ty, subst s' e) | Match (e1, ty, e2, x, y, e3) -> let s' = List.remove_assoc y (List.remove_assoc x s) in - Match (subst s e1, ty, subst s e2, x, y, subst s' e3) + Match (subst s e1, ty, subst s e2, x, y, subst s' e3) | Apply (e1, e2) -> Apply (subst s e1, subst s e2) | Pair (e1, e2) -> Pair (subst s e1, subst s e2) | Fst e -> Fst (subst s e) diff --git a/src/minihaskell/type_check.ml b/src/minihaskell/type_check.ml index c53887a..d8981b9 100644 --- a/src/minihaskell/type_check.ml +++ b/src/minihaskell/type_check.ml @@ -20,7 +20,7 @@ and type_of ctx = function | Syntax.Var x -> (try List.assoc x ctx with - Not_found -> type_error "unknown identifier %s" x) + Not_found -> type_error "unknown identifier %s" x) | Syntax.Int _ -> Syntax.TInt @@ -71,7 +71,7 @@ and type_of ctx = function | Syntax.If (e1, e2, e3) -> check ctx Syntax.TBool e1 ; let ty = type_of ctx e2 in - check ctx ty e3 ; ty + check ctx ty e3 ; ty | Syntax.Fun (x, ty, e) -> Syntax.TArrow (ty, type_of ((x,ty)::ctx) e) @@ -83,20 +83,20 @@ and type_of ctx = function | Syntax.Match (e1, ty, e2, x, y, e3) -> (match type_of ctx e1 with | Syntax.TList _ -> - check ctx (Syntax.TList ty) e1; - let ty2 = type_of ctx e2 in - check ((x,ty)::(y, Syntax.TList ty)::ctx) ty2 e3 ; ty2 + check ctx (Syntax.TList ty) e1; + let ty2 = type_of ctx e2 in + check ((x,ty)::(y, Syntax.TList ty)::ctx) ty2 e3 ; ty2 | ty -> type_error "%s is used as a list but its type is %s" (Syntax.string_of_expr e1) - (Syntax.string_of_type ty)) + (Syntax.string_of_type ty)) | Syntax.Apply (e1, e2) -> (match type_of ctx e1 with | Syntax.TArrow (ty1, ty2) -> check ctx ty1 e2 ; ty2 | ty -> - type_error "%s is used as a function but its type is %s" + type_error "%s is used as a function but its type is %s" Syntax.(string_of_expr e1) - (Syntax.string_of_type ty)) + (Syntax.string_of_type ty)) | Syntax.Pair (e1, e2) -> Syntax.TTimes (type_of ctx e1, type_of ctx e2) @@ -105,7 +105,7 @@ and type_of ctx = function (match type_of ctx e with | Syntax.TTimes (ty1, _) -> ty1 | ty -> - type_error "%s is used as a pair but its type is %s" + type_error "%s is used as a pair but its type is %s" (Syntax.string_of_expr e) (Syntax.string_of_type ty)) @@ -113,6 +113,6 @@ and type_of ctx = function (match type_of ctx e with | Syntax.TTimes (_, ty2) -> ty2 | ty -> - type_error "%s is used as a pair but its type is %s" + type_error "%s is used as a pair but its type is %s" (Syntax.string_of_expr e) - (Syntax.string_of_type ty)) + (Syntax.string_of_type ty)) diff --git a/src/miniml/lexer.mll b/src/miniml/lexer.mll index c3a910f..e58b9e7 100644 --- a/src/miniml/lexer.mll +++ b/src/miniml/lexer.mll @@ -17,7 +17,7 @@ rule token = parse | "if" { IF } | "then" { THEN } | "else" { ELSE } - | "let" { LET } + | "let" { LET } | ";;" { SEMISEMI } | '=' { EQUAL } | '<' { LESS } diff --git a/src/miniml/machine.ml b/src/miniml/machine.ml index 7ccb82d..0d26f18 100644 --- a/src/miniml/machine.ml +++ b/src/miniml/machine.ml @@ -48,9 +48,9 @@ and instr = | ISub (** subtraction *) | IEqual (** equality *) | ILess (** less than *) - | IVar of name (** push value of variable *) - | IInt of int (** push integer constant *) - | IBool of bool (** push boolean constant *) + | IVar of name (** push value of variable *) + | IInt of int (** push integer constant *) + | IBool of bool (** push boolean constant *) | IClosure of name * name * frame (** push closure *) | IBranch of frame * frame (** branch *) | ICall (** execute a closure *) @@ -143,22 +143,22 @@ let exec instr frms stck envs = | IInt k -> (frms, (MInt k) :: stck, envs) | IBool b -> (frms, (MBool b) :: stck, envs) | IClosure (f, x, frm) -> - (match envs with - env :: _ -> - let rec c = MClosure (x, frm, (f,c) :: env) in - (frms, c :: stck, envs) - | [] -> error "no environment for a closure") + (match envs with + env :: _ -> + let rec c = MClosure (x, frm, (f,c) :: env) in + (frms, c :: stck, envs) + | [] -> error "no environment for a closure") (* Control instructions *) | IBranch (f1, f2) -> - let (b, stck') = pop_bool stck in - ((if b then f1 else f2) :: frms, stck', envs) + let (b, stck') = pop_bool stck in + ((if b then f1 else f2) :: frms, stck', envs) | ICall -> - let (x, frm, env, v, stck') = pop_app stck in - (frm :: frms, stck', ((x,v) :: env) :: envs) + let (x, frm, env, v, stck') = pop_app stck in + (frm :: frms, stck', ((x,v) :: env) :: envs) | IPopEnv -> - (match envs with - [] -> error "no environment to pop" - | _ :: envs' -> (frms, stck, envs')) + (match envs with + [] -> error "no environment to pop" + | _ :: envs' -> (frms, stck, envs')) (** [run frm env] executes the frame [frm] in environment [env]. *) let run frm env = diff --git a/src/miniml/miniml.ml b/src/miniml/miniml.ml index 2d7732b..0e7dd5e 100644 --- a/src/miniml/miniml.ml +++ b/src/miniml/miniml.ml @@ -32,7 +32,7 @@ module MiniML = Zoo.Main (struct (ctx, env) | Syntax.Def (x, e) -> (* check the type of [e], compile it, run it, and return a new - context-environemtn pair with [x] defined as [e]. *) + context-environemtn pair with [x] defined as [e]. *) let ty = Type_check.type_of ctx e in let frm = Compile.compile e in let v = Machine.run frm env in diff --git a/src/miniml/parser.mly b/src/miniml/parser.mly index dc47e01..dade4c4 100644 --- a/src/miniml/parser.mly +++ b/src/miniml/parser.mly @@ -63,7 +63,7 @@ plain_expr: { e } | MINUS n = INT { Int (-n) } - | e1 = expr PLUS e2 = expr + | e1 = expr PLUS e2 = expr { Plus (e1, e2) } | e1 = expr MINUS e2 = expr { Minus (e1, e2) } @@ -89,14 +89,14 @@ simple_expr: mark_position(plain_simple_expr) { $1 } plain_simple_expr: | x = VAR { Var x } - | TRUE + | TRUE { Bool true } | FALSE { Bool false } | n = INT { Int n } - | LPAREN e = plain_expr RPAREN - { e } + | LPAREN e = plain_expr RPAREN + { e } ty: | TBOOL diff --git a/src/miniml/syntax.ml b/src/miniml/syntax.ml index 9737f7d..6d8e442 100644 --- a/src/miniml/syntax.ml +++ b/src/miniml/syntax.ml @@ -12,17 +12,17 @@ type ty = (* Expressions *) type expr = expr' Zoo.located and expr' = - | Var of name (* Variable *) - | Int of int (* Non-negative integer constant *) - | Bool of bool (* Boolean constant *) - | Times of expr * expr (* Product [e1 * e2] *) - | Plus of expr * expr (* Sum [e1 + e2] *) - | Minus of expr * expr (* Difference [e1 - e2] *) - | Equal of expr * expr (* Integer comparison [e1 = e2] *) - | Less of expr * expr (* Integer comparison [e1 < e2] *) - | If of expr * expr * expr (* Conditional [if e1 then e2 else e3] *) + | Var of name (* Variable *) + | Int of int (* Non-negative integer constant *) + | Bool of bool (* Boolean constant *) + | Times of expr * expr (* Product [e1 * e2] *) + | Plus of expr * expr (* Sum [e1 + e2] *) + | Minus of expr * expr (* Difference [e1 - e2] *) + | Equal of expr * expr (* Integer comparison [e1 = e2] *) + | Less of expr * expr (* Integer comparison [e1 < e2] *) + | If of expr * expr * expr (* Conditional [if e1 then e2 else e3] *) | Fun of name * name * ty * ty * expr (* Function [fun f(x:s):t is e] *) - | Apply of expr * expr (* Application [e1 e2] *) + | Apply of expr * expr (* Application [e1 e2] *) (* Toplevel commands *) type command = diff --git a/src/miniml/type_check.ml b/src/miniml/type_check.ml index 9c1f5ac..a0bfdf4 100644 --- a/src/miniml/type_check.ml +++ b/src/miniml/type_check.ml @@ -22,7 +22,7 @@ and type_of ctx {Zoo.data=e; loc} = match e with | Var x -> (try List.assoc x ctx with - Not_found -> typing_error ~loc "unknown variable %s" x) + Not_found -> typing_error ~loc "unknown variable %s" x) | Int _ -> TInt | Bool _ -> TBool | Times (e1, e2) -> check ctx TInt e1 ; check ctx TInt e2 ; TInt @@ -33,14 +33,14 @@ and type_of ctx {Zoo.data=e; loc} = | If (e1, e2, e3) -> check ctx TBool e1 ; let ty = type_of ctx e2 in - check ctx ty e3 ; ty + check ctx ty e3 ; ty | Fun (f, x, ty1, ty2, e) -> check ((f, TArrow(ty1,ty2)) :: (x, ty1) :: ctx) ty2 e ; TArrow (ty1, ty2) | Apply (e1, e2) -> begin match type_of ctx e1 with - TArrow (ty1, ty2) -> check ctx ty1 e2 ; ty2 - | ty -> - typing_error ~loc + TArrow (ty1, ty2) -> check ctx ty1 e2 ; ty2 + | ty -> + typing_error ~loc "this expression is used as a function but its type is %t" (Print.ty ty) end diff --git a/src/miniml_error/lexer.mll b/src/miniml_error/lexer.mll index 3315ce8..88ee9d4 100644 --- a/src/miniml_error/lexer.mll +++ b/src/miniml_error/lexer.mll @@ -17,7 +17,7 @@ rule token = parse | "if" { IF } | "then" { THEN } | "else" { ELSE } - | "let" { LET } + | "let" { LET } | ";;" { SEMISEMI } | '=' { EQUAL } | '<' { LESS } diff --git a/src/miniml_error/machine.ml b/src/miniml_error/machine.ml index 3cd6c41..941a086 100644 --- a/src/miniml_error/machine.ml +++ b/src/miniml_error/machine.ml @@ -58,9 +58,9 @@ and instr = | ISub (** subtraction *) | IEqual (** equality *) | ILess (** less than *) - | IVar of name (** push value of variable *) - | IInt of int (** push integer constant *) - | IBool of bool (** push boolean constant *) + | IVar of name (** push value of variable *) + | IInt of int (** push integer constant *) + | IBool of bool (** push boolean constant *) | IClosure of name * name * frame (** push closure *) | IBranch of frame * frame (** branch *) | ICall (** execute a closure *) @@ -165,22 +165,22 @@ let exec instr frms stck envs = | IInt k -> (frms, (MInt k) :: stck, envs) | IBool b -> (frms, (MBool b) :: stck, envs) | IClosure (f, x, frm) -> - (match envs with - env :: _ -> - let rec c = MClosure (x, frm, (f,c) :: env) in - (frms, c :: stck, envs) - | [] -> error "no environment for a closure") + (match envs with + env :: _ -> + let rec c = MClosure (x, frm, (f,c) :: env) in + (frms, c :: stck, envs) + | [] -> error "no environment for a closure") (* Control instructions *) | IBranch (f1, f2) -> - let (b, stck') = pop_bool stck in - ((if b then f1 else f2) :: frms, stck', envs) + let (b, stck') = pop_bool stck in + ((if b then f1 else f2) :: frms, stck', envs) | ICall -> - let (x, frm, env, v, stck') = pop_app stck in - (frm :: frms, stck', ((x,v) :: env) :: envs) + let (x, frm, env, v, stck') = pop_app stck in + (frm :: frms, stck', ((x,v) :: env) :: envs) | IPopEnv -> - (match envs with - [] -> error "no environment to pop" - | _ :: envs' -> (frms, stck, envs')) + (match envs with + [] -> error "no environment to pop" + | _ :: envs' -> (frms, stck, envs')) (** [run frm env] executes the frame [frm] in environment [env]. *) let run frm env = diff --git a/src/miniml_error/parser.mly b/src/miniml_error/parser.mly index f71c1f8..3077519 100644 --- a/src/miniml_error/parser.mly +++ b/src/miniml_error/parser.mly @@ -64,7 +64,7 @@ plain_expr: { e } | MINUS n = INT { Int (-n) } - | e1 = expr PLUS e2 = expr + | e1 = expr PLUS e2 = expr { Plus (e1, e2) } | e1 = expr MINUS e2 = expr { Minus (e1, e2) } @@ -92,14 +92,14 @@ simple_expr: mark_position(plain_simple_expr) { $1 } plain_simple_expr: | x = VAR { Var x } - | TRUE + | TRUE { Bool true } | FALSE { Bool false } | n = INT { Int n } - | LPAREN e = plain_expr RPAREN - { e } + | LPAREN e = plain_expr RPAREN + { e } ty: | TBOOL diff --git a/src/miniml_error/syntax.ml b/src/miniml_error/syntax.ml index 01e7fba..432c491 100644 --- a/src/miniml_error/syntax.ml +++ b/src/miniml_error/syntax.ml @@ -12,18 +12,18 @@ type ty = (* Expressions *) type expr = expr' Zoo.located and expr' = - | Var of name (* Variable *) - | Int of int (* Non-negative integer constant *) - | Bool of bool (* Boolean constant *) - | Times of expr * expr (* Product [e1 * e2] *) - | Plus of expr * expr (* Sum [e1 + e2] *) - | Minus of expr * expr (* Difference [e1 - e2] *) + | Var of name (* Variable *) + | Int of int (* Non-negative integer constant *) + | Bool of bool (* Boolean constant *) + | Times of expr * expr (* Product [e1 * e2] *) + | Plus of expr * expr (* Sum [e1 + e2] *) + | Minus of expr * expr (* Difference [e1 - e2] *) | Division of expr * expr (* Division [e1/e2], may result in [Abort] *) - | Equal of expr * expr (* Integer comparison [e1 = e2] *) - | Less of expr * expr (* Integer comparison [e1 < e2] *) - | If of expr * expr * expr (* Conditional [if e1 then e2 else e3] *) + | Equal of expr * expr (* Integer comparison [e1 = e2] *) + | Less of expr * expr (* Integer comparison [e1 < e2] *) + | If of expr * expr * expr (* Conditional [if e1 then e2 else e3] *) | Fun of name * name * ty * ty * expr (* Function [fun f(x:s):t is e] *) - | Apply of expr * expr (* Application [e1 e2] *) + | Apply of expr * expr (* Application [e1 e2] *) | Abort (* Special value indicating an error *) (* Toplevel commands *) diff --git a/src/miniprolog/README.md b/src/miniprolog/README.md index 586daa1..556ccf5 100644 --- a/src/miniprolog/README.md +++ b/src/miniprolog/README.md @@ -63,4 +63,4 @@ Sample session, see also the file `example.miniprolog`. B = leia more? (y/n) [y] y No - miniProlog> + miniProlog> diff --git a/src/miniprolog/solve.ml b/src/miniprolog/solve.ml index 8501fc8..8caeb94 100644 --- a/src/miniprolog/solve.ml +++ b/src/miniprolog/solve.ml @@ -40,10 +40,10 @@ let rec display_solution ch env = | "Yes", _ -> Zoo.print_info "Yes@." | answer, [] -> Zoo.print_info "%s@." answer | answer, ch -> begin - Zoo.print_info "%s@.more? (y/n) [y]@?" answer; - match read_line () with - | "y" | "yes" | "Y" | "YES" | "Yes" | "" -> continue_search ch - | _ -> raise NoSolution + Zoo.print_info "%s@.more? (y/n) [y]@?" answer; + match read_line () with + | "y" | "yes" | "Y" | "YES" | "Yes" | "" -> continue_search ch + | _ -> raise NoSolution end (** [continue_search ch] looks for other answers. It accepts a list of @@ -76,28 +76,28 @@ and solve ch asrl env c n = let rec reduce_atom a = function | [] -> None | (b,lst)::asrl' -> - (try - let env' = Unify.unify_atoms env a (renumber_atom n b) in - Some (asrl', env', List.map (renumber_atom n) lst) - with Unify.NoUnify -> reduce_atom a asrl') + (try + let env' = Unify.unify_atoms env a (renumber_atom n b) in + Some (asrl', env', List.map (renumber_atom n) lst) + with Unify.NoUnify -> reduce_atom a asrl') in match c with | [] -> - (* All atoms are solved, we found a solution. *) - display_solution ch env + (* All atoms are solved, we found a solution. *) + display_solution ch env | a::c' -> - (* Reduce the first atom in the clause. *) - (match reduce_atom a asrl with - | None -> - (* This clause cannot be solved, look for other solutions. *) - continue_search ch - | Some (asrl', env', d) -> - (* The atom was reduced to subgoals [d]. Continue - search with the subgoals added to the list of - goals. *) - let ch' = (asrl', env, c, n)::ch (* Add a new choice. *) - in - solve ch' !base env' (d @ c') (n+1)) + (* Reduce the first atom in the clause. *) + (match reduce_atom a asrl with + | None -> + (* This clause cannot be solved, look for other solutions. *) + continue_search ch + | Some (asrl', env', d) -> + (* The atom was reduced to subgoals [d]. Continue + search with the subgoals added to the list of + goals. *) + let ch' = (asrl', env, c, n)::ch (* Add a new choice. *) + in + solve ch' !base env' (d @ c') (n+1)) (** [solve_toplevel c] searches for the proof of clause [c] using the global databased [!base]. This function is called from the main diff --git a/src/miniprolog/syntax.ml b/src/miniprolog/syntax.ml index 7069e80..1da4a09 100644 --- a/src/miniprolog/syntax.ml +++ b/src/miniprolog/syntax.ml @@ -57,7 +57,7 @@ let lookup env x = let rec subst_term env = function | Var x as e -> (let e' = lookup env x in - if e = e' then e' else subst_term env e') + if e = e' then e' else subst_term env e') | Const _ as e -> e | App (c, ls) -> App (c, List.map (subst_term env) ls) @@ -76,10 +76,10 @@ let string_of_env env = match List.filter (fun ((_, n), _) -> n = 0) env with | [] -> "Yes" | env' -> String.concat "\n" - (List.map - (fun ((x, _), e) -> - x ^ " = " ^ string_of_term (subst_term env e)) - (List.rev env')) + (List.map + (fun ((x, _), e) -> + x ^ " = " ^ string_of_term (subst_term env e)) + (List.rev env')) (** [occurs x t] returns [true] when variable instance [x] appears in term [t]. *) diff --git a/src/miniprolog/unify.ml b/src/miniprolog/unify.ml index 8eff810..b335c05 100644 --- a/src/miniprolog/unify.ml +++ b/src/miniprolog/unify.ml @@ -12,10 +12,10 @@ let rec unify_terms env t1 t2 = match subst_term env t1, subst_term env t2 with | t1, t2 when t1 = t2 -> env | (Var y, t) | (t, Var y) -> - if occurs y t then - raise NoUnify - else - (y,t) :: env + if occurs y t then + raise NoUnify + else + (y,t) :: env | Const _, _ -> raise NoUnify | App (c1, ts1), App (c2, ts2) when c1 = c2 -> unify_lists env ts1 ts2 | App _, _ -> raise NoUnify diff --git a/src/poly/example.poly b/src/poly/example.poly index ac9ec07..46556be 100644 --- a/src/poly/example.poly +++ b/src/poly/example.poly @@ -13,8 +13,8 @@ let append = rec append is fun lst1 => fun lst2 => match lst1 with - [] => lst2 - | x::xs => x :: (append xs lst2) + [] => lst2 + | x::xs => x :: (append xs lst2) ;; # fold_left f x0 (x1::x2::...::xn) = f(f(f(...f(x0 x1) x2) x3)...) @@ -29,8 +29,8 @@ let fold_left = let flatten = rec flatten is fun lsts => match lsts with - [] => [] - | l :: ls => append l (flatten ls) + [] => [] + | l :: ls => append l (flatten ls) ;; let zip2 = rec zip2 is @@ -38,13 +38,13 @@ let zip2 = rec zip2 is match l1 with [] => l2 | x::xs => x :: (match l2 with - [] => xs - | y::ys => y::(zip2 xs ys)) + [] => xs + | y::ys => y::(zip2 xs ys)) ;; # zip let zip = rec zip is fun lsts => match lsts with - [] => [] + [] => [] | l::ls => zip2 l (zip ls) diff --git a/src/poly/interpret.ml b/src/poly/interpret.ml index 228c7d4..49d50a9 100644 --- a/src/poly/interpret.ml +++ b/src/poly/interpret.ml @@ -17,75 +17,75 @@ let runtime_error msg = raise (Runtime_error msg) let rec interp env = function | Var x -> (try - let r = List.assoc x env in - match !r with - VClosure (env', e) -> let v = interp env' e in r := v ; v - | v -> v + let r = List.assoc x env in + match !r with + VClosure (env', e) -> let v = interp env' e in r := v ; v + | v -> v with - Not_found -> runtime_error ("Unknown variable " ^ x)) + Not_found -> runtime_error ("Unknown variable " ^ x)) | Int k -> VInt k | Bool b -> VBool b | Times (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt k1, VInt k2 -> VInt (k1 * k2) - | _ -> runtime_error "Integers expected in multiplication") + | VInt k1, VInt k2 -> VInt (k1 * k2) + | _ -> runtime_error "Integers expected in multiplication") | Divide (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt _, VInt 0 -> runtime_error ("Division by 0") - | VInt k1, VInt k2 -> VInt (k1 / k2) - | _ -> runtime_error "Integers expected in division") + | VInt _, VInt 0 -> runtime_error ("Division by 0") + | VInt k1, VInt k2 -> VInt (k1 / k2) + | _ -> runtime_error "Integers expected in division") | Mod (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt _, VInt 0 -> runtime_error ("Division by 0") - | VInt k1, VInt k2 -> VInt (k1 mod k2) - | _ -> runtime_error "Integers expected in remainder") + | VInt _, VInt 0 -> runtime_error ("Division by 0") + | VInt k1, VInt k2 -> VInt (k1 mod k2) + | _ -> runtime_error "Integers expected in remainder") | Plus (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt k1, VInt k2 -> VInt (k1 + k2) - | _ -> runtime_error "Integers expected in addition") + | VInt k1, VInt k2 -> VInt (k1 + k2) + | _ -> runtime_error "Integers expected in addition") | Minus (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt k1, VInt k2 -> VInt (k1 - k2) - | _ -> runtime_error "Integers expected in subtraction") + | VInt k1, VInt k2 -> VInt (k1 - k2) + | _ -> runtime_error "Integers expected in subtraction") | Equal (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt k1, VInt k2 -> VBool (k1 = k2) - | _ -> runtime_error "Integers expected in =") + | VInt k1, VInt k2 -> VBool (k1 = k2) + | _ -> runtime_error "Integers expected in =") | Less (e1, e2) -> (match (interp env e1), (interp env e2) with - | VInt k1, VInt k2 -> VBool (k1 < k2) - | _ -> runtime_error "Integers expected in <") + | VInt k1, VInt k2 -> VBool (k1 < k2) + | _ -> runtime_error "Integers expected in <") | If (e1, e2, e3) -> (match interp env e1 with - | VBool true -> interp env e2 - | VBool false -> interp env e3 - | _ -> runtime_error "Boolean expected in if") + | VBool true -> interp env e2 + | VBool false -> interp env e3 + | _ -> runtime_error "Boolean expected in if") | Fun _ as e -> VClosure (env, e) | Apply (e1, e2) -> (match interp env e1 with - | VClosure (env', Fun (x, e)) -> - interp ((x, ref (VClosure (env, e2)))::env') e - | _ -> runtime_error "Function expected in application") + | VClosure (env', Fun (x, e)) -> + interp ((x, ref (VClosure (env, e2)))::env') e + | _ -> runtime_error "Function expected in application") | Pair _ as e -> VClosure (env, e) | Fst e -> (match interp env e with - | VClosure (env', Pair (e1, _)) -> interp env' e1 - | _ -> runtime_error "Pair expected in fst") + | VClosure (env', Pair (e1, _)) -> interp env' e1 + | _ -> runtime_error "Pair expected in fst") | Snd e -> (match interp env e with - | VClosure (env', Pair (_, e2)) -> interp env' e2 - | _ -> runtime_error "Pair expected in snd") + | VClosure (env', Pair (_, e2)) -> interp env' e2 + | _ -> runtime_error "Pair expected in snd") | Rec (x, e) -> let rec env' = (x,ref (VClosure (env',e))) :: env in - interp env' e + interp env' e | Nil -> VNil | Cons _ as e -> VClosure (env, e) | Match (e1, e2, x, y, e3) -> (match interp env e1 with - | VNil -> interp env e2 - | VClosure (env', Cons (d1, d2)) -> - interp ((x,ref (VClosure(env',d1)))::(y,ref (VClosure(env',d2)))::env) e3 - | _ -> runtime_error "List expected in match") + | VNil -> interp env e2 + | VClosure (env', Cons (d1, d2)) -> + interp ((x,ref (VClosure(env',d1)))::(y,ref (VClosure(env',d2)))::env) e3 + | _ -> runtime_error "List expected in match") (** [print_result n v] prints at most [n] nodes of the value [v]. *) @@ -98,19 +98,19 @@ let rec print_result n v = | VBool b -> print_string (string_of_bool b) | VNil -> print_string "[]" | VClosure (env, Pair (e1, e2)) -> - print_char '(' ; - print_result (n/2) (interp env e1) ; - print_string ", " ; - print_result (n/2) (interp env e2) ; - print_char ')' + print_char '(' ; + print_result (n/2) (interp env e1) ; + print_string ", " ; + print_result (n/2) (interp env e2) ; + print_char ')' | VClosure (env, Cons (e1, e2)) -> - let v1 = interp env e1 in - (match v1 with - VClosure (_, Cons _) -> - print_char '(' ; print_result (n/2) v1 ; print_char ')' - | _ -> print_result (n/2) v1) ; - print_string " :: " ; - print_result (n-1) (interp env e2) + let v1 = interp env e1 in + (match v1 with + VClosure (_, Cons _) -> + print_char '(' ; print_result (n/2) v1 ; print_char ')' + | _ -> print_result (n/2) v1) ; + print_string " :: " ; + print_result (n-1) (interp env e2) | VClosure (_, Fun _) -> print_string "" | _ -> print_string "?" ) ; diff --git a/src/poly/lexer.mll b/src/poly/lexer.mll index 28648dc..ede0e89 100644 --- a/src/poly/lexer.mll +++ b/src/poly/lexer.mll @@ -16,7 +16,7 @@ rule token = parse | "fun" { FUN } | "if" { IF } | "is" { IS } - | "let" { LET } + | "let" { LET } | "match" { MATCH } | "rec" { REC } | "snd" { SND } diff --git a/src/poly/parser.mly b/src/poly/parser.mly index 7385275..0da9f7e 100644 --- a/src/poly/parser.mly +++ b/src/poly/parser.mly @@ -66,7 +66,7 @@ expr: | arith { $1 } | boolean { $1 } | expr CONS expr { Cons ($1, $3) } - | IF expr THEN expr ELSE expr { If ($2, $4, $6) } + | IF expr THEN expr ELSE expr { If ($2, $4, $6) } | FUN VAR DARROW expr { Fun ($2, $4) } | REC VAR IS expr { Rec ($2, $4) } | MATCH expr WITH nil DARROW expr ALTERNATIVE VAR CONS VAR DARROW expr @@ -79,21 +79,21 @@ app: | non_app non_app { Apply ($1, $2) } non_app: - VAR { Var $1 } - | TRUE { Bool true } - | FALSE { Bool false } - | INT { Int $1 } + VAR { Var $1 } + | TRUE { Bool true } + | FALSE { Bool false } + | INT { Int $1 } | nil { Nil } - | LPAREN expr RPAREN { $2 } + | LPAREN expr RPAREN { $2 } | LPAREN expr COMMA expr RPAREN { Pair ($2, $4) } arith: | MINUS INT { Int (-$2) } - | expr PLUS expr { Plus ($1, $3) } - | expr MINUS expr { Minus ($1, $3) } - | expr TIMES expr { Times ($1, $3) } - | expr DIVIDE expr { Divide ($1, $3) } - | expr MOD expr { Mod ($1, $3) } + | expr PLUS expr { Plus ($1, $3) } + | expr MINUS expr { Minus ($1, $3) } + | expr TIMES expr { Times ($1, $3) } + | expr DIVIDE expr { Divide ($1, $3) } + | expr MOD expr { Mod ($1, $3) } nil: LBRACK RBRACK { () } diff --git a/src/poly/syntax.ml b/src/poly/syntax.ml index ef9ffd4..db55d63 100644 --- a/src/poly/syntax.ml +++ b/src/poly/syntax.ml @@ -48,20 +48,20 @@ let rename ty = | TInt -> TInt, c | TBool -> TBool, c | TParam k -> - (try - TParam (List.assoc k s), c - with - Not_found -> TParam j, (j+1, (k, j)::s)) + (try + TParam (List.assoc k s), c + with + Not_found -> TParam j, (j+1, (k, j)::s)) | TArrow (t1, t2) -> - let u1, c' = ren c t1 in - let u2, c'' = ren c' t2 in - TArrow (u1,u2), c'' + let u1, c' = ren c t1 in + let u2, c'' = ren c' t2 in + TArrow (u1,u2), c'' | TTimes (t1, t2) -> - let u1, c' = ren c t1 in - let u2, c'' = ren c' t2 in - TTimes (u1,u2), c'' + let u1, c' = ren c t1 in + let u2, c'' = ren c' t2 in + TTimes (u1,u2), c'' | TList t -> - let u, c' = ren c t in TList u, c' + let u, c' = ren c t in TList u, c' in fst (ren (0,[]) ty) @@ -75,18 +75,18 @@ let rename2 t1 t2 = (** [string_of_type] converts a Poly type to string. *) let string_of_type ty = let a = [|"a";"b";"c";"d";"e";"f";"g";"h";"i"; - "j";"k";"l";"m";"n";"o";"p";"q";"r"; - "s";"t";"u";"v";"w";"x";"y";"z"|] + "j";"k";"l";"m";"n";"o";"p";"q";"r"; + "s";"t";"u";"v";"w";"x";"y";"z"|] in let rec to_str n ty = let (m, str) = match ty with - | TInt -> (4, "int") - | TBool -> (4, "bool") - | TParam k -> (4, (if k < Array.length a then "'" ^ a.(k) else "'ty" ^ string_of_int k)) - | TList ty -> (3, to_str 3 ty ^ " list") - | TTimes (ty1, ty2) -> (2, (to_str 2 ty1) ^ " * " ^ (to_str 2 ty2)) - | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2)) + | TInt -> (4, "int") + | TBool -> (4, "bool") + | TParam k -> (4, (if k < Array.length a then "'" ^ a.(k) else "'ty" ^ string_of_int k)) + | TList ty -> (3, to_str 3 ty ^ " list") + | TTimes (ty1, ty2) -> (2, (to_str 2 ty1) ^ " * " ^ (to_str 2 ty2)) + | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2)) in if m > n then str else "(" ^ str ^ ")" in @@ -97,33 +97,33 @@ let string_of_expr e = let rec to_str n e = let (m, str) = match e with - Int n -> (10, string_of_int n) - | Bool b -> (10, string_of_bool b) - | Var x -> (10, x) - | Pair (e1, e2) -> (10, "(" ^ (to_str 0 e1) ^ ", " ^ (to_str 0 e2) ^ ")") - | Nil -> (10, "[]") - | Fst e -> (9, "fst " ^ (to_str 9 e)) - | Snd e -> (9, "snd " ^ (to_str 9 e)) - | Apply (_, _) -> (10, "") - (* (9, (to_str 8 e1) ^ " " ^ (to_str 9 e2)) *) - | Times (e1, e2) -> (8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2)) - | Divide (e1, e2) -> (8, (to_str 7 e1) ^ " / " ^ (to_str 8 e2)) - | Mod (e1, e2) -> (8, (to_str 7 e1) ^ " % " ^ (to_str 8 e2)) - | Plus (e1, e2) -> (7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2)) - | Minus (e1, e2) -> (7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2)) - | Cons (e1, e2) -> (6, (to_str 6 e1) ^ " :: " ^ (to_str 5 e2)) - | Equal (e1, e2) -> (5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2)) - | Less (e1, e2) -> (5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2)) - | If (e1, e2, e3) -> (4, "if " ^ (to_str 4 e1) ^ " then " ^ - (to_str 4 e2) ^ " else " ^ (to_str 4 e3)) - | Match (e1, e2, x, y, e3) -> - (3, "match " ^ (to_str 3 e1) ^ " with " ^ - "[] -> " ^ (to_str 3 e2) ^ " | " ^ - x ^ "::" ^ y ^ " -> " ^ (to_str 3 e3)) - | Fun (_, _) -> (10, "") - (* (2, "fun " ^ x ^ " -> " ^ (to_str 0 e)) *) - | Rec (_, _) -> (10, "") - (* (1, "rec " ^ x ^ " is " ^ (to_str 0 e)) *) + Int n -> (10, string_of_int n) + | Bool b -> (10, string_of_bool b) + | Var x -> (10, x) + | Pair (e1, e2) -> (10, "(" ^ (to_str 0 e1) ^ ", " ^ (to_str 0 e2) ^ ")") + | Nil -> (10, "[]") + | Fst e -> (9, "fst " ^ (to_str 9 e)) + | Snd e -> (9, "snd " ^ (to_str 9 e)) + | Apply (_, _) -> (10, "") + (* (9, (to_str 8 e1) ^ " " ^ (to_str 9 e2)) *) + | Times (e1, e2) -> (8, (to_str 7 e1) ^ " * " ^ (to_str 8 e2)) + | Divide (e1, e2) -> (8, (to_str 7 e1) ^ " / " ^ (to_str 8 e2)) + | Mod (e1, e2) -> (8, (to_str 7 e1) ^ " % " ^ (to_str 8 e2)) + | Plus (e1, e2) -> (7, (to_str 6 e1) ^ " + " ^ (to_str 7 e2)) + | Minus (e1, e2) -> (7, (to_str 6 e1) ^ " - " ^ (to_str 7 e2)) + | Cons (e1, e2) -> (6, (to_str 6 e1) ^ " :: " ^ (to_str 5 e2)) + | Equal (e1, e2) -> (5, (to_str 5 e1) ^ " = " ^ (to_str 5 e2)) + | Less (e1, e2) -> (5, (to_str 5 e1) ^ " < " ^ (to_str 5 e2)) + | If (e1, e2, e3) -> (4, "if " ^ (to_str 4 e1) ^ " then " ^ + (to_str 4 e2) ^ " else " ^ (to_str 4 e3)) + | Match (e1, e2, x, y, e3) -> + (3, "match " ^ (to_str 3 e1) ^ " with " ^ + "[] -> " ^ (to_str 3 e2) ^ " | " ^ + x ^ "::" ^ y ^ " -> " ^ (to_str 3 e3)) + | Fun (_, _) -> (10, "") + (* (2, "fun " ^ x ^ " -> " ^ (to_str 0 e)) *) + | Rec (_, _) -> (10, "") + (* (1, "rec " ^ x ^ " is " ^ (to_str 0 e)) *) in if m > n then str else "(" ^ str ^ ")" @@ -148,7 +148,7 @@ let rec subst s = function | Rec (x, e) -> let s' = List.remove_assoc x s in Rec (x, subst s' e) | Match (e1, e2, x, y, e3) -> let s' = List.remove_assoc y (List.remove_assoc x s) in - Match (subst s e1, subst s e2, x, y, subst s' e3) + Match (subst s e1, subst s e2, x, y, subst s' e3) | Apply (e1, e2) -> Apply (subst s e1, subst s e2) | Pair (e1, e2) -> Pair (subst s e1, subst s e2) | Fst e -> Fst (subst s e) diff --git a/src/poly/type_infer.ml b/src/poly/type_infer.ml index ba53ec9..3cb56e3 100644 --- a/src/poly/type_infer.ml +++ b/src/poly/type_infer.ml @@ -18,20 +18,20 @@ let refresh ty = | TInt -> TInt, s | TBool -> TBool, s | TParam k -> - (try - List.assoc k s, s - with Not_found -> let t = fresh () in t, (k,t)::s) + (try + List.assoc k s, s + with Not_found -> let t = fresh () in t, (k,t)::s) | TArrow (t1, t2) -> - let u1, s' = refresh s t1 in - let u2, s'' = refresh s' t2 in - TArrow (u1, u2), s'' + let u1, s' = refresh s t1 in + let u2, s'' = refresh s' t2 in + TArrow (u1, u2), s'' | TTimes (t1, t2) -> - let u1, s' = refresh s t1 in - let u2, s'' = refresh s' t2 in - TTimes (u1, u2), s'' + let u1, s' = refresh s t1 in + let u2, s'' = refresh s' t2 in + TTimes (u1, u2), s'' | TList t -> - let u, s' = refresh s t in - TList u, s' + let u, s' = refresh s t in + TList u, s' in fst (refresh [] ty) @@ -60,21 +60,21 @@ let solve eq = | (t1, t2) :: eq when t1 = t2 -> solve eq sbst | ((TParam k, t) :: eq | (t, TParam k) :: eq) when (not (occurs k t)) -> - let ts = tsubst [(k,t)] in - solve - (List.map (fun (ty1,ty2) -> (ts ty1, ts ty2)) eq) - ((k,t)::(List.map (fun (n, u) -> (n, ts u)) sbst)) + let ts = tsubst [(k,t)] in + solve + (List.map (fun (ty1,ty2) -> (ts ty1, ts ty2)) eq) + ((k,t)::(List.map (fun (n, u) -> (n, ts u)) sbst)) | (TTimes (u1,v1), TTimes (u2,v2)) :: eq | (TArrow (u1,v1), TArrow (u2,v2)) :: eq -> - solve ((u1,u2)::(v1,v2)::eq) sbst + solve ((u1,u2)::(v1,v2)::eq) sbst | (TList t1, TList t2) :: eq -> solve ((t1,t2) :: eq) sbst | (t1,t2)::_ -> - let u1, u2 = rename2 t1 t2 in - type_error ("The types " ^ string_of_type u1 ^ " and " ^ - string_of_type u2 ^ " are incompatible") + let u1, u2 = rename2 t1 t2 in + type_error ("The types " ^ string_of_type u1 ^ " and " ^ + string_of_type u2 ^ " are incompatible") in solve eq [] @@ -84,13 +84,13 @@ let solve eq = let constraints_of gctx = let rec cnstr ctx = function | Var x -> - (try - List.assoc x ctx, [] - with Not_found -> - (try - (* we call [refresh] here to get let-polymorphism *) - refresh (List.assoc x gctx), [] - with Not_found -> type_error ("Unknown variable " ^ x))) + (try + List.assoc x ctx, [] + with Not_found -> + (try + (* we call [refresh] here to get let-polymorphism *) + refresh (List.assoc x gctx), [] + with Not_found -> type_error ("Unknown variable " ^ x))) | Int _ -> TInt, [] @@ -103,67 +103,67 @@ let constraints_of gctx = | Mod (e1, e2) | Plus (e1, e2) | Minus (e1, e2) -> - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - TInt, (ty1,TInt) :: (ty2,TInt) :: eq1 @ eq2 + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + TInt, (ty1,TInt) :: (ty2,TInt) :: eq1 @ eq2 | Equal (e1, e2) | Less (e1, e2) -> - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - TBool, (ty1,TInt) :: (ty2,TInt) :: eq1 @ eq2 + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + TBool, (ty1,TInt) :: (ty2,TInt) :: eq1 @ eq2 | Cons (e1, e2) -> - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - let ty = TList ty1 in - ty, (ty2, ty) :: eq1 @ eq2 + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + let ty = TList ty1 in + ty, (ty2, ty) :: eq1 @ eq2 | If (e1, e2, e3) -> - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - let ty3, eq3 = cnstr ctx e3 in - ty2, (ty1, TBool) :: (ty2, ty3) :: eq1 @ eq2 @ eq3 + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + let ty3, eq3 = cnstr ctx e3 in + ty2, (ty1, TBool) :: (ty2, ty3) :: eq1 @ eq2 @ eq3 | Fun (x, e) -> - let ty1 = fresh () in - let ty2, eq = cnstr ((x,ty1)::ctx) e in - TArrow (ty1, ty2), eq + let ty1 = fresh () in + let ty2, eq = cnstr ((x,ty1)::ctx) e in + TArrow (ty1, ty2), eq | Rec (x, e) -> - let ty1 = fresh () in - let ty2, eq = cnstr ((x,ty1)::ctx) e in - ty1, (ty1, ty2) :: eq + let ty1 = fresh () in + let ty2, eq = cnstr ((x,ty1)::ctx) e in + ty1, (ty1, ty2) :: eq | Match (e1, e2, x, y, e3) -> - let ty = fresh () in - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - let ty3, eq3 = cnstr ((x,ty)::(y, TList ty)::ctx) e3 in - ty2, (ty1, TList ty) :: (ty2, ty3) :: eq1 @ eq2 @ eq3 + let ty = fresh () in + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + let ty3, eq3 = cnstr ((x,ty)::(y, TList ty)::ctx) e3 in + ty2, (ty1, TList ty) :: (ty2, ty3) :: eq1 @ eq2 @ eq3 | Apply (e1, e2) -> - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - let ty = fresh () in - ty, (ty1, TArrow (ty2,ty)) :: eq1 @ eq2 + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + let ty = fresh () in + ty, (ty1, TArrow (ty2,ty)) :: eq1 @ eq2 | Pair (e1, e2) -> - let ty1, eq1 = cnstr ctx e1 in - let ty2, eq2 = cnstr ctx e2 in - TTimes (ty1, ty2), eq1 @ eq2 + let ty1, eq1 = cnstr ctx e1 in + let ty2, eq2 = cnstr ctx e2 in + TTimes (ty1, ty2), eq1 @ eq2 | Fst e -> - let ty, eq = cnstr ctx e in - let ty1 = fresh () in - let ty2 = fresh () in - ty1, (ty, TTimes (ty1, ty2)) :: eq + let ty, eq = cnstr ctx e in + let ty1 = fresh () in + let ty2 = fresh () in + ty1, (ty, TTimes (ty1, ty2)) :: eq | Snd e -> - let ty, eq = cnstr ctx e in - let ty1 = fresh () in - let ty2 = fresh () in - ty2, (ty, TTimes (ty1, ty2)) :: eq + let ty, eq = cnstr ctx e in + let ty1 = fresh () in + let ty2 = fresh () in + ty2, (ty, TTimes (ty1, ty2)) :: eq in cnstr [] diff --git a/src/sub/eval.ml b/src/sub/eval.ml index 4c6cc44..f3c2922 100644 --- a/src/sub/eval.ml +++ b/src/sub/eval.ml @@ -17,58 +17,58 @@ let rec eval env = function | Int _ as e -> e | Plus (e1, e2) -> (match eval env e1, eval env e2 with - Int k1, Int k2 -> Int (k1 + k2) - | _, _ -> runtime_error "integers expected in addition") + Int k1, Int k2 -> Int (k1 + k2) + | _, _ -> runtime_error "integers expected in addition") | Minus (e1, e2) -> (match eval env e1, eval env e2 with - Int k1, Int k2 -> Int (k1 - k2) - | _, _ -> runtime_error "integers expected in subtraction") + Int k1, Int k2 -> Int (k1 - k2) + | _, _ -> runtime_error "integers expected in subtraction") | Times (e1, e2) -> (match eval env e1, eval env e2 with - Int k1, Int k2 -> Int (k1 * k2) - | _, _ -> runtime_error "integers expected in multiplication") + Int k1, Int k2 -> Int (k1 * k2) + | _, _ -> runtime_error "integers expected in multiplication") | Divide (e1, e2) -> (match eval env e1, eval env e2 with - Int _, Int 0 -> runtime_error "division by zero" - | Int k1, Int k2 -> Int (k1 / k2) - | _, _ -> runtime_error "integers expeced in quotient") + Int _, Int 0 -> runtime_error "division by zero" + | Int k1, Int k2 -> Int (k1 / k2) + | _, _ -> runtime_error "integers expeced in quotient") | Bool _ as e -> e | Equal (e1, e2) -> (match eval env e1, eval env e2 with - Int k1, Int k2 -> Bool (k1 = k2) - | _, _ -> runtime_error "integers expected in equality") + Int k1, Int k2 -> Bool (k1 = k2) + | _, _ -> runtime_error "integers expected in equality") | Less (e1, e2) -> (match eval env e1, eval env e2 with - Int k1, Int k2 -> Bool (k1 < k2) - | _, _ -> runtime_error "integers expected in comparison") + Int k1, Int k2 -> Bool (k1 < k2) + | _, _ -> runtime_error "integers expected in comparison") | And (e1, e2) -> (match eval env e1, eval env e2 with - Bool b1, Bool b2 -> Bool (b1 && b2) - | _, _ -> runtime_error "boolean values expected in conjunction") + Bool b1, Bool b2 -> Bool (b1 && b2) + | _, _ -> runtime_error "boolean values expected in conjunction") | Or (e1, e2) -> (match eval env e1, eval env e2 with - Bool b1, Bool b2 -> Bool (b1 || b2) - | _, _ -> runtime_error "boolean values expected in disjunction") + Bool b1, Bool b2 -> Bool (b1 || b2) + | _, _ -> runtime_error "boolean values expected in disjunction") | Not b -> (match eval env b with - Bool b -> Bool (not b) - | _ -> runtime_error "boolean values expected in negation") + Bool b -> Bool (not b) + | _ -> runtime_error "boolean values expected in negation") | If (e1, e2, e3) -> (match eval env e1 with - Bool true -> eval env e2 - | Bool false -> eval env e3 - | _ -> runtime_error "boolean value expected in conditional") + Bool true -> eval env e2 + | Bool false -> eval env e3 + | _ -> runtime_error "boolean value expected in conditional") | Fun (f, x, _, _, e) -> let rec c = Closure ((f,c)::env, x, e) in c | Closure _ as e -> e | Let (x, e1, e2) -> eval ((x, eval env e1)::env) e2 | App (e1, e2) -> (match eval env e1 with - Closure (env', x, e) -> eval ((x,eval env e2)::env') e - | _ -> runtime_error "invalid application") + Closure (env', x, e) -> eval ((x,eval env e2)::env') e + | _ -> runtime_error "invalid application") | Record rs -> Record (List.map (fun (l,e) -> (l, eval env e)) rs) | Project (e, l) -> (match eval env e with - Record vs -> eval env (snd (List.find (fun (l',_) -> l = l') vs)) - | _ -> runtime_error "record expected") + Record vs -> eval env (snd (List.find (fun (l',_) -> l = l') vs)) + | _ -> runtime_error "record expected") diff --git a/src/sub/lexer.mll b/src/sub/lexer.mll index 7ca2185..aba5ac6 100644 --- a/src/sub/lexer.mll +++ b/src/sub/lexer.mll @@ -19,7 +19,7 @@ rule token = parse | "in" { IN } | "is" { IS } | "int" { TINT } - | "let" { LET } + | "let" { LET } | "not" { NOT } | "or" { OR } | "then" { THEN } diff --git a/src/sub/parser.mly b/src/sub/parser.mly index 246925d..fe3251e 100644 --- a/src/sub/parser.mly +++ b/src/sub/parser.mly @@ -63,7 +63,7 @@ expr: | arith { $1 } | boolean { $1 } | LET VAR EQUAL expr IN expr { Let ($2, $4, $6) } - | IF expr THEN expr ELSE expr { If ($2, $4, $6) } + | IF expr THEN expr ELSE expr { If ($2, $4, $6) } | FUN VAR LPAREN VAR COLON ty RPAREN COLON ty IS expr { Fun ($2, $4, $6, $9, $11) } app: @@ -71,21 +71,21 @@ app: | non_app non_app { App ($1, $2) } non_app: - VAR { Var $1 } - | TRUE { Bool true } - | FALSE { Bool false } - | INT { Int $1 } - | LPAREN expr RPAREN { $2 } + VAR { Var $1 } + | TRUE { Bool true } + | FALSE { Bool false } + | INT { Int $1 } + | LPAREN expr RPAREN { $2 } | LBRACE RBRACE { Record [] } | LBRACE record_list RBRACE { Record $2 } | non_app PERIOD VAR { Project ($1, $3) } arith: | MINUS INT { Int (-$2) } - | expr PLUS expr { Plus ($1, $3) } - | expr MINUS expr { Minus ($1, $3) } - | expr TIMES expr { Times ($1, $3) } - | expr DIVIDE expr { Divide ($1, $3) } + | expr PLUS expr { Plus ($1, $3) } + | expr MINUS expr { Minus ($1, $3) } + | expr TIMES expr { Times ($1, $3) } + | expr DIVIDE expr { Divide ($1, $3) } boolean: | expr EQUAL expr { Equal ($1, $3) } @@ -102,8 +102,8 @@ field: | VAR EQUAL expr { ($1, $3) } ty: - TBOOL { TBool } - | TINT { TInt } + TBOOL { TBool } + | TINT { TInt } | ty TARROW ty { TArrow ($1, $3) } | LBRACE RBRACE { TRecord [] } | LBRACE trecord_list RBRACE { TRecord $2 } diff --git a/src/sub/syntax.ml b/src/sub/syntax.ml index 42afd94..dfff3a0 100644 --- a/src/sub/syntax.ml +++ b/src/sub/syntax.ml @@ -48,14 +48,14 @@ let string_of_type ty = let rec to_str n ty = let (m, str) = match ty with - | TInt -> (4, "int") - | TBool -> (4, "bool") - | TRecord ts -> - (4, "{" ^ - String.concat ", " - (List.map (fun (l,t) -> l ^ " : " ^ (to_str (-1) t)) ts) ^ - "}") - | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2)) + | TInt -> (4, "int") + | TBool -> (4, "bool") + | TRecord ts -> + (4, "{" ^ + String.concat ", " + (List.map (fun (l,t) -> l ^ " : " ^ (to_str (-1) t)) ts) ^ + "}") + | TArrow (ty1, ty2) -> (1, (to_str 1 ty1) ^ " -> " ^ (to_str 0 ty2)) in if m > n then str else "(" ^ str ^ ")" in @@ -67,7 +67,7 @@ let rec string_of_value = function | Bool b -> string_of_bool b | Record rs -> "{" ^ String.concat ", " - (List.map (fun (l,e) -> l ^ " = " ^ (string_of_value e)) rs) ^ - "}" + (List.map (fun (l,e) -> l ^ " = " ^ (string_of_value e)) rs) ^ + "}" | Closure _ -> "" | _ -> assert false diff --git a/src/sub/type_check.ml b/src/sub/type_check.ml index c0162bd..d118606 100644 --- a/src/sub/type_check.ml +++ b/src/sub/type_check.ml @@ -26,9 +26,9 @@ let lookup_type x ctx = let rec type_of ctx = function Var x -> lookup_type x ctx | Int _ -> TInt - | Plus (e1, e2) - | Minus (e1, e2) - | Times (e1, e2) + | Plus (e1, e2) + | Minus (e1, e2) + | Times (e1, e2) | Divide (e1, e2) -> check ctx e1 TInt; check ctx e2 TInt; TInt | Bool _ -> TBool | Equal (e1, e2) @@ -40,9 +40,9 @@ let rec type_of ctx = function check ctx e1 TBool; let ty2 = type_of ctx e2 in let ty3 = type_of ctx e3 in - if subtype ty2 ty3 then ty3 - else if subtype ty3 ty2 then ty2 - else type_error "incompatible types in conditional" + if subtype ty2 ty3 then ty3 + else if subtype ty3 ty2 then ty2 + else type_error "incompatible types in conditional" | Fun (f, x, ty1, ty2, e) -> check ((f, TArrow(ty1,ty2)) :: (x, ty1) :: ctx) e ty2 ; TArrow (ty1, ty2) @@ -50,17 +50,17 @@ let rec type_of ctx = function | Let (x, e1, e2) -> type_of ((x, type_of ctx e1)::ctx) e2 | App (e1, e2) -> (match type_of ctx e1 with - TArrow (ty1, ty2) -> check ctx e2 ty1; ty2 - | _ -> type_error "function expected") + TArrow (ty1, ty2) -> check ctx e2 ty1; ty2 + | _ -> type_error "function expected") | Record rs -> check_labels (List.map fst rs) ; TRecord (List.map (fun (l, e) -> (l, type_of ctx e)) rs) | Project (e, l) -> (match type_of ctx e with - TRecord ts -> - (try List.assoc l ts with - Not_found -> type_error ("no such field " ^ l)) - | _ -> type_error "record expected" ) + TRecord ts -> + (try List.assoc l ts with + Not_found -> type_error ("no such field " ^ l)) + | _ -> type_error "record expected" ) (** [check ctx e ty] checks whether [e] can be given type [ty] in context [ctx]. *) @@ -71,11 +71,11 @@ and check ctx e ty = and subtype ty1 ty2 = (ty1 = ty2) || (match ty1, ty2 with - TArrow (u1, v1), TArrow (u2, v2) -> - (subtype u2 u1) && (subtype v1 v2) + TArrow (u1, v1), TArrow (u2, v2) -> + (subtype u2 u1) && (subtype v1 v2) | TRecord ts1, TRecord ts2 -> - List.for_all - (fun (l,ty) -> List.exists (fun (l',ty') -> l = l' && subtype ty' ty) ts1) - ts2 + List.for_all + (fun (l,ty) -> List.exists (fun (l',ty') -> l = l' && subtype ty' ty) ts1) + ts2 | _, _ -> false )