formalsec / smtml / 175

Committed 12 Jul 2024 09:10AM UTC coverage: 50.585% (+1.4%) from 49.176%

Build # 175

Build Type

push

github

Committed by

filipeom

Commit Message

Test relop simplification

Run Details

1125 of 2224 relevant lines covered (50.58%)

22.03 hits per line

Source File
Press 'n' to go to next uncovered line, 'b' for previous

28.3

/lib/value.ml

(***************************************************************************)
(* This file is part of the third-party OCaml library `smtml`.             *)
(* Copyright (C) 2023-2024 formalsec                                       *)
(*                                                                         *)
(* This program is free software: you can redistribute it and/or modify    *)
(* it under the terms of the GNU General Public License as published by    *)
(* the Free Software Foundation, either version 3 of the License, or       *)
(* (at your option) any later version.                                     *)
(*                                                                         *)
(* This program is distributed in the hope that it will be useful,         *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of          *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the           *)
(* GNU General Public License for more details.                            *)
(*                                                                         *)
(* You should have received a copy of the GNU General Public License       *)
(* along with this program.  If not, see <https://www.gnu.org/licenses/>.  *)
(***************************************************************************)

open Ty

type t =
  | True
  | False
  | Unit
  | Int of int
  | Real of float
  | Str of string
  | Num of Num.t
  | List of t list
  | App : [> `Op of string ] * t list -> t

let rec compare (v1 : t) (v2 : t) : int =
  match (v1, v2) with
  | True, True | False, False | Unit, Unit -> 0
  | False, True -> -1
  | True, False -> 1
  | Int x1, Int x2 -> Int.compare x1 x2
  | Real x1, Real x2 -> Float.compare x1 x2
  | Str x1, Str x2 -> String.compare x1 x2
  | Num x1, Num x2 -> Num.compare x1 x2
  | List l1, List l2 -> List.compare compare l1 l2
  | App (`Op op1, vs1), App (`Op op2, vs2) ->
    let c = String.compare op1 op2 in
    if c = 0 then List.compare compare vs1 vs2 else c
  | _ -> compare v1 v2

let rec equal (v1 : t) (v2 : t) : bool =
  match (v1, v2) with
  | True, True | False, False | Unit, Unit -> true
  | Int x1, Int x2 -> Int.equal x1 x2
  | Real x1, Real x2 -> x1 = x2
  | Str x1, Str x2 -> String.equal x1 x2
  | Num x1, Num x2 -> Num.equal x1 x2
  | List l1, List l2 -> List.equal equal l1 l2
  | App (`Op op1, vs1), App (`Op op2, vs2) ->
    String.equal op1 op2 && List.equal equal vs1 vs2
  | _ -> false

let rec pp (fmt : Format.formatter) (v : t) : unit =
  let open Format in
  match v with
  | True -> pp_print_string fmt "true"
  | False -> pp_print_string fmt "false"
  | Unit -> pp_print_string fmt "unit"
  | Int x -> pp_print_int fmt x
  | Real x -> fprintf fmt "%F" x
  | Num x -> Num.pp fmt x
  | Str x -> Format.fprintf fmt "%S" x
  | List l ->
    fprintf fmt "[%a]"
      (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp)
      l
  | App (`Op op, vs) ->
    fprintf fmt "%s(%a)" op
      (pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp)
      vs
  | _ -> assert false

let to_string (v : t) : string = Format.asprintf "%a" pp v

let rec to_json (v : t) : Yojson.Basic.t =
  match v with
  | True -> `Bool true
  | False -> `Bool false
  | Unit -> `String "unit"
  | Int int -> `Int int
  | Real real -> `Float real
  | Str str -> `String str
  | Num n -> Num.to_json n
  | List l -> `List (List.map to_json l)
  | App _ -> assert false

let type_of (v : t) : Ty.t =
  match v with
  | True | False -> Ty_bool
  | Unit -> Ty_unit
  | Int _ -> Ty_int
  | Real _ -> Ty_real
  | Str _ -> Ty_str
  | Num n -> Num.type_of n
  | List _ -> Ty_list
  | App _ -> Ty_app

1	(***************************************************************************)
2	(* This file is part of the third-party OCaml library `smtml`. *)
3	(* Copyright (C) 2023-2024 formalsec *)
4	(* *)
5	(* This program is free software: you can redistribute it and/or modify *)
6	(* it under the terms of the GNU General Public License as published by *)
7	(* the Free Software Foundation, either version 3 of the License, or *)
8	(* (at your option) any later version. *)
9	(* *)
10	(* This program is distributed in the hope that it will be useful, *)
11	(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
12	(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
13	(* GNU General Public License for more details. *)
14	(* *)
15	(* You should have received a copy of the GNU General Public License *)
16	(* along with this program. If not, see <https://www.gnu.org/licenses/>. *)
17	(***************************************************************************)
18
19	open Ty
20
21	type t =
22	\| True
23	\| False
24	\| Unit
25	\| Int of int
26	\| Real of float
27	\| Str of string
28	\| Num of Num.t
29	\| List of t list
30	\| App : [> `Op of string ] * t list -> t
31
32	let rec compare (v1 : t) (v2 : t) : int =
33	match (v1, v2) with	×
34	\| True, True \| False, False \| Unit, Unit -> 0	×
35	\| False, True -> -1	×
36	\| True, False -> 1	×
37	\| Int x1, Int x2 -> Int.compare x1 x2	×
38	\| Real x1, Real x2 -> Float.compare x1 x2	×
39	\| Str x1, Str x2 -> String.compare x1 x2	×
40	\| Num x1, Num x2 -> Num.compare x1 x2	×
41	\| List l1, List l2 -> List.compare compare l1 l2	×
42	\| App (`Op op1, vs1), App (`Op op2, vs2) ->	×
43	let c = String.compare op1 op2 in
44	if c = 0 then List.compare compare vs1 vs2 else c	×
45	\| _ -> compare v1 v2	×
46
47	let rec equal (v1 : t) (v2 : t) : bool =
48	match (v1, v2) with	758✔
49	\| True, True \| False, False \| Unit, Unit -> true	×
50	\| Int x1, Int x2 -> Int.equal x1 x2	328✔
51	\| Real x1, Real x2 -> x1 = x2	52✔
52	\| Str x1, Str x2 -> String.equal x1 x2	46✔
53	\| Num x1, Num x2 -> Num.equal x1 x2	227✔
54	\| List l1, List l2 -> List.equal equal l1 l2	5✔
55	\| App (`Op op1, vs1), App (`Op op2, vs2) ->	5✔
56	String.equal op1 op2 && List.equal equal vs1 vs2	5✔
57	\| _ -> false	×
58
59	let rec pp (fmt : Format.formatter) (v : t) : unit =
60	let open Format in	34✔
61	match v with
62	\| True -> pp_print_string fmt "true"	3✔
63	\| False -> pp_print_string fmt "false"	1✔
64	\| Unit -> pp_print_string fmt "unit"	×
65	\| Int x -> pp_print_int fmt x	12✔
66	\| Real x -> fprintf fmt "%F" x	2✔
67	\| Num x -> Num.pp fmt x	15✔
68	\| Str x -> Format.fprintf fmt "%S" x	1✔
69	\| List l ->	×
70	fprintf fmt "[%a]"
71	(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp)	×
72	l
73	\| App (`Op op, vs) ->	×
74	fprintf fmt "%s(%a)" op
75	(pp_print_list ~pp_sep:(fun fmt () -> pp_print_string fmt ", ") pp)	×
76	vs
77	\| _ -> assert false
78
79	let to_string (v : t) : string = Format.asprintf "%a" pp v	×
80
81	let rec to_json (v : t) : Yojson.Basic.t =
82	match v with	×
83	\| True -> `Bool true	×
84	\| False -> `Bool false	×
85	\| Unit -> `String "unit"	×
86	\| Int int -> `Int int	×
87	\| Real real -> `Float real	×
88	\| Str str -> `String str	×
89	\| Num n -> Num.to_json n	×
90	\| List l -> `List (List.map to_json l)	×
91	\| App _ -> assert false
92
93	let type_of (v : t) : Ty.t =
94	match v with	×
95	\| True \| False -> Ty_bool	×
96	\| Unit -> Ty_unit	×
97	\| Int _ -> Ty_int	×
98	\| Real _ -> Ty_real	×
99	\| Str _ -> Ty_str	×
100	\| Num n -> Num.type_of n	×
101	\| List _ -> Ty_list	×
102	\| App _ -> Ty_app	×

formalsec / smtml / 175

Source File Press 'n' to go to next uncovered line, 'b' for previous

Source File
Press 'n' to go to next uncovered line, 'b' for previous