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/2432cce16b3e73a2b2a33caf8652dccf4820...