Skip to content

Commit

Permalink
refactor untyped_let_binding
Browse files Browse the repository at this point in the history
  • Loading branch information
@gfngfn
gfngfn committed Sep 15, 2024
1 parent de10f1a commit 0b82aed
Show file tree
Hide file tree
Showing 4 changed files with 146 additions and 51 deletions.
24 changes: 22 additions & 2 deletions src/frontend/moduleTypechecker.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -737,7 +737,17 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind :
in
if valattr.ValueAttribute.is_test then
match (stage, valbind) with
| (Stage1, UTNonRec(ident, mnquant, _retty, utast1)) -> (* TODO: `retty` *)
| (Stage1, UTNonRec(utletbind)) ->
let
UTLetBinding{
identifier = ident;
quantifier = mnquant;
parameters = param_units;
return_type = mntyopt_ret;
body = utast_body;
} = utletbind
in
let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *)
let* () = check_empty_manual_quantifier rng mnquant in
let (_, test_name) = ident in
let ty_expected =
Expand All @@ -753,7 +763,17 @@ and typecheck_binding (config : typecheck_config) (tyenv : Typeenv.t) (utbind :
else
let* (rec_or_nonrecs, ssig) =
match valbind with
| UTNonRec(ident, ManualQuantifier(typarams, rowparams), _retty, utast1) -> (* TODO: use `retty` *)
| UTNonRec(utletbind) ->
let
UTLetBinding{
identifier = ident;
quantifier = ManualQuantifier(typarams, rowparams);
parameters = param_units;
return_type = _mntyopt_ret;
body = utast_body;
} = utletbind
in
let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *)
let* (typarammap, _) = TypeParameterMap.empty |> add_type_parameters (Level.succ Level.bottom) typarams in
let* (rowparammap, _) = pre.row_parameters |> add_row_parameters (Level.succ Level.bottom) rowparams in
let pre =
Expand Down
125 changes: 84 additions & 41 deletions src/frontend/parser.mly
View file
Original file line number Diff line number Diff line change
Expand Up @@ -31,13 +31,6 @@
) utasts (Range.dummy "expr-list-nil", UTEndOfList)


let curry_lambda_abstraction (param_units : untyped_parameter_unit list) (utast : untyped_abstract_tree) : untyped_abstract_tree =
let rng = Range.dummy "curry_lambda_abstraction" in
utast |> List.fold_right (fun param_unit utast ->
(rng, UTFunction(param_unit, utast))
) param_units


(* TODO (enhance): more efficient implementation *)
let rec omit_pre_spaces str =
let len = String.length str in
Expand Down Expand Up @@ -483,11 +476,16 @@ bind_value_rec:
{ valbinds }
;
bind_value_nonrec:
| ident=bound_identifier; quant_and_param_units=quant_and_param_units; retty=return_type; EXACT_EQ; utast=expr
| ident=bound_identifier; quant_and_param_units=quant_and_param_units; mntyopt_ret=return_type; EXACT_EQ; utast=expr
{
let (mnquant, param_units) = quant_and_param_units in
let curried = curry_lambda_abstraction param_units utast in
(ident, mnquant, retty, curried)
UTLetBinding{
identifier = ident;
quantifier = mnquant;
parameters = param_units;
return_type = mntyopt_ret;
body = utast;
}
}
;
return_type:
Expand All @@ -498,12 +496,21 @@ bind_inline:
| ident_ctx=LOWER; cs=BACKSLASH_CMD; quant_and_param_units=quant_and_param_units; EXACT_EQ; utast=expr
{
let (mnquant, param_units) = quant_and_param_units in
(cs, mnquant, None,
make_standard (Ranged ident_ctx) (Ranged utast) (UTLambdaInlineCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast;
}))
let utast_cmd_abs =
make_standard (Ranged ident_ctx) (Ranged utast)
(UTLambdaInlineCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast;
})
in
UTLetBinding{
identifier = cs;
quantifier = mnquant;
parameters = [];
return_type = None;
body = utast_cmd_abs;
}
}
| cs=BACKSLASH_CMD; quant_and_param_units=quant_and_param_units; EXACT_EQ; utast=expr
{
Expand All @@ -515,24 +522,42 @@ bind_inline:
let utast_ctx = (rng_ctx, UTContentOf([], ident_ctx)) in
(Range.dummy "read-inline-of-lightweight-let-inline", UTReadInline(utast_ctx, utast))
in
(cs, mnquant, None,
make_standard (Ranged cs) (Ranged utast) (UTLambdaInlineCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast_body;
}))
let utast_cmd_abs =
make_standard (Ranged cs) (Ranged utast)
(UTLambdaInlineCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast_body;
})
in
UTLetBinding{
identifier = cs;
quantifier = mnquant;
parameters = [];
return_type = None;
body = utast_cmd_abs;
}
}
;
bind_block:
| ident_ctx=LOWER; cs=PLUS_CMD; quant_and_param_units=quant_and_param_units; EXACT_EQ; utast=expr
{
let (mnquant, param_units) = quant_and_param_units in
(cs, mnquant, None,
make_standard (Ranged ident_ctx) (Ranged utast) (UTLambdaBlockCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast;
}))
let utast_cmd_abs =
make_standard (Ranged ident_ctx) (Ranged utast)
(UTLambdaBlockCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast;
})
in
UTLetBinding{
identifier = cs;
quantifier = mnquant;
parameters = [];
return_type = None;
body = utast_cmd_abs;
}
}
| cs=PLUS_CMD; quant_and_param_units=quant_and_param_units; EXACT_EQ; utast=expr
{
Expand All @@ -544,25 +569,43 @@ bind_block:
let utast_ctx = (rng_ctx, UTContentOf([], ident_ctx)) in
(Range.dummy "read-block-of-lightweight-let-block", UTReadBlock(utast_ctx, utast))
in
(cs, mnquant, None,
make_standard (Ranged cs) (Ranged utast) (UTLambdaBlockCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast_body;
}))
let utast_cmd_abs =
make_standard (Ranged cs) (Ranged utast)
(UTLambdaBlockCommand{
parameters = param_units;
context_variable = ident_ctx;
body = utast_body;
})
in
UTLetBinding{
identifier = cs;
quantifier = mnquant;
parameters = [];
return_type = None;
body = utast_cmd_abs;
}
}
;
bind_math:
| ident_ctx=LOWER; cs=BACKSLASH_CMD; quant_and_param_units=quant_and_param_units; scripts_param_opt=option(scripts_param); EXACT_EQ; utast=expr
{
let (mnquant, param_units) = quant_and_param_units in
(cs, mnquant, None,
make_standard (Ranged cs) (Ranged utast) (UTLambdaMathCommand{
parameters = param_units;
context_variable = ident_ctx;
script_variables = scripts_param_opt;
body = utast;
}))
let utast_cmd_abs =
make_standard (Ranged cs) (Ranged utast)
(UTLambdaMathCommand{
parameters = param_units;
context_variable = ident_ctx;
script_variables = scripts_param_opt;
body = utast;
})
in
UTLetBinding{
identifier = cs;
quantifier = mnquant;
parameters = [];
return_type = None;
body = utast_cmd_abs;
}
}
;
scripts_param:
Expand Down
31 changes: 25 additions & 6 deletions src/frontend/typechecker.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -647,7 +647,17 @@ let rec typecheck (pre : pre) (tyenv : Typeenv.t) ((rng, utastmain) : untyped_ab
Exhchecker.main rng patbrs tyO pre tyenv;
return (PatternMatch(rng, eO, patbrs), beta)

| UTLetIn(UTNonRec((ident, ManualQuantifier(typarams, rowparams), _retty, utast1)), utast2) -> (* TODO: use `retty` *)
| UTLetIn(UTNonRec(utletbind), utast2) ->
let
UTLetBinding{
identifier = ident;
quantifier = ManualQuantifier(typarams, rowparams);
parameters = param_units;
return_type = _mntyopt_ret;
body = utast_body;
} = utletbind
in
let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *)
let* (typarammap, _) = pre.type_parameters |> add_type_parameters (Level.succ pre.level) typarams in
let* (rowparammap, _) = pre.row_parameters |> add_row_parameters (Level.succ pre.level) rowparams in
let presub =
Expand Down Expand Up @@ -1163,14 +1173,14 @@ and typecheck_letrec (pre : pre) (tyenv : Typeenv.t) (utrecbinds : untyped_let_b
(* First, adds a type variable for each bound identifier. *)
let (tyenv, utrecacc) =
utrecbinds |> List.fold_left (fun (tyenv, utrecacc) utrecbind ->
let ((varrng, varnm), _mnquant, _retty, astdef) = utrecbind in

let UTLetBinding{ identifier = (varrng, varnm); _ } = utrecbind in
let tvuref =
let tvid = fresh_free_id pre.quantifiability (Level.succ pre.level) in
ref (MonoFree(tvid))
in
let tv = Updatable(tvuref) in
let rng = get_range astdef in
let beta = (rng, TypeVariable(tv)) in
let beta = (varrng, TypeVariable(tv)) in
let pbeta = TypeConv.lift_poly beta in
let evid = EvalVarID.fresh (varrng, varnm) in
let tyenv =
Expand All @@ -1190,8 +1200,17 @@ and typecheck_letrec (pre : pre) (tyenv : Typeenv.t) (utrecbinds : untyped_let_b

(* Typechecks each body of the definitions: *)
let* tupleacc =
utrecacc |> Alist.to_list |> foldM (fun tupleacc utrec ->
let (((_, varnm), ManualQuantifier(typarams, rowparams), _retty, utast1), beta, evid) = utrec in (* TODO: use `retty` *)
utrecacc |> Alist.to_list |> foldM (fun tupleacc (utrecbind, beta, evid) ->
let
UTLetBinding{
identifier = (_, varnm);
quantifier = ManualQuantifier(typarams, rowparams);
parameters = param_units;
return_type = _mntyopt_ret;
body = utast_body;
} = utrecbind
in
let utast1 = curry_lambda_abstraction param_units utast_body in (* TODO: use `mntyopt_ret` *)
let* (typarammap, _) = pre.type_parameters |> add_type_parameters (Level.succ pre.level) typarams in
let* (rowparammap, _) = pre.row_parameters |> add_row_parameters (Level.succ pre.level) rowparams in
let presub =
Expand Down
17 changes: 15 additions & 2 deletions src/frontend/types.cppo.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -404,7 +404,7 @@ and untyped_declaration_main =
| UTDeclMacro of macro_name ranged * manual_macro_type ranged

and manual_quantifier =
ManualQuantifier of (type_variable_name ranged) list * (row_variable_name ranged * manual_row_base_kind) list
| ManualQuantifier of (type_variable_name ranged) list * (row_variable_name ranged * manual_row_base_kind) list

and manual_macro_type =
| MInlineMacroType of manual_macro_parameter_type list
Expand All @@ -423,7 +423,13 @@ and untyped_rec_or_nonrec =
| UTMutable of untyped_let_mutable_binding

and untyped_let_binding =
var_name ranged * manual_quantifier * manual_type option * untyped_abstract_tree
| UTLetBinding of {
identifier : var_name ranged;
quantifier : manual_quantifier;
parameters : untyped_parameter_unit list;
return_type : manual_type option;
body : untyped_abstract_tree;
}

and untyped_let_mutable_binding =
var_name ranged * untyped_abstract_tree
Expand Down Expand Up @@ -1565,3 +1571,10 @@ let unlift_rec_or_nonrec (cd_rec_or_nonrec : code_rec_or_nonrec) : rec_or_nonrec
| CdNonRec(symb, code) -> NonRec(CodeSymbol.unlift symb, unlift_code code)
| CdRec(cdrecbinds) -> Rec(List.map unlift_letrec_binding cdrecbinds)
| CdMutable(symb, code) -> Mutable(CodeSymbol.unlift symb, unlift_code code)


let curry_lambda_abstraction (param_units : untyped_parameter_unit list) (utast : untyped_abstract_tree) : untyped_abstract_tree =
let rng = Range.dummy "curry_lambda_abstraction" in
utast |> List.fold_right (fun param_unit utast ->
(rng, UTFunction(param_unit, utast))
) param_units

0 comments on commit 0b82aed

Please sign in to comment.