ma proposition

src/main.ml

+open Term
+open Typing
+
+let alpha = Name.from_string "alpha"
+let talpha = Ty.var alpha
+let aa = Ty.arrow talpha talpha
+
+let a = Name.from_string "a"
+let b = Name.from_string "b"
+let t1 = lam a talpha (app (var a) (var b))
+let t2 = lam a talpha (app (var a) (var b))
+
+let ta = app (var a) (var b)
+let tb = app (var a) (var b)
+
+let g = Name.from_string "g"
+let f = Name.from_string "f"
+let h = Name.from_string "h"
+
+let tk = lam g aa (lam f aa (app (var g) (var f)))
+
+let termfun t = 
+  match t.node with
+  | App ({ node = Var v}, t2) when Name.equal v g -> app (var h) t2
+  | _ -> t
+
+let tl = map termfun tk
+
+let _ = 
+  Format.printf "%a = %a = %b@." print t1 print t2 (equal t1 t2);
+  Format.printf "%a = %a = %b@." print ta print tb (equal ta tb);
+  Format.printf "%a -> %a : %b@." print tk print tl (alpha_equal tk tl)
+
+let x = Name.from_string "x"
+let y = Name.from_string "y"
+
+let pat = ptuple (pvar x) (pvar y)
+let ap = app (var x) (var y)
+
+let t = app (case tk pat [x;y] ap) (tuple ap ap)
+
+let _ = 
+  Format.printf "%a@." print t;
+  Typing.theory [ Formula (close_polyterm [] t) ]

src/misc.ml

+let combine n acc = 
+  let r = acc * 65599 + n in
+  if r < 0 then
+    if r = min_int then max_int
+    else 0 - r
+  else r
+
+let combine2 n acc1 acc2 = combine n (combine acc1 acc2)
+let combine3 n acc1 acc2 acc3 = combine n (combine acc1 (combine acc2 acc3))
+
+let hash_int : int -> int = Hashtbl.hash
+let hash_string : string -> int = Hashtbl.hash
+
+module IntMap = 
+  Map.Make(struct type t = int let compare = Pervasives.compare end)
+
+open Format
+let id x = x
+let ksprintf k s =
+  ignore(flush_str_formatter ());
+  kfprintf (fun _ -> k (flush_str_formatter ())) str_formatter s
+
+let sprintf s = ksprintf id s
+
+let rec print_list sep prf fmt = function
+  | [] -> ()
+  | [x] -> prf fmt x
+  | (x::xs) -> prf fmt x; sep fmt (); print_list sep prf fmt xs
+
+let comma fmt () = pp_print_string fmt ","

src/name.ml

+type t = { tag : int ; name : string }
+
+let fresh =
+  let cnt = ref 0 in
+  fun t -> 
+    let tag = !cnt in
+    incr cnt;
+    { t with tag = tag }
+
+let from_string s = fresh { name = s; tag = 0}
+
+let equal a b = a.tag = b.tag
+let compare a b = Pervasives.compare a.tag b.tag
+let hash n = Hashtbl.hash n.tag
+
+let unsafe_to_string n = n.name
+
+let name_map = Hashtbl.create 47
+
+let default_string = "anon"
+
+let strip_numbers s = 
+  let rec aux n = 
+    if n <= 0 then 0
+    else
+      match s.[n-1] with
+      | '0'..'9' -> aux (n-1)
+      | _ -> n in
+  let n = aux (String.length s) in
+  if n = 0 then default_string else String.sub s 0 n
+
+let fresh_string name = 
+  let s = strip_numbers name in
+  try
+    let i = Hashtbl.find name_map s in
+    let s' = s ^ (string_of_int !i) in
+    incr i; s'
+  with Not_found ->
+    let x = ref 1 in
+  Hashtbl.add name_map s x;
+  s
+
+let to_string n = fresh_string (unsafe_to_string n)
+
+module HT = struct
+  type t' = t
+  type t = t'
+  let equal = equal
+  let hash = hash
+  let compare = compare
+end
+module H = Hashtbl.Make (HT)
+module M = Map.Make (HT)
+module S = Set.Make (HT)
+
+let get_cur_name, reset =
+  let current_name_map = H.create 47 in
+  let reset () = 
+    H.clear current_name_map; 
+    Hashtbl.clear name_map in
+  let get_name x = 
+    try H.find current_name_map x
+    with Not_found ->
+      let s = to_string x in
+      H.add current_name_map x s;
+      s in
+  get_name, reset
+
+let to_string = get_cur_name
+  
+let print fmt x = Format.fprintf fmt "%s" (get_cur_name x)
+
+let build_map nl = 
+  let m,_ = 
+    List.fold_left (fun (m, i) n -> M.add n i m, i + 1) 
+      (M.empty, 0) nl in
+  m
+

