Commit 93e3ff55 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Add a directive to debug the tallying.

parent e925dc34
Pipeline #183 passed with stages
in 4 minutes and 40 seconds
......@@ -162,14 +162,14 @@ let eval_quiet tenv cenv e =
Compile.compile_eval_expr cenv e
let debug ppf tenv _cenv = function
| `Subtype (t1, t2) ->
| `Subtype (t1, t2) ->
Format.fprintf ppf "[DEBUG:subtype]@.";
let t1 = Types.descr (Typer.typ tenv t1)
and t2 = Types.descr (Typer.typ tenv t2) in
let s = Types.subtype t1 t2 in
Format.fprintf ppf "%a %a %a : %b@." print_norm t1 print_protect "<="
print_norm t2 s
| `Sample t -> (
| `Sample t -> (
let open Types in
Format.fprintf ppf "[DEBUG:sample]@.";
try
......@@ -177,7 +177,7 @@ let debug ppf tenv _cenv = function
Format.fprintf ppf "%a@." print_sample (Sample.get t);
Format.fprintf ppf "witness: %a@." Types.print_witness t
with Not_found -> Format.fprintf ppf "Empty type : no sample !@.")
| `Filter (t, p) ->
| `Filter (t, p) ->
let t = Typer.typ tenv t and p = Typer.pat tenv p in
Format.fprintf ppf "[DEBUG:filter t=%a p=%a]@." Types.Print.print
(Types.descr t) Patterns.Print.print (Patterns.descr p);
......@@ -186,12 +186,12 @@ let debug ppf tenv _cenv = function
(fun x t ->
Format.fprintf ppf " %a:%a@." Ident.print x print_norm (Types.descr t))
f
| `Accept p ->
| `Accept p ->
Format.fprintf ppf "[DEBUG:accept]@.";
let p = Typer.pat tenv p in
let t = Patterns.accept p in
Format.fprintf ppf " %a@." Types.Print.print (Types.descr t)
| `Compile (t, pl) ->
| `Compile (t, pl) ->
Format.fprintf ppf "[DEBUG:compile]@.";
let no = ref (-1) in
let t = Types.descr (Typer.typ tenv t)
......@@ -212,7 +212,7 @@ let debug ppf tenv _cenv = function
| Auto_pat.Match (_, n) -> Format.fprintf ppf "Pat(%i)@." n)
rhs;
Format.fprintf ppf "@.Dispatcher:@.%a@." Print_auto.print_state state
| `Single t -> (
| `Single t -> (
Format.fprintf ppf "[DEBUG:single]@.";
let t = Typer.typ tenv t in
try
......@@ -221,6 +221,24 @@ let debug ppf tenv _cenv = function
with
| Exit -> Format.fprintf ppf "Non constant@."
| Not_found -> Format.fprintf ppf "Empty@.")
| `Tallying (delta, tlist) ->
Format.fprintf ppf "[DEBUG:tallying]@.";
let delta, vlist =
List.fold_left
(fun (acc_d, acc_v) u ->
let v = Var.mk (U.get_str u) in
(Var.Set.add v acc_d, (u, v) :: acc_v))
(Var.Set.empty, []) delta
in
let tprobs =
List.map
(fun (p1, p2) ->
( Types.descr @@ Typer.var_typ vlist tenv p1,
Types.descr @@ Typer.var_typ vlist tenv p2 ))
tlist
in
let subst = Types.Tallying.tallying delta tprobs in
Format.fprintf ppf "Result:%a@." Types.Subst.print_list subst
let flush_ppf ppf = Format.fprintf ppf "@."
......
......@@ -30,7 +30,9 @@ and debug_directive =
| `Accept of ppat
| `Compile of ppat * ppat list
| `Subtype of ppat * ppat
| `Single of ppat ]
| `Single of ppat
| `Tallying of U.t list * (ppat * ppat) list
]
and toplevel_directive =
[ `Quit
......
......@@ -103,6 +103,37 @@ let mk_app_pat loc var l =
match var.Cduce_loc.descr with
PatVar(p, []) -> mk loc (PatVar(p, l))
| _ -> parsing_error loc "invalid parametric type"
;;
let parse_pat_list err p f =
let rec loop r acc =
match r with
Elem { descr = e; _ } -> (match f e with Some x -> x :: acc | None -> err ())
| Seq (r1, r2) -> loop r2 (loop r1 acc)
| _ -> err ()
in
match p.Cduce_loc.descr with
Regexp (r) -> loop r []
| _ -> err ()
;;
let parse_poly_list loc p =
let err () =
parsing_error loc
"debug tallying expects a list of variables as first argument"
in
let l = parse_pat_list err p (function (Poly e) -> Some e | _ -> None) in
List.sort_uniq U.compare l
;;
let parse_pat_pair_list loc p =
let err () =
parsing_error loc
"debug tallying expects a finite list of pair of types as second argument"
in
parse_pat_list err p
(function Prod(p1, p2) -> Some (p1, p2) | _ -> None)
;;
%}
/* Keywords */
......@@ -302,6 +333,10 @@ match n with
| "sample", [t] -> `Sample t
| "subtype", [t1; t2] -> `Subtype (t1, t2)
| "single", [t] -> `Single t
| "tallying", [delta; plist] ->
let delta = parse_poly_list $sloc delta in
let plist = parse_pat_pair_list $sloc plist in
`Tallying (delta, plist)
| _ -> parsing_error $loc(d) (Format.sprintf "invalid debug directive %s" d)
in Directive (`Debug dir)
}
......
......@@ -24,6 +24,7 @@ val enter_type: id -> Types.t * Var.t list -> t -> t
val iter_values: t -> (id -> Types.t -> unit) -> unit
val typ: t -> Ast.ppat -> Types.Node.t
val var_typ : (Utf8.t * Var.t) list -> t -> Ast.ppat -> Types.Node.t
val pat: t -> Ast.ppat -> Patterns.node
val dump_types: Format.formatter -> t -> unit
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment