very unstable state
This commit is contained in:
parent
055bee804e
commit
8d6f19ac6c
@ -116,7 +116,7 @@ and declaration =
|
|||||||
(* Non-recursive values *)
|
(* Non-recursive values *)
|
||||||
|
|
||||||
and let_binding = {
|
and let_binding = {
|
||||||
variable : variable;
|
bindings : pattern list;
|
||||||
lhs_type : (colon * type_expr) option;
|
lhs_type : (colon * type_expr) option;
|
||||||
eq : equal;
|
eq : equal;
|
||||||
let_rhs : expr
|
let_rhs : expr
|
||||||
@ -544,8 +544,8 @@ and print_terminator = function
|
|||||||
Some semi -> print_token semi ";"
|
Some semi -> print_token semi ";"
|
||||||
| None -> ()
|
| None -> ()
|
||||||
|
|
||||||
and print_let_binding {variable; lhs_type; eq; let_rhs} =
|
and print_let_binding {bindings; lhs_type; eq; let_rhs} =
|
||||||
print_var variable;
|
List.iter print_pattern bindings;
|
||||||
(match lhs_type with
|
(match lhs_type with
|
||||||
None -> ()
|
None -> ()
|
||||||
| Some (colon, type_expr) ->
|
| Some (colon, type_expr) ->
|
||||||
|
@ -125,7 +125,7 @@ and declaration =
|
|||||||
(* Non-recursive values *)
|
(* Non-recursive values *)
|
||||||
|
|
||||||
and let_binding = { (* p = e p : t = e *)
|
and let_binding = { (* p = e p : t = e *)
|
||||||
variable : variable;
|
bindings : pattern list;
|
||||||
lhs_type : (colon * type_expr) option;
|
lhs_type : (colon * type_expr) option;
|
||||||
eq : equal;
|
eq : equal;
|
||||||
let_rhs : expr
|
let_rhs : expr
|
||||||
|
@ -42,142 +42,9 @@ let rec sub_rec fresh path (map, rank) pattern =
|
|||||||
let map' = split fresh map path' pattern
|
let map' = split fresh map path' pattern
|
||||||
in map', rank+1
|
in map', rank+1
|
||||||
|
|
||||||
and split fresh map path = function
|
|
||||||
PTuple t -> let apply = sub_rec fresh path in
|
|
||||||
Utils.nsepseq_foldl apply (map,1) t.value |> fst
|
|
||||||
| PPar p -> split fresh map path p.value.inside
|
|
||||||
| PVar v -> if VMap.mem v.value map
|
|
||||||
then
|
|
||||||
let err =
|
|
||||||
Region.{value="Non-linear pattern."; region=v.region}
|
|
||||||
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
|
||||||
else
|
|
||||||
let proj = mk_projection fresh path
|
|
||||||
in VMap.add v.value (None, proj) map
|
|
||||||
| PWild _ -> map
|
|
||||||
| PUnit _ -> let anon = Utils.gen_sym () in
|
|
||||||
let unit = ghost, TAlias (ghost_of "unit")
|
|
||||||
and proj = mk_projection fresh path
|
|
||||||
in VMap.add anon (Some unit, proj) map
|
|
||||||
| PRecord {region; _}
|
|
||||||
| PConstr {region; _}
|
|
||||||
| PTyped {region; _} ->
|
|
||||||
let err = Region.{value="Not implemented yet."; region}
|
|
||||||
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
|
||||||
| p -> let _, _, map = split_pattern p in map
|
|
||||||
|
|
||||||
and split_pattern = function
|
|
||||||
PPar p -> split_pattern p.value.inside
|
|
||||||
| PVar v -> v, None, VMap.empty
|
|
||||||
| PWild _ -> Utils.gen_sym () |> ghost_of, None, VMap.empty
|
|
||||||
| PUnit _ -> let fresh = Utils.gen_sym () |> ghost_of in
|
|
||||||
let unit = TAlias (ghost_of "unit")
|
|
||||||
in fresh, Some unit, VMap.empty
|
|
||||||
| PTyped {value=p; _} ->
|
|
||||||
let var', type', map = split_pattern p.pattern in
|
|
||||||
(match type' with
|
|
||||||
None -> var', Some p.type_expr, map
|
|
||||||
| Some t when t = p.type_expr -> var', Some t, map (* hack *)
|
|
||||||
| Some t -> fail_syn_unif t p.type_expr)
|
|
||||||
| PTuple t ->
|
|
||||||
let fresh = Utils.gen_sym () |> ghost_of
|
|
||||||
and init = VMap.empty, 1 in
|
|
||||||
let apply (map, rank) pattern =
|
|
||||||
split fresh map (rank,[]) pattern, rank+1 in
|
|
||||||
let map = Utils.nsepseq_foldl apply init t.value |> fst
|
|
||||||
in fresh, None, map
|
|
||||||
| PRecord {region; _}
|
|
||||||
| PConstr {region; _} ->
|
|
||||||
let err = Region.{value="Not implemented yet."; region}
|
|
||||||
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
|
||||||
| PInt {region; _} | PTrue region
|
|
||||||
| PFalse region | PString {region; _}
|
|
||||||
| PList Sugar {region; _} | PList PCons {region; _} ->
|
|
||||||
let err = Region.{value="Incomplete pattern."; region}
|
|
||||||
in (Lexer.prerr ~kind:"Syntactical" err; exit 1)
|
|
||||||
|
|
||||||
let mk_let_bindings =
|
|
||||||
let apply var (lhs_type, proj) =
|
|
||||||
let new_bind = {
|
|
||||||
variable = ghost_of var;
|
|
||||||
lhs_type;
|
|
||||||
eq = ghost;
|
|
||||||
let_rhs = EProj (ghost_of proj)} in
|
|
||||||
let new_let = Let (ghost_of (ghost, new_bind))
|
|
||||||
in Utils.nseq_cons new_let
|
|
||||||
in VMap.fold apply
|
|
||||||
|
|
||||||
let mk_let_in_bindings =
|
|
||||||
let apply var (lhs_type, proj) acc =
|
|
||||||
let binding = {
|
|
||||||
variable = ghost_of var;
|
|
||||||
lhs_type;
|
|
||||||
eq = ghost;
|
|
||||||
let_rhs = EProj (ghost_of proj)} in
|
|
||||||
let let_in = {
|
|
||||||
kwd_let = ghost;
|
|
||||||
binding;
|
|
||||||
kwd_in = ghost;
|
|
||||||
body = acc}
|
|
||||||
in ELetIn (ghost_of let_in)
|
|
||||||
in VMap.fold apply
|
|
||||||
|
|
||||||
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
|
(* We rewrite "fun p -> e" into "fun x -> match x with p -> e" *)
|
||||||
|
|
||||||
let norm_fun_expr patterns expr =
|
|
||||||
let apply pattern expr =
|
|
||||||
match pattern with
|
|
||||||
PVar var ->
|
|
||||||
let fun_expr = {
|
|
||||||
kwd_fun = ghost;
|
|
||||||
param = var;
|
|
||||||
p_annot = None;
|
|
||||||
arrow = ghost;
|
|
||||||
body = expr}
|
|
||||||
in EFun (ghost_of fun_expr)
|
|
||||||
| PTyped p ->
|
|
||||||
let pattern = p.value.pattern
|
|
||||||
and type_expr = p.value.type_expr in
|
|
||||||
let fresh = Utils.gen_sym () |> ghost_of in
|
|
||||||
let clause = {pattern; arrow=ghost; rhs=expr} in
|
|
||||||
let clause = ghost_of clause in
|
|
||||||
let cases = ghost_of (clause, []) in
|
|
||||||
let case = {
|
|
||||||
kwd_match = ghost;
|
|
||||||
expr = EVar fresh;
|
|
||||||
opening = With ghost;
|
|
||||||
lead_vbar = None;
|
|
||||||
cases;
|
|
||||||
closing = End ghost} in
|
|
||||||
let case = ECase (ghost_of case) in
|
|
||||||
let fun_expr = {
|
|
||||||
kwd_fun = ghost;
|
|
||||||
param = fresh;
|
|
||||||
p_annot = Some (p.value.colon, type_expr);
|
|
||||||
arrow = ghost;
|
|
||||||
body = case}
|
|
||||||
in EFun (ghost_of fun_expr)
|
|
||||||
| _ -> let fresh = Utils.gen_sym () |> ghost_of in
|
|
||||||
let clause = {pattern; arrow=ghost; rhs=expr} in
|
|
||||||
let clause = ghost_of clause in
|
|
||||||
let cases = ghost_of (clause, []) in
|
|
||||||
let case = {
|
|
||||||
kwd_match = ghost;
|
|
||||||
expr = EVar fresh;
|
|
||||||
opening = With ghost;
|
|
||||||
lead_vbar = None;
|
|
||||||
cases;
|
|
||||||
closing = End ghost} in
|
|
||||||
let case = ECase (ghost_of case) in
|
|
||||||
let fun_expr = {
|
|
||||||
kwd_fun = ghost;
|
|
||||||
param = fresh;
|
|
||||||
p_annot = None;
|
|
||||||
arrow = ghost;
|
|
||||||
body = case}
|
|
||||||
in EFun (ghost_of fun_expr)
|
|
||||||
in Utils.nseq_foldr apply patterns expr
|
|
||||||
|
|
||||||
(* END HEADER *)
|
(* END HEADER *)
|
||||||
%}
|
%}
|
||||||
|
|
||||||
@ -416,11 +283,11 @@ field_decl:
|
|||||||
|
|
||||||
entry_binding:
|
entry_binding:
|
||||||
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
let let_rhs = norm_fun_expr $2 $5 in
|
let let_rhs = $5 in
|
||||||
{variable = $1; lhs_type=$3; eq=$4; let_rhs}
|
{bindings = ($1 , $2); lhs_type=$3; eq=$4; let_rhs}
|
||||||
}
|
}
|
||||||
| ident type_annotation? eq fun_expr(expr) {
|
| ident type_annotation? eq fun_expr(expr) {
|
||||||
{variable = $1; lhs_type=$2; eq=$3; let_rhs=$4} }
|
{bindings = ($1 , []); lhs_type=$2; eq=$3; let_rhs=$4} }
|
||||||
|
|
||||||
(* Top-level non-recursive definitions *)
|
(* Top-level non-recursive definitions *)
|
||||||
|
|
||||||
@ -428,14 +295,15 @@ let_declaration:
|
|||||||
reg(kwd(Let) let_binding {$1,$2}) {
|
reg(kwd(Let) let_binding {$1,$2}) {
|
||||||
let kwd_let, (binding, map) = $1.value in
|
let kwd_let, (binding, map) = $1.value in
|
||||||
let let0 = Let {$1 with value = kwd_let, binding}
|
let let0 = Let {$1 with value = kwd_let, binding}
|
||||||
in mk_let_bindings map (let0,[])
|
in
|
||||||
|
mk_let_bindings map (let0,[])
|
||||||
}
|
}
|
||||||
|
|
||||||
let_binding:
|
let_binding:
|
||||||
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
ident nseq(sub_irrefutable) type_annotation? eq expr {
|
||||||
let let_rhs = norm_fun_expr $2 $5 in
|
let let_rhs = $5 in
|
||||||
let map = VMap.empty in
|
let map = VMap.empty in
|
||||||
{variable=$1; lhs_type=$3; eq=$4; let_rhs}, map
|
{bindings= ($1 , $2); lhs_type=$3; eq=$4; let_rhs}, map
|
||||||
}
|
}
|
||||||
| irrefutable type_annotation? eq expr {
|
| irrefutable type_annotation? eq expr {
|
||||||
let variable, type_opt, map = split_pattern $1 in
|
let variable, type_opt, map = split_pattern $1 in
|
||||||
|
@ -237,20 +237,7 @@ let rec simpl_expression :
|
|||||||
)
|
)
|
||||||
| _ -> default_action ()
|
| _ -> default_action ()
|
||||||
)
|
)
|
||||||
| EFun lamb ->
|
| EFun lamb -> simpl_fun lamb
|
||||||
let%bind input_type = bind_map_option
|
|
||||||
(fun (_,type_expr) -> simpl_type_expression type_expr)
|
|
||||||
lamb.value.p_annot in
|
|
||||||
let body, body_type =
|
|
||||||
match lamb.value.body with
|
|
||||||
EAnnot {value = expr, type_expr} -> expr, Some type_expr
|
|
||||||
| expr -> expr, None in
|
|
||||||
let%bind output_type =
|
|
||||||
bind_map_option simpl_type_expression body_type in
|
|
||||||
let%bind result = simpl_expression body in
|
|
||||||
let binder = lamb.value.param.value, input_type in
|
|
||||||
let lambda = {binder; input_type; output_type; result = result}
|
|
||||||
in return @@ E_lambda lambda
|
|
||||||
| ESeq s ->
|
| ESeq s ->
|
||||||
let items : Raw.expr list = pseq_to_list s.value.elements in
|
let items : Raw.expr list = pseq_to_list s.value.elements in
|
||||||
(match items with
|
(match items with
|
||||||
@ -269,6 +256,50 @@ let rec simpl_expression :
|
|||||||
let%bind match_false = simpl_expression c.ifnot in
|
let%bind match_false = simpl_expression c.ifnot in
|
||||||
return @@ E_matching (expr, (Match_bool {match_true; match_false}))
|
return @@ E_matching (expr, (Match_bool {match_true; match_false}))
|
||||||
|
|
||||||
|
and simpl_fun lamb : expr result =
|
||||||
|
let return x = ok x in
|
||||||
|
let rec aux args body =
|
||||||
|
match body with
|
||||||
|
| Raw.EFun l -> (
|
||||||
|
let l' = l.value in
|
||||||
|
let annot = Option.map snd l'.p_annot in
|
||||||
|
aux (args @ [(l'.param.value , annot)]) l'.body
|
||||||
|
)
|
||||||
|
| _ -> (args , body) in
|
||||||
|
let (args , body) = aux [] (Raw.EFun lamb) in
|
||||||
|
let%bind args' =
|
||||||
|
let aux = fun (name , ty_opt) ->
|
||||||
|
let%bind ty =
|
||||||
|
match ty_opt with
|
||||||
|
| Some ty -> simpl_type_expression ty
|
||||||
|
| None when name = "storage" -> ok (T_variable "storage")
|
||||||
|
| None -> simple_fail "missing type annotation on input"
|
||||||
|
in
|
||||||
|
ok (name , ty)
|
||||||
|
in
|
||||||
|
bind_map_list aux args
|
||||||
|
in
|
||||||
|
let arguments_name = "arguments" in
|
||||||
|
let (binder , input_type) =
|
||||||
|
let type_expression = T_tuple (List.map snd args') in
|
||||||
|
(arguments_name , type_expression) in
|
||||||
|
let body, body_type =
|
||||||
|
match body with
|
||||||
|
| EAnnot {value = expr, type_expr} -> expr, Some type_expr
|
||||||
|
| expr -> expr, None in
|
||||||
|
let%bind output_type =
|
||||||
|
bind_map_option simpl_type_expression body_type in
|
||||||
|
let%bind result = simpl_expression body in
|
||||||
|
let wrapped_result =
|
||||||
|
let aux = fun i (name , ty) wrapped ->
|
||||||
|
let accessor = E_accessor (E_variable arguments_name , [ Access_tuple i ]) in
|
||||||
|
e_let_in (name , Some ty) accessor wrapped
|
||||||
|
in
|
||||||
|
let wraps = List.mapi aux args' in
|
||||||
|
List.fold_right' (fun x f -> f x) result wraps in
|
||||||
|
let lambda = {binder = (binder , Some input_type); input_type = (Some input_type); output_type; result = wrapped_result}
|
||||||
|
in return @@ E_lambda lambda
|
||||||
|
|
||||||
|
|
||||||
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
|
and simpl_logic_expression ?te_annot (t:Raw.logic_expr) : expr result =
|
||||||
let return x = ok @@ make_option_typed x te_annot in
|
let return x = ok @@ make_option_typed x te_annot in
|
||||||
|
@ -351,7 +351,6 @@ and simpl_fun_declaration : Raw.fun_decl -> ((name * type_expression option) * e
|
|||||||
let arguments_name = "arguments" in
|
let arguments_name = "arguments" in
|
||||||
let%bind params = bind_map_list simpl_param lst in
|
let%bind params = bind_map_list simpl_param lst in
|
||||||
let (binder , input_type) =
|
let (binder , input_type) =
|
||||||
(* let type_expression = T_record (SMap.of_list params) in *)
|
|
||||||
let type_expression = T_tuple (List.map snd params) in
|
let type_expression = T_tuple (List.map snd params) in
|
||||||
(arguments_name , type_expression) in
|
(arguments_name , type_expression) in
|
||||||
let%bind tpl_declarations =
|
let%bind tpl_declarations =
|
||||||
|
Loading…
Reference in New Issue
Block a user