diff options
Diffstat (limited to 'src/process_file.ml')
| -rw-r--r-- | src/process_file.ml | 53 |
1 files changed, 3 insertions, 50 deletions
diff --git a/src/process_file.ml b/src/process_file.ml index 3c2d4a22..dbe6d62d 100644 --- a/src/process_file.ml +++ b/src/process_file.ml @@ -126,33 +126,6 @@ let cond_pragma l defs = in scan defs -let astid_to_string (Ast.Id_aux (id, _)) = - match id with - | Ast.Id x | Ast.DeIid x -> x - -let parseid_to_string (Parse_ast.Id_aux (id, _)) = - match id with - | Parse_ast.Id x | Parse_ast.DeIid x -> x - -let rec realise_union_anon_rec_types orig_union arms = - match orig_union with - | Parse_ast.TD_variant (union_id, typq, _, flag) -> - begin match arms with - | [] -> [] - | arm :: arms -> - match arm with - | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_id _), _)) -> (None, arm) :: realise_union_anon_rec_types orig_union arms - | (Parse_ast.Tu_aux ((Parse_ast.Tu_ty_anon_rec (fields, id)), l)) -> - let open Parse_ast in - let record_str = "_" ^ parseid_to_string union_id ^ "_" ^ parseid_to_string id ^ "_record" in - let record_id = Id_aux (Id record_str, Generated l) in - let new_arm = Tu_aux ((Tu_ty_id ((ATyp_aux (ATyp_id record_id, Generated l)), id)), Generated l) in - let new_rec_def = DEF_type (TD_aux (TD_record (record_id, typq, fields, flag), Generated l)) in - (Some new_rec_def, new_arm) :: (realise_union_anon_rec_types orig_union arms) - end - | _ -> - raise (Reporting.err_unreachable Parse_ast.Unknown __POS__ "Non union type-definition passed to realise_union_anon_rec_typs") - let rec preprocess opts = function | [] -> [] | Parse_ast.DEF_pragma ("define", symbol, _) :: defs -> @@ -218,20 +191,6 @@ let rec preprocess opts = function | Parse_ast.DEF_pragma (p, arg, l) :: defs -> Parse_ast.DEF_pragma (p, arg, l) :: preprocess opts defs - (* realise any anonymous record arms of variants *) - | Parse_ast.DEF_type (Parse_ast.TD_aux - (Parse_ast.TD_variant (id, typq, arms, flag) as union, l) - ) :: defs -> - let records_and_arms = realise_union_anon_rec_types union arms in - let rec filter_records = function [] -> [] - | Some x :: xs -> x :: filter_records xs - | None :: xs -> filter_records xs - in - let generated_records = filter_records (List.map fst records_and_arms) in - let rewritten_arms = List.map snd records_and_arms in - let rewritten_union = Parse_ast.TD_variant (id, typq, rewritten_arms, flag) in - generated_records @ (Parse_ast.DEF_type (Parse_ast.TD_aux (rewritten_union, l))) :: preprocess opts defs - | (Parse_ast.DEF_default (Parse_ast.DT_aux (Parse_ast.DT_order (_, Parse_ast.ATyp_aux (atyp, _)), _)) as def) :: defs -> begin match atyp with | Parse_ast.ATyp_inc -> symbols := StringSet.add "_DEFAULT_INC" !symbols; def :: preprocess opts defs @@ -402,14 +361,8 @@ let rewrite env rewriters defs = | Type_check.Type_error (_, l, err) -> raise (Reporting.err_typ l (Type_error.string_of_type_error err)) -let rewrite_ast env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)] -let rewrite_ast_lem env = rewrite env Rewrites.rewrite_defs_lem -let rewrite_ast_coq env = rewrite env Rewrites.rewrite_defs_coq -let rewrite_ast_ocaml env = rewrite env Rewrites.rewrite_defs_ocaml -let rewrite_ast_c env ast = - ast - |> rewrite env Rewrites.rewrite_defs_c - |> rewrite env [("constant_fold", fun _ -> Constant_fold.rewrite_constant_function_calls env)] +let rewrite_ast_initial env = rewrite env [("initial", fun _ -> Rewriter.rewrite_defs)] + +let rewrite_ast_target tgt env = rewrite env (Rewrites.rewrite_defs_target tgt) -let rewrite_ast_interpreter env = rewrite env Rewrites.rewrite_defs_interpreter let rewrite_ast_check env = rewrite env Rewrites.rewrite_defs_check |