Commit d4a06c97 authored by Andrei Paskevich's avatar Andrei Paskevich

localize program declarations

parent 811ab575
......@@ -60,9 +60,9 @@ module Incremental = struct
let new_decl d =
ref_set uc_ref (Typing.add_decl (ref_get uc_ref) d)
let new_use_clone d =
let new_use_clone loc d =
let env = ref_get env_ref in let lenv = ref_get lenv_ref in
ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) d)
ref_set uc_ref (Typing.add_use_clone env lenv (ref_get uc_ref) loc d)
end
......@@ -313,9 +313,9 @@ new_decl:
| decl
{ Incremental.new_decl $1 }
| use_clone
{ Incremental.new_use_clone $1 }
{ Incremental.new_use_clone (floc ()) $1 }
| namespace_head namespace_import namespace_name list0_decl END
{ Incremental.close_namespace (floc_i 3) $2 $3 }
{ Incremental.close_namespace (floc_ij 1 3) $2 $3 }
;
namespace_head:
......@@ -364,9 +364,9 @@ inductive:
use_clone:
| USE use
{ (floc (), $2, None) }
{ ($2, None) }
| CLONE use clone_subst
{ (floc (), $2, Some $3) }
{ ($2, Some $3) }
;
use:
......@@ -1034,11 +1034,11 @@ list1_full_decl:
full_decl:
| decl
{ Dlogic $1 }
{ floc (), Dlogic $1 }
| use_clone
{ Duseclone $1 }
{ floc (), Duseclone $1 }
| NAMESPACE namespace_import namespace_name list0_full_decl END
{ Dnamespace (floc_i 3, $3, $2, $4) }
{ floc_ij 1 3, Dnamespace ($3, $2, $4) }
;
list0_program_decl:
......@@ -1056,6 +1056,13 @@ list1_program_decl:
;
program_decl:
| program_decl_one
{ floc (), $1 }
| NAMESPACE namespace_import namespace_name list0_program_decl END
{ floc_ij 1 3, Dnamespace ($3, $2, $4) }
;
program_decl_one:
| decl
{ Dlogic $1 }
| use_clone
......@@ -1076,8 +1083,6 @@ program_decl:
{ Dexn (add_lab $2 $3, Some $4) }
| USE use_module
{ $2 }
| NAMESPACE namespace_import namespace_name list0_program_decl END
{ Dnamespace (floc_i 3, $3, $2, $4) }
;
lident_rich_pgm:
......@@ -1107,7 +1112,7 @@ list1_recfun_sep_and:
recfun:
| ghost lident_rich_pgm labels list1_type_v_binder
opt_cast opt_variant EQUAL triple
{ add_lab $2 $3, $1, $4, $6, cast_body $5 $8 }
{ floc (), add_lab $2 $3, $1, $4, $6, cast_body $5 $8 }
;
expr:
......
......@@ -162,7 +162,7 @@ type metarg =
| PMAstr of string
| PMAint of int
type use_clone = loc * use * clone_subst list option
type use_clone = use * clone_subst list option
type decl =
| TypeDecl of type_decl list
......@@ -204,11 +204,12 @@ type type_v =
| Tpure of pty
| Tarrow of binder list * type_c
and type_c =
{ pc_result_type : type_v;
pc_effect : effect;
pc_pre : pre;
pc_post : post; }
and type_c = {
pc_result_type : type_v;
pc_effect : effect;
pc_pre : pre;
pc_post : post;
}
type expr = {
expr_desc : expr_desc;
......@@ -222,8 +223,7 @@ and expr_desc =
| Eapply of expr * expr
| Efun of binder list * triple
| Elet of ident * ghost * expr * expr
| Eletrec of
(ident * ghost * binder list * variant option * triple) list * expr
| Eletrec of letrec list * expr
| Etuple of expr list
| Erecord of (qualid * expr) list
| Eupdate of expr * (qualid * expr) list
......@@ -248,27 +248,29 @@ and expr_desc =
| Eabstract of expr * post
| Enamed of label * expr
and letrec = loc * ident * ghost * binder list * variant option * triple
and triple = pre * expr * post
type program_decl =
| Dlet of ident * ghost * expr
| Dletrec of (ident * ghost * binder list * variant option * triple) list
| Dletrec of letrec list
| Dlogic of decl
| Duseclone of use_clone
| Dparam of ident * ghost * type_v
| Dexn of ident * pty option
(* modules *)
| Duse of qualid * bool option * (*as:*) string option
| Dnamespace of loc * string option * (* import: *) bool * program_decl list
| Dnamespace of string option * (*import:*) bool * (loc * program_decl) list
type theory = {
pth_name : ident;
pth_decl : program_decl list;
pth_name : ident;
pth_decl : (loc * program_decl) list;
}
type module_ = {
mod_name : ident;
mod_decl : program_decl list;
mod_name : ident;
mod_decl : (loc * program_decl) list;
}
type theory_module =
......
......@@ -1165,7 +1165,7 @@ let type_inst th t s =
in
List.fold_left add_inst empty_inst s
let add_use_clone env lenv th (loc, use, subst) =
let add_use_clone env lenv th loc (use, subst) =
if Debug.test_flag debug_parse_only then th else
let use_or_clone th =
let q, id = split_qualid use.use_theory in
......
......@@ -33,7 +33,8 @@ val debug_type_only : Debug.flag
val add_decl : theory_uc -> Ptree.decl -> theory_uc
val add_use_clone :
unit Env.library -> theory Mstr.t -> theory_uc -> Ptree.use_clone -> theory_uc
unit Env.library -> theory Mstr.t -> theory_uc ->
Loc.position -> Ptree.use_clone -> theory_uc
val close_namespace :
Loc.position -> bool -> string option -> theory_uc -> theory_uc
......
......@@ -42,12 +42,12 @@ let add_theory env path lenv m =
let loc = id.id_loc in
let env = Lexer.library_of_env (Env.env_of_library env) in
let th = Theory.create_theory ~path (Denv.create_user_id id) in
let rec add_decl th = function
let rec add_decl th (loc,dcl) = match dcl with
| Dlogic d ->
Typing.add_decl th d
| Duseclone d ->
Typing.add_use_clone env lenv th d
| Dnamespace (loc, name, import, dl) ->
Typing.add_use_clone env lenv th loc d
| Dnamespace (name, import, dl) ->
let th = Theory.open_namespace th in
let th = List.fold_left add_decl th dl in
Typing.close_namespace loc import name th
......
......@@ -281,12 +281,12 @@ let add_effect_pdecl d uc =
let add_pure_pdecl d uc =
{ uc with uc_pure = Typing.add_decl uc.uc_pure d; }
let add_use_clone env ltm d uc =
let add_use_clone env ltm loc d uc =
let env = Lexer.library_of_env (Env.env_of_library env) in
{ uc with
uc_impure = Typing.add_use_clone env ltm uc.uc_impure d;
uc_effect = Typing.add_use_clone env ltm uc.uc_effect d;
uc_pure = Typing.add_use_clone env ltm uc.uc_pure d; }
uc_impure = Typing.add_use_clone env ltm uc.uc_impure loc d;
uc_effect = Typing.add_use_clone env ltm uc.uc_effect loc d;
uc_pure = Typing.add_use_clone env ltm uc.uc_pure loc d; }
(*
Local Variables:
......
......@@ -80,7 +80,8 @@ val add_effect_pdecl : Ptree.decl -> uc -> uc
val add_pure_pdecl : Ptree.decl -> uc -> uc
val add_use_clone :
t Mstr.t Env.library -> Theory.theory Mstr.t -> Ptree.use_clone -> uc -> uc
t Mstr.t Env.library -> Theory.theory Mstr.t ->
Loc.position -> Ptree.use_clone -> uc -> uc
(** add in impure, effect and pure *)
(** builtins *)
......
......@@ -731,7 +731,7 @@ and dexpr_desc ~ghost ~userloc env loc = function
and dletrec ~ghost ~userloc env dl =
(* add all functions into environment *)
let add_one env (id, gh, bl, var, t) =
let add_one env (_loc, id, gh, bl, var, t) =
no_ghost gh;
let ty = create_type_var id.id_loc in
let env = add_local_top env id.id ty in
......@@ -2305,7 +2305,7 @@ let find_module penv lmod q id = match q with
(* env = to retrieve theories and modules from the loadpath
lmod = local modules *)
let rec decl ~wp env ltm lmod uc = function
let rec decl ~wp env ltm lmod uc (loc,dcl) = match dcl with
| Ptree.Dlet (id, gh, e) ->
no_ghost gh;
let denv = create_denv uc in
......@@ -2399,7 +2399,7 @@ let rec decl ~wp env ltm lmod uc = function
with ClashSymbol s ->
errorm ~loc "clash with previous symbol %s" s
end
| Ptree.Dnamespace (loc, id, import, dl) ->
| Ptree.Dnamespace (id, import, dl) ->
let uc = open_namespace uc in
let uc = List.fold_left (decl ~wp env ltm lmod) uc dl in
begin try close_namespace uc import id
......@@ -2411,7 +2411,7 @@ let rec decl ~wp env ltm lmod uc = function
| Ptree.Dlogic (PropDecl _ | Meta _ as d) ->
Pgm_module.add_pure_pdecl d uc
| Ptree.Duseclone d ->
Pgm_module.add_use_clone env ltm d uc
Pgm_module.add_use_clone env ltm loc d uc
(*
Local Variables:
......
......@@ -26,4 +26,4 @@ val decl :
wp:bool -> Pgm_module.t Util.Mstr.t Env.library ->
Theory.theory Util.Mstr.t ->
Pgm_module.t Util.Mstr.t ->
Pgm_module.uc -> Ptree.program_decl -> Pgm_module.uc
Pgm_module.uc -> (Ptree.loc * Ptree.program_decl) -> Pgm_module.uc
......@@ -92,6 +92,6 @@ and dexpr_desc =
| DEghost of dexpr
| DEany of dtype_c
and drecfun = ident * ghost * dity * dlambda
and drecfun = loc * ident * ghost * dity * dlambda
and dlambda = dbinder list * dvariant list * dpre * dexpr * dpost * dxpost
......@@ -404,7 +404,7 @@ and de_desc denv loc = function
DElet (id, gh, e1, e2), e2.de_type
| Ptree.Eletrec (rdl, e1) ->
let rdl = dletrec denv rdl in
let add_one denv ({ id = id }, _, dity, _) =
let add_one denv (_, { id = id }, _, dity, _) =
{ denv with locals = Mstr.add id (denv.tvars, dity) denv.locals } in
let denv = List.fold_left add_one denv rdl in
let e1 = dexpr denv e1 in
......@@ -559,16 +559,16 @@ and de_desc denv loc = function
and dletrec denv rdl =
(* add all functions into environment *)
let add_one denv (id, gh, bl, var, tr) =
let add_one denv (_,id,_,_,_,_) =
let res = create_type_variable () in
add_var id res denv, (id, gh, res, bl, var, tr) in
let denv, rdl = Util.map_fold_left add_one denv rdl in
add_var id res denv, res in
let denv, tyl = Util.map_fold_left add_one denv rdl in
(* then type-check all of them and unify *)
let type_one (id, gh, res, bl, var, tr) =
let type_one (loc, id, gh, bl, var, tr) res =
let lam, dity = dlambda denv bl var tr in
Loc.try2 id.id_loc unify dity res;
id, gh, dity, lam in
List.map type_one rdl
loc, id, gh, dity, lam in
List.map2 type_one rdl tyl
and dlambda denv bl var (p, e, (q, xq)) =
let denv,bl,tyl = dbinders denv bl in
......@@ -881,7 +881,7 @@ and expr_desc lenv loc de = match de.de_desc with
e_for pv efrom dir eto inv e1
and expr_rec lenv rdl =
let step1 lenv (id, gh, dity, lam) =
let step1 lenv (_loc, id, gh, dity, lam) =
let vta = match vty_ghostify gh (vty_of_dity dity) with
| VTarrow vta -> vta
| VTvalue _ -> assert false in
......@@ -1304,10 +1304,10 @@ let add_theory lib path mt m =
let { id = id; id_loc = loc } = m.pth_name in
if Mstr.mem id mt then Loc.errorm ~loc "clash with previous theory %s" id;
let uc = create_theory ~path (Denv.create_user_id m.pth_name) in
let rec add_decl uc = function
let rec add_decl uc (loc, decl) = match decl with
| Dlogic d ->
Typing.add_decl uc d
| Duseclone (loc, use, inst) ->
| Duseclone (use, inst) ->
let path, s = Typing.split_qualid use.use_theory in
let th = find_theory loc lib mt path s in
(* open namespace, if any *)
......@@ -1325,7 +1325,7 @@ let add_theory lib path mt m =
| None -> uc
| Some imp -> Theory.close_namespace uc imp use.use_as
end
| Dnamespace (loc, name, import, dl) ->
| Dnamespace (name, import, dl) ->
let uc = Theory.open_namespace uc in
let uc = List.fold_left add_decl uc dl in
Loc.try3 loc Theory.close_namespace uc import name
......@@ -1341,12 +1341,12 @@ let add_module lib path mm mt m =
if Mstr.mem id mm then Loc.errorm ~loc "clash with previous module %s" id;
if Mstr.mem id mt then Loc.errorm ~loc "clash with previous theory %s" id;
let uc = create_module ~path (Denv.create_user_id m.mod_name) in
let rec add_decl uc = function
let rec add_decl uc (loc,decl) = match decl with
| Dlogic (TypeDecl tdl) ->
add_types uc tdl
| Dlogic d ->
add_to_theory Typing.add_decl uc d
| Duseclone (loc, use, inst) ->
| Duseclone (use, inst) ->
let path, s = Typing.split_qualid use.use_theory in
let mth = find_module loc lib mm mt path s in
(* open namespace, if any *)
......@@ -1367,7 +1367,7 @@ let add_module lib path mm mt m =
| None -> uc
| Some imp -> close_namespace uc imp use.use_as
end
| Dnamespace (loc, name, import, dl) ->
| Dnamespace (name, import, dl) ->
let uc = open_namespace uc in
let uc = List.fold_left add_decl uc dl in
Loc.try3 loc close_namespace uc import name
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment