deplacement de Term.Ty dans ty.ml

Makefile.in

@@ -98,7 +98,7 @@ doc/version.tex src/version.ml: Version version.sh config.status
 
 LIBCMO = src/lib/pp.cmo src/lib/loc.cmo src/lib/util.cmo src/lib/hashcons.cmo 
 
-CMO = $(LIBCMO) src/name.cmo src/term.cmo src/pretty.cmo \
+CMO = $(LIBCMO) src/name.cmo src/ty.cmo src/term.cmo src/pretty.cmo \
       src/parser.cmo src/lexer.cmo src/env.cmo src/typing.cmo src/main.cmo
 CMX = $(CMO:.cmo=.cmx)
 

src/env.ml

 
 open Format
 open Pp
+open Ty
 open Term
 
 (** Error reporting *)

src/env.mli

 
+open Ty
 open Term
 
 type t
 
 (** Building *)
 
-val create : string list -> t
-  (** create an environment for a given loadpath *)
+val empty : t
 
-val open_theory : t -> t
-val close_theory : t -> string -> t
+type th
 
-val open_namespace : t -> t
-val close_namespace : t -> string -> t
+val open_theory : t -> string -> th
+val close_theory : th -> t
+
+val open_namespace : th -> string -> import:bool -> th
+val close_namespace : th -> th
+
+val use_export : th -> string -> th
+
+type th_subst = {
+  subst_ts : tysymbol Mts.t;
+  subst_fs : fsymbol  Mfs.t;
+  subst_ps : psymbol  Mps.t;
+}
+
+val clone_export : th -> string -> th_subst -> th
 
 (** Querying *)
 
@@ -20,7 +32,7 @@ type path =
   | Pident of string
   | Pdot of path * string
 
-val find_tysymbol : path -> t -> tysymbol
+val find_tysymbol : th -> path -> tysymbol
 
 
 (** Error reporting *)

src/lib/util.ml

@@ -23,3 +23,7 @@ let map_fold_left f acc l =
   acc, List.rev rev
 
     
+exception FoldSkip
+
+let forall_fn pr _ t = pr t || raise FoldSkip
+let exists_fn pr _ t = pr t && raise FoldSkip

src/lib/util.mli

@@ -16,3 +16,10 @@
 
 val map_fold_left : 
   ('acc -> 'a -> 'acc * 'b) -> 'acc -> 'a list -> 'acc * 'b list
