From: acondolu <andrea.condoluci@unibo.it>
Date: Thu, 31 May 2018 12:40:38 +0000 (+0200)
Subject: Added constructor for constants
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=bbfb776c34c1d31d05943f80618a33cc6d297260;p=fireball-separation.git

Added constructor for constants

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

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