Skip to content

Commit

Permalink
Remove structured_string
Browse files Browse the repository at this point in the history
  • Loading branch information
@f52985
f52985 committed Jan 23, 2024
1 parent 3dc053d commit 55692ca
Show file tree
Hide file tree
Showing 4 changed files with 8 additions and 368 deletions.
347 changes: 0 additions & 347 deletions spectec/src/il/print.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -282,350 +282,3 @@ let rec string_of_def d =

let string_of_script ds =
concat "" (List.map string_of_def ds)


let sprintf = Printf.sprintf

let structured_string_of_list stringifier = function
| [] -> "[]"
| h :: t ->
"[" ^
List.fold_left
(fun acc elem -> acc ^ ", " ^ stringifier elem)
(stringifier h) t ^ "]"


(* Structured string *)

let structured_string_of_hint hint =
let identity x = x in
sprintf "{hintid : \"%s\"; hintexp : %s}"
(hint.hintid.it)
(structured_string_of_list identity hint.hintexp)

let structured_string_of_hints hints =
structured_string_of_list structured_string_of_hint hints

let structured_string_of_hintdef hintdef =
match hintdef.it with
| SynH (id, hints) -> sprintf "SynH (%s, %s)" id.it (structured_string_of_list structured_string_of_hint hints)
| RelH (id, hints) -> sprintf "RelH (%s, %s)" id.it (structured_string_of_list structured_string_of_hint hints)
| DecH (id, hints) -> sprintf "DecH (%s, %s)" id.it (structured_string_of_list structured_string_of_hint hints)

let structured_string_of_atom = function
| Atom atomid -> sprintf "Atom \"%s\"" atomid
| Infinity -> "Infinity"
| Bot -> "Bot"
| Top -> "Top"
| Dot -> "Dot"
| Dot2 -> "Dot2"
| Dot3 -> "Dot3"
| Semicolon -> "Semicolon"
| Backslash -> "Backslash"
| In -> "In"
| Arrow -> "Arrow"
| Arrow2 -> "Arrow2"
| Colon -> "Colon"
| Sub -> "Sub"
| Sup -> "Sup"
| Assign -> "Assign"
| Equiv -> "Equiv"
| Approx -> "Approx"
| SqArrow -> "SqArrow"
| SqArrowStar ->"SqArrowStar"
| Prec -> "Prec"
| Succ -> "Succ"
| Tilesturn -> "Tilesturn"
| Turnstile -> "Turnstile"
| Quest -> "Quest"
| Plus -> "Plus"
| Star -> "Star"
| Comma -> "Comma"
| Bar -> "Bar"
| LParen -> "LParen"
| LBrack -> "LBrack"
| LBrace -> "LBrace"
| RParen -> "RParen"
| RBrack -> "RBrack"
| RBrace -> "RBrace"

let structured_string_of_unop = function
| NotOp -> "NotOp"
| PlusOp _ -> "PlusOp"
| MinusOp _ -> "MinusOp"

let structured_string_of_binop = function
| AndOp -> "AndOp"
| OrOp -> "OrOp"
| ImplOp -> "ImplOp"
| EquivOp -> "EquivOp"
| AddOp _ -> "AddOp"
| SubOp _ -> "SubOp"
| MulOp _ -> "MulOp"
| DivOp _ -> "DivOp"
| ExpOp _ -> "ExpOp"

let structured_string_of_cmpop = function
| EqOp -> "EqOp"
| NeOp -> "NeOp"
| LtOp _ -> "LtOp"
| GtOp _ -> "GtOp"
| LeOp _ -> "LeOp"
| GeOp _ -> "GeOp"

let structured_string_of_mixop mixop =
structured_string_of_list
(structured_string_of_list structured_string_of_atom)
mixop


(* Types *)

let rec structured_string_of_iter iter =
match iter with
| Opt -> "Opt"
| List -> "List"
| List1 -> "List1"
| ListN (exp, None) -> sprintf "ListN (%s)" (structured_string_of_exp exp)
| ListN (exp, Some id) ->
sprintf "ListN (%s, %s)" (structured_string_of_exp exp) id.it

and structured_string_of_typ typ =
match typ.it with
| VarT id -> sprintf "VarT \"%s\"" id.it
| BoolT -> "BoolT"
| NumT _ -> "NumT"
| TextT -> "TextT"
| TupT typs -> sprintf "TupT (%s)" (structured_string_of_typs typs)
| IterT (typ1, iter) ->
sprintf "IterT (%s, %s)"
(structured_string_of_typ typ1)
(structured_string_of_iter iter)

and structured_string_of_typs _typs =
(* structured_string_of_list structured_string_of_typ typs *)
"TODO: structured_string_of_typs"

and structured_string_of_deftyp deftyp =
match deftyp.it with
| AliasT typ -> sprintf "AliasT (%s)" (structured_string_of_typ typ)
| NotationT (mixop, typ) ->
sprintf "NotationT (%s, %s)"
(structured_string_of_mixop mixop)
(structured_string_of_typ typ)
| StructT typfields ->
sprintf "StructT (%s)" (structured_string_of_typfields typfields)
| VariantT (typcases) ->
sprintf "VariantT (%s)"
(structured_string_of_list structured_string_of_typcase typcases)

and _structured_string_of_typfield (atom, typ, hints) =
sprintf "(%s, %s, %s)"
(structured_string_of_atom atom)
(structured_string_of_typ typ)
(structured_string_of_hints hints)

and structured_string_of_typfields _typfields =
(* structured_string_of_list structured_string_of_typfield typfields *)
"TODO: structured_string_of_typs"

and structured_string_of_typcase (atom, _typ, hints) =
sprintf "(%s, %s, %s)"
(structured_string_of_atom atom)
(* (structured_string_of_typ typ) *)
"TODO: structured_string_of_typcases"
(structured_string_of_hints hints)


(* Expressions *)

and structured_string_of_exp exp =
match exp.it with
| VarE id -> sprintf "VarE \"%s\"" id.it
| BoolE b -> sprintf "BoolE %s" (string_of_bool b)
| NatE n -> sprintf "NatE %s" (string_of_int n)
| TextE t -> sprintf "TextE \"%s\"" (String.escaped t)
| UnE (unop, exp2) ->
sprintf "UnE (%s, %s)"
(structured_string_of_unop unop)
(structured_string_of_exp exp2)
| BinE (binop, exp1, exp2) ->
sprintf "BinE (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_binop binop)
(structured_string_of_exp exp2)
| CmpE (cmpop, exp1, exp2) ->
sprintf "CmpE (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_cmpop cmpop)
(structured_string_of_exp exp2)
| IdxE (exp1, exp2) ->
sprintf "IdxE (%s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
| SliceE (exp1, exp2, exp3) ->
sprintf "SliceE (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
(structured_string_of_exp exp3)
| UpdE (exp1, path, exp2) ->
sprintf "UpdE (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_path path)
(structured_string_of_exp exp2)
| ExtE (exp1, path, exp2) ->
sprintf "ExtE (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_path path)
(structured_string_of_exp exp2)
| StrE expfields ->
sprintf "StrE (%s)"
(structured_string_of_list structured_string_of_expfield expfields)
| DotE (exp1, atom) ->
sprintf "DotE (%s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_atom atom)
| CompE (exp1, exp2) ->
sprintf "CompE (%s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
| LenE exp1 -> sprintf "LenE (%s)" (structured_string_of_exp exp1)
| TupE exps -> sprintf "TupE (%s)" (structured_string_of_exps exps)
| MixE (mixop, exp1) ->
sprintf "MixE (%s, %s)"
(structured_string_of_mixop mixop)
(structured_string_of_exp exp1)
| CallE (id, exp) ->
sprintf "CallE (\"%s\", %s)"
id.it
(structured_string_of_exp exp)
| IterE (exp1, iterexp) ->
sprintf "IterE (%s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_iterexp iterexp)
| OptE None -> "OptE ()"
| OptE Some exp -> sprintf "OptE (%s)" (structured_string_of_exp exp)
| TheE exp -> sprintf "TheE (%s)" (structured_string_of_exp exp)
| ListE exps -> sprintf "ListE (%s)" (structured_string_of_exps exps)
| CatE (exp1, exp2) ->
sprintf "CatE (%s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
| CaseE (atom, exp1) ->
sprintf "CaseE (%s, %s)"
(structured_string_of_atom atom)
(structured_string_of_exp exp1)
| SubE (exp1, typ1, typ2) ->
sprintf "SubE (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_typ typ1)
(structured_string_of_typ typ2)

and structured_string_of_exps exps =
structured_string_of_list structured_string_of_exp exps

and structured_string_of_iterexp (iter, ids) =
sprintf "(%s, %s)"
(structured_string_of_iter iter)
(structured_string_of_list (fun id -> sprintf "\"%s\"" id.it) ids)


and structured_string_of_expfield (atom, exp) =
sprintf "(%s, %s)" (structured_string_of_atom atom) (structured_string_of_exp exp)

and structured_string_of_path path =
match path.it with
| RootP -> "RootP"
| IdxP (path1, exp) ->
sprintf "IdxP (%s, %s)"
(structured_string_of_path path1)
(structured_string_of_exp exp)
| SliceP (path1, exp1, exp2) ->
sprintf "SliceP (%s, %s, %s)"
(structured_string_of_path path1)
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
| DotP (path1, atom) ->
sprintf "DotP (%s, %s)"
(structured_string_of_path path1)
(structured_string_of_atom atom)


(* Definitions *)

let structured_string_of_bind (id, typ, iters) =
sprintf "(\"%s\", %s, %s)"
id.it
(structured_string_of_typ typ)
(structured_string_of_list structured_string_of_iter iters)

let structured_string_of_binds binds =
structured_string_of_list structured_string_of_bind binds


let rec structured_string_of_premise prem =
match prem.it with
| RulePr (id, mixop, exp) ->
sprintf "RulePr (\"%s\", %s, %s)"
id.it
(structured_string_of_mixop mixop)
(structured_string_of_exp exp)
| IfPr (exp) -> sprintf "IfPr (%s)" (structured_string_of_exp exp)
| LetPr (exp1, exp2, ids) ->
sprintf "LetPr (%s, %s, %s)"
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
(structured_string_of_list Source.it ids)
| ElsePr -> "ElsePr"
| IterPr (prem, iterexp) ->
sprintf "IterPr (%s, %s)"
(structured_string_of_premise prem)
(structured_string_of_iterexp iterexp)

let structured_string_of_rule rule =
match rule.it with
| RuleD (id, binds, mixop, exp, prems) ->
sprintf "RuleD (\"%s\", %s, %s, %s, %s)"
id.it
(structured_string_of_binds binds)
(structured_string_of_mixop mixop)
(structured_string_of_exp exp)
(structured_string_of_list structured_string_of_premise prems)

let structured_string_of_clause clause =
match clause.it with
| DefD (binds, exp1, exp2, prems) ->
sprintf "DefD (%s, %s, %s, %s)"
(structured_string_of_binds binds)
(structured_string_of_exp exp1)
(structured_string_of_exp exp2)
(structured_string_of_list structured_string_of_premise prems)

let rec structured_string_of_def def =
match def.it with
| SynD (id, deftyp) ->
sprintf "SynD (\n \"%s\",\n %s\n)\n"
id.it
(structured_string_of_deftyp deftyp)
| RelD (id, mixop, typ, rules) ->
sprintf "RelD (\n \"%s\",\n %s,\n %s,\n %s\n)\n"
id.it
(structured_string_of_mixop mixop)
(structured_string_of_typ typ)
(structured_string_of_list structured_string_of_rule rules)
| DecD (id, typ1, typ2, clauses) ->
sprintf "DecD (\n \"%s\",\n %s,\n %s,\n %s\n)\n"
id.it
(structured_string_of_typ typ1)
(structured_string_of_typ typ2)
(structured_string_of_list structured_string_of_clause clauses)
| RecD defs ->
sprintf "RecD (%s)\n" (structured_string_of_list structured_string_of_def defs)
| HintD hintdef ->
sprintf "HintD (%s)\n" (structured_string_of_hintdef hintdef)


(* Scripts *)

let structured_string_of_script defs =
concat "" (List.map structured_string_of_def defs)
15 changes: 0 additions & 15 deletions spectec/src/il/print.mli
View file
Original file line number Diff line number Diff line change
Expand Up @@ -13,18 +13,3 @@ val string_of_prem : premise -> string
val string_of_def : def -> string
val string_of_deftyp : deftyp -> string
val string_of_script : script -> string

val structured_string_of_atom : atom -> string
val structured_string_of_unop : unop -> string
val structured_string_of_binop : binop -> string
val structured_string_of_cmpop : cmpop -> string
val structured_string_of_mixop : mixop -> string
val structured_string_of_iter : iter -> string
val structured_string_of_typ : typ -> string
val structured_string_of_exp : exp -> string
val structured_string_of_path : path -> string
val structured_string_of_binds : binds -> string
val structured_string_of_premise : premise -> string
val structured_string_of_def : def -> string
val structured_string_of_deftyp : deftyp -> string
val structured_string_of_script : script -> string
6 changes: 4 additions & 2 deletions spectec/src/il2al/translate.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -206,6 +206,8 @@ and exp2expr exp =
| [ []; [ Ast.Star; atom ]; [ Ast.Star ] ], [ e1; e2 ]
| [ []; [ atom ]; [] ], [ e1; e2 ] ->
infixE (exp2expr e1, Print.string_of_atom atom, exp2expr e2) ~at:at
| [ []; [ Ast.Arrow ]; [ Ast.Star ]; [] ], [ e1; e2; e3 ] -> (* HARDCODE *)
infixE (exp2expr e1, "->", catE (exp2expr e2, exp2expr e3)) ~at:at
(* Constructor *)
(* TODO: Need a better way to convert these CaseE into ConsturctE *)
| [ [ Ast.Atom "FUNC" ]; []; [ Ast.Star ]; [] ], _ ->
Expand Down Expand Up @@ -243,10 +245,10 @@ and exp2expr exp =
| [ Ast.Atom name ] :: ll, el
when List.for_all (fun l -> l = [] || l = [ Ast.Star ] || l = [ Ast.Quest ]) ll ->
caseE ((name, String.lowercase_ascii name), List.map exp2expr el) ~at:at
| _ -> yetE (Print.structured_string_of_exp exp) ~at:at)
| _ -> yetE (Print.string_of_exp exp) ~at:at)
| Ast.OptE inner_exp -> optE (Option.map exp2expr inner_exp) ~at:at
(* Yet *)
| _ -> yetE (Print.structured_string_of_exp exp) ~at:at
| _ -> yetE (Print.string_of_exp exp) ~at:at

(* `Ast.exp` -> `expr list` *)
and exp2args exp =
Expand Down
Loading

0 comments on commit 55692ca

Please sign in to comment.