Commit ab6e7358 authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

No commit message

No commit message
parent a981758e
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
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 ","
......@@ -165,24 +165,12 @@ module Pattern = struct
end
module Hpattern = Hashcons.Make(Pattern)
(* let pat_vars acc0 p = *)
(* Name.M.fold *)
(* (fun x ty acc -> assert (not (Name.M.mem x acc0)); Name.M.add x ty acc) *)
(* p.pat_vars acc0 *)
(* let patn_vars acc = function *)
(* | Pwild -> acc *)
(* | Pvar (n, ty) -> assert (not (Name.M.mem n acc)); Name.M.add n ty acc *)
(* | Papp (_, pl) -> List.fold_left pat_vars acc pl *)
(* | Pas (p, n) -> assert (not (Name.S.mem n acc)); pat_vars (Name.S.add n acc) p *)
let mk_pattern n ty = { pat_node = n; pat_ty = ty; pat_tag = -1 }
let pat_wild ty = Hpattern.hashcons (mk_pattern Pwild ty)
let pat_var n ty = Hpattern.hashcons (mk_pattern (Pvar n) ty)
let pat_app f pl ty = Hpattern.hashcons (mk_pattern (Papp (f, pl)) ty)
let pat_as p n = Hpattern.hashcons (mk_pattern (Pas (p, n)) p.pat_ty)
type term = {
t_node : term_node;
t_label : label list;
......@@ -389,46 +377,46 @@ let f_label_add l f = Hfmla.hashcons { f with f_label = l :: f.f_label }
let name_map_cardinal m = Name.M.fold (fun _ _ acc -> acc + 1) m 0
(* replaces named variables [v] in term [t] by de Bruijn index 0 *)
let rec abs_term lvl v ty t = match t.t_node with
(* replaces named variables by de Bruijn indices in term [t]
using a map [m] *)
let rec abs_term lvl m t = match t.t_node with
| Tbvar _ ->
t
| Tvar u when Name.equal u v ->
assert (t.t_ty == ty); t_bvar lvl ty
| Tvar _ ->
t
| Tvar u ->
(try let i = Name.M.find u m in t_bvar (i + lvl) t.t_ty
with Not_found -> t)
| Tapp (f, tl) ->
t_app f (List.map (abs_term lvl v ty) tl) t.t_ty
t_app f (List.map (abs_term lvl m) tl) t.t_ty
| Tcase (t1, bl) ->
t_case (abs_term lvl v ty t1) (List.map (abs_tbranch lvl v ty) bl) t.t_ty
t_case (abs_term lvl m t1) (List.map (abs_tbranch lvl m) bl) t.t_ty
| Tlet (t1, (u, _, t2)) ->
t_let u (abs_term lvl v ty t1) (abs_term (lvl + 1) v ty t2)
t_let u (abs_term lvl m t1) (abs_term (lvl + 1) m t2)
| Teps (u, tyu, f) ->
t_eps u tyu (abs_fmla (lvl + 1) v ty f)
t_eps u tyu (abs_fmla (lvl + 1) m f)
and abs_tbranch lvl v ty (pat, m, t) =
(pat, m, abs_term (lvl + m) v ty t)
and abs_tbranch lvl m (pat, nv, t) =
(pat, nv, abs_term (lvl + nv) m t)
and abs_fmla lvl v ty f = match f.f_node with
and abs_fmla lvl m f = match f.f_node with
| Fapp (p, tl) ->
f_app p (List.map (abs_term lvl v ty) tl)
f_app p (List.map (abs_term lvl m) tl)
| Fquant (q, (u, tyu, f1)) ->
f_quant q u tyu (abs_fmla (lvl + 1) v ty f1)
f_quant q u tyu (abs_fmla (lvl + 1) m f1)
| Fbinop (op, f1, f2) ->
f_binary op (abs_fmla lvl v ty f1) (abs_fmla lvl v ty f2)
f_binary op (abs_fmla lvl m f1) (abs_fmla lvl m f2)
| Funop (op, f1) ->
f_unary op (abs_fmla lvl v ty f1)
f_unary op (abs_fmla lvl m f1)
| Ftrue | Ffalse ->
f
| Fif (f1, f2, f3) ->
f_if (abs_fmla lvl v ty f1) (abs_fmla lvl v ty f2) (abs_fmla lvl v ty f3)
f_if (abs_fmla lvl m f1) (abs_fmla lvl m f2) (abs_fmla lvl m f3)
| Flet (t, (u, _, f1)) ->
f_let u (abs_term lvl v ty t) (abs_fmla (lvl + 1) v ty f1)
f_let u (abs_term lvl m t) (abs_fmla (lvl + 1) m f1)
| Fcase (t, bl) ->
f_case (abs_term lvl v ty t) (List.map (abs_fbranch lvl v ty) bl)
f_case (abs_term lvl m t) (List.map (abs_fbranch lvl m) bl)
and abs_fbranch lvl v ty (pat, m, f) =
(pat, m, abs_fmla (lvl + m) v ty f)
and abs_fbranch lvl m (pat, nv, f) =
(pat, nv, abs_fmla (lvl + nv) m f)
(* applies substitution [s] (mapping de Bruijn variables to terms) to [t2] *)
......@@ -450,7 +438,8 @@ let rec subst_term lvl s t = match t.t_node with
| Tbvar n when n < lvl ->
t
| Tbvar n ->
(try Subst.find (n - lvl) s with Not_found -> assert false)
(try t_var (Subst.find (n - lvl) s) t.t_ty
with Not_found -> assert false)
| Tvar _ ->
t
| Tapp (f, tl) ->
......@@ -462,8 +451,8 @@ let rec subst_term lvl s t = match t.t_node with
| Teps (u, tyu, f) ->
t_eps u tyu (subst_fmla (lvl + 1) s f)
and subst_tbranch lvl s (pat, m, t) =
(pat, m, subst_term (lvl + m) s t)
and subst_tbranch lvl s (pat, nv, t) =
(pat, nv, subst_term (lvl + nv) s t)
and subst_fmla lvl s f = match f.f_node with
| Fapp (p, tl) ->
......@@ -483,29 +472,59 @@ and subst_fmla lvl s f = match f.f_node with
| Fcase (t, bl) ->
f_case (subst_term lvl s t) (List.map (subst_fbranch lvl s) bl)
and subst_fbranch lvl s (pat, m, f) =
(pat, m, subst_fmla (lvl + m) s f)
and subst_fbranch lvl s (pat, nv, f) =
(pat, nv, subst_fmla (lvl + nv) s f)
(* smart constructors *)
let t_let v t1 t2 = t_let v t1 (abs_term 0 v t1.t_ty t2)
let t_eps v ty f = t_eps v ty (abs_fmla 0 v ty f)
let name_map_singleton v = Name.M.add v 0 Name.M.empty
let t_let v t1 t2 = t_let v t1 (abs_term 0 (name_map_singleton v) t2)
let t_eps v ty f = t_eps v ty (abs_fmla 0 (name_map_singleton v) f)
let t_app f tl = assert false (*TODO*)
let t_case t bl = assert false (*TODO*)
let f_quant q v ty f = f_quant q v ty (abs_fmla 0 v ty f)
let varmap_for_pattern p =
let i = ref (-1) in
let rec make acc p = match p.pat_node with
| Pwild ->
acc
| Pvar n ->
assert (not (Name.M.mem n acc));
incr i; Name.M.add n !i acc
| Papp (_, pl) ->
List.fold_left make acc pl
| Pas (p, n) ->
assert (not (Name.M.mem n acc));
incr i; make (Name.M.add n !i acc) p
in
let m = make Name.M.empty p in
m, !i + 1
let t_case t bl =
let make_tbranch (p, t) =
let m, nv = varmap_for_pattern p in (p, nv, abs_term 0 m t)
in
t_case t (List.map make_tbranch bl)
let f_quant q v ty f = f_quant q v ty (abs_fmla 0 (name_map_singleton v) f)
let f_forall = f_quant Fforall
let f_exists = f_quant Fexists
let f_let v t1 f2 = f_let v t1 (abs_fmla 0 v t1.t_ty f2)
let f_case t bl = assert false (*TODO*)
let f_let v t1 f2 = f_let v t1 (abs_fmla 0 (name_map_singleton v) f2)
let f_app s tl = assert false (*TODO*)
let f_case t bl =
let make_fbranch (p, f) =
let m, nv = varmap_for_pattern p in (p, nv, abs_fmla 0 m f)
in
f_case t (List.map make_fbranch bl)
(* opening binders *)
let open_bind_term (v, ty, t) =
let v = Name.fresh v in
v, ty, subst_term 0 (Subst.singleton (t_var v ty)) t
v, ty, subst_term 0 (Subst.singleton v) t
let rec subst_pat ns p = match p.pat_node with
| Pwild ->
......@@ -518,27 +537,26 @@ let rec subst_pat ns p = match p.pat_node with
pat_as (subst_pat ns p)
(try Name.M.find n ns with Not_found -> assert false)
let substs_for_pat m =
let i = ref (-1) in
let substs_for_pat pat =
let m, _ = varmap_for_pattern pat in
Name.M.fold
(fun x ty (s, ns) ->
incr i;
(fun x i (vars, s, ns) ->
let x' = Name.fresh x in
Subst.add !i (t_var x' ty) s, Name.M.add x x' ns)
Name.S.add x' vars, Subst.add i x' s, Name.M.add x x' ns)
m
(Subst.empty, Name.M.empty)
(Name.S.empty, Subst.empty, Name.M.empty)
let open_tbranch (pat, m, t) =
let s, ns = substs_for_pat m in
(subst_pat ns pat, subst_term 0 s t)
let open_tbranch (pat, _, t) =
let vars, s, ns = substs_for_pat pat in
(subst_pat ns pat, vars, subst_term 0 s t)
let open_bind_fmla (v, ty, f) =
let v = Name.fresh v in
v, ty, subst_fmla 0 (Subst.singleton (t_var v ty)) f
v, ty, subst_fmla 0 (Subst.singleton v) f
let open_fbranch (pat, m, f) =
let s, ns = substs_for_pat m in
(subst_pat ns pat, subst_fmla 0 s f)
let open_fbranch (pat, _, f) =
let vars, s, ns = substs_for_pat pat in
(subst_pat ns pat, vars, subst_fmla 0 s f)
(* TODO : substitution functions named variables -> terms
......
......@@ -75,19 +75,19 @@ type unop =
type term = private {
t_node : term_node;
t_label : label;
t_label : label list;
t_ty : ty;
t_tag : int;
}
and fmla = private {
f_node : fmla_node;
f_label : label;
f_label : label list;
f_tag : int;
}
and term_node = private
| Tbvar of int * int
| Tbvar of int
| Tvar of vsymbol
| Tapp of fsymbol * term list
| Tcase of term * tbranch list
......@@ -118,7 +118,7 @@ and fbranch
type pattern = private {
pat_node : pattern_node;
pat_vars : vsymbol_set;
pat_ty : ty;
pat_tag : int;
}
......@@ -128,16 +128,16 @@ and pattern_node = private
| Papp of fsymbol * pattern list
| Pas of pattern * vsymbol
val pat_wild : pattern
val pat_wild : ty -> pattern
val pat_var : vsymbol -> ty -> pattern
val pat_app : fsymbol -> pattern list -> pattern
val pat_app : fsymbol -> pattern list -> ty -> pattern
val pat_as : pattern -> vsymbol -> pattern
(* smart constructors for term *)
val t_var : vsymbol -> ty -> term
val t_app : fsymbol -> term list -> term
val t_case : term -> (pattern * term) list -> term
val t_app : fsymbol -> term list -> ty -> term
val t_case : term -> (pattern * term) list -> ty -> term
val t_let : vsymbol -> term -> term -> term
val t_eps : vsymbol -> ty -> fmla -> term
......@@ -172,11 +172,11 @@ val f_label_add : label -> fmla -> fmla
(* bindings *)
val open_bind_term : bind_term -> vsymbol * term
val open_tbranch : tbranch -> pattern * term
val open_bind_term : bind_term -> vsymbol * ty * term
val open_tbranch : tbranch -> pattern * vsymbol_set * term
val open_bind_fmla : bind_fmla -> vsymbol * fmla
val open_fbranch : fbranch -> pattern * fmla
val open_bind_fmla : bind_fmla -> vsymbol * ty * fmla
val open_fbranch : fbranch -> pattern * vsymbol_set * fmla
(* equality *)
......
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
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) = instantiate tl t
let prop = var (Name.from_string "prop")
let split t =
match t.node with
| Arrow (t1,t2) -> t1,t2
| _ -> failwith "not an arrow"
let tuple_split t =
match t.node with
| Tuple (t1,t2) -> t1,t2
| _ -> failwith "not a tuple"
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
type node= private
| BVar of int
| Var of Name.t
| Tuple of t * t
| Arrow of t * t
and t =
private {tag : int ; node : node }
and scheme
val hc_equal : t -> t -> bool
val hash : t -> int
val print : Name.t list -> Format.formatter -> t -> unit
val equal : t -> t -> bool
val var : Name.t -> t
val tuple : t -> t -> t
val arrow : t -> t -> t
val instantiate_scheme : t list -> scheme -> t
val open_ : scheme -> Name.t list * t
val close : Name.t list -> t -> scheme
val as_scheme : t -> scheme
(** internal use *)
val abstract : Name.t list -> t -> t
val instantiate : t list -> t -> t
val prop : t
val split : t -> t * t
val tuple_split : t -> t * t
(**************************************************************************)
(* *)
(* Copyright (C) Francois Bobot, Jean-Christophe Filliatre, *)
(* Johannes Kanig and Andrei Paskevich. *)
(* *)
(* This software is free software; you can redistribute it and/or *)
(* modify it under the terms of the GNU Library General Public *)
(* License version 2.1, with the special exception on linking *)
(* described in file LICENSE. *)
(* *)
(* This software is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *)
(* *)
(**************************************************************************)
open Term
module Env : sig
type t
val empty : t
val add : t -> Name.t -> Ty.scheme -> t
val get : t -> Name.t -> Ty.scheme
val mem : t -> Name.t -> bool
end = struct
module M = Name.M
type t = Ty.scheme M.t
let add env x t = M.add x t env
let get env x = M.find x env
let mem env x = M.mem x env
let empty = M.empty
end
let rec infer_term env t =
match t.node with
| BVar _ -> failwith "encountered bound variable"
| Var n ->
begin try Obj.magic (Env.get env n)
with Not_found -> failwith "unknown variable" end
| App (t1,t2) ->
let ty1 = infer_term env t1 in
let ta,tb = Ty.split ty1 in
check_term env ta t2; tb
| Tuple (t1,t2) ->
let ty1 = infer_term env t1 in
let ty2 = infer_term env t2 in
Ty.tuple ty1 ty2
| Lam (ty,b) ->
let n,t = open_lam b in
let env = Env.add env n (Ty.as_scheme ty) in
let ty' = infer_term env t in
Ty.arrow ty ty'
| Case (t1,c) ->
let ty1 = infer_term env t1 in
let p,nl,t2 = open_case c in
let env = check_pattern env ty1 p in
infer_term env t2
and check_term env ty t =
let t = infer_term env t in
if Ty.equal t ty then () else failwith "expected term of other type"
and check_pattern env ty p =
match p with
| PBVar _ -> assert false
| PVar n ->
if not (Env.mem env n) then Env.add env n (Ty.as_scheme ty)
else failwith "nonlinear pattern"
| Wildcard -> env
| PTuple (p1,p2) ->
let ty1,ty2 = Ty.tuple_split ty in
let env = check_pattern env ty1 p1 in
check_pattern env ty2 p2
let check_polyterm env ty p =
let _,t = open_polyterm p in
check_term env ty t
let decl env d =
match d with
| Logic (n,s) -> Env.add env n s
| Formula p ->