Skip to content

Commit

Permalink
fmt
Browse files Browse the repository at this point in the history
  • Loading branch information
@cmester0
cmester0 committed Feb 21, 2024
1 parent c193395 commit b2e428b
Show file tree
Hide file tree
Showing 2 changed files with 92 additions and 54 deletions.
4 changes: 3 additions & 1 deletion engine/backends/coq/coq/coq_backend.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -339,7 +339,9 @@ struct
C.AST.App (C.AST.Var (pglobal_ident constructor), [ pexpr e ])
| Construct { constructor; fields; base } ->
(* __TODO_term__ span "constructor" *)
C.AST.Var (pglobal_ident constructor ^ C.ty_to_string_without_paren (pty span e.typ))
C.AST.Var
(pglobal_ident constructor
^ C.ty_to_string_without_paren (pty span e.typ))
| Closure { params; body } ->
C.AST.Lambda (List.map ~f:ppat params, pexpr body)
| MacroInvokation { macro; args; witness } ->
Expand Down
142 changes: 89 additions & 53 deletions engine/backends/coq/coq_ast.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -150,80 +150,100 @@ functor

let rec ty_to_string (x : AST.ty) : string * bool =
match x with
| AST.WildTy -> "_", false
| AST.Bool -> Lib.Notation.bool_str, false
| AST.Coproduct [] -> "⊥", false
| AST.WildTy -> ("_", false)
| AST.Bool -> (Lib.Notation.bool_str, false)
| AST.Coproduct [] -> ("⊥", false)
| AST.Coproduct l ->
let ty_str =
String.concat ~sep:(" " ^ "∐" ^ " ") (List.map ~f:ty_to_string_without_paren l)
String.concat
~sep:(" " ^ "∐" ^ " ")
(List.map ~f:ty_to_string_without_paren l)
in
ty_str, true
| AST.Product [] | AST.Unit -> Lib.Notation.unit_str, false (* TODO: might need paren *)
| AST.TypeTy -> Lib.Notation.type_str, false (* TODO: might need paren *)
| AST.Int { size = AST.USize; signed } -> "uint_size", false
| AST.Int { size; signed } -> "int" ^ int_size_to_string size, false
| AST.NameTy s -> s, false
| AST.RecordTy (name, fields) -> (* [ AST.Record (name, fields) ] *) name, false
(ty_str, true)
| AST.Product [] | AST.Unit ->
(Lib.Notation.unit_str, false (* TODO: might need paren *))
| AST.TypeTy -> (Lib.Notation.type_str, false (* TODO: might need paren *))
| AST.Int { size = AST.USize; signed } -> ("uint_size", false)
| AST.Int { size; signed } -> ("int" ^ int_size_to_string size, false)
| AST.NameTy s -> (s, false)
| AST.RecordTy (name, fields) ->
(* [ AST.Record (name, fields) ] *) (name, false)
| AST.Product l ->
let ty_str =
String.concat ~sep:(" " ^ "×" ^ " ") (List.map ~f:ty_to_string_without_paren l)
String.concat
~sep:(" " ^ "×" ^ " ")
(List.map ~f:ty_to_string_without_paren l)
in
ty_str, true
(ty_str, true)
| AST.Arrow (a, b) ->
let a_ty_str = ty_to_string_without_paren a in
let b_ty_str = ty_to_string_without_paren b in
a_ty_str ^ " " ^ "->" ^ " " ^ b_ty_str, true
(a_ty_str ^ " " ^ "->" ^ " " ^ b_ty_str, true)
| AST.ArrayTy (t, l) ->
let ty_str = ty_to_string_with_paren t in
"nseq" ^ " " ^ ty_str ^ " " ^ (* Int.to_string *) l, true
("nseq" ^ " " ^ ty_str ^ " " ^ (* Int.to_string *) l, true)
| AST.SliceTy t ->
let ty_str = ty_to_string_with_paren t in
"seq" ^ " " ^ ty_str, true
("seq" ^ " " ^ ty_str, true)
| AST.AppTy (i, []) -> ty_to_string i
(* | AST.AppTy (i, [ y ]) -> *)
(* let ty_defs, ty_str = ty_to_string y in *)
(* (ty_defs, i ^ " " ^ ty_str) *)
| AST.AppTy (i, p) ->
let ty_str = String.concat ~sep:" " (List.map ~f:ty_to_string_with_paren p) in
ty_to_string_without_paren i ^ " " ^ ty_str, true
let ty_str =
String.concat ~sep:" " (List.map ~f:ty_to_string_with_paren p)
in
(ty_to_string_without_paren i ^ " " ^ ty_str, true)
| AST.NatMod (t, i, s) ->
(* [ *)
(* AST.Notation *)
(* ( t, *)
(* AST.ArrayTy *)
(* (AST.Int { size = U8; signed = false }, Int.to_string i) ); *)
(* ] *)
"nat_mod 0x" ^ s, true
("nat_mod 0x" ^ s, true)
| AST.Forall ([], [], ty) -> ty_to_string ty
| AST.Forall (implicit_vars, [], ty) ->
"forall" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " " ^ ty_to_string_without_paren ty, true
( "forall" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " "
^ ty_to_string_without_paren ty,
true )
| AST.Forall ([], vars, ty) ->
"forall" ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " " ^ ty_to_string_without_paren ty, true
( "forall" ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " "
^ ty_to_string_without_paren ty,
true )
| AST.Forall (implicit_vars, vars, ty) ->
"forall" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " " ^ ty_to_string_without_paren ty, true
( "forall" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " "
^ ty_to_string_without_paren ty,
true )
| AST.Exists ([], [], ty) -> ty_to_string ty
| AST.Exists (implicit_vars, [], ty) ->
"exists" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " " ^ ty_to_string_without_paren ty, true
( "exists" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " "
^ ty_to_string_without_paren ty,
true )
| AST.Exists ([], vars, ty) ->
"exists" ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " " ^ ty_to_string_without_paren ty, true
( "exists" ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " "
^ ty_to_string_without_paren ty,
true )
| AST.Exists (implicit_vars, vars, ty) ->
"exists" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " " ^ ty_to_string_without_paren ty, true
( "exists" ^ " " ^ "{"
^ String.concat ~sep:" " implicit_vars
^ "}" ^ "," ^ " "
^ String.concat ~sep:" " vars
^ "," ^ " "
^ ty_to_string_without_paren ty,
true )
| _ -> .

