formatting

1 files changed, 241 insertions, 249 deletions

diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml
index 1abea36..069f2ec 100644
--- a/src/trace/smtForm.ml
+++ b/src/trace/smtForm.ml
@@ -18,17 +18,17 @@ open Util
 open SmtMisc
 open CoqTerms
 
-module type ATOM = 
-  sig 
+module type ATOM =
+  sig
 
-    type t 
+    type t
     val index : t -> int
 
     val equal : t -> t -> bool
 
     val is_bool_type : t -> bool
 
-  end 
+  end
 
 
 type fop =
@@ -42,80 +42,80 @@ type fop =
   | Fite
   | Fnot2 of int
 
-type ('a,'f) gen_pform = 
+type ('a,'f) gen_pform =
   | Fatom of 'a
   | Fapp of fop * 'f array
 
 
 module type FORM =
-  sig 
-    type hatom 
+  sig
+    type hatom
     type t
     type pform = (hatom, t) gen_pform
 
-      val pform_true : pform
-      val pform_false : pform
+    val pform_true : pform
+    val pform_false : pform
 
-      val equal : t -> t -> bool
+    val equal : t -> t -> bool
 
-      val to_lit : t -> int
-      val index : t -> int
-      val pform : t -> pform
+    val to_lit : t -> int
+    val index : t -> int
+    val pform : t -> pform
 
-      val neg : t -> t
-      val is_pos : t -> bool
-      val is_neg : t -> bool
+    val neg : t -> t
+    val is_pos : t -> bool
+    val is_neg : t -> bool
 
       val to_smt : (Format.formatter -> hatom -> unit) -> Format.formatter -> t -> unit
 
