Add checks for variable identifiers in pattern subsumption

5 files changed, 43 insertions, 33 deletions

diff --git a/src/process_file.ml b/src/process_file.ml
index 2425a9bb..cfd27265 100644
--- a/src/process_file.ml
+++ b/src/process_file.ml
@@ -114,7 +114,7 @@ let check_ast (defs : Type_internal.tannot Ast.defs) (k : kind Envmap.t) (o:Ast.
   Type_check.check (Type_check.Env (d_env, Type_internal.initial_typ_env,Type_internal.nob,Envmap.empty)) defs 
 
 let rewrite_ast (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs defs
-let rewrite_ast_lem (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_lem defs
+let rewrite_ast_lem (Type_check.Env (_, typ_env, _, _)) (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_lem typ_env defs
 let rewrite_ast_ocaml (defs: Type_internal.tannot Ast.defs) = Rewriter.rewrite_defs_ocaml defs
 
 let open_output_with_check file_name =
@@ -237,4 +237,3 @@ let output libpath out_arg files =
     (fun (f, defs) ->
        output1 libpath out_arg f defs)
     files
-
diff --git a/src/process_file.mli b/src/process_file.mli
index aa8d3265..e2c04cd2 100644
--- a/src/process_file.mli
+++ b/src/process_file.mli
@@ -45,7 +45,7 @@ val convert_ast : Parse_ast.defs -> Type_internal.tannot Ast.defs * Type_interna
 val initi_check_ast : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs * Type_internal.kind Type_internal.Envmap.t * Ast.order
 val check_ast: Type_internal.tannot Ast.defs -> Type_internal.kind Type_internal.Envmap.t -> Ast.order -> Type_internal.tannot Ast.defs * Type_check.envs
 val rewrite_ast: Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
-val rewrite_ast_lem : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
+val rewrite_ast_lem : Type_check.envs -> Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 val rewrite_ast_ocaml : Type_internal.tannot Ast.defs -> Type_internal.tannot Ast.defs
 
 val opt_new_typecheck : bool ref
diff --git a/src/rewriter.ml b/src/rewriter.ml
index 8e120dda..a2eccece 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1417,13 +1417,22 @@ let remove_wildcards pre (P_aux (_,(l,_)) as pat) =
         | (p,annot) -> P_aux (p,annot) }
     pat
 
+(* Based on current type checker's behaviour *)
+let pat_id_is_variable t_env id =
+  match Envmap.apply t_env id with
+  | Some (Base(_,Constructor _,_,_,_,_))
+  | Some (Base(_,Enum _,_,_,_,_))
+    -> false
+  | _ -> true
+
 (* Check if one pattern subsumes the other, and if so, calculate a
    substitution of variables that are used in the same position.
    TODO: Check somewhere that there are no variable clashes (the same variable
    name used in different positions of the patterns)
  *)
-let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,_) as pat2) =
+let rec subsumes_pat typ_env (P_aux (p1,annot1) as pat1) (P_aux (p2,_) as pat2) =
   let rewrap p = P_aux (p,annot1) in
+  let subsumes = subsumes_pat typ_env in
   let subsumes_list s pats1 pats2 =
     if List.length pats1 = List.length pats2
     then
@@ -1437,33 +1446,36 @@ let rec subsumes_pat (P_aux (p1,annot1) as pat1) (P_aux (p2,_) as pat2) =
   match p1, p2 with
   | P_lit (L_aux (lit1,_)), P_lit (L_aux (lit2,_)) ->
       if lit1 = lit2 then Some [] else None
-  | P_as (pat1,_), _ -> subsumes_pat pat1 pat2
-  | _, P_as (pat2,_) -> subsumes_pat pat1 pat2
-  | P_typ (_,pat1), _ -> subsumes_pat pat1 pat2
-  | _, P_typ (_,pat2) -> subsumes_pat pat1 pat2
+  | P_as (pat1,_), _ -> subsumes pat1 pat2
+  | _, P_as (pat2,_) -> subsumes pat1 pat2
+  | P_typ (_,pat1), _ -> subsumes pat1 pat2
+  | _, P_typ (_,pat2) -> subsumes pat1 pat2
   | P_id (Id_aux (id1,_) as aid1), P_id (Id_aux (id2,_) as aid2) ->
-    if id1 = id2 then Some [] else Some [(id2,id1)]
-  | P_id id1, _ -> Some []
+    if id1 = id2 then Some []
+    else if pat_id_is_variable typ_env (id_to_string aid1) &&
+            pat_id_is_variable typ_env (id_to_string aid1)
+           then Some [(id2,id1)] else None
+  | P_id id1, _ -> if pat_id_is_variable typ_env (id_to_string id1) then Some [] else None
   | P_wild, _ -> Some []
   | P_app (Id_aux (id1,l1),args1), P_app (Id_aux (id2,_),args2) ->
-    if id1 = id2 then subsumes_list subsumes_pat args1 args2 else None
+    if id1 = id2 then subsumes_list subsumes args1 args2 else None
   | P_record (fps1,b1), P_record (fps2,b2) ->
-    if b1 = b2 then subsumes_list subsumes_fpat fps1 fps2 else None
+    if b1 = b2 then subsumes_list (subsumes_fpat typ_env) fps1 fps2 else None
   | P_vector pats1, P_vector pats2
   | P_vector_concat pats1, P_vector_concat pats2
   | P_tup pats1, P_tup pats2
   | P_list pats1, P_list pats2 ->
-    subsumes_list subsumes_pat pats1 pats2
+    subsumes_list subsumes pats1 pats2
   | P_vector_indexed ips1, P_vector_indexed ips2 ->
     let (is1,ps1) = List.split ips1 in
     let (is2,ps2) = List.split ips2 in
-    if is1 = is2 then subsumes_list subsumes_pat ps1 ps2 else None
+    if is1 = is2 then subsumes_list subsumes ps1 ps2 else None
   | _ -> None
-and subsumes_fpat (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
-  if id1 = id2 then subsumes_pat pat1 pat2 else None
+and subsumes_fpat typ_env (FP_aux (FP_Fpat (id1,pat1),_)) (FP_aux (FP_Fpat (id2,pat2),_)) =
+  if id1 = id2 then subsumes_pat typ_env pat1 pat2 else None
 
-let equiv_pats pat1 pat2 =
-  match subsumes_pat pat1 pat2, subsumes_pat pat2 pat1 with
+let equiv_pats typ_env pat1 pat2 =
+  match subsumes_pat typ_env pat1 pat2, subsumes_pat typ_env pat2 pat1 with
   | Some _, Some _ -> true
   | _, _ -> false
 
@@ -1511,13 +1523,13 @@ let case_exp e t cs =
   (* let efr = union_effs (List.map get_effsum_pexp ps) in *)
   fix_effsum_exp (E_aux (E_case (e,ps), gen_annot (get_loc e) t pure_e))
 
-let rewrite_guarded_clauses l cs =
+let rewrite_guarded_clauses typ_env l cs =
   let rec group clauses =
     let add_clause (pat,cls,annot) c = (pat,cls @ [c],annot) in
     let rec group_aux current acc = (function
       | ((pat,guard,body,annot) as c) :: cs ->
           let (current_pat,_,_) = current in
-          (match subsumes_pat current_pat pat with
+          (match subsumes_pat typ_env current_pat pat with
             | Some substs ->
                 let pat' = List.fold_left subst_id_pat pat substs in
                 let guard' = (match guard with
@@ -1552,7 +1564,7 @@ let rewrite_guarded_clauses l cs =
         (match guard with
           | Some exp ->
               let else_exp =
-                if equiv_pats current_pat pat'
+                if equiv_pats typ_env current_pat pat'
                 then if_exp current_pat (c' :: cs)
                 else case_exp (pat_to_exp current_pat) (get_type_annot annot') (group (c' :: cs)) in
               fix_effsum_exp (E_aux (E_if (exp,body,else_exp), annot))
@@ -1563,7 +1575,7 @@ let rewrite_guarded_clauses l cs =
             "if_exp given empty list in rewrite_guarded_clauses")) in
   group cs
 
-let rewrite_exp_remove_bitvector_pat rewriters nmap (E_aux (exp,(l,annot)) as full_exp) =
+let rewrite_exp_remove_bitvector_pat typ_env rewriters nmap (E_aux (exp,(l,annot)) as full_exp) =
   let rewrap e = E_aux (e,(l,annot)) in
   let rewrite_rec = rewriters.rewrite_exp rewriters nmap in
   let rewrite_base = rewrite_exp rewriters nmap in
@@ -1574,7 +1586,7 @@ let rewrite_exp_remove_bitvector_pat rewriters nmap (E_aux (exp,(l,annot)) as fu
        let (pat',(guard,decls,_)) = remove_bitvector_pat pat in
        let body' = decls (rewrite_rec body) in
        (pat',guard,body',annot') in
-     let clauses = rewrite_guarded_clauses l (List.map clause ps) in
+     let clauses = rewrite_guarded_clauses typ_env l (List.map clause ps) in
      if (effectful e) then
        let e = rewrite_rec e in
        let (E_aux (_,(el,eannot))) = e in
@@ -1598,7 +1610,7 @@ let rewrite_exp_remove_bitvector_pat rewriters nmap (E_aux (exp,(l,annot)) as fu
   | _ -> rewrite_base full_exp
 
 let rewrite_fun_remove_bitvector_pat
-      rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) =
+      typ_env rewriters (FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))) =
   let _ = reset_fresh_name_counter () in
   (* TODO Can there be clauses with different id's in one FD_function? *)
   let funcls = match funcls with
@@ -1607,18 +1619,18 @@ let rewrite_fun_remove_bitvector_pat
           let (pat,(guard,decls,_)) = remove_bitvector_pat pat in
           let exp = decls (rewriters.rewrite_exp rewriters None exp) in
           (pat,guard,exp,annot) in
-        let cs = rewrite_guarded_clauses l (List.map clause funcls) in
+        let cs = rewrite_guarded_clauses typ_env l (List.map clause funcls) in
         List.map (fun (pat,exp,annot) -> FCL_aux (FCL_Funcl(id,pat,exp),annot)) cs
     | _ -> funcls (* TODO is the empty list possible here? *) in
   FD_aux (FD_function(recopt,tannotopt,effectopt,funcls),(l,fdannot))
 
-let rewrite_defs_remove_bitvector_pats (Defs defs) =
+let rewrite_defs_remove_bitvector_pats typ_env (Defs defs) =
   let rewriters =
-    {rewrite_exp = rewrite_exp_remove_bitvector_pat;
+    {rewrite_exp = rewrite_exp_remove_bitvector_pat typ_env;
      rewrite_pat = rewrite_pat;
      rewrite_let = rewrite_let;
      rewrite_lexp = rewrite_lexp;
-     rewrite_fun = rewrite_fun_remove_bitvector_pat;
+     rewrite_fun = rewrite_fun_remove_bitvector_pat typ_env;
      rewrite_def = rewrite_def;
      rewrite_defs = rewrite_defs_base } in
   let rewrite_def d =
@@ -2587,10 +2599,10 @@ let rewrite_defs_remove_e_assign =
     }
 
 
-let rewrite_defs_lem =
+let rewrite_defs_lem typ_env =
   top_sort_defs >>
   rewrite_defs_remove_vector_concat >>
-  rewrite_defs_remove_bitvector_pats >>
+  rewrite_defs_remove_bitvector_pats typ_env >>
   rewrite_defs_exp_lift_assign >> 
   rewrite_defs_remove_blocks >> 
   rewrite_defs_letbind_effects >> 
diff --git a/src/rewriter.mli b/src/rewriter.mli
index 615d0fa0..19ab4aca 100644
--- a/src/rewriter.mli
+++ b/src/rewriter.mli
@@ -61,7 +61,7 @@ type 'a rewriters = { rewrite_exp  : 'a rewriters -> (nexp_map * 'a namemap) opt
 val rewrite_exp : tannot rewriters -> (nexp_map * tannot namemap) option -> tannot exp -> tannot exp
 val rewrite_defs : tannot defs -> tannot defs
 val rewrite_defs_ocaml : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for ocaml out*)
-val rewrite_defs_lem : tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*)
+val rewrite_defs_lem : tannot emap -> tannot defs -> tannot defs (*Perform rewrites to exclude AST nodes not supported for lem out*)
 
 (* the type of interpretations of pattern-matching expressions *)
 type ('a,'pat,'pat_aux,'fpat,'fpat_aux) pat_alg =
@@ -153,4 +153,3 @@ val fold_exp : ('a,'exp,'exp_aux,'lexp,'lexp_aux,'fexp,'fexp_aux,'fexps,'fexps_a
       'pat,'pat_aux,'fpat,'fpat_aux) exp_alg -> 'a exp -> 'exp
 
 val id_pat_alg : ('a,'a pat, 'a pat_aux, 'a fpat, 'a fpat_aux) pat_alg
-
diff --git a/src/sail.ml b/src/sail.ml
index d84144e1..e7a2bd99 100644
--- a/src/sail.ml
+++ b/src/sail.ml
@@ -174,7 +174,7 @@ let main() =
          else output "" (Ocaml_out (Some (List.hd !opt_libs_ocaml))) [out_name,ast_ocaml]
        else ());
       (if !(opt_print_lem)
-       then let ast_lem = rewrite_ast_lem ast in
+       then let ast_lem = rewrite_ast_lem type_envs ast in
          if !(opt_libs_lem) = []
          then output "" (Lem_out None) [out_name,ast_lem]
          else output "" (Lem_out (Some (List.hd !opt_libs_lem))) [out_name,ast_lem]