Added constructor for constants

TODO: correctly translate constants to pure terms in `purify'

diff --git a/ocaml/andrea.ml b/ocaml/andrea.ml
index 07cf670c134c75c5787c332302ca1b8c265fa186..8b47f88a5693153a630fdad73b9a20a2f3556226 100644 (file)
--- a/ocaml/andrea.ml
+++ b/ocaml/andrea.ml
@@ -12,6 +12,7 @@ type t =
  | A of t * t\r
  | L of t\r
  | B (* bottom *)\r
+ | C of int\r
 ;;\r
 \r
 let delta = L(A(V 0, V 0));;\r
@@ -22,6 +23,7 @@ let eta_eq =
   | L t1, t2 -> aux l1 (l2+1) t1 t2\r
   | t1, L t2 -> aux (l1+1) l2 t1 t2\r
   | V a, V b -> a + l1 = b + l2\r
+  | C a, C b -> a = b\r
   | A(t1,t2), A(u1,u2) -> aux l1 l2 t1 u1 && aux l1 l2 t2 u2\r
   | _, _ -> false\r
  in aux 0 0\r
@@ -38,6 +40,7 @@ let string_of_t =
   let rec string_of_term_w_pars level = function\r
     | V v -> if v >= level then "`" ^ string_of_int (v-level) else\r
        string_of_bvar (level - v-1)\r
+    | C n -> "c" ^ string_of_int n\r
     | A _\r
     | L _ as t -> "(" ^ string_of_term_no_pars level t ^ ")"\r
     | B -> "BOT"\r
@@ -86,6 +89,7 @@ let rec is_inert =
  function\r
  | A(t,_) -> is_inert t\r
  | V _ -> true\r
+ | C _\r
  | L _ | B -> false\r
 ;;\r
 \r
@@ -111,9 +115,11 @@ let rec subst level delift sub =
   let t1 = subst level delift sub t1 in\r
   let t2 = subst level delift sub t2 in\r
   mk_app t1 t2\r
+ | C _ as t -> t\r
  | B -> B\r
 and mk_app t1 t2 = if t2 = B || (t1 = delta && t2 = delta) then B\r
  else match t1 with\r
+ | C _ as t -> t\r
  | B -> B\r
  | L t1 -> subst 0 true (0, t2) t1\r
  | _ -> A (t1, t2)\r
@@ -123,6 +129,7 @@ and lift n =
   | V m -> V (if m >= lev then m + n else m)\r
   | L t -> L (aux (lev+1) t)\r
   | A (t1, t2) -> A (aux lev t1, aux lev t2)\r
+  | C _ as t -> t\r
   | B -> B\r
  in aux 0\r
 ;;\r
@@ -139,6 +146,7 @@ print_endline ("-- SUBST " ^ string_of_t (V (fst sub)) ^ " |-> " ^ string_of_t (
 \r
 let get_subterm_with_head_and_args hd_var n_args =\r
  let rec aux lev = function\r
+ | C _\r
  | V _ | B -> None\r
  | L t -> aux (lev+1) t\r
  | A(t1,t2) as t ->\r
@@ -155,6 +163,7 @@ let rec purify = function
  | L t -> Pure.L (purify t)\r
  | A (t1,t2) -> Pure.A (purify t1, purify t2)\r
  | V n -> Pure.V n\r
+ | C _ -> Pure.V max_int (* FIXME *)\r
  | B -> Pure.B\r
 ;;\r
 \r