Module Qcert.Compiler.Component.UriComponent

Require Import String.
Require Import List.
Require Import ZArith.
Require Import EquivDec.
Require Import Equivalence.

Require Import Utils.
Require Import ForeignData.
Require Import ForeignOperators.
Require Import ForeignToJava.
Require Import JavaSystem.

Import ListNotations.
Local Open Scope string_scope.



Axiom URI_encode : string -> string.
Extract Inlined Constant URI_encode => "(fun x -> Uri_component.encode x)".
Axiom URI_decode : string -> string.
Extract Inlined Constant URI_decode => "(fun x -> Uri_component.decode x)".

Section UriOperators.
  Inductive uri_unary_op :=
  | uop_uri_encode : uri_unary_op
  | uop_uri_decode : uri_unary_op
  .

  Section toString.
    Definition uri_unary_op_tostring (f:uri_unary_op) : string :=
      match f with
      | uop_uri_encode => "uriEncode"
      | uop_uri_decode => "uriDecode"
      end.

  End toString.

  Section toJava.
    Definition cname : string := "UriComponent".

    Definition uri_to_java_unary_op
               (indent:nat) (eol:string)
               (quotel:string) (fu:uri_unary_op)
               (d:java_json) : java_json
      := match fu with
         | uop_uri_encode => mk_java_unary_op0_foreign cname "uriEncode" d
         | uop_uri_decode => mk_java_unary_op0_foreign cname "uriDecode" d
         end.

  End toJava.

  Section toEJson.
    Inductive ejson_uri_runtime_op :=
    | EJsonRuntimeUriEncode
    | EJsonRuntimeUriDecode
    .

    Definition ejson_uri_runtime_op_tostring op : string :=
      match op with
      | EJsonRuntimeUriEncode => "uriEncode"
      | EJsonRuntimeUriDecode => "uriDecode"
      end.

    Definition ejson_uri_runtime_op_fromstring opname : option ejson_uri_runtime_op :=
      match opname with
      | "uriEncode" => Some EJsonRuntimeUriEncode
      | "uriDecode" => Some EJsonRuntimeUriDecode
      | _ => None
      end.

  End toEJson.
End UriOperators.