added the full parsing support for try catch lemmas

parsing/Pretty.ml

@@ -295,8 +295,32 @@ and string_of_pi pi : string =
   | Predicate (str, t) -> str ^ "(" ^ (string_of_args string_of_term t) ^ ")"
   | Subsumption (a, b) -> Format.asprintf "%s <: %s" (string_of_term a) (string_of_term b)
 
+
+and  string_of_effect_cases_specs (h_ops:(string * string option * disj_spec) list): string = 
+  match h_ops with 
+  | [] -> ""
+  | [(effname, param, spec)] -> 
+    (effname  ^  (match param with | None -> " " | Some p -> "("^ p ^ ") ")^ ": " ^ 
+    string_of_disj_spec spec)
+  | (effname, param, spec) ::xs -> 
+    (effname  ^  (match param with | None -> " " | Some p -> "("^ p ^ ") ")^ ": " ^ 
+    string_of_disj_spec spec ^ "\n"
+    ) ^ string_of_effect_cases_specs xs 
+
+
+and string_of_normal_case_specs ((param, h_norm):(string * disj_spec)): string = 
+  ((match param with | p -> p ^ "")^ ": " ^ string_of_disj_spec (h_norm)); 
+
+and string_of_handlingcases ((h_normal, h_ops):handlingcases) : string = 
+    "{\n" ^ 
+    string_of_normal_case_specs h_normal ^ "\n" ^ 
+    string_of_effect_cases_specs h_ops 
+    ^ "\n}\n"
+
+
+
 and string_of_try_catch_lemma (x:tryCatchLemma) : string = 
-  let (tcl_head, tcl_handledCont, tcl_summary) = x in 
+  let (tcl_head, tcl_handledCont, (h_normal, h_ops), tcl_summary) = x in 
   "TRY " 
   ^ 
   string_of_spec tcl_head 
@@ -305,8 +329,8 @@ and string_of_try_catch_lemma (x:tryCatchLemma) : string =
   | None -> "" | Some conti -> " # " ^ string_of_disj_spec conti)
 
 
-  ^ " CATCH \n"
-  ^ "=== " ^ string_of_disj_spec tcl_summary
+  ^ " CATCH \n" ^ string_of_handlingcases (h_normal, h_ops )
+  ^ "=> " ^ string_of_disj_spec tcl_summary
 
 and string_of_handler_type (h:handler_type) : string = 
     match h with

parsing/forward_rules.ml

@@ -453,6 +453,11 @@ let findTheActualArg4Acc_x_e_ret (arg:term) (specs:disj_spec): term =
 
   | _ -> failwith ("findTheTermAssocatiedWith_x_e_ret empty spec")
 
+
+
+
+
+
 (** this is the entrance of the try-catch reduction **)
 let rec handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:normalisedStagedSpec) (h_norm:(string * disj_spec)) (h_ops:(string * string option * disj_spec) list) : spec list * fvenv = 
 
@@ -489,9 +494,10 @@ let rec handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:nor
       concatenateSpecsWithSpec (normalise_spec_list [(scr_normal)]) h_spec
 
     in
-    print_endline ("\nhandling_spec " ^ (string_of_spec (normalisedStagedSpec2Spec scr_spec))); 
+    (*print_endline ("\nhandling_spec " ^ (string_of_spec (normalisedStagedSpec2Spec scr_spec))); 
 
     print_endline ("Final results [] : " ^ string_of_spec_list current);
+    *)
     current, env
 
   | (TryCatchStage _) :: _ -> [(normalisedStagedSpec2Spec scr_spec)], env
@@ -531,12 +537,16 @@ let rec handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:nor
 
 
       match match_summary with 
-      | Some (tcl_head, Some tcl_handledCont, tcl_summary) -> 
+      | Some (tcl_head, Some tcl_handledCont, (handlerSpec),  tcl_summary) -> 
 
 
-      print_endline (string_of_try_catch_lemma (tcl_head, Some tcl_handledCont, tcl_summary) ^ "\n");
+      print_endline (string_of_try_catch_lemma (tcl_head, Some tcl_handledCont, handlerSpec, tcl_summary) ^ "\n");
       print_endline (string_of_effHOTryCatchStages (EffHOStage x) ^ " # " ^ string_of_spec_list handledContinuation);
       print_endline ("");
+
+      print_endline (string_of_handlingcases (h_norm,h_ops)); 
+
+
 
 
         let effFormalArg = 