and ty_to_string_with_paren (x : AST.ty) : string =
Expand Down Expand Up @@ -272,7 +292,8 @@ functor
(List.map ~f:(fun t -> pat_to_string t false (depth + 1)) vals)
^ ")"
| AST.AscriptionPat (p, ty) ->
"(" ^ pat_to_string p true depth ^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty
"(" ^ pat_to_string p true depth ^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty
^ ")" (* TODO: Should this be true of false? *)
| AST.DisjunctivePat pats ->
let f pat = pat_to_string pat true depth in
Expand Down Expand Up @@ -330,7 +351,8 @@ functor
~f:(function
| AST.Newline n -> newline_indent (depth + n)
| AST.Typing (typ, true, n) -> ty_to_string_with_paren typ
| AST.Typing (typ, false, n) -> ty_to_string_without_paren typ
| AST.Typing (typ, false, n) ->
ty_to_string_without_paren typ
| AST.Value (x, true, n) ->
term_to_string_with_paren x (depth + n)
| AST.Value (x, false, n) ->
Expand Down Expand Up @@ -500,7 +522,8 @@ functor
^ " " ^ ";")
trait_items
in
"Class" ^ " " ^ name ^ " " ^ "(Self : " ^ ty_to_string_with_paren AST.TypeTy
"Class" ^ " " ^ name ^ " " ^ "(Self : "
^ ty_to_string_with_paren AST.TypeTy
^ ")"
^ params_to_string_typed arguments
^ " " ^ ":=" ^ " " ^ "{" ^ field_str ^ newline_indent 0 ^ "}" ^ "."
Expand All @@ -515,7 +538,8 @@ functor
decl_to_string (AST.Parameter (field_name, field_ty))
| Coercion (field_name, field_ty) ->
decl_to_string
(AST.Module (field_name, ty_to_string_with_paren field_ty, [], []))
(AST.Module
(field_name, ty_to_string_with_paren field_ty, [], []))
(* Should be "::" in newer versions of coq *))
trait_items
in
Expand All @@ -535,7 +559,8 @@ functor
decl_to_string (AST.Parameter (field_name, field_ty))
| Coercion (field_name, field_ty) ->
decl_to_string
(AST.Module (field_name, ty_to_string_with_paren field_ty, [], []))
(AST.Module
(field_name, ty_to_string_with_paren field_ty, [], []))
(* Should be "::" in newer versions of coq *))
trait_items
in
Expand Down Expand Up @@ -579,7 +604,9 @@ functor
^ params_to_string_typed arguments
^ " " ^ "=>" ^ " ")
^ term_to_string_without_paren term 1
^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty ^ " " ^ "in")
^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty
^ " " ^ "in")
| _ -> None)
impl_list
in
Expand All @@ -600,7 +627,9 @@ functor
^ params_to_string_typed arguments
^ " " ^ "=>" ^ " ")
^ term_to_string_without_paren term 1
^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty ^ ")")
^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty
^ ")")
impl_list)
in
let ty_str = ty_to_string_without_paren self_ty in
Expand Down Expand Up @@ -689,13 +718,18 @@ functor
match param with
| Implicit (pat, ty) ->
"{" ^ pat_to_string pat true 0 ^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty ^ "}"
^ ty_to_string_without_paren ty
^ "}"
| Explicit (pat, ty) ->
"(" ^ pat_to_string pat true 0 ^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty ^ ")"
| Typeclass (None, ty) -> "`{" ^ " " ^ ty_to_string_without_paren ty ^ "}"
^ ty_to_string_without_paren ty
^ ")"
| Typeclass (None, ty) ->
"`{" ^ " " ^ ty_to_string_without_paren ty ^ "}"
| Typeclass (Some name, ty) ->
"`{" ^ name ^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty ^ "}")
"`{" ^ name ^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty
^ "}")
params)

and params_to_string params : string =
Expand Down Expand Up @@ -743,6 +777,8 @@ functor
| Coercion (ty_name, ty) -> (ty_name, ":>", ty)
(* Should be "::" in newer versions of coq *)
in
pre ^ ty_name ^ " " ^ ":" ^ " " ^ ty_to_string_without_paren ty ^ post)
pre ^ ty_name ^ " " ^ ":" ^ " "
^ ty_to_string_without_paren ty
^ post)
variants)
end

0 comments on commit b2e428b

Please sign in to comment.