introduction d'un module Env ; grand chantier en cours (plus rien ne fonctionne)

parent 63c06aff
......@@ -99,7 +99,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
CMO = $(LIBCMO) src/name.cmo src/hashcons.cmo src/term.cmo src/pretty.cmo \
src/parser.cmo src/lexer.cmo src/typing.cmo src/main.cmo
src/parser.cmo src/lexer.cmo src/env.cmo src/typing.cmo src/main.cmo
CMX = $(CMO:.cmo=.cmx)
bin/why.opt: $(CMX)
......
open Format
open Pp
open Term
(** Error reporting *)
type error =
| UnboundNamespace of string
| OpenTheory
| CloseTheory
| NoOpenedTheory
| NoOpenedNamespace
exception Error of error
let error e = raise (Error e)
(** The environment type *)
module M = Map.Make(String)
type namespace = {
tysymbols : tysymbol M.t; (* type symbols *)
fsymbols : fsymbol M.t; (* function symbols *)
psymbols : psymbol M.t; (* predicate symbols *)
namespace : namespace M.t;
}
type decl =
unit (* TODO *)
type theory = {
th_ns : namespace;
th_decl : decl list;
}
type t = {
loadpath : string list;
theories : theory M.t;
ns_stack : (namespace * namespace) list; (* stack of imports/exports *)
}
(** Creating environments *)
let empty_ns = {
tysymbols = M.empty;
fsymbols = M.empty;
psymbols = M.empty;
namespace = M.empty;
}
let is_empty_ns ns =
M.is_empty ns.tysymbols &&
M.is_empty ns.fsymbols &&
M.is_empty ns.psymbols &&
M.is_empty ns.namespace
let create lp = {
loadpath = lp;
theories = M.empty;
ns_stack = [];
}
let open_theory t = match t.ns_stack with
| [] -> { t with ns_stack = [empty_ns, empty_ns] }
| _ -> error OpenTheory
let close_theory t s = match t.ns_stack with
| [_, e] ->
let th = { th_ns = e; th_decl = [] (* TODO *) } in
{ t with theories = M.add s th t.theories }
| _ ->
error CloseTheory
let open_namespace t = match t.ns_stack with
| (i, _) :: _ as st ->
{ t with ns_stack = (i, empty_ns) :: st }
| [] ->
error NoOpenedTheory
let close_namespace t s = match t.ns_stack with
| (_, e0) :: (i, e) :: st ->
let add ns = { ns with namespace = M.add s e0 ns.namespace } in
{ t with ns_stack = (add i, add e) :: st }
| [_] ->
error NoOpenedNamespace
| [] ->
error NoOpenedTheory
let add_tysymbol x ty env = { env with tysymbols = M.add x ty env.tysymbols }
let add_fsymbol x ty env = { env with fsymbols = M.add x ty env.fsymbols }
let add_psymbol x ty env = { env with psymbols = M.add x ty env.psymbols }
(* let self_id = "(\*self*\)" *)
(* let self env = M.find self_id env.theories *)
(* let empty = { empty_env with theories = M.add self_id empty_env M.empty } *)
(* let add_self f x v env = *)
(* f x v { env with theories = *)
(* M.add self_id (f x v (self env)) env.theories } *)
(* let add_tysymbol = add_self add_tysymbol *)
(* let add_fsymbol = add_self add_fsymbol *)
(* let add_psymbol = add_self add_psymbol *)
(* let add_theory = add_self add_theory *)
(** Querying environments *)
let ns env = match env.ns_stack with
| (ns, _) :: _ -> ns
| [] -> error NoOpenedTheory
let find_tysymbol s env = M.find s env.tysymbols
let find_fsymbol s env = M.find s env.fsymbols
let find_psymbol s env = M.find s env.psymbols
type path =
| Pident of string
| Pdot of path * string
let find_local_namespace s env =
try M.find s env.namespace
with Not_found -> error (UnboundNamespace s)
let rec find_namespace q env = match q with
| Pident t -> find_local_namespace t env
| Pdot (q, t) -> let env = find_namespace q env in find_local_namespace t env
let rec find f q env = match q with
| Pident x -> f x env
| Pdot (m, x) -> let env = find_namespace m env in f x env
let find_tysymbol p env = find find_tysymbol p (ns env)
(** Error reporting *)
let report fmt = function
| UnboundNamespace s ->
fprintf fmt "unbound namespace %s" s
| OpenTheory ->
fprintf fmt "cannot open a new theory in a non-empty context"
| CloseTheory ->
fprintf fmt "cannot close theory: there are still unclosed namespaces"
| NoOpenedTheory ->
fprintf fmt "no opened theory"
| NoOpenedNamespace ->
fprintf fmt "no opened namespace"
(** Debugging *)
let rec print_env fmt env =
fprintf fmt "@[<hov 2>types: ";
M.iter (fun x ty -> fprintf fmt "%s -> %a;@ " x Name.print ty.Ty.ts_name)
env.tysymbols;
fprintf fmt "@]@\n@[<hov 2>function symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.fs_name)
env.fsymbols;
fprintf fmt "@]@\n@[<hov 2>predicate symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.ps_name)
env.psymbols;
fprintf fmt "@]@\n@[<hov 2>namespace: ";
M.iter (fun x th -> fprintf fmt "%s -> [@[%a@]];@ " x print_env th)
env.namespace;
fprintf fmt "@]"
let print fmt t =
print_env fmt (ns t)
(*
Local Variables:
compile-command: "make -C .. test"
End:
*)
open Term
type t
(** Building *)
val create : string list -> t
(** create an environment for a given loadpath *)
val open_theory : t -> t
val close_theory : t -> string -> t
val open_namespace : t -> t
val close_namespace : t -> string -> t
(** Querying *)
type path =
| Pident of string
| Pdot of path * string
val find_tysymbol : path -> t -> tysymbol
(* val find_fsymbol : t -> path -> fsymbol *)
(** Error reporting *)
type error
exception Error of error
val report : Format.formatter -> error -> unit
(** Debugging *)
val print : Format.formatter -> t -> unit
......@@ -47,12 +47,14 @@
"begin", BEGIN;
"bool", BOOL;
"check", CHECK;
"clone", CLONE;
"do", DO;
"done", DONE;
"else", ELSE;
"end", END;
"exception", EXCEPTION;
"exists", EXISTS;
"export", EXPORT;
"external", EXTERNAL;
"false", FALSE;
"for", FOR;
......@@ -61,17 +63,17 @@
"function", FUNCTION;
"goal", GOAL;
"if", IF;
"import", IMPORT;
"in", IN;
"include", INCLUDE;
"inductive", INDUCTIVE;
(*"int", INT;*)
"invariant", INVARIANT;
"let", LET;
"logic", LOGIC;
"match", MATCH;
"namespace", NAMESPACE;
"not", NOT;
"of", OF;
"open", OPEN;
"or", OR;
"parameter", PARAMETER;
"predicate", PREDICATE;
......@@ -89,7 +91,7 @@
"try", TRY;
"type", TYPE;
"unit", UNIT;
"uses", USES;
"use", USE;
"variant", VARIANT;
"void", VOID;
"while", WHILE;
......
......@@ -46,11 +46,12 @@ let type_file env file =
Loc.set_file file lb;
let f = Lexer.parse_logic_file lb in
close_in c;
if !parse_only then env else Typing.add_decls env f
if !parse_only then env else List.fold_left Typing.add_theory env f
let () =
try
ignore (List.fold_left type_file Typing.empty !files)
let env = Env.create [] in
ignore (List.fold_left type_file env !files)
with e ->
eprintf "%a@." report e;
exit 1
......
......@@ -93,16 +93,18 @@
%token <string> STRING
%token ABSURD AMPAMP AND ARRAY ARROW AS ASSERT AT AXIOM
%token BANG BAR BARBAR BEGIN
%token BIGARROW BOOL CHECK COLON COLONEQUAL COMMA DO DONE DOT ELSE END EOF EQUAL
%token EXCEPTION EXISTS EXTERNAL FALSE FOR FORALL FPI FUN FUNCTION GE GOAL GT
%token IF IN INCLUDE INDUCTIVE INT INVARIANT
%token BIGARROW BOOL CHECK CLONE COLON COLONEQUAL COMMA DO
%token DONE DOT ELSE END EOF EQUAL
%token EXCEPTION EXISTS EXPORT EXTERNAL FALSE FOR FORALL FPI
%token FUN FUNCTION GE GOAL GT
%token IF IMPORT IN INCLUDE INDUCTIVE INT INVARIANT
%token LE LEFTB LEFTBLEFTB LEFTPAR LEFTSQ LET LOGIC LRARROW LT MATCH MINUS
%token NOT NOTEQ OF OPEN OR PARAMETER PERCENT PLUS PREDICATE PROP
%token NAMESPACE NOT NOTEQ OF OR PARAMETER PERCENT PLUS PREDICATE PROP
%token QUOTE RAISE RAISES READS REAL REC REF RETURNS RIGHTB RIGHTBRIGHTB
%token RIGHTPAR RIGHTSQ
%token SEMICOLON SLASH
%token THEN THEORY TIMES TRUE TRY TYPE UNDERSCORE
%token UNIT USES VARIANT VOID WHILE WITH WRITES
%token UNIT USE VARIANT VOID WHILE WITH WRITES
/* Precedences */
......@@ -146,8 +148,6 @@
%%
logic_file:
| list1_decl EOF
{ $1 }
| list1_theory EOF
{ $1 }
| EOF
......@@ -211,10 +211,10 @@ decl:
{ Goal (loc (), $2, $4) }
| TYPE typedecl typedefn
{ let loc, vl, id = $2 in $3 loc vl id }
| USES list1_uses_sep_comma
{ Uses (loc (), $2) }
| OPEN uident
{ Open $2 }
| USE use
{ Use (loc (), $2) }
| NAMESPACE uident list0_decl END
{ Namespace (loc (), $2, $3) }
;
list1_theory:
......@@ -226,7 +226,7 @@ list1_theory:
theory:
| THEORY uident list0_decl END
{ Theory ({ th_loc = loc (); th_name = $2; th_decl = $3 }) }
{ { th_loc = loc (); th_name = $2; th_decl = $3 } }
;
typedecl:
......@@ -495,14 +495,17 @@ list1_lident_sep_comma:
| lident COMMA list1_lident_sep_comma { $1 :: $3 }
;
list1_uses_sep_comma:
| uses { [$1] }
| uses COMMA list1_uses_sep_comma { $1 :: $3 }
use:
| imp_exp uqualid
{ { use_theory = $2; use_as = None; use_imp_exp = $1 } }
| imp_exp uident COLON uqualid
{ { use_theory = $4; use_as = Some $2; use_imp_exp = $1 } }
;
uses:
| uqualid { None, $1 }
| uident COLON uqualid { Some $1, $3 }
imp_exp:
| IMPORT { Import }
| EXPORT { Export }
| /* epsilon */ { Nothing }
;
/******* programs **************************************************
......
......@@ -70,15 +70,16 @@ type plogic_type =
| PPredicate of pty list
| PFunction of pty list * pty
type uses = ident option * qualid
type imp_exp =
| Import | Export | Nothing
type theory = {
th_loc : loc;
th_name : ident;
th_decl : logic_decl list;
type use = {
use_theory : qualid;
use_as : ident option;
use_imp_exp : imp_exp;
}
and logic_decl =
type logic_decl =
| Logic of loc * ident list * plogic_type
| Predicate_def of loc * ident * (loc * ident * pty) list * lexpr
| Inductive_def of loc * ident * plogic_type * (loc * ident * lexpr) list
......@@ -87,8 +88,14 @@ and logic_decl =
| Goal of loc * ident * lexpr
| TypeDecl of loc * ident list * ident
| AlgType of (loc * ident list * ident * (loc * ident * pty list) list) list
| Theory of theory
| Uses of loc * uses list
| Open of ident
| Use of loc * use
| Namespace of loc * ident * logic_decl list
type theory = {
th_loc : loc;
th_name : ident;
th_decl : logic_decl list;
}
type logic_file = theory list
type logic_file = logic_decl list
......@@ -7,15 +7,14 @@ theory A
end
theory B
uses A
open A
use import A
logic d : t
logic p : t -> prop
end
theory C
uses B
uses T : B.A
use B
use T : B.A
logic e : T.t
axiom test : B.p(T.c)
end
......@@ -34,8 +33,7 @@ theory List
logic is_nil : 'a list -> prop
uses Int
open Int
use import Int
logic length : 'a list -> int
......@@ -63,8 +61,8 @@ end
theory Test
uses Eq, L : List
open L
use Eq
use import L : List
axiom a : forall x : 'a. not Eq.eq(nil, cons(nil, nil))
end
\ No newline at end of file
......@@ -82,63 +82,6 @@ let report fmt = function
| AlreadyTheory s ->
fprintf fmt "already using a theory with name %s" s
(** typing environments *)
module M = Map.Make(String)
type env = {
tysymbols : tysymbol M.t; (* type symbols *)
fsymbols : fsymbol M.t; (* function symbols *)
psymbols : psymbol M.t; (* predicate symbols *)
theories : env M.t; (* theories (including "self") *)
}
let empty0 = {
tysymbols = M.empty;
fsymbols = M.empty;
psymbols = M.empty;
theories = M.empty;
}
let find_tysymbol s env = M.find s.id env.tysymbols
let find_fsymbol s env = M.find s.id env.fsymbols
let find_psymbol s env = M.find s.id env.psymbols
let add_tysymbol x ty env = { env with tysymbols = M.add x ty env.tysymbols }
let add_fsymbol x ty env = { env with fsymbols = M.add x ty env.fsymbols }
let add_psymbol x ty env = { env with psymbols = M.add x ty env.psymbols }
let add_theory x t env = { env with theories = M.add x t env.theories }
let self_id = "(*self*)"
let self env = M.find self_id env.theories
let empty = { empty0 with theories = M.add self_id empty0 M.empty }
let add_self f x v env =
f x v { env with theories =
M.add self_id (f x v (self env)) env.theories }
let add_tysymbol = add_self add_tysymbol
let add_fsymbol = add_self add_fsymbol
let add_psymbol = add_self add_psymbol
let add_theory = add_self add_theory
(** debugging *)
let rec print_env fmt env =
fprintf fmt "@[<hov 2>types: ";
M.iter (fun x ty -> fprintf fmt "%s -> %a;@ " x Name.print ty.Ty.ts_name)
env.tysymbols;
fprintf fmt "@]@\n@[<hov 2>function symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.fs_name)
env.fsymbols;
fprintf fmt "@]@\n@[<hov 2>predicate symbols: ";
M.iter (fun x s -> fprintf fmt "%s -> %a;@ " x Name.print s.ps_name)
env.psymbols;
fprintf fmt "@]@\n@[<hov 2>theories: ";
M.iter (fun x th -> fprintf fmt "%s -> [@[%a@]];@ " x print_env th)
env.theories;
fprintf fmt "@]"
(** typing using destructive type variables
parsed trees intermediate trees typed trees
......@@ -213,8 +156,10 @@ let rec unify t1 t2 = match t1, t2 with
environment + local variables.
It is only local to this module and created with [create_denv] below. *)
module M = Map.Make(String)
type denv = {
env : env;
env : Env.t;
utyvars : (string, type_var) Hashtbl.t; (* user type variables *)
dvars : dty M.t; (* local variables, to be bound later *)
}
......@@ -251,31 +196,19 @@ let rec specialize env t = match t.Ty.ty_node with
| Ty.Tyapp (s, tl) ->
Tyapp (s, List.map (specialize env) tl)
let find_local_theory t env =
try M.find t.id env.theories
with Not_found -> error ~loc:t.id_loc (UnboundTheory t.id)
let rec find_theory q env = match q with
| Qident t -> find_local_theory t env
| Qdot (q, t) -> let env = find_theory q env in find_local_theory t env
let rec find f q env = match q with
| Qident x -> f x env
| Qdot (m, x) -> let env = find_theory m env in f x env
let specialize_tysymbol x env =
let s = find find_tysymbol x env.env in
let s = Env.find_tysymbol x env.env in
let env = Htv.create 17 in
s, List.map (find_type_var env) s.Ty.ts_args
let specialize_fsymbol x env =
let s = find find_fsymbol x env.env in
let s = (* Env.find_fsymbol x env *) assert false (*TODO*) in
let tl, t = s.fs_scheme in
let env = Htv.create 17 in
s, List.map (specialize env) tl, specialize env t
let specialize_psymbol x env =
let s = find find_psymbol x env.env in
let s = (* find_psymbol x env.env *) assert false (*TODO*) in
let env = Htv.create 17 in
s, List.map (specialize env) s.ps_scheme
......@@ -285,6 +218,10 @@ let rec qloc = function
| Qident x -> x.id_loc
| Qdot (m, x) -> Loc.join (qloc m) x.id_loc
let rec path = function
| Qident x -> Env.Pident x.id
| Qdot (p, x) -> Env.Pdot (path p, x.id)
(* parsed types -> intermediate types *)
let rec dty env = function
| PPTtyvar {id=x} ->
......@@ -292,7 +229,7 @@ let rec dty env = function
| PPTtyapp (p, x) ->
let loc = qloc x in
let s, tv =
try specialize_tysymbol x env
try specialize_tysymbol (path x) env
with Not_found -> error ~loc:loc (UnboundType x)
in
let np = List.length p in
......@@ -451,6 +388,7 @@ and fmla env = function
open Ptree
(***
let add_type loc sl s env =
if M.mem s.id env.tysymbols then error ~loc (ClashType s.id);
let tyvars = ref M.empty in
......@@ -479,6 +417,7 @@ let add_predicate loc pl env {id=id} =
let pl = List.map ty pl in
let s = create_psymbol (Name.from_string id) pl in
add_psymbol id s env
***)
let fmla env f =
let denv = create_denv env in
......@@ -494,6 +433,7 @@ let axiom loc s f env =
ignore (fmla env f);
env
(***
let uses_theory env (as_t, q) =
let loc = qloc q in
let rec find_theory q = match q with
......@@ -516,22 +456,25 @@ let open_theory t env =
fsymbols = open_map th.fsymbols env.fsymbols;
psymbols = open_map th.psymbols env.psymbols;
theories = open_map th.theories env.theories }
***)
let rec add_decl env = function
| TypeDecl (loc, sl, s) ->
add_type loc sl s env
(* add_type loc sl s env *)
assert false (*TODO*)
| Logic (loc, ids, PPredicate pl) ->
List.fold_left (add_predicate loc pl) env ids
(* List.fold_left (add_predicate loc pl) env ids *)
assert false (*TODO*)
| Logic (loc, ids, PFunction (pl, t)) ->
List.fold_left (add_function loc pl t) env ids
(* List.fold_left (add_function loc pl t) env ids *)
assert false (*TODO*)
| Axiom (loc, s, f) ->
axiom loc s f env
| Theory th ->
add_theory th env
| Uses (loc, uses) ->
List.fold_left uses_theory env uses
| Open id ->
open_theory id env
| Use (loc, use) ->
(* use_theory env use *)
assert false (*TODO*)
| Namespace _ ->
assert false (*TODO*)
| AlgType _
| Goal _
| Function_def _
......@@ -542,13 +485,14 @@ let rec add_decl env = function
and add_decls env = List.fold_left add_decl env
and add_theory th env =
let id = th.th_name.id in
if M.mem id env.theories then error ~loc:th.th_loc (ClashTheory id);
let th_env = { env with theories = M.add self_id empty0 env.theories } in
let th_env = add_decls th_env th.th_decl in
(* printf "add_theory %s@\n%a@." id print_env (M.find self_id th_env.theories); *)
{ env with theories = M.add id (M.find self_id th_env.theories) env.theories }
let add_theory env th =
assert false (*TODO*)
(* let id = th.th_name.id in *)
(* if M.mem id env.theories then error ~loc:th.th_loc (ClashTheory id); *)
(* let th_env = { env with theories = M.add self_id empty0 env.theories } in *)
(* let th_env = add_decls th_env th.th_decl in *)
(* (\* printf "add_theory %s@\n%a@." id print_env (M.find self_id th_env.theories); *\) *)
(* { env with theories = M.add id (M.find self_id th_env.theories) env.theories } *)
(*
Local Variables:
......