From 2e2d78d55d6512e479d5638dd18dae343eec9c03 Mon Sep 17 00:00:00 2001 From: Chris Hawblitzel Date: Tue, 21 Jul 2020 20:46:51 -0700 Subject: [PATCH] Update importFStarTypes for upcoming F* changes --- tools/ImportFStarTypes/src/main.fs | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/tools/ImportFStarTypes/src/main.fs b/tools/ImportFStarTypes/src/main.fs index 5dd04b34..d9424eb7 100644 --- a/tools/ImportFStarTypes/src/main.fs +++ b/tools/ImportFStarTypes/src/main.fs @@ -255,9 +255,10 @@ let rec parse_exp (e:raw_exp):f_exp = EArrow (a, x, parse_exp e1, parse_exp e2) ) with Err s -> EUnsupported s - | RList [RColon _; e1; RId (_, ("Tm_type" | "Tm_delayed"))] -> parse_exp e1 - | RList [RColon _; e1; RList [RColon _; RId (_, ("Tm_name" | "Tm_fvar")); _]] -> parse_exp e1 - | RList [RColon _; e1; e2] -> ETyped (parse_exp e1, parse_exp e2) +// | RList [RColon _; e1; RId (_, ("Tm_type" | "Tm_delayed"))] -> parse_exp e1 +// | RList [RColon _; e1; RList [RColon _; RId (_, ("Tm_name" | "Tm_fvar")); _]] -> parse_exp e1 +// | RList [RColon _; e1; e2] -> ETyped (parse_exp e1, parse_exp e2) + | RList [RColon _; e1; _] -> parse_exp e1 | RList [RRefine _; RList [RColon _; RId (_, x); e1]; e2] -> ERefine (parse_id x, parse_exp e1, parse_exp e2) | RList [RAscribed _; e1; e2] -> ETyped (parse_exp e1, parse_exp e2) | RList [RPattern _; RList pats; e] -> @@ -1185,7 +1186,7 @@ let main (argv:string array) = let modules = List.filter (fun (x:string list) -> match x with s::_ when s = sModule -> true | _ -> false) modules in let get_module_blocks (lines:string list):string list list = let lines = List.filter (fun (x:string) -> not (x.StartsWith("#") || x.Contains("): (Warning "))) lines in - match splitWhere (fun (x:string) -> x.StartsWith("Exports:")) lines with + match splitWhere (fun (x:string) -> x.StartsWith("Declarations:")) lines with | [_; (_::lines)] -> splitWhere (fun (x:string) ->