Jonathan Graveline pushed to branch graveline at Stefan / Typer
Commits: 905fc6f0 by Jonathan Graveline at 2018-05-10T01:08:36Z Modification and use of susp within sform_load - - - - -
1 changed file:
- src/elab.ml
Changes:
===================================== src/elab.ml ===================================== --- a/src/elab.ml +++ b/src/elab.ml @@ -50,6 +50,7 @@ open Lexp open Env open Debruijn module DB = Debruijn +module M = Myers module EV = Eval
open Grammar @@ -1518,160 +1519,37 @@ let 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 sform_load user_elctx loc sargs ot = + + let read_file file_name elctx = + let pres = prelex_file file_name in + let sxps = lex default_stt pres in + let nods = sexp_parse_all_to_list (ectx_get_grammar elctx) + sxps (Some ";") in + let _, elctx = lexp_p_decls nods elctx + in elctx 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 + 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
- (* lets get a base for DeBruijn index *) - (*let tup_setype = *) + let tuple = OL.ctx2tup def_lctx loaded_lctx in + let tuple' = Lexp.mkSusp tuple (S.Shift (S.Identity,(user_len - def_len))) in
- (*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 - ) + (* + 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) + *) + (tuple',Lazy)
(* Register special forms. *) let register_special_forms () =
View it on GitLab: https://gitlab.com/monnier/typer/commit/905fc6f078077666c408459718b161e7ad4e...