Manipulate unmutable variables inside of loop in OCaml

Question

I have the following code in OCaml.I have defined all necesar functions and tested them step by step the evalution should work good but I didn't succed to manipulate the variables inside of while.How can I make x,vn,v to change their value?I think I should rewrite the while like a rec loop but can't figure out exactly: Here is the rest of code: http://pastebin.com/Ash3xw6y

Pseudocode: 
  input : f formula
  output: yes if f valid 
           else not
    begin:
        V =set of prop variables
        eliminate from f => and <=>
        while (V is not empty)
           choose x from V
           V =V -{x}
           replace f with f[x->true]&&f[x->false]
            simplify as much as possible f
            if f is evaluated with true then return true 
                 else if (not f) is evaluated true then return false
            end if
           end while
      return false
  end

type bexp = V of 
            | string
            | B of bool
            | Neg of bexp
            | And of bexp * bexp 
            | Or of bexp * bexp
            | Impl of bexp * bexp
            | Eqv of bexp * bexp  

module StringSet=Set.make(String)

let is_valide f=
  let v= stringset_of_list (ens f []) in  (*set of all variables of f *)
  let g= elim f in  (*eliminate => and <=> *)
  let quit_loop=ref false in  
  while not !quit_loop
  do
    let x=StringSet.choose  v in
    let vn=StringSet.remove x v in
    if StringSet.is_empty vn=true then quit_loop:=true;
    let h= And( replace x (B true) g ,replace x (B false) g)in
    let j=simplify h in
    if (only_bools j) then
      if (eval j) then print_string "yes" 
      else print_string "not"
  done

(New form)

   let tautology f =
           let rec tautology1 x v g =     
               let h= And( remplace x (B true) g ,remplace x (B false) g)in
               let j= simplify h in
     if not (only_bools j) then tautology (StringSet.choose (StringSet.remove x v)     (StringSet.remove x v)  j 
                 else 
                   if (eval1 j) then print_string "yes \n "  else
                     if (eval1 (Neg (j)))  then  print_string "not \n";
           in tautology1 (StringSet.choose (stringset_of_list (ens f [])) (stringset_of_list (ens f []))  (elim f);;

Answer 1

while loop belongs to imperative programming part in OCaml.

Basically, you can't modify immutable variables in while or for loops or anywhere.

To let a variable to be mutable, you need to define it like let var = ref .... ref is the keyword for mutables.

Read these two chapters:

1. https://realworldocaml.org/v1/en/html/a-guided-tour.html#imperative-programming
2. https://realworldocaml.org/v1/en/html/imperative-programming-1.html

---

You can define x,vn,v as refs, but I guess it will be ugly.

I suggest you think your code in a functional way.

Since you haven't placed functions ens etc here, I can't produce an example refine for u.