let version = "0.091"

(* Point fixe déterministe (avec relation bien fondée),
   avec la notion de terminaison.
   Pas d'extraction pour le moment.
*)

open Num

type reel = num
type naturel = num

let string_of_reel = string_of_num
let string_of_naturel = string_of_num

type spec = {
  spec_nom : string;
  spec_nom_infixe : string option;
  spec_scope : ty;
  spec_ty : ty;
  mutable spec_formule : formule;
}

and variable = string
    (* | Variable_textuelle of string *)

and ty = 
| Type_fleche of (ty * ty)
| Type_couple of (ty * ty)
| Type_o of ty
| Type_reel
| Type_bool
| Type_nat

and valeur = 
| Valeur_prob of expr
| Valeur_reelle of reel
| Valeur_nat of naturel
| Valeur_bool of bool
| Valeur_lambda of ((variable * ty) * terme)
    (* | Valeur_couple of (valeur * valeur)
       n'apparaît jamais sans évaluation de terme.
       En effet le parseur renvoie un couple sous la forme
       Terme_couple. *)
| Valeur_spec of spec

and terme = 
| Terme_valeur of valeur
| Terme_variable of variable
| Terme_application of (terme * terme)
| Terme_couple of (terme * terme)
| Terme_fst of terme
| Terme_snd of terme
| Terme_fix_det of terme_fix_det
| Terme_fix_prob of terme_fix_prob
| Terme_si of (terme * (terme * terme))
| Terme_egale of (terme * terme)

and terme_fix_det = {
  tfd_point_fixe : variable;
  tfd_param : variable;
  tfd_ty_param : ty;
  tfd_ordre_variant : string;
  tfd_ty_corps : ty;
  tfd_corps : terme
}

and terme_fix_prob = {
  tfp_point_fixe : variable;
  tfp_ens_variant : string;
  tfp_ordre_variant : string;
  tfp_ty_corps : ty;
  tfp_corps : expr;
}

and expr = 
| Expr_terme of terme
| Expr_sample of ((variable * terme) * expr)
| Expr_s

and f_var_abstr = (string * int)

and f_variable =
| Fv_variable of variable
| Fv_var_abstr of f_var_abstr (* int *)
| Fv_resultat
| Fv_flot_sortie

and f_terme =
| Ft_r of reel
| Ft_nat of naturel
| Ft_bool of bool
| Ft_variable of f_variable
| Ft_spec of (spec * (f_terme list))
| Ft_egale of (f_terme * f_terme) 
    (* égalité booléenne entre deux termes. *)

and formule =

|  F_terme of f_terme 

| F_true

| F_egale of (f_terme * f_terme)
    (* égalité propositionnelle entre deux variables surtout, 
       mais aussi entre variable et valeur.
    *)

| F_equiv of (f_variable * f_terme)
    (* pour les termes propositionnels pris comme booléens dans le
       code, comme x < y *)

| F_flot_cons of (f_variable * (f_variable * f_variable))

| F_relation_carre of
    (f_variable * (f_variable * (f_variable * f_variable)))

| F_relation_triangle of (f_variable * (f_variable * f_variable))

| F_relation_croix of (f_variable * (f_variable * f_variable))

| F_and of (formule * formule)
| F_imp of (formule * formule)

| F_existe of ((f_var_abstr * (f_variable list)) * formule)

| F_pour_tout of (f_var_abstr * formule)

| F_triangle of
    (f_variable * ((f_var_abstr * f_var_abstr) * formule))
| F_croix of
    (f_variable * ((f_var_abstr * f_var_abstr) * formule))
| F_carre of
    (
      f_variable * (
	(f_var_abstr * (f_var_abstr * f_var_abstr))
	* formule
     )
    )

| F_terminaison_triangle of
    (f_variable * (f_var_abstr * formule))

| F_terminaison_carre of 
    (f_variable * (f_var_abstr * formule))

| F_coq of (
    ((variable * ty) list * string)
    * (f_variable list * f_variable list)
  )

let f_and_opt = function
  | (F_true, f) -> f
  | (f, F_true) -> f
  | q -> F_and q

let f_imp_opt = function
  | (F_true, f) -> f
  | (_, F_true) -> F_true
  | q -> F_imp q

let type_s = Type_reel

let egalite ty v y =
  if ty = Type_bool
  then F_equiv (v, y)
  else F_egale (Ft_variable v, y)

exception Exception_scope_impossible of ty option

let nouvelle_variable_abstraite =
  let l = ref [] in
  let rec aux s = function
    | [] -> ([s, 0], (s, 0))
    | ((t, n)::q) when t = s ->
	let p = n + 1 in
	  ((t, p)::q, (t, p))
    | a::q ->
	let (q', res) = aux s q in (a::q', res)

  in fun s -> 
    let (l', res) = aux s !l in (l := l'; res)


(* La substitution de variables dans les formules. *)


let rec controle_variable_liee y u f =
  if y = Fv_var_abstr u
  then let u2 =
    nouvelle_variable_abstraite (fst u)
  in (u2, subst_formule y (Fv_var_abstr u2) f)
  else (u, f)