src/name.mli

+type t
+(** the type of Names *)
+
+val from_string : string -> t
+(** create a new name from a string *)
+
+val fresh : t -> t
+(** generate a new name from an old one *)
+
+val equal : t -> t -> bool
+(** efficient equality test on names *)
+
+val compare : t -> t -> int
+(** efficient comparison on names *)
+
+val hash : t -> int
+(** compute a hash for this name *)
+
+val unsafe_to_string : t -> string
+(** convert a name to a string; does not guarantee uniqueness. *)
+
+val to_string : t -> string
+(** get a unique string for a name. This name is memoized between calls,
+  so that [to_string n] always returns the same string for the same name.
+  Call [reset] to reset the memoization information. *)
+
+val print : Format.formatter -> t -> unit
+(** pretty printing names, using [to_string] to obtain a unique string. *)
+
+val reset : unit -> unit
+(* Reset the memoization information. Strings obtained using
+   [to_string] or [print] after resetting are not guaranteed to be different
+   from strings obtained before. *)
+
+module M : Map.S with type key = t
+module S : Set.S with type elt = t
+
+val build_map : t list -> int M.t
+(** from the list [ [n_1; ... ; n_m] ] of names build the map
+ * [ n_1 |-> 0 ; ... n_m |-> m -1 ] *)

src/term.ml

+include Termbase
+
+let map f t = 
+  let rec aux t =
+    let t = match t.node with
+    | BVar _ -> assert false
+    | Var _ -> t
+    | App (t1,t2) -> app (aux t1) (aux t2)
+    | Tuple (t1,t2) -> tuple (aux t1) (aux t2)
+    | Case (t,c) -> 
+        let p,nl,t = open_case c in
+        case t p nl (aux t)
+    | Lam (ty,b) -> 
+        let n,t = open_lam b in
+        lam n ty (aux t) in
+    f t in
+  aux t
+

src/term.mli

+type node = Termbase.node = private
+  | BVar of int * int
+  | Var of Name.t
+  | Tuple of t * t
+  | App of t * t
+  | Lam of Ty.t * varbind
+  | Case of t * case
+and t = Termbase.t = private { tag : int ; node : node }
+and varbind = Termbase.varbind
+and pattern = Termbase.pattern = private
+  | PBVar of int
+  | PVar of Name.t
+  | PTuple of pattern * pattern
+  | Wildcard
+and case = Termbase.case
+
+type decl = Termbase.decl =
+  | Logic of Name.t * Ty.scheme
+  | Formula of poly_term
+and poly_term = Termbase.poly_term
+
+val lam : Name.t -> Ty.t -> t -> t
+val app : t -> t -> t
+val var : Name.t -> t
+val equal : t -> t -> bool
+val alpha_equal : t -> t -> bool
+val case : t -> pattern -> Name.t list -> t -> t
+val tuple : t -> t -> t
+
+val map : (t -> t) -> t -> t
+
+val print : Format.formatter -> t -> unit
+
+val wildcard : pattern
+val pvar : Name.t -> pattern
+val ptuple : pattern -> pattern -> pattern
+
+val open_lam : varbind -> Name.t * t
+
+val open_polyterm : poly_term -> Name.t list * t
+val close_polyterm : Name.t list -> t -> poly_term
+
+val open_case : case -> pattern * Name.t list * t
+val close_case : pattern -> Name.t list -> t -> case
+

src/termbase.ml

