Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: 34d24f66 by Jonathan Graveline at 2018-05-10T15:20:01Z Correction in 'sform_load' and removed unused '_sform_default_rctx' - - - - -
1 changed file:
- src/elab.ml
Changes:
===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -114,14 +114,11 @@ let get_special_form name = added before default context's function WARNING : With this setup you can't use special form "load_" within - builtins.typer and pervasive.typer!!! + 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 @@ -1519,8 +1516,13 @@ let lexp_print_var_info ctx = print_string "\n") done
-(* sform_load current elab_context, loc of load, string argument, output type *) -let sform_load user_elctx loc sargs ot = +(* arguments : + elab_context from where load is called, + loc is location of load call, + sargs should be an array of one file name, + ot is the expected type of output tuple. +*) +let sform_load usr_elctx loc sargs ot =
let read_file file_name elctx = let pres = prelex_file file_name in @@ -1529,26 +1531,24 @@ let sform_load user_elctx loc sargs ot = sxps (Some ";") in let _, elctx = lexp_p_decls nods elctx in elctx in - - let loaded_elctx = match sargs with - | [String (_,path); ] -> read_file path !_sform_default_ectx - | _ -> (error loc "argument to load should be one file path (String)"; !_sform_default_ectx) in
- let (_,(user_len,var_map),user_lctx,_) = user_elctx in - let (_,(_,_),loaded_lctx,_) = loaded_elctx in - let (_,(def_len,_),def_lctx,_) = !_sform_default_ectx in + (* read file as elab_context *) + let ld_elctx = match sargs with + | [String (_,file_name)] -> read_file file_name !_sform_default_ectx + | _ -> (error loc "argument to load should be one file name (String)"; !_sform_default_ectx) in + + (* get lexp_context *) + let usr_lctx = ectx_to_lctx usr_elctx in + let ld_lctx = ectx_to_lctx ld_elctx in + let dflt_lctx = ectx_to_lctx !_sform_default_ectx in
- let tuple = OL.ctx2tup def_lctx loaded_lctx in - let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(user_len - def_len))) in + (* length of some lexp_context *) + let usr_len = M.length usr_lctx in + let dflt_len = M.length dflt_lctx in
- (* - print_string "\nHere's unmodified tuple : \n"; - lexp_print tuple; - print_string "\nHere's modified tuple : \n"; - lexp_print tuple'; - (*sform_dummy_ret user_elctx loc*) - (tuple', Lazy) - *) + (* create a tuple from context and shift it to user context *) + let tuple = OL.ctx2tup dflt_lctx ld_lctx in + let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(usr_len - dflt_len))) in (tuple',Lazy)
(* Register special forms. *) @@ -1641,7 +1641,6 @@ let 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/34d24f66d0bbe6c30a29862da7c576694a84...
Afficher les réponses par date