Skip to content

GitLab

Commit 4d6154fd authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

rebranch from Name to Ident, feel free to revert

parent bbd30c19
Hide whitespace changes
Inline Side-by-side
Showing with 129 additions and 101 deletions
src/core/term.ml
View file @ 4d6154fd
......@@ -18,20 +18,21 @@
(**************************************************************************)
open Util
open Ident
open Ty
(** Variable symbols *)
type vsymbol = {
vs_name : Name.t;
vs_name : ident;
vs_ty : ty;
vs_tag : int;
}
module Vsym = struct
type t = vsymbol
let equal vs1 vs2 = Name.equal vs1.vs_name vs2.vs_name
let hash vs = Name.hash vs.vs_name
let equal vs1 vs2 = vs1.vs_name == vs2.vs_name
let hash vs = vs.vs_name.id_tag
let tag n vs = { vs with vs_tag = n }
let compare vs1 vs2 = Pervasives.compare vs1.vs_tag vs2.vs_tag
end
......@@ -43,13 +44,12 @@ module Svs = Set.Make(Vsym)
let mk_vs name ty = { vs_name = name; vs_ty = ty; vs_tag = -1 }
let create_vsymbol name ty = Hvs.hashcons (mk_vs name ty)
(* TODO: needs refactoring *)
let fresh_vsymbol v = create_vsymbol (Name.fresh v.vs_name) v.vs_ty
let fresh_vsymbol v = create_vsymbol (id_clone v.vs_name) v.vs_ty
(** Function symbols *)
type fsymbol = {
fs_name : Name.t;
fs_name : ident;
fs_scheme : ty list * ty;
fs_constr : bool;
fs_tag : int;
......@@ -57,8 +57,8 @@ type fsymbol = {
module Fsym = struct
type t = fsymbol
let equal fs1 fs2 = Name.equal fs1.fs_name fs2.fs_name
let hash fs = Name.hash fs.fs_name
let equal fs1 fs2 = fs1.fs_name == fs2.fs_name
let hash fs = fs.fs_name.id_tag
let tag n fs = { fs with fs_tag = n }
let compare fs1 fs2 = Pervasives.compare fs1.fs_tag fs2.fs_tag
end
......@@ -78,15 +78,15 @@ let create_fsymbol name scheme constr = Hfs.hashcons (mk_fs name scheme constr)
(** Predicate symbols *)
type psymbol = {
ps_name : Name.t;
ps_name : ident;
ps_scheme : ty list;
ps_tag : int;
}
module Psym = struct
type t = psymbol
let equal ps1 ps2 = Name.equal ps1.ps_name ps2.ps_name
let hash ps = Name.hash ps.ps_name
let equal ps1 ps2 = ps1.ps_name == ps2.ps_name
let hash ps = ps.ps_name.id_tag
let tag n ps = { ps with ps_tag = n }
let compare ps1 ps2 = Pervasives.compare ps1.ps_tag ps2.ps_tag
end
......@@ -133,7 +133,7 @@ module Hpat = struct
| Papp (s, pl) -> Hashcons.combine_list hash_pattern s.fs_tag pl
| Pas (p, v) -> Hashcons.combine (hash_pattern p) v.vs_tag
let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.Ty.ty_tag
let hash p = Hashcons.combine (hash_node p.pat_node) p.pat_ty.ty_tag
let tag n p = { p with pat_tag = n }
......@@ -176,15 +176,15 @@ let pat_app f pl ty =
if not f.fs_constr then raise ConstructorExpected else
let args, res = f.fs_scheme in
let _ =
try List.fold_left2 Ty.matching
(Ty.matching Name.M.empty res ty)
try List.fold_left2 matching
(matching Mid.empty res ty)
args (List.map (fun p -> p.pat_ty) pl)
with Invalid_argument _ -> raise BadArity
in
pat_app f pl ty
let pat_as p v =
if p.pat_ty == v.vs_ty then pat_as p v else raise Ty.TypeMismatch
if p.pat_ty == v.vs_ty then pat_as p v else raise TypeMismatch
(* safe map over patterns *)
......@@ -305,7 +305,7 @@ module T = struct
let hash t =
Hashcons.combine (t_hash_node t.t_node)
(Hashcons.combine_list Hashtbl.hash t.t_ty.Ty.ty_tag t.t_label)
(Hashcons.combine_list Hashtbl.hash t.t_ty.ty_tag t.t_label)
let tag n t = { t with t_tag = n }
......@@ -540,13 +540,13 @@ and f_subst m lvl f = f_map_unsafe (t_subst m) (f_subst m) lvl f
let t_subst_single v t1 t =
if v.vs_ty == t1.t_ty then t_subst (Mvs.add v t1 Mvs.empty) 0 t
else raise Ty.TypeMismatch
else raise TypeMismatch
let f_subst_single v t1 f =
if v.vs_ty == t1.t_ty then f_subst (Mvs.add v t1 Mvs.empty) 0 f
else raise Ty.TypeMismatch
else raise TypeMismatch
let vt_check v t = if v.vs_ty == t.t_ty then () else raise Ty.TypeMismatch
let vt_check v t = if v.vs_ty == t.t_ty then () else raise TypeMismatch
let t_subst m t = let _ = Mvs.iter vt_check m in t_subst m 0 t
let f_subst m f = let _ = Mvs.iter vt_check m in f_subst m 0 f
......@@ -741,11 +741,11 @@ and f_subst_term t1 t2 lvl f =
let t_subst_term t1 t2 t =
if t1.t_ty == t2.t_ty then t_subst_term t1 t2 0 t
else raise Ty.TypeMismatch
else raise TypeMismatch
let f_subst_term t1 t2 f =
if t1.t_ty == t2.t_ty then f_subst_term t1 t2 0 f
else raise Ty.TypeMismatch
else raise TypeMismatch
(* substitutes fmla [f2] for fmla [f1] in term [t] *)
......@@ -770,11 +770,11 @@ and f_subst_term_alpha t1 t2 lvl f =
let t_subst_term_alpha t1 t2 t =
if t1.t_ty == t2.t_ty then t_subst_term_alpha t1 t2 0 t
else raise Ty.TypeMismatch
else raise TypeMismatch
let f_subst_term_alpha t1 t2 f =
if t1.t_ty == t2.t_ty then f_subst_term_alpha t1 t2 0 f
else raise Ty.TypeMismatch
else raise TypeMismatch
(* substitutes fmla [f2] for fmla [f1] in term [t] modulo alpha *)
......@@ -806,7 +806,7 @@ and f_skip lvl (sT,sF,acc) f =
let rec t_map_skip fnT fnF sT sF lvl t =
if Sterm.mem t sT then let t1 = fnT t in
if (t1.t_ty == t.t_ty) then t1 else raise Ty.TypeMismatch
if (t1.t_ty == t.t_ty) then t1 else raise TypeMismatch
else t_map_unsafe (t_map_skip fnT fnF sT sF)
(f_map_skip fnT fnF sT sF) lvl t
......@@ -817,7 +817,7 @@ and f_map_skip fnT fnF sT sF lvl f =
let t_map_skip fnT fnF lvl t =
if lvl == 0 then let t1 = fnT t in
if (t1.t_ty == t.t_ty) then t1 else raise Ty.TypeMismatch
if (t1.t_ty == t.t_ty) then t1 else raise TypeMismatch
else let sT,sF,_ = t_skip lvl skip_empty t in
t_map_skip fnT fnF sT sF lvl t
......@@ -880,11 +880,11 @@ let f_exists_trans prT prF f =
let t_let v t1 t2 =
if v.vs_ty == t1.t_ty then t_let v t1 (t_abst_single v t2)
else raise Ty.TypeMismatch
else raise TypeMismatch
let f_let v t1 f2 =
if v.vs_ty == t1.t_ty then f_let v t1 (f_abst_single v f2)
else raise Ty.TypeMismatch
else raise TypeMismatch
let t_eps v f = t_eps v (f_abst_single v f)
......@@ -895,8 +895,8 @@ let f_exists = f_quant Fexists
let t_app f tl ty =
let args, res = f.fs_scheme in
let _ =
try List.fold_left2 Ty.matching
(Ty.matching Name.M.empty res ty)
try List.fold_left2 matching
(matching Mid.empty res ty)
args (List.map (fun t -> t.t_ty) tl)
with Invalid_argument _ -> raise BadArity
in
......@@ -904,7 +904,7 @@ let t_app f tl ty =
let f_app p tl =
let _ =
try List.fold_left2 Ty.matching Name.M.empty
try List.fold_left2 matching Mid.empty
p.ps_scheme (List.map (fun t -> t.t_ty) tl)
with Invalid_argument _ -> raise BadArity
in
......@@ -928,15 +928,15 @@ let pat_varmap p =
let t_case t bl ty =
let t_make_branch (p, tbr) =
if tbr.t_ty != ty then raise Ty.TypeMismatch else
if p.pat_ty != t.t_ty then raise Ty.TypeMismatch else
if tbr.t_ty != ty then raise TypeMismatch else
if p.pat_ty != t.t_ty then raise TypeMismatch else
let m, nv = pat_varmap p in (p, nv, t_abst m 0 tbr)
in
t_case t (List.map t_make_branch bl) ty
let f_case t bl =
let f_make_branch (p, fbr) =
if p.pat_ty != t.t_ty then raise Ty.TypeMismatch else
if p.pat_ty != t.t_ty then raise TypeMismatch else
let m, nv = pat_varmap p in (p, nv, f_abst m 0 fbr)
in
f_case t (List.map f_make_branch bl)
......
src/core/term.mli
View file @ 4d6154fd
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Ident
open Ty
exception NonLinear
......@@ -26,7 +27,7 @@ exception ConstructorExpected
(** Variable symbols *)
type vsymbol = private {
vs_name : Name.t;
vs_name : ident;
vs_ty : ty;
vs_tag : int;
}
......@@ -34,18 +35,18 @@ type vsymbol = private {
module Svs : Set.S with type elt = vsymbol
module Mvs : Map.S with type key = vsymbol
val create_vsymbol : Name.t -> ty -> vsymbol
val create_vsymbol : ident -> ty -> vsymbol
(** Function symbols *)
type fsymbol = private {
fs_name : Name.t;
fs_name : ident;
fs_scheme : ty list * ty;
fs_constr : bool;
fs_tag : int;
}
val create_fsymbol : Name.t -> ty list * ty -> bool -> fsymbol
val create_fsymbol : ident -> ty list * ty -> bool -> fsymbol
module Sfs : Set.S with type elt = fsymbol
module Mfs : Map.S with type key = fsymbol
......@@ -53,12 +54,12 @@ module Mfs : Map.S with type key = fsymbol
(** Predicate symbols *)
type psymbol = private {
ps_name : Name.t;
ps_name : ident;
ps_scheme : ty list;
ps_tag : int;
}
val create_psymbol : Name.t -> ty list -> psymbol
val create_psymbol : ident -> ty list -> psymbol
module Sps : Set.S with type elt = psymbol
module Mps : Map.S with type key = psymbol
......
src/core/theory.ml
View file @ 4d6154fd
......@@ -19,6 +19,7 @@
open Format
open Pp
open Ident
open Ty
open Term
......@@ -47,7 +48,7 @@ type ty_decl = tysymbol * ty_def
type logic_decl =
| Lfunction of fsymbol * (vsymbol list * term) option (* FIXME: binders *)
| Lpredicate of psymbol * (vsymbol list * fmla) option (* FIXME: binders *)
| Linductive of psymbol * (Name.t * fmla) list
| Linductive of psymbol * (ident * fmla) list
type prop_kind =
| Axiom | Lemma | Goal
......@@ -55,14 +56,14 @@ type prop_kind =
type decl =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_kind * Name.t * fmla
| Dprop of prop_kind * ident * fmla
type decl_or_use =
| Decl of decl
| Use of t
and t = {
t_name : Name.t;
t_name : ident;
t_namespace : namespace;
t_decls : decl_or_use list;
}
......@@ -76,7 +77,7 @@ and namespace = {
}
type th = {
th_name : Name.t;
th_name : ident;
th_stack : (namespace * namespace) list; (* stack of imports/exports *)
th_decls : decl_or_use list;
}
......@@ -113,7 +114,7 @@ let open_namespace th = match th.th_stack with
let close_namespace th n ~import = match th.th_stack with
| (_, e0) :: (i, e) :: st ->
let s = Name.to_string n in
let s = n.id_short in
let add ns = { ns with namespace = M.add s e0 ns.namespace } in
{ th with th_stack = (add i, add e) :: st }
| [_] ->
......@@ -139,7 +140,7 @@ let add_psymbol x ty ns = { ns with psymbols = M.add x ty ns.psymbols }
let add_ns add x v th = match th.th_stack with
| (i, e) :: st ->
let x = Name.unsafe_to_string x in (add x v i, add x v e) :: st
let x = x.id_short in (add x v i, add x v e) :: st
| [] -> assert false
let add_decl th d =
......@@ -189,15 +190,20 @@ let report fmt = function
(** Debugging *)
let print_ident =
let printer = create_printer () in
let print fmt id = Format.fprintf fmt "%s" (id_unique printer id) in
print
let rec print_namespace fmt ns =
fprintf fmt "@[<hov 2>types: ";
M.iter (fun x ty -> fprintf fmt "%s -> %a;@ " x Name.print ty.Ty.ts_name)
M.iter (fun x ty -> fprintf fmt "%s -> %a;@ " x print_ident ty.ts_name)
ns.tysymbols;
fprintf fmt "@]@\n@[<hov 2>function symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.fs_name)
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x print_ident s.fs_name)
ns.fsymbols;
fprintf fmt "@]@\n@[<hov 2>predicate symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.ps_name)
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x print_ident s.ps_name)
ns.psymbols;
fprintf fmt "@]@\n@[<hov 2>namespace: ";
M.iter (fun x th -> fprintf fmt "%s -> [@[%a@]];@ " x print_namespace th)
......
src/core/theory.mli
View file @ 4d6154fd
......@@ -17,6 +17,7 @@
(* *)
(**************************************************************************)
open Ident
open Ty
open Term
......@@ -29,7 +30,7 @@ type ty_decl = tysymbol * ty_def
type logic_decl =
| Lfunction of fsymbol * (vsymbol list * term) option (* FIXME: binders *)
| Lpredicate of psymbol * (vsymbol list * fmla) option (* FIXME: binders *)
| Linductive of psymbol * (Name.t * fmla) list
| Linductive of psymbol * (ident * fmla) list
type prop_kind =
| Axiom | Lemma | Goal
......@@ -37,14 +38,14 @@ type prop_kind =
type decl =
| Dtype of ty_decl list
| Dlogic of logic_decl list
| Dprop of prop_kind * Name.t * fmla
| Dprop of prop_kind * ident * fmla
type decl_or_use =
| Decl of decl
| Use of t
and t = private {
t_name : Name.t;
t_name : ident;
t_namespace : namespace;
t_decls : decl_or_use list;
}
......@@ -56,10 +57,10 @@ and namespace
type th
(** a theory under construction *)
val create_theory : Name.t -> th
val create_theory : ident -> th
val open_namespace : th -> th
val close_namespace : th -> Name.t -> import:bool -> th
val close_namespace : th -> ident -> import:bool -> th
val use_export : th -> t -> th
......
src/core/ty.ml
View file @ 4d6154fd
......@@ -18,15 +18,16 @@
(**************************************************************************)
open Util
open Ident
(** Types *)
type tvsymbol = Name.t
type tvsymbol = ident
(* type symbols and types *)
type tysymbol = {
ts_name : Name.t;
ts_name : ident;
ts_args : tvsymbol list;
ts_def : ty option;
ts_tag : int;
......@@ -43,8 +44,8 @@ and ty_node =
module Tsym = struct
type t = tysymbol
let equal ts1 ts2 = Name.equal ts1.ts_name ts2.ts_name
let hash ts = Name.hash ts.ts_name
let equal ts1 ts2 = ts1.ts_name == ts2.ts_name
let hash ts = ts.ts_name.id_tag
let tag n ts = { ts with ts_tag = n }
let compare ts1 ts2 = Pervasives.compare ts1.ts_tag ts2.ts_tag
end
......@@ -66,14 +67,14 @@ module Ty = struct
type t = ty
let equal ty1 ty2 = match ty1.ty_node, ty2.ty_node with
| Tyvar n1, Tyvar n2 -> Name.equal n1 n2
| Tyvar n1, Tyvar n2 -> n1 == n2
| Tyapp (s1, l1), Tyapp (s2, l2) -> s1 == s2 && List.for_all2 (==) l1 l2
| _ -> false
let hash_ty ty = ty.ty_tag
let hash ty = match ty.ty_node with
| Tyvar v -> Name.hash v
| Tyvar v -> v.id_tag
| Tyapp (s, tl) -> Hashcons.combine_list hash_ty (s.ts_tag) tl
let tag n ty = { ty with ty_tag = n }
......@@ -107,13 +108,13 @@ exception NonLinear
exception UnboundTypeVariable
let rec tv_known vs ty = match ty.ty_node with
| Tyvar n -> Name.S.mem n vs
| Tyvar n -> Sid.mem n vs
| _ -> ty_forall (tv_known vs) ty
let create_tysymbol name args def =
let add s v = if Name.S.mem v s
then raise NonLinear else Name.S.add v s in
let s = List.fold_left add Name.S.empty args in
let add s v = if Sid.mem v s
then raise NonLinear else Sid.add v s in
let s = List.fold_left add Sid.empty args in
let _ = match def with
| Some ty -> tv_known s ty || raise UnboundTypeVariable
| _ -> true
......@@ -123,15 +124,15 @@ let create_tysymbol name args def =
exception BadTypeArity
let rec tv_inst m ty = match ty.ty_node with
| Tyvar n -> Name.M.find n m
| Tyvar n -> Mid.find n m
| _ -> ty_map (tv_inst m) ty
let ty_app s tl =
if List.length tl == List.length s.ts_args
then match s.ts_def with
| Some ty ->
let add m v t = Name.M.add v t m in
tv_inst (List.fold_left2 add Name.M.empty s.ts_args tl) ty
let add m v t = Mid.add v t m in
tv_inst (List.fold_left2 add Mid.empty s.ts_args tl) ty
| _ ->
ty_app s tl
else raise BadTypeArity
......@@ -144,8 +145,8 @@ let rec matching s ty1 ty2 =
if ty1 == ty2 then s
else match ty1.ty_node, ty2.ty_node with
| Tyvar n1, _ ->
(try if Name.M.find n1 s == ty2 then s else raise TypeMismatch
with Not_found -> Name.M.add n1 ty2 s)
(try if Mid.find n1 s == ty2 then s else raise TypeMismatch
with Not_found -> Mid.add n1 ty2 s)
| Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
List.fold_left2 matching s l1 l2
| _ ->
......
src/core/ty.mli
View file @ 4d6154fd
......@@ -17,14 +17,16 @@
(* *)
(**************************************************************************)
open Ident
(** Types *)
type tvsymbol = Name.t
type tvsymbol = ident
(* type symbols and types *)
type tysymbol = private {
ts_name : Name.t;
ts_name : ident;
ts_args : tvsymbol list;
ts_def : ty option;
ts_tag : int;
......@@ -42,7 +44,7 @@ and ty_node = private
exception NonLinear
exception UnboundTypeVariable
val create_tysymbol : Name.t -> tvsymbol list -> ty option -> tysymbol
val create_tysymbol : ident -> tvsymbol list -> ty option -> tysymbol
module Sts : Set.S with type elt = tysymbol
module Mts : Map.S with type key = tysymbol
......@@ -59,6 +61,6 @@ val ty_exists : (ty -> bool) -> ty -> bool
exception TypeMismatch
val matching : ty Name.M.t -> ty -> ty -> ty Name.M.t
val ty_match : ty -> ty -> ty Name.M.t -> ty Name.M.t option
val matching : ty Mid.t -> ty -> ty -> ty Mid.t
val ty_match : ty -> ty -> ty Mid.t -> ty Mid.t option
src/parser/typing.ml
View file @ 4d6154fd
......@@ -20,6 +20,7 @@
open Util
open Format
open Pp
open Ident
open Ty
open Term
open Ptree
......@@ -39,7 +40,7 @@ type error =
| UnboundSymbol of string
| TermExpectedType of (formatter -> unit) * (formatter -> unit)
(* actual / expected *)
| BadNumberOfArguments of Name.t * int * int
| BadNumberOfArguments of Ident.ident * int * int
| ClashTheory of string
| ClashNamespace of string
| UnboundTheory of string
......@@ -81,7 +82,7 @@ let report fmt = function
| UnboundSymbol s ->
fprintf fmt "Unbound symbol '%s'" s
| BadNumberOfArguments (s, n, m) ->
fprintf fmt "@[Symbol `%a' is aplied to %d terms,@ " Name.print s n;
fprintf fmt "@[Symbol `%s' is aplied to %d terms,@ " s.id_short n;
fprintf fmt "but is expecting %d arguments@]" m
| TermExpectedType (ty1, ty2) ->
fprintf fmt "@[This term has type "; ty1 fmt;
......@@ -147,14 +148,14 @@ let rec print_dty fmt = function
| Tyvar { type_val = Some t } ->
print_dty fmt t
| Tyvar { type_val = None; tvsymbol = v } ->
fprintf fmt "'%a" Name.print v
fprintf fmt "'%s" v.id_short
| Tyapp (s, []) ->
fprintf fmt "%a" Name.print s.Ty.ts_name
fprintf fmt "%s" s.ts_name.id_short
| Tyapp (s, [t]) ->
fprintf fmt "%a %a" print_dty t Name.print s.Ty.ts_name
fprintf fmt "%a %s" print_dty t s.ts_name.id_short
| Tyapp (s, l) ->
fprintf fmt "(%a) %a"
(print_list comma print_dty) l Name.print s.Ty.ts_name
fprintf fmt "(%a) %s"
(print_list comma print_dty) l s.ts_name.id_short
let create_type_var =
let t = ref 0 in
......@@ -209,13 +210,14 @@ let find_user_type_var x env =
try
Hashtbl.find env.utyvars x
with Not_found ->
let v = create_type_var ~user:true (Name.from_string x) in
(* TODO: shouldn't we localize this ident? *)
let v = create_type_var ~user:true (id_fresh x x) in
Hashtbl.add env.utyvars x v;
v
(* Specialize *)
module Htv = Hashtbl.Make(Name)
module Htv = Hid
let find_type_var env tv =
try
......@@ -225,7 +227,7 @@ let find_type_var env tv =
Htv.add env tv v;
v
let rec specialize env t = match t.Ty.ty_node with
let rec specialize env t = match t.ty_node with
| Ty.Tyvar tv ->
Tyvar (find_type_var env tv)
| Ty.Tyapp (s, tl) ->
......@@ -257,7 +259,7 @@ let find_tysymbol p th =
let specialize_tysymbol x env =
let s = find_tysymbol x env.th in
let env = Htv.create 17 in
s, List.map (find_type_var env) s.Ty.ts_args
s, List.map (find_type_var env) s.ts_args
let find_fsymbol {id=x; id_loc=loc} ns =
try find_fsymbol ns x
......@@ -429,7 +431,8 @@ and fmla env = function
| Fif (f1, f2, f3) ->
f_if (fmla env f1) (fmla env f2) (fmla env f3)
| Fquant (q, x, t, f1) ->
let v = create_vsymbol (Name.from_string x) (ty t) in
(* TODO: shouldn't we localize this ident? *)
let v = create_vsymbol (id_fresh x x) (ty t) in
let env = M.add x v env in
f_quant q v (fmla env f1)
| Fapp (s, tl) ->
......@@ -440,18 +443,21 @@ and fmla env = function