Skip to content
Snippets Groups Projects
Commit a6c8ca27 authored by charguer's avatar charguer Committed by Thomas Wood
Browse files

nim

parents db267237 444a7264
No related branches found
No related tags found
No related merge requests found
......@@ -20,45 +20,57 @@ let string_of_lident idt =
let names = Longident.flatten idt in
String.concat "." names
let string_of_lident_loc li =
string_of_lident li.txt
let string_of_constant = function
| Const_int n -> string_of_int n
| Const_char c -> String.make 1 c
| Const_string (s, _) -> s
(*| Const_char c -> String.make 1 c
| Const_string (s, _) -> "\"" ^ s ^ "\"" *)
| Const_float f -> f
| Const_int32 _ -> unsupported "int32 type"
(*| Const_int32 _ -> unsupported "int32 type"
| Const_int64 _ -> unsupported "int64 type"
| Const_nativeint _ -> unsupported "native int type"
| Const_nativeint _ -> unsupported "native int type"*)
| _ -> unsupported "constant"
(*
let string_of_recflag = function
| Nonrecursive -> ""
| Recursive -> " rec"
*)
(*#########################################################################*)
(* ** Printing of items *)
(*
let string_of_typed_var s t =
sprintf "(%s : %s)" s (string_of_type_exp t)
*)
(*
let string_of_path p =
Path.name p
*)
let show_string s =
s
(*#########################################################################*)
(* ** Some Contexts *)
let create_context l = l
(*#########################################################################*)
(* ** Printing of patterns *)
let string_of_pattern par p =
let string_of_pattern matchedexpr par p =
(* It also returns a context of expressions to be substituted. *)
let rec aux par p =
match p.pat_desc with
| Tpat_any -> "_"
| Tpat_var (id,_) -> string_of_typed_var (string_of_ident id) p.pat_type
| Tpat_any -> "default",
create_context []
| Tpat_var (id,_) -> "default",
create_context [id, matchedexpr]
(*
| Tpat_alias (p, ak, _) -> unsupported "alias patterns"
(* let sp = aux false p in
begin match ak with
......@@ -66,31 +78,42 @@ let string_of_pattern par p =
| TPat_constraint _ -> sp
| TPat_type pp -> sp (* ignore type *)
end *)
*)
| Tpat_constant c ->
sprintf "%s" (string_of_constant c)
sprintf "case %s" (string_of_constant c),
create_context []
| Tpat_tuple l ->
show_par true (sprintf "%s" (show_list (aux false) "," l))
| Tpat_construct (p,cd,ps) ->
let c = string_of_lident_loc p in
"default",
let li = List.length l in
create_context
(List.flatten (List.mapi (fun i -> function
| Tpat_any -> []
| Tpat_var (id, _) ->
[id, "proj_" ^ string_of_int i ^ "_" ^ string_of_int li ^ "(" ^ matchedexpr ^ ")"]) l))
| Tpat_construct (p,cd,ps) -> unsupported "construct patterns"
(*
let c = string_of_path p in
if ps = []
then c
else if List.length ps = 1
then show_par par (c ^ " " ^ aux true (List.hd ps))
else
show_par par (sprintf "%s (%s)" c (show_list (aux false) "," ps))
| Tpat_or (p1,p2,_) ->
show_par par (sprintf "%s (%s)" c (show_list (aux false) "," ps)) *)
(*| Tpat_or (p1,p2,_) ->
show_par par (sprintf "%s | %s" (aux false p1) (aux false p2))
| Tpat_lazy p1 ->
show_par par (sprintf "lazy %s" (aux true p1))
| Tpat_variant (_,_,_) -> unsupported "variant patterns"
| Tpat_record _ -> unsupported "record patterns"
| Tpat_array pats -> unsupported "array patterns"
| Tpat_array pats -> unsupported "array patterns"*)
| _ -> unsupported "pattern"
in
aux false p
let string_of_let_pattern par p =
let _typ = p.pat_type in
sprintf "%s" (string_of_pattern par p)
let string_of_let_pattern par fvs p =
let typ = p.pat_type in
let styp = string_of_type_sch fvs typ in
sprintf "%s : %s" (string_of_pattern par p) styp
(*
match p.pat_desc with
| Tpat_var id ->
......@@ -107,32 +130,26 @@ let rec string_of_expression par e =
string_of_expression (bool_of_option par) e in
let aux_pat ?par e =
string_of_pattern (bool_of_option par) e in
let string_of_branch b =
let p = b.c_lhs in
let e = b.c_rhs in
(* TODO: check b.c_guard is not used *)
let string_of_branch (p,e) =
Format.sprintf "@[@[%s@] ->@ @[%s@]@]" (aux_pat p) (aux e) in
(*let typ = e.exp_type in*)
match e.exp_desc with
| Texp_ident (p,loc,vd) -> string_of_path p (* string_of_typed_var (string_of_path p) vd.val_type*)
| Texp_constant c -> string_of_constant c
| Texp_let (rf, l, e) ->
let l = List.map (fun b -> (b.vb_pat, b.vb_expr)) l in
let show_pe (p,e) =
let sp = (string_of_let_pattern false p) in
let sp = (string_of_let_pattern false fvs p) in
let se = aux e in
Format.sprintf "%s =@ @[%s@]" sp se in
let sl = show_list show_pe " and " l in
let se = aux e in
Format.sprintf "@[let%s %s in@ @[%s@]@]" (string_of_recflag rf) sl se
| Texp_function (_,c1::[], pa) ->
let _p = c1.c_lhs in
let e = c1.c_rhs in
let p1 = c1.c_lhs in
let e1 = c1.c_rhs in
let rec explore pats e =
match e.exp_desc with
| Texp_function (_,c1::[], pa) ->
let p1 = c1.c_lhs in
let e1 = c1.c_rhs in
| Texp_function (_,(p1,e1)::[], pa) ->
explore (p1::pats) e1
| _ -> List.rev pats, e
in
......@@ -153,8 +170,7 @@ let rec string_of_expression par e =
let sl = show_list show_arg " " l in
let s = sprintf "%s %s" se sl in
show_par par s
| Texp_match (e, l, le, pa) ->
if le <> [] then unsupported "match with exception branches";
| Texp_match (e, l, pa) ->
let se = aux e in
let s = Format.sprintf "@[match@ @[%s@] with@ @[%s@]@]"
se (show_list string_of_branch " | " l) in
......@@ -163,7 +179,7 @@ let rec string_of_expression par e =
| Texp_tuple l ->
show_par true (show_list aux ", " l)
| Texp_construct (p, cd, es) ->
let c = string_of_lident_loc p in
let c = string_of_path p in
if es = []
then c
else if List.length es = 1
......@@ -174,14 +190,14 @@ let rec string_of_expression par e =
| Texp_record (l,Some eo) -> unsupported "record-with"
| Texp_record (l,None) ->
let print_item (p,li,ei) =
Format.sprintf "%s = %s" (string_of_lident_loc p) (aux ei) in
Format.sprintf "%s = %s" (string_of_path p) (aux ei) in
let s = Format.sprintf "@[{%s}@]" (show_list print_item "; " l) in
show_par par s
| Texp_field (e,p,i) ->
let s = Format.sprintf "@[%s.%s@]" (aux e) (string_of_lident_loc p) in
let s = Format.sprintf "@[%s.%s@]" (aux e) (string_of_path p) in
show_par par s
| Texp_setfield (e,p,i,e2) ->
let s = Format.sprintf "@[%s.%s <- %s@]" (aux e) (string_of_lident_loc p) (aux e2) in
let s = Format.sprintf "@[%s.%s <- %s@]" (aux e) (string_of_path p) (aux e2) in
show_par par s
| Texp_array l -> unsupported "array expression" (* Texp_array (List.map aux l)*)
| Texp_ifthenelse (e1, e2, None) ->
......@@ -190,30 +206,37 @@ let rec string_of_expression par e =
| Texp_ifthenelse (e1, e2, Some e3) ->
let s = Format.sprintf "@[if %s@ then %s@ else %s@]" (aux e1) (aux e2) (aux e3) in
show_par par s
| Texp_when (e1,e2) -> (*todo:better printing so that compiles *)
Format.sprintf "<< when %s >> %s" (aux e1) (aux e2)
| Texp_sequence (e1,e2) ->
let s = Format.sprintf "@[%s@ ; %s@]" (aux e1) (aux e2) in
show_par par s
| Texp_while (e1,e2) ->
let s = Format.sprintf "@[while %s@ do %s@ done@]" (aux e1) (aux e2) in
show_par par s
| Texp_for (i,pat,e1,e2,d,e3) ->
(* TODO: what is pat? *)
| Texp_for (i,e1,e2,d,e3) ->
let s = Format.sprintf "@[for %s = %s to %s do@ %s@ done@]" (Ident.name i) (aux e1) (aux e2) (aux e3) in
show_par par s
| Texp_send (_,_,_) -> unsupported "send expression"
| Texp_new _ -> unsupported "new expression"
| Texp_instvar (_,_,_) -> unsupported "inst-var expression"
| Texp_setinstvar (_,_,_,_) -> unsupported "set-inst-var expression"
| Texp_instvar (_,_) -> unsupported "inst-var expression"
| Texp_setinstvar (_,_,_) -> unsupported "set-inst-var expression"
| Texp_override _ -> unsupported "Pexp_override expression"
| Texp_letmodule (_,_,_,_) -> unsupported "let-module expression"
| Texp_letmodule (_,_,_) -> unsupported "let-module expression"
| Texp_assert e ->
let s = Format.sprintf "@[assert %s@]" (aux e) in
show_par par s
| Texp_assertfalse ->
show_par par "assert false"
| Texp_lazy e ->
let s = Format.sprintf "@[lazy %s@]" (aux e) in
show_par par s
| Texp_object _ -> unsupported "objects"
| Texp_poly (_,_) -> unsupported "poly"
| Texp_newtype (_,_) -> unsupported "newtype"
| Texp_pack _ -> unsupported "pack"
| Texp_open (_,_) -> unsupported "open"
| Texp_constraint (e,_,_) -> aux e
(*#########################################################################*)
......@@ -285,9 +308,9 @@ let is_simple_type_decl (name,decl) =
let rec string_of_module m =
match m.mod_desc with
| Tmod_ident (p, li) -> string_of_path p
| Tmod_ident p -> string_of_path p
| Tmod_structure s -> sprintf "struct\n%s\nend\n" (string_of_structure s)
| Tmod_functor (id,_,mt,me) -> sprintf "%s : _ ==>%s\n" (string_of_ident id) (string_of_module me)
| Tmod_functor (id,mt,me) -> sprintf "%s : _ ==>%s\n" (string_of_ident id) (string_of_module me)
| Tmod_apply (me1,me2,mc) -> sprintf "%s %s" (string_of_module me1) (string_of_module me2)
| Tmod_constraint (me,_,mt,mc) -> sprintf "(%s : _)" (string_of_module me)
| Tmod_unpack (_,_) -> unsupported "unpack"
......@@ -298,33 +321,23 @@ and string_of_structure (s:structure) =
and string_of_structure_item (si:structure_item) =
Printtyp.reset();
match si.str_desc with
| Tstr_eval (e,_) -> sprintf "let _ = %s" (string_of_expression false e)
| Tstr_value (r,l) ->
let show_pe b =
let p = b.vb_pat in
let e = b.vb_expr in
let sp = string_of_let_pattern false p in
| Tstr_eval e -> sprintf "let _ = %s" (string_of_expression false e)
| Tstr_value (r,fvs,l) ->
let show_pe (p,e) =
let sp = string_of_let_pattern false fvs p in
let se = string_of_expression false e in
Format.sprintf "%s =@ @[%s@]" sp se in
let sl = show_list show_pe " and " l in
Format.sprintf "@[let%s %s@]" (string_of_recflag r) sl
(* Format.sprintf "@[let%s %s =@ @[<2>%s@]@]" *)
| Tstr_primitive _ -> unsupported "primitive"
(* sprintf "val %s : _" (string_of_ident id) *)
| Tstr_primitive (id,v) -> sprintf "val %s : _" (string_of_ident id)
| Tstr_type l -> sprintf "type _ = _"
| Tstr_exception _ -> unsupported "exception"
(* sprintf "exception %s = _" (string_of_ident id) *)
| Tstr_module mb -> Format.sprintf "@[module %s =@ @[<2>%s] @]" (string_of_ident mb.mb_id) (string_of_module_binding mb)
| Tstr_exception (id,e) -> sprintf "exception %s = _" (string_of_ident id)
| Tstr_exn_rebind (id,p) -> unsupported "exception-rebind"
| Tstr_module (id,m) -> Format.sprintf "@[module %s =@ @[<2>%s] @]" (string_of_ident id) (string_of_module m)
| Tstr_recmodule _ -> unsupported "recursive modules"
| Tstr_modtype _ -> unsupported "module type declaration"
(* sprintf "module type %s = _" (string_of_ident id) *)
| Tstr_open p -> unsupported "open" (* sprintf "open %s = _" (string_of_path p) *)
| Tstr_modtype (id,mt) -> sprintf "module type %s = _" (string_of_ident id)
| Tstr_open p -> sprintf "open %s = _" (string_of_path p)
| Tstr_class _ -> unsupported "objects"
| Tstr_class_type _ -> unsupported "objects"
| Tstr_include _ -> unsupported "includ"
(* sprintf "include %s" (string_of_module m) *)
| Tstr_typext _ -> unsupported "extension"
| Tstr_attribute _ -> unsupported "attribute"
and string_of_module_binding mb =
string_of_module mb.mb_expr
\ No newline at end of file
| Tstr_include (m,ids) -> sprintf "include %s" (string_of_module m)
* build_error
** Coq
Definition build_error S vproto vmsg : result :=
let O := object_new vproto "Error" in
let '(l, S') := object_alloc S O in
ifb vmsg = undef then out_ter S' l
else result_not_yet_implemented.
** ML
let build_error S vproto vmsg =
let O = object_new vproto "Error" in
let (l, S') := object_alloc S O in
if value_compare vmsg undef then out_ter S' l
else result_not_yet_implemented
** JS
function build_error(S, vproto, vmsg) {
var O = object_new(vproto, "Error");
var l = object_alloc(S, O).first;
var S2 = object_alloc(S, O).second;
if (value_compare(vmsg, undef) {
return out_ter(S2, l);
} else {
return result_not_yet_implemented;
}
}
** JS, with log
function build_error(S, vproto, vmsg) {
log_custom({line: line, type: "enter"});
var res = build_error__body(S, vproto, vmsg);
var ctx = ctx_empty();
ctx = ctx_push(ctx, "res", res, "result");
log_custom({line: line, type: "exit", ctx: ctx});
return res;
}
function build_error__body(S, vproto, vmsg) {
var ctx = ctx_empty();
ctx = ctx_push(ctx, "S", S, "state");
ctx = ctx_push(ctx, "vproto", vproto, "value");
ctx = ctx_push(ctx, "vmsg", vmsg, "value");
log(1, ctx, "build_error");
var O = object_new(vproto, "Error");
ctx = ctx_push(ctx, "O", O, "object");
log(2, ctx, "var");
var l = object_alloc(S, O).first;
var S2 = object_alloc(S, O).second;
ctx = ctx_push(ctx, "l", l, "location");
ctx = ctx_push(ctx, "S2", S2, "state");
log(3, ctx, "var");
if (value_compare(vmsg, undef) {
log(4, ctx, "case");
return out_ter(S2, l);
} else {
log(5, ctx, "case");
return result_not_yet_implemented;
}
}
* run_error
** Coq
Definition run_error T S ne : specres T :=
if_object (build_error S (prealloc_native_error_proto ne) undef) (fun S' l =>
result_some (specret_out (out_ter S' (res_throw l)))).
** ML
let run_error (*T*) S ne =
if_object (build_error S (prealloc_native_error_proto ne) undef) (fun S' l ->
result_some (specret_out (out_ter S' (res_throw l))))
** JS
function run_error(S, ne) {
return if_object(build_error(S, prealloc_native_error_proto(ne), undef), function (S2, l) {
return result_some(specret_out(out_ter(S2, (res_throw(l)))))});
}
** JS, with log
function run_error(S, ne) {
log_custom({line: line, type: "enter"});
var res = run_error__body(S, ne);
var ctx = ctx_empty();
ctx = ctx_push(ctx, "res", res, "result");
log_custom({line: line, type: "exit", ctx: ctx});
return res;
}
function run_error__body(S, ne) {
var ctx = ctx_empty();
ctx = ctx_push(ctx, "S", S, "state");
ctx = ctx_push(ctx, "ne", ne, "error");
log(1, ctx, "run_error");
return if_object(build_error(S, prealloc_native_error_proto(ne), undef), function (S2, l) {
ctx = ctx_push(ctx, "S2", S2, "state");
ctx = ctx_push(ctx, "l", l, "location");
log(2, ctx, "fun");
return result_some(specret_out(out_ter(S2, (res_throw(l)))))});
}
* object_proto_is_prototype_of
** Coq
Definition object_proto_is_prototype_of runs S l0 l : result :=
if_some (run_object_method object_proto_ S l) (fun B =>
match B return result with
| null => out_ter S false
| value_object l' =>
ifb l' = l0
then out_ter S true
else runs_type_object_proto_is_prototype_of runs S l0 l'
| value_prim _ =>
impossible_with_heap_because S "[run_object_method] returned a primitive in [object_proto_is_prototype_of_body]."
end).
** ML
let object_proto_is_prototype_of S l0 l =
if_some (run_object_method object_proto_ S l) (fun B ->
match B with
| null -> out_ter S false
| value_object l' ->
if loc_compare l' l0
then out_ter S true
else runs_type_object_proto_is_prototype_of S l0 l'
| value_prim _ ->
impossible_with_heap_because S "[run_object_method] returned a primitive in [object_proto_is_prototype_of_body]."
end)
** JS
function object_proto_is_prototype_of(S, l0, l) {
return if_some (run_object_method(object_proto_, S, l), function (B) {
switch (B.tag) {
case "null": // "prim"?
return out_ter(S, false);
case "value_object":
var l2 = B.l;
if (loc_compare (l2, l0)) {
return out_ter(S, true);
} else {
return runs_type_object_proto_is_prototype_of(S, l0, l2);
}
case "value_prim":
return impossible_with_heap_because(S, "[run_object_method] returned a primitive in [object_proto_is_prototype_of_body].");
}
});
}
** JS, with log
function object_proto_is_prototype_of(S, l0, l) {
log_custom({line: line, type: "enter"});
var res = object_proto_is_prototype_of__body(S, l0, l);
var ctx = ctx_empty();
ctx = ctx_push(ctx, "res", res, "result");
log_custom({line: line, type: "exit", ctx: ctx});
return res;
}
function object_proto_is_prototype_of__body(S, l0, l) {
var ctx = ctx_empty();
ctx = ctx_push(ctx, "S", S, "state");
ctx = ctx_push(ctx, "l0", l0, "location");
ctx = ctx_push(ctx, "l", l, "location");
log(1, ctx, "object_proto_is_prototype_of");
return if_some (run_object_method(object_proto_, S, l), function (B) {
ctx = ctx_push(ctx, "B", B);
log(2, ctx, "fun");
switch (B.tag) {
case "null": // "prim"?
log(3, ctx, "case");
return out_ter(S, false);
case "value_object":
var l2 = B.l;
ctx = ctx_push(ctx, "l2", l2);
log(3, ctx, "case");
if (loc_compare (l2, l0)) {
log(4, ctx, "case");
return out_ter(S, true);
} else {
log(5, ctx, "case");
return runs_type_object_proto_is_prototype_of(S, l0, l2);
}
case "value_prim":
log(6, ctx, "case");
return impossible_with_heap_because(S, "[run_object_method] returned a primitive in [object_proto_is_prototype_of_body].");
}
});
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment