(************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* *) module Gram = Pcoq.Gram module Constr = Pcoq.Constr module Tactic = Pcoq.Tactic module Programs = struct let gec s = Gram.Entry.create ("Programs."^s) (* types *) let type_v = gec "type_v" let type_v0 = gec "type_v0" let type_v1 = gec "type_v1" let type_v2 = gec "type_v2" let type_v3 = gec "type_v3" let type_v_app = gec "type_v_app" let type_c = gec "type_c" let effects = gec "effects" let reads = gec "reads" let writes = gec "writes" let pre_condition = gec "pre_condition" let post_condition = gec "post_condition" (* binders *) let binder = gec "binder" let binder_type = gec "binder_type" let binders = gec "binders" (* programs *) let program = gec "program" let prog1 = gec "prog1" let prog2 = gec "prog2" let prog3 = gec "prog3" let prog4 = gec "prog4" let prog5 = gec "prog5" let prog6 = gec "prog6" let prog7 = gec "prog7" let ast1 = gec "ast1" let ast2 = gec "ast2" let ast3 = gec "ast3" let ast4 = gec "ast4" let ast5 = gec "ast5" let ast6 = gec "ast6" let ast7 = gec "ast7" let arg = gec "arg" let block = gec "block" let block_statement = gec "block_statement" let relation = gec "relation" let variable = gec "variable" let invariant = gec "invariant" let variant = gec "variant" let assertion = gec "assertion" let precondition = gec "precondition" let postcondition = gec "postcondition" let predicate = gec "predicate" let name = gec "name" end open Programs let ast_of_int n = CDelimiters (dummy_loc, "Z", CNumeral (dummy_loc, Bignat.POS (Bignat.of_string n))) let constr_of_int n = Constrintern.interp_constr Evd.empty (Global.env ()) (ast_of_int n) open Util open Coqast let mk_id loc id = mkRefC (Ident (loc, id)) let mk_ref loc s = mk_id loc (Constrextern.id_of_v7_string s) let mk_appl loc1 loc2 f args = CApp (join_loc loc1 loc2, (None,mk_ref loc1 f), List.map (fun a -> a,None) args) let conj_assert {a_name=n;a_value=a} {a_value=b} = let loc1 = constr_loc a in let loc2 = constr_loc a in { a_value = mk_appl loc1 loc2 "and" [a;b]; a_name = n } let conj = function None,None -> None | None,b -> b | a,None -> a | Some a,Some b -> Some (conj_assert a b) let without_effect loc d = { desc = d; pre = []; post = None; loc = loc; info = () } let isevar = Expression isevar let bin_op op loc e1 e2 = without_effect loc (Apply (without_effect loc (Expression (constant op)), [ Term e1; Term e2 ])) let un_op op loc e = without_effect loc (Apply (without_effect loc (Expression (constant op)), [Term e])) let bool_bin op loc a1 a2 = let w = without_effect loc in let d = SApp ( [Variable op], [a1; a2]) in w d let bool_or loc = bool_bin connective_or loc let bool_and loc = bool_bin connective_and loc let bool_not loc a = let w = without_effect loc in let d = SApp ( [Variable connective_not ], [a]) in w d let ast_zwf_zero loc = mk_appl loc loc "Zwf" [mk_ref loc "Z0"] (* program -> Coq AST *) let bdize c = let env = Global.env_of_context (Pcicenv.cci_sign_of Prename.empty_ren Penv.empty) in Constrextern.extern_constr true env c let rec coqast_of_program loc = function | Variable id -> mk_id loc id | Acc id -> mk_id loc id | Apply (f,l) -> let f = coqast_of_program f.loc f.desc in let args = List.map (function Term t -> (coqast_of_program t.loc t.desc,None) | _ -> invalid_arg "coqast_of_program") l in CApp (dummy_loc, (None,f), args) | Expression c -> bdize c | _ -> invalid_arg "coqast_of_program" (* The construction `for' is syntactic sugar. * * for i = v1 to v2 do { invariant Inv } block done * * ==> (let rec f i { variant v2+1-i } = * { i <= v2+1 /\ Inv(i) } * (if i > v2 then tt else begin block; (f (i+1)) end) * { Inv(v2+1) } * in (f v1)) { Inv(v2+1) } *) let ast_plus_un loc ast = let un = ast_of_int "1" in mk_appl loc loc "Zplus" [ast;un] let make_ast_for loc i v1 v2 inv block = let f = for_name() in let id_i = id_of_string i in let var_i = without_effect loc (Variable id_i) in let var_f = without_effect loc (Variable f) in let succ_v2 = let a_v2 = coqast_of_program v2.loc v2.desc in ast_plus_un loc a_v2 in let post = named_app (subst_ast_in_ast [ id_i, succ_v2 ]) inv in let e1 = let test = bin_op "Z_gt_le_bool" loc var_i v2 in let br_t = without_effect loc (Expression (constant "tt")) in let br_f = let un = without_effect loc (Expression (constr_of_int "1")) in let succ_i = bin_op "Zplus" loc var_i un in let f_succ_i = without_effect loc (Apply (var_f, [Term succ_i])) in without_effect loc (Seq (block @ [Statement f_succ_i])) in let inv' = let i_le_sv2 = mk_appl loc loc "Zle" [mk_ref loc i; succ_v2] in conj_assert {a_value=i_le_sv2;a_name=inv.a_name} inv in { desc = If(test,br_t,br_f); loc = loc; pre = [pre_of_assert false inv']; post = Some post; info = () } in let bl = let typez = mk_ref loc "Z" in [(id_of_string i, BindType (TypePure typez))] in let fv1 = without_effect loc (Apply (var_f, [Term v1])) in let v = TypePure (mk_ref loc "unit") in let var = let a = mk_appl loc loc "Zminus" [succ_v2;mk_ref loc i] in (a, ast_zwf_zero loc) in Let (f, without_effect loc (LetRec (f,bl,v,var,e1)), fv1) let mk_prog loc p pre post = { desc = p.desc; pre = p.pre @ pre; post = conj (p.post,post); loc = loc; info = () } if !Options.v7 then GEXTEND Gram (* Types ******************************************************************) type_v: [ [ t = type_v0 -> t ] ] ; type_v0: [ [ t = type_v1 -> t ] ] ; type_v1: [ [ t = type_v2 -> t ] ] ; type_v2: [ LEFTA [ v = type_v2; IDENT "ref" -> Ref v | t = type_v3 -> t ] ] ; type_v3: [ [ IDENT "array"; size = Constr.constr; "of"; v = type_v0 -> Array (size,v) | IDENT "fun"; bl = binders; c = type_c -> make_arrow bl c | c = Constr.constr -> TypePure c ] ] ; type_c: [ [ IDENT "returns"; id = IDENT; ":"; v = type_v; e = effects; p = OPT pre_condition; q = OPT post_condition; "end" -> ((id_of_string id, v), e, list_of_some p, q) ] ] ; effects: [ [ r = OPT reads; w = OPT writes -> let r' = match r with Some l -> l | _ -> [] in let w' = match w with Some l -> l | _ -> [] in List.fold_left (fun e x -> Peffect.add_write x e) (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r') w' ] ] ; reads: [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ] ; writes: [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ] ; pre_condition: [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ] ; post_condition: [ [ IDENT "post"; c = predicate -> c ] ] ; (* Binders (for both types and programs) **********************************) binder: [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" -> List.map (fun s -> (id_of_string s, t)) sl ] ] ; binder_type: [ [ "Set" -> BindSet | v = type_v -> BindType v ] ] ; binders: [ [ bl = LIST0 binder -> List.flatten bl ] ] ; (* annotations *) predicate: [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ] ; name: [ [ "as"; s = IDENT -> Name (id_of_string s) | -> Anonymous ] ] ; (* Programs ***************************************************************) variable: [ [ s = IDENT -> id_of_string s ] ] ; assertion: [ [ "{"; c = predicate; "}" -> c ] ] ; precondition: [ [ "{"; c = predicate; "}" -> pre_of_assert false c ] ] ; postcondition: [ [ "{"; c = predicate; "}" -> c ] ] ; program: [ [ p = prog1 -> p ] ] ; prog1: [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog2: [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog3: [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog4: [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog5: [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog6: [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; ast1: [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y | x = prog2 -> x ] ] ; ast2: [ [ IDENT "not"; x = prog3 -> bool_not loc x | x = prog3 -> x ] ] ; ast3: [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y | x = prog4 -> x ] ] ; ast4: [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y | x = prog5 -> x ] ] ; ast5: [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y | x = prog6 -> x ] ] ; ast6: [ [ "-"; x = prog6 -> un_op "Zopp" loc x | x = ast7 -> without_effect loc x ] ] ; ast7: [ [ v = variable -> Variable v | n = INT -> Expression (constr_of_int n) | "!"; v = variable -> Acc v | "?" -> isevar | v = variable; ":="; p = program -> Aff (v,p) | v = variable; "["; e = program; "]" -> TabAcc (true,v,e) | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e) | v = variable; "["; e = program; "]"; ":="; p = program -> TabAff (true,v,e,p) | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> TabAff (true,v,e,p) | IDENT "if"; e1 = program; IDENT "then"; e2 = program; IDENT "else"; e3 = program -> If (e1,e2,e3) | IDENT "if"; e1 = program; IDENT "then"; e2 = program -> If (e1,e2,without_effect loc (Expression (constant "tt"))) | IDENT "while"; b = program; IDENT "do"; "{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}"; bl = block; IDENT "done" -> While (b, inv, wf, bl) | IDENT "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program; IDENT "do"; "{"; inv = invariant; "}"; bl = block; IDENT "done" -> make_ast_for loc i v1 v2 inv bl | IDENT "let"; v = variable; "="; IDENT "ref"; p1 = program; "in"; p2 = program -> LetRef (v, p1, p2) | IDENT "let"; v = variable; "="; p1 = program; "in"; p2 = program -> Let (v, p1, p2) | IDENT "begin"; b = block; "end" -> Seq b | IDENT "fun"; bl = binders; "->"; p = program -> Lam (bl,p) | IDENT "let"; IDENT "rec"; f = variable; bl = binders; ":"; v = type_v; "{"; IDENT "variant"; var = variant; "}"; "="; p = program -> LetRec (f,bl,v,var,p) | IDENT "let"; IDENT "rec"; f = variable; bl = binders; ":"; v = type_v; "{"; IDENT "variant"; var = variant; "}"; "="; p = program; "in"; p2 = program -> Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2) | "@"; s = STRING; p = program -> Debug (s,p) | "("; p = program; args = LIST0 arg; ")" -> match args with [] -> if p.pre<>[] or p.post<>None then Pp.warning "Some annotations are lost"; p.desc | _ -> Apply(p,args) ] ] ; arg: [ [ "'"; t = type_v -> Type t | p = program -> Term p ] ] ; block: [ [ s = block_statement; ";"; b = block -> s::b | s = block_statement -> [s] ] ] ; block_statement: [ [ IDENT "label"; s = IDENT -> Label s | IDENT "assert"; c = assertion -> Assert c | p = program -> Statement p ] ] ; relation: [ [ "<" -> "Z_lt_ge_bool" | "<=" -> "Z_le_gt_bool" | ">" -> "Z_gt_le_bool" | ">=" -> "Z_ge_lt_bool" | "=" -> "Z_eq_bool" | "<>" -> "Z_noteq_bool" ] ] ; (* Other entries (invariants, etc.) ***************************************) invariant: [ [ IDENT "invariant"; c = predicate -> c ] ] ; variant: [ [ c = Constr.constr; IDENT "for"; r = Constr.constr -> (c, r) | c = Constr.constr -> (c, ast_zwf_zero loc) ] ] ; END else GEXTEND Gram GLOBAL: type_v program; (* Types ******************************************************************) type_v: [ [ t = type_v0 -> t ] ] ; type_v0: [ [ t = type_v1 -> t ] ] ; type_v1: [ [ t = type_v2 -> t ] ] ; type_v2: [ LEFTA [ v = type_v2; IDENT "ref" -> Ref v | t = type_v3 -> t ] ] ; type_v3: [ [ IDENT "array"; size = Constr.constr; IDENT "of"; v = type_v0 -> Array (size,v) | "fun"; bl = binders; c = type_c -> make_arrow bl c | c = Constr.constr -> TypePure c ] ] ; type_c: [ [ IDENT "returns"; id = IDENT; ":"; v = type_v; e = effects; p = OPT pre_condition; q = OPT post_condition; "end" -> ((id_of_string id, v), e, list_of_some p, q) ] ] ; effects: [ [ r = OPT reads; w = OPT writes -> let r' = match r with Some l -> l | _ -> [] in let w' = match w with Some l -> l | _ -> [] in List.fold_left (fun e x -> Peffect.add_write x e) (List.fold_left (fun e x -> Peffect.add_read x e) Peffect.bottom r') w' ] ] ; reads: [ [ IDENT "reads"; l = LIST0 IDENT SEP "," -> List.map id_of_string l ] ] ; writes: [ [ IDENT "writes"; l=LIST0 IDENT SEP "," -> List.map id_of_string l ] ] ; pre_condition: [ [ IDENT "pre"; c = predicate -> pre_of_assert false c ] ] ; post_condition: [ [ IDENT "post"; c = predicate -> c ] ] ; (* Binders (for both types and programs) **********************************) binder: [ [ "("; sl = LIST1 IDENT SEP ","; ":"; t = binder_type ; ")" -> List.map (fun s -> (id_of_string s, t)) sl ] ] ; binder_type: [ [ "Set" -> BindSet | v = type_v -> BindType v ] ] ; binders: [ [ bl = LIST0 binder -> List.flatten bl ] ] ; (* annotations *) predicate: [ [ c = Constr.constr; n = name -> { a_name = n; a_value = c } ] ] ; dpredicate: [ [ c = Constr.lconstr; n = name -> { a_name = n; a_value = c } ] ] ; name: [ [ "as"; s = IDENT -> Name (id_of_string s) | -> Anonymous ] ] ; (* Programs ***************************************************************) variable: [ [ s = IDENT -> id_of_string s ] ] ; assertion: [ [ "{"; c = dpredicate; "}" -> c ] ] ; precondition: [ [ "{"; c = dpredicate; "}" -> pre_of_assert false c ] ] ; postcondition: [ [ "{"; c = dpredicate; "}" -> c ] ] ; program: [ [ p = prog1 -> p ] ] ; prog1: [ [ pre = LIST0 precondition; ast = ast1; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog2: [ [ pre = LIST0 precondition; ast = ast2; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog3: [ [ pre = LIST0 precondition; ast = ast3; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog4: [ [ pre = LIST0 precondition; ast = ast4; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog5: [ [ pre = LIST0 precondition; ast = ast5; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; prog6: [ [ pre = LIST0 precondition; ast = ast6; post = OPT postcondition -> mk_prog loc ast pre post ] ] ; ast1: [ [ x = prog2; IDENT "or"; y = prog1 -> bool_or loc x y | x = prog2; IDENT "and"; y = prog1 -> bool_and loc x y | x = prog2 -> x ] ] ; ast2: [ [ IDENT "not"; x = prog3 -> bool_not loc x | x = prog3 -> x ] ] ; ast3: [ [ x = prog4; rel = relation; y = prog4 -> bin_op rel loc x y | x = prog4 -> x ] ] ; ast4: [ [ x = prog5; "+"; y = prog4 -> bin_op "Zplus" loc x y | x = prog5; "-"; y = prog4 -> bin_op "Zminus" loc x y | x = prog5 -> x ] ] ; ast5: [ [ x = prog6; "*"; y = prog5 -> bin_op "Zmult" loc x y | x = prog6 -> x ] ] ; ast6: [ [ "-"; x = prog6 -> un_op "Zopp" loc x | x = ast7 -> without_effect loc x ] ] ; ast7: [ [ v = variable -> Variable v | n = INT -> Expression (constr_of_int n) | "!"; v = variable -> Acc v | "?" -> isevar | v = variable; ":="; p = program -> Aff (v,p) | v = variable; "["; e = program; "]" -> TabAcc (true,v,e) | v = variable; "#"; "["; e = program; "]" -> TabAcc (true,v,e) | v = variable; "["; e = program; "]"; ":="; p = program -> TabAff (true,v,e,p) | v = variable; "#"; "["; e = program; "]"; ":="; p = program -> TabAff (true,v,e,p) | "if"; e1 = program; "then"; e2 = program; "else"; e3 = program -> If (e1,e2,e3) | "if"; e1 = program; "then"; e2 = program -> If (e1,e2,without_effect loc (Expression (constant "tt"))) | IDENT "while"; b = program; IDENT "do"; "{"; inv = OPT invariant; IDENT "variant"; wf = variant; "}"; bl = block; IDENT "done" -> While (b, inv, wf, bl) | "for"; i = IDENT; "="; v1 = program; IDENT "to"; v2 = program; IDENT "do"; "{"; inv = invariant; "}"; bl = block; IDENT "done" -> make_ast_for loc i v1 v2 inv bl | "let"; v = variable; "="; IDENT "ref"; p1 = program; "in"; p2 = program -> LetRef (v, p1, p2) | "let"; v = variable; "="; p1 = program; "in"; p2 = program -> Let (v, p1, p2) | IDENT "begin"; b = block; "end" -> Seq b | "fun"; bl = binders; "=>"; p = program -> Lam (bl,p) | "let"; IDENT "rec"; f = variable; bl = binders; ":"; v = type_v; "{"; IDENT "variant"; var = variant; "}"; "="; p = program -> LetRec (f,bl,v,var,p) | "let"; IDENT "rec"; f = variable; bl = binders; ":"; v = type_v; "{"; IDENT "variant"; var = variant; "}"; "="; p = program; "in"; p2 = program -> Let (f, without_effect loc (LetRec (f,bl,v,var,p)), p2) | "@"; s = STRING; p = program -> Debug (s,p) | "("; p = program; args = LIST0 arg; ")" -> match args with [] -> if p.pre<>[] or p.post<>None then Pp.warning "Some annotations are lost"; p.desc | _ -> Apply(p,args) ] ] ; arg: [ [ "'"; t = type_v -> Type t | p = program -> Term p ] ] ; block: [ [ s = block_statement; ";"; b = block -> s::b | s = block_statement -> [s] ] ] ; block_statement: [ [ IDENT "label"; s = IDENT -> Label s | IDENT "assert"; c = assertion -> Assert c | p = program -> Statement p ] ] ; relation: [ [ "<" -> "Z_lt_ge_bool" | "<=" -> "Z_le_gt_bool" | ">" -> "Z_gt_le_bool" | ">=" -> "Z_ge_lt_bool" | "=" -> "Z_eq_bool" | "<>" -> "Z_noteq_bool" ] ] ; (* Other entries (invariants, etc.) ***************************************) invariant: [ [ IDENT "invariant"; c = predicate -> c ] ] ; variant: [ [ c = Constr.constr; "for"; r = Constr.constr -> (c, r) | c = Constr.constr -> (c, ast_zwf_zero loc) ] ] ; END ;; let wit_program, globwit_program, rawwit_program = Genarg.create_arg "program" let wit_type_v, globwit_type_v, rawwit_type_v = Genarg.create_arg "type_v" open Pp open Util open Himsg open Vernacinterp open Vernacexpr open Declare let is_assumed global ids = if List.length ids = 1 then msgnl (str (if global then "A global variable " else "") ++ pr_id (List.hd ids) ++ str " is assumed") else msgnl (str (if global then "Some global variables " else "") ++ prlist_with_sep (fun () -> (str ", ")) pr_id ids ++ str " are assumed") open Pcoq (* Variables *) let wit_variables, globwit_variables, rawwit_variables = Genarg.create_arg "variables" let variables = Gram.Entry.create "Variables" GEXTEND Gram variables: [ [ l = LIST1 Prim.ident SEP "," -> l ] ]; END let pr_variables _prc _prtac l = spc() ++ prlist_with_sep pr_coma pr_id l let _ = Pptactic.declare_extra_genarg_pprule true (rawwit_variables, pr_variables) (globwit_variables, pr_variables) (wit_variables, pr_variables) (* then_tac *) open Genarg open Tacinterp let pr_then_tac _ prt = function | None -> mt () | Some t -> pr_semicolon () ++ prt t ARGUMENT EXTEND then_tac TYPED AS tactic_opt PRINTED BY pr_then_tac INTERPRETED BY interp_genarg GLOBALIZED BY intern_genarg | [ ";" tactic(t) ] -> [ Some t ] | [ ] -> [ None ] END (* Correctness *) VERNAC COMMAND EXTEND Correctness [ "Correctness" preident(str) program(pgm) then_tac(tac) ] -> [ Ptactic.correctness str pgm (option_map Tacinterp.interp tac) ] END (* Show Programs *) let show_programs () = fold_all (fun (id,v) _ -> msgnl (pr_id id ++ str " : " ++ hov 2 (match v with TypeV v -> pp_type_v v | Set -> (str "Set")) ++ fnl ())) Penv.empty () VERNAC COMMAND EXTEND ShowPrograms [ "Show" "Programs" ] -> [ show_programs () ] END (* Global Variable *) let global_variable ids v = List.iter (fun id -> if Penv.is_global id then Util.errorlabstrm "PROGVARIABLE" (str"Clash with previous constant " ++ pr_id id)) ids; Pdb.check_type_v (all_refs ()) v; let env = empty in let ren = update empty_ren "" [] in let v = Ptyping.cic_type_v env ren v in if not (is_mutable v) then begin let c = Entries.ParameterEntry (trad_ml_type_v ren env v), Decl_kinds.IsAssumption Decl_kinds.Definitional in List.iter (fun id -> ignore (Declare.declare_constant id c)) ids; if_verbose (is_assumed false) ids end; if not (is_pure v) then begin List.iter (fun id -> ignore (Penv.add_global id v None)) ids; if_verbose (is_assumed true) ids end VERNAC COMMAND EXTEND ProgVariable [ "Global" "Variable" variables(ids) ":" type_v(t) ] -> [ global_variable ids t] END let pr_id id = pr_id (Constrextern.v7_to_v8_id id) (* Type printer *) let pr_reads = function | [] -> mt () | l -> spc () ++ hov 0 (str "reads" ++ spc () ++ prlist_with_sep pr_coma pr_id l) let pr_writes = function | [] -> mt () | l -> spc () ++ hov 0 (str "writes" ++ spc () ++ prlist_with_sep pr_coma pr_id l) let pr_effects x = let (ro,rw) = Peffect.get_repr x in pr_reads ro ++ pr_writes rw let pr_predicate delimited { a_name = n; a_value = c } = (if delimited then Ppconstr.pr_lconstr else Ppconstr.pr_constr) c ++ (match n with Name id -> spc () ++ str "as " ++ pr_id id | Anonymous -> mt()) let pr_assert b { p_name = x; p_value = v } = pr_predicate b { a_name = x; a_value = v } let pr_pre_condition_list = function | [] -> mt () | [pre] -> spc() ++ hov 0 (str "pre" ++ spc () ++ pr_assert false pre) | _ -> assert false let pr_post_condition_opt = function | None -> mt () | Some post -> spc() ++ hov 0 (str "post" ++ spc () ++ pr_predicate false post) let rec pr_type_v_v8 = function | Array (a,v) -> str "array" ++ spc() ++ Ppconstr.pr_constr a ++ spc() ++ str "of " ++ pr_type_v_v8 v | v -> pr_type_v3 v and pr_type_v3 = function | Ref v -> pr_type_v3 v ++ spc () ++ str "ref" | Arrow (bl,((id,v),e,prel,postl)) -> str "fun" ++ spc() ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ str "returns" ++ spc () ++ pr_id id ++ str ":" ++ pr_type_v_v8 v ++ pr_effects e ++ pr_pre_condition_list prel ++ pr_post_condition_opt postl ++ spc () ++ str "end" | TypePure a -> Ppconstr.pr_constr a | v -> str "(" ++ pr_type_v_v8 v ++ str ")" and pr_binder = function | (id,BindType c) -> str "(" ++ pr_id id ++ str ":" ++ pr_type_v_v8 c ++ str ")" | (id,BindSet) -> str "(" ++ pr_id id ++ str ":" ++ str "Set" ++ str ")" | (id,Untyped) -> str "<<<<< TODO: Untyped binder >>>>" let _ = Pptactic.declare_extra_genarg_pprule true (rawwit_type_v, fun _ _ -> pr_type_v_v8) (globwit_type_v, fun _ -> raise Not_found) (wit_type_v, fun _ -> raise Not_found) (* Program printer *) let pr_precondition pred = str "{" ++ pr_assert true pred ++ str "}" ++ spc () let pr_postcondition pred = str "{" ++ pr_predicate true pred ++ str "}" let pr_invariant = function | None -> mt () | Some c -> hov 2 (str "invariant" ++ spc () ++ pr_predicate false c) let pr_variant (c1,c2) = Ppconstr.pr_constr c1 ++ (try Constrextern.check_same_type c2 (ast_zwf_zero dummy_loc); mt () with _ -> spc() ++ hov 0 (str "for" ++ spc () ++ Ppconstr.pr_constr c2)) let rec pr_desc = function | Variable id -> (* Unsafe: should distinguish global names and bound vars *) let vars = (* TODO *) Idset.empty in let id = try snd (repr_qualid (snd (qualid_of_reference (Constrextern.extern_reference dummy_loc vars (Nametab.locate (make_short_qualid id)))))) with _ -> id in pr_id id | Acc id -> str "!" ++ pr_id id | Aff (id,p) -> pr_id id ++ spc() ++ str ":=" ++ spc() ++ pr_prog p | TabAcc (b,id,p) -> pr_id id ++ str "[" ++ pr_prog p ++ str "]" | TabAff (b,id,p1,p2) -> pr_id id ++ str "[" ++ pr_prog p1 ++ str "]" ++ str ":=" ++ pr_prog p2 | Seq bll -> hv 0 (str "begin" ++ spc () ++ pr_block bll ++ spc () ++ str "end") | While (p1,inv,var,bll) -> hv 0 ( hov 0 (str "while" ++ spc () ++ pr_prog p1 ++ spc () ++ str "do") ++ brk (1,2) ++ hv 2 ( str "{ " ++ pr_invariant inv ++ spc() ++ hov 0 (str "variant" ++ spc () ++ pr_variant var) ++ str " }") ++ cut () ++ hov 0 (pr_block bll) ++ cut () ++ str "done") | If (p1,p2,p3) -> hov 1 (str "if " ++ pr_prog p1) ++ spc () ++ hov 0 (str "then" ++ spc () ++ pr_prog p2) ++ spc () ++ hov 0 (str "else" ++ spc () ++ pr_prog p3) | Lam (bl,p) -> hov 0 (str "fun" ++ spc () ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ str "=>") ++ pr_prog p | Apply ({desc=Expression e; pre=[]; post=None} as p,args) when isConst e -> begin match string_of_id (snd (repr_path (Nametab.sp_of_global (ConstRef (destConst e))))), args with | "Zmult", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"*" ++ pr_arg a2 ++ str ")" | "Zplus", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"+" ++ pr_arg a2 ++ str ")" | "Zminus", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"-" ++ pr_arg a2 ++ str ")" | "Zopp", [a] -> str "( -" ++ pr_arg a ++ str ")" | "Z_lt_ge_bool", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"<" ++ pr_arg a2 ++ str ")" | "Z_le_gt_bool", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"<=" ++ pr_arg a2 ++ str ")" | "Z_gt_le_bool", [a1;a2] -> str "(" ++ pr_arg a1 ++ str">" ++ pr_arg a2 ++ str ")" | "Z_ge_lt_bool", [a1;a2] -> str "(" ++ pr_arg a1 ++ str">=" ++ pr_arg a2 ++ str ")" | "Z_eq_bool", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"=" ++ pr_arg a2 ++ str ")" | "Z_noteq_bool", [a1;a2] -> str "(" ++ pr_arg a1 ++ str"<> " ++ pr_arg a2 ++ str ")" | _ -> str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++ str ")" end | Apply (p,args) -> str "(" ++ pr_prog p ++ spc () ++ prlist_with_sep spc pr_arg args ++ str ")" | SApp ([Variable v], args) -> begin match string_of_id v, args with | "prog_bool_and", [a1;a2] -> str"(" ++ pr_prog a1 ++ spc() ++ str"and " ++ pr_prog a2 ++str")" | "prog_bool_or", [a1;a2] -> str"(" ++ pr_prog a1 ++ spc() ++ str"or " ++ pr_prog a2 ++ str")" | "prog_bool_not", [a] -> str "(not " ++ pr_prog a ++ str ")" | _ -> failwith "Correctness printer: TODO" end | SApp _ -> failwith "Correctness printer: TODO" | LetRef (v,p1,p2) -> hov 2 ( str "let " ++ pr_id v ++ str " =" ++ spc () ++ str "ref" ++ spc () ++ pr_prog p1 ++ str " in") ++ spc () ++ pr_prog p2 | Let (id, {desc=LetRec (f,bl,v,var,p); pre=[]; post=None },p2) when f=id -> hov 2 ( str "let rec " ++ pr_id f ++ spc () ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ str ":" ++ pr_type_v_v8 v ++ spc () ++ hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ spc() ++ str "=" ++ spc () ++ pr_prog p ++ str " in") ++ spc () ++ pr_prog p2 | Let (v,p1,p2) -> hov 2 ( str "let " ++ pr_id v ++ str " =" ++ spc () ++ pr_prog p1 ++ str" in") ++ spc () ++ pr_prog p2 | LetRec (f,bl,v,var,p) -> str "let rec " ++ pr_id f ++ spc () ++ hov 0 (prlist_with_sep cut pr_binder bl) ++ spc () ++ str ":" ++ pr_type_v_v8 v ++ spc () ++ hov 2 (str "{ variant" ++ spc () ++ pr_variant var ++ str " }") ++ spc () ++ str "=" ++ spc () ++ pr_prog p | PPoint _ -> str "TODO: Ppoint" (* Internal use only *) | Expression c -> (* Numeral or "tt": use a printer which doesn't globalize *) Ppconstr.pr_constr (Constrextern.extern_constr_in_scope false "Z_scope" (Global.env()) c) | Debug (s,p) -> str "@" ++ Pptactic.qsnew s ++ pr_prog p and pr_block_st = function | Label s -> hov 0 (str "label" ++ spc() ++ str s) | Assert pred -> hov 0 (str "assert" ++ spc() ++ hov 0 (pr_postcondition pred)) | Statement p -> pr_prog p and pr_block bl = prlist_with_sep pr_semicolon pr_block_st bl and pr_arg = function | Past.Term p -> pr_prog p | Past.Type t -> str "'" ++ pr_type_v_v8 t | Refarg _ -> str "TODO: Refarg" (* Internal use only *) and pr_prog0 b { desc = desc; pre = pre; post = post } = hv 0 ( prlist pr_precondition pre ++ hov 0 (if b & post<>None then str"(" ++ pr_desc desc ++ str")" else pr_desc desc) ++ Ppconstr.pr_opt pr_postcondition post) and pr_prog x = pr_prog0 true x let _ = Pptactic.declare_extra_genarg_pprule true (rawwit_program, fun _ _ a -> spc () ++ pr_prog0 false a) (globwit_program, fun _ -> raise Not_found) (wit_program, fun _ -> raise Not_found)