diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 278 | ||||
| -rw-r--r-- | src/ltac2_plugin.mlpack | 7 | ||||
| -rw-r--r-- | src/tac2core.ml | 648 | ||||
| -rw-r--r-- | src/tac2core.mli | 62 | ||||
| -rw-r--r-- | src/tac2entries.ml | 648 | ||||
| -rw-r--r-- | src/tac2entries.mli | 57 | ||||
| -rw-r--r-- | src/tac2env.ml | 242 | ||||
| -rw-r--r-- | src/tac2env.mli | 106 | ||||
| -rw-r--r-- | src/tac2expr.mli | 195 | ||||
| -rw-r--r-- | src/tac2intern.ml | 1454 | ||||
| -rw-r--r-- | src/tac2intern.mli | 41 | ||||
| -rw-r--r-- | src/tac2interp.ml | 160 | ||||
| -rw-r--r-- | src/tac2interp.mli | 28 | ||||
| -rw-r--r-- | src/tac2print.ml | 296 | ||||
| -rw-r--r-- | src/tac2print.mli | 37 |
15 files changed, 4259 insertions, 0 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 new file mode 100644 index 0000000000..36057b3a67 --- /dev/null +++ b/src/g_ltac2.ml4 @@ -0,0 +1,278 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Names +open Pcoq +open Constrexpr +open Misctypes +open Tac2expr +open Ltac_plugin + +let tac2expr = Tac2entries.Pltac.tac2expr +let tac2type = Gram.entry_create "tactic:tac2type" +let tac2def_val = Gram.entry_create "tactic:tac2def_val" +let tac2def_typ = Gram.entry_create "tactic:tac2def_typ" +let tac2def_ext = Gram.entry_create "tactic:tac2def_ext" +let tac2def_syn = Gram.entry_create "tactic:tac2def_syn" +let tac2mode = Gram.entry_create "vernac:ltac2_command" + +let inj_wit wit loc x = CTacExt (loc, Genarg.in_gen (Genarg.rawwit wit) x) +let inj_constr loc c = inj_wit Stdarg.wit_constr loc c +let inj_open_constr loc c = inj_wit Stdarg.wit_open_constr loc c +let inj_ident loc c = inj_wit Stdarg.wit_ident loc c + +GEXTEND Gram + GLOBAL: tac2expr tac2type tac2def_val tac2def_typ tac2def_ext tac2def_syn; + tac2pat: + [ "1" LEFTA + [ id = Prim.qualid; pl = LIST1 tac2pat LEVEL "0" -> CPatRef (!@loc, RelId id, pl) + | id = Prim.qualid -> CPatRef (!@loc, RelId id, []) ] + | "0" + [ "_" -> CPatAny (!@loc) + | "()" -> CPatTup (Loc.tag ~loc:!@loc []) + | id = Prim.qualid -> CPatRef (!@loc, RelId id, []) + | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (Loc.tag ~loc:!@loc pl) ] + ] + ; + tac2expr: + [ "5" + [ "fun"; it = LIST1 input_fun ; "=>"; body = tac2expr LEVEL "5" -> CTacFun (!@loc, it, body) + | "let"; isrec = rec_flag; + lc = LIST1 let_clause SEP "with"; "in"; + e = tac2expr LEVEL "5" -> CTacLet (!@loc, isrec, lc, e) + | "match"; e = tac2expr LEVEL "5"; "with"; bl = branches ;"end" -> + CTacCse (!@loc, e, bl) + ] + | "2" LEFTA + [ e1 = tac2expr; ";"; e2 = tac2expr -> CTacSeq (!@loc, e1, e2) ] + | "1" LEFTA + [ e = tac2expr; el = LIST1 tac2expr LEVEL "0" -> CTacApp (!@loc, e, el) + | e = SELF; ".("; qid = Prim.qualid; ")" -> CTacPrj (!@loc, e, RelId qid) + | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, RelId qid, r) + | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "1" SEP "," -> CTacTup (Loc.tag ~loc:!@loc (e0 :: el)) ] + | "0" + [ "("; a = tac2expr LEVEL "5"; ")" -> a + | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t) + | "()" -> CTacTup (Loc.tag ~loc:!@loc []) + | "("; ")" -> CTacTup (Loc.tag ~loc:!@loc []) + | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (Loc.tag ~loc:!@loc a) + | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a) + | a = tactic_atom -> a ] + ] + ; + branches: + [ [ -> [] + | "|"; bl = LIST1 branch SEP "|" -> bl + | bl = LIST1 branch SEP "|" -> bl ] + ] + ; + branch: + [ [ pat = tac2pat LEVEL "1"; "=>"; e = tac2expr LEVEL "5" -> (pat, e) ] ] + ; + rec_flag: + [ [ IDENT "rec" -> true + | -> false ] ] + ; + typ_param: + [ [ "'"; id = Prim.ident -> id ] ] + ; + tactic_atom: + [ [ n = Prim.integer -> CTacAtm (Loc.tag ~loc:!@loc (AtmInt n)) + | s = Prim.string -> CTacAtm (Loc.tag ~loc:!@loc (AtmStr s)) + | id = Prim.qualid -> CTacRef (RelId id) + | IDENT "constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_constr !@loc c + | IDENT "open_constr"; ":"; "("; c = Constr.lconstr; ")" -> inj_open_constr !@loc c + | IDENT "ident"; ":"; "("; c = Prim.ident; ")" -> inj_ident !@loc c + ] ] + ; + let_clause: + [ [ id = binder; ":="; te = tac2expr -> + (id, None, te) + | id = binder; args = LIST1 input_fun; ":="; te = tac2expr -> + (id, None, CTacFun (!@loc, args, te)) ] ] + ; + tac2type: + [ "5" RIGHTA + [ t1 = tac2type; "->"; t2 = tac2type -> CTypArrow (!@loc, t1, t2) ] + | "2" + [ t = tac2type; "*"; tl = LIST1 tac2type SEP "*" -> CTypTuple (!@loc, t :: tl) ] + | "1" LEFTA + [ t = SELF; qid = Prim.qualid -> CTypRef (!@loc, RelId qid, [t]) ] + | "0" + [ "("; t = tac2type LEVEL "5"; ")" -> t + | id = typ_param -> CTypVar (Loc.tag ~loc:!@loc (Name id)) + | "_" -> CTypVar (Loc.tag ~loc:!@loc Anonymous) + | qid = Prim.qualid -> CTypRef (!@loc, RelId qid, []) + | "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> + CTypRef (!@loc, RelId qid, p) ] + ]; + locident: + [ [ id = Prim.ident -> Loc.tag ~loc:!@loc id ] ] + ; + binder: + [ [ "_" -> Loc.tag ~loc:!@loc Anonymous + | l = Prim.ident -> Loc.tag ~loc:!@loc (Name l) ] ] + ; + input_fun: + [ [ b = binder -> (b, None) + | "("; b = binder; ":"; t = tac2type; ")" -> (b, Some t) ] ] + ; + tac2def_body: + [ [ name = binder; it = LIST0 input_fun; ":="; e = tac2expr -> + let e = if List.is_empty it then e else CTacFun (!@loc, it, e) in + (name, e) + ] ] + ; + tac2def_val: + [ [ isrec = rec_flag; l = LIST1 tac2def_body SEP "with" -> + StrVal (isrec, l) + ] ] + ; + tac2typ_knd: + [ [ t = tac2type -> CTydDef (Some t) + | "["; ".."; "]" -> CTydOpn + | "["; t = tac2alg_constructors; "]" -> CTydAlg t + | "{"; t = tac2rec_fields; "}"-> CTydRec t ] ] + ; + tac2alg_constructors: + [ [ "|"; cs = LIST1 tac2alg_constructor SEP "|" -> cs + | cs = LIST0 tac2alg_constructor SEP "|" -> cs ] ] + ; + tac2alg_constructor: + [ [ c = Prim.ident -> (c, []) + | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ] + ; + tac2rec_fields: + [ [ f = tac2rec_field; ";"; l = tac2rec_fields -> f :: l + | f = tac2rec_field; ";" -> [f] + | f = tac2rec_field -> [f] + | -> [] ] ] + ; + tac2rec_field: + [ [ mut = [ -> false | IDENT "mutable" -> true]; id = Prim.ident; ":"; t = tac2type -> (id, mut, t) ] ] + ; + tac2rec_fieldexprs: + [ [ f = tac2rec_fieldexpr; ";"; l = tac2rec_fieldexprs -> f :: l + | f = tac2rec_fieldexpr; ";" -> [f] + | f = tac2rec_fieldexpr-> [f] + | -> [] ] ] + ; + tac2rec_fieldexpr: + [ [ qid = Prim.qualid; ":="; e = tac2expr LEVEL "1" -> RelId qid, e ] ] + ; + tac2typ_prm: + [ [ -> [] + | id = typ_param -> [Loc.tag ~loc:!@loc id] + | "("; ids = LIST1 [ id = typ_param -> Loc.tag ~loc:!@loc id ] SEP "," ;")" -> ids + ] ] + ; + tac2typ_def: + [ [ prm = tac2typ_prm; id = Prim.qualid; (r, e) = tac2type_body -> (id, r, (prm, e)) ] ] + ; + tac2type_body: + [ [ -> false, CTydDef None + | ":="; e = tac2typ_knd -> false, e + | "::="; e = tac2typ_knd -> true, e + ] ] + ; + tac2def_typ: + [ [ "Type"; isrec = rec_flag; l = LIST1 tac2typ_def SEP "with" -> + StrTyp (isrec, l) + ] ] + ; + tac2def_ext: + [ [ "@"; IDENT "external"; id = locident; ":"; t = tac2type LEVEL "5"; ":="; + plugin = Prim.string; name = Prim.string -> + let ml = { mltac_plugin = plugin; mltac_tactic = name } in + StrPrm (id, t, ml) + ] ] + ; + syn_node: + [ [ "_" -> Loc.tag ~loc:!@loc None + | id = Prim.ident -> Loc.tag ~loc:!@loc (Some id) + ] ] + ; + sexpr: + [ [ s = Prim.string -> SexprStr (Loc.tag ~loc:!@loc s) + | n = Prim.integer -> SexprInt (Loc.tag ~loc:!@loc n) + | id = syn_node -> SexprRec (!@loc, id, []) + | id = syn_node; "("; tok = LIST1 sexpr SEP "," ; ")" -> + SexprRec (!@loc, id, tok) + ] ] + ; + syn_level: + [ [ -> None + | ":"; n = Prim.integer -> Some n + ] ] + ; + tac2def_syn: + [ [ "Notation"; toks = LIST1 sexpr; n = syn_level; ":="; + e = tac2expr -> + StrSyn (toks, n, e) + ] ] + ; +END + +GEXTEND Gram + Pcoq.Constr.operconstr: LEVEL "0" + [ [ IDENT "ltac2"; ":"; "("; tac = tac2expr; ")" -> + let arg = Genarg.in_gen (Genarg.rawwit Tac2env.wit_ltac2) tac in + CAst.make ~loc:!@loc (CHole (None, IntroAnonymous, Some arg)) ] ] + ; +END + +let pr_ltac2entry _ = mt () (** FIXME *) +let pr_ltac2expr _ = mt () (** FIXME *) + +VERNAC ARGUMENT EXTEND ltac2_entry +PRINTED BY pr_ltac2entry +| [ tac2def_val(v) ] -> [ v ] +| [ tac2def_typ(t) ] -> [ t ] +| [ tac2def_ext(e) ] -> [ e ] +| [ tac2def_syn(e) ] -> [ e ] +END + +VERNAC COMMAND EXTEND VernacDeclareTactic2Definition CLASSIFIED AS SIDEFF +| [ "Ltac2" ltac2_entry(e) ] -> [ + let local = Locality.LocalityFixme.consume () in + Tac2entries.register_struct ?local e + ] +END + +let _ = + let mode = { + Proof_global.name = "Ltac2"; + set = (fun () -> set_command_entry tac2mode); + reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode); + } in + Proof_global.register_proof_mode mode + +VERNAC ARGUMENT EXTEND ltac2_expr +PRINTED BY pr_ltac2expr +| [ tac2expr(e) ] -> [ e ] +END + +open G_ltac +open Vernac_classifier + +VERNAC tac2mode EXTEND VernacLtac2 +| [ - ltac2_expr(t) ltac_use_default(default) ] => + [ classify_as_proofstep ] -> [ +(* let g = Option.default (Proof_global.get_default_goal_selector ()) g in *) + Tac2entries.call ~default t + ] +END + +open Stdarg + +VERNAC COMMAND EXTEND Ltac2Print CLASSIFIED AS SIDEFF +| [ "Print" "Ltac2" reference(tac) ] -> [ Tac2entries.print_ltac tac ] +END + diff --git a/src/ltac2_plugin.mlpack b/src/ltac2_plugin.mlpack new file mode 100644 index 0000000000..3d87a8cddb --- /dev/null +++ b/src/ltac2_plugin.mlpack @@ -0,0 +1,7 @@ +Tac2env +Tac2print +Tac2intern +Tac2interp +Tac2entries +Tac2core +G_ltac2 diff --git a/src/tac2core.ml b/src/tac2core.ml new file mode 100644 index 0000000000..91a3bfa168 --- /dev/null +++ b/src/tac2core.ml @@ -0,0 +1,648 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CSig +open Pp +open Names +open Genarg +open Geninterp +open Tac2env +open Tac2expr +open Tac2interp +open Proofview.Notations + +(** Standard values *) + +let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n)) + +let val_tag t = match val_tag t with +| Val.Base t -> t +| _ -> assert false + +let val_constr = val_tag (topwit Stdarg.wit_constr) +let val_ident = val_tag (topwit Stdarg.wit_ident) +let val_pp = Val.create "ltac2:pp" + +let extract_val (type a) (tag : a Val.typ) (Val.Dyn (tag', v)) : a = +match Val.eq tag tag' with +| None -> assert false +| Some Refl -> v + +module Core = +struct + +let t_int = coq_core "int" +let t_string = coq_core "string" +let t_array = coq_core "array" +let t_unit = coq_core "unit" +let t_list = coq_core "list" +let t_constr = coq_core "constr" +let t_ident = coq_core "ident" +let t_option = coq_core "option" + +let c_nil = coq_core "[]" +let c_cons = coq_core "::" + +let c_none = coq_core "None" +let c_some = coq_core "Some" + +end + +open Core + +let v_unit = ValInt 0 +let v_nil = ValInt 0 +let v_cons v vl = ValBlk (0, [|v; vl|]) + +module Value = +struct + +let of_unit () = v_unit + +let to_unit = function +| ValInt 0 -> () +| _ -> assert false + +let of_int n = ValInt n +let to_int = function +| ValInt n -> n +| _ -> assert false + +let of_bool b = if b then ValInt 0 else ValInt 1 + +let to_bool = function +| ValInt 0 -> true +| ValInt 1 -> false +| _ -> assert false + +let of_char n = ValInt (Char.code n) +let to_char = function +| ValInt n -> Char.chr n +| _ -> assert false + +let of_string s = ValStr s +let to_string = function +| ValStr s -> s +| _ -> assert false + +let rec of_list = function +| [] -> v_nil +| x :: l -> v_cons x (of_list l) + +let rec to_list = function +| ValInt 0 -> [] +| ValBlk (0, [|v; vl|]) -> v :: to_list vl +| _ -> assert false + +let of_ext tag c = + ValExt (Val.Dyn (tag, c)) + +let to_ext tag = function +| ValExt e -> extract_val tag e +| _ -> assert false + +let of_constr c = of_ext val_constr c +let to_constr c = to_ext val_constr c + +let of_ident c = of_ext val_ident c +let to_ident c = to_ext val_ident c + +(** FIXME: handle backtrace in Ltac2 exceptions *) +let of_exn c = match fst c with +| LtacError (kn, c) -> ValOpn (kn, c) +| _ -> of_ext val_exn c + +let to_exn c = match c with +| ValOpn (kn, c) -> (LtacError (kn, c), Exninfo.null) +| _ -> to_ext val_exn c + +let of_pp c = of_ext val_pp c +let to_pp c = to_ext val_pp c + +end + +let val_valexpr = Val.create "ltac2:valexpr" + +(** Stdlib exceptions *) + +let err_notfocussed = + LtacError (coq_core "Not_focussed", [||]) + +let err_outofbounds = + LtacError (coq_core "Out_of_bounds", [||]) + +let err_notfound = + LtacError (coq_core "Not_found", [||]) + +(** Helper functions *) + +let thaw f = interp_app f [v_unit] +let throw e = Proofview.tclLIFT (Proofview.NonLogical.raise e) + +let return x = Proofview.tclUNIT x +let pname s = { mltac_plugin = "ltac2"; mltac_tactic = s } + +let wrap f = + return () >>= fun () -> return (f ()) + +let wrap_unit f = + return () >>= fun () -> f (); return v_unit + +let pf_apply f = + Proofview.Goal.goals >>= function + | [] -> + Proofview.tclENV >>= fun env -> + Proofview.tclEVARMAP >>= fun sigma -> + f env sigma + | [gl] -> + gl >>= fun gl -> + f (Proofview.Goal.env gl) (Tacmach.New.project gl) + | _ :: _ :: _ -> + throw err_notfocussed + +(** Primitives *) + +(** Printing *) + +let prm_print : ml_tactic = function +| [pp] -> wrap_unit (fun () -> Feedback.msg_notice (Value.to_pp pp)) +| _ -> assert false + +let prm_message_of_int : ml_tactic = function +| [ValInt s] -> return (ValExt (Val.Dyn (val_pp, int s))) +| _ -> assert false + +let prm_message_of_string : ml_tactic = function +| [ValStr s] -> return (ValExt (Val.Dyn (val_pp, str (Bytes.to_string s)))) +| _ -> assert false + +let prm_message_of_constr : ml_tactic = function +| [c] -> + pf_apply begin fun env sigma -> + let c = Value.to_constr c in + let pp = Printer.pr_econstr_env env sigma c in + return (ValExt (Val.Dyn (val_pp, pp))) + end +| _ -> assert false + +let prm_message_concat : ml_tactic = function +| [m1; m2] -> + let m1 = Value.to_pp m1 in + let m2 = Value.to_pp m2 in + return (Value.of_pp (Pp.app m1 m2)) +| _ -> assert false + +(** Array *) + +let prm_array_make : ml_tactic = function +| [ValInt n; x] -> + if n < 0 || n > Sys.max_array_length then throw err_outofbounds + else wrap (fun () -> ValBlk (0, Array.make n x)) +| _ -> assert false + +let prm_array_length : ml_tactic = function +| [ValBlk (_, v)] -> return (ValInt (Array.length v)) +| _ -> assert false + +let prm_array_set : ml_tactic = function +| [ValBlk (_, v); ValInt n; x] -> + if n < 0 || n >= Array.length v then throw err_outofbounds + else wrap_unit (fun () -> v.(n) <- x) +| _ -> assert false + +let prm_array_get : ml_tactic = function +| [ValBlk (_, v); ValInt n] -> + if n < 0 || n >= Array.length v then throw err_outofbounds + else wrap (fun () -> v.(n)) +| _ -> assert false + +(** Int *) + +let prm_int_equal : ml_tactic = function +| [m; n] -> + return (Value.of_bool (Value.to_int m == Value.to_int n)) +| _ -> assert false + +let binop f : ml_tactic = function +| [m; n] -> return (Value.of_int (f (Value.to_int m) (Value.to_int n))) +| _ -> assert false + +let prm_int_compare args = binop Int.compare args +let prm_int_add args = binop (+) args +let prm_int_sub args = binop (-) args +let prm_int_mul args = binop ( * ) args + +let prm_int_neg : ml_tactic = function +| [m] -> return (Value.of_int (~- (Value.to_int m))) +| _ -> assert false + +(** String *) + +let prm_string_make : ml_tactic = function +| [n; c] -> + let n = Value.to_int n in + let c = Value.to_char c in + if n < 0 || n > Sys.max_string_length then throw err_outofbounds + else wrap (fun () -> Value.of_string (Bytes.make n c)) +| _ -> assert false + +let prm_string_length : ml_tactic = function +| [s] -> + return (Value.of_int (Bytes.length (Value.to_string s))) +| _ -> assert false + +let prm_string_set : ml_tactic = function +| [s; n; c] -> + let s = Value.to_string s in + let n = Value.to_int n in + let c = Value.to_char c in + if n < 0 || n >= Bytes.length s then throw err_outofbounds + else wrap_unit (fun () -> Bytes.set s n c) +| _ -> assert false + +let prm_string_get : ml_tactic = function +| [s; n] -> + let s = Value.to_string s in + let n = Value.to_int n in + if n < 0 || n >= Bytes.length s then throw err_outofbounds + else wrap (fun () -> Value.of_char (Bytes.get s n)) +| _ -> assert false + +(** Terms *) + +(** constr -> constr *) +let prm_constr_type : ml_tactic = function +| [c] -> + let c = Value.to_constr c in + let get_type env sigma = + Proofview.V82.wrap_exceptions begin fun () -> + let (sigma, t) = Typing.type_of env sigma c in + let t = Value.of_constr t in + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT t + end in + pf_apply get_type +| _ -> assert false + +(** constr -> constr *) +let prm_constr_equal : ml_tactic = function +| [c1; c2] -> + let c1 = Value.to_constr c1 in + let c2 = Value.to_constr c2 in + Proofview.tclEVARMAP >>= fun sigma -> + let b = EConstr.eq_constr sigma c1 c2 in + Proofview.tclUNIT (Value.of_bool b) +| _ -> assert false + +(** Error *) + +let prm_throw : ml_tactic = function +| [e] -> + let (e, info) = Value.to_exn e in + Proofview.tclLIFT (Proofview.NonLogical.raise ~info e) +| _ -> assert false + +(** Control *) + +(** exn -> 'a *) +let prm_zero : ml_tactic = function +| [e] -> + let (e, info) = Value.to_exn e in + Proofview.tclZERO ~info e +| _ -> assert false + +(** exn -> 'a *) +let prm_plus : ml_tactic = function +| [x; k] -> + Proofview.tclOR (thaw x) (fun e -> interp_app k [Value.of_exn e]) +| _ -> assert false + +(** (unit -> 'a) -> 'a *) +let prm_once : ml_tactic = function +| [f] -> Proofview.tclONCE (thaw f) +| _ -> assert false + +(** (unit -> unit) list -> unit *) +let prm_dispatch : ml_tactic = function +| [l] -> + let l = Value.to_list l in + let l = List.map (fun f -> Proofview.tclIGNORE (thaw f)) l in + Proofview.tclDISPATCH l >>= fun () -> return v_unit +| _ -> assert false + +(** (unit -> unit) list -> (unit -> unit) -> (unit -> unit) list -> unit *) +let prm_extend : ml_tactic = function +| [lft; tac; rgt] -> + let lft = Value.to_list lft in + let lft = List.map (fun f -> Proofview.tclIGNORE (thaw f)) lft in + let tac = Proofview.tclIGNORE (thaw tac) in + let rgt = Value.to_list rgt in + let rgt = List.map (fun f -> Proofview.tclIGNORE (thaw f)) rgt in + Proofview.tclEXTEND lft tac rgt >>= fun () -> return v_unit +| _ -> assert false + +(** (unit -> unit) -> unit *) +let prm_enter : ml_tactic = function +| [f] -> + let f = Proofview.tclIGNORE (thaw f) in + Proofview.tclINDEPENDENT f >>= fun () -> return v_unit +| _ -> assert false + +(** int -> int -> (unit -> 'a) -> 'a *) +let prm_focus : ml_tactic = function +| [i; j; tac] -> + let i = Value.to_int i in + let j = Value.to_int j in + Proofview.tclFOCUS i j (thaw tac) +| _ -> assert false + +(** unit -> unit *) +let prm_shelve : ml_tactic = function +| [_] -> Proofview.shelve >>= fun () -> return v_unit +| _ -> assert false + +(** unit -> unit *) +let prm_shelve_unifiable : ml_tactic = function +| [_] -> Proofview.shelve_unifiable >>= fun () -> return v_unit +| _ -> assert false + +let prm_new_goal : ml_tactic = function +| [ev] -> + let ev = Evar.unsafe_of_int (Value.to_int ev) in + Proofview.tclEVARMAP >>= fun sigma -> + if Evd.mem sigma ev then + Proofview.Unsafe.tclNEWGOALS [ev] <*> Proofview.tclUNIT v_unit + else throw err_notfound +| _ -> assert false + +(** unit -> constr *) +let prm_goal : ml_tactic = function +| [_] -> + Proofview.Goal.enter_one begin fun gl -> + let concl = Tacmach.New.pf_nf_concl gl in + return (Value.of_constr concl) + end +| _ -> assert false + +(** ident -> constr *) +let prm_hyp : ml_tactic = function +| [id] -> + let id = Value.to_ident id in + pf_apply begin fun env _ -> + let mem = try ignore (Environ.lookup_named id env); true with Not_found -> false in + if mem then return (Value.of_constr (EConstr.mkVar id)) + else Tacticals.New.tclZEROMSG + (str "Hypothesis " ++ quote (Id.print id) ++ str " not found") (** FIXME: Do something more sensible *) + end +| _ -> assert false + +(** (unit -> constr) -> unit *) +let prm_refine : ml_tactic = function +| [c] -> + let c = thaw c >>= fun c -> Proofview.tclUNIT ((), Value.to_constr c) in + Proofview.Goal.nf_enter begin fun gl -> + Refine.generic_refine ~typecheck:true c gl + end >>= fun () -> return v_unit +| _ -> assert false + + +(** Registering *) + +let () = Tac2env.define_primitive (pname "print") prm_print +let () = Tac2env.define_primitive (pname "message_of_string") prm_message_of_string +let () = Tac2env.define_primitive (pname "message_of_int") prm_message_of_int +let () = Tac2env.define_primitive (pname "message_of_constr") prm_message_of_constr +let () = Tac2env.define_primitive (pname "message_concat") prm_message_concat + +let () = Tac2env.define_primitive (pname "array_make") prm_array_make +let () = Tac2env.define_primitive (pname "array_length") prm_array_length +let () = Tac2env.define_primitive (pname "array_get") prm_array_get +let () = Tac2env.define_primitive (pname "array_set") prm_array_set + +let () = Tac2env.define_primitive (pname "string_make") prm_string_make +let () = Tac2env.define_primitive (pname "string_length") prm_string_length +let () = Tac2env.define_primitive (pname "string_get") prm_string_get +let () = Tac2env.define_primitive (pname "string_set") prm_string_set + +let () = Tac2env.define_primitive (pname "constr_type") prm_constr_type +let () = Tac2env.define_primitive (pname "constr_equal") prm_constr_equal + +let () = Tac2env.define_primitive (pname "int_equal") prm_int_equal +let () = Tac2env.define_primitive (pname "int_compare") prm_int_compare +let () = Tac2env.define_primitive (pname "int_neg") prm_int_neg +let () = Tac2env.define_primitive (pname "int_add") prm_int_add +let () = Tac2env.define_primitive (pname "int_sub") prm_int_sub +let () = Tac2env.define_primitive (pname "int_mul") prm_int_mul + +let () = Tac2env.define_primitive (pname "throw") prm_throw + +let () = Tac2env.define_primitive (pname "zero") prm_zero +let () = Tac2env.define_primitive (pname "plus") prm_plus +let () = Tac2env.define_primitive (pname "once") prm_once +let () = Tac2env.define_primitive (pname "dispatch") prm_dispatch +let () = Tac2env.define_primitive (pname "extend") prm_extend +let () = Tac2env.define_primitive (pname "enter") prm_enter + +let () = Tac2env.define_primitive (pname "focus") prm_focus +let () = Tac2env.define_primitive (pname "shelve") prm_shelve +let () = Tac2env.define_primitive (pname "shelve_unifiable") prm_shelve_unifiable +let () = Tac2env.define_primitive (pname "new_goal") prm_new_goal +let () = Tac2env.define_primitive (pname "goal") prm_goal +let () = Tac2env.define_primitive (pname "hyp") prm_hyp +let () = Tac2env.define_primitive (pname "refine") prm_refine + +(** ML types *) + +let constr_flags () = + let open Pretyping in + { + use_typeclasses = true; + solve_unification_constraints = true; + use_hook = Pfedit.solve_by_implicit_tactic (); + fail_evar = true; + expand_evars = true + } + +let open_constr_no_classes_flags () = + let open Pretyping in + { + use_typeclasses = false; + solve_unification_constraints = true; + use_hook = Pfedit.solve_by_implicit_tactic (); + fail_evar = false; + expand_evars = true + } + +(** Embed all Ltac2 data into Values *) +let to_lvar ist = + let open Glob_ops in + let map e = Val.Dyn (val_valexpr, e) in + let lfun = Id.Map.map map ist in + { empty_lvar with Glob_term.ltac_genargs = lfun } + +let interp_constr flags ist (c, _) = + let open Pretyping in + pf_apply begin fun env sigma -> + Proofview.V82.wrap_exceptions begin fun () -> + let ist = to_lvar ist in + let (sigma, c) = understand_ltac flags env sigma ist WithoutTypeConstraint c in + let c = Val.Dyn (val_constr, c) in + Proofview.Unsafe.tclEVARS sigma >>= fun () -> + Proofview.tclUNIT c + end + end + +let () = + let interp ist c = interp_constr (constr_flags ()) ist c in + let obj = { + ml_type = t_constr; + ml_interp = interp; + } in + define_ml_object Stdarg.wit_constr obj + +let () = + let interp ist c = interp_constr (open_constr_no_classes_flags ()) ist c in + let obj = { + ml_type = t_constr; + ml_interp = interp; + } in + define_ml_object Stdarg.wit_open_constr obj + +let () = + let interp _ id = return (Val.Dyn (val_ident, id)) in + let obj = { + ml_type = t_ident; + ml_interp = interp; + } in + define_ml_object Stdarg.wit_ident obj + +let () = + let interp ist env sigma concl tac = + let fold id (Val.Dyn (tag, v)) (accu : environment) : environment = + match Val.eq tag val_valexpr with + | None -> accu + | Some Refl -> Id.Map.add id v accu + in + let ist = Id.Map.fold fold ist Id.Map.empty in + let tac = Proofview.tclIGNORE (interp ist tac) in + let c, sigma = Pfedit.refine_by_tactic env sigma concl tac in + (EConstr.of_constr c, sigma) + in + Pretyping.register_constr_interp0 wit_ltac2 interp + +(** Built-in notation scopes *) + +let add_scope s f = + Tac2entries.register_scope (Id.of_string s) f + +let scope_fail () = CErrors.user_err (str "Invalid parsing token") + +let dummy_loc = Loc.make_loc (-1, -1) + +let rthunk e = + let loc = Tac2intern.loc_of_tacexpr e in + let var = [Loc.tag ~loc Anonymous, Some (CTypRef (loc, AbsKn Core.t_unit, []))] in + CTacFun (loc, var, e) + +let add_generic_scope s entry arg = + let parse = function + | [] -> + let scope = Extend.Aentry entry in + let act x = rthunk (CTacExt (dummy_loc, in_gen (rawwit arg) x)) in + Tac2entries.ScopeRule (scope, act) + | _ -> scope_fail () + in + add_scope s parse + +let () = add_scope "list0" begin function +| [tok] -> + let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in + let scope = Extend.Alist0 scope in + let act l = + let l = List.map act l in + CTacLst (None, l) + in + Tac2entries.ScopeRule (scope, act) +| [tok; SexprStr (_, str)] -> + let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in + let sep = Extend.Atoken (CLexer.terminal str) in + let scope = Extend.Alist0sep (scope, sep) in + let act l = + let l = List.map act l in + CTacLst (None, l) + in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + +let () = add_scope "list1" begin function +| [tok] -> + let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in + let scope = Extend.Alist1 scope in + let act l = + let l = List.map act l in + CTacLst (None, l) + in + Tac2entries.ScopeRule (scope, act) +| [tok; SexprStr (_, str)] -> + let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in + let sep = Extend.Atoken (CLexer.terminal str) in + let scope = Extend.Alist1sep (scope, sep) in + let act l = + let l = List.map act l in + CTacLst (None, l) + in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + +let () = add_scope "opt" begin function +| [tok] -> + let Tac2entries.ScopeRule (scope, act) = Tac2entries.parse_scope tok in + let scope = Extend.Aopt scope in + let act opt = match opt with + | None -> + CTacRef (AbsKn (TacConstructor Core.c_none)) + | Some x -> + CTacApp (dummy_loc, CTacRef (AbsKn (TacConstructor Core.c_some)), [act x]) + in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + +let () = add_scope "self" begin function +| [] -> + let scope = Extend.Aself in + let act tac = rthunk tac in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + +let () = add_scope "next" begin function +| [] -> + let scope = Extend.Anext in + let act tac = rthunk tac in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + +let () = add_scope "tactic" begin function +| [] -> + (** Default to level 5 parsing *) + let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, 5) in + let act tac = rthunk tac in + Tac2entries.ScopeRule (scope, act) +| [SexprInt (loc, n)] -> + let () = if n < 0 || n > 5 then scope_fail () in + let scope = Extend.Aentryl (Tac2entries.Pltac.tac2expr, n) in + let act tac = rthunk tac in + Tac2entries.ScopeRule (scope, act) +| _ -> scope_fail () +end + +let () = add_generic_scope "ident" Pcoq.Prim.ident Stdarg.wit_ident +let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr diff --git a/src/tac2core.mli b/src/tac2core.mli new file mode 100644 index 0000000000..fc90499ac6 --- /dev/null +++ b/src/tac2core.mli @@ -0,0 +1,62 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Tac2env +open Tac2expr + +(** {5 Hardwired data} *) + +module Core : +sig + +val t_list : type_constant +val c_nil : ltac_constant +val c_cons : ltac_constant + +val t_int : type_constant +val t_option : type_constant +val t_string : type_constant +val t_array : type_constant + +end + +(** {5 Ltac2 FFI} *) + +(** These functions allow to convert back and forth between OCaml and Ltac2 + data representation. The [to_*] functions raise an anomaly whenever the data + has not expected shape. *) + +module Value : +sig + +val of_unit : unit -> valexpr +val to_unit : valexpr -> unit + +val of_int : int -> valexpr +val to_int : valexpr -> int + +val of_bool : bool -> valexpr +val to_bool : valexpr -> bool + +val of_char : char -> valexpr +val to_char : valexpr -> char + +val of_list : valexpr list -> valexpr +val to_list : valexpr -> valexpr list + +val of_constr : EConstr.t -> valexpr +val to_constr : valexpr -> EConstr.t + +val of_exn : Exninfo.iexn -> valexpr +val to_exn : valexpr -> Exninfo.iexn + +val of_ident : Id.t -> valexpr +val to_ident : valexpr -> Id.t + +end diff --git a/src/tac2entries.ml b/src/tac2entries.ml new file mode 100644 index 0000000000..46f390a6d4 --- /dev/null +++ b/src/tac2entries.ml @@ -0,0 +1,648 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open CErrors +open Names +open Libnames +open Libobject +open Nametab +open Tac2expr +open Tac2print +open Tac2intern +open Vernacexpr + +(** Grammar entries *) + +module Pltac = +struct +let tac2expr = Pcoq.Gram.entry_create "tactic:tac2expr" +end + +(** Tactic definition *) + +type tacdef = { + tacdef_local : bool; + tacdef_expr : glb_tacexpr; + tacdef_type : type_scheme; +} + +let perform_tacdef visibility ((sp, kn), def) = + let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp (TacConstant kn) in + Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type) + +let load_tacdef i obj = perform_tacdef (Until i) obj +let open_tacdef i obj = perform_tacdef (Exactly i) obj + +let cache_tacdef ((sp, kn), def) = + let () = Tac2env.push_ltac (Until 1) sp (TacConstant kn) in + Tac2env.define_global kn (def.tacdef_expr, def.tacdef_type) + +let subst_tacdef (subst, def) = + let expr' = subst_expr subst def.tacdef_expr in + let type' = subst_type_scheme subst def.tacdef_type in + if expr' == def.tacdef_expr && type' == def.tacdef_type then def + else { def with tacdef_expr = expr'; tacdef_type = type' } + +let classify_tacdef o = Substitute o + +let inTacDef : tacdef -> obj = + declare_object {(default_object "TAC2-DEFINITION") with + cache_function = cache_tacdef; + load_function = load_tacdef; + open_function = open_tacdef; + subst_function = subst_tacdef; + classify_function = classify_tacdef} + +(** Type definition *) + +type typdef = { + typdef_local : bool; + typdef_expr : glb_quant_typedef; +} + +let change_kn_label kn id = + let (mp, dp, _) = KerName.repr kn in + KerName.make mp dp (Label.of_id id) + +let change_sp_label sp id = + let (dp, _) = Libnames.repr_path sp in + Libnames.make_path dp id + +let push_typedef visibility sp kn (_, def) = match def with +| GTydDef _ -> + Tac2env.push_type visibility sp kn +| GTydAlg cstrs -> + (** Register constructors *) + let iter (c, _) = + let spc = change_sp_label sp c in + let knc = change_kn_label kn c in + Tac2env.push_ltac visibility spc (TacConstructor knc) + in + Tac2env.push_type visibility sp kn; + List.iter iter cstrs +| GTydRec fields -> + (** Register fields *) + let iter (c, _, _) = + let spc = change_sp_label sp c in + let knc = change_kn_label kn c in + Tac2env.push_projection visibility spc knc + in + Tac2env.push_type visibility sp kn; + List.iter iter fields +| GTydOpn -> + Tac2env.push_type visibility sp kn + +let next i = + let ans = !i in + let () = incr i in + ans + +let define_typedef kn (params, def as qdef) = match def with +| GTydDef _ -> + Tac2env.define_type kn qdef +| GTydAlg cstrs -> + (** Define constructors *) + let constant = ref 0 in + let nonconstant = ref 0 in + let iter (c, args) = + let knc = change_kn_label kn c in + let tag = if List.is_empty args then next constant else next nonconstant in + let data = { + Tac2env.cdata_prms = params; + cdata_type = kn; + cdata_args = args; + cdata_indx = Some tag; + } in + Tac2env.define_constructor knc data + in + Tac2env.define_type kn qdef; + List.iter iter cstrs +| GTydRec fs -> + (** Define projections *) + let iter i (id, mut, t) = + let knp = change_kn_label kn id in + let proj = { + Tac2env.pdata_prms = params; + pdata_type = kn; + pdata_ptyp = t; + pdata_mutb = mut; + pdata_indx = i; + } in + Tac2env.define_projection knp proj + in + Tac2env.define_type kn qdef; + List.iteri iter fs +| GTydOpn -> + Tac2env.define_type kn qdef + +let perform_typdef vs ((sp, kn), def) = + let () = if not def.typdef_local then push_typedef vs sp kn def.typdef_expr in + define_typedef kn def.typdef_expr + +let load_typdef i obj = perform_typdef (Until i) obj +let open_typdef i obj = perform_typdef (Exactly i) obj + +let cache_typdef ((sp, kn), def) = + let () = push_typedef (Until 1) sp kn def.typdef_expr in + define_typedef kn def.typdef_expr + +let subst_typdef (subst, def) = + let expr' = subst_quant_typedef subst def.typdef_expr in + if expr' == def.typdef_expr then def else { def with typdef_expr = expr' } + +let classify_typdef o = Substitute o + +let inTypDef : typdef -> obj = + declare_object {(default_object "TAC2-TYPE-DEFINITION") with + cache_function = cache_typdef; + load_function = load_typdef; + open_function = open_typdef; + subst_function = subst_typdef; + classify_function = classify_typdef} + +(** Type extension *) + +type extension_data = { + edata_name : Id.t; + edata_args : int glb_typexpr list; +} + +type typext = { + typext_local : bool; + typext_prms : int; + typext_type : type_constant; + typext_expr : extension_data list; +} + +let push_typext vis sp kn def = + let iter data = + let spc = change_sp_label sp data.edata_name in + let knc = change_kn_label kn data.edata_name in + Tac2env.push_ltac vis spc (TacConstructor knc) + in + List.iter iter def.typext_expr + +let define_typext kn def = + let iter data = + let knc = change_kn_label kn data.edata_name in + let cdata = { + Tac2env.cdata_prms = def.typext_prms; + cdata_type = def.typext_type; + cdata_args = data.edata_args; + cdata_indx = None; + } in + Tac2env.define_constructor knc cdata + in + List.iter iter def.typext_expr + +let cache_typext ((sp, kn), def) = + let () = define_typext kn def in + push_typext (Until 1) sp kn def + +let perform_typext vs ((sp, kn), def) = + let () = if not def.typext_local then push_typext vs sp kn def in + define_typext kn def + +let load_typext i obj = perform_typext (Until i) obj +let open_typext i obj = perform_typext (Exactly i) obj + +let subst_typext (subst, e) = + let open Mod_subst in + let subst_data data = + let edata_args = List.smartmap (fun e -> subst_type subst e) data.edata_args in + if edata_args == data.edata_args then data + else { data with edata_args } + in + let typext_type = subst_kn subst e.typext_type in + let typext_expr = List.smartmap subst_data e.typext_expr in + if typext_type == e.typext_type && typext_expr == e.typext_expr then + e + else + { e with typext_type; typext_expr } + +let classify_typext o = Substitute o + +let inTypExt : typext -> obj = + declare_object {(default_object "TAC2-TYPE-EXTENSION") with + cache_function = cache_typext; + load_function = load_typext; + open_function = open_typext; + subst_function = subst_typext; + classify_function = classify_typext} + +(** Toplevel entries *) + +let dummy_loc = Loc.make_loc (-1, -1) + +let register_ltac ?(local = false) isrec tactics = + if isrec then + let map (na, e) = (na, None, e) in + let bindings = List.map map tactics in + let map ((loc, na), e) = match na with + | Anonymous -> None + | Name id -> + let qid = Libnames.qualid_of_ident id in + let e = CTacLet (dummy_loc, true, bindings, CTacRef (RelId (loc, qid))) in + let (e, t) = intern e in + let e = match e with + | GTacLet (true, _, e) -> assert false + | _ -> assert false + in + Some (e, t) + in + let tactics = List.map map tactics in + assert false (** FIXME *) + else + let map ((loc, na), e) = + let (e, t) = intern e in + let () = + if not (is_value e) then + user_err ?loc (str "Tactic definition must be a syntactical value") + in + let id = match na with + | Anonymous -> + user_err ?loc (str "Tactic definition must have a name") + | Name id -> id + in + let kn = Lib.make_kn id in + let exists = + try let _ = Tac2env.interp_global kn in true with Not_found -> false + in + let () = + if exists then + user_err ?loc (str "Tactic " ++ Nameops.pr_id id ++ str " already exists") + in + (id, e, t) + in + let defs = List.map map tactics in + let iter (id, e, t) = + let def = { + tacdef_local = local; + tacdef_expr = e; + tacdef_type = t; + } in + ignore (Lib.add_leaf id (inTacDef def)) + in + List.iter iter defs + +let qualid_to_ident (loc, qid) = + let (dp, id) = Libnames.repr_qualid qid in + if DirPath.is_empty dp then (loc, id) + else user_err ?loc (str "Identifier expected") + +let register_typedef ?(local = false) isrec types = + let same_name ((_, id1), _) ((_, id2), _) = Id.equal id1 id2 in + let () = match List.duplicates same_name types with + | [] -> () + | ((loc, id), _) :: _ -> + user_err ?loc (str "Multiple definition of the type name " ++ Id.print id) + in + let check ((loc, id), (params, def)) = + let same_name (_, id1) (_, id2) = Id.equal id1 id2 in + let () = match List.duplicates same_name params with + | [] -> () + | (loc, id) :: _ -> + user_err ?loc (str "The type parameter " ++ Id.print id ++ + str " occurs several times") + in + match def with + | CTydDef _ -> + if isrec then + user_err ?loc (str "The type abbreviation " ++ Id.print id ++ + str " cannot be recursive") + | CTydAlg cs -> + let same_name (id1, _) (id2, _) = Id.equal id1 id2 in + let () = match List.duplicates same_name cs with + | [] -> () + | (id, _) :: _ -> + user_err (str "Multiple definitions of the constructor " ++ Id.print id) + in + () + | CTydRec ps -> + let same_name (id1, _, _) (id2, _, _) = Id.equal id1 id2 in + let () = match List.duplicates same_name ps with + | [] -> () + | (id, _, _) :: _ -> + user_err (str "Multiple definitions of the projection " ++ Id.print id) + in + () + | CTydOpn -> + if isrec then + user_err ?loc (str "The open type declaration " ++ Id.print id ++ + str " cannot be recursive") + in + let () = List.iter check types in + let self = + if isrec then + let fold accu ((_, id), (params, _)) = + Id.Map.add id (Lib.make_kn id, List.length params) accu + in + List.fold_left fold Id.Map.empty types + else Id.Map.empty + in + let map ((_, id), def) = + let typdef = { + typdef_local = local; + typdef_expr = intern_typedef self def; + } in + (id, typdef) + in + let types = List.map map types in + let iter (id, def) = ignore (Lib.add_leaf id (inTypDef def)) in + List.iter iter types + +let register_primitive ?(local = false) (loc, id) t ml = + let t = intern_open_type t in + let rec count_arrow = function + | GTypArrow (_, t) -> 1 + count_arrow t + | _ -> 0 + in + let arrows = count_arrow (snd t) in + let () = if Int.equal arrows 0 then + user_err ?loc (str "External tactic must have at least one argument") in + let () = + try let _ = Tac2env.interp_primitive ml in () with Not_found -> + user_err ?loc (str "Unregistered primitive " ++ + quote (str ml.mltac_plugin) ++ spc () ++ quote (str ml.mltac_tactic)) + in + let init i = Id.of_string (Printf.sprintf "x%i" i) in + let names = List.init arrows init in + let bnd = List.map (fun id -> Name id) names in + let arg = List.map (fun id -> GTacVar id) names in + let e = GTacFun (bnd, GTacPrm (ml, arg)) in + let def = { + tacdef_local = local; + tacdef_expr = e; + tacdef_type = t; + } in + ignore (Lib.add_leaf id (inTacDef def)) + +let register_open ?(local = false) (loc, qid) (params, def) = + let kn = + try Tac2env.locate_type qid + with Not_found -> + user_err ?loc (str "Unbound type " ++ pr_qualid qid) + in + let (tparams, t) = Tac2env.interp_type kn in + let () = match t with + | GTydOpn -> () + | GTydAlg _ | GTydRec _ | GTydDef _ -> + user_err ?loc (str "Type " ++ pr_qualid qid ++ str " is not an open type") + in + let () = + let loc = Option.default dummy_loc loc in + if not (Int.equal (List.length params) tparams) then + Tac2intern.error_nparams_mismatch loc (List.length params) tparams + in + match def with + | CTydOpn -> () + | CTydAlg def -> + let intern_type t = + let tpe = CTydDef (Some t) in + let (_, ans) = intern_typedef Id.Map.empty (params, tpe) in + match ans with + | GTydDef (Some t) -> t + | _ -> assert false + in + let map (id, tpe) = + let tpe = List.map intern_type tpe in + { edata_name = id; edata_args = tpe } + in + let def = List.map map def in + let def = { + typext_local = local; + typext_type = kn; + typext_prms = tparams; + typext_expr = def; + } in + Lib.add_anonymous_leaf (inTypExt def) + | CTydRec _ | CTydDef _ -> + user_err ?loc (str "Extensions only accept inductive constructors") + +let register_type ?local isrec types = match types with +| [qid, true, def] -> + let (loc, _) = qid in + let () = if isrec then user_err ?loc (str "Extensions cannot be recursive") in + register_open ?local qid def +| _ -> + let map (qid, redef, def) = + let (loc, _) = qid in + let () = if redef then + user_err ?loc (str "Types can only be extended one by one") + in + (qualid_to_ident qid, def) + in + let types = List.map map types in + register_typedef ?local isrec types + +(** Parsing *) + +type 'a token = +| TacTerm of string +| TacNonTerm of Name.t * 'a + +type scope_rule = +| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule + +type scope_interpretation = sexpr list -> scope_rule + +let scope_table : scope_interpretation Id.Map.t ref = ref Id.Map.empty + +let register_scope id s = + scope_table := Id.Map.add id s !scope_table + +module ParseToken = +struct + +let loc_of_token = function +| SexprStr (loc, _) -> Option.default dummy_loc loc +| SexprInt (loc, _) -> Option.default dummy_loc loc +| SexprRec (loc, _, _) -> loc + +let parse_scope = function +| SexprRec (_, (loc, Some id), toks) -> + if Id.Map.mem id !scope_table then + Id.Map.find id !scope_table toks + else + CErrors.user_err ?loc (str "Unknown scope" ++ spc () ++ Nameops.pr_id id) +| tok -> + let loc = loc_of_token tok in + CErrors.user_err ~loc (str "Invalid parsing token") + +let parse_token = function +| SexprStr (_, s) -> TacTerm s +| SexprRec (_, (_, na), [tok]) -> + let na = match na with None -> Anonymous | Some id -> Name id in + let scope = parse_scope tok in + TacNonTerm (na, scope) +| tok -> + let loc = loc_of_token tok in + CErrors.user_err ~loc (str "Invalid parsing token") + +end + +let parse_scope = ParseToken.parse_scope + +type synext = { + synext_tok : sexpr list; + synext_exp : raw_tacexpr; + synext_lev : int option; + synext_loc : bool; +} + +type krule = +| KRule : + (raw_tacexpr, 'act, Loc.t -> raw_tacexpr) Extend.rule * + ((Loc.t -> (Name.t * raw_tacexpr) list -> raw_tacexpr) -> 'act) -> krule + +let rec get_rule (tok : scope_rule token list) : krule = match tok with +| [] -> KRule (Extend.Stop, fun k loc -> k loc []) +| TacNonTerm (na, ScopeRule (scope, inj)) :: tok -> + let KRule (rule, act) = get_rule tok in + let rule = Extend.Next (rule, scope) in + let act k e = act (fun loc acc -> k loc ((na, inj e) :: acc)) in + KRule (rule, act) +| TacTerm t :: tok -> + let KRule (rule, act) = get_rule tok in + let rule = Extend.Next (rule, Extend.Atoken (CLexer.terminal t)) in + let act k _ = act k in + KRule (rule, act) + +let perform_notation syn st = + let tok = List.rev_map ParseToken.parse_token syn.synext_tok in + let KRule (rule, act) = get_rule tok in + let mk loc args = + let map (na, e) = + let loc = loc_of_tacexpr e in + (Loc.tag ~loc na, None, e) + in + let bnd = List.map map args in + CTacLet (loc, false, bnd, syn.synext_exp) + in + let rule = Extend.Rule (rule, act mk) in + let lev = match syn.synext_lev with + | None -> None + | Some lev -> Some (string_of_int lev) + in + let rule = (lev, None, [rule]) in + ([Pcoq.ExtendRule (Pltac.tac2expr, None, (None, [rule]))], st) + +let ltac2_notation = + Pcoq.create_grammar_command "ltac2-notation" perform_notation + +let cache_synext (_, syn) = + Pcoq.extend_grammar_command ltac2_notation syn + +let open_synext i (_, syn) = + if Int.equal i 1 then Pcoq.extend_grammar_command ltac2_notation syn + +let subst_synext (subst, syn) = + let e = Tac2intern.subst_rawexpr subst syn.synext_exp in + if e == syn.synext_exp then syn else { syn with synext_exp = e } + +let classify_synext o = + if o.synext_loc then Dispose else Substitute o + +let inTac2Notation : synext -> obj = + declare_object {(default_object "TAC2-NOTATION") with + cache_function = cache_synext; + open_function = open_synext; + subst_function = subst_synext; + classify_function = classify_synext} + +let register_notation ?(local = false) tkn lev body = + (** Check that the tokens make sense *) + let entries = List.map ParseToken.parse_token tkn in + let fold accu tok = match tok with + | TacTerm _ -> accu + | TacNonTerm (Name id, _) -> Id.Set.add id accu + | TacNonTerm (Anonymous, _) -> accu + in + let ids = List.fold_left fold Id.Set.empty entries in + (** Globalize so that names are absolute *) + let body = Tac2intern.globalize ids body in + let ext = { + synext_tok = tkn; + synext_exp = body; + synext_lev = lev; + synext_loc = local; + } in + Lib.add_anonymous_leaf (inTac2Notation ext) + +(** Toplevel entries *) + +let register_struct ?local str = match str with +| StrVal (isrec, e) -> register_ltac ?local isrec e +| StrTyp (isrec, t) -> register_type ?local isrec t +| StrPrm (id, t, ml) -> register_primitive ?local id t ml +| StrSyn (tok, lev, e) -> register_notation ?local tok lev e + +(** Printing *) + +let print_ltac ref = + let (loc, qid) = qualid_of_reference ref in + let kn = + try Tac2env.locate_ltac qid + with Not_found -> user_err ?loc (str "Unknown tactic " ++ pr_qualid qid) + in + match kn with + | TacConstant kn -> + let (e, _, (_, t)) = Tac2env.interp_global kn in + let name = int_name () in + Feedback.msg_notice ( + hov 0 ( + hov 2 (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype name t) ++ fnl () ++ + hov 2 (pr_qualid qid ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr e) + ) + ) + | TacConstructor kn -> + let _ = Tac2env.interp_constructor kn in + Feedback.msg_notice (hov 2 (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid)) + +(** Calling tactics *) + +let solve default tac = + let status = Proof_global.with_current_proof begin fun etac p -> + let with_end_tac = if default then Some etac else None in + let (p, status) = Pfedit.solve SelectAll None tac ?with_end_tac p in + (* in case a strict subtree was completed, + go back to the top of the prooftree *) + let p = Proof.maximal_unfocus Vernacentries.command_focus p in + p, status + end in + if not status then Feedback.feedback Feedback.AddedAxiom + +let call ~default e = + let loc = loc_of_tacexpr e in + let (e, (_, t)) = intern e in + let () = check_unit ~loc t in + let tac = Tac2interp.interp Id.Map.empty e in + solve default (Proofview.tclIGNORE tac) + +(** Primitive algebraic types than can't be defined Coq-side *) + +let register_prim_alg name params def = + let id = Id.of_string name in + let def = List.map (fun (cstr, tpe) -> (Id.of_string_soft cstr, tpe)) def in + let def = (params, GTydAlg def) in + let def = { typdef_local = false; typdef_expr = def } in + ignore (Lib.add_leaf id (inTypDef def)) + +let coq_def n = KerName.make2 Tac2env.coq_prefix (Label.make n) + +let t_list = coq_def "list" + +let _ = Mltop.declare_cache_obj begin fun () -> + register_prim_alg "unit" 0 ["()", []]; + register_prim_alg "list" 1 [ + ("[]", []); + ("::", [GTypVar 0; GTypRef (t_list, [GTypVar 0])]); + ]; +end "ltac2_plugin" diff --git a/src/tac2entries.mli b/src/tac2entries.mli new file mode 100644 index 0000000000..71e8150057 --- /dev/null +++ b/src/tac2entries.mli @@ -0,0 +1,57 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc +open Names +open Libnames +open Tac2expr + +(** {5 Toplevel definitions} *) + +val register_ltac : ?local:bool -> rec_flag -> + (Name.t located * raw_tacexpr) list -> unit + +val register_type : ?local:bool -> rec_flag -> + (qualid located * redef_flag * raw_quant_typedef) list -> unit + +val register_primitive : ?local:bool -> + Id.t located -> raw_typexpr -> ml_tactic_name -> unit + +val register_struct : ?local:bool -> strexpr -> unit + +val register_notation : ?local:bool -> sexpr list -> int option -> + raw_tacexpr -> unit + +(** {5 Notations} *) + +type scope_rule = +| ScopeRule : (raw_tacexpr, 'a) Extend.symbol * ('a -> raw_tacexpr) -> scope_rule + +type scope_interpretation = sexpr list -> scope_rule + +val register_scope : Id.t -> scope_interpretation -> unit +(** Create a new scope with the provided name *) + +val parse_scope : sexpr -> scope_rule +(** Use this to interpret the subscopes for interpretation functions *) + +(** {5 Inspecting} *) + +val print_ltac : Libnames.reference -> unit + +(** {5 Eval loop} *) + +(** Evaluate a tactic expression in the current environment *) +val call : default:bool -> raw_tacexpr -> unit + +(** {5 Parsing entries} *) + +module Pltac : +sig +val tac2expr : raw_tacexpr Pcoq.Gram.entry +end diff --git a/src/tac2env.ml b/src/tac2env.ml new file mode 100644 index 0000000000..5ccdd018ee --- /dev/null +++ b/src/tac2env.ml @@ -0,0 +1,242 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open CErrors +open Util +open Names +open Libnames +open Tac2expr + +type constructor_data = { + cdata_prms : int; + cdata_type : type_constant; + cdata_args : int glb_typexpr list; + cdata_indx : int option; +} + +type projection_data = { + pdata_prms : int; + pdata_type : type_constant; + pdata_ptyp : int glb_typexpr; + pdata_mutb : bool; + pdata_indx : int; +} + +type ltac_state = { + ltac_tactics : (glb_tacexpr * type_scheme) KNmap.t; + ltac_constructors : constructor_data KNmap.t; + ltac_projections : projection_data KNmap.t; + ltac_types : glb_quant_typedef KNmap.t; +} + +let empty_state = { + ltac_tactics = KNmap.empty; + ltac_constructors = KNmap.empty; + ltac_projections = KNmap.empty; + ltac_types = KNmap.empty; +} + +let ltac_state = Summary.ref empty_state ~name:"ltac2-state" + +(** Get a dynamic value from syntactical value *) +let rec eval_pure = function +| GTacAtm (AtmInt n) -> ValInt n +| GTacRef kn -> + let (e, _) = + try KNmap.find kn ltac_state.contents.ltac_tactics + with Not_found -> assert false + in + eval_pure e +| GTacFun (na, e) -> + ValCls { clos_env = Id.Map.empty; clos_var = na; clos_exp = e } +| GTacCst (_, n, []) -> ValInt n +| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el) +| GTacOpn (kn, el) -> ValOpn (kn, Array.map_of_list eval_pure el) +| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ | GTacSet _ +| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ | GTacWth _ -> + anomaly (Pp.str "Term is not a syntactical value") + +let define_global kn e = + let state = !ltac_state in + ltac_state := { state with ltac_tactics = KNmap.add kn e state.ltac_tactics } + +let interp_global kn = + let (e, t) = KNmap.find kn ltac_state.contents.ltac_tactics in + (e, eval_pure e, t) + +let define_constructor kn t = + let state = !ltac_state in + ltac_state := { state with ltac_constructors = KNmap.add kn t state.ltac_constructors } + +let interp_constructor kn = KNmap.find kn ltac_state.contents.ltac_constructors + +let define_projection kn t = + let state = !ltac_state in + ltac_state := { state with ltac_projections = KNmap.add kn t state.ltac_projections } + +let interp_projection kn = KNmap.find kn ltac_state.contents.ltac_projections + +let define_type kn e = + let state = !ltac_state in + ltac_state := { state with ltac_types = KNmap.add kn e state.ltac_types } + +let interp_type kn = KNmap.find kn ltac_state.contents.ltac_types + +module ML = +struct + type t = ml_tactic_name + let compare n1 n2 = + let c = String.compare n1.mltac_plugin n2.mltac_plugin in + if Int.equal c 0 then String.compare n1.mltac_tactic n2.mltac_tactic + else c +end + +module MLMap = Map.Make(ML) + +let primitive_map = ref MLMap.empty + +let define_primitive name f = primitive_map := MLMap.add name f !primitive_map +let interp_primitive name = MLMap.find name !primitive_map + +(** Name management *) + +module FullPath = +struct + type t = full_path + let equal = eq_full_path + let to_string = string_of_path + let repr sp = + let dir,id = repr_path sp in + id, (DirPath.repr dir) +end + +type tacref = Tac2expr.tacref = +| TacConstant of ltac_constant +| TacConstructor of ltac_constructor + +module TacRef = +struct +type t = tacref +let equal r1 r2 = match r1, r2 with +| TacConstant c1, TacConstant c2 -> KerName.equal c1 c2 +| TacConstructor c1, TacConstructor c2 -> KerName.equal c1 c2 +| _ -> false +end + +module KnTab = Nametab.Make(FullPath)(KerName) +module RfTab = Nametab.Make(FullPath)(TacRef) + +type nametab = { + tab_ltac : RfTab.t; + tab_ltac_rev : full_path KNmap.t * full_path KNmap.t; + tab_type : KnTab.t; + tab_type_rev : full_path KNmap.t; + tab_proj : KnTab.t; + tab_proj_rev : full_path KNmap.t; +} + +let empty_nametab = { + tab_ltac = RfTab.empty; + tab_ltac_rev = (KNmap.empty, KNmap.empty); + tab_type = KnTab.empty; + tab_type_rev = KNmap.empty; + tab_proj = KnTab.empty; + tab_proj_rev = KNmap.empty; +} + +let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab" + +let push_ltac vis sp kn = + let tab = !nametab in + let tab_ltac = RfTab.push vis sp kn tab.tab_ltac in + let (constant_map, constructor_map) = tab.tab_ltac_rev in + let tab_ltac_rev = match kn with + | TacConstant c -> (KNmap.add c sp constant_map, constructor_map) + | TacConstructor c -> (constant_map, KNmap.add c sp constructor_map) + in + nametab := { tab with tab_ltac; tab_ltac_rev } + +let locate_ltac qid = + let tab = !nametab in + RfTab.locate qid tab.tab_ltac + +let locate_extended_all_ltac qid = + let tab = !nametab in + RfTab.find_prefixes qid tab.tab_ltac + +let shortest_qualid_of_ltac kn = + let tab = !nametab in + let sp = match kn with + | TacConstant c -> KNmap.find c (fst tab.tab_ltac_rev) + | TacConstructor c -> KNmap.find c (snd tab.tab_ltac_rev) + in + RfTab.shortest_qualid Id.Set.empty sp tab.tab_ltac + +let push_type vis sp kn = + let tab = !nametab in + let tab_type = KnTab.push vis sp kn tab.tab_type in + let tab_type_rev = KNmap.add kn sp tab.tab_type_rev in + nametab := { tab with tab_type; tab_type_rev } + +let locate_type qid = + let tab = !nametab in + KnTab.locate qid tab.tab_type + +let locate_extended_all_type qid = + let tab = !nametab in + KnTab.find_prefixes qid tab.tab_type + +let shortest_qualid_of_type kn = + let tab = !nametab in + let sp = KNmap.find kn tab.tab_type_rev in + KnTab.shortest_qualid Id.Set.empty sp tab.tab_type + +let push_projection vis sp kn = + let tab = !nametab in + let tab_proj = KnTab.push vis sp kn tab.tab_proj in + let tab_proj_rev = KNmap.add kn sp tab.tab_proj_rev in + nametab := { tab with tab_proj; tab_proj_rev } + +let locate_projection qid = + let tab = !nametab in + KnTab.locate qid tab.tab_proj + +let locate_extended_all_projection qid = + let tab = !nametab in + KnTab.find_prefixes qid tab.tab_proj + +let shortest_qualid_of_projection kn = + let tab = !nametab in + let sp = KNmap.find kn tab.tab_proj_rev in + KnTab.shortest_qualid Id.Set.empty sp tab.tab_proj + +type 'a ml_object = { + ml_type : type_constant; + ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic; +} + +module MLTypeObj = +struct + type ('a, 'b, 'c) obj = 'b ml_object + let name = "ltac2_ml_type" + let default _ = None +end + +module MLType = Genarg.Register(MLTypeObj) + +let define_ml_object t tpe = MLType.register0 t tpe +let interp_ml_object t = MLType.obj t + +(** Absolute paths *) + +let coq_prefix = + MPfile (DirPath.make (List.map Id.of_string ["Init"; "ltac2"; "Coq"])) + +(** Generic arguments *) + +let wit_ltac2 = Genarg.make0 "ltac2" diff --git a/src/tac2env.mli b/src/tac2env.mli new file mode 100644 index 0000000000..c4b8c1e0ca --- /dev/null +++ b/src/tac2env.mli @@ -0,0 +1,106 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Genarg +open Names +open Libnames +open Nametab +open Tac2expr + +(** Ltac2 global environment *) + +(** {5 Toplevel definition of values} *) + +val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit +val interp_global : ltac_constant -> (glb_tacexpr * valexpr * type_scheme) + +(** {5 Toplevel definition of types} *) + +val define_type : type_constant -> glb_quant_typedef -> unit +val interp_type : type_constant -> glb_quant_typedef + +(** {5 Toplevel definition of algebraic constructors} *) + +type constructor_data = { + cdata_prms : int; + (** Type parameters *) + cdata_type : type_constant; + (** Inductive definition to which the constructor pertains *) + cdata_args : int glb_typexpr list; + (** Types of the constructor arguments *) + cdata_indx : int option; + (** Index of the constructor in the ADT. Numbering is duplicated between + argumentless and argument-using constructors, e.g. in type ['a option] + [None] and [Some] have both index 0. This field is empty whenever the + constructor is a member of an open type. *) +} + +val define_constructor : ltac_constructor -> constructor_data -> unit +val interp_constructor : ltac_constructor -> constructor_data + +(** {5 Toplevel definition of projections} *) + +type projection_data = { + pdata_prms : int; + (** Type parameters *) + pdata_type : type_constant; + (** Record definition to which the projection pertains *) + pdata_ptyp : int glb_typexpr; + (** Type of the projection *) + pdata_mutb : bool; + (** Whether the field is mutable *) + pdata_indx : int; + (** Index of the projection *) +} + +val define_projection : ltac_projection -> projection_data -> unit +val interp_projection : ltac_projection -> projection_data + +(** {5 Name management} *) + +val push_ltac : visibility -> full_path -> tacref -> unit +val locate_ltac : qualid -> tacref +val locate_extended_all_ltac : qualid -> tacref list +val shortest_qualid_of_ltac : tacref -> qualid + +val push_type : visibility -> full_path -> type_constant -> unit +val locate_type : qualid -> type_constant +val locate_extended_all_type : qualid -> type_constant list +val shortest_qualid_of_type : type_constant -> qualid + +val push_projection : visibility -> full_path -> ltac_projection -> unit +val locate_projection : qualid -> ltac_projection +val locate_extended_all_projection : qualid -> ltac_projection list +val shortest_qualid_of_projection : ltac_projection -> qualid + +(** {5 Toplevel definitions of ML tactics} *) + +(** This state is not part of the summary, contrarily to the ones above. It is + intended to be used from ML plugins to register ML-side functions. *) + +val define_primitive : ml_tactic_name -> ml_tactic -> unit +val interp_primitive : ml_tactic_name -> ml_tactic + +(** {5 ML primitive types} *) + +type 'a ml_object = { + ml_type : type_constant; + ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic; +} + +val define_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object -> unit +val interp_ml_object : ('a, 'b, 'c) genarg_type -> 'b ml_object + +(** {5 Absolute paths} *) + +val coq_prefix : ModPath.t +(** Path where primitive datatypes are defined in Ltac2 plugin. *) + +(** {5 Generic arguments} *) + +val wit_ltac2 : (raw_tacexpr, glb_tacexpr, Util.Empty.t) genarg_type diff --git a/src/tac2expr.mli b/src/tac2expr.mli new file mode 100644 index 0000000000..acdad9bab4 --- /dev/null +++ b/src/tac2expr.mli @@ -0,0 +1,195 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Loc +open Genarg +open Names +open Libnames + +type mutable_flag = bool +type rec_flag = bool +type redef_flag = bool +type lid = Id.t +type uid = Id.t + +type ltac_constant = KerName.t +type ltac_constructor = KerName.t +type ltac_projection = KerName.t +type type_constant = KerName.t + +type 'a or_relid = +| RelId of qualid located +| AbsKn of 'a + +(** {5 Misc} *) + +type ml_tactic_name = { + mltac_plugin : string; + mltac_tactic : string; +} + +(** {5 Type syntax} *) + +type raw_typexpr = +| CTypVar of Name.t located +| CTypArrow of Loc.t * raw_typexpr * raw_typexpr +| CTypTuple of Loc.t * raw_typexpr list +| CTypRef of Loc.t * type_constant or_relid * raw_typexpr list + +type raw_typedef = +| CTydDef of raw_typexpr option +| CTydAlg of (uid * raw_typexpr list) list +| CTydRec of (lid * mutable_flag * raw_typexpr) list +| CTydOpn + +type 'a glb_typexpr = +| GTypVar of 'a +| GTypArrow of 'a glb_typexpr * 'a glb_typexpr +| GTypTuple of 'a glb_typexpr list +| GTypRef of type_constant * 'a glb_typexpr list + +type glb_typedef = +| GTydDef of int glb_typexpr option +| GTydAlg of (uid * int glb_typexpr list) list +| GTydRec of (lid * mutable_flag * int glb_typexpr) list +| GTydOpn + +type type_scheme = int * int glb_typexpr + +type raw_quant_typedef = Id.t located list * raw_typedef +type glb_quant_typedef = int * glb_typedef + +(** {5 Term syntax} *) + +type atom = +| AtmInt of int +| AtmStr of string + +type tacref = +| TacConstant of ltac_constant +| TacConstructor of ltac_constructor + +(** Tactic expressions *) +type raw_patexpr = +| CPatAny of Loc.t +| CPatRef of Loc.t * ltac_constructor or_relid * raw_patexpr list +| CPatTup of raw_patexpr list located + +type raw_tacexpr = +| CTacAtm of atom located +| CTacRef of tacref or_relid +| CTacFun of Loc.t * (Name.t located * raw_typexpr option) list * raw_tacexpr +| CTacApp of Loc.t * raw_tacexpr * raw_tacexpr list +| CTacLet of Loc.t * rec_flag * (Name.t located * raw_typexpr option * raw_tacexpr) list * raw_tacexpr +| CTacTup of raw_tacexpr list located +| CTacArr of raw_tacexpr list located +| CTacLst of raw_tacexpr list located +| CTacCnv of Loc.t * raw_tacexpr * raw_typexpr +| CTacSeq of Loc.t * raw_tacexpr * raw_tacexpr +| CTacCse of Loc.t * raw_tacexpr * raw_taccase list +| CTacRec of Loc.t * raw_recexpr +| CTacPrj of Loc.t * raw_tacexpr * ltac_projection or_relid +| CTacSet of Loc.t * raw_tacexpr * ltac_projection or_relid * raw_tacexpr +| CTacExt of Loc.t * raw_generic_argument + +and raw_taccase = raw_patexpr * raw_tacexpr + +and raw_recexpr = (ltac_projection or_relid * raw_tacexpr) list + +type case_info = +| GCaseTuple of int +| GCaseAlg of type_constant + +type 'a open_match = { + opn_match : 'a; + opn_branch : (Name.t * Name.t array * 'a) KNmap.t; + (** Invariant: should not be empty *) + opn_default : Name.t * 'a; +} + +type glb_tacexpr = +| GTacAtm of atom +| GTacVar of Id.t +| GTacRef of ltac_constant +| GTacFun of Name.t list * glb_tacexpr +| GTacApp of glb_tacexpr * glb_tacexpr list +| GTacLet of rec_flag * (Name.t * glb_tacexpr) list * glb_tacexpr +| GTacArr of glb_tacexpr list +| GTacCst of case_info * int * glb_tacexpr list +| GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array +| GTacPrj of type_constant * glb_tacexpr * int +| GTacSet of type_constant * glb_tacexpr * int * glb_tacexpr +| GTacOpn of ltac_constructor * glb_tacexpr list +| GTacWth of glb_tacexpr open_match +| GTacExt of glob_generic_argument +| GTacPrm of ml_tactic_name * glb_tacexpr list + +(** {5 Parsing & Printing} *) + +type exp_level = +| E5 +| E4 +| E3 +| E2 +| E1 +| E0 + +type sexpr = +| SexprStr of string located +| SexprInt of int located +| SexprRec of Loc.t * Id.t option located * sexpr list + +(** {5 Toplevel statements} *) + +type strexpr = +| StrVal of rec_flag * (Name.t located * raw_tacexpr) list + (** Term definition *) +| StrTyp of rec_flag * (qualid located * redef_flag * raw_quant_typedef) list + (** Type definition *) +| StrPrm of Id.t located * raw_typexpr * ml_tactic_name + (** External definition *) +| StrSyn of sexpr list * int option * raw_tacexpr + (** Syntactic extensions *) + + +(** {5 Dynamic semantics} *) + +(** Values are represented in a way similar to OCaml, i.e. they constrast + immediate integers (integers, constructors without arguments) and structured + blocks (tuples, arrays, constructors with arguments), as well as a few other + base cases, namely closures, strings, named constructors, and dynamic type + coming from the Coq implementation. *) + +type tag = int + +type valexpr = +| ValInt of int + (** Immediate integers *) +| ValBlk of tag * valexpr array + (** Structured blocks *) +| ValStr of Bytes.t + (** Strings *) +| ValCls of closure + (** Closures *) +| ValOpn of KerName.t * valexpr array + (** Open constructors *) +| ValExt of Geninterp.Val.t + (** Arbitrary data *) + +and closure = { + mutable clos_env : valexpr Id.Map.t; + (** Mutable so that we can implement recursive functions imperatively *) + clos_var : Name.t list; + (** Bound variables *) + clos_exp : glb_tacexpr; + (** Body *) +} + +type ml_tactic = valexpr list -> valexpr Proofview.tactic + +type environment = valexpr Id.Map.t diff --git a/src/tac2intern.ml b/src/tac2intern.ml new file mode 100644 index 0000000000..b63e6a0cd8 --- /dev/null +++ b/src/tac2intern.ml @@ -0,0 +1,1454 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Util +open Genarg +open CErrors +open Names +open Libnames +open Misctypes +open Tac2env +open Tac2print +open Tac2expr + +(** Hardwired types and constants *) + +let coq_type n = KerName.make2 Tac2env.coq_prefix (Label.make n) + +let t_int = coq_type "int" +let t_string = coq_type "string" +let t_array = coq_type "array" +let t_unit = coq_type "unit" +let t_list = coq_type "list" + +let c_nil = GTacCst (GCaseAlg t_list, 0, []) +let c_cons e el = GTacCst (GCaseAlg t_list, 0, [e; el]) + +(** Union find *) + +module UF : +sig +type elt +type 'a t +val equal : elt -> elt -> bool +val create : unit -> 'a t +val fresh : 'a t -> elt +val find : elt -> 'a t -> (elt * 'a option) +val union : elt -> elt -> 'a t -> unit +val set : elt -> 'a -> 'a t -> unit +module Map : +sig + type key = elt + type +'a t + val empty : 'a t + val add : key -> 'a -> 'a t -> 'a t + val mem : key -> 'a t -> bool + val find : key -> 'a t -> 'a + val exists : (key -> 'a -> bool) -> 'a t -> bool +end +end += +struct +type elt = int +let equal = Int.equal +module Map = Int.Map + +type 'a node = +| Canon of int * 'a option +| Equiv of elt + +type 'a t = { + mutable uf_data : 'a node array; + mutable uf_size : int; +} + +let resize p = + if Int.equal (Array.length p.uf_data) p.uf_size then begin + let nsize = 2 * p.uf_size + 1 in + let v = Array.make nsize (Equiv 0) in + Array.blit p.uf_data 0 v 0 (Array.length p.uf_data); + p.uf_data <- v; + end + +let create () = { uf_data = [||]; uf_size = 0 } + +let fresh p = + resize p; + let n = p.uf_size in + p.uf_data.(n) <- (Canon (1, None)); + p.uf_size <- n + 1; + n + +let rec lookup n p = + let node = Array.get p.uf_data n in + match node with + | Canon (size, v) -> n, size, v + | Equiv y -> + let ((z, _, _) as res) = lookup y p in + if not (Int.equal z y) then Array.set p.uf_data n (Equiv z); + res + +let find n p = + let (x, _, v) = lookup n p in (x, v) + +let union x y p = + let ((x, size1, _) as xcan) = lookup x p in + let ((y, size2, _) as ycan) = lookup y p in + let xcan, ycan = if size1 < size2 then xcan, ycan else ycan, xcan in + let x, _, xnode = xcan in + let y, _, ynode = ycan in + assert (Option.is_empty xnode); + assert (Option.is_empty ynode); + p.uf_data.(x) <- Equiv y; + p.uf_data.(y) <- Canon (size1 + size2, None) + +let set x v p = + let (x, s, v') = lookup x p in + assert (Option.is_empty v'); + p.uf_data.(x) <- Canon (s, Some v) + +end + +type mix_var = +| GVar of UF.elt +| LVar of int + +type mix_type_scheme = int * mix_var glb_typexpr + +type environment = { + env_var : mix_type_scheme Id.Map.t; + (** Type schemes of bound variables *) + env_cst : UF.elt glb_typexpr UF.t; + (** Unification state *) + env_als : UF.elt Id.Map.t ref; + (** Map user-facing type variables to unification variables *) + env_opn : bool; + (** Accept unbound type variables *) + env_rec : (KerName.t * int) Id.Map.t; + (** Recursive type definitions *) +} + +let empty_env () = { + env_var = Id.Map.empty; + env_cst = UF.create (); + env_als = ref Id.Map.empty; + env_opn = true; + env_rec = Id.Map.empty; +} + +let env_name env = + (** Generate names according to a provided environment *) + let mk num = + let base = num mod 26 in + let rem = num / 26 in + let name = String.make 1 (Char.chr (97 + base)) in + let suff = if Int.equal rem 0 then "" else string_of_int rem in + let name = name ^ suff in + name + in + let fold id elt acc = UF.Map.add elt (Id.to_string id) acc in + let vars = Id.Map.fold fold env.env_als.contents UF.Map.empty in + let vars = ref vars in + let rec fresh n = + let name = mk n in + if UF.Map.exists (fun _ name' -> String.equal name name') !vars then fresh (succ n) + else name + in + fun n -> + if UF.Map.mem n !vars then UF.Map.find n !vars + else + let ans = fresh 0 in + let () = vars := UF.Map.add n ans !vars in + ans + +let ltac2_env : environment Genintern.Store.field = + Genintern.Store.field () + +let fresh_id env = UF.fresh env.env_cst + +let get_alias (loc, id) env = + try Id.Map.find id env.env_als.contents + with Not_found -> + if env.env_opn then + let n = fresh_id env in + let () = env.env_als := Id.Map.add id n env.env_als.contents in + n + else user_err ?loc (str "Unbound type parameter " ++ Id.print id) + +let push_name id t env = match id with +| Anonymous -> env +| Name id -> { env with env_var = Id.Map.add id t env.env_var } + +let dummy_loc = Loc.make_loc (-1, -1) + +let loc_of_tacexpr = function +| CTacAtm (loc, _) -> Option.default dummy_loc loc +| CTacRef (RelId (loc, _)) -> Option.default dummy_loc loc +| CTacRef (AbsKn _) -> dummy_loc +| CTacFun (loc, _, _) -> loc +| CTacApp (loc, _, _) -> loc +| CTacLet (loc, _, _, _) -> loc +| CTacTup (loc, _) -> Option.default dummy_loc loc +| CTacArr (loc, _) -> Option.default dummy_loc loc +| CTacLst (loc, _) -> Option.default dummy_loc loc +| CTacCnv (loc, _, _) -> loc +| CTacSeq (loc, _, _) -> loc +| CTacCse (loc, _, _) -> loc +| CTacRec (loc, _) -> loc +| CTacPrj (loc, _, _) -> loc +| CTacSet (loc, _, _, _) -> loc +| CTacExt (loc, _) -> loc + +let loc_of_patexpr = function +| CPatAny loc -> loc +| CPatRef (loc, _, _) -> loc +| CPatTup (loc, _) -> Option.default dummy_loc loc + +let error_nargs_mismatch loc nargs nfound = + user_err ~loc (str "Constructor expects " ++ int nargs ++ + str " arguments, but is applied to " ++ int nfound ++ + str " arguments") + +let error_nparams_mismatch loc nargs nfound = + user_err ~loc (str "Type expects " ++ int nargs ++ + str " arguments, but is applied to " ++ int nfound ++ + str " arguments") + +let rec subst_type subst (t : 'a glb_typexpr) = match t with +| GTypVar id -> subst id +| GTypArrow (t1, t2) -> GTypArrow (subst_type subst t1, subst_type subst t2) +| GTypTuple tl -> GTypTuple (List.map (fun t -> subst_type subst t) tl) +| GTypRef (qid, args) -> + GTypRef (qid, List.map (fun t -> subst_type subst t) args) + +let rec intern_type env (t : raw_typexpr) : UF.elt glb_typexpr = match t with +| CTypVar (loc, Name id) -> GTypVar (get_alias (Loc.tag ?loc id) env) +| CTypVar (_, Anonymous) -> GTypVar (fresh_id env) +| CTypRef (loc, rel, args) -> + let (kn, nparams) = match rel with + | RelId (loc, qid) -> + let (dp, id) = repr_qualid qid in + if DirPath.is_empty dp && Id.Map.mem id env.env_rec then + Id.Map.find id env.env_rec + else + let kn = + try Tac2env.locate_type qid + with Not_found -> + user_err ?loc (str "Unbound type constructor " ++ pr_qualid qid) + in + let (nparams, _) = Tac2env.interp_type kn in + (kn, nparams) + | AbsKn kn -> + let (nparams, _) = Tac2env.interp_type kn in + (kn, nparams) + in + let nargs = List.length args in + let () = + if not (Int.equal nparams nargs) then + let loc, qid = match rel with + | RelId lid -> lid + | AbsKn kn -> Some loc, shortest_qualid_of_type kn + in + user_err ?loc (strbrk "The type constructor " ++ pr_qualid qid ++ + strbrk " expects " ++ int nparams ++ strbrk " argument(s), but is here \ + applied to " ++ int nargs ++ strbrk "argument(s)") + in + GTypRef (kn, List.map (fun t -> intern_type env t) args) +| CTypArrow (loc, t1, t2) -> GTypArrow (intern_type env t1, intern_type env t2) +| CTypTuple (loc, tl) -> GTypTuple (List.map (fun t -> intern_type env t) tl) + +let fresh_type_scheme env (t : type_scheme) : UF.elt glb_typexpr = + let (n, t) = t in + let subst = Array.init n (fun _ -> fresh_id env) in + let substf i = GTypVar subst.(i) in + subst_type substf t + +let fresh_mix_type_scheme env (t : mix_type_scheme) : UF.elt glb_typexpr = + let (n, t) = t in + let subst = Array.init n (fun _ -> fresh_id env) in + let substf = function + | LVar i -> GTypVar subst.(i) + | GVar n -> GTypVar n + in + subst_type substf t + +let fresh_reftype env (kn : KerName.t) = + let (n, _) = Tac2env.interp_type kn in + let subst = Array.init n (fun _ -> fresh_id env) in + let t = GTypRef (kn, Array.map_to_list (fun i -> GTypVar i) subst) in + (subst, t) + +(** First-order unification algorithm *) + +let is_unfoldable kn = match snd (Tac2env.interp_type kn) with +| GTydDef (Some _) -> true +| GTydDef None | GTydAlg _ | GTydRec _ | GTydOpn -> false + +let unfold env kn args = + let (nparams, def) = Tac2env.interp_type kn in + let def = match def with + | GTydDef (Some t) -> t + | _ -> assert false + in + let args = Array.of_list args in + let subst n = args.(n) in + subst_type subst def + +(** View function, allows to ensure head normal forms *) +let rec kind env t = match t with +| GTypVar id -> + let (id, v) = UF.find id env.env_cst in + begin match v with + | None -> GTypVar id + | Some t -> kind env t + end +| GTypRef (kn, tl) -> + if is_unfoldable kn then kind env (unfold env kn tl) else t +| GTypArrow _ | GTypTuple _ -> t + +exception Occur + +let rec occur_check env id t = match kind env t with +| GTypVar id' -> if UF.equal id id' then raise Occur +| GTypArrow (t1, t2) -> + let () = occur_check env id t1 in + occur_check env id t2 +| GTypTuple tl -> + List.iter (fun t -> occur_check env id t) tl +| GTypRef (kn, tl) -> + List.iter (fun t -> occur_check env id t) tl + +exception CannotUnify of UF.elt glb_typexpr * UF.elt glb_typexpr + +let unify_var env id t = match kind env t with +| GTypVar id' -> + if not (UF.equal id id') then UF.union id id' env.env_cst +| GTypArrow _ | GTypRef _ | GTypTuple _ -> + try + let () = occur_check env id t in + UF.set id t env.env_cst + with Occur -> raise (CannotUnify (GTypVar id, t)) + +let rec unify env t1 t2 = match kind env t1, kind env t2 with +| GTypVar id, t | t, GTypVar id -> + unify_var env id t +| GTypArrow (t1, u1), GTypArrow (t2, u2) -> + let () = unify env t1 t2 in + unify env u1 u2 +| GTypTuple tl1, GTypTuple tl2 -> + if Int.equal (List.length tl1) (List.length tl2) then + List.iter2 (fun t1 t2 -> unify env t1 t2) tl1 tl2 + else raise (CannotUnify (t1, t2)) +| GTypRef (kn1, tl1), GTypRef (kn2, tl2) -> + if KerName.equal kn1 kn2 then + List.iter2 (fun t1 t2 -> unify env t1 t2) tl1 tl2 + else raise (CannotUnify (t1, t2)) +| _ -> raise (CannotUnify (t1, t2)) + +let unify ?loc env t1 t2 = + try unify env t1 t2 + with CannotUnify (u1, u2) -> + let name = env_name env in + user_err ?loc (str "This expression has type " ++ pr_glbtype name t1 ++ + str " but an expression what expected of type " ++ pr_glbtype name t2) + +(** Term typing *) + +let is_pure_constructor kn = + match snd (Tac2env.interp_type kn) with + | GTydAlg _ | GTydOpn -> true + | GTydRec fields -> + let is_pure (_, mut, _) = not mut in + List.for_all is_pure fields + | GTydDef _ -> assert false (** Type definitions have no constructors *) + +let rec is_value = function +| GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true +| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false +| GTacCst (GCaseTuple _, _, el) -> List.for_all is_value el +| GTacCst (_, _, []) -> true +| GTacOpn (_, el) -> List.for_all is_value el +| GTacCst (GCaseAlg kn, _, el) -> is_pure_constructor kn && List.for_all is_value el +| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ +| GTacWth _ -> false + +let is_rec_rhs = function +| GTacFun _ -> true +| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _ +| GTacSet _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _ +| GTacCse _ | GTacOpn _ | GTacWth _ -> false + +let rec fv_type f t accu = match t with +| GTypVar id -> f id accu +| GTypArrow (t1, t2) -> fv_type f t1 (fv_type f t2 accu) +| GTypTuple tl -> List.fold_left (fun accu t -> fv_type f t accu) accu tl +| GTypRef (kn, tl) -> List.fold_left (fun accu t -> fv_type f t accu) accu tl + +let fv_env env = + let rec f id accu = match UF.find id env.env_cst with + | id, None -> UF.Map.add id () accu + | _, Some t -> fv_type f t accu + in + let fold_var id (_, t) accu = + let fmix id accu = match id with + | LVar _ -> accu + | GVar id -> f id accu + in + fv_type fmix t accu + in + let fv_var = Id.Map.fold fold_var env.env_var UF.Map.empty in + let fold_als _ id accu = f id accu in + Id.Map.fold fold_als !(env.env_als) fv_var + +let abstract_var env (t : UF.elt glb_typexpr) : mix_type_scheme = + let fv = fv_env env in + let count = ref 0 in + let vars = ref UF.Map.empty in + let rec subst id = + let (id, t) = UF.find id env.env_cst in + match t with + | None -> + if UF.Map.mem id fv then GTypVar (GVar id) + else + begin try UF.Map.find id !vars + with Not_found -> + let n = !count in + let var = GTypVar (LVar n) in + let () = incr count in + let () = vars := UF.Map.add id var !vars in + var + end + | Some t -> subst_type subst t + in + let t = subst_type subst t in + (!count, t) + +let monomorphic (t : UF.elt glb_typexpr) : mix_type_scheme = + let subst id = GTypVar (GVar id) in + (0, subst_type subst t) + +let warn_not_unit = + CWarnings.create ~name:"not-unit" ~category:"ltac" + (fun () -> strbrk "The following expression should have type unit.") + +let warn_redundant_clause = + CWarnings.create ~name:"redundant-clause" ~category:"ltac" + (fun () -> strbrk "The following clause is redundant.") + +let check_elt_unit loc env t = + let maybe_unit = match kind env t with + | GTypVar _ -> true + | GTypArrow _ | GTypTuple _ -> false + | GTypRef (kn, _) -> KerName.equal kn t_unit + in + if not maybe_unit then warn_not_unit ~loc () + +let check_elt_empty loc env t = match kind env t with +| GTypVar _ -> + user_err ~loc (str "Cannot infer an empty type for this expression") +| GTypArrow _ | GTypTuple _ -> + let name = env_name env in + user_err ~loc (str "Type " ++ pr_glbtype name t ++ str " is not an empty type") +| GTypRef (kn, _) -> + let def = Tac2env.interp_type kn in + match def with + | _, GTydAlg [] -> kn + | _ -> + let name = env_name env in + user_err ~loc (str "Type " ++ pr_glbtype name t ++ str " is not an empty type") + +let check_unit ?loc t = + let maybe_unit = match t with + | GTypVar _ -> true + | GTypArrow _ | GTypTuple _ -> false + | GTypRef (kn, _) -> KerName.equal kn t_unit + in + if not maybe_unit then warn_not_unit ?loc () + +let check_redundant_clause = function +| [] -> () +| (p, _) :: _ -> warn_redundant_clause ~loc:(loc_of_patexpr p) () + +let get_variable0 mem var = match var with +| RelId (loc, qid) -> + let (dp, id) = repr_qualid qid in + if DirPath.is_empty dp && mem id then ArgVar (loc, id) + else + let kn = + try Tac2env.locate_ltac qid + with Not_found -> + CErrors.user_err ?loc (str "Unbound value " ++ pr_qualid qid) + in + ArgArg kn +| AbsKn kn -> ArgArg kn + +let get_variable env var = + let mem id = Id.Map.mem id env.env_var in + get_variable0 mem var + +let get_constructor env var = match var with +| RelId (loc, qid) -> + let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in + begin match c with + | Some (TacConstructor knc) -> + let kn = Tac2env.interp_constructor knc in + ArgArg (kn, knc) + | Some (TacConstant _) -> + CErrors.user_err ?loc (str "The term " ++ pr_qualid qid ++ + str " is not the constructor of an inductive type.") + | None -> + let (dp, id) = repr_qualid qid in + if DirPath.is_empty dp then ArgVar (loc, id) + else CErrors.user_err ?loc (str "Unbound constructor " ++ pr_qualid qid) + end +| AbsKn knc -> + let kn = Tac2env.interp_constructor knc in + ArgArg (kn, knc) + +let get_projection var = match var with +| RelId (loc, qid) -> + let kn = try Tac2env.locate_projection qid with Not_found -> + user_err ?loc (pr_qualid qid ++ str " is not a projection") + in + Tac2env.interp_projection kn +| AbsKn kn -> + Tac2env.interp_projection kn + +let intern_atm env = function +| AtmInt n -> (GTacAtm (AtmInt n), GTypRef (t_int, [])) +| AtmStr s -> (GTacAtm (AtmStr s), GTypRef (t_string, [])) + +let invalid_pattern ?loc kn t = + let pt = match t with + | GCaseAlg kn' -> pr_typref kn + | GCaseTuple n -> str "tuple" + in + user_err ?loc (str "Invalid pattern, expected a pattern for type " ++ + pr_typref kn ++ str ", found a pattern of type " ++ pt) (** FIXME *) + +(** Pattern view *) + +type glb_patexpr = +| GPatVar of Name.t +| GPatRef of ltac_constructor * glb_patexpr list +| GPatTup of glb_patexpr list + +let rec intern_patexpr env = function +| CPatAny _ -> GPatVar Anonymous +| CPatRef (_, qid, []) -> + begin match get_constructor env qid with + | ArgVar (_, id) -> GPatVar (Name id) + | ArgArg (_, kn) -> GPatRef (kn, []) + end +| CPatRef (_, qid, pl) -> + begin match get_constructor env qid with + | ArgVar (loc, id) -> + user_err ?loc (str "Unbound constructor " ++ Nameops.pr_id id) + | ArgArg (_, kn) -> GPatRef (kn, List.map (fun p -> intern_patexpr env p) pl) + end +| CPatTup (_, pl) -> + GPatTup (List.map (fun p -> intern_patexpr env p) pl) + +type pattern_kind = +| PKind_empty +| PKind_variant of type_constant +| PKind_open of type_constant +| PKind_tuple of int +| PKind_any + +let get_pattern_kind env pl = match pl with +| [] -> PKind_empty +| p :: pl -> + let rec get_kind (p, _) pl = match intern_patexpr env p with + | GPatVar _ -> + begin match pl with + | [] -> PKind_any + | p :: pl -> get_kind p pl + end + | GPatRef (kn, pl) -> + let data = Tac2env.interp_constructor kn in + if Option.is_empty data.cdata_indx then PKind_open data.cdata_type + else PKind_variant data.cdata_type + | GPatTup tp -> PKind_tuple (List.length tp) + in + get_kind p pl + +(** Internalization *) + +let is_constructor env qid = match get_variable env qid with +| ArgArg (TacConstructor _) -> true +| _ -> false + +let rec intern_rec env = function +| CTacAtm (_, atm) -> intern_atm env atm +| CTacRef qid as e -> + begin match get_variable env qid with + | ArgVar (_, id) -> + let sch = Id.Map.find id env.env_var in + (GTacVar id, fresh_mix_type_scheme env sch) + | ArgArg (TacConstant kn) -> + let (_, _, sch) = Tac2env.interp_global kn in + (GTacRef kn, fresh_type_scheme env sch) + | ArgArg (TacConstructor kn) -> + let loc = loc_of_tacexpr e in + intern_constructor env loc kn [] + end +| CTacFun (loc, bnd, e) -> + let fold (env, bnd, tl) ((_, na), t) = + let t = match t with + | None -> GTypVar (fresh_id env) + | Some t -> intern_type env t + in + let env = push_name na (monomorphic t) env in + (env, na :: bnd, t :: tl) + in + let (env, bnd, tl) = List.fold_left fold (env, [], []) bnd in + let bnd = List.rev bnd in + let (e, t) = intern_rec env e in + let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in + (GTacFun (bnd, e), t) +| CTacApp (loc, CTacRef qid, args) as e when is_constructor env qid -> + let kn = match get_variable env qid with + | ArgArg (TacConstructor kn) -> kn + | _ -> assert false + in + let loc = loc_of_tacexpr e in + intern_constructor env loc kn args +| CTacApp (loc, f, args) -> + let (f, ft) = intern_rec env f in + let fold arg (args, t) = + let (arg, argt) = intern_rec env arg in + (arg :: args, GTypArrow (argt, t)) + in + let ret = GTypVar (fresh_id env) in + let (args, t) = List.fold_right fold args ([], ret) in + let () = unify ~loc env ft t in + (GTacApp (f, args), ret) +| CTacLet (loc, false, el, e) -> + let fold accu ((loc, na), _, _) = match na with + | Anonymous -> accu + | Name id -> + if Id.Set.mem id accu then + user_err ?loc (str "Variable " ++ Id.print id ++ str " is bound several \ + times in this matching") + else Id.Set.add id accu + in + let _ = List.fold_left fold Id.Set.empty el in + let fold ((loc, na), tc, e) (el, p) = + let (e, t) = intern_rec env e in + let () = match tc with + | None -> () + | Some tc -> + let tc = intern_type env tc in + unify ?loc env t tc + in + let t = if is_value e then abstract_var env t else monomorphic t in + ((na, e) :: el), ((na, t) :: p) + in + let (el, p) = List.fold_right fold el ([], []) in + let nenv = List.fold_left (fun accu (na, t) -> push_name na t env) env p in + let (e, t) = intern_rec nenv e in + (GTacLet (false, el, e), t) +| CTacLet (loc, true, el, e) -> + intern_let_rec env loc el e +| CTacTup (loc, []) -> + (GTacCst (GCaseAlg t_unit, 0, []), GTypRef (t_unit, [])) +| CTacTup (loc, el) -> + let fold e (el, tl) = + let (e, t) = intern_rec env e in + (e :: el, t :: tl) + in + let (el, tl) = List.fold_right fold el ([], []) in + (GTacCst (GCaseTuple (List.length el), 0, el), GTypTuple tl) +| CTacArr (loc, []) -> + let id = fresh_id env in + (GTacArr [], GTypRef (t_int, [GTypVar id])) +| CTacArr (loc, e0 :: el) -> + let (e0, t0) = intern_rec env e0 in + let fold e el = intern_rec_with_constraint env e t0 :: el in + let el = e0 :: List.fold_right fold el [] in + (GTacArr el, GTypRef (t_array, [t0])) +| CTacLst (loc, []) -> + let id = fresh_id env in + (c_nil, GTypRef (t_list, [GTypVar id])) +| CTacLst (loc, e0 :: el) -> + let (e0, t0) = intern_rec env e0 in + let fold e el = c_cons (intern_rec_with_constraint env e t0) el in + let el = c_cons e0 (List.fold_right fold el c_nil) in + (el, GTypRef (t_list, [t0])) +| CTacCnv (loc, e, tc) -> + let (e, t) = intern_rec env e in + let tc = intern_type env tc in + let () = unify ~loc env t tc in + (e, tc) +| CTacSeq (loc, e1, e2) -> + let (e1, t1) = intern_rec env e1 in + let (e2, t2) = intern_rec env e2 in + let () = check_elt_unit loc env t1 in + (GTacLet (false, [Anonymous, e1], e2), t2) +| CTacCse (loc, e, pl) -> + intern_case env loc e pl +| CTacRec (loc, fs) -> + intern_record env loc fs +| CTacPrj (loc, e, proj) -> + let pinfo = get_projection proj in + let loc = loc_of_tacexpr e in + let (e, t) = intern_rec env e in + let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in + let params = Array.map_to_list (fun i -> GTypVar i) subst in + let exp = GTypRef (pinfo.pdata_type, params) in + let () = unify ~loc env t exp in + let substf i = GTypVar subst.(i) in + let ret = subst_type substf pinfo.pdata_ptyp in + (GTacPrj (pinfo.pdata_type, e, pinfo.pdata_indx), ret) +| CTacSet (loc, e, proj, r) -> + let pinfo = get_projection proj in + let () = + if not pinfo.pdata_mutb then + let loc = match proj with + | RelId (loc, _) -> loc + | AbsKn _ -> None + in + user_err ?loc (str "Field is not mutable") + in + let subst = Array.init pinfo.pdata_prms (fun _ -> fresh_id env) in + let params = Array.map_to_list (fun i -> GTypVar i) subst in + let exp = GTypRef (pinfo.pdata_type, params) in + let e = intern_rec_with_constraint env e exp in + let substf i = GTypVar subst.(i) in + let ret = subst_type substf pinfo.pdata_ptyp in + let r = intern_rec_with_constraint env r ret in + (GTacSet (pinfo.pdata_type, e, pinfo.pdata_indx, r), GTypRef (t_unit, [])) +| CTacExt (loc, ext) -> + let open Genintern in + let GenArg (Rawwit tag, _) = ext in + let tpe = interp_ml_object tag in + (** External objects do not have access to the named context because this is + not stable by dynamic semantics. *) + let genv = Global.env_of_context Environ.empty_named_context_val in + let ist = empty_glob_sign genv in + let ist = { ist with extra = Store.set ist.extra ltac2_env env } in + let (_, ext) = Flags.with_option Ltac_plugin.Tacintern.strict_check (fun () -> generic_intern ist ext) () in + (GTacExt ext, GTypRef (tpe.ml_type, [])) + +and intern_rec_with_constraint env e exp = + let loc = loc_of_tacexpr e in + let (e, t) = intern_rec env e in + let () = unify ~loc env t exp in + e + +and intern_let_rec env loc el e = + let fold accu ((loc, na), _, _) = match na with + | Anonymous -> accu + | Name id -> + if Id.Set.mem id accu then + user_err ?loc (str "Variable " ++ Id.print id ++ str " is bound several \ + times in this matching") + else Id.Set.add id accu + in + let _ = List.fold_left fold Id.Set.empty el in + let map env ((loc, na), t, e) = + let id = fresh_id env in + let env = push_name na (monomorphic (GTypVar id)) env in + (env, (loc, na, t, e, id)) + in + let (env, el) = List.fold_map map env el in + let fold (loc, na, tc, e, id) (el, tl) = + let loc_e = loc_of_tacexpr e in + let (e, t) = intern_rec env e in + let () = + if not (is_rec_rhs e) then + user_err ~loc:loc_e (str "This kind of expression is not allowed as \ + right-hand side of a recursive binding") + in + let () = unify ?loc env t (GTypVar id) in + let () = match tc with + | None -> () + | Some tc -> + let tc = intern_type env tc in + unify ?loc env t tc + in + ((na, e) :: el, t :: tl) + in + let (el, tl) = List.fold_right fold el ([], []) in + let (e, t) = intern_rec env e in + (GTacLet (true, el, e), t) + +(** For now, patterns recognized by the pattern-matching compiling are limited + to depth-one where leaves are either variables or catch-all *) +and intern_case env loc e pl = + let (e', t) = intern_rec env e in + let todo ~loc () = user_err ~loc (str "Pattern not handled yet") in + match get_pattern_kind env pl with + | PKind_any -> + let (pat, b) = List.hd pl in + let na = match intern_patexpr env pat with + | GPatVar na -> na + | _ -> assert false + in + let () = check_redundant_clause (List.tl pl) in + let env = push_name na (monomorphic t) env in + let (b, tb) = intern_rec env b in + (GTacLet (false, [na, e'], b), tb) + | PKind_empty -> + let kn = check_elt_empty loc env t in + let r = fresh_id env in + (GTacCse (e', GCaseAlg kn, [||], [||]), GTypVar r) + | PKind_tuple len -> + begin match pl with + | [] -> assert false + | [CPatTup (_, []), b] -> + let () = unify ~loc:(loc_of_tacexpr e) env t (GTypRef (t_unit, [])) in + let (b, tb) = intern_rec env b in + (GTacCse (e', GCaseAlg t_unit, [|b|], [||]), tb) + | [CPatTup (_, pl), b] -> + let map = function + | CPatAny _ -> Anonymous + | CPatRef (loc, qid, []) -> + begin match get_constructor env qid with + | ArgVar (_, id) -> Name id + | ArgArg _ -> todo ~loc () + end + | p -> todo ~loc:(loc_of_patexpr p) () + in + let ids = Array.map_of_list map pl in + let tc = GTypTuple (List.map (fun _ -> GTypVar (fresh_id env)) pl) in + let () = unify ~loc:(loc_of_tacexpr e) env t tc in + let (b, tb) = intern_rec env b in + (GTacCse (e', GCaseTuple len, [||], [|ids, b|]), tb) + | (p, _) :: _ -> todo ~loc:(loc_of_patexpr p) () + end + | PKind_variant kn -> + let subst, tc = fresh_reftype env kn in + let () = unify ~loc:(loc_of_tacexpr e) env t tc in + let (params, def) = Tac2env.interp_type kn in + let cstrs = match def with + | GTydAlg c -> c + | _ -> assert false + in + let count (const, nonconst) (c, args) = match args with + | [] -> (succ const, nonconst) + | _ :: _ -> (const, succ nonconst) + in + let nconst, nnonconst = List.fold_left count (0, 0) cstrs in + let const = Array.make nconst None in + let nonconst = Array.make nnonconst None in + let ret = GTypVar (fresh_id env) in + let rec intern_branch = function + | [] -> () + | (pat, br) :: rem -> + let tbr = match pat with + | CPatAny _ -> + let () = check_redundant_clause rem in + let (br', brT) = intern_rec env br in + (** Fill all remaining branches *) + let fill (ncst, narg) (_, args) = + if List.is_empty args then + let () = + if Option.is_empty const.(ncst) then const.(ncst) <- Some br' + in + (succ ncst, narg) + else + let () = + if Option.is_empty const.(narg) then + let ids = Array.map_of_list (fun _ -> Anonymous) args in + nonconst.(narg) <- Some (ids, br') + in + (ncst, succ narg) + in + let _ = List.fold_left fill (0, 0) cstrs in + brT + | CPatRef (loc, qid, args) -> + let data = match get_constructor env qid with + | ArgVar _ -> todo ~loc () + | ArgArg (data, _) -> + let () = + let kn' = data.cdata_type in + if not (KerName.equal kn kn') then + invalid_pattern ~loc kn (GCaseAlg kn') + in + data + in + let get_id = function + | CPatAny _ -> Anonymous + | CPatRef (loc, qid, []) -> + begin match get_constructor env qid with + | ArgVar (_, id) -> Name id + | ArgArg _ -> todo ~loc () + end + | p -> todo ~loc:(loc_of_patexpr p) () + in + let ids = List.map get_id args in + let nids = List.length ids in + let nargs = List.length data.cdata_args in + let () = + if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids + in + let fold env id tpe = + (** Instantiate all arguments *) + let subst n = GTypVar subst.(n) in + let tpe = subst_type subst tpe in + push_name id (monomorphic tpe) env + in + let nenv = List.fold_left2 fold env ids data.cdata_args in + let (br', brT) = intern_rec nenv br in + let () = + let index = match data.cdata_indx with + | Some i -> i + | None -> assert false + in + if List.is_empty args then + if Option.is_empty const.(index) then const.(index) <- Some br' + else warn_redundant_clause ~loc () + else + let ids = Array.of_list ids in + if Option.is_empty nonconst.(index) then nonconst.(index) <- Some (ids, br') + else warn_redundant_clause ~loc () + in + brT + | CPatTup (loc, tup) -> + invalid_pattern ?loc kn (GCaseTuple (List.length tup)) + in + let () = unify ~loc:(loc_of_tacexpr br) env ret tbr in + intern_branch rem + in + let () = intern_branch pl in + let map = function + | None -> user_err ~loc (str "TODO: Unhandled match case") (** FIXME *) + | Some x -> x + in + let const = Array.map map const in + let nonconst = Array.map map nonconst in + let ce = GTacCse (e', GCaseAlg kn, const, nonconst) in + (ce, ret) + | PKind_open kn -> + let subst, tc = fresh_reftype env kn in + let () = unify ~loc:(loc_of_tacexpr e) env t tc in + let ret = GTypVar (fresh_id env) in + let rec intern_branch map = function + | [] -> + user_err ~loc (str "Missing default case") + | (pat, br) :: rem -> + match intern_patexpr env pat with + | GPatVar na -> + let () = check_redundant_clause rem in + let nenv = push_name na (monomorphic tc) env in + let br' = intern_rec_with_constraint nenv br ret in + let def = (na, br') in + (map, def) + | GPatRef (knc, args) -> + let get = function + | GPatVar na -> na + | GPatRef _ | GPatTup _ -> + user_err ~loc (str "TODO: Unhandled match case") (** FIXME *) + in + let loc = loc_of_patexpr pat in + let ids = List.map get args in + let data = Tac2env.interp_constructor knc in + let () = + if not (KerName.equal kn data.cdata_type) then + invalid_pattern ~loc kn (GCaseAlg data.cdata_type) + in + let nids = List.length ids in + let nargs = List.length data.cdata_args in + let () = + if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids + in + let fold env id tpe = + (** Instantiate all arguments *) + let subst n = GTypVar subst.(n) in + let tpe = subst_type subst tpe in + push_name id (monomorphic tpe) env + in + let nenv = List.fold_left2 fold env ids data.cdata_args in + let br' = intern_rec_with_constraint nenv br ret in + let map = + if KNmap.mem knc map then + let () = warn_redundant_clause ~loc () in + map + else + KNmap.add knc (Anonymous, Array.of_list ids, br') map + in + intern_branch map rem + | GPatTup tup -> + invalid_pattern ~loc kn (GCaseTuple (List.length tup)) + in + let (map, def) = intern_branch KNmap.empty pl in + (GTacWth { opn_match = e'; opn_branch = map; opn_default = def }, ret) + +and intern_constructor env loc kn args = + let cstr = interp_constructor kn in + let nargs = List.length cstr.cdata_args in + if Int.equal nargs (List.length args) then + let subst = Array.init cstr.cdata_prms (fun _ -> fresh_id env) in + let substf i = GTypVar subst.(i) in + let types = List.map (fun t -> subst_type substf t) cstr.cdata_args in + let ans = GTypRef (cstr.cdata_type, List.init cstr.cdata_prms (fun i -> GTypVar subst.(i))) in + let map arg tpe = intern_rec_with_constraint env arg tpe in + let args = List.map2 map args types in + match cstr.cdata_indx with + | Some idx -> + (GTacCst (GCaseAlg cstr.cdata_type, idx, args), ans) + | None -> + (GTacOpn (kn, args), ans) + else + error_nargs_mismatch loc nargs (List.length args) + +and intern_record env loc fs = + let map (proj, e) = + let loc = match proj with + | RelId (loc, _) -> loc + | AbsKn _ -> None + in + let proj = get_projection proj in + (loc, proj, e) + in + let fs = List.map map fs in + let kn = match fs with + | [] -> user_err ~loc (str "Cannot infer the corresponding record type") + | (_, proj, _) :: _ -> proj.pdata_type + in + let params, typdef = match Tac2env.interp_type kn with + | n, GTydRec def -> n, def + | _ -> assert false + in + let subst = Array.init params (fun _ -> fresh_id env) in + (** Set the answer [args] imperatively *) + let args = Array.make (List.length typdef) None in + let iter (loc, pinfo, e) = + if KerName.equal kn pinfo.pdata_type then + let index = pinfo.pdata_indx in + match args.(index) with + | None -> + let exp = subst_type (fun i -> GTypVar subst.(i)) pinfo.pdata_ptyp in + let e = intern_rec_with_constraint env e exp in + args.(index) <- Some e + | Some _ -> + let (name, _, _) = List.nth typdef pinfo.pdata_indx in + user_err ?loc (str "Field " ++ Id.print name ++ str " is defined \ + several times") + else + user_err ?loc (str "Field " ++ (*KerName.print knp ++*) str " does not \ + pertain to record definition " ++ pr_typref pinfo.pdata_type) + in + let () = List.iter iter fs in + let () = match Array.findi (fun _ o -> Option.is_empty o) args with + | None -> () + | Some i -> + let (field, _, _) = List.nth typdef i in + user_err ~loc (str "Field " ++ Id.print field ++ str " is undefined") + in + let args = Array.map_to_list Option.get args in + let tparam = List.init params (fun i -> GTypVar subst.(i)) in + (GTacCst (GCaseAlg kn, 0, args), GTypRef (kn, tparam)) + +let normalize env (count, vars) (t : UF.elt glb_typexpr) = + let get_var id = + try UF.Map.find id !vars + with Not_found -> + let () = assert env.env_opn in + let n = GTypVar !count in + let () = incr count in + let () = vars := UF.Map.add id n !vars in + n + in + let rec subst id = match UF.find id env.env_cst with + | id, None -> get_var id + | _, Some t -> subst_type subst t + in + subst_type subst t + +let intern e = + let env = empty_env () in + let (e, t) = intern_rec env e in + let count = ref 0 in + let vars = ref UF.Map.empty in + let t = normalize env (count, vars) t in + (e, (!count, t)) + +let intern_typedef self (ids, t) : glb_quant_typedef = + let env = { (empty_env ()) with env_rec = self } in + (** Initialize type parameters *) + let map id = get_alias id env in + let ids = List.map map ids in + let count = ref (List.length ids) in + let vars = ref UF.Map.empty in + let iter n id = vars := UF.Map.add id (GTypVar n) !vars in + let () = List.iteri iter ids in + (** Do not accept unbound type variables *) + let env = { env with env_opn = false } in + let intern t = + let t = intern_type env t in + normalize env (count, vars) t + in + let count = !count in + match t with + | CTydDef None -> (count, GTydDef None) + | CTydDef (Some t) -> (count, GTydDef (Some (intern t))) + | CTydAlg constrs -> + let map (c, t) = (c, List.map intern t) in + let constrs = List.map map constrs in + (count, GTydAlg constrs) + | CTydRec fields -> + let map (c, mut, t) = (c, mut, intern t) in + let fields = List.map map fields in + (count, GTydRec fields) + | CTydOpn -> (count, GTydOpn) + +let intern_open_type t = + let env = empty_env () in + let t = intern_type env t in + let count = ref 0 in + let vars = ref UF.Map.empty in + let t = normalize env (count, vars) t in + (!count, t) + +(** Globalization *) + +let add_name accu = function +| Name id -> Id.Set.add id accu +| Anonymous -> accu + +let get_projection0 var = match var with +| RelId (loc, qid) -> + let kn = try Tac2env.locate_projection qid with Not_found -> + user_err ?loc (pr_qualid qid ++ str " is not a projection") + in + kn +| AbsKn kn -> kn + +let rec globalize ids e = match e with +| CTacAtm _ -> e +| CTacRef ref -> + let mem id = Id.Set.mem id ids in + begin match get_variable0 mem ref with + | ArgVar _ -> e + | ArgArg kn -> CTacRef (AbsKn kn) + end +| CTacFun (loc, bnd, e) -> + let fold accu ((_, na), _) = add_name accu na in + let ids = List.fold_left fold ids bnd in + let e = globalize ids e in + CTacFun (loc, bnd, e) +| CTacApp (loc, e, el) -> + let e = globalize ids e in + let el = List.map (fun e -> globalize ids e) el in + CTacApp (loc, e, el) +| CTacLet (loc, isrec, bnd, e) -> + let fold accu ((_, na), _, _) = add_name accu na in + let ext = List.fold_left fold Id.Set.empty bnd in + let eids = Id.Set.union ext ids in + let e = globalize eids e in + let map (qid, t, e) = + let ids = if isrec then eids else ids in + (qid, t, globalize ids e) + in + let bnd = List.map map bnd in + CTacLet (loc, isrec, bnd, e) +| CTacTup (loc, el) -> + let el = List.map (fun e -> globalize ids e) el in + CTacTup (loc, el) +| CTacArr (loc, el) -> + let el = List.map (fun e -> globalize ids e) el in + CTacArr (loc, el) +| CTacLst (loc, el) -> + let el = List.map (fun e -> globalize ids e) el in + CTacLst (loc, el) +| CTacCnv (loc, e, t) -> + let e = globalize ids e in + CTacCnv (loc, e, t) +| CTacSeq (loc, e1, e2) -> + let e1 = globalize ids e1 in + let e2 = globalize ids e2 in + CTacSeq (loc, e1, e2) +| CTacCse (loc, e, bl) -> + let e = globalize ids e in + let bl = List.map (fun b -> globalize_case ids b) bl in + CTacCse (loc, e, bl) +| CTacRec (loc, r) -> + let map (p, e) = + let p = get_projection0 p in + let e = globalize ids e in + (AbsKn p, e) + in + CTacRec (loc, List.map map r) +| CTacPrj (loc, e, p) -> + let e = globalize ids e in + let p = get_projection0 p in + CTacPrj (loc, e, AbsKn p) +| CTacSet (loc, e, p, e') -> + let e = globalize ids e in + let p = get_projection0 p in + let e' = globalize ids e' in + CTacSet (loc, e, AbsKn p, e') +| CTacExt (loc, arg) -> + let arg = pr_argument_type (genarg_tag arg) in + CErrors.user_err ~loc (str "Cannot globalize generic arguments of type" ++ spc () ++ arg) + +and globalize_case ids (p, e) = + (globalize_pattern ids p, globalize ids e) + +and globalize_pattern ids p = match p with +| CPatAny _ -> p +| CPatRef (loc, cst, pl) -> + let cst = match get_constructor () cst with + | ArgVar _ -> cst + | ArgArg (_, knc) -> AbsKn knc + in + let pl = List.map (fun p -> globalize_pattern ids p) pl in + CPatRef (loc, cst, pl) +| CPatTup (loc, pl) -> + let pl = List.map (fun p -> globalize_pattern ids p) pl in + CPatTup (loc, pl) + +(** Kernel substitution *) + +open Mod_subst + +let rec subst_type subst t = match t with +| GTypVar _ -> t +| GTypArrow (t1, t2) -> + let t1' = subst_type subst t1 in + let t2' = subst_type subst t2 in + if t1' == t1 && t2' == t2 then t + else GTypArrow (t1', t2') +| GTypTuple tl -> + let tl'= List.smartmap (fun t -> subst_type subst t) tl in + if tl' == tl then t else GTypTuple tl' +| GTypRef (kn, tl) -> + let kn' = subst_kn subst kn in + let tl' = List.smartmap (fun t -> subst_type subst t) tl in + if kn' == kn && tl' == tl then t else GTypRef (kn', tl') + +let subst_case_info subst ci = match ci with +| GCaseAlg kn -> + let kn' = subst_kn subst kn in + if kn' == kn then ci else GCaseAlg kn' +| GCaseTuple _ -> ci + +let rec subst_expr subst e = match e with +| GTacAtm _ | GTacVar _ | GTacPrm _ -> e +| GTacRef kn -> GTacRef (subst_kn subst kn) +| GTacFun (ids, e) -> GTacFun (ids, subst_expr subst e) +| GTacApp (f, args) -> + GTacApp (subst_expr subst f, List.map (fun e -> subst_expr subst e) args) +| GTacLet (r, bs, e) -> + let bs = List.map (fun (na, e) -> (na, subst_expr subst e)) bs in + GTacLet (r, bs, subst_expr subst e) +| GTacArr el -> + GTacArr (List.map (fun e -> subst_expr subst e) el) +| GTacCst (t, n, el) as e0 -> + let t' = match t with + | GCaseAlg kn -> + let kn' = subst_kn subst kn in + if kn' == kn then t else GCaseAlg kn' + | GCaseTuple _ -> t + in + let el' = List.smartmap (fun e -> subst_expr subst e) el in + if t' == t && el' == el then e0 else GTacCst (t', n, el') +| GTacCse (e, ci, cse0, cse1) -> + let cse0' = Array.map (fun e -> subst_expr subst e) cse0 in + let cse1' = Array.map (fun (ids, e) -> (ids, subst_expr subst e)) cse1 in + let ci' = subst_case_info subst ci in + GTacCse (subst_expr subst e, ci', cse0', cse1') +| GTacWth { opn_match = e; opn_branch = br; opn_default = (na, def) } as e0 -> + let e' = subst_expr subst e in + let def' = subst_expr subst def in + let fold kn (self, vars, p) accu = + let kn' = subst_kn subst kn in + let p' = subst_expr subst p in + if kn' == kn && p' == p then accu + else KNmap.add kn' (self, vars, p') (KNmap.remove kn accu) + in + let br' = KNmap.fold fold br br in + if e' == e && br' == br && def' == def then e0 + else GTacWth { opn_match = e'; opn_default = (na, def'); opn_branch = br' } +| GTacPrj (kn, e, p) as e0 -> + let kn' = subst_kn subst kn in + let e' = subst_expr subst e in + if kn' == kn && e' == e then e0 else GTacPrj (kn', e', p) +| GTacSet (kn, e, p, r) as e0 -> + let kn' = subst_kn subst kn in + let e' = subst_expr subst e in + let r' = subst_expr subst r in + if kn' == kn && e' == e && r' == r then e0 else GTacSet (kn', e', p, r') +| GTacExt ext -> + let ext' = Genintern.generic_substitute subst ext in + if ext' == ext then e else GTacExt ext' +| GTacOpn (kn, el) as e0 -> + let kn' = subst_kn subst kn in + let el' = List.smartmap (fun e -> subst_expr subst e) el in + if kn' == kn && el' == el then e0 else GTacOpn (kn', el') + +let subst_typedef subst e = match e with +| GTydDef t -> + let t' = Option.smartmap (fun t -> subst_type subst t) t in + if t' == t then e else GTydDef t' +| GTydAlg constrs -> + let map (c, tl as p) = + let tl' = List.smartmap (fun t -> subst_type subst t) tl in + if tl' == tl then p else (c, tl') + in + let constrs' = List.smartmap map constrs in + if constrs' == constrs then e else GTydAlg constrs' +| GTydRec fields -> + let map (c, mut, t as p) = + let t' = subst_type subst t in + if t' == t then p else (c, mut, t') + in + let fields' = List.smartmap map fields in + if fields' == fields then e else GTydRec fields' +| GTydOpn -> GTydOpn + +let subst_quant_typedef subst (prm, def as qdef) = + let def' = subst_typedef subst def in + if def' == def then qdef else (prm, def') + +let subst_type_scheme subst (prm, t as sch) = + let t' = subst_type subst t in + if t' == t then sch else (prm, t') + +let subst_or_relid subst ref = match ref with +| RelId _ -> ref +| AbsKn kn -> + let kn' = subst_kn subst kn in + if kn' == kn then ref else AbsKn kn' + +let rec subst_rawtype subst t = match t with +| CTypVar _ -> t +| CTypArrow (loc, t1, t2) -> + let t1' = subst_rawtype subst t1 in + let t2' = subst_rawtype subst t2 in + if t1' == t1 && t2' == t2 then t else CTypArrow (loc, t1', t2') +| CTypTuple (loc, tl) -> + let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in + if tl' == tl then t else CTypTuple (loc, tl') +| CTypRef (loc, ref, tl) -> + let ref' = subst_or_relid subst ref in + let tl' = List.smartmap (fun t -> subst_rawtype subst t) tl in + if ref' == ref && tl' == tl then t else CTypRef (loc, ref', tl') + +let subst_tacref subst ref = match ref with +| RelId _ -> ref +| AbsKn (TacConstant kn) -> + let kn' = subst_kn subst kn in + if kn' == kn then ref else AbsKn (TacConstant kn') +| AbsKn (TacConstructor kn) -> + let kn' = subst_kn subst kn in + if kn' == kn then ref else AbsKn (TacConstructor kn') + +let subst_projection subst prj = match prj with +| RelId _ -> prj +| AbsKn kn -> + let kn' = subst_kn subst kn in + if kn' == kn then prj else AbsKn kn' + +let rec subst_rawpattern subst p = match p with +| CPatAny _ -> p +| CPatRef (loc, c, pl) -> + let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in + let c' = match c with + | RelId _ -> c + | AbsKn kn -> + let kn' = subst_kn subst kn in + if kn' == kn then c else AbsKn kn' + in + if pl' == pl && c' == c then p else CPatRef (loc, c', pl') +| CPatTup (loc, pl) -> + let pl' = List.smartmap (fun p -> subst_rawpattern subst p) pl in + if pl' == pl then p else CPatTup (loc, pl') + +(** Used for notations *) +let rec subst_rawexpr subst t = match t with +| CTacAtm _ -> t +| CTacRef ref -> + let ref' = subst_tacref subst ref in + if ref' == ref then t else CTacRef ref' +| CTacFun (loc, bnd, e) -> + let map (na, t as p) = + let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in + if t' == t then p else (na, t') + in + let bnd' = List.smartmap map bnd in + let e' = subst_rawexpr subst e in + if bnd' == bnd && e' == e then t else CTacFun (loc, bnd', e') +| CTacApp (loc, e, el) -> + let e' = subst_rawexpr subst e in + let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in + if e' == e && el' == el then t else CTacApp (loc, e', el') +| CTacLet (loc, isrec, bnd, e) -> + let map (na, t, e as p) = + let t' = Option.smartmap (fun t -> subst_rawtype subst t) t in + let e' = subst_rawexpr subst e in + if t' == t && e' == e then p else (na, t', e') + in + let bnd' = List.smartmap map bnd in + let e' = subst_rawexpr subst e in + if bnd' == bnd && e' == e then t else CTacLet (loc, isrec, bnd', e') +| CTacTup (loc, el) -> + let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in + if el' == el then t else CTacTup (loc, el') +| CTacArr (loc, el) -> + let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in + if el' == el then t else CTacArr (loc, el') +| CTacLst (loc, el) -> + let el' = List.smartmap (fun e -> subst_rawexpr subst e) el in + if el' == el then t else CTacLst (loc, el') +| CTacCnv (loc, e, c) -> + let e' = subst_rawexpr subst e in + let c' = subst_rawtype subst c in + if c' == c && e' == e then t else CTacCnv (loc, e', c') +| CTacSeq (loc, e1, e2) -> + let e1' = subst_rawexpr subst e1 in + let e2' = subst_rawexpr subst e2 in + if e1' == e1 && e2' == e2 then t else CTacSeq (loc, e1', e2') +| CTacCse (loc, e, bl) -> + let map (p, e as x) = + let p' = subst_rawpattern subst p in + let e' = subst_rawexpr subst e in + if p' == p && e' == e then x else (p', e') + in + let e' = subst_rawexpr subst e in + let bl' = List.smartmap map bl in + if e' == e && bl' == bl then t else CTacCse (loc, e', bl') +| CTacRec (loc, el) -> + let map (prj, e as p) = + let prj' = subst_projection subst prj in + let e' = subst_rawexpr subst e in + if prj' == prj && e' == e then p else (prj', e') + in + let el' = List.smartmap map el in + if el' == el then t else CTacRec (loc, el') +| CTacPrj (loc, e, prj) -> + let prj' = subst_projection subst prj in + let e' = subst_rawexpr subst e in + if prj' == prj && e' == e then t else CTacPrj (loc, e', prj') +| CTacSet (loc, e, prj, r) -> + let prj' = subst_projection subst prj in + let e' = subst_rawexpr subst e in + let r' = subst_rawexpr subst r in + if prj' == prj && e' == e && r' == r then t else CTacSet (loc, e', prj', r') +| CTacExt _ -> assert false (** Should not be generated by gloabalization *) + +(** Registering *) + +let () = + let open Genintern in + let intern ist tac = + let env = match Genintern.Store.get ist.extra ltac2_env with + | None -> empty_env () + | Some env -> env + in + let loc = loc_of_tacexpr tac in + let (tac, t) = intern_rec env tac in + let () = check_elt_unit loc env t in + (ist, tac) + in + Genintern.register_intern0 wit_ltac2 intern +let () = Genintern.register_subst0 wit_ltac2 subst_expr diff --git a/src/tac2intern.mli b/src/tac2intern.mli new file mode 100644 index 0000000000..3d400a5cdd --- /dev/null +++ b/src/tac2intern.mli @@ -0,0 +1,41 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Genarg +open Names +open Mod_subst +open Tac2expr + +val loc_of_tacexpr : raw_tacexpr -> Loc.t + +val intern : raw_tacexpr -> glb_tacexpr * type_scheme +val intern_typedef : (KerName.t * int) Id.Map.t -> raw_quant_typedef -> glb_quant_typedef +val intern_open_type : raw_typexpr -> type_scheme + +(** Check that a term is a value. Only values are safe to marshall between + processes. *) +val is_value : glb_tacexpr -> bool +val check_unit : ?loc:Loc.t -> int glb_typexpr -> unit + +val subst_type : substitution -> 'a glb_typexpr -> 'a glb_typexpr +val subst_expr : substitution -> glb_tacexpr -> glb_tacexpr +val subst_quant_typedef : substitution -> glb_quant_typedef -> glb_quant_typedef +val subst_type_scheme : substitution -> type_scheme -> type_scheme + +val subst_rawexpr : substitution -> raw_tacexpr -> raw_tacexpr + +(** {5 Notations} *) + +val globalize : Id.Set.t -> raw_tacexpr -> raw_tacexpr +(** Replaces all qualified identifiers by their corresponding kernel name. The + set represents bound variables in the context. *) + +(** Errors *) + +val error_nargs_mismatch : Loc.t -> int -> int -> 'a +val error_nparams_mismatch : Loc.t -> int -> int -> 'a diff --git a/src/tac2interp.ml b/src/tac2interp.ml new file mode 100644 index 0000000000..664b7de3d6 --- /dev/null +++ b/src/tac2interp.ml @@ -0,0 +1,160 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open CErrors +open Genarg +open Names +open Proofview.Notations +open Tac2expr + +exception LtacError of KerName.t * valexpr array + +let () = register_handler begin function +| LtacError (kn, _) -> + let c = Tac2print.pr_constructor kn in + hov 0 (str "Uncaught Ltac2 exception:" ++ spc () ++ hov 0 c) +| _ -> raise Unhandled +end + +let val_exn = Geninterp.Val.create "ltac2:exn" + +type environment = valexpr Id.Map.t + +let empty_environment = Id.Map.empty + +let push_name ist id v = match id with +| Anonymous -> ist +| Name id -> Id.Map.add id v ist + +let get_var ist id = + try Id.Map.find id ist with Not_found -> + anomaly (str "Unbound variable " ++ Id.print id) + +let get_ref ist kn = + try pi2 (Tac2env.interp_global kn) with Not_found -> + anomaly (str "Unbound reference" ++ KerName.print kn) + +let return = Proofview.tclUNIT + +let rec interp ist = function +| GTacAtm (AtmInt n) -> return (ValInt n) +| GTacAtm (AtmStr s) -> return (ValStr (Bytes.of_string s)) +| GTacVar id -> return (get_var ist id) +| GTacRef qid -> return (get_ref ist qid) +| GTacFun (ids, e) -> + let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in + return (ValCls cls) +| GTacApp (f, args) -> + interp ist f >>= fun f -> + Proofview.Monad.List.map (fun e -> interp ist e) args >>= fun args -> + interp_app f args +| GTacLet (false, el, e) -> + let fold accu (na, e) = + interp ist e >>= fun e -> + return (push_name accu na e) + in + Proofview.Monad.List.fold_left fold ist el >>= fun ist -> + interp ist e +| GTacLet (true, el, e) -> + let map (na, e) = match e with + | GTacFun (ids, e) -> + let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in + na, cls + | _ -> anomaly (str "Ill-formed recursive function") + in + let fixs = List.map map el in + let fold accu (na, cls) = match na with + | Anonymous -> accu + | Name id -> Id.Map.add id (ValCls cls) accu + in + let ist = List.fold_left fold ist fixs in + (** Hack to make a cycle imperatively in the environment *) + let iter (_, e) = e.clos_env <- ist in + let () = List.iter iter fixs in + interp ist e +| GTacArr el -> + Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el -> + return (ValBlk (0, Array.of_list el)) +| GTacCst (_, n, []) -> return (ValInt n) +| GTacCst (_, n, el) -> + Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el -> + return (ValBlk (n, Array.of_list el)) +| GTacCse (e, _, cse0, cse1) -> + interp ist e >>= fun e -> interp_case ist e cse0 cse1 +| GTacWth { opn_match = e; opn_branch = cse; opn_default = def } -> + interp ist e >>= fun e -> interp_with ist e cse def +| GTacPrj (_, e, p) -> + interp ist e >>= fun e -> interp_proj ist e p +| GTacSet (_, e, p, r) -> + interp ist e >>= fun e -> + interp ist r >>= fun r -> + interp_set ist e p r +| GTacOpn (kn, el) -> + Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el -> + return (ValOpn (kn, Array.of_list el)) +| GTacPrm (ml, el) -> + Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el -> + Tac2env.interp_primitive ml el +| GTacExt e -> + let GenArg (Glbwit tag, e) = e in + let tpe = Tac2env.interp_ml_object tag in + tpe.Tac2env.ml_interp ist e >>= fun e -> return (ValExt e) + +and interp_app f args = match f with +| ValCls { clos_env = ist; clos_var = ids; clos_exp = e } -> + let rec push ist ids args = match ids, args with + | [], [] -> interp ist e + | [], _ :: _ -> interp ist e >>= fun f -> interp_app f args + | _ :: _, [] -> + let cls = { clos_env = ist; clos_var = ids; clos_exp = e } in + return (ValCls cls) + | id :: ids, arg :: args -> push (push_name ist id arg) ids args + in + push ist ids args +| ValExt _ | ValInt _ | ValBlk _ | ValStr _ | ValOpn _ -> + anomaly (str "Unexpected value shape") + +and interp_case ist e cse0 cse1 = match e with +| ValInt n -> interp ist cse0.(n) +| ValBlk (n, args) -> + let (ids, e) = cse1.(n) in + let ist = CArray.fold_left2 push_name ist ids args in + interp ist e +| ValExt _ | ValStr _ | ValCls _ | ValOpn _ -> + anomaly (str "Unexpected value shape") + +and interp_with ist e cse def = match e with +| ValOpn (kn, args) -> + let br = try Some (KNmap.find kn cse) with Not_found -> None in + begin match br with + | None -> + let (self, def) = def in + let ist = push_name ist self e in + interp ist def + | Some (self, ids, p) -> + let ist = push_name ist self e in + let ist = CArray.fold_left2 push_name ist ids args in + interp ist p + end +| ValInt _ | ValBlk _ | ValExt _ | ValStr _ | ValCls _ -> + anomaly (str "Unexpected value shape") + +and interp_proj ist e p = match e with +| ValBlk (_, args) -> + return args.(p) +| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ -> + anomaly (str "Unexpected value shape") + +and interp_set ist e p r = match e with +| ValBlk (_, args) -> + let () = args.(p) <- r in + return (ValInt 0) +| ValInt _ | ValExt _ | ValStr _ | ValCls _ | ValOpn _ -> + anomaly (str "Unexpected value shape") diff --git a/src/tac2interp.mli b/src/tac2interp.mli new file mode 100644 index 0000000000..bf6b2d4dde --- /dev/null +++ b/src/tac2interp.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Genarg +open Names +open Tac2expr + +type environment = valexpr Id.Map.t + +val empty_environment : environment + +val interp : environment -> glb_tacexpr -> valexpr Proofview.tactic + +val interp_app : valexpr -> valexpr list -> valexpr Proofview.tactic + +(** {5 Exceptions} *) + +exception LtacError of KerName.t * valexpr array +(** Ltac2-defined exceptions seen from OCaml side *) + +val val_exn : Exninfo.iexn Geninterp.Val.typ +(** Toplevel representation of OCaml exceptions. Invariant: no [LtacError] + should be put into a value with tag [val_exn]. *) diff --git a/src/tac2print.ml b/src/tac2print.ml new file mode 100644 index 0000000000..e6f0582e3d --- /dev/null +++ b/src/tac2print.ml @@ -0,0 +1,296 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Util +open Pp +open Genarg +open Names +open Tac2expr +open Tac2env + +(** Utils *) + +let change_kn_label kn id = + let (mp, dp, _) = KerName.repr kn in + KerName.make mp dp (Label.of_id id) + +let paren p = hov 2 (str "(" ++ p ++ str ")") + +(** Type printing *) + +type typ_level = +| T5_l +| T5_r +| T2 +| T1 +| T0 + +let pr_typref kn = + Libnames.pr_qualid (Tac2env.shortest_qualid_of_type kn) + +let pr_glbtype_gen pr lvl c = + let rec pr_glbtype lvl = function + | GTypVar n -> str "'" ++ str (pr n) + | GTypRef (kn, []) -> pr_typref kn + | GTypRef (kn, [t]) -> + let paren = match lvl with + | T5_r | T5_l | T2 | T1 -> fun x -> x + | T0 -> paren + in + paren (pr_glbtype lvl t ++ spc () ++ pr_typref kn) + | GTypRef (kn, tl) -> + let paren = match lvl with + | T5_r | T5_l | T2 | T1 -> fun x -> x + | T0 -> paren + in + paren (str "(" ++ prlist_with_sep (fun () -> str ", ") (pr_glbtype lvl) tl ++ str ")" ++ spc () ++ pr_typref kn) + | GTypArrow (t1, t2) -> + let paren = match lvl with + | T5_r -> fun x -> x + | T5_l | T2 | T1 | T0 -> paren + in + paren (pr_glbtype T5_l t1 ++ spc () ++ str "->" ++ spc () ++ pr_glbtype T5_r t2) + | GTypTuple tl -> + let paren = match lvl with + | T5_r | T5_l -> fun x -> x + | T2 | T1 | T0 -> paren + in + paren (prlist_with_sep (fun () -> str " * ") (pr_glbtype T2) tl) + in + hov 0 (pr_glbtype lvl c) + +let pr_glbtype pr c = pr_glbtype_gen pr T5_r c + +let int_name () = + let vars = ref Int.Map.empty in + fun n -> + if Int.Map.mem n !vars then Int.Map.find n !vars + else + let num = Int.Map.cardinal !vars in + let base = num mod 26 in + let rem = num / 26 in + let name = String.make 1 (Char.chr (97 + base)) in + let suff = if Int.equal rem 0 then "" else string_of_int rem in + let name = name ^ suff in + let () = vars := Int.Map.add n name !vars in + name + +(** Term printing *) + +let pr_constructor kn = + Libnames.pr_qualid (Tac2env.shortest_qualid_of_ltac (TacConstructor kn)) + +let pr_projection kn = + Libnames.pr_qualid (Tac2env.shortest_qualid_of_projection kn) + +type exp_level = Tac2expr.exp_level = +| E5 +| E4 +| E3 +| E2 +| E1 +| E0 + +let pr_atom = function +| AtmInt n -> int n +| AtmStr s -> qstring s + +let pr_name = function +| Name id -> Id.print id +| Anonymous -> str "_" + +let find_constructor n empty def = + let rec find n = function + | [] -> assert false + | (id, []) :: rem -> + if empty then + if Int.equal n 0 then id + else find (pred n) rem + else find n rem + | (id, _ :: _) :: rem -> + if not empty then + if Int.equal n 0 then id + else find (pred n) rem + else find n rem + in + find n def + +let order_branches cbr nbr def = + let rec order cidx nidx def = match def with + | [] -> [] + | (id, []) :: rem -> + let ans = order (succ cidx) nidx rem in + (id, [], cbr.(cidx)) :: ans + | (id, _ :: _) :: rem -> + let ans = order cidx (succ nidx) rem in + let (vars, e) = nbr.(nidx) in + (id, Array.to_list vars, e) :: ans + in + order 0 0 def + +let pr_glbexpr_gen lvl c = + let rec pr_glbexpr lvl = function + | GTacAtm atm -> pr_atom atm + | GTacVar id -> Id.print id + | GTacRef gr -> + let qid = shortest_qualid_of_ltac (TacConstant gr) in + Libnames.pr_qualid qid + | GTacFun (nas, c) -> + let nas = pr_sequence pr_name nas in + let paren = match lvl with + | E0 | E1 | E2 | E3 | E4 -> paren + | E5 -> fun x -> x + in + paren (str "fun" ++ spc () ++ nas ++ spc () ++ str "=>" ++ spc () ++ + hov 0 (pr_glbexpr E5 c)) + | GTacApp (c, cl) -> + let paren = match lvl with + | E0 -> paren + | E1 | E2 | E3 | E4 | E5 -> fun x -> x + in + paren (pr_glbexpr E1 c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)) + | GTacLet (mut, bnd, e) -> + let paren = match lvl with + | E0 | E1 | E2 | E3 | E4 -> paren + | E5 -> fun x -> x + in + let mut = if mut then str "rec" ++ spc () else mt () in + let pr_bnd (na, e) = + pr_name na ++ spc () ++ str ":=" ++ spc () ++ hov 2 (pr_glbexpr E5 e) ++ spc () + in + let bnd = prlist_with_sep (fun () -> str "with" ++ spc ()) pr_bnd bnd in + paren (str "let" ++ spc () ++ mut ++ bnd ++ str "in" ++ spc () ++ pr_glbexpr E5 e) + | GTacCst (GCaseTuple _, _, cl) -> + let paren = match lvl with + | E0 | E1 -> paren + | E2 | E3 | E4 | E5 -> fun x -> x + in + paren (prlist_with_sep (fun () -> str "," ++ spc ()) (pr_glbexpr E1) cl) + | GTacArr cl -> + mt () (** FIXME when implemented *) + | GTacCst (GCaseAlg tpe, n, cl) -> + begin match Tac2env.interp_type tpe with + | _, GTydAlg def -> + let paren = match lvl with + | E0 -> paren + | E1 | E2 | E3 | E4 | E5 -> fun x -> x + in + let id = find_constructor n (List.is_empty cl) def in + let kn = change_kn_label tpe id in + let cl = match cl with + | [] -> mt () + | _ -> spc () ++ pr_sequence (pr_glbexpr E0) cl + in + paren (pr_constructor kn ++ cl) + | _, GTydRec def -> + let args = List.combine def cl in + let pr_arg ((id, _, _), arg) = + let kn = change_kn_label tpe id in + pr_projection kn ++ spc () ++ str ":=" ++ spc () ++ pr_glbexpr E1 arg + in + let args = prlist_with_sep (fun () -> str ";" ++ spc ()) pr_arg args in + str "{" ++ spc () ++ args ++ spc () ++ str "}" + | _, (GTydDef _ | GTydOpn) -> assert false + end + | GTacCse (e, info, cst_br, ncst_br) -> + let e = pr_glbexpr E5 e in + let br = match info with + | GCaseAlg kn -> + let def = match Tac2env.interp_type kn with + | _, GTydAlg def -> def + | _, GTydDef _ | _, GTydRec _ | _, GTydOpn -> assert false + in + let br = order_branches cst_br ncst_br def in + let pr_branch (cstr, vars, p) = + let cstr = change_kn_label kn cstr in + let cstr = pr_constructor cstr in + let vars = match vars with + | [] -> mt () + | _ -> spc () ++ pr_sequence pr_name vars + in + hov 0 (str "|" ++ spc () ++ cstr ++ vars ++ spc () ++ str "=>" ++ spc () ++ + hov 2 (pr_glbexpr E5 p)) ++ spc () + in + prlist pr_branch br + | GCaseTuple n -> + let (vars, p) = ncst_br.(0) in + let p = pr_glbexpr E5 p in + let vars = prvect_with_sep (fun () -> str "," ++ spc ()) pr_name vars in + str "|" ++ spc () ++ paren vars ++ spc () ++ str "=>" ++ spc () ++ p + in + hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end") + | GTacWth wth -> + let e = pr_glbexpr E5 wth.opn_match in + let pr_pattern c self vars p = + let self = match self with + | Anonymous -> mt () + | Name id -> spc () ++ str "as" ++ spc () ++ Id.print id + in + hov 0 (str "|" ++ spc () ++ c ++ vars ++ self ++ spc () ++ str "=>" ++ spc () ++ + hov 2 (pr_glbexpr E5 p)) ++ spc () + in + let pr_branch (cstr, (self, vars, p)) = + let cstr = pr_constructor cstr in + let vars = match Array.to_list vars with + | [] -> mt () + | vars -> spc () ++ pr_sequence pr_name vars + in + pr_pattern cstr self vars p + in + let br = prlist pr_branch (KNmap.bindings wth.opn_branch) in + let (def_as, def_p) = wth.opn_default in + let def = pr_pattern (str "_") def_as (mt ()) def_p in + let br = br ++ def in + hov 0 (hov 0 (str "match" ++ spc () ++ e ++ spc () ++ str "with") ++ spc () ++ Pp.v 0 br ++ str "end") + | GTacPrj (kn, e, n) -> + let def = match Tac2env.interp_type kn with + | _, GTydRec def -> def + | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false + in + let (proj, _, _) = List.nth def n in + let proj = change_kn_label kn proj in + let proj = pr_projection proj in + let e = pr_glbexpr E0 e in + e ++ str "." ++ paren proj + | GTacSet (kn, e, n, r) -> + let def = match Tac2env.interp_type kn with + | _, GTydRec def -> def + | _, GTydDef _ | _, GTydAlg _ | _, GTydOpn -> assert false + in + let (proj, _, _) = List.nth def n in + let proj = change_kn_label kn proj in + let proj = pr_projection proj in + let e = pr_glbexpr E0 e in + let r = pr_glbexpr E1 r in + e ++ str "." ++ paren proj ++ spc () ++ str ":=" ++ spc () ++ r + | GTacOpn (kn, cl) -> + let paren = match lvl with + | E0 -> paren + | E1 | E2 | E3 | E4 | E5 -> fun x -> x + in + let c = pr_constructor kn in + paren (c ++ spc () ++ (pr_sequence (pr_glbexpr E0) cl)) + | GTacExt arg -> + let GenArg (Glbwit tag, arg) = arg in + let name = match tag with + | ExtraArg tag -> ArgT.repr tag + | _ -> assert false + in + str name ++ str ":" ++ paren (Genprint.glb_print tag arg) + | GTacPrm (prm, args) -> + let args = match args with + | [] -> mt () + | _ -> spc () ++ pr_sequence (pr_glbexpr E0) args + in + str "@external" ++ spc () ++ qstring prm.mltac_plugin ++ spc () ++ + qstring prm.mltac_tactic ++ args + in + hov 0 (pr_glbexpr lvl c) + +let pr_glbexpr c = + pr_glbexpr_gen E5 c diff --git a/src/tac2print.mli b/src/tac2print.mli new file mode 100644 index 0000000000..ddd599641d --- /dev/null +++ b/src/tac2print.mli @@ -0,0 +1,37 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Pp +open Names +open Tac2expr + +(** {5 Printing types} *) + +type typ_level = +| T5_l +| T5_r +| T2 +| T1 +| T0 + +val pr_typref : type_constant -> std_ppcmds +val pr_glbtype_gen : ('a -> string) -> typ_level -> 'a glb_typexpr -> std_ppcmds +val pr_glbtype : ('a -> string) -> 'a glb_typexpr -> std_ppcmds + +(** {5 Printing expressions} *) + +val pr_constructor : ltac_constructor -> std_ppcmds +val pr_projection : ltac_projection -> std_ppcmds +val pr_glbexpr_gen : exp_level -> glb_tacexpr -> std_ppcmds +val pr_glbexpr : glb_tacexpr -> std_ppcmds + +(** {5 Utilities} *) + +val int_name : unit -> (int -> string) +(** Create a function that give names to integers. The names are generated on + the fly, in the order they are encountered. *) |