Small cleanup

Remove unneeded types, e.g. provisions for scalc
This commit is contained in:
Louis Gesbert 2022-08-26 11:06:00 +02:00 committed by Denis Merigoux
parent 7e0d24efd2
commit 5bda9e98d0
No known key found for this signature in database
GPG Key ID: EE99DCFA365C3EE3
3 changed files with 14 additions and 27 deletions

View File

@ -107,7 +107,7 @@ let rec format_typ
| TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1 | TArray t1 -> Format.fprintf fmt "@[%a@ array@]" format_typ t1
| TAny d -> Format.fprintf fmt "any[%d]" (Any.hash d) | TAny d -> Format.fprintf fmt "any[%d]" (Any.hash d)
exception Type_error of A.any_marked_expr * unionfind_typ * unionfind_typ exception Type_error of A.any_expr * unionfind_typ * unionfind_typ
type mark = { pos : Pos.t; uf : unionfind_typ } type mark = { pos : Pos.t; uf : unionfind_typ }

View File

@ -148,8 +148,6 @@ type scopelang = [ `Scopelang ]
type dcalc = [ `Dcalc ] type dcalc = [ `Dcalc ]
type lcalc = [ `Lcalc ] type lcalc = [ `Lcalc ]
(* type scalc = [ `Scalc ] *)
type 'a any = [< desugared | scopelang | dcalc | lcalc ] as 'a type 'a any = [< desugared | scopelang | dcalc | lcalc ] as 'a
(** Literals are the same throughout compilation except for the [LEmptyError] (** Literals are the same throughout compilation except for the [LEmptyError]
@ -194,16 +192,15 @@ and ('a, 't) naked_gexpr =
| EApp : ('a, 't) gexpr * ('a, 't) gexpr list -> ('a any, 't) naked_gexpr | EApp : ('a, 't) gexpr * ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
| EOp : operator -> ('a any, 't) naked_gexpr | EOp : operator -> ('a any, 't) naked_gexpr
| EArray : ('a, 't) gexpr list -> ('a any, 't) naked_gexpr | EArray : ('a, 't) gexpr list -> ('a any, 't) naked_gexpr
(* All but statement calculus *)
| EVar : | EVar :
('a, 't) naked_gexpr Bindlib.var ('a, 't) naked_gexpr Bindlib.var
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr -> ('a any, 't) naked_gexpr
| EAbs : | EAbs :
(('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder * typ list (('a, 't) naked_gexpr, ('a, 't) gexpr) Bindlib.mbinder * typ list
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr -> ('a any, 't) naked_gexpr
| EIfThenElse : | EIfThenElse :
('a, 't) gexpr * ('a, 't) gexpr * ('a, 't) gexpr ('a, 't) gexpr * ('a, 't) gexpr * ('a, 't) gexpr
-> (([< desugared | scopelang | dcalc | lcalc ] as 'a), 't) naked_gexpr -> ('a any, 't) naked_gexpr
(* Early stages *) (* Early stages *)
| ELocation : | ELocation :
'a glocation 'a glocation
@ -254,16 +251,6 @@ type ('e, 'b) binder = (('a, 't) naked_gexpr, 'b) Bindlib.binder
(** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib} (** The expressions use the {{:https://lepigre.fr/ocaml-bindlib/} Bindlib}
library, based on higher-order abstract syntax *) library, based on higher-order abstract syntax *)
(* (\* Statement calculus *\)
* | ESVar: LocalName.t -> (scalc as 'a, 't) naked_gexpr
* | ESStruct: ('a, 't) gexpr list * StructName.t -> (scalc as 'a, 't) naked_gexpr
* | ESStructFieldAccess: ('a, 't) gexpr * StructFieldName.t * StructName.t -> (scalc as 'a, 't) naked_gexpr
* | ESInj: ('a, 't) gexpr * EnumConstructor.t * EnumName.t -> (scalc as 'a, 't) naked_gexpr
* | ESFunc: TopLevelName.t -> (scalc as 'a, 't) naked_gexpr *)
type 'e anyexpr = 'e constraint 'e = (_ any, _) gexpr
(** Shorter alias for functions taking any kind of expression *)
(** {2 Markings} *) (** {2 Markings} *)
type untyped = { pos : Pos.t } [@@ocaml.unboxed] type untyped = { pos : Pos.t } [@@ocaml.unboxed]
@ -277,7 +264,7 @@ type typed = { pos : Pos.t; ty : typ }
type _ mark = Untyped : untyped -> untyped mark | Typed : typed -> typed mark type _ mark = Untyped : untyped -> untyped mark | Typed : typed -> typed mark
(** Useful for errors and printing, for example *) (** Useful for errors and printing, for example *)
type any_marked_expr = AnyExpr : (_ any, _ mark) gexpr -> any_marked_expr type any_expr = AnyExpr : (_ any, _ mark) gexpr -> any_expr
(** {2 Higher-level program structure} *) (** {2 Higher-level program structure} *)
@ -308,7 +295,7 @@ type 'e scope_let = {
scope_let_next : ('e, 'e scope_body_expr) binder; scope_let_next : ('e, 'e scope_body_expr) binder;
scope_let_pos : Pos.t; scope_let_pos : Pos.t;
} }
constraint 'e = ('a, 'm mark) gexpr constraint 'e = (_ any, _ mark) gexpr
(** This type is parametrized by the expression type so it can be reused in (** This type is parametrized by the expression type so it can be reused in
later intermediate representations. *) later intermediate representations. *)
@ -318,14 +305,14 @@ type 'e scope_let = {
and 'e scope_body_expr = and 'e scope_body_expr =
| Result of 'e | Result of 'e
| ScopeLet of 'e scope_let | ScopeLet of 'e scope_let
constraint 'e = (_, _ mark) gexpr constraint 'e = (_ any, _ mark) gexpr
type 'e scope_body = { type 'e scope_body = {
scope_body_input_struct : StructName.t; scope_body_input_struct : StructName.t;
scope_body_output_struct : StructName.t; scope_body_output_struct : StructName.t;
scope_body_expr : ('e, 'e scope_body_expr) binder; scope_body_expr : ('e, 'e scope_body_expr) binder;
} }
constraint 'e = (_, _ mark) gexpr constraint 'e = (_ any, _ mark) gexpr
(** Instead of being a single expression, we give a little more ad-hoc structure (** Instead of being a single expression, we give a little more ad-hoc structure
to the scope body by decomposing it in an ordered list of let-bindings, and to the scope body by decomposing it in an ordered list of let-bindings, and
a result expression that uses the let-binded variables. The first binder is a result expression that uses the let-binded variables. The first binder is
@ -336,14 +323,14 @@ type 'e scope_def = {
scope_body : 'e scope_body; scope_body : 'e scope_body;
scope_next : ('e, 'e scopes) binder; scope_next : ('e, 'e scopes) binder;
} }
constraint 'e = (_, _ mark) gexpr constraint 'e = (_ any, _ mark) gexpr
(** Finally, we do the same transformation for the whole program for the kinded (** Finally, we do the same transformation for the whole program for the kinded
lets. This permit us to use bindlib variables for scopes names. *) lets. This permit us to use bindlib variables for scopes names. *)
and 'e scopes = and 'e scopes =
| Nil | Nil
| ScopeDef of 'e scope_def | ScopeDef of 'e scope_def
constraint 'e = (_, _ mark) gexpr constraint 'e = (_ any, _ mark) gexpr
type struct_ctx = (StructFieldName.t * typ) list StructMap.t type struct_ctx = (StructFieldName.t * typ) list StructMap.t
type enum_ctx = (EnumConstructor.t * typ) list EnumMap.t type enum_ctx = (EnumConstructor.t * typ) list EnumMap.t

View File

@ -85,7 +85,7 @@ val format :
?debug:bool (** [true] for debug printing *) -> ?debug:bool (** [true] for debug printing *) ->
decl_ctx -> decl_ctx ->
Format.formatter -> Format.formatter ->
ScopeName.t * 'e anyexpr scope_body -> ScopeName.t * 'e scope_body ->
unit unit
val to_expr : val to_expr :
@ -112,6 +112,6 @@ val build_typ_from_sig :
(** {2 Analysis and tests} *) (** {2 Analysis and tests} *)
val free_vars_body_expr : 'e anyexpr scope_body_expr -> 'e Var.Set.t val free_vars_body_expr : 'e scope_body_expr -> 'e Var.Set.t
val free_vars_body : 'e anyexpr scope_body -> 'e Var.Set.t val free_vars_body : 'e scope_body -> 'e Var.Set.t
val free_vars : 'e anyexpr scopes -> 'e Var.Set.t val free_vars : 'e scopes -> 'e Var.Set.t