(* Ce fichier est très impératif. *)


open Lo
open Lo_lex
open Lo_parse
open Lo_print
open Arg

let contexte_0 = ([], Fv_variable "stream_in")

exception Exception_variable_deja_definie of string

let executer_instruction ((gamma, s0) as contexte) i =
  print_newline ();
  match i with
      (*
    | Instr_expr e' -> 
	let e = - transformer_expr_sous_aff aff - e' in
	let (t, f) = typage_expr s0 gamma e in
	let (_, nu) as res = nouvelle_variable_abstraite "result" in
	let (_, nu_s) as s1 = nouvelle_variable_abstraite "stream" in
	let numero_s = string_of_int nu_s
	in
	let numero = string_of_int nu in
	let f2 = subst_formule Fv_resultat (Fv_var_abstr res) (
	  subst_formule Fv_flot_sortie (Fv_var_abstr s1) f
	) in
	  begin
	    print_string ("Variable stream_" ^ numero_s ^ " : Flot.\n");
	    print_string ("Variable result_" ^ numero ^ " : " ^
	      string_of_type t ^ ".");
	    print_newline ();
	    print_newline ();
	    print_string ("Hypothesis Prog_" ^ numero ^
			    " : ");
	    print_newline ();	    
	    print_string (string_of_formule f2);
	    print_newline ();
	    print_string ".";
	    print_newline ();
	    print_newline ();
	    (gamma, Fv_var_abstr s1)
	  end
      *)
    | Instr_variable (v, t) ->
	let rec aux = function
	  | [] -> 
	      print_string ("Variable " ^ v ^ " : " ^
			      coq_string_of_type t ^ ".");
	      print_newline ();
	      print_newline ();
	      ((v, t)::gamma, s0)
	  | (v', _) :: _ when v = v' ->
	      raise (Exception_variable_deja_definie v)
	  | _ :: q ->
	      aux q
	in 
	  aux gamma

    | Instr_affectations l ->
	begin
	  List.iter (
	    fun ((x, a), m) ->
	      List.iter
		(fun (v, _) -> if v = x then
		   raise (Exception_variable_deja_definie v)
		) gamma;
	      let (b, (p', q')) = typage_terme gamma m
	      in
		if b <> a
		then raise (
		  Exception_types_incompatibles {
		    incompat_terme = m;
		    incompat_attendu = a;
		    incompat_obtenu = b
		  }
		)
		else
		  let p =
		    subst_formule Fv_resultat (Fv_variable x) p'
		  and q = 
		    subst_formule Fv_resultat (Fv_variable x) q'
		  in let phi2 = f_imp_opt (p, q)
		  in begin
		      print_string (
			"Variable " ^ x ^ " : " ^ coq_string_of_type a ^
			  "."
		      );
		      print_newline ();
		      print_string (
			"Hypothesis Hyp_" ^ x ^ " : \n" ^
			  string_of_formule phi2 ^ "\n."
		      );
		      print_newline ();
		      print_newline ();
		    end;
	  ) l;
	  let gamma' = List.map (
	    fun ((x,a),_) -> ( x, a)
	  ) l @ gamma
	  and l' = (* List.map (
	    fun (v,m) -> (v, transformer_terme_sous_aff aff m)
		      ) *) l
	  in (gamma', s0)
	end


let execution phi p t l =
  try
    
    let objet = p t l in Some (phi objet)

  with 
    | Exception_spec_introuvable spec ->
	(
	  prerr_string "> Impossible de trouver la fonction spéciale : ";
	  prerr_string spec;
	  prerr_newline ();
	  None
	)
    | Exception_variable_non_typee v ->
	(
	  prerr_string "> Variable non typée : ";
	  prerr_string (string_of_variable v);
	  prerr_newline ();
	  None
	)
    | Exception_types_incompatibles t ->
	(
	  prerr_string "> Types incompatibles.\n>Terme : ";
	  prerr_string (string_of_terme t.incompat_terme);
	  prerr_newline ();
	  prerr_string "> Type obtenu : ";
	  prerr_string (pcaml_string_of_type t.incompat_obtenu);
	  prerr_newline ();
	  prerr_string "> Type attendu : ";
	  prerr_string (pcaml_string_of_type t.incompat_attendu);
	  prerr_newline (); 
	  None
	)
    | Exception_type_fleche_attendu (m, t) ->
	(
	  prerr_string "> Type flèche attendu\n>Terme : ";
	  prerr_string (string_of_terme m);
	  prerr_newline ();
	  prerr_string "> Type obtenu : ";
	  prerr_string (pcaml_string_of_type t);
	  prerr_newline ();
	  None
	)
    | Exception_type_couple_attendu (m, t) ->
	(
	  prerr_string ">Type couple attendu\n>Terme : ";
	  prerr_string (string_of_terme m);
	  prerr_newline ();
	  prerr_string "Type obtenu : ";
	  prerr_string (pcaml_string_of_type t);
	  prerr_newline ();
	  None
	)
    | Exception_type_o_attendu (m, t) ->
	(
	  prerr_string "> Type O attendu\n>Terme : ";
	  prerr_string (string_of_terme m);
	  prerr_newline ();
	  prerr_string "> Type obtenu : ";
	  prerr_string (pcaml_string_of_type t);
	  prerr_newline ();
	  None
	)
    | Exception_variable_deja_definie s ->
	(
	  prerr_string	("> La variable " ^ s ^ " est déjà définie.");
	  prerr_newline ();
	  None
	)
    | Sys.Break ->
        (
          prerr_string "> Interruption.";
          prerr_newline ();
          None
        )
    | Exception_fin -> raise Exception_fin
    | exn ->
	(	  
	  prerr_string ("> Exception : " ^ Printexc.to_string exn);
          prerr_newline ();
	  None
	)
	  

let (au_revoir, bonjour) = 
  let deja_affiche = ref false in
  let b_aux () =
    if !deja_affiche then () else begin
      deja_affiche := true;
      print_newline ();
      print_string ("(* Proba Caml (ALICE) version " ^ version ^ " *)\n");
      print_newline ();
      print_string "Section Prog.\n";
      (* print_string "\nVariable stream_in : Flot."; *)
      print_newline ();
      print_newline ();
      prerr_string "> Bonjour !";
      prerr_newline ();
    end
  and a_aux () =
    if !deja_affiche then begin
      print_newline ();
      print_string "End Prog.";
      print_newline ();
      prerr_newline ();
      prerr_string "> A bientôt !";
      prerr_newline ();
      prerr_newline ();
      fermer_sortie sortie_standard;
      fermer_sortie sortie_erreur;
    end else ()
  in (a_aux, b_aux)

let contexte = ref contexte_0
	  
let rec boucle_clavier contexte =
  bonjour ();
  try
    match
      let l = Lexing.from_channel stdin in
	prerr_string "# ";
	flush stderr;
	execution
	  (executer_instruction contexte)
	  programme_clavier (token false) l
    with
      | None -> boucle_clavier contexte
      | Some ct2 -> boucle_clavier ct2	  
  with
    | Exception_fin -> contexte

let executer_clavier () =
  contexte := boucle_clavier !contexte

let executer_fichier fichier =
  let ch = open_in fichier in
  let l = Lexing.from_channel ch in
    bonjour ();
    match
      execution
	(List.fold_left executer_instruction !contexte)
	programme_fichier (token true) l
    with
      | None -> 
	  begin
	    prerr_string ("> Fichier : " ^ fichier);
	    prerr_newline ();
	    raise Exception_fin
	  end
      | Some c -> contexte := c
	  
let rediriger_sortie sortie canal =
  fermer_sortie sortie;
  sortie := Some canal

let rediriger_vers_fichier sortie nom =
  rediriger_sortie sortie (open_out nom)

let msg_usage =
  "Proba Caml (ALICE) version " ^ version ^ " - The PI transformer\nUSAGE : " ^ Sys.argv.(0) ^ " [options] [fichiers entrée]"

let rec liste_options () = align [
  "-v", Unit (fun () -> rediriger_sortie sortie_erreur stderr),
  " Affiche les erreurs sur la sortie erreur standard (défaut)";

  "-q", Unit (fun () -> fermer_sortie sortie_erreur),
  " N'affiche pas les erreurs";

  "-l", Unit (fun () -> rediriger_sortie sortie_standard stdout),
  " Affiche le code Coq produit sur la sortie standard (défaut)";
  
  "-s", Unit (fun () -> fermer_sortie sortie_standard),
  " N'affiche pas le code Coq produit";

  "-o", String (rediriger_vers_fichier sortie_standard),
  "fichier Enregistre le code Coq produit dans un fichier";

  "-e", String (rediriger_vers_fichier sortie_erreur),
  "fichier Enregistre les erreurs dans un fichier";

  "--", String executer_fichier,
  "fichier Permet de lire un fichier d'entrée dont le nom commence par -";

  "-h", Unit (fun () -> usage (liste_options ()) msg_usage),
  " Affiche ce message d'aide.";

  "-k", Unit executer_clavier,
  " Passe la main à l'utilisateur (invite clavier)";

  "--help", Unit (fun () -> usage (liste_options ()) msg_usage),
  " Affiche ce message d'aide.";
]

let _ =
  Sys.catch_break true;
  if Array.length Sys.argv = 1
  then
    executer_clavier ()
  else begin try
    Arg.parse (liste_options ()) executer_fichier msg_usage
  with _ -> () end
  ;
  au_revoir ()