(* Impression *) open Lo open Num let string_of_variable s = s let rec pcaml_string_of_type = function | Type_reel -> "R" | Type_bool -> "bool" | Type_nat -> "nat" | Type_fleche (a, b) -> "(" ^ pcaml_string_of_type a ^ " -> " ^ pcaml_string_of_type b ^ ")" | Type_couple (a, b) -> "(" ^ pcaml_string_of_type a ^ " * " ^ pcaml_string_of_type b ^ ")" | Type_o a -> "O " ^ pcaml_string_of_type a ^ "" let rec coq_string_of_type = function | Type_reel -> "R" | Type_bool -> "bool" | Type_nat -> "nat" | Type_fleche (a, b) -> "(" ^ coq_string_of_type a ^ " ->> " ^ coq_string_of_type b ^ ")" | Type_couple (a, b) -> "(" ^ coq_string_of_type a ^ " ** " ^ coq_string_of_type b ^ ")" | Type_o a -> "(o " ^ coq_string_of_type a ^ ")" let rec string_of_terme = function | Terme_variable v -> string_of_variable v | Terme_valeur v -> string_of_valeur v | Terme_application ( Terme_application ( Terme_valeur ( Valeur_spec ( { spec_nom_infixe = Some op; spec_scope = ty; } ) ), a ), b ) -> "(" ^ string_of_terme a ^ " " ^ op ^ " " ^ string_of_terme b ^ ")%" ^ pcaml_string_of_type ty | Terme_application (m1, m2) -> "(" ^ string_of_terme m1 ^ " " ^ string_of_terme m2 ^ ")" | Terme_couple (m1, m2) -> "(" ^ string_of_terme m1 ^ ", " ^ string_of_terme m2 ^ ")" | Terme_fst m -> "(fst " ^ string_of_terme m ^ ")" | Terme_snd m -> "(snd " ^ string_of_terme m ^ ")" | Terme_fix_det f -> "(fix " ^ f.tfd_point_fixe ^ "(" ^ f.tfd_param ^ " : " ^ pcaml_string_of_type f.tfd_ty_param ^ ") variant \"" ^ f.tfd_ordre_variant ^ "\" : " ^ pcaml_string_of_type f.tfd_ty_corps ^ " := " ^ string_of_terme f.tfd_corps ^ ")" | Terme_fix_prob f -> "(fix " ^ f.tfp_point_fixe ^ " prob \"" ^ f.tfp_ens_variant ^ "\" variant \"" ^ f.tfp_ordre_variant ^ "\" : " ^ pcaml_string_of_type f.tfp_ty_corps ^ " := " ^ string_of_expr f.tfp_corps ^ ")" | Terme_si (cond, (vt, vf)) -> "(if " ^ string_of_terme cond ^ " then " ^ string_of_terme vt ^ " else " ^ string_of_terme vf ^ ")" | Terme_egale (t1, t2) -> "(" ^ string_of_terme t1 ^ " = " ^ string_of_terme t2 ^ ")" and string_of_valeur = function | Valeur_prob e -> "(prob " ^ string_of_expr e ^ ")" | Valeur_spec x -> string_of_spec x | Valeur_lambda ((x, a), m) -> "(fun " ^ string_of_variable x ^ " : " ^ pcaml_string_of_type a ^ " => " ^ string_of_terme m ^ ")" | Valeur_reelle r -> string_of_reel r | Valeur_nat n -> string_of_naturel n | Valeur_bool true -> "true" | Valeur_bool false -> "false" and string_of_expr = function | Expr_terme m -> string_of_terme m | Expr_sample ((x, m), e) -> "sample " ^ string_of_variable x ^ " from " ^ string_of_terme m ^ " in " ^ string_of_expr e | Expr_s -> "S" and string_of_f_variable = function | Fv_resultat -> "result" (* "_" *) | Fv_flot_sortie -> "stream_out" | Fv_variable v -> string_of_variable v | Fv_var_abstr v -> string_of_f_var_abstr v and string_of_f_var_abstr (x, n) = x ^ "_" ^ string_of_int n and string_of_f_terme = function | Ft_r n -> string_of_reel n ^ "%R" | Ft_nat n -> string_of_naturel n ^ "%nat" | Ft_bool true -> "true" | Ft_bool false -> "false" | Ft_variable v -> string_of_f_variable v | Ft_spec ( { spec_nom_infixe = Some op; spec_scope = ty; }, [a; b] ) -> "(" ^ string_of_f_terme a ^ " " ^ op ^ " " ^ string_of_f_terme b ^ ")%" ^ coq_string_of_type ty | Ft_spec ({spec_nom = nom;}, l) -> "(" ^ nom ^ List.fold_left (fun a t -> a ^ " " ^ string_of_f_terme t) "" l ^ ")" | Ft_egale (a, b) -> "(" ^ string_of_f_terme a ^ " = " ^ string_of_f_terme b ^ ")" and string_of_formule = function | F_terme t -> string_of_f_terme t | F_true -> "True" | F_egale (a, b) -> "(" ^ string_of_f_terme a ^ " = " ^ string_of_f_terme b ^ ")" | F_equiv (x, t) -> "(" ^ string_of_f_variable x ^ " = true <-> " ^ string_of_f_terme t ^ ")" | F_flot_cons (s, (eps, s')) -> "(" ^ string_of_f_variable s ^ " = " ^ string_of_f_variable eps ^ "::" ^ string_of_f_variable s' ^ ")" | F_relation_carre (p, (s, (x, t))) -> "{" ^ string_of_f_variable s ^ " >> " ^ string_of_f_variable p ^ " ~> " ^ string_of_f_variable x ^ " >> " ^ string_of_f_variable t ^ "}" | F_relation_triangle (f, (x, y)) -> "(" ^ string_of_f_variable x ^ " -- " ^ string_of_f_variable f ^ " --> " ^ string_of_f_variable y ^ ")" | F_relation_croix (c, (a, b)) -> "(" ^ string_of_f_variable a ^ " << " ^ string_of_f_variable c ^ " >> " ^ string_of_f_variable b ^ ")" | F_and (f1, f2) -> "(" ^ string_of_formule f1 ^ " /\\ " ^ string_of_formule f2 ^ ")" | F_imp (f1, f2) -> "(" ^ string_of_formule f1 ^ " -> " ^ string_of_formule f2 ^ ")" | F_existe ((v, _), f) -> "(exists " ^ string_of_f_var_abstr v ^ ", " ^ string_of_formule f ^ ")" | F_pour_tout (x, f) -> "(forall " ^ string_of_f_var_abstr x ^", " ^ string_of_formule f ^ ")" | F_triangle (t, ((x, y), f)) -> "(" ^ string_of_f_variable t ^ " |> fun " ^ string_of_f_var_abstr x ^ " " ^ string_of_f_var_abstr y ^ " => " ^ string_of_formule f ^ ")" | F_croix (t, ((x, y), f)) -> "(" ^ string_of_f_variable t ^ " (X) fun " ^ string_of_f_var_abstr x ^ " " ^ string_of_f_var_abstr y ^ " => " ^ string_of_formule f ^ ")" | F_carre (t, ((s, (x, s')), f)) -> "(" ^ string_of_f_variable t ^ " [] fun " ^ string_of_f_var_abstr s ^ " " ^ string_of_f_var_abstr x ^ " " ^ string_of_f_var_abstr s' ^ " => " ^ string_of_formule f ^ ")" | F_terminaison_triangle (f, (x, phi)) -> "(Terminaison_triangle " ^ string_of_f_variable f ^ " (fun " ^ string_of_f_var_abstr x ^ " => " ^ string_of_formule phi ^ "))" | F_terminaison_carre (p, (s, phi)) -> "(Terminaison_carre " ^ string_of_f_variable p ^ " (fun " ^ string_of_f_var_abstr s ^ " => " ^ string_of_formule phi ^ "))" | F_coq ((gamma, phi), (g2, autres)) -> "((" ^ begin if gamma = [] then "" else List.fold_left (fun a (v, t) -> a ^ " (" ^ v ^ " : " ^ coq_string_of_type t ^ ")" ) "fun" gamma ^ " => " end ^ phi ^ ")" ^ List.fold_left (fun a v2 -> a ^ " " ^ string_of_f_variable v2) "" g2 ^ List.fold_left (fun a v2 -> a ^ " " ^ string_of_f_variable v2) "" autres ^ ")"