diff --git a/generator/print_tast.ml b/generator/print_tast.ml
index 7051c1cf7d3edcb9cc9c3c4c8d0620e23fbf0685..496149d373e14259433d5658dfb4d661dc75f313 100644
--- a/generator/print_tast.ml
+++ b/generator/print_tast.ml
@@ -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)
diff --git a/generator/transformations.org b/generator/transformations.org
new file mode 100644
index 0000000000000000000000000000000000000000..c4ef84bab4624b2cfdecc899f0f0c995212c3604
--- /dev/null
+++ b/generator/transformations.org
@@ -0,0 +1,204 @@
+
+* 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].");
+ }
+ });
+}
+