Adding what it should look like.

generator/print_tast.ml

@@ -22,39 +22,55 @@ let string_of_lident idt =
 
 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 
@@ -62,10 +78,18 @@ 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))
+         "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
@@ -75,13 +99,14 @@ let string_of_pattern par p =
             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,_) -> 
+     (*| 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
 

generator/transformations.org

+
+* 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].");
+    }
+  });
+}
+