diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/monomorphise.ml | 9 | ||||
| -rw-r--r-- | src/pretty_print_coq.ml | 9 | ||||
| -rw-r--r-- | src/pretty_print_lem.ml | 8 |
3 files changed, 19 insertions, 7 deletions
diff --git a/src/monomorphise.ml b/src/monomorphise.ml index 2723d143..aaf1672a 100644 --- a/src/monomorphise.ml +++ b/src/monomorphise.ml @@ -575,6 +575,7 @@ let nexp_subst_fns substs = | P_record (fps,flag) -> re (P_record (List.map s_fpat fps, flag)) | P_vector ps -> re (P_vector (List.map s_pat ps)) | P_vector_concat ps -> re (P_vector_concat (List.map s_pat ps)) + | P_string_append ps -> re (P_string_append (List.map s_pat ps)) | P_tup ps -> re (P_tup (List.map s_pat ps)) | P_list ps -> re (P_list (List.map s_pat ps)) | P_cons (p1,p2) -> re (P_cons (s_pat p1, s_pat p2)) @@ -671,6 +672,7 @@ let bindings_from_pat p = | P_var (p,kid) -> aux_pat p | P_vector ps | P_vector_concat ps + | P_string_append ps | P_app (_,ps) | P_tup ps | P_list ps @@ -1023,6 +1025,9 @@ let rec freshen_pat_bindings p = | P_vector_concat ps -> let ps,vs = List.split (List.map aux ps) in mkp (P_vector_concat ps),List.concat vs + | P_string_append ps -> + let ps,vs = List.split (List.map aux ps) in + mkp (P_string_append ps),List.concat vs | P_tup ps -> let ps,vs = List.split (List.map aux ps) in mkp (P_tup ps),List.concat vs @@ -1865,6 +1870,8 @@ let split_defs all_errors splits defs = relist spl (fun ps -> P_vector ps) ps | P_vector_concat ps -> relist spl (fun ps -> P_vector_concat ps) ps + | P_string_append ps -> + relist spl (fun ps -> P_string_append ps) ps | P_tup ps -> relist spl (fun ps -> P_tup ps) ps | P_list ps -> @@ -2108,6 +2115,7 @@ let split_defs all_errors splits defs = | DEF_internal_mutrec _ -> [d] | DEF_fundef fd -> [DEF_fundef (map_fundef fd)] + | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "mappings should be gone by now" | DEF_val lb -> [DEF_val (map_letbind lb)] | DEF_scattered sd -> List.map (fun x -> DEF_scattered x) (map_scattered_def sd) in @@ -3350,6 +3358,7 @@ let initial_env fn_id fn_l (TypQ_aux (tq,_)) pat body set_assertions = | P_record (fpats,_) -> of_list (List.map (fun (FP_aux (FP_Fpat (_,p),_)) -> p) fpats) | P_vector pats | P_vector_concat pats + | P_string_append pats | P_tup pats | P_list pats -> of_list pats diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index adfb378a..74f5adb8 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -397,7 +397,7 @@ let maybe_expand_range_type (Typ_aux (typ,l) as full_typ) = let kid = mk_kid "n" in let var = nvar kid in Some (Typ_aux (Typ_exist ([kid], nc_gteq var (nconstant Nat_big_num.zero), atom_typ var), - Generated l)) + Parse_ast.Generated l)) | _ -> None let expand_range_type typ = Util.option_default typ (maybe_expand_range_type typ) @@ -725,7 +725,8 @@ let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) = | _ -> raise (Reporting_basic.err_unreachable l __POS__ "list pattern not a list") in doc_op (string "::") (doc_pat ctxt true (p, el_typ)) (doc_pat ctxt true (p', typ)) - | P_record (_,_) -> empty (* TODO *) + | P_string_append _ -> unreachable l __POS__ "Coq doesn't support string append patterns" + | P_not _ -> unreachable l __POS__ "Coq doesn't support not patterns" let contains_early_return exp = let e_app (f, args) = @@ -823,7 +824,7 @@ let replace_atom_return_type ret_typ = match ret_typ with | Typ_aux (Typ_app (Id_aux (Id "atom",_), [Typ_arg_aux (Typ_arg_nexp nexp,_)]),l) -> let kid = mk_kid "_retval" in (* TODO: collision avoidance *) - true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Generated l) + true, Typ_aux (Typ_exist ([kid], nc_eq (nvar kid) nexp, atom_typ (nvar kid)),Parse_ast.Generated l) | _ -> false, ret_typ let is_range_from_atom env (Typ_aux (argty,_)) (Typ_aux (fnty,_)) = @@ -2014,7 +2015,7 @@ let rec doc_def unimplemented def = | DEF_internal_mutrec fundefs -> doc_mutrec_lem fundefs ^/^ hardline | DEF_val (LB_aux (LB_val (pat, exp), _)) -> doc_val pat exp | DEF_scattered sdef -> failwith "doc_def: shoulnd't have DEF_scattered at this point" - + | DEF_mapdef (MD_aux (_, (l,_))) -> unreachable l __POS__ "Coq doesn't support mappings" | DEF_kind _ -> empty let find_exc_typ defs = diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 70db46b8..578a770a 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -421,8 +421,7 @@ let doc_quant_item vars_included (QI_aux (qi, _)) = match qi with None -> doc_var kid | Some set -> (*when KidSet.mem kid set -> doc_var kid*) let nexps = NexpSet.filter (fun nexp -> KidSet.mem (orig_kid kid) (nexp_frees nexp)) set in - separate_map space doc_nexp_lem (NexpSet.elements nexps) - | _ -> empty) + separate_map space doc_nexp_lem (NexpSet.elements nexps)) | _ -> empty let doc_typquant_items_lem vars_included (TypQ_aux(tq,_)) = match tq with @@ -525,7 +524,8 @@ let rec doc_pat_lem ctxt apat_needed (P_aux (p,(l,annot)) as pa) = match p with | _ -> parens (separate_map comma_sp (doc_pat_lem ctxt false) pats)) | P_list pats -> brackets (separate_map semi (doc_pat_lem ctxt false) pats) (*Never seen but easy in lem*) | P_cons (p,p') -> doc_op (string "::") (doc_pat_lem ctxt true p) (doc_pat_lem ctxt true p') - | P_record (_,_) -> empty (* TODO *) + | P_string_append _ -> unreachable l __POS__ "Lem doesn't support string append patterns" + | P_not _ -> unreachable l __POS__ "Lem doesn't support not patterns" let rec typ_needs_printed (Typ_aux (t,_) as typ) = match t with | Typ_tup ts -> List.exists typ_needs_printed ts @@ -1269,6 +1269,7 @@ let doc_rec_lem force_rec (Rec_aux(r,_)) = match r with let doc_tannot_opt_lem (Typ_annot_opt_aux(t,_)) = match t with | Typ_annot_opt_some(tq,typ) -> (*doc_typquant_lem tq*) (doc_typ_lem typ) + | Typ_annot_opt_none -> empty let doc_fun_body_lem ctxt exp = let doc_exp = doc_exp_lem ctxt false exp in @@ -1417,6 +1418,7 @@ let rec doc_def_lem def = | DEF_scattered sdef -> failwith "doc_def_lem: shoulnd't have DEF_scattered at this point" | DEF_kind _ -> empty + | DEF_mapdef (MD_aux (_, (l, _))) -> unreachable l __POS__ "Lem doesn't support mappings" let find_exc_typ defs = let is_exc_typ_def = function |