65 lines
1.6 KiB
OCaml
65 lines
1.6 KiB
OCaml
open Lam
|
|
open Types
|
|
open Proof
|
|
|
|
(* fonction d'affichage *)
|
|
let rec string_of_ty = function
|
|
TVar s -> s
|
|
| Arr(t1, t2) ->
|
|
let s1 = string_of_ty t1 in
|
|
let s2 = string_of_ty t2 in
|
|
"(" ^ s1 ^ " -> " ^ s2 ^ ")"
|
|
| Bot -> "False"
|
|
| And (t1, t2) ->
|
|
let s1 = string_of_ty t1 in
|
|
let s2 = string_of_ty t2 in
|
|
"(" ^ s1 ^ " /\\ " ^ s2 ^ ")"
|
|
| Or (t1, t2) ->
|
|
let s1 = string_of_ty t1 in
|
|
let s2 = string_of_ty t2 in
|
|
"(" ^ s1 ^ " \\/ " ^ s2 ^ ")"
|
|
| Unknown -> "Unknown"
|
|
|
|
let rec string_of_expr = function
|
|
Fun ((s, t), e) ->
|
|
let s_ty = string_of_ty t in
|
|
let s_e = string_of_expr e in
|
|
"fun (" ^ s ^ " : " ^ s_ty ^ ") => (" ^ s_e ^ ")"
|
|
| App (e1, e2) ->
|
|
"("^(string_of_expr e1)^" "^(string_of_expr e2)^")"
|
|
| Var (s) -> s
|
|
| Exf (e, t) ->
|
|
let s_e = string_of_expr e in
|
|
let s_ty = string_of_ty t in
|
|
"exf (" ^ s_e ^ " : " ^ s_ty ^ ")"
|
|
| Pair (e1, e2) ->
|
|
"Pair("^(string_of_expr e1)^", "^(string_of_expr e2)^")"
|
|
| Left e | Right e ->
|
|
"["^(string_of_expr e)^"]"
|
|
|
|
|
|
|
|
let print_ty t =
|
|
print_string (string_of_ty t)
|
|
|
|
let print_expr e =
|
|
print_string (string_of_expr e)
|
|
|
|
let print_goal ((_, ty, c) : goal) : unit =
|
|
let rec print_hyps (c : context) : unit = match c with
|
|
[] -> ()
|
|
| (hyp_id, _, _, ty)::q ->
|
|
print_string (hyp_id^" : "^(string_of_ty ty)^"\n");
|
|
print_hyps q
|
|
in
|
|
print_string "\027[1m";
|
|
print_hyps c;
|
|
print_ty ty;
|
|
print_string "\n==========\027[0m\n"
|
|
|
|
let affiche_val _ = print_string "TODO"
|
|
|
|
let print_error (error_type : string) (details : string) =
|
|
output_string stderr ("\027[1;31mError:\027[0m \027[34m"^error_type^"\027[0m "^details^"\n");
|
|
flush stderr
|