Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits:
2432cce1 by Jonathan Graveline at 2018-05-07T22:21:30Z
New sform_load. Work in progress.
- - - - -
1 changed file:
- src/elab.ml
Changes:
=====================================
src/elab.ml
=====================================
--- a/src/elab.ml
+++ b/src/elab.ml
@@ -108,6 +108,19 @@ let add_special_form (name, func) =
let get_special_form name =
SMap.find name (!special_forms)
+(*
+ Used for sform_load because sform are
+ added before default context's function
+ WARNING :
+ With this setup you can't use special form "load_" within
+ builtins.typer and pervasive.typer!!!
+*)
+let _sform_default_ectx = ref empty_elab_context
+let _sform_default_rctx = ref make_runtime_ctx
+let _set_default_ectx ectx =
+ _sform_default_ectx := ectx
+let _set_default_rctx rctx =
+ _sform_default_rctx := rctx
(* The prefix `elab_check_` is used for functions which do internal checking
* (i.e. errors signalled here correspond to internal errors rather than
@@ -1488,7 +1501,7 @@ let sform_type ctx loc sargs ot =
sform_dummy_ret ctx loc
(* Only print var info *)
-and lexp_print_var_info ctx =
+let lexp_print_var_info ctx =
let ((m, _), env, _) = ctx in
let n = Myers.length env in
@@ -1505,6 +1518,161 @@ and lexp_print_var_info ctx =
print_string "\n")
done
+(* load a whole file as a string (there may be a limit on string size) *)
+let _load_whole_file file =
+ let fin = open_in file in
+ let n = in_channel_length fin in
+ let rawstr = Bytes.create n in
+ really_input fin rawstr 0 n;
+ close_in fin;
+ (Bytes.to_string rawstr)
+
+let rec init_tup (tup : Lexp.lexp) : Lexp.lexp = init_tup' (0,SMap.empty) tup
+
+and init_tup' (depth, var_map) lexp =
+ let redecl _ = Some (depth) in
+ let s_ctx = (depth + 1, var_map) in
+ let init' = init_tup' (depth,var_map) in
+ match lexp with
+
+ | Var ((loc, name), _) -> (
+ match (SMap.find_opt name var_map) with
+ | Some (idx) -> Var ((loc, name), (depth - idx - 1))
+ | None -> (error loc ("undefined variable '"^name^"'"); Var ((loc,name),0))
+ )
+
+ | Metavar (_, subst, (loc, name)) -> (
+ match (SMap.find_opt name var_map) with
+ | Some (idx) -> Metavar ((depth - idx - 1),subst, (loc,name))
+ | None -> (error loc ("undefined variable '"^name^"'"); Metavar (0,subst,(loc,name)))
+ )
+
+ | Susp (e, s) -> Susp ((init' e), s)
+
+ | Let (loc, decls, body) ->
+ let f ((d,vmap),lexps) ((loc,name),l,t) =
+ let vmap' = (SMap.update name redecl vmap) in
+ (d+1,vmap'), ((loc,name),(init_tup' (d,vmap') l),(init_tup' (d,vmap') t)) :: lexps in
+ let (senv',decls') = List.fold_left f ((depth,var_map),[]) decls in
+ Let (loc, (List.rev decls'), (init_tup' senv' body))
+
+ | Arrow(k, v, tp, loc2, expr) -> (
+ match v with
+ | Some (loc,name) ->
+ let vmap' = (SMap.update name redecl var_map) in
+ Arrow (k, v, (init_tup' (depth,vmap') tp), loc2, (init_tup' (depth + 1,vmap') expr))
+ | None -> Arrow(k,v,(init_tup' (depth,var_map) tp),loc2,(init_tup' (depth + 1,var_map) expr))
+ )
+
+ | Lambda(k, (loc, name), ltype, lbody) ->
+ let vmap' = (SMap.update name redecl var_map) in
+ Lambda (k, (loc, name), (init_tup' (depth,vmap') ltype), (init_tup' (depth+1,vmap')lbody))
+
+ | Cons(t, (l,v)) ->
+ let vmap' = (SMap.update v redecl var_map) in
+ Cons ((init_tup' (depth,vmap') t), (l,v))
+
+ | Call(a, args) ->
+ let f ((depth,vmap),lexps) (k,l) =
+ (depth+1,vmap), (k,(init_tup' (depth,vmap) l)) :: lexps in
+ let (senv',args') = List.fold_left f ((depth,var_map),[]) args in
+ Call ((init' a),(List.rev args'))
+
+ | Inductive (a, (b, name), args, ctors) ->
+ let vmap'' = (SMap.update name redecl var_map) in
+ (* args *)
+ let f1 ((depth,vmap),lexps) (k,(l,v),t) =
+ let vmap' = (SMap.update v redecl vmap) in
+ (depth+1,vmap'), (k,(l,v),(init_tup' (depth,vmap) t)) :: lexps in
+ (* ctors sub list fold function *)
+ let f2 ((depth,vmap),lexps) (k,v,t) =
+ (depth+1,vmap), (k,v,(init_tup' (depth,vmap) t)) :: lexps in
+ (* ctors map fold function *)
+ let f3 key ll ((depth,vmap),lexps) =
+ let vmap' = (SMap.update key redecl vmap) in
+ let ((depth,vmap''),ll') = List.fold_left f2 ((depth,vmap'),[]) ll in
+ (depth+1,vmap''), (key,(List.rev ll')) :: lexps in
+ (* list key*a to map when called with fold *)
+ let f4 ctors_map (key,ll) = (SMap.add key ll ctors_map) in
+ (* calling all fold function *)
+ let (senv',args') = List.fold_left f1 ((depth,vmap''),[]) args in
+ let (senv'',ctors_list) = SMap.fold f3 ctors (senv',[]) in
+ let ctors' = List.fold_left f4 SMap.empty (List.rev ctors_list) in
+ Inductive (a,(b,name),(List.rev args'),ctors')
+
+ | Case (a, target, ret, map, dflt) ->
+ let mf (loc,k,l) = (loc,k,(init' l)) in
+ let map' = SMap.map mf map in (
+ match dflt with
+ | None -> Case (a, (init' target), (init' ret), map', None)
+ | Some (v, df) -> Case (a, target, ret, map', Some (v, (init' df)))
+ )
+ (* not handling Builtin... is it needed? *)
+ (* sounds like not builtin anymore if redefined *)
+ | Sort (a, Stype l) -> Sort (a, Stype (init' l))
+ | SortLevel (SLsucc e) -> SortLevel (SLsucc (init' e))
+ | SortLevel (SLlub (e1, e2)) -> SortLevel (SLlub ((init' e1), (init' e2)))
+ | _ -> (lexp_print lexp; lexp)
+
+(* sform_load current elab_context, loc of load, string argument, output type *)
+let sform_load ctx loc sargs ot =
+
+ (* COPY PASTE *) (* see end of file for origin *)
+ let _lexp_decl_str (str: string) tenv grm limit (ctx : elab_context) =
+ let sdecls = _sexp_parse_str str tenv grm limit in
+ lexp_p_decls sdecls ctx in
+
+ let lexp_decl_str str ctx =
+ _lexp_decl_str str default_stt (ectx_get_grammar ctx) (Some ";") ctx in
+
+ let eval_decl_str str lctx rctx =
+ let lxps, lctx = lexp_decl_str str lctx in
+ let elxps = (List.map OL.clean_decls lxps) in
+ (EV.eval_decls_toplevel elxps rctx), lctx in
+ (* END OF COPY PASTE *)
+
+ (* get the whole file as string *)
+ let fstr = match sargs with
+ | [String (_,file_str)] -> _load_whole_file file_str
+ | _ -> "load_error" in
+
+ (* get all runtime_env and elab_context *)
+ let rctx, elctx = eval_decl_str fstr !_sform_default_ectx !_sform_default_rctx in
+
+ (* Things we want : new elab_context, tuple, new grammar, DB.senv_type ... *)
+
+ let lctx = DB.ectx_to_lctx !_sform_default_ectx in
+ let nlctx = DB.ectx_to_lctx elctx in
+ let modtup = OL.ctx2tup lctx nlctx in
+
+ let grm = DB.ectx_get_grammar elctx in
+ let mergefun (str: SMap.key) (a: 't option) (b: 't option) =
+ match a, b with
+ | (Some aa, None) -> Some aa
+ | (None, Some bb) -> Some bb
+ (* Keep the grammar created by the load call *)
+ | (Some aa, Some bb) -> Some aa
+ | (None, None) -> None in
+ let grm' = SMap.merge mergefun grm (ectx_get_grammar ctx) in
+
+ (* need to append tuple to lexp_ctx' and modify senv_type *)
+ (* ??? assuming meta_scope isn't changed, just adding a tuple in the current scope ??? *)
+ let (g,d,l,m) = ctx in
+
+ let modtup' = init_tup' d modtup in
+
+ (* lets get a base for DeBruijn index *)
+ (*let tup_setype = *)
+
+ (*sform_dummy_ret modtup loc*)
+ (
+ print_string "\nhere's unmodified tuple : \n\n";
+ lexp_print modtup;
+ print_string "\n\nhere's modified tuple : \n\n";
+ lexp_print modtup';
+ sform_dummy_ret (grm',d,l,m) loc
+ )
+
(* Register special forms. *)
let register_special_forms () =
List.iter add_special_form
@@ -1524,6 +1692,7 @@ let register_special_forms () =
("case_", sform_case);
("let_in_", sform_letin);
("Type_", sform_type);
+ ("load_", sform_load);
(* FIXME: We should add here `let_in_`, `case_`, etc... *)
("get-attribute", sform_get_attribute);
("new-attribute", sform_new_attribute);
@@ -1589,9 +1758,13 @@ let default_ectx
builtin_size := get_size lctx;
let lctx = read_file (btl_folder ^ "/pervasive.typer") lctx in
+ let _ = _set_default_ectx lctx in
lctx
-let default_rctx = EV.from_ectx default_ectx
+let default_rctx =
+ let rctx = EV.from_ectx default_ectx in
+ let _ = _set_default_rctx rctx in
+ rctx
(* String Parsing
* --------------------------------------------------------- *)
View it on GitLab: https://gitlab.com/monnier/typer/commit/2432cce16b3e73a2b2a33caf8652dccf482…
--
View it on GitLab: https://gitlab.com/monnier/typer/commit/2432cce16b3e73a2b2a33caf8652dccf482…
You're receiving this email because of your account on gitlab.com.
Stefan pushed to branch master at Stefan / Typer
Commits:
3a47ced1 by Stefan Monnier at 2018-05-01T16:20:42Z
Adjust to newer OCaml version
- - - - -
3 changed files:
- src/lexp.ml
- tests/utest_lib.ml
- tests/utest_main.ml
Changes:
=====================================
src/lexp.ml
=====================================
--- a/src/lexp.ml
+++ b/src/lexp.ml
@@ -1,6 +1,6 @@
(* lexp.ml --- Lambda-expressions: the core language.
-Copyright (C) 2011-2017 Free Software Foundation, Inc.
+Copyright (C) 2011-2018 Free Software Foundation, Inc.
Author: Stefan Monnier <monnier(a)iro.umontreal.ca>
Keywords: languages, lisp, dependent types.
@@ -175,7 +175,7 @@ let metavar_lookup (id : meta_id) : metavar_info
* try Hashtbl.find hc_table e
* with Not_found -> Hashtbl.add hc_table e e; e *)
-module WHC = Tweak.Make (struct type t = lexp
+module WHC = Weak.Make (struct type t = lexp
(* Using (=) instead of `compare` results
* in an *enormous* slowdown. Apparently
* `compare` checks == before recursing
=====================================
tests/utest_lib.ml
=====================================
--- a/tests/utest_lib.ml
+++ b/tests/utest_lib.ml
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2016 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2016, 2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -80,26 +80,28 @@ let set_verbose lvl =
let arg_defs = [
("--verbose=",
- Arg.Int set_verbose, " Set verbose level");
+ Arg.Int set_verbose, " Set verbose level");
("--samples=",
- Arg.String (fun g -> _global_sample_dir := g), " Set sample directory");
-(* Allow users to select which test to run *)
+ Arg.String (fun g -> _global_sample_dir := g), " Set sample directory");
+ (* Allow users to select which test to run *)
("--fsection=",
- Arg.String (fun g -> _global_fsection := String.uppercase g), " Set test filter");
+ Arg.String (fun g -> _global_fsection := String.uppercase_ascii g),
+ " Set test filter");
("--ftitle=",
- Arg.String (fun g -> _global_ftitle := String.uppercase g), " Set test filter");
-]
+ Arg.String (fun g -> _global_ftitle := String.uppercase_ascii g),
+ " Set test filter");
+ ]
let must_run_section str =
- if (String.length !_global_fsection) != 0 then(
- let name = String.uppercase str in
- if name = !_global_fsection then true else false)
+ if (String.length !_global_fsection) != 0 then
+ let name = String.uppercase_ascii str in
+ if name = !_global_fsection then true else false
else true
let must_run_title str =
- if (String.length !_global_ftitle) != 0 then(
- let name = String.uppercase str in
- if name = !_global_ftitle then true else false)
+ if (String.length !_global_ftitle) != 0 then
+ let name = String.uppercase_ascii str in
+ if name = !_global_ftitle then true else false
else true
let parse_args () = Arg.parse arg_defs (fun s -> ()) ""
=====================================
tests/utest_main.ml
=====================================
--- a/tests/utest_main.ml
+++ b/tests/utest_main.ml
@@ -3,7 +3,7 @@
*
* ---------------------------------------------------------------------------
*
- * Copyright (C) 2011-2016 Free Software Foundation, Inc.
+ * Copyright (C) 2011-2016, 2018 Free Software Foundation, Inc.
*
* Author: Pierre Delaunay <pierre.delaunay(a)hec.ca>
* Keywords: languages, lisp, dependent types.
@@ -43,19 +43,19 @@ let _global_filter = ref false
let arg_defs = [
("--verbose=",
- Arg.Int (fun g -> _global_verbose_lvl := g), " Set verbose level");
+ Arg.Int (fun g -> _global_verbose_lvl := g), " Set verbose level");
("--samples=",
- Arg.String (fun g -> _global_sample_dir := g), " Set sample directory");
+ Arg.String (fun g -> _global_sample_dir := g), " Set sample directory");
("--tests=",
- Arg.String (fun g -> _global_tests_dir := g), " Set tests directory");
+ Arg.String (fun g -> _global_tests_dir := g), " Set tests directory");
(* Allow users to select which test to run *)
("--fsection=",
- Arg.String (fun g -> _global_fsection := String.uppercase g;
- _global_filter := true), " Set test filter");
+ Arg.String (fun g -> _global_fsection := String.uppercase_ascii g;
+ _global_filter := true), " Set test filter");
("--ftitle=",
- Arg.String (fun g -> _global_ftitle := String.uppercase g;
- _global_filter := true), " Set test filter");
-]
+ Arg.String (fun g -> _global_ftitle := String.uppercase_ascii g;
+ _global_filter := true), " Set test filter");
+ ]
let verbose n = (n <= (!_global_verbose_lvl))
@@ -86,9 +86,9 @@ let print_file_name i n name pass =
print_string reset
let must_run str =
- if (!_global_filter) then(
- let name = String.uppercase (cut_name str) in
- if name = !_global_fsection then true else false)
+ if (!_global_filter) then
+ let name = String.uppercase_ascii (cut_name str) in
+ if name = !_global_fsection then true else false
else true
(* search *_test.byte executable en run them
View it on GitLab: https://gitlab.com/monnier/typer/commit/3a47ced12982355439efa8304b6cd40f618…
---
View it on GitLab: https://gitlab.com/monnier/typer/commit/3a47ced12982355439efa8304b6cd40f618…
You're receiving this email because of your account on gitlab.com.