[Git][monnier/typer][graveline] Correction in 'sform_load' and removed unused '_sform_default_rctx'
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... -- View it on GitLab: https://gitlab.com/monnier/typer/commit/34d24f66d0bbe6c30a29862da7c576694a84... You're receiving this email because of your account on gitlab.com.
Afficher les réponses par date
participants (1)
-
Jonathan Graveline