+type node = 
+  | BVar of int * int
+  | Var of Name.t
+  | Tuple of t * t
+  | App of t * t
+  | Lam of Ty.t * varbind
+  | Case of t * case
+and t = { tag : int ; node : node }
+and varbind = Name.t list * t
+and pattern = 
+  | PBVar of int
+  | PVar of Name.t
+  | PTuple of pattern * pattern
+  | Wildcard
+and case = pattern * varbind
+type decl = 
+  | Logic of Name.t * Ty.scheme
+  | Formula of poly_term
+
+and poly_term = Name.t list * t
+
+module TBase = struct
+  type node' = node 
+  type node = node'
+  type t' = t
+  type t = t'
+
+  let rec equal n1 n2 = 
+    match n1, n2 with 
+    | BVar (i1,j1), BVar (i2,j2) -> i1 = i2 && j1 = j2
+    | App (ta1, ta2), App (tb1, tb2) 
+    | Tuple (ta1, ta2), Tuple (tb1, tb2) -> 
+        equal_t ta1 tb1 && equal_t ta2 tb2
+    | Lam (ty1, (n1,t1)), Lam (ty2, (n2,t2)) -> 
+         equal_names n1 n2 && equal_t t1 t2 && Ty.hc_equal ty1 ty2
+    | Var n1, Var n2 -> Name.equal n1 n2
+    | Case (ta,(p1,(n1,t1))), Case (tb,(p2,(n2,t2))) ->
+        equal_t ta tb && equal_pattern p1 p2 && 
+        equal_names n1 n2 && equal_t t1 t2
+    | BVar _, _ | _, BVar _ -> false
+    | Var _, _ | _, Var _ -> false
+    | App _, _ | _, App _ -> false
+    | Tuple _, _ | _, Tuple _ -> false
+    | Lam _, _ | _, Lam _ -> false
+
+  and equal_t t1 t2 = t1 == t2
+  and equal_names l1 l2 = List.for_all2 Name.equal l1 l2
+  and equal_pattern p1 p2 = 
+    match p1, p2 with
+    | Wildcard, Wildcard -> true
+    | PBVar i1, PBVar i2 -> i1 = i2
+    | PVar n1, PVar n2 -> Name.equal n1 n2
+    | PTuple (ta1, ta2), PTuple (tb1, tb2) -> 
+        equal_pattern ta1 tb1 && equal_pattern ta2 tb2
+    | Wildcard, _ | _, Wildcard -> false
+    | PVar _, _ | _ , PVar _ -> false
+    | PBVar _, _| _ , PBVar _ -> false
+
+  let node t = t.node
+
+  open Misc
+  let rec hash_pattern p = 
+    match p with
+    | PBVar i -> combine 7 (hash_int i)
+    | PVar n -> combine 8 (Name.hash n)
+    | PTuple (p1,p2) -> combine2 9 (hash_pattern p1) (hash_pattern p2)
+    | Wildcard -> combine 10 11
+
+  let hash_name_list = 
+    List.fold_left (fun acc n -> combine2 4 (Name.hash n) acc)
+
+  let hash n = 
+    match n with
+    | BVar (i,j) -> combine2 1 (hash_int i) (hash_int j)
+    | Var n -> combine 2 (Name.hash n)
+    | App (t1,t2) -> combine2 3 t1.tag t2.tag
+    | Lam (ty,(n,t)) -> combine2 12 (hash_name_list t.tag n) (Ty.hash ty)
+    | Tuple (t1,t2) -> combine2 5 t1.tag t2.tag
+    | Case (t,(p,(nl,t2))) -> 
+        combine3 6 t.tag (hash_pattern p) (hash_name_list t2.tag nl)
+end
+
+module HTerms = Hashcons.Make(TBase)
+
+let equal a b = a.tag = b.tag
+let mk_t n t = { tag = t; node = n }
+let var n = HTerms.hashcons (Var n) mk_t
+let bvar i j = HTerms.hashcons (BVar (i,j)) mk_t
+let app t1 t2 = HTerms.hashcons (App (t1,t2)) mk_t
+let tuple t1 t2 = HTerms.hashcons (Tuple (t1,t2)) mk_t
+let raw_lam t b = HTerms.hashcons (Lam (t,b)) mk_t
+let raw_case t p b = HTerms.hashcons (Case (t, (p, b))) mk_t
+
+let build_map nl = 
+  let m,_ = 
+    List.fold_left (fun (m, i) n -> Name.M.add n i m, i + 1) 
+      (Name.M.empty, 0) nl in
+  m
+
+let abstract nl t = 
+  let m = build_map nl in
+  let rec aux i t = 
+    match t.node with
+    | Var n' ->
+        begin try let j = Name.M.find n' m in bvar i j
+        with Not_found -> t end
+    | BVar _ -> t
+    | App (t1,t2) -> app (aux i t1) (aux i t2)
+    | Tuple (t1,t2) -> tuple (aux i t1) (aux i t2)
+    | Lam (ty, (nl,t)) -> raw_lam ty (nl, aux (i+1) t)
+    | Case (ta,(p,(nl,t))) -> raw_case (aux i ta) p (nl, aux (i+1) t) in
+  aux 0 t
+
+let abstract_pattern nl p = 
+  let m = build_map nl in
+  let rec aux p = 
+    match p with
+    | PVar n ->
+        begin try let i = Name.M.find n m in PBVar i
+        with Not_found -> p end
+    | PBVar _ | Wildcard -> p
+    | PTuple (p1,p2) -> PTuple (aux p1, aux p2) in
+  aux p
+
+
+let instantiate tl t = 
+  let rec aux i t = 
+    match t.node with
+    | BVar (i',j) when i = i' -> List.nth tl j
+    | BVar _ | Var _ -> t
+    | App (t1,t2) -> app (aux i t1) (aux i t2)
+    | Tuple (t1,t2) -> tuple (aux i t1) (aux i t2)
+    | Lam (ty, (n,t)) -> raw_lam ty (n, aux (i+1) t) 
+    | Case (t1, (p,(nl,t2))) -> raw_case (aux i t1) p (nl, aux (i+1) t) in
+  aux 0 t
+
+let instantiate_pattern pl p =
+  let rec aux p = 
+    match p with
+    | PBVar i -> List.nth pl i
+    | PVar _ | Wildcard -> p
+    | PTuple (p1,p2) -> PTuple (aux p1, aux p2) in
+  aux p
+
+open Format
+let rec print env fmt t = 
+  match t.node with
+  | BVar (i,j) -> 
+      begin try Name.print fmt (List.nth (List.nth env i) j)
+      with Invalid_argument "List.nth" -> fprintf fmt "{{%d,%d}}" i j end
+  | Var n -> Name.print fmt n
+  | App (t1,t2) -> fprintf fmt "%a %a" (print env) t1 (paren env) t2
+  | Tuple (t1,t2) -> fprintf fmt "(%a, %a)" (print env) t1 (print env) t2
+  | Lam (ty, (n,t)) -> 
+      fprintf fmt "(λ%a : %a . %a)" 
+        (Misc.print_list Misc.comma Name.print) n 
+        (Ty.print []) ty 
+        (print (n::env)) t
+  | Case (t1, (p,(n,t2))) ->
+      fprintf fmt "case %a of %a -> %a" (print env) t1 (print_pattern n) p 
+        (print (n::env)) t2
+and paren env fmt t = 
+  if is_compound t then fprintf fmt "(%a)" (print env) t else print env fmt t
+and is_compound t = 
+  (* decide if this term has to be printed with parens in some contexts *)
+  match t.node with
+  | BVar _ | Var _ | Lam _ | Tuple _ -> false
+  | App _ | Case _ -> true
+and print_pattern l fmt p = 
+  match p with
+  | PBVar i -> 
+      begin try Name.print fmt (List.nth l i)
+      with Invalid_argument "List.nth" -> fprintf fmt "{{%d}}" i end
+  | PVar v -> Name.print fmt v
+  | PTuple (t1,t2) -> 
+      fprintf fmt "(%a, %a)" (print_pattern l) t1 (print_pattern l) t2
+  | Wildcard -> fprintf fmt "_"
+
+let print = print [] 
+
+let rec alpha_equal a b = 
+  if equal a b then true else
+    match a.node, b.node with
+    | BVar (i1,j1), BVar (i2,j2) -> i1 = i2 && j1 = j2
+    | Var n1, Var n2 -> Name.equal n1 n2
+    | App (ta1, ta2), App (tb1, tb2)
+    | Tuple (ta1, ta2), Tuple (tb1, tb2) ->
+        alpha_equal ta1 tb1 && alpha_equal ta2 tb2
+    | Lam (ty1, (_,t1)), Lam (ty2, (_,t2)) -> 
+        Ty.equal ty1 ty2 && alpha_equal t1 t2
+    | Case (ta,(p1,(_,t1))), (Case (tb, (p2,(_,t2)))) ->
+        alpha_equal ta tb && TBase.equal_pattern p1 p2 && alpha_equal t1 t2
+    | BVar _, _ | _, BVar _ -> false
+    | Var _, _ | _, Var _ -> false
+    | App _, _ | _, App _ -> false
+    | Tuple _, _ | _, Tuple _ -> false
+    | Lam _, _ | _, Lam _ -> false
+
+
+let unsafe_map ~tyfun ~termfun t = 
+  let rec aux t = 
+    let t = match t.node with
+    | BVar _ | Var _ -> t
+    | App (t1,t2) -> app (aux t1) (aux t2)
+    | Tuple (t1,t2) -> tuple (aux t1) (aux t2)
+    | Case (t1, (p,(n,t2))) -> raw_case (aux t1) p (n,aux t2)
+    | Lam (ty, (n,t)) -> raw_lam (tyfun ty) (n, aux t) in
+    termfun t in
+  aux t
+
+let open_ (n,t) = n, instantiate (List.map var n) t
+
+let close n t = 
+  let n' = List.map Name.fresh n in
+  n', abstract n t
+
+let lam n ty t = raw_lam ty (close [n] t)
+
+let open_case (p,(nl,t)) = 
+  let pl = List.map (fun n -> PVar n) nl in
+  let tl = List.map var nl in
+  instantiate_pattern pl p, nl, instantiate tl t
+
+let close_case p nl t = 
+  let nl' = List.map Name.fresh nl in
+  abstract_pattern nl p, (nl', abstract nl t)
+
+let case t1 p nl t2 = 
+  let p, b = close_case p nl t2 in
+  raw_case t1 p b
+
+let wildcard = Wildcard
+let pvar x = PVar x
+let ptuple p1 p2 = PTuple (p1,p2)
+
+let open_polyterm (nl,t) = 
+  let tl = List.map Ty.var nl in
+  nl, unsafe_map ~tyfun:(Ty.instantiate tl) ~termfun:(fun x -> x) t
+
+let close_polyterm nl t = 
+  let nl' = List.map Name.fresh nl in
+  nl', unsafe_map ~tyfun:(Ty.abstract nl) ~termfun:(fun x -> x) t
+
+let open_lam b = 
+  let nl, t = open_ b in
+  List.hd nl, t

src/termbase.mli

+type node = private
+  | BVar of int * int
+  | Var of Name.t
+  | Tuple of t * t
+  | App of t * t
+  | Lam of Ty.t * varbind
+  | Case of t * case
+and t = private { tag : int ; node : node }
+and varbind
+and pattern = private
+  | PBVar of int
+  | PVar of Name.t
+  | PTuple of pattern * pattern
+  | Wildcard
+and case
+
+type decl = 
+  | Logic of Name.t * Ty.scheme
+  | Formula of poly_term
+and poly_term
+
+(** smart constructors *)
+val lam : Name.t -> Ty.t -> t -> t
+val app : t -> t -> t
+val tuple : t -> t -> t
+val var : Name.t -> t
+val equal : t -> t -> bool
+val alpha_equal : t -> t -> bool
+val case : t -> pattern -> Name.t list -> t -> t
+
+val open_case : case -> pattern * Name.t list * t
+val close_case : pattern -> Name.t list -> t -> case
+
+val unsafe_map : 
+  tyfun:(Ty.t -> Ty.t) ->
+  termfun:(t -> t) -> t -> t
+(** [unsafe_map f t] recursively descends into [t] and then applies [f]
+   everywhere going up; This function is unsafe in the sense that you might
+   encounter [BVar] constructors. Only use it for simple rewriting that does not
+   affect names, or does only affect global variables *)
+
+val print : Format.formatter -> t -> unit
+
+val wildcard : pattern
+val pvar : Name.t -> pattern
+val ptuple : pattern -> pattern -> pattern
+
+val open_polyterm : poly_term -> Name.t list * t
+val close_polyterm : Name.t list -> t -> poly_term
+
+val open_lam : varbind -> Name.t * t

src/ty.ml

+type node = 
+  | BVar of int
+  | Var of Name.t
+  | Tuple of t * t
+  | Arrow of t * t
+and t = {tag : int ; node : node }
+and scheme = Name.t list * t
+
+module Base = struct
+  type node' = node 
+  type node = node'
+  type t' = t
+  type t = t'
+
+  let rec equal t1 t2 = 
+    match t1, t2 with
+    | Var n1, Var n2 -> Name.equal n1 n2
+    | BVar (i1), BVar (i2) -> i1 = i2
+    | Tuple (ta1, ta2), Tuple (tb1, tb2)
+    | Arrow (ta1, ta2), Arrow (tb1, tb2) -> 
+        equal_t ta1 tb1 && equal_t ta2 tb2
+    | Var _, _ | _, Var _ -> false
+    | BVar _, _ | _, BVar _ -> false
+    | Tuple _, _ | _, Tuple _ -> false
+  and equal_t t1 t2 = t1 == t2
+
+  let node t = t.node
+
+  open Misc
+
+  let hash n = 
+    match n with
+    | BVar (i) -> combine 1 (hash_int i)
+    | Var n -> combine 2 (Name.hash n)
+    | Arrow (t1,t2) -> combine2 3 t1.tag t2.tag
+    | Tuple (t1,t2) -> combine2 5 t1.tag t2.tag
+end
+
+let hc_equal = Base.equal_t
+let hash t = t.tag
+
+module HBase = Hashcons.Make (Base)
+
+let mk_t n t = { tag = t; node = n }
+let bvar i = HBase.hashcons (BVar (i)) mk_t
+let var v = HBase.hashcons (Var v) mk_t
+let tuple t1 t2 = HBase.hashcons (Tuple (t1,t2)) mk_t
+let arrow t1 t2 = HBase.hashcons (Arrow (t1,t2)) mk_t
+
+let map f t = 
+  let rec aux t = 
+    let t =
+      match t.node with
+      | Var _ | BVar _  -> t
+      | Tuple (t1,t2) -> tuple (aux t1) (aux t2)
+      | Arrow (t1,t2) -> arrow (aux t1) (aux t2) in
+    f t in
+  aux t
+
+let abstract nl = 
+  let m = Name.build_map nl in
+  let f t = match t.node with
+  | Var n -> 
+      begin try let i = Name.M.find n m in bvar i
+      with Not_found -> t end
+  | _ -> t in
+  map f
+
+let instantiate tl =
+  let f t = match t.node with
+  | BVar i -> List.nth tl i
+  | _ -> t in
+  map f
+
+open Format
+
+let rec print tenv fmt t = 
+  match t.node with
+  | BVar i -> 
+      begin try Name.print fmt (List.nth tenv i)
+      with Invalid_argument "List.nth" -> Format.printf "{{%d}}" i end
+  | Var n -> Name.print fmt n
+  | Tuple (t1,t2) -> fprintf fmt "%a * %a" (print tenv) t1 (print tenv) t2
+  | Arrow (t1,t2) -> fprintf fmt "%a -> %a" (print tenv) t1 (paren tenv) t2
+and is_compound t = 
+  match t.node with
+  | Arrow _ -> true
+  | BVar _ | Var _ | Tuple _ -> false
+and paren tenv fmt t = 
+  if is_compound t then fprintf fmt "(%a)" (print tenv) t 
+  else print tenv fmt t
+
+let equal a b = a == b
+
+let open_ (nl,t) = 
+  let tl = List.map var nl in
+  nl, instantiate tl t 
+
+let close nl t = 
+  let nl' = List.map Name.fresh nl in
+  nl', abstract nl t
+
+let as_scheme t = [],t
+
+let instantiate_scheme tl (_,t) =