and subst_formule x y = function

  | F_true -> F_true

  | F_terme t -> F_terme (subst_terme x y t)

  | F_egale (t1, t2) ->
      F_egale (subst_terme x y t1, subst_terme x y t2)

  | F_equiv (v, t) ->
      F_equiv (subst_variable x y v, subst_terme x y t)

  | F_flot_cons (s, (eps, t)) ->
      F_flot_cons (
	subst_variable x y s,
	(subst_variable x y eps, subst_variable x y t)
      )

  | F_relation_carre (p, (s, (z, t))) ->
      F_relation_carre (
	subst_variable x y p, (
	  subst_variable x y s, 
	  (subst_variable x y z, subst_variable x y t)
	)
      )

  | F_relation_triangle (f, (a, b)) ->
      F_relation_triangle (
	subst_variable x y f,
	(subst_variable x y a, subst_variable x y b)
      )

  | F_relation_croix (c, (a, b)) ->
      F_relation_croix (
	subst_variable x y c,
	(subst_variable x y a, subst_variable x y b)
      )
  
  | F_and (f1, f2) ->
      F_and (subst_formule x y f1, subst_formule x y f2)
  | F_imp (f1, f2) ->
      F_imp (subst_formule x y f1, subst_formule x y f2)

  | F_existe ((v, l), f) as phi ->
      if x = Fv_var_abstr v
      then phi
      else let l2 = List.map (subst_variable x y) l in
	(* problème : y peut être v *)
      let v2, f15 = controle_variable_liee y v f
      in
      let f2 = subst_formule x y f15
      in F_existe ((v2, l2), f2)

  | F_pour_tout (v, f) as phi ->
      if x = Fv_var_abstr v
      then phi
      else let v2, f2 = controle_variable_liee y v f
      in F_pour_tout (v2, subst_formule x y f2)

  | F_triangle (t, ((u, v), f)) ->
      let t2 = subst_variable x y t in
	if x = Fv_var_abstr u || x = Fv_var_abstr v
	then F_triangle (t2, ((u, v), f))
	else
	  (* problème : y peut être l'une des deux u,v *)
	  let u2, f11 = controle_variable_liee y u f
	  in let v2, f12 = controle_variable_liee y v f11
	  in let f2 = subst_formule x y f12
	  in F_triangle (t2, ((u2, v2), f2))
   
  | F_croix (t, ((u, v), f)) ->
      let t2 = subst_variable x y t in
	if x = Fv_var_abstr u || x = Fv_var_abstr v
	then F_croix (t2, ((u, v), f))
	else
	  (* problème : y peut être l'une des deux u,v *)
	  let u2, f11 = controle_variable_liee y u f
	  in let v2, f12 = controle_variable_liee y v f11
	  in let f2 = subst_formule x y f12
	  in F_croix (t2, ((u2, v2), f2))
	  
  | F_carre (t, ((s, (u, s')), f)) ->
      let t2 = subst_variable x y t in
	if
	  x = Fv_var_abstr s ||
	  x = Fv_var_abstr u ||
	  x = Fv_var_abstr s'
	then F_carre (t2, ((s, (u, s')), f))
	else
	  (* problème : y peut être s, u, s' *)
	  let s2, f11 = controle_variable_liee y s f
	  in let u2, f12 = controle_variable_liee y u f11
	  in let s'2, f13 = controle_variable_liee y s' f12
	  in let f2 = subst_formule x y f13
	  in F_carre (t2, ((s2, (u2, s'2)), f2))

  | F_terminaison_triangle (k, (v, f)) ->
      let k2 = subst_variable x y k in
      let v2, f2 = controle_variable_liee y v f in
	F_terminaison_triangle (
	  k2,
	  (v2, subst_formule x y f2)
	)

  | F_terminaison_carre (k, (v, f)) ->
      let k2 = subst_variable x y k in
      let v2, f2 = controle_variable_liee y v f in
	F_terminaison_carre (
	  k2,
	  (v2, subst_formule x y f2)
	)

  | F_coq (vf, (w1, w2)) ->
      F_coq (vf, 
	     (List.map (subst_variable x y) w1,
	      List.map (subst_variable x y) w2
	     ))
     

and subst_variable x y v = if v = x then y else v

and subst_terme x y = function
  | Ft_r _ as t -> t
  | Ft_bool _ as t -> t
  | Ft_nat _ as t -> t
  | Ft_variable v -> Ft_variable (subst_variable x y v)
  | Ft_spec (s, l) -> Ft_spec (s, List.map (subst_terme x y) l)
  | Ft_egale (t1, t2) -> Ft_egale (subst_terme x y t1, subst_terme x y t2)



let spec_binaire ?precond
    type_valeurs type_resultat nom_prefixe nom_infixe =
  let s = {
    spec_nom = nom_prefixe;
    spec_nom_infixe = Some nom_infixe;
    spec_ty = Type_fleche (
      type_valeurs,
      Type_fleche (type_valeurs, type_resultat)
    );
    spec_scope = type_valeurs;
    spec_formule = F_true;
  } in
  let a = nouvelle_variable_abstraite "a"
  and g = nouvelle_variable_abstraite "g"
  and b = nouvelle_variable_abstraite "b"
  and y = nouvelle_variable_abstraite "y"
  in let corps_g_correct =
      F_triangle (
	Fv_var_abstr g, (
	  (b, y),
	  egalite type_resultat
	    (Fv_var_abstr y)
	    (Ft_spec (s,
		      [Ft_variable (Fv_var_abstr a);
		       Ft_variable (Fv_var_abstr b);]))
	)
      )
  in
    s.spec_formule <-
      f_and_opt (
	F_terminaison_triangle (Fv_resultat, (a, F_true)),
	F_triangle (
	  Fv_resultat, (
	    (a, g),
	    let corps_g_termine = match precond with
	      | None -> F_true
 	      | Some ((a', b'), psi') -> 
		  subst_formule 
		    (Fv_var_abstr a') (Fv_var_abstr a) (
		      subst_formule 
			(Fv_var_abstr b') (Fv_var_abstr b)
			psi'
		    )
	    in 
	      f_and_opt (
		F_terminaison_triangle (
		  Fv_var_abstr g,
		  (b, corps_g_termine)
		),
		corps_g_correct
	      )
	  )
	)
      );
    s     

let spec_unaire ?precond type_valeur type_resultat nom =
  let s = {
    spec_nom = nom;
    spec_nom_infixe = None;
    spec_ty = Type_fleche (type_valeur, type_resultat);
    spec_scope = type_valeur;
    spec_formule = F_true;
  } in
  let x = nouvelle_variable_abstraite "x"
  and y = nouvelle_variable_abstraite "y"
  in
  let corps_termine = match precond with
    | None -> F_true
    | Some (x', phi') -> 
	subst_formule (Fv_var_abstr x') (Fv_var_abstr x) phi'
  in
    s.spec_formule <-
      f_and_opt (
	F_terminaison_triangle (Fv_resultat, (x, corps_termine)),
	F_triangle (
	  Fv_resultat, (
	    (x, y),
	    egalite type_resultat (Fv_var_abstr y)
	      (Ft_spec (s, [Ft_variable (Fv_var_abstr x)]))
	  )
	)
      );
    s

let spec_nullaire ty nom =
  let s = {
    spec_nom = nom;
    spec_nom_infixe = None;
    spec_ty = ty;
    spec_scope = ty;
    spec_formule = F_true;
  } in
    s.spec_formule <- egalite ty Fv_resultat (Ft_spec (s, []));
    s

(* Pour le log, il faut s'assurer que x > 0 *)

let rgt = 
  spec_binaire Type_reel Type_bool "Rgt" ">"

let rzero =
  spec_nullaire Type_reel "R0"

let specs = [
  
(* Specs réelles. *)

  (spec_binaire Type_reel Type_reel "Rplus" "+"); 
  (spec_binaire Type_reel Type_reel "Rminus" "-");
  (spec_binaire Type_reel Type_reel "Rmult" "*");
  (spec_binaire Type_reel Type_reel "Rdiv" "/");
 
  (spec_binaire Type_reel Type_bool "Rle" "<=");
  (spec_binaire Type_reel Type_bool "Rlt" "<");
  (spec_binaire Type_reel Type_bool "Rge" ">=");
  rgt;  

  (spec_unaire
     ~precond:(
       let x = nouvelle_variable_abstraite "x" in
	 (x,
	  F_terme (
	    Ft_spec (rgt, [Ft_variable (Fv_var_abstr x);
			   Ft_spec (rzero, []);])
	  ))
     )
     Type_reel Type_reel "Ln");

  (spec_unaire Type_reel Type_reel "Exp");

  rzero;
  (spec_nullaire Type_reel "R1");


(* Specs naturelles. *)

  (spec_binaire Type_nat Type_nat "Plus" "+"); 
  (spec_binaire Type_nat Type_nat "Minus" "-");
  (spec_binaire Type_nat Type_nat "Mult" "*");
 
  (spec_binaire Type_nat Type_bool"Le" "<=");
  (spec_binaire Type_nat Type_bool "Lt" "<");
  (spec_binaire Type_nat Type_bool "Ge" ">=");
  (spec_binaire Type_nat Type_bool "Gt" ">");

  (spec_unaire Type_nat Type_nat "Succ");
  (spec_unaire Type_nat Type_nat "Pred");

  (spec_nullaire Type_nat "Zero");

]

exception Exception_spec_introuvable of string
exception Exception_spec2_introuvable of string

let string_of_spec s = s.spec_nom

let spec_of_string s =
  let rec aux = function
    | [] -> raise (Exception_spec_introuvable s)
    | u::_ when u.spec_nom = s -> u
    | _::q -> aux q
  in aux specs

let spec2_of_string s ty =
  let rec aux = function
    | [] -> raise (Exception_spec2_introuvable s)
    | u::q when u.spec_scope = ty ->
	begin match u.spec_nom_infixe with
	  | Some s' when s' = s -> u
	  | _ -> aux q
	end
    | _::q -> aux q
  in aux specs






(* Extraction (plus fort que le match pour explorer 
   la structure des formules) *)

(* Demander le type de formule (triangle, croix, carré) et la variable
   sur laquelle elle porte, et il renvoie les variables liées et la
   sous-formule correspondantes. *)

(* Pour l'instant, pas opérationnel (en fait, elles sont en état de
   fonctionner, mais elles ne sont pas utilisées). *)

let extraction cas_base conj f formule =

  let rec aux f' =
    match cas_base f' with
      | Some _ as res -> res
      | None -> aux2 f'
	  
  and aux2 = function
    | F_triangle (_, ((x, y), _))
	when Fv_var_abstr x = f || Fv_var_abstr y = f -> None
	
    | F_triangle (g, (vg, phi)) ->
	begin match aux phi with
	  | None -> None
	  | Some (v, psi) ->
	      Some (v, F_triangle (g, (vg, psi)))
	end
	  
    | F_croix (_, ((x, y), _)) 
	when Fv_var_abstr x = f || Fv_var_abstr y = f -> None
	
    | F_croix (g, (vg, phi)) ->
	begin match aux phi with
	  | None -> None
	  | Some (v, psi) ->
	      Some (v, F_croix (g, (vg, psi)))
	end
	  
    | F_carre (_, ((s, (x, t)), _)) 
	when
	  Fv_var_abstr x = f ||
	  Fv_var_abstr s = f ||
	  Fv_var_abstr t = f
	  -> None

    | F_carre (g, (vg, phi)) ->
	begin match aux phi with
	  | None -> None
	  | Some (v, psi) ->
	      Some (v, F_carre (g, (vg, psi)))
	end

    | F_existe ((x, _), _) when Fv_var_abstr x = f -> None

    | F_existe (xl, phi) ->
	begin match aux phi with
	  | None -> None
	  | Some (v, psi) ->
	      Some (v, F_existe (xl, psi))
	end

    | F_and (f1, f2) ->
	begin match aux f1, aux f2 with
	  | None, None -> None
	  | Some (v, phi), None ->
	      Some (v, f_and_opt (phi, f2))
	  | None, Some (v, phi) ->
	      Some (v, f_and_opt (f1, phi))
	  | Some a, Some b -> Some (conj a b)
	end

    | F_imp (f1, f2) ->
	begin match aux f2 with
	  | None -> None
	  | Some (v, phi) -> Some (v, f_imp_opt (f1, phi))
	end

    | _ -> None

  in aux formule
	

let extraction_triangle f formule =

  let cas_base = function
    | F_triangle (g, ((x, y), phi)) when g = f ->
	let x2 = nouvelle_variable_abstraite (fst x)
	and y2 = nouvelle_variable_abstraite (fst y)
	in let phi2 =
	    subst_formule (Fv_var_abstr x) (Fv_var_abstr x2) (
	      subst_formule
		(Fv_var_abstr y) (Fv_var_abstr y2)
		phi
	    )
	in Some ((x2, y2), phi2)
    | _ -> None

  and conj ((x1, y1), phi1) ((x2, y2), phi2) =
    (
      (x1, y1),
      f_and_opt (
	phi1,
	subst_formule (Fv_var_abstr x2) (Fv_var_abstr x1) (
	  subst_formule (Fv_var_abstr y2) (Fv_var_abstr y1) phi2
	)
      )
    )

  in match extraction cas_base conj f formule with
    | None ->
	let x = nouvelle_variable_abstraite "x"
	and y = nouvelle_variable_abstraite "y"
	in ((x, y), formule)
    | Some v -> v

let extraction_croix f formule =

  let cas_base = function
    | F_croix (g, ((x, y), phi)) when g = f ->
	let x2 = nouvelle_variable_abstraite (fst x)
	and y2 = nouvelle_variable_abstraite (fst y)
	in let phi2 =
	    subst_formule (Fv_var_abstr x) (Fv_var_abstr x2) (
	      subst_formule
		(Fv_var_abstr y) (Fv_var_abstr y2)
		phi
	    )
	in Some ((x2, y2), phi2)
    | _ -> None

  and conj ((x1, y1), phi1) ((x2, y2), phi2) =
    (
      (x1, y1),
      f_and_opt (
	phi1,
	subst_formule (Fv_var_abstr x2) (Fv_var_abstr x1) (
	  subst_formule (Fv_var_abstr y2) (Fv_var_abstr y1) phi2
	)
      )
    )

  in match extraction cas_base conj f formule with
    | None ->
	let x = nouvelle_variable_abstraite "x"
	and y = nouvelle_variable_abstraite "y"
	in ((x, y), formule)
    | Some v -> v


let extraction_carre f formule =

  let cas_base  = function
    | F_carre (g, ((s, (x, t)), phi)) when g = f ->
	let s2 = nouvelle_variable_abstraite (fst s) 
	in
	let phi11 =
	  subst_formule (Fv_var_abstr s) (Fv_var_abstr s2) phi
	in
	let x2 = nouvelle_variable_abstraite (fst x)
	in
	let phi12 =
	  subst_formule (Fv_var_abstr x) (Fv_var_abstr x2) phi11
	in
	let t2 = nouvelle_variable_abstraite (fst t)
	in 
	let phi13 =
	  subst_formule (Fv_var_abstr t) (Fv_var_abstr t2) phi12
	in
	let phi2 = phi13
	in Some ((s2, (x2, t2)), phi2)
    | _ -> None

  and conj ((s1, (x1, t1)), phi1) ((s2, (x2, t2)), phi2) =
    (
      (s1, (x1, t1)),
      f_and_opt (
	phi1,
	subst_formule (Fv_var_abstr s2) (Fv_var_abstr s1) (
	  subst_formule (Fv_var_abstr x2) (Fv_var_abstr x1) (
	    subst_formule (Fv_var_abstr t2) (Fv_var_abstr t1) phi2 
	  )
	)
      )
    )

  in match extraction cas_base conj f formule with
    | None ->
	let s = nouvelle_variable_abstraite "s"
	and x = nouvelle_variable_abstraite "x"
	and t = nouvelle_variable_abstraite "t"
	in ((s, (x, t)), formule)
    | Some v -> v


(* (Typage et en fait) recherche de la postcondition absolue *)

(* gamma est un contexte où les variables ont un type.
   Les fonctions de typage renvoient un type et deux formules, l'une
   précondition de terminaison, l'autre postcondition en cas de terminaison.
*)

exception Exception_variable_non_typee of variable

type types_incompatibles = {
 incompat_terme : terme;
 incompat_attendu : ty;
 incompat_obtenu : ty;
}
exception Exception_types_incompatibles of types_incompatibles

exception Exception_type_fleche_attendu of (terme * ty)
exception Exception_type_couple_attendu of (terme * ty)
exception Exception_type_o_attendu of (terme * ty)

let rec rechercher ex a0 = function
| [] -> raise ex
| (a,b) :: _ when a = a0 -> b
| _ :: r -> rechercher ex a0 r



let variables = List.map (fun (x, _) -> Fv_variable x)

let rec typage_valeur gamma = function
  | Valeur_reelle n ->
      Type_reel, (F_true, F_egale (Ft_variable Fv_resultat, Ft_r n))

  | Valeur_nat n ->
      Type_nat, (F_true, F_egale (Ft_variable Fv_resultat, Ft_nat n))

  | Valeur_bool b ->
      Type_bool, (F_true, F_egale (Ft_variable Fv_resultat, Ft_bool b))

  | Valeur_spec s -> s.spec_ty, (F_true, s.spec_formule)

  | Valeur_lambda ((x', tx), u) ->
      let (tu, (alpha', beta')) = typage_terme ((x', tx)::gamma) u
      in
      let x = nouvelle_variable_abstraite x'
      and y = nouvelle_variable_abstraite "y"
      in
      let alpha =
	subst_formule (Fv_variable x') (Fv_var_abstr x) alpha'
      and beta =
	subst_formule Fv_resultat (Fv_var_abstr y) (
	  subst_formule (Fv_variable x') (Fv_var_abstr x) beta'
	)
      in	
	(
	  Type_fleche (tx, tu),
	  (
	    F_true,
	    f_and_opt (
	      F_terminaison_triangle (Fv_resultat, (x, alpha)),
	      F_triangle (Fv_resultat, ((x, y), beta))	      
	    )
	  )
	)

  | Valeur_prob e ->
      let s = nouvelle_variable_abstraite "s"
      and y = nouvelle_variable_abstraite "y"
      and t = nouvelle_variable_abstraite "t" in
      let (te, (alpha, beta')) = typage_expr (Fv_var_abstr s) gamma e
      in
      let beta = 
	subst_formule Fv_resultat (Fv_var_abstr y) (
	  subst_formule Fv_flot_sortie (Fv_var_abstr t) beta'
	)
      in
	(
	  Type_o te,
	  (
	    F_true,
	    f_and_opt (
	      F_terminaison_carre (Fv_resultat, (s, alpha)),
	      F_carre (Fv_resultat, ((s, (y, t)), beta)) 
	    )
	  )
	)
	  

and typage_terme  gamma = function
  | Terme_valeur v -> typage_valeur gamma v

  | Terme_variable v ->
      let t =
	rechercher (Exception_variable_non_typee v) v gamma
      in
	(
	  t,
	  (
	    F_true,
	    F_egale (
	      Ft_variable Fv_resultat,
	      Ft_variable (Fv_variable v)
	    )
	  )
	)
	  
  | Terme_application (f', a') ->
      let tf', (pf, qf') = typage_terme gamma f'
      and ta', (pa, qa') = typage_terme gamma a'
      in begin match tf' with
	| Type_fleche (ta, tb) when ta' = ta ->
	    let f = nouvelle_variable_abstraite "f"
	    and a = nouvelle_variable_abstraite "a" in
	    let qf = 
	      subst_formule Fv_resultat (Fv_var_abstr f) qf'
	    and qa =
	      subst_formule Fv_resultat (Fv_var_abstr a) qa'
	    in (
		tb,
		(
		  f_and_opt (
		    f_and_opt (pf, pa),
		    F_pour_tout (
		      f,
		      F_terminaison_triangle (
			Fv_var_abstr f,
			(
			  a,
			  f_and_opt (f_and_opt (pf, pa), f_and_opt (qf, qa))
			)
		      )
		    )
		  ),
		  F_existe (
		    (f, Fv_resultat::(variables gamma)),
		    F_existe (
		      (a, Fv_resultat::(variables gamma)),
		      f_and_opt (
			f_and_opt (qf, qa),
			F_relation_triangle (
			  Fv_var_abstr f,
			  (Fv_var_abstr a, Fv_resultat)
			)
		      )
		    )
		  )
		)
	      )
	| Type_fleche (ta, _) -> raise (
	    Exception_types_incompatibles {
	      incompat_terme = a';
	      incompat_attendu = ta;
	      incompat_obtenu = ta';
	    }
	  )
	    
	| _ -> raise (
	    Exception_type_fleche_attendu (f', tf')
	  )
	end
	   

  | Terme_couple (a', b') ->
      let (ta, (pa, qa')) = typage_terme gamma a'
      and (tb, (pb, qb')) = typage_terme gamma b'
      in
      let a = nouvelle_variable_abstraite "a"
      and b = nouvelle_variable_abstraite "b"
      in
      let qa = subst_formule Fv_resultat (Fv_var_abstr a) qa'
      and qb = subst_formule Fv_resultat (Fv_var_abstr b) qb'
      in
	(
	  Type_couple (ta, tb),
	  (
	    f_and_opt (pa, pb),
	    f_and_opt (
	      F_existe (
		(a, Fv_resultat::(variables gamma)),
		F_existe (
		  (b, Fv_resultat::(variables gamma)),		  
		  F_relation_croix (
		    Fv_resultat, 
		    (Fv_var_abstr a, Fv_var_abstr b)
		  )
		)
	      ),
	      F_croix (
		Fv_resultat,
		((a, b), f_and_opt (qa, qb))
	      )
	    )
	  )
	)

  | Terme_fst c' ->
      let (tc', (pc, qc')) = typage_terme gamma c'
      in begin match tc' with
	| Type_couple (ty, _) ->
	    let m = nouvelle_variable_abstraite "m"
	    and c = nouvelle_variable_abstraite "c"
	    in 
	    let qc = subst_formule Fv_resultat (Fv_var_abstr c) qc'
	    in
	      (
		ty,
		(
		  pc,
		  F_existe (
		    (c, Fv_resultat::(variables gamma)),
		    F_existe (
		      (m, Fv_resultat::(variables gamma)),
		      f_and_opt (
			qc,
			F_relation_croix (
			  Fv_var_abstr c,
			  (Fv_resultat, Fv_var_abstr m)
			)
		      )
		    )
		  )
		)
	      )
	| _ -> raise (
	    Exception_type_couple_attendu (c', tc')
	  )
	end

  | Terme_snd c' ->
      let (tc', (pc, qc')) = typage_terme gamma c'
      in begin match tc' with
	| Type_couple (_, ty) ->
	    let m = nouvelle_variable_abstraite "m"
	    and c = nouvelle_variable_abstraite "c"
	    in 
	    let qc = subst_formule Fv_resultat (Fv_var_abstr c) qc'
	    in
	      (
		ty,
		(
		  pc,
		  F_existe (
		    (c, Fv_resultat::(variables gamma)),
		    F_existe (
		      (m, Fv_resultat::(variables gamma)),
		      f_and_opt (
			qc,
			F_relation_croix (
			  Fv_var_abstr c,
			  (Fv_var_abstr m, Fv_resultat)
			)
		      )
		    )
		  )
		)
	      )
	| _ -> raise (
	    Exception_type_couple_attendu (c', tc')
	  )
	end

  (* Voilà la fausse note : le si. *)
	  
  | Terme_si (b, (t, f)) ->
      let (tb, (pb, qb')) = typage_terme gamma b
      and (tt, (pt, qt)) = typage_terme gamma t
      and (tf, (pf, qf)) = typage_terme gamma f in
	if tb <> Type_bool	  
	then raise (
	  Exception_types_incompatibles {
	    incompat_terme = b;
	    incompat_obtenu = tb;
	    incompat_attendu = Type_bool;
	  }
	)
	else if tt <> tf
	then raise (
	  Exception_types_incompatibles {
	    incompat_terme = f;
	    incompat_obtenu = tf;
	    incompat_attendu = tt;
	  }
	)
	else let b = nouvelle_variable_abstraite "b"
	in
	let qb = subst_formule Fv_resultat (Fv_var_abstr b) qb'
	in 
	  (
	    tt,
	    (
	      f_and_opt (
		pb,
		F_pour_tout (
		  b,
		  f_imp_opt (
		    f_and_opt (pb, qb),
		    f_and_opt (
		      f_imp_opt (
			F_egale (
			  Ft_variable (Fv_var_abstr b),
			  Ft_bool true
			),
			pt
		      ),
		      f_imp_opt (
			F_egale (
			  Ft_variable (Fv_var_abstr b),
			  Ft_bool false
			),
			pf
		      )
		    )
		  )
		)
	      ),
	      F_existe (
		(b, Fv_resultat::(variables gamma)),
		f_and_opt (
		  qb,
		  f_and_opt (
		    f_imp_opt (
		      F_egale (
			Ft_variable (Fv_var_abstr b),
			Ft_bool true
		      ),
		      qt
		    ),
		    f_imp_opt (
		      F_egale (
			Ft_variable (Fv_var_abstr b),
			Ft_bool false
		      ),
		      qf
		    )
		  )
		)
	      )
	    )	      
	  )
	  
  | Terme_egale (u', v') ->
      let (tu, (pu, qu')) = typage_terme gamma u'
      and (tv, (pv, qv')) = typage_terme gamma v'
      in
	if tu <> tv
	then raise (
	  Exception_types_incompatibles {
	    incompat_terme = v';
	    incompat_obtenu = tv;
	    incompat_attendu = tu;
	  }
	)
	else let u = nouvelle_variable_abstraite "u"
	in let v = nouvelle_variable_abstraite "v"
	in
	let qu = subst_formule Fv_resultat (Fv_var_abstr u) qu'
	and qv = subst_formule Fv_resultat (Fv_var_abstr v) qv'
	in
	  (
	    Type_bool,
	    (
	      f_and_opt (pu, pv),
	      F_existe (
		(u, Fv_resultat::(variables gamma)),
		F_existe (
		  (v, Fv_resultat::(variables gamma)),
		  F_and (
		    F_and (qu, qv),
		    F_equiv (
		      Fv_resultat, 
		      Ft_egale (
			Ft_variable (Fv_var_abstr u),
			Ft_variable (Fv_var_abstr v)
		      )
		    )
		  )
		)
	      )
	    )
	  )


  | Terme_fix_det t ->
      let ty = Type_fleche (t.tfd_ty_param, t.tfd_ty_corps)
      in
      let (tk, (pk, qk)) =
	typage_terme (
	  (t.tfd_point_fixe, ty)
	  :: (t.tfd_param, t.tfd_ty_param)
	  :: gamma
	) t.tfd_corps
      in
	if tk <> t.tfd_ty_corps
	then raise (
	  Exception_types_incompatibles {
	    incompat_terme = t.tfd_corps;
	    incompat_obtenu = tk;
	    incompat_attendu = t.tfd_ty_corps;
	  }
	)
	else let f = nouvelle_variable_abstraite t.tfd_point_fixe
	in let n = nouvelle_variable_abstraite t.tfd_param
	in let m = nouvelle_variable_abstraite "m"
	in let hyp_lt = 
	  F_coq ((gamma, t.tfd_ordre_variant),
		 (variables gamma, [Fv_var_abstr m; Fv_var_abstr n]))
	in let y = nouvelle_variable_abstraite "y"
	in let py =
	  subst_formule (Fv_variable t.tfd_point_fixe) Fv_resultat (
	    subst_formule
	      (Fv_variable t.tfd_param) (Fv_var_abstr n)
	      pk
	  )
	and qy = 
	  subst_formule (Fv_variable t.tfd_point_fixe) Fv_resultat (
	    subst_formule (Fv_variable t.tfd_param) (Fv_var_abstr n) (
	      subst_formule Fv_resultat (Fv_var_abstr y) qk
	    )
	  )
	in
	  (
	    ty,
	    (
	      F_true,
	      (
		f_and_opt (
		  F_terminaison_triangle (
		    Fv_resultat, (
		      n,
		      f_and_opt (
			py,
			F_terminaison_triangle (
			  Fv_resultat, (m, hyp_lt)
			)
		      )
		    )
		  ),
		  F_triangle (
		    Fv_resultat,
		    ((n, y), qy)
		  )
		)
	      )
	    )
	  )

  | Terme_fix_prob e ->
      let ty = Type_o e.tfp_ty_corps
      in
      let s = nouvelle_variable_abstraite "s" in
      let (tk, (pk, qk)) =
	typage_expr
	  (Fv_var_abstr s) ((e.tfp_point_fixe, ty)::gamma)
	  e.tfp_corps
      in
	if tk <> e.tfp_ty_corps
	then raise (
	  Exception_types_incompatibles {
	    incompat_terme = Terme_valeur (Valeur_prob e.tfp_corps);
	    incompat_obtenu = Type_o tk;
	    incompat_attendu = ty;
	  }
	)
	else let p = nouvelle_variable_abstraite e.tfp_point_fixe
	in let s' = nouvelle_variable_abstraite "s'"
	in let t = nouvelle_variable_abstraite "t"
	in let y = nouvelle_variable_abstraite "y"
	in 
	let py =
	  subst_formule (Fv_variable e.tfp_point_fixe) Fv_resultat pk
	and qy =
	  subst_formule (Fv_variable e.tfp_point_fixe) Fv_resultat (
	    subst_formule Fv_resultat (Fv_var_abstr y) (
	      subst_formule Fv_flot_sortie (Fv_var_abstr t) qk
	    ) 
	  )
	in
	let hyp_ens s = F_coq (
	  (gamma, e.tfp_ens_variant),
	  (variables gamma, [Fv_var_abstr s])
	) in
	let hyp_lt = F_coq (
	  (gamma, e.tfp_ordre_variant),
	  (variables gamma, [Fv_var_abstr s'; Fv_var_abstr s])
	) in
	  (
	    ty,
	    (
	      F_true,
	      (
		f_and_opt (
		  F_terminaison_carre (
		    Fv_resultat,
		    (
		      s,
		      f_and_opt (
			F_terminaison_carre (
			  Fv_resultat, 
			  (s',  f_and_opt (hyp_lt, hyp_ens s'))
			),
			f_and_opt (py, hyp_ens s)
		      )
		    )
		  ),
		  F_carre (Fv_resultat, ((s, (y, t)), qy))
		)
	      )
	    )
	  )
	  

and typage_expr s gamma = function
  | Expr_terme t ->
      let (tt, (p, q)) = typage_terme gamma t
      in
	(
	  tt,
	  (
	    p,
	    f_and_opt (
	      q,
	      F_egale (Ft_variable Fv_flot_sortie, Ft_variable s)
	    )
	  )
	)

  | Expr_sample ((x', m'), e') ->
      let tm, (pm, qm') = typage_terme gamma m'
      in begin match tm with
	| Type_o tx ->
	    let s' = nouvelle_variable_abstraite "s" in
	    let m = nouvelle_variable_abstraite "m" in
	    let x = nouvelle_variable_abstraite x' in
	    let qm = subst_formule Fv_resultat (Fv_var_abstr m) qm'
	    and te, (pe', qe') =
	      typage_expr (Fv_var_abstr s') ((x', tx)::gamma) e'
	    in
	    let pe =
	      subst_formule (Fv_variable x') (Fv_var_abstr x) pe' 
	    and qe =
	      subst_formule (Fv_variable x') (Fv_var_abstr x) qe'
	    in
	      (
		te,
		(
		  f_and_opt (
		    pm,
		    F_pour_tout (
		      m,
		      f_imp_opt (
			pm,
			f_imp_opt (
			  qm,
			  f_and_opt (
			    F_existe (
			      (x, (variables gamma)),
			      (
				F_existe (
				  (s', (variables gamma)),
				  F_relation_carre (
				    Fv_var_abstr m,
				    (
				      s,
				      (
					Fv_var_abstr x,
					Fv_var_abstr s'
				      )
				    )
				  )
				)
			      )
			    ),
			    F_pour_tout (
			      x, 
			      F_pour_tout (
				s', 
				f_imp_opt (
				  F_relation_carre (
				    Fv_var_abstr m,
				    (
				      s,
				      (
					Fv_var_abstr x,
					Fv_var_abstr s'
				      )
				    )
				  ),
				  pe
				)
			      )
			    )
			  )
			)
		      )
		    )
		  ),
		  F_existe (
		    (
		      m,
		      Fv_resultat
		      :: Fv_flot_sortie
		      :: (variables gamma)
		    ), 
		    f_and_opt (
		      qm,
		      F_existe (
			(
			  x,
			  Fv_resultat
			  :: Fv_flot_sortie
			  :: (variables gamma)
			),
			F_existe (
			  (
			    s',
			    Fv_resultat
			    :: Fv_flot_sortie
			    :: (variables gamma)
			  ),
			  f_and_opt (
			    F_relation_carre (
			      Fv_var_abstr m,
			      (
				s,
				(
				  Fv_var_abstr x,
				  Fv_var_abstr s'
				)
			      )
			    ),
			    qe
			  )
			)
		      )
		    )
		  )
		)
	      )	
	| _ -> raise (Exception_type_o_attendu (m', tm))
	end 

  | Expr_s -> (
      type_s, 
      (F_true, (F_flot_cons (s, (Fv_resultat, Fv_flot_sortie))))
    )



(* Pour le toplevel *)

exception Exception_fin

type instruction = 
  | Instr_affectations of ((string * ty) * terme) list
  | Instr_variable of (string * ty)


let affectations corps l =
  let rec aux = function
    | [] -> corps, []
  
    | ((x, a), vx) :: q ->
	let corps2, vals2 = aux q in
	  (
	    Terme_valeur (
	      Valeur_lambda ((x, a), corps2)
	    ),
	    vx::vals2
	  )
	      
  in let corps2, vals2 = aux l in
  let rec construire k = function
    | [] -> k
    | v::q -> construire (Terme_application (k, v)) q
  in construire corps2 vals2
       
let transformer_terme_sous_aff aff m0 =
  let rec aux m = function
    | [] -> m
    | l::q -> aux (affectations m l) q
  in aux m0 aff
       
let rec transformer_expr_sous_aff aff = function
  | Expr_s -> Expr_s
  | Expr_terme m -> Expr_terme (transformer_terme_sous_aff aff m)
  | Expr_sample ((x, m), e) ->
      Expr_sample ((x, transformer_terme_sous_aff aff m),
		   transformer_expr_sous_aff aff e)



let sortie_erreur = ref (Some stderr)
let sortie_standard = ref (Some stdout)

let fermer_sortie sortie =
 match !sortie with
   | None -> ()
   | Some s when s = stdout || s = stderr -> sortie := None
   | Some s -> (close_out s; sortie := None)

let imprimer_sur_sortie sortie s = match !sortie with
  | Some o -> (output_string o s; flush o)
  | None -> ()

let print_string = imprimer_sur_sortie sortie_standard 
let print_newline () = print_string "\n"

let prerr_string = imprimer_sur_sortie sortie_erreur
let prerr_newline () = prerr_string "\n"