-      (* Building formula from positive formula *)
-      exception NotWellTyped of pform
-      type reify 
-      val create : unit -> reify 
-      val clear : reify -> unit
-      val get : reify -> pform -> t
-      
-      (** Give a coq term, build the corresponding formula *)  
-      val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
-   
-      (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
-      val flatten : reify -> t -> t
-
-      (** Producing Coq terms *) 
-
-      val to_coq : t -> Term.constr
-
-      val pform_tbl : reify -> pform array
-
-      val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
-      val interp_tbl : reify -> Term.constr * Term.constr
-      val nvars : reify -> int 
-      (** Producing a Coq term corresponding to the interpretation 
+    (* Building formula from positive formula *)
+    exception NotWellTyped of pform
+    type reify
+    val create : unit -> reify
+    val clear : reify -> unit
+    val get : reify -> pform -> t
+
+    (** Give a coq term, build the corresponding formula *)
+    val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t
+
+    (** Flattening of [Fand] and [For], removing of [Fnot2]  *)
+    val flatten : reify -> t -> t
+
+    (** Producing Coq terms *)
+
+    val to_coq : t -> Term.constr
+
+    val pform_tbl : reify -> pform array
+
+    val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array
+    val interp_tbl : reify -> Term.constr * Term.constr
+    val nvars : reify -> int
+    (** Producing a Coq term corresponding to the interpretation
           of a formula *)
-      (** [interp_atom] map [hatom] to coq term, it is better if it produce
+    (** [interp_atom] map [hatom] to coq term, it is better if it produce
           shared terms. *)
-      val interp_to_coq : 
-	  (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t -> 
-	    t -> Term.constr
+    val interp_to_coq :
+      (hatom -> Term.constr) -> (int, Term.constr) Hashtbl.t ->
+      t -> Term.constr
   end
 
 module Make (Atom:ATOM) =
-  struct 
+  struct
 
-    type hatom = Atom.t 
+    type hatom = Atom.t
 
     type pform = (Atom.t, t) gen_pform
- 
+
     and hpform = pform gen_hashed
-	  
-    and t = 
+
+    and t =
       | Pos of hpform
-      | Neg of hpform 
+      | Neg of hpform
 
     let pform_true = Fapp (Ftrue,[||])
     let pform_false = Fapp (Ffalse,[||])
 
-    let equal h1 h2 = 
+    let equal h1 h2 =
       match h1, h2 with
       | Pos hp1, Pos hp2 -> hp1.index == hp2.index
       | Neg hp1, Neg hp2 -> hp1.index == hp2.index
@@ -132,11 +132,11 @@ module Make (Atom:ATOM) =
     let neg = function
       | Pos hp -> Neg hp
       | Neg hp -> Pos hp
-	    
+
     let is_pos = function
       | Pos _ -> true
       | _ -> false
-	    
+
     let is_neg = function
       | Neg _ -> true
       | _ -> false
@@ -175,63 +175,63 @@ module Make (Atom:ATOM) =
 
 
     module HashedForm =
-      struct 
-	
+      struct
+
 	type t = pform
-	      
-	let equal pf1 pf2 = 
+
+	let equal pf1 pf2 =
 	  match pf1, pf2 with
 	  | Fatom ha1, Fatom ha2 -> Atom.equal ha1 ha2
 	  | Fapp(op1,args1), Fapp(op2,args2) ->
 	      op1 = op2 && 
-	      Array.length args1 == Array.length args2 &&
-	      (try 
-		for i = 0 to Array.length args1 - 1 do
-		  if not (equal args1.(i) args2.(i)) then raise Not_found 
-		done;
-		true
-	      with Not_found -> false)
+	       Array.length args1 == Array.length args2 &&
+	         (try
+		    for i = 0 to Array.length args1 - 1 do
+		      if not (equal args1.(i) args2.(i)) then raise Not_found
+		    done;
+		    true
+	          with Not_found -> false)
 	  | _, _ -> false
 
-	let hash pf = 
+	let hash pf =
 	  match pf with
-	  | Fatom ha1 -> Atom.index ha1 * 2 
-	  | Fapp(op, args) -> 
-	      let hash_args =
-		match Array.length args with
-		| 0 -> 0
-		| 1 -> to_lit args.(0)
-		| 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
-		| _ -> 
-		    (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
-		      to_lit args.(0) in
-	      (hash_args * 10 + Hashtbl.hash op) * 2 + 1
-		
+	  | Fatom ha1 -> Atom.index ha1 * 2
+	  | Fapp(op, args) ->
+	     let hash_args =
+	       match Array.length args with
+	       | 0 -> 0
+	       | 1 -> to_lit args.(0)
+	       | 2 -> (to_lit args.(1)) lsl 2 + to_lit args.(0)
+	       | _ ->
+		  (to_lit args.(2)) lsl 4 + (to_lit args.(1)) lsl 2 +
+		    to_lit args.(0) in
+	     (hash_args * 10 + Hashtbl.hash op) * 2 + 1
+
       end
 
     module HashForm = Hashtbl.Make (HashedForm)
 
     type reify = {
 	mutable count : int;
-                tbl : t HashForm.t 
-      }  
+                tbl : t HashForm.t
+      }
 
     exception NotWellTyped of pform
-   	
-    let check pf = 
+
+    let check pf =
       match pf with
       | Fatom ha ->  if not (Atom.is_bool_type ha) then raise (NotWellTyped pf)
       | Fapp (op, args) ->
-	  match op with
-	  | Ftrue | Ffalse -> 
-	      if Array.length args <> 0 then raise (NotWellTyped pf)
-	  | Fnot2 _ -> 
-	      if Array.length args <> 1 then raise (NotWellTyped pf)
-	  | Fand | For -> ()
-	  | Fxor | Fimp | Fiff ->
-	      if Array.length args <> 2 then raise (NotWellTyped pf)
-	  | Fite ->
-	      if Array.length args <> 3 then raise (NotWellTyped pf)
+	 match op with
+	 | Ftrue | Ffalse ->
+	    if Array.length args <> 0 then raise (NotWellTyped pf)
+	 | Fnot2 _ ->
+	    if Array.length args <> 1 then raise (NotWellTyped pf)
+	 | Fand | For -> ()
+	 | Fxor | Fimp | Fiff ->
+	    if Array.length args <> 2 then raise (NotWellTyped pf)
+	 | Fite ->
+	    if Array.length args <> 3 then raise (NotWellTyped pf)
 
     let declare reify pf =
       check pf;
@@ -241,8 +241,8 @@ module Make (Atom:ATOM) =
       res
 
     let create () =
-      let reify = 
-	{ count = 0; 
+      let reify =
+	{ count = 0;
 	  tbl =  HashForm.create 17 } in
       let _ = declare reify pform_true in
       let _ = declare reify pform_false in
@@ -256,12 +256,11 @@ module Make (Atom:ATOM) =
       ()
 
     let get reify pf =
-      try HashForm.find reify.tbl pf 
+      try HashForm.find reify.tbl pf
       with Not_found -> declare reify pf
 
-
-    (** Given a coq term, build the corresponding formula *)  
-    type coq_cst = 
+    (** Given a coq term, build the corresponding formula *)
+    type coq_cst =
       | CCtrue
       | CCfalse
       | CCnot
@@ -283,11 +282,11 @@ module Make (Atom:ATOM) =
     let op_tbl () =
       let tbl = ConstrHashtbl.create 29 in
       let add (c1,c2) = ConstrHashtbl.add tbl (Lazy.force c1) c2 in
-      List.iter add 
+      List.iter add
 	[
-	 ctrue,CCtrue; cfalse,CCfalse;
-	 candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot;
-         ceqb,CCiff; cifb,CCifb ];
+	  ctrue,CCtrue; cfalse,CCfalse;
+	  candb,CCand; corb,CCor; cxorb,CCxor; cimplb,CCimp; cnegb,CCnot;
+          ceqb,CCiff; cifb,CCifb ];
       tbl
 
     let op_tbl = lazy (op_tbl ())
@@ -296,125 +295,124 @@ module Make (Atom:ATOM) =
 
     let of_coq atom_of_coq reify c =
       let op_tbl = Lazy.force op_tbl in
-      let get_cst c = 
-	try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
+      let get_cst c =
+        try ConstrHashtbl.find op_tbl c with Not_found -> CCunknown in
       let rec mk_hform h =
-	let c, args = Term.decompose_app h in
-	match get_cst c with
-	| CCtrue  -> get reify (Fapp(Ftrue,empty_args))
-	| CCfalse -> get reify (Fapp(Ffalse,empty_args))
-	| CCnot -> mk_fnot 1 args
-	| CCand -> mk_fand [] args
-	| CCor  -> mk_for [] args
-	| CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
-	| CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
-	| CCimp ->
-          (match args with
+        let c, args = Term.decompose_app h in
+        match get_cst c with
+        | CCtrue  -> get reify (Fapp(Ftrue,empty_args))
+        | CCfalse -> get reify (Fapp(Ffalse,empty_args))
+        | CCnot -> mk_fnot 1 args
+        | CCand -> mk_fand [] args
+        | CCor  -> mk_for [] args
+        | CCxor -> op2 (fun l -> Fapp(Fxor,l)) args
+        | CCiff -> op2 (fun l -> Fapp(Fiff,l)) args
+        | CCimp ->
+           (match args with
             | [b1;b2] ->
+               let l1 = mk_hform b1 in
+               let l2 = mk_hform b2 in
+               get reify (Fapp (Fimp, [|l1;l2|]))
+            | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
+        | CCifb ->
+           (* We should also be able to reify if then else *)
+           begin match args with
+           | [b1;b2;b3] ->
               let l1 = mk_hform b1 in
               let l2 = mk_hform b2 in
-              get reify (Fapp (Fimp, [|l1;l2|]))
-            | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for implb")
-	| CCifb ->
-	    (* We should also be able to reify if then else *)
-	    begin match args with
-	    | [b1;b2;b3] ->
-		let l1 = mk_hform b1 in
-		let l2 = mk_hform b2 in
-		let l3 = mk_hform b3 in
-		get reify (Fapp(Fite, [|l1;l2;l3|]))
-	    | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
-	    end
-	| _ -> 
-	    let a = atom_of_coq  h in
-            get reify (Fatom a)
+              let l3 = mk_hform b3 in
+              get reify (Fapp (Fite, [|l1;l2;l3|]))
+           | _ -> Structures.error "SmtForm.Form.of_coq: wrong number of arguments for ifb"
+           end
+        | _ ->
+           let a = atom_of_coq h in
+           get reify (Fatom a)
 
       and op2 f args =
-	match args with
-	| [b1;b2] ->
-	    let l1 = mk_hform b1 in
-            let l2 = mk_hform b2 in
-            get reify (f [|l1; l2|])
-	| _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
-	  
+        match args with
+        | [b1;b2] ->
+           let l1 = mk_hform b1 in
+           let l2 = mk_hform b2 in
+           get reify (f [|l1; l2|])
+        | _ ->  Structures.error "SmtForm.Form.of_coq: wrong number of arguments"
+
       and mk_fnot i args =
-	match args with
-	| [t] -> 
-	    let c,args = Term.decompose_app t in
-	    if Term.eq_constr c (Lazy.force cnegb) then
-              mk_fnot (i+1) args
-	    else 
-              let q,r = i lsr 1 , i land 1 in
-              let l = mk_hform t in
-              let l = if r = 0 then l else neg l in
-	      if q = 0 then l
-	      else get reify (Fapp(Fnot2 q, [|l|]))
-	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
-	  
-      and mk_fand acc args = 
-	match args with
-	| [t1;t2] -> 
-	    let l2 = mk_hform t2 in
-	    let c, args = Term.decompose_app t1 in
-	    if Term.eq_constr c (Lazy.force candb) then
-              mk_fand (l2::acc) args
-	    else 
-	      let l1 = mk_hform t1 in
-	      get reify (Fapp(Fand, Array.of_list  (l1::l2::acc)))
-	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb" 
-
-      and mk_for acc args = 
-	match args with
-	| [t1;t2] -> 
-	    let l2 = mk_hform t2 in
-	    let c, args = Term.decompose_app t1 in
-	    if Term.eq_constr c (Lazy.force corb) then
-              mk_for (l2::acc) args
-	    else 
-	      let l1 = mk_hform t1 in
-	      get reify (Fapp(For, Array.of_list (l1::l2::acc)))
-	| _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
-
-      let l = mk_hform c in
-      l
+        match args with
+        | [t] ->
+           let c,args = Term.decompose_app t in
+           if Term.eq_constr c (Lazy.force cnegb) then
+             mk_fnot (i+1) args
+           else
+             let q,r = i lsr 1 , i land 1 in
+             let l = mk_hform t in
+             let l = if r = 0 then l else neg l in
+             if q = 0 then l
+             else get reify (Fapp(Fnot2 q, [|l|]))
+        | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for negb"
+
+      and mk_fand acc args =
+        match args with
+        | [t1;t2] ->
+           let l2 = mk_hform t2 in
+           let c, args = Term.decompose_app t1 in
+           if Term.eq_constr c (Lazy.force candb) then
+             mk_fand (l2::acc) args
+           else
+             let l1 = mk_hform t1 in
+             get reify (Fapp(Fand, Array.of_list (l1::l2::acc)))
+        | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for andb"
+
+      and mk_for acc args =
+        match args with
+        | [t1;t2] ->
+           let l2 = mk_hform t2 in
+           let c, args = Term.decompose_app t1 in
+           if Term.eq_constr c (Lazy.force corb) then
+             mk_for (l2::acc) args
+           else
+             let l1 = mk_hform t1 in
+             get reify (Fapp(For, Array.of_list (l1::l2::acc)))
+        | _ -> Structures.error "SmtForm.Form.mk_hform: wrong number of arguments for orb" in
+
+      mk_hform c
 
     (** Flattening of Fand and For, removing of Fnot2 *)
     let set_sign f f' =
       if is_pos f then f' else neg f'
 
-    let rec flatten reify f = 
+    let rec flatten reify f =
       match pform f with
       | Fatom _ -> f
       | Fapp(Fnot2 _,args) -> set_sign f (flatten reify args.(0))
       | Fapp(Fand, args) -> set_sign f (flatten_and reify [] (Array.to_list args))
       | Fapp(For,args) -> set_sign f (flatten_or reify [] (Array.to_list args))
       | Fapp(op,args) ->
-          (* TODO change Fimp into For ? *)
-	  set_sign f (get reify (Fapp(op, Array.map (flatten reify) args)))
+         (* TODO change Fimp into For ? *)
+	 set_sign f (get reify (Fapp(op, Array.map (flatten reify) args)))
 
     and flatten_and reify acc args =
       match args with
       | [] -> get reify (Fapp(Fand, Array.of_list (List.rev acc)))
       | a::args ->
-	  (* TODO change (not For) and (not Fimp) into Fand *)
-	  match pform a with
-	  | Fapp(Fand, args') when is_pos a ->
-	      let args = Array.fold_right (fun a args -> a::args) args' args in
-	      flatten_and reify acc args
-	  | _ -> flatten_and reify (flatten reify a :: acc) args
+	 (* TODO change (not For) and (not Fimp) into Fand *)
+	 match pform a with
+	 | Fapp(Fand, args') when is_pos a ->
+	    let args = Array.fold_right (fun a args -> a::args) args' args in
+	    flatten_and reify acc args
+	 | _ -> flatten_and reify (flatten reify a :: acc) args
 
     and flatten_or reify acc args =
       (* TODO change Fimp and (not Fand) into For *)
       match args with
       | [] -> get reify (Fapp(For, Array.of_list (List.rev acc)))
       | a::args ->
-	  match pform a with
-	  | Fapp(For, args') when is_pos a ->
-	      let args = Array.fold_right (fun a args -> a::args) args' args in
-	      flatten_or reify acc args
-	  | _ -> flatten_or reify (flatten reify a :: acc) args
+	 match pform a with
+	 | Fapp(For, args') when is_pos a ->
+	    let args = Array.fold_right (fun a args -> a::args) args' args in
+	    flatten_or reify acc args
+	 | _ -> flatten_or reify (flatten reify a :: acc) args
 
-    (** Producing Coq terms *) 
+    (** Producing Coq terms *)
 
     let to_coq hf = mkInt (to_lit hf)
 
@@ -422,20 +420,20 @@ module Make (Atom:ATOM) =
       let cargs = Array.make (Array.length args + 1) (mkInt 0) in
       Array.iteri (fun i hf -> cargs.(i) <- to_coq hf) args;
       Structures.mkArray (Lazy.force cint, cargs)
-	
+
     let pf_to_coq = function
-      | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]	
+      | Fatom a -> mklApp cFatom [|mkInt (Atom.index a)|]
       | Fapp(op,args) ->
-        match op with
-	| Ftrue -> Lazy.force cFtrue
-	| Ffalse -> Lazy.force cFfalse
-	| Fand -> mklApp cFand [| args_to_coq args|]
-	| For  -> mklApp cFor [| args_to_coq args|]
-	| Fimp -> mklApp cFimp [| args_to_coq args|]
-	| Fxor -> mklApp cFxor (Array.map to_coq args)
-	| Fiff -> mklApp cFiff (Array.map to_coq args)
-	| Fite -> mklApp cFite (Array.map to_coq args)
-	| Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
+         match op with
+	 | Ftrue -> Lazy.force cFtrue
+	 | Ffalse -> Lazy.force cFfalse
+	 | Fand -> mklApp cFand [| args_to_coq args|]
+	 | For  -> mklApp cFor [| args_to_coq args|]
+	 | Fimp -> mklApp cFimp [| args_to_coq args|]
+	 | Fxor -> mklApp cFxor (Array.map to_coq args)
+	 | Fiff -> mklApp cFiff (Array.map to_coq args)
+	 | Fite -> mklApp cFite (Array.map to_coq args)
+	 | Fnot2 i -> mklApp cFnot2 [|mkInt i; to_coq args.(0)|]
 
     let pform_tbl reify =
       let t = Array.make reify.count pform_true in
@@ -464,55 +462,49 @@ module Make (Atom:ATOM) =
     (** [interp_atom] map [Atom.t] to coq term, it is better if it produce
 	shared terms. *)
     let interp_to_coq interp_atom form_tbl f =
-      let rec interp_form f = 
+      let rec interp_form f =
 	let l = to_lit f in
-	try Hashtbl.find form_tbl l 
+	try Hashtbl.find form_tbl l
 	with Not_found ->
-	  if is_neg f then 
-	    let pc = interp_form (neg f) in
-	    let nc = mklApp cnegb [|pc|] in
-	    Hashtbl.add form_tbl l nc;
-	    nc
-	  else
-	    let pc = 
-	      match pform f with
-	      | Fatom a -> interp_atom a
-	      | Fapp(op, args) ->
-		  match op with
-		  | Ftrue -> Lazy.force ctrue
-		  | Ffalse -> Lazy.force cfalse
-		  | Fand -> interp_args candb args
-		  | For -> interp_args corb args
-		  | Fxor -> interp_args cxorb args
-		  | Fimp -> 
-		      let r = ref (interp_form args.(Array.length args - 1)) in
-		      for i = Array.length args - 2 downto 0 do
-			r := mklApp cimplb [|interp_form args.(i); !r|]
-		      done;
-		      !r
-		  | Fiff -> interp_args ceqb args
-		  | Fite -> 
-		      (* TODO with if here *)
-		      mklApp cifb (Array.map interp_form args)
-		  | Fnot2 n -> 
-		      let r = ref (interp_form args.(0)) in
-		      for i = 1 to n do	r := mklApp cnegb [|!r|] done;
-		      !r in 
-	    Hashtbl.add form_tbl l pc;
-	    pc
+	      if is_neg f then
+	        let pc = interp_form (neg f) in
+	        let nc = mklApp cnegb [|pc|] in
+	        Hashtbl.add form_tbl l nc;
+	        nc
+	      else
+	        let pc =
+	          match pform f with
+	          | Fatom a -> interp_atom a
+	          | Fapp(op, args) ->
+		     match op with
+		     | Ftrue -> Lazy.force ctrue
+		     | Ffalse -> Lazy.force cfalse
+		     | Fand -> interp_args candb args
+		     | For -> interp_args corb args
+		     | Fxor -> interp_args cxorb args
+		     | Fimp ->
+		        let r = ref (interp_form args.(Array.length args - 1)) in
+		        for i = Array.length args - 2 downto 0 do
+		          r := mklApp cimplb [|interp_form args.(i); !r|]
+		        done;
+		        !r
+		     | Fiff -> interp_args ceqb args
+		     | Fite ->
+		        (* TODO with if here *)
+		        mklApp cifb (Array.map interp_form args)
+		     | Fnot2 n ->
+		        let r = ref (interp_form args.(0)) in
+		        for i = 1 to n do
+                          r := mklApp cnegb [|!r|]
+                        done;
+                        !r in
+	        Hashtbl.add form_tbl l pc;
+	        pc
       and interp_args op args =
 	let r = ref (interp_form args.(0)) in
-	for i = 1 to Array.length args - 1 do
-	  r := mklApp op [|!r;interp_form args.(i)|] 
-	done;
-	!r in
-      interp_form f
-
-  end
-	
-
-	  
-
-    
-
-  
+	  for i = 1 to Array.length args - 1 do
+	    r := mklApp op [|!r;interp_form args.(i)|]
+	  done;
+	  !r in
+        interp_form f
+end