+
+exception FoldSkip
+
+val forall_fn : ('a -> bool) -> 'b -> 'a -> bool
+val exists_fn : ('a -> bool) -> 'b -> 'a -> bool
+
+

src/pretty.mli

@@ -15,6 +15,7 @@
 (**************************************************************************)
 
 open Format
+open Ty
 open Term
 
 val print_ty : formatter -> ty -> unit

src/term.ml

@@ -14,154 +14,13 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type label = string
-
-exception FoldSkip
+open Util
+open Ty
 
-let forall_fn pr _ t = pr t || raise FoldSkip
-let exists_fn pr _ t = pr t && raise FoldSkip
+type label = string
 
 exception NonLinear
 
-(** Types *)
-
-module Ty = struct
-
-  type tvsymbol = Name.t
-
-  (* type symbols and types *)
-
-  type tysymbol = {
-    ts_name : Name.t;
-    ts_args : tvsymbol list;
-    ts_def  : ty option;
-    ts_tag  : int;
-  }
-
-  and ty = {
-    ty_node : ty_node;
-    ty_tag : int;
-  }
-
-  and ty_node =
-    | Tyvar of tvsymbol
-    | Tyapp of tysymbol * ty list
-
-  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 tag n ts = { ts with ts_tag = n }
-  end
-  module Hts = Hashcons.Make(Tsym)
-
-  let mk_ts name args def = {
-    ts_name = name;
-    ts_args = args;
-    ts_def  = def;
-    ts_tag  = -1
-  }
-
-  let create_tysymbol name args def = Hts.hashcons (mk_ts name args def)
-
-  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
-      | 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
-      | Tyapp (s, tl) -> Hashcons.combine_list hash_ty (s.ts_tag) tl
-
-    let tag n ty = { ty with ty_tag = n }
-
-  end
-  module Hty = Hashcons.Make(Ty)
-
-  let mk_ty n = { ty_node = n; ty_tag = -1 }
-  let ty_var n = Hty.hashcons (mk_ty (Tyvar n))
-  let ty_app s tl = Hty.hashcons (mk_ty (Tyapp (s, tl)))
-
-  (* generic traversal functions *)
-
-  let ty_map fn ty = match ty.ty_node with
-    | Tyvar _ -> ty
-    | Tyapp (f, tl) -> ty_app f (List.map fn tl)
-
-  let ty_fold fn acc ty = match ty.ty_node with
-    | Tyvar _ -> acc
-    | Tyapp (f, tl) -> List.fold_left fn acc tl
-
-  let ty_forall pr ty =
-    try ty_fold (forall_fn pr) true ty with FoldSkip -> false
-
-  let ty_exists pr ty =
-    try ty_fold (exists_fn pr) false ty with FoldSkip -> true
-
-  (* smart constructors *)
-
-  exception UnboundTypeVariable
-
-  let rec tv_known vs ty = match ty.ty_node with
-    | Tyvar n -> Name.S.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 _ = match def with
-      | Some ty -> tv_known s ty || raise UnboundTypeVariable
-      | _ -> true
-    in
-    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
-    | _ -> 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
-      | _ ->
-          ty_app s tl
-    else raise BadTypeArity
-
-  (* type matching *)
-
-  exception TypeMismatch
-
-  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)
-      | Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
-          List.fold_left2 matching s l1 l2
-      | _ ->
-          raise TypeMismatch
-
-  let ty_match ty1 ty2 s =
-    try Some (matching s ty1 ty2) with TypeMismatch -> None
-
-end
-
-type tvsymbol = Ty.tvsymbol
-type tysymbol = Ty.tysymbol
-type ty = Ty.ty
-
 (** Variable symbols *)
 
 type vsymbol = {
@@ -202,8 +61,11 @@ module Fsym = struct
   let equal fs1 fs2 = Name.equal fs1.fs_name fs2.fs_name
   let hash fs = Name.hash fs.fs_name
   let tag n fs = { fs with fs_tag = n }
+  let compare fs1 fs2 = Pervasives.compare fs1.fs_tag fs2.fs_tag
 end
 module Hfs = Hashcons.Make(Fsym)
+module Sfs = Set.Make(Fsym)
+module Mfs = Map.Make(Fsym)
 
 let mk_fs name scheme constr = {
   fs_name = name;
@@ -227,8 +89,11 @@ module Psym = struct
   let equal ps1 ps2 = Name.equal ps1.ps_name ps2.ps_name
   let hash ps = Name.hash ps.ps_name
   let tag n ps = { ps with ps_tag = n }
+  let compare ps1 ps2 = Pervasives.compare ps1.ps_tag ps2.ps_tag
 end
 module Hps = Hashcons.Make(Psym)
+module Sps = Set.Make(Psym)
+module Mps = Map.Make(Psym)
 
 let mk_ps name scheme = { ps_name = name; ps_scheme = scheme; ps_tag = -1 }
 let create_psymbol name scheme = Hps.hashcons (mk_ps name scheme)

src/term.mli

@@ -14,49 +14,9 @@
 (*                                                                        *)
 (**************************************************************************)
 
-type label
-
-(** Types *)
-
-module Ty : sig
-
-  type tvsymbol = Name.t
-
-  (* type symbols and types *)
-
-  type tysymbol = private {
-    ts_name : Name.t;
-    ts_args : tvsymbol list;
-    ts_def  : ty option;
-    ts_tag  : int;
-  }
-
-  and ty = private {
-    ty_node : ty_node;
-    ty_tag  : int;
-  }
-
-  and ty_node = private
-    | Tyvar of tvsymbol
-    | Tyapp of tysymbol * ty list
-
-  val create_tysymbol : Name.t -> tvsymbol list -> ty option -> tysymbol
+open Ty
 
-  val ty_var : tvsymbol -> ty
-  val ty_app : tysymbol -> ty list -> ty
-
-  val ty_map : (ty -> ty) -> ty -> ty
-  val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
-  val ty_forall : (ty -> bool) -> ty -> bool
-  val ty_exists : (ty -> bool) -> ty -> bool
-
-  val ty_match : ty -> ty -> ty Name.M.t -> ty Name.M.t option
-
-end
-
-type tvsymbol = Ty.tvsymbol
-type tysymbol = Ty.tysymbol
-type ty = Ty.ty
+type label
 
 (** Variable symbols *)
 
@@ -66,8 +26,8 @@ type vsymbol = private {
   vs_tag : int;
 }
 
-module Mvs : Map.S with type key = vsymbol
 module Svs : Set.S with type elt = vsymbol
+module Mvs : Map.S with type key = vsymbol
 
 val create_vsymbol : Name.t -> ty -> vsymbol
 
@@ -82,6 +42,9 @@ type fsymbol = private {
 
 val create_fsymbol : Name.t -> ty list * ty -> bool -> fsymbol
 
+module Sfs : Set.S with type elt = fsymbol
+module Mfs : Map.S with type key = fsymbol
+
 (** Predicate symbols *)
 
 type psymbol = private {
@@ -92,6 +55,9 @@ type psymbol = private {
 
 val create_psymbol : Name.t -> ty list -> psymbol
 
+module Sps : Set.S with type elt = psymbol
+module Mps : Map.S with type key = psymbol
+
 (** Patterns *)
 
 type pattern = private {

src/ty.ml

+
+open Util
+
+(** Types *)
+
+type tvsymbol = Name.t
+
+(* type symbols and types *)
+    
+type tysymbol = {
+  ts_name : Name.t;
+  ts_args : tvsymbol list;
+  ts_def  : ty option;
+  ts_tag  : int;
+}
+
+and ty = {
+  ty_node : ty_node;
+  ty_tag : int;
+}
+
+and ty_node =
+  | Tyvar of tvsymbol
+  | Tyapp of tysymbol * ty list
+
+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 tag n ts = { ts with ts_tag = n }
+  let compare ts1 ts2 = Pervasives.compare ts1.ts_tag ts2.ts_tag
+end
+module Hts = Hashcons.Make(Tsym)
+module Sts = Set.Make(Tsym)
+module Mts = Map.Make(Tsym)
+
+let mk_ts name args def = {
+  ts_name = name;
+  ts_args = args;
+  ts_def  = def;
+  ts_tag  = -1
+}
+
+let create_tysymbol name args def = Hts.hashcons (mk_ts name args def)
+
+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
+    | 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
+    | Tyapp (s, tl) -> Hashcons.combine_list hash_ty (s.ts_tag) tl
+
+  let tag n ty = { ty with ty_tag = n }
+
+end
+module Hty = Hashcons.Make(Ty)
+
+let mk_ty n = { ty_node = n; ty_tag = -1 }
+let ty_var n = Hty.hashcons (mk_ty (Tyvar n))
+let ty_app s tl = Hty.hashcons (mk_ty (Tyapp (s, tl)))
+
+(* generic traversal functions *)
+
+let ty_map fn ty = match ty.ty_node with
+  | Tyvar _ -> ty
+  | Tyapp (f, tl) -> ty_app f (List.map fn tl)
+
+let ty_fold fn acc ty = match ty.ty_node with
+  | Tyvar _ -> acc
+  | Tyapp (f, tl) -> List.fold_left fn acc tl
+
+let ty_forall pr ty =
+  try ty_fold (forall_fn pr) true ty with FoldSkip -> false
+
+let ty_exists pr ty =
+  try ty_fold (exists_fn pr) false ty with FoldSkip -> true
+
+(* smart constructors *)
+
+exception NonLinear
+exception UnboundTypeVariable
+
+let rec tv_known vs ty = match ty.ty_node with
+  | Tyvar n -> Name.S.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 _ = match def with
+    | Some ty -> tv_known s ty || raise UnboundTypeVariable
+    | _ -> true
+  in
+  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
+  | _ -> 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
+    | _ ->
+        ty_app s tl
+  else raise BadTypeArity
+
+(* type matching *)
+
+exception TypeMismatch
+
+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)
+    | Tyapp (f1, l1), Tyapp (f2, l2) when f1 == f2 ->
+        List.fold_left2 matching s l1 l2
+    | _ ->
+        raise TypeMismatch
+
+let ty_match ty1 ty2 s =
+  try Some (matching s ty1 ty2) with TypeMismatch -> None
+

src/ty.mli

+
+(** Types *)
+
+type tvsymbol = Name.t
+
+(* type symbols and types *)
+
+type tysymbol = private {
+  ts_name : Name.t;
+  ts_args : tvsymbol list;
+  ts_def  : ty option;
+  ts_tag  : int;
+}
+
+and ty = private {
+  ty_node : ty_node;
+  ty_tag  : int;
+}
+
+and ty_node = private
+  | Tyvar of tvsymbol
+  | Tyapp of tysymbol * ty list
+
+exception NonLinear
+exception UnboundTypeVariable
+
+val create_tysymbol : Name.t -> tvsymbol list -> ty option -> tysymbol
+
+module Sts : Set.S with type elt = tysymbol
+module Mts : Map.S with type key = tysymbol
+
+exception BadTypeArity
+
+val ty_var : tvsymbol -> ty
+val ty_app : tysymbol -> ty list -> ty
+
+val ty_map : (ty -> ty) -> ty -> ty
+val ty_fold : ('a -> ty -> 'a) -> 'a -> ty -> 'a
+val ty_forall : (ty -> bool) -> ty -> bool
+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
+