Commit 4d1a93e2 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

don't accept "use export T as ..." (thanks, François)

parent f759427d
......@@ -333,16 +333,17 @@ use_clone:
;
use:
| imp_exp tqualid
{ { use_theory = $2; use_as = qualid_last $2; use_imp_exp = $1 } }
| imp_exp tqualid AS uident
{ { use_theory = $2; use_as = $4.id; use_imp_exp = $1 } }
| opt_import tqualid
{ { use_theory = $2; use_import = Some ($1, qualid_last $2) } }
| opt_import tqualid AS uident
{ { use_theory = $2; use_import = Some ($1, $4.id) } }
| EXPORT tqualid
{ { use_theory = $2; use_import = None } }
;
imp_exp:
| IMPORT { Some true }
| EXPORT { None }
| /* epsilon */ { Some false }
opt_import:
| /* epsilon */ { false }
| IMPORT { true }
;
clone_subst:
......
......@@ -87,10 +87,8 @@ type plogic_type =
| PFunction of pty list * pty
type use = {
use_theory : qualid;
use_as : string;
use_imp_exp : bool option;
(* None = export, Some false = default, Some true = import *)
use_theory : qualid;
use_import : (bool (* import *) * string (* as *)) option;
}
type clone_subst =
......
......@@ -1187,12 +1187,12 @@ let add_use_clone env lenv th loc (use, subst) =
| None -> use_export th t
| Some s -> clone_export th t (type_inst th t s)
in
let use_or_clone th = match use.use_imp_exp with
| Some imp ->
let use_or_clone th = match use.use_import with
| Some (import, use_as) ->
(* use T = namespace T use_export T end *)
let th = open_namespace th use.use_as in
let th = open_namespace th use_as in
let th = use_or_clone th in
close_namespace th imp
close_namespace th import
| None ->
use_or_clone th
in
......
......@@ -1982,16 +1982,17 @@ let use_clone_pure lib mth uc loc (use,inst) =
let path, s = Typing.split_qualid use.use_theory in
let th = find_theory loc lib mth path s in
(* open namespace, if any *)
let uc = if use.use_imp_exp = None then uc
else Theory.open_namespace uc use.use_as in
let uc = match use.use_import with
| Some (_, use_as) -> Theory.open_namespace uc use_as
| None -> uc in
(* use or clone *)
let uc = match inst with
| None -> Theory.use_export uc th
| Some inst -> Theory.clone_export uc th (Typing.type_inst uc th inst) in
(* close namespace, if any *)
match use.use_imp_exp with
match use.use_import with
| Some (import, _) -> Theory.close_namespace uc import
| None -> uc
| Some imp -> Theory.close_namespace uc imp
let use_clone_pure lib mth uc loc use =
if Debug.test_flag Typing.debug_parse_only then uc else
......@@ -2001,8 +2002,9 @@ let use_clone lib mmd mth uc loc (use,inst) =
let path, s = Typing.split_qualid use.use_theory in
let mth = find_module loc lib mmd mth path s in
(* open namespace, if any *)
let uc = if use.use_imp_exp = None then uc
else open_namespace uc use.use_as in
let uc = match use.use_import with
| Some (_, use_as) -> open_namespace uc use_as
| None -> uc in
(* use or clone *)
let uc = match mth, inst with
| Module m, None -> use_export uc m
......@@ -2012,9 +2014,9 @@ let use_clone lib mmd mth uc loc (use,inst) =
| Theory th, Some inst ->
clone_export_theory uc th (Typing.type_inst (get_theory uc) th inst) in
(* close namespace, if any *)
match use.use_imp_exp with
match use.use_import with
| Some (import, _) -> close_namespace uc import
| None -> uc
| Some imp -> close_namespace uc imp
let use_clone lib mmd mth uc loc use =
if Debug.test_flag Typing.debug_parse_only then uc else
......
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