@@ -560,8 +570,6 @@ let rec handling_spec typ env (match_summary:tryCatchLemma option) (scr_spec:nor
         let contiRet = findTheActualArg4Acc_x_e_ret x.e_ret handledContinuation in 
 
 
-
-
         (* SYH: here hard coded the instantiation for m and acc for the purpose of the toss example. *)
         let mi = match typ with | Deep -> ("m", Num 2) | Shallow -> ("m", Num 1) in 
         let instantiate_tcl_summary = renameSpecListAndInstantiate tcl_summary (mi::("acc", contiRet)::bindings) in
@@ -858,12 +866,12 @@ let rec infer_of_expression (env:fvenv) (history:disj_spec) (expr:core_lang): di
           in
           (*let sp = normalize_spec sp in *)
           let sp = (normalise_spec_list sp) in 
+
+          (*
+          print_endline (string_of_effect_cases_specs [(effname,param, sp)]); 
+    *)
 
-          (*print_endline ("Inferred_effect_cases_specs: --------- \n" ^ effname  ^  (match param with | None -> " " | Some p -> "("^ p ^ ") ")^ ": " ^ 
-          string_of_disj_spec sp
-          ); 
-          *)  
-
+
 
           (effname, param, sp) :: t, env
         ) eff_cases ([], env)
@@ -872,10 +880,12 @@ let rec infer_of_expression (env:fvenv) (history:disj_spec) (expr:core_lang): di
       let inferred_val_case, env =
         let (param, body)  = val_case in
         let inf_val_spec, env = infer_of_expression env [[]] body in
+        let inf_val_spec = normalise_spec_list inf_val_spec in 
+
+        (*
+        print_endline (string_of_normal_case_specs (param, inf_val_spec)); 
+*)
 
-        (*print_endline ("Inferred_nromal_clause_spec: --------- \n" ^  (match param with | p -> p ^ "")^ ": " ^ 
-        string_of_disj_spec (normalise_spec_list inf_val_spec));  
-        *)
 
         (param, inf_val_spec), env
       in

parsing/hiptypes.ml

@@ -35,7 +35,7 @@ and core_handler_ops = (string * string option * disj_spec option * core_lang) l
 (* x :: xs -> e is represented as ("::", [x, xs], e) *)
 and constr_cases = (string * string list * core_lang) list
 
-and tryCatchLemma = (spec * disj_spec option * disj_spec) (*tcl_head, tcl_handledCont, tcl_summary*)
+and tryCatchLemma = (spec * disj_spec option * (handlingcases) * disj_spec) (*tcl_head, tcl_handledCont, tcl_summary*)
 
 and handler_type = Shallow | Deep 
 

parsing/parser.mly

@@ -2749,13 +2749,32 @@ handler_type:
 | SHALLOW {Shallow}
 | {Deep}
 
+option_formal_arg :
+| str= LIDENT {Some str }
+| {None }
+
+
+handler_effect_cases:
+| {[]}
+| eff = UIDENT LPAREN arg = option_formal_arg RPAREN COLON h_effect_spec= disj_effect_spec BAR  
+  h_ops = handler_effect_cases 
+  {(eff, arg, h_effect_spec)::h_ops}
+
+
 type_try_catch_lemma:
 | LSPECCOMMENT ht=handler_type RSPECCOMMENT
 {ht, None}
-| LSPECCOMMENT ht=handler_type TRY head_spec= effect_spec conti=option_conti_sharp EFFCATCH EQUAL 
+| LSPECCOMMENT ht=handler_type TRY head_spec= effect_spec conti=option_conti_sharp EFFCATCH 
+  LBRACE h_normal_param = LIDENT  COLON h_normal_spec= disj_effect_spec BAR 
+  h_ops = handler_effect_cases 
+  RBRACE
+  EQUAL 
   summary = disj_effect_spec
    RSPECCOMMENT
-  {(ht, Some (head_spec, conti, summary))}
+  {
+    let h_normal = (h_normal_param, h_normal_spec) in 
+
+    (ht, Some (head_spec, conti, (h_normal, h_ops),  summary))}
 | {(Deep, None)}
 
 

src/demo/2_Inductive_Sum.ml

@@ -18,6 +18,9 @@ let handler n
   match sumEff n with 
   (* try-catch lemma defined here *)
   (*@   try ex r; req n>=0; sumEff(n,r) # Norm(emp,acc+r) catch 
+     {v : ens res=v | 
+     Inc(v) : ex v207 v208 v209 v210 v211; req i->v207; ens i->v210/\v208=(v207+v)/\v210=(v208-1); continue(k, 1, v211); ens res=v211 | 
+     }
      =  ex w; req i->w; Norm (i->w+(n*.(n-1)/2), n+acc)  @*) 
   | v ->  v
   | effect (Inc v) k ->