Skip to content

Commit

Permalink
extrraction: ml: unconditionally sanitize identifiers
Browse files Browse the repository at this point in the history 
in case some internal F* identifiers are not valid in OCaml,this
should do the trick of fixing it up

c.f. #1001
  • Loading branch information
@mtzguido
mtzguido committed May 4, 2017
1 parent 2ae9572 commit 2345691
Show file tree
Hide file tree
Showing 5 changed files with 172 additions and 81 deletions.
19 changes: 18 additions & 1 deletion src/extraction/FStar.Extraction.ML.UEnv.fs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,6 +191,22 @@ let extend_ty (g:env) (a:bv) (mapped_to:option<mlty>) : env =
let tcenv = TypeChecker.Env.push_bv g.tcenv a in // push_local_binding g.tcenv (Env.Binding_typ(a.v, a.sort)) in
{g with gamma=gamma; tcenv=tcenv}

let sanitize (s:string) : string =
let mem = FStar.List.mem in
let low = ['a';'b';'c';'d';'e';'f';'g';'h';'i';'j';'k';'l';'m';'o';'p';'q';'r';'s';'t';'u';'v';'w';'x';'y';'z'] in
let high = ['A';'B';'C';'D';'E';'F';'G';'H';'I';'J';'K';'L';'M';'O';'P';'Q';'R';'S';'T';'U';'V';'W';'X';'Y';'Z'] in
let num = ['0';'1';'2';'3';'4';'5';'6';'7';'8';'9'] in
let spec = ['_';'\''] in
let cs = FStar.String.list_of_string s in
let valid c = mem c (low@high@num@spec) in
let cs' = List.fold_right (fun c cs -> (if valid c then [c] else ['_';'_'])@cs) cs [] in
let cs' = match cs' with
| (c::cs) when mem c num ->
'_'::c::cs
| _ -> cs in
FStar.String.string_of_list cs'


// Need to avoid shadowing an existing identifier (see comment about ty_or_exp_b)
let find_uniq gamma mlident =
let rec find_uniq mlident i =
Expand All @@ -207,6 +223,7 @@ let find_uniq gamma mlident =
else
target_mlident
in
let mlident = sanitize mlident in
find_uniq mlident 0

let extend_bv (g:env) (x:bv) (t_x:mltyscheme) (add_unit:bool) (is_rec:bool)
Expand Down Expand Up @@ -302,4 +319,4 @@ let action_name (ed:Syntax.eff_decl) (a:Syntax.action) =
let nm = a.action_name.ident.idText in
let module_name = ed.mname.ns in
let lid = Ident.lid_of_ids (module_name@[Ident.id_of_text nm]) in
(mlpath_of_lident lid), lid
(mlpath_of_lident lid), lid
158 changes: 116 additions & 42 deletions src/ocaml-output/FStar_Extraction_ML_UEnv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -269,6 +269,79 @@ let extend_ty:
tydefs = (uu___111_566.tydefs);
currentModule = (uu___111_566.currentModule)
}
let sanitize: Prims.string -> Prims.string =
fun s ->
let mem1 = FStar_List.mem in
let low =
['a';
'b';
'c';
'd';
'e';
'f';
'g';
'h';
'i';
'j';
'k';
'l';
'm';
'o';
'p';
'q';
'r';
's';
't';
'u';
'v';
'w';
'x';
'y';
'z'] in
let high =
['A';
'B';
'C';
'D';
'E';
'F';
'G';
'H';
'I';
'J';
'K';
'L';
'M';
'O';
'P';
'Q';
'R';
'S';
'T';
'U';
'V';
'W';
'X';
'Y';
'Z'] in
let num = ['0'; '1'; '2'; '3'; '4'; '5'; '6'; '7'; '8'; '9'] in
let spec = ['_'; '\''] in
let cs = FStar_String.list_of_string s in
let valid c =
mem1 c
(FStar_List.append low
(FStar_List.append high (FStar_List.append num spec))) in
let cs' =
FStar_List.fold_right
(fun c ->
fun cs1 ->
FStar_List.append (if valid c then [c] else ['_'; '_']) cs1) cs
[] in
let cs'1 =
match cs' with
| c::cs1 when mem1 c num -> '_' :: c :: cs1
| uu____604 -> cs in
FStar_String.string_of_list cs'1
let find_uniq: binding Prims.list -> Prims.string -> Prims.string =
fun gamma ->
fun mlident ->
Expand All @@ -280,8 +353,8 @@ let find_uniq: binding Prims.list -> Prims.string -> Prims.string =
let target_mlident = Prims.strcat mlident1 suffix in
let has_collision =
FStar_List.existsb
(fun uu___110_586 ->
match uu___110_586 with
(fun uu___110_625 ->
match uu___110_625 with
| Bv (_,FStar_Util.Inl (mlident',_))|Fv
(_,FStar_Util.Inl (mlident',_)) ->
target_mlident = (Prims.fst mlident')
Expand All @@ -291,7 +364,8 @@ let find_uniq: binding Prims.list -> Prims.string -> Prims.string =
if has_collision
then find_uniq mlident1 (i + (Prims.parse_int "1"))
else target_mlident in
find_uniq mlident (Prims.parse_int "0")
let mlident1 = sanitize mlident in
find_uniq mlident1 (Prims.parse_int "0")
let extend_bv:
env ->
FStar_Syntax_Syntax.bv ->
Expand All @@ -309,9 +383,9 @@ let extend_bv:
let ml_ty =
match t_x with
| ([],t) -> t
| uu____683 -> FStar_Extraction_ML_Syntax.MLTY_Top in
let uu____684 = FStar_Extraction_ML_Syntax.bv_as_mlident x in
match uu____684 with
| uu____723 -> FStar_Extraction_ML_Syntax.MLTY_Top in
let uu____724 = FStar_Extraction_ML_Syntax.bv_as_mlident x in
match uu____724 with
| (mlident,nocluewhat) ->
let mlsymbol = find_uniq g.gamma mlident in
let mlident1 = (mlsymbol, nocluewhat) in
Expand All @@ -334,14 +408,14 @@ let extend_bv:
(Bv (x, (FStar_Util.Inr (mlsymbol, mlx1, t_x, is_rec))))
:: (g.gamma) in
let tcenv =
let uu____715 = FStar_Syntax_Syntax.binders_of_list [x] in
FStar_TypeChecker_Env.push_binders g.tcenv uu____715 in
((let uu___112_718 = g in
let uu____755 = FStar_Syntax_Syntax.binders_of_list [x] in
FStar_TypeChecker_Env.push_binders g.tcenv uu____755 in
((let uu___112_758 = g in
{
tcenv;
gamma;
tydefs = (uu___112_718.tydefs);
currentModule = (uu___112_718.currentModule)
tydefs = (uu___112_758.tydefs);
currentModule = (uu___112_758.currentModule)
}), mlident1)
let rec mltyFvars:
FStar_Extraction_ML_Syntax.mlty ->
Expand All @@ -351,8 +425,8 @@ let rec mltyFvars:
match t with
| FStar_Extraction_ML_Syntax.MLTY_Var x -> [x]
| FStar_Extraction_ML_Syntax.MLTY_Fun (t1,f,t2) ->
let uu____729 = mltyFvars t1 in
let uu____731 = mltyFvars t2 in FStar_List.append uu____729 uu____731
let uu____769 = mltyFvars t1 in
let uu____771 = mltyFvars t2 in FStar_List.append uu____769 uu____771
| FStar_Extraction_ML_Syntax.MLTY_Named (args,path) ->
FStar_List.collect mltyFvars args
| FStar_Extraction_ML_Syntax.MLTY_Tuple ts ->
Expand All @@ -369,8 +443,8 @@ let rec subsetMlidents:
| [] -> true
let tySchemeIsClosed: FStar_Extraction_ML_Syntax.mltyscheme -> Prims.bool =
fun tys ->
let uu____755 = mltyFvars (Prims.snd tys) in
subsetMlidents uu____755 (Prims.fst tys)
let uu____795 = mltyFvars (Prims.snd tys) in
subsetMlidents uu____795 (Prims.fst tys)
let extend_fv':
env ->
FStar_Syntax_Syntax.fv ->
Expand All @@ -385,21 +459,21 @@ let extend_fv':
fun t_x ->
fun add_unit ->
fun is_rec ->
let uu____779 = tySchemeIsClosed t_x in
if uu____779
let uu____819 = tySchemeIsClosed t_x in
if uu____819
then
let ml_ty =
match t_x with
| ([],t) -> t
| uu____785 -> FStar_Extraction_ML_Syntax.MLTY_Top in
let uu____786 =
let uu____792 = y in
match uu____792 with
| uu____825 -> FStar_Extraction_ML_Syntax.MLTY_Top in
let uu____826 =
let uu____832 = y in
match uu____832 with
| (ns,i) ->
let mlsymbol =
FStar_Extraction_ML_Syntax.avoid_keyword i in
((ns, mlsymbol), mlsymbol) in
match uu____786 with
match uu____826 with
| (mlpath,mlsymbol) ->
let mly = FStar_Extraction_ML_Syntax.MLE_Name mlpath in
let mly1 =
Expand All @@ -416,12 +490,12 @@ let extend_fv':
let gamma =
(Fv (x, (FStar_Util.Inr (mlsymbol, mly1, t_x, is_rec))))
:: (g.gamma) in
((let uu___113_839 = g in
((let uu___113_879 = g in
{
tcenv = (uu___113_839.tcenv);
tcenv = (uu___113_879.tcenv);
gamma;
tydefs = (uu___113_839.tydefs);
currentModule = (uu___113_839.currentModule)
tydefs = (uu___113_879.tydefs);
currentModule = (uu___113_879.currentModule)
}), (mlsymbol, (Prims.parse_int "0")))
else failwith "freevars found"
let extend_fv:
Expand Down Expand Up @@ -456,10 +530,10 @@ let extend_lb:
match l with
| FStar_Util.Inl x -> extend_bv g x t_x add_unit is_rec false
| FStar_Util.Inr f ->
let uu____893 =
let uu____933 =
FStar_Extraction_ML_Syntax.mlpath_of_lident
(f.FStar_Syntax_Syntax.fv_name).FStar_Syntax_Syntax.v in
(match uu____893 with
(match uu____933 with
| (p,y) -> extend_fv' g f (p, y) t_x add_unit is_rec)
let extend_tydef:
env -> FStar_Syntax_Syntax.fv -> FStar_Extraction_ML_Syntax.mltydecl -> env
Expand All @@ -468,12 +542,12 @@ let extend_tydef:
fun fv ->
fun td ->
let m = module_name_of_fv fv in
let uu___114_916 = g in
let uu___114_956 = g in
{
tcenv = (uu___114_916.tcenv);
gamma = (uu___114_916.gamma);
tcenv = (uu___114_956.tcenv);
gamma = (uu___114_956.gamma);
tydefs = ((m, td) :: (g.tydefs));
currentModule = (uu___114_916.currentModule)
currentModule = (uu___114_956.currentModule)
}
let emptyMlPath:
(FStar_Extraction_ML_Syntax.mlsymbol Prims.list* Prims.string) = ([], "")
Expand All @@ -489,14 +563,14 @@ let mkContext: FStar_TypeChecker_Env.env -> env =
([], (["Prims"], "string"))),
FStar_Extraction_ML_Syntax.E_IMPURE,
(FStar_Extraction_ML_Syntax.MLTY_Var a)))) in
let uu____953 =
let uu____956 =
let uu____957 =
let uu____993 =
let uu____996 =
let uu____997 =
FStar_Syntax_Syntax.lid_as_fv FStar_Syntax_Const.failwith_lid
FStar_Syntax_Syntax.Delta_constant None in
FStar_Util.Inr uu____957 in
extend_lb env uu____956 FStar_Syntax_Syntax.tun failwith_ty false false in
FStar_All.pipe_right uu____953 Prims.fst
FStar_Util.Inr uu____997 in
extend_lb env uu____996 FStar_Syntax_Syntax.tun failwith_ty false false in
FStar_All.pipe_right uu____993 Prims.fst
let monad_op_name:
FStar_Syntax_Syntax.eff_decl ->
Prims.string -> (FStar_Extraction_ML_Syntax.mlpath* FStar_Ident.lident)
Expand All @@ -506,8 +580,8 @@ let monad_op_name:
let lid =
FStar_Syntax_Util.mk_field_projector_name_from_ident
ed.FStar_Syntax_Syntax.mname (FStar_Ident.id_of_text nm) in
let uu____969 = FStar_Extraction_ML_Syntax.mlpath_of_lident lid in
(uu____969, lid)
let uu____1009 = FStar_Extraction_ML_Syntax.mlpath_of_lident lid in
(uu____1009, lid)
let action_name:
FStar_Syntax_Syntax.eff_decl ->
FStar_Syntax_Syntax.action ->
Expand All @@ -521,5 +595,5 @@ let action_name:
let lid =
FStar_Ident.lid_of_ids
(FStar_List.append module_name [FStar_Ident.id_of_text nm]) in
let uu____982 = FStar_Extraction_ML_Syntax.mlpath_of_lident lid in
(uu____982, lid)
let uu____1022 = FStar_Extraction_ML_Syntax.mlpath_of_lident lid in
(uu____1022, lid)
48 changes: 24 additions & 24 deletions src/ocaml-output/FStar_Legacy_Interactive.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -48,55 +48,55 @@ let push:
match uu____218 with
| (dsenv,env) ->
let env1 =
let uu___234_229 = env in
let uu___230_229 = env in
{
FStar_TypeChecker_Env.solver =
(uu___234_229.FStar_TypeChecker_Env.solver);
(uu___230_229.FStar_TypeChecker_Env.solver);
FStar_TypeChecker_Env.range =
(uu___234_229.FStar_TypeChecker_Env.range);
(uu___230_229.FStar_TypeChecker_Env.range);
FStar_TypeChecker_Env.curmodule =
(uu___234_229.FStar_TypeChecker_Env.curmodule);
(uu___230_229.FStar_TypeChecker_Env.curmodule);
FStar_TypeChecker_Env.gamma =
(uu___234_229.FStar_TypeChecker_Env.gamma);
(uu___230_229.FStar_TypeChecker_Env.gamma);
FStar_TypeChecker_Env.gamma_cache =
(uu___234_229.FStar_TypeChecker_Env.gamma_cache);
(uu___230_229.FStar_TypeChecker_Env.gamma_cache);
FStar_TypeChecker_Env.modules =
(uu___234_229.FStar_TypeChecker_Env.modules);
(uu___230_229.FStar_TypeChecker_Env.modules);
FStar_TypeChecker_Env.expected_typ =
(uu___234_229.FStar_TypeChecker_Env.expected_typ);
(uu___230_229.FStar_TypeChecker_Env.expected_typ);
FStar_TypeChecker_Env.sigtab =
(uu___234_229.FStar_TypeChecker_Env.sigtab);
(uu___230_229.FStar_TypeChecker_Env.sigtab);
FStar_TypeChecker_Env.is_pattern =
(uu___234_229.FStar_TypeChecker_Env.is_pattern);
(uu___230_229.FStar_TypeChecker_Env.is_pattern);
FStar_TypeChecker_Env.instantiate_imp =
(uu___234_229.FStar_TypeChecker_Env.instantiate_imp);
(uu___230_229.FStar_TypeChecker_Env.instantiate_imp);
FStar_TypeChecker_Env.effects =
(uu___234_229.FStar_TypeChecker_Env.effects);
(uu___230_229.FStar_TypeChecker_Env.effects);
FStar_TypeChecker_Env.generalize =
(uu___234_229.FStar_TypeChecker_Env.generalize);
(uu___230_229.FStar_TypeChecker_Env.generalize);
FStar_TypeChecker_Env.letrecs =
(uu___234_229.FStar_TypeChecker_Env.letrecs);
(uu___230_229.FStar_TypeChecker_Env.letrecs);
FStar_TypeChecker_Env.top_level =
(uu___234_229.FStar_TypeChecker_Env.top_level);
(uu___230_229.FStar_TypeChecker_Env.top_level);
FStar_TypeChecker_Env.check_uvars =
(uu___234_229.FStar_TypeChecker_Env.check_uvars);
(uu___230_229.FStar_TypeChecker_Env.check_uvars);
FStar_TypeChecker_Env.use_eq =
(uu___234_229.FStar_TypeChecker_Env.use_eq);
(uu___230_229.FStar_TypeChecker_Env.use_eq);
FStar_TypeChecker_Env.is_iface =
(uu___234_229.FStar_TypeChecker_Env.is_iface);
(uu___230_229.FStar_TypeChecker_Env.is_iface);
FStar_TypeChecker_Env.admit =
(uu___234_229.FStar_TypeChecker_Env.admit);
(uu___230_229.FStar_TypeChecker_Env.admit);
FStar_TypeChecker_Env.lax = lax1;
FStar_TypeChecker_Env.lax_universes =
(uu___234_229.FStar_TypeChecker_Env.lax_universes);
(uu___230_229.FStar_TypeChecker_Env.lax_universes);
FStar_TypeChecker_Env.type_of =
(uu___234_229.FStar_TypeChecker_Env.type_of);
(uu___230_229.FStar_TypeChecker_Env.type_of);
FStar_TypeChecker_Env.universe_of =
(uu___234_229.FStar_TypeChecker_Env.universe_of);
(uu___230_229.FStar_TypeChecker_Env.universe_of);
FStar_TypeChecker_Env.use_bv_sorts =
(uu___234_229.FStar_TypeChecker_Env.use_bv_sorts);
(uu___230_229.FStar_TypeChecker_Env.use_bv_sorts);
FStar_TypeChecker_Env.qname_and_index =
(uu___234_229.FStar_TypeChecker_Env.qname_and_index)
(uu___230_229.FStar_TypeChecker_Env.qname_and_index)
} in
let res = FStar_Universal.push_context (dsenv, env1) msg in
(FStar_Options.push ();
Expand Down
2 changes: 1 addition & 1 deletion src/ocaml-output/FStar_Main.ml
View file
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
open Prims
let uu___237: Prims.unit = FStar_Version.dummy ()
let uu___233: Prims.unit = FStar_Version.dummy ()
let process_args:
Prims.unit -> (FStar_Getopt.parse_cmdline_res* Prims.string Prims.list) =
fun uu____6 -> FStar_Options.parse_cmd_line ()
Expand Down
Loading

0 comments on commit 2345691

Please sign in to comment.