From 7cdbee76d454047271ef6cdaa82a2b7e2ed590ba Mon Sep 17 00:00:00 2001 From: Brian Campbell Date: Thu, 7 Jun 2018 18:00:59 +0100 Subject: Coq: add destructuring of atom existentials in patterns Plus test case, broken builtin name --- lib/vector_dec.sail | 2 +- src/pretty_print_coq.ml | 124 +++++++++++++++++++++++++++++++--------------- test/coq/pass/exatom.sail | 9 ++++ test/coq/run_tests.sh | 37 ++++++++------ 4 files changed, 115 insertions(+), 57 deletions(-) create mode 100644 test/coq/pass/exatom.sail diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail index 60f49af8..d9b80b32 100644 --- a/lib/vector_dec.sail +++ b/lib/vector_dec.sail @@ -122,7 +122,7 @@ val unsigned = { lem: "uint", interpreter: "uint", c: "sail_uint", - coq: "uint" + coq: "unsigned" } : forall 'n. bits('n) -> range(0, 2 ^ 'n - 1) val signed = "sint" : forall 'n. bits('n) -> range(- (2 ^ ('n - 1)), 2 ^ ('n - 1) - 1) diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 53571655..b3d48447 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -555,40 +555,80 @@ let is_ctor env id = match Env.lookup_id id env with | Enum _ -> true | _ -> false +let is_auto_decomposed_exist env typ = + match destruct_exist env typ with + | Some (kids, nc, (Typ_aux (Typ_app (id, _),_) as typ')) when string_of_id id = "atom" -> Some typ' + | _ -> None + (*Note: vector concatenation, literal vectors, indexed vectors, and record should be removed prior to pp. The latter two have never yet been seen *) -let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot))) = match p with - (* Special case translation of the None constructor to remove the unit arg *) - | P_app(id, _) when string_of_id id = "None" -> string "None" - | P_app(id, ((_ :: _) as pats)) -> - let ppp = doc_unop (doc_id_ctor id) - (parens (separate_map comma (doc_pat ctxt true) pats)) in - if apat_needed then parens ppp else ppp - | P_app(id, []) -> doc_id_ctor id - | P_lit lit -> doc_lit lit - | P_wild -> underscore - | P_id id -> doc_id id - | P_var(p,_) -> doc_pat ctxt true p - | P_as(p,id) -> parens (separate space [doc_pat ctxt true p; string "as"; doc_id id]) - | P_typ(typ,p) -> - let doc_p = doc_pat ctxt true p in - doc_p - (* Type annotations aren't allowed everywhere in patterns in Coq *) - (*parens (doc_op colon doc_p (doc_typ typ))*) - | P_vector pats -> - let ppp = brackets (separate_map semi (doc_pat ctxt true) pats) in - if apat_needed then parens ppp else ppp - | P_vector_concat pats -> - raise (Reporting_basic.err_unreachable l - "vector concatenation patterns should have been removed before pretty-printing") - | P_tup pats -> - (match pats with - | [p] -> doc_pat ctxt apat_needed p - | _ -> parens (separate_map comma_sp (doc_pat ctxt false) pats)) - | P_list pats -> brackets (separate_map semi (doc_pat ctxt false) pats) - | P_cons (p,p') -> doc_op (string "::") (doc_pat ctxt true p) (doc_pat ctxt true p') - | P_record (_,_) -> empty (* TODO *) +let rec doc_pat ctxt apat_needed (P_aux (p,(l,annot)) as pat, typ) = + let env = env_of_annot (l,annot) in + let typ = Env.expand_synonyms env typ in + match is_auto_decomposed_exist env typ with + | Some typ' -> + let pat_pp = doc_pat ctxt true (pat, typ') in + let pat_pp = separate space [string "existT"; underscore; pat_pp; underscore] in + if apat_needed then parens pat_pp else pat_pp + | None -> + match p with + (* Special case translation of the None constructor to remove the unit arg *) + | P_app(id, _) when string_of_id id = "None" -> string "None" + | P_app(id, ((_ :: _) as pats)) -> + let ppp = doc_unop (doc_id_ctor id) + (* TODO: we shouldn't use pat_typ_of here, + we should either get the type checker to put the full type in the + annotation (including all existentials), or provide some other way to + retrieve the full types for the args from typ. *) + (parens (separate_map comma (fun p -> doc_pat ctxt true (p, pat_typ_of p)) pats)) in + if apat_needed then parens ppp else ppp + | P_app(id, []) -> doc_id_ctor id + | P_lit lit -> doc_lit lit + | P_wild -> underscore + | P_id id -> doc_id id + | P_var(p,_) -> doc_pat ctxt true (p, typ) + | P_as(p,id) -> parens (separate space [doc_pat ctxt true (p, typ); string "as"; doc_id id]) + | P_typ(ptyp,p) -> + let doc_p = doc_pat ctxt true (p, ptyp) in + doc_p + (* Type annotations aren't allowed everywhere in patterns in Coq *) + (*parens (doc_op colon doc_p (doc_typ typ))*) + | P_vector pats -> + let el_typ = + match destruct_vector env typ with + | Some (_,_,t) -> t + | None -> failwith "vector pattern doesn't have vector type" + in + let ppp = brackets (separate_map semi (fun p -> doc_pat ctxt true (p,el_typ)) pats) in + if apat_needed then parens ppp else ppp + | P_vector_concat pats -> + raise (Reporting_basic.err_unreachable l + "vector concatenation patterns should have been removed before pretty-printing") + | P_tup pats -> + let typs = match typ with + | Typ_aux (Typ_tup typs, _) -> typs + | _ -> failwith "tuple pattern doesn't have tuple type" + in + (match pats, typs with + | [p], [typ'] -> doc_pat ctxt apat_needed (p, typ') + | [_], _ -> failwith "tuple pattern length does not match tuple type length" + | _ -> parens (separate_map comma_sp (doc_pat ctxt false) (List.combine pats typs))) + | P_list pats -> + let el_typ = match typ with + | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_) + when Id.compare f (mk_id "list") = 0 -> el_typ + | _ -> failwith "list pattern not a list" + in + brackets (separate_map semi (fun p -> doc_pat ctxt false (p, el_typ)) pats) + | P_cons (p,p') -> + let el_typ = match typ with + | Typ_aux (Typ_app (f, [Typ_arg_aux (Typ_arg_typ el_typ,_)]),_) + when Id.compare f (mk_id "list") = 0 -> el_typ + | _ -> failwith "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 *) let contains_early_return exp = let e_app (f, args) = @@ -941,7 +981,7 @@ let doc_exp_lem, doc_let_lem = let only_integers e = expY e in let epp = group ((separate space [string "match"; only_integers e; string "with"]) ^/^ - (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt (typ_of e)) pexps) ^/^ (string "end")) in if aexp_needed then parens (align epp) else align epp | E_try (e, pexps) -> @@ -949,7 +989,7 @@ let doc_exp_lem, doc_let_lem = let try_catch = if ctxt.early_ret then "try_catchR" else "try_catch" in let epp = group ((separate space [string try_catch; expY e; string "(function "]) ^/^ - (separate_map (break 1) (doc_case ctxt) pexps) ^/^ + (separate_map (break 1) (doc_case ctxt exc_typ) pexps) ^/^ (string "end)")) in if aexp_needed then parens (align epp) else align epp else @@ -979,10 +1019,10 @@ let doc_exp_lem, doc_let_lem = tuple patterns to Isabelle *) separate space [string ">>= fun varstup => let"; - doc_pat ctxt true pat; + doc_pat ctxt true (pat, typ_of e1); string "= varstup in"] | _ -> - separate space [string ">>= fun"; doc_pat ctxt true pat; bigarrow] + separate space [string ">>= fun"; doc_pat ctxt true (pat, typ_of e1); bigarrow] in infix 0 1 middle (expV b e1) (expN e2) in @@ -1037,7 +1077,7 @@ let doc_exp_lem, doc_let_lem = (top_exp ctxt false e) | LB_val(pat,e) -> prefix 2 1 - (separate space [string "let"; squote ^^ doc_pat ctxt true pat; coloneq]) + (separate space [string "let"; squote ^^ doc_pat ctxt true (pat, typ_of e); coloneq]) (top_exp ctxt false e) and doc_fexp ctxt recordtyp (FE_aux(FE_Fexp(id,e),_)) = @@ -1047,9 +1087,9 @@ let doc_exp_lem, doc_let_lem = else doc_id id in group (doc_op coloneq fname (top_exp ctxt true e)) - and doc_case ctxt = function + and doc_case ctxt typ = function | Pat_aux(Pat_exp(pat,e),_) -> - group (prefix 3 1 (separate space [pipe; doc_pat ctxt false pat;bigarrow]) + group (prefix 3 1 (separate space [pipe; doc_pat ctxt false (pat,typ);bigarrow]) (group (top_exp ctxt false e))) | Pat_aux(Pat_when(_,_,_),(l,_)) -> raise (Reporting_basic.err_unreachable l @@ -1323,12 +1363,14 @@ let merge_kids_atoms pats = let gone,map,_ = List.fold_left try_eliminate (KidSet.empty, KBindings.empty, KidSet.empty) pats in gone,map -let doc_binder ctxt (P_aux (p,_) as pat, typ) = +let doc_binder ctxt (P_aux (p,ann) as pat, typ) = + let env = env_of_annot ann in + let exp_typ = Env.expand_synonyms env typ in match p with | P_id id - | P_typ (_,P_aux (P_id id,_)) -> + | P_typ (_,P_aux (P_id id,_)) when Util.is_none (is_auto_decomposed_exist env exp_typ) -> parens (separate space [doc_id id; colon; doc_typ ctxt typ]) - | _ -> squote ^^ parens (separate space [doc_pat ctxt true pat; colon; doc_typ ctxt typ]) + | _ -> squote ^^ parens (separate space [doc_pat ctxt true (pat, exp_typ); colon; doc_typ ctxt typ]) let doc_funcl (FCL_aux(FCL_Funcl(id, pexp), annot)) = let (tq,typ) = Env.get_val_spec_orig id (env_of_annot annot) in diff --git a/test/coq/pass/exatom.sail b/test/coq/pass/exatom.sail new file mode 100644 index 00000000..db162536 --- /dev/null +++ b/test/coq/pass/exatom.sail @@ -0,0 +1,9 @@ +$include + +val f : forall 'n, 'n in {8,16}. atom('n) -> atom('n) + +val make : unit -> {'n, 'n in {8,16}. atom('n)} + +val test : {'n, 'n in {8,16}. atom('n)} -> int + +function test(v) = f(v) diff --git a/test/coq/run_tests.sh b/test/coq/run_tests.sh index f782ed80..2be5e535 100755 --- a/test/coq/run_tests.sh +++ b/test/coq/run_tests.sh @@ -3,7 +3,8 @@ set -e DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" SAILDIR="$DIR/../.." -TESTSDIR="$DIR/../typecheck/pass" +TYPECHECKTESTSDIR="$DIR/../typecheck/pass" +EXTRATESTSDIR="$DIR/pass" BBVDIR="$DIR/../../../bbv" RED='\033[0;31m' @@ -49,20 +50,26 @@ printf "\n" >> $DIR/tests.xml cd $DIR -for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`; -do - if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null; - then - if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null; - then - green "tested $i expecting pass" "pass" - else - yellow "tested $i expecting pass" "failed to typecheck generated Coq" - fi - else - red "tested $i expecting pass" "failed to generate Coq" - fi -done +function check_tests_dir { + TESTSDIR="$1" + for i in `ls $TESTSDIR/ | grep sail | grep -vf "$DIR/skip"`; + do + if $SAILDIR/sail -coq -dcoq_undef_axioms -o out $TESTSDIR/$i &>/dev/null; + then + if coqc -R "$BBVDIR" bbv -R "$SAILDIR/lib/coq" Sail out_types.v out.v &>/dev/null; + then + green "tested $i expecting pass" "pass" + else + yellow "tested $i expecting pass" "failed to typecheck generated Coq" + fi + else + red "tested $i expecting pass" "failed to generate Coq" + fi + done +} + +check_tests_dir "$TYPECHECKTESTSDIR" +check_tests_dir "$EXTRATESTSDIR" finish_suite "Coq tests" -- cgit v1.2.3