From 94f4ade387013a2e3fe8d1042fbd152088ce1daa Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 3 Oct 2016 14:46:58 +0200 Subject: Introduction of the Ltac2 plugin. For now, it is only a simple mini-ML whose effects are the proofview monad. There is no facility to manipulate terms nor any hardwired tactic. Pattern-matching is restricted to superficial constructors, the language is lacking a lot of user-friendly interfaces, the grammar is crappy, and much more. --- Ltac2.v | 42 +++ g_ltac2.ml4 | 206 ++++++++++++ ltac2_plugin.mlpack | 6 + tac2core.ml | 119 +++++++ tac2core.mli | 34 ++ tac2entries.ml | 321 ++++++++++++++++++ tac2entries.mli | 33 ++ tac2env.ml | 139 ++++++++ tac2env.mli | 58 ++++ tac2expr.mli | 136 ++++++++ tac2intern.ml | 921 ++++++++++++++++++++++++++++++++++++++++++++++++++++ tac2intern.mli | 30 ++ tac2interp.ml | 108 ++++++ tac2interp.mli | 19 ++ vo.itarget | 1 + 15 files changed, 2173 insertions(+) create mode 100644 Ltac2.v create mode 100644 g_ltac2.ml4 create mode 100644 ltac2_plugin.mlpack create mode 100644 tac2core.ml create mode 100644 tac2core.mli create mode 100644 tac2entries.ml create mode 100644 tac2entries.mli create mode 100644 tac2env.ml create mode 100644 tac2env.mli create mode 100644 tac2expr.mli create mode 100644 tac2intern.ml create mode 100644 tac2intern.mli create mode 100644 tac2interp.ml create mode 100644 tac2interp.mli create mode 100644 vo.itarget diff --git a/Ltac2.v b/Ltac2.v new file mode 100644 index 0000000000..a952524e71 --- /dev/null +++ b/Ltac2.v @@ -0,0 +1,42 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* unit := "ltac2" "print". +Ltac2 @ external of_string : string -> message := "ltac2" "message_of_string". +Ltac2 @ external of_int : int -> message := "ltac2" "message_of_int". + +End Message. + +Module Array. + +Ltac2 @external make : int -> 'a -> ('a) array := "ltac2" "array_make". +Ltac2 @external length : ('a) array -> int := "ltac2" "array_length". +Ltac2 @external get : ('a) array -> int -> 'a := "ltac2" "array_get". +Ltac2 @external set : ('a) array -> int -> 'a -> unit := "ltac2" "array_set". + +End Array. diff --git a/g_ltac2.ml4 b/g_ltac2.ml4 new file mode 100644 index 0000000000..349220f9de --- /dev/null +++ b/g_ltac2.ml4 @@ -0,0 +1,206 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* CPatRef (!@loc, id, pl) + | id = Prim.qualid -> CPatRef (!@loc, id, []) ] + | "0" + [ "_" -> CPatAny (!@loc) + | "()" -> CPatTup (!@loc, []) + | id = Prim.qualid -> CPatRef (!@loc, id, []) + | "("; pl = LIST0 tac2pat LEVEL "1" SEP ","; ")" -> CPatTup (!@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) + | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "0" SEP "," -> CTacTup (!@loc, e0 :: el) ] + | "0" + [ "("; a = tac2expr LEVEL "5"; ")" -> a + | "("; a = tac2expr; ":"; t = tac2type; ")" -> CTacCnv (!@loc, a, t) + | "()" -> CTacTup (!@loc, []) + | "("; ")" -> CTacTup (!@loc, []) + | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (!@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, AtmInt n) + | s = Prim.string -> CTacAtm (!@loc, AtmStr s) + | id = Prim.qualid -> CTacRef id + ] ] + ; + 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" + [ "("; p = LIST1 tac2type LEVEL "5" SEP ","; ")"; qid = Prim.qualid -> CTypRef (!@loc, qid, p) ] + | "0" + [ "("; t = tac2type; ")" -> t + | id = typ_param -> CTypVar (!@loc, Name id) + | "_" -> CTypVar (!@loc, Anonymous) + | qid = Prim.qualid -> CTypRef (!@loc, qid, []) ] + ]; + locident: + [ [ id = Prim.ident -> (!@loc, id) ] ] + ; + binder: + [ [ "_" -> (!@loc, Anonymous) + | l = Prim.ident -> (!@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) + | t = tac2alg_type -> CTydAlg t ] ] + ; + tac2alg_type: + [ [ -> [] + | "|"; bl = LIST1 tac2alg_constructor SEP "|" -> bl ] ] + ; + tac2alg_constructor: + [ [ c = Prim.ident -> (c, []) + | c = Prim.ident; "("; args = LIST0 tac2type SEP ","; ")"-> (c, args) ] ] + ; + tac2typ_prm: + [ [ -> [] + | id = typ_param -> [!@loc, id] + | "("; ids = LIST1 [ id = typ_param -> (!@loc, id) ] SEP "," ;")" -> ids + ] ] + ; + tac2typ_def: + [ [ prm = tac2typ_prm; id = locident; ":="; e = tac2typ_knd -> + (id, (prm, e)) + | prm = tac2typ_prm; id = locident -> (id, (prm, CTydDef None)) + ] ] + ; + 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) + ] ] + ; +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 ] +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/ltac2_plugin.mlpack b/ltac2_plugin.mlpack new file mode 100644 index 0000000000..561bd0eb0a --- /dev/null +++ b/ltac2_plugin.mlpack @@ -0,0 +1,6 @@ +Tac2env +Tac2intern +Tac2interp +Tac2entries +Tac2core +G_ltac2 diff --git a/tac2core.ml b/tac2core.ml new file mode 100644 index 0000000000..af4124e647 --- /dev/null +++ b/tac2core.ml @@ -0,0 +1,119 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* () +| _ -> 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 + +end + +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 + +let val_pp = Val.create "ltac2:pp" +let get_pp v = extract_val val_pp v + +(** Helper functions *) + +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 + +(** Primitives *) + +let prm_print : ml_tactic = function +| [ValExt pp] -> wrap_unit (fun () -> Feedback.msg_notice (get_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 s))) +| _ -> assert false + +let prm_array_make : ml_tactic = function +| [ValInt n; x] -> 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] -> wrap_unit (fun () -> v.(n) <- x) +| _ -> assert false + +let prm_array_get : ml_tactic = function +| [ValBlk (_, v); ValInt n] -> wrap (fun () -> v.(n)) +| _ -> 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 "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 diff --git a/tac2core.mli b/tac2core.mli new file mode 100644 index 0000000000..14bde483c1 --- /dev/null +++ b/tac2core.mli @@ -0,0 +1,34 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* valexpr +val to_unit : valexpr -> unit + +val of_list : valexpr list -> valexpr +val to_list : valexpr -> valexpr list + +end diff --git a/tac2entries.ml b/tac2entries.ml new file mode 100644 index 0000000000..7572270ab3 --- /dev/null +++ b/tac2entries.ml @@ -0,0 +1,321 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 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 knc + in + Tac2env.push_type visibility sp kn; + List.iter iter cstrs +| GTydRec _ -> + assert false (** FIXME *) + +let next i = + let ans = !i in + let () = incr i in + ans + +let dummy_var i = Id.of_string (Printf.sprintf "_%i" i) + +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 ids = List.mapi (fun i _ -> dummy_var i) args in + let c = GTacCst (kn, tag, List.map (fun id -> GTacVar id) ids) in + let c = + if List.is_empty args then c + else GTacFun (List.map (fun id -> Name id) ids, c) + in + let fold arg tpe = GTypArrow (arg, tpe) in + let cT = GTypRef (kn, List.init params (fun i -> GTypVar i)) in + let cT = List.fold_right fold args cT in + let data = { + Tac2env.cdata_type = kn; + cdata_args = params, args; + cdata_indx = tag; + } in + Tac2env.define_constructor knc data; + Tac2env.define_global knc (c, (params, cT)) + in + Tac2env.define_type kn qdef; + List.iter iter cstrs +| GTydRec _ -> + assert false (** FIXME *) + +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} + +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 (Loc.ghost, true, bindings, CTacRef (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 register_type ?(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 _ -> () (** FIXME *) + | CTydRec _ -> assert false (** FIXME *) + 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_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 + +(** 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 + let (_, (_, t)) = Tac2env.interp_global kn in + Feedback.msg_notice (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype t) + +(** 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_prefix = DirPath.make (List.map Id.of_string ["Ltac2"; "ltac2"; "Coq"]) +let coq_def n = KerName.make2 (MPfile 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/tac2entries.mli b/tac2entries.mli new file mode 100644 index 0000000000..9c5d0a15fd --- /dev/null +++ b/tac2entries.mli @@ -0,0 +1,33 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* rec_flag -> + (Name.t located * raw_tacexpr) list -> unit + +val register_type : ?local:bool -> rec_flag -> + (Id.t located * 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 + +(** {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 diff --git a/tac2env.ml b/tac2env.ml new file mode 100644 index 0000000000..d17e657516 --- /dev/null +++ b/tac2env.ml @@ -0,0 +1,139 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 } +| GTacTup el -> ValBlk (0, Array.map_of_list eval_pure el) +| GTacCst (_, n, []) -> ValInt n +| GTacCst (_, n, el) -> ValBlk (n, Array.map_of_list eval_pure el) +| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ +| GTacApp _ | GTacCse _ | GTacPrm _ -> + 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 + (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_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 + +module KnTab = Nametab.Make(FullPath)(KerName) + +type nametab = { + tab_ltac : KnTab.t; + tab_type : KnTab.t; +} + +let empty_nametab = { tab_ltac = KnTab.empty; tab_type = KnTab.empty } + +let nametab = Summary.ref empty_nametab ~name:"ltac2-nametab" + +let push_ltac vis sp kn = + let tab = !nametab in + nametab := { tab with tab_ltac = KnTab.push vis sp kn tab.tab_ltac } + +let locate_ltac qid = + let tab = !nametab in + KnTab.locate qid tab.tab_ltac + +let locate_extended_all_ltac qid = + let tab = !nametab in + KnTab.find_prefixes qid tab.tab_ltac + +let push_type vis sp kn = + let tab = !nametab in + nametab := { tab with tab_type = KnTab.push vis sp kn tab.tab_type } + +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 diff --git a/tac2env.mli b/tac2env.mli new file mode 100644 index 0000000000..efabdb5466 --- /dev/null +++ b/tac2env.mli @@ -0,0 +1,58 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* (glb_tacexpr * type_scheme) -> unit +val interp_global : ltac_constant -> (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_type : type_constant; + cdata_args : int * int glb_typexpr list; + cdata_indx : int; +} + +val define_constructor : ltac_constructor -> constructor_data -> unit +val interp_constructor : ltac_constructor -> constructor_data + +(** {5 Name management} *) + +val push_ltac : visibility -> full_path -> ltac_constant -> unit +val locate_ltac : qualid -> ltac_constant +val locate_extended_all_ltac : qualid -> ltac_constant list + +val push_type : visibility -> full_path -> type_constant -> unit +val locate_type : qualid -> type_constant +val locate_extended_all_type : qualid -> type_constant list + +(** {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 diff --git a/tac2expr.mli b/tac2expr.mli new file mode 100644 index 0000000000..445c69aa23 --- /dev/null +++ b/tac2expr.mli @@ -0,0 +1,136 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* valexpr Proofview.tactic diff --git a/tac2intern.ml b/tac2intern.ml new file mode 100644 index 0000000000..b1b35b0787 --- /dev/null +++ b/tac2intern.ml @@ -0,0 +1,921 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* elt -> bool +val create : unit -> 'a t +val fresh : 'a t -> elt +val size : 'a t -> int +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 +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 size p = p.uf_size + +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 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 loc_of_tacexpr = function +| CTacAtm (loc, _) -> loc +| CTacRef (loc, _) -> loc +| CTacFun (loc, _, _) -> loc +| CTacApp (loc, _, _) -> loc +| CTacLet (loc, _, _, _) -> loc +| CTacTup (loc, _) -> loc +| CTacArr (loc, _) -> loc +| CTacLst (loc, _) -> loc +| CTacCnv (loc, _, _) -> loc +| CTacSeq (loc, _, _) -> loc +| CTacCse (loc, _, _) -> loc + +let loc_of_patexpr = function +| CPatAny loc -> loc +| CPatRef (loc, _, _) -> loc +| CPatTup (loc, _) -> loc + +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, id) env) +| CTypVar (_, Anonymous) -> GTypVar (fresh_id env) +| CTypRef (_, (loc, qid), args) -> + let (dp, id) = repr_qualid qid in + let (kn, nparams) = + 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) + in + let nargs = List.length args in + let () = + if not (Int.equal nparams nargs) then + 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 _ -> 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)) + +(** FIXME *) +let rec pr_glbtype = function +| GTypVar n -> str "?" +| GTypRef (kn, tl) -> + KerName.print kn ++ str "(" ++ prlist_with_sep (fun () -> str ", ") pr_glbtype tl ++ str ")" +| GTypArrow (t1, t2) -> str "Arr(" ++ pr_glbtype t1 ++ str ", " ++ pr_glbtype t2 ++ str ")" +| GTypTuple tl -> str "Tup(" ++ prlist_with_sep (fun () -> str ", ") pr_glbtype tl ++ str ")" + +let unify loc env t1 t2 = + try unify env t1 t2 + with CannotUnify (u1, u2) -> + user_err ~loc (str "This expression has type " ++ pr_glbtype t1 ++ + str " but an expression what expected of type " ++ pr_glbtype t2) + +(** Term typing *) + +let rec is_value = function +| GTacAtm (AtmInt _) | GTacVar _ | GTacRef _ | GTacFun _ -> true +| GTacAtm (AtmStr _) | GTacApp _ | GTacLet _ -> false +| GTacTup el -> List.for_all is_value el +| GTacCst (_, _, []) -> true +| GTacCst (kn, n, el) -> + (** To be a value, a constructor must be immutable *) + assert false (** TODO *) +| GTacArr _ | GTacCse _ | GTacPrm _ -> false + +let is_rec_rhs = function +| GTacFun _ -> true +| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ -> false +| GTacTup _ | GTacArr _ | GTacPrm _ | GTacCst _ | GTacCse _ -> 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 _ -> + user_err ~loc (str "Type " ++ pr_glbtype t ++ str " is not an empty type") +| GTypRef (kn, _) -> + let def = Tac2env.interp_type kn in + match def with + | _, GTydAlg [] -> kn + | _ -> + user_err ~loc (str "Type " ++ pr_glbtype 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_variable env (loc, qid) = + let (dp, id) = repr_qualid qid in + if DirPath.is_empty dp && Id.Map.mem id env.env_var 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 + +let get_constructor env (loc, qid) = + let c = try Some (Tac2env.locate_ltac qid) with Not_found -> None in + match c with + | Some knc -> + let kn = + try Tac2env.interp_constructor knc + with Not_found -> + CErrors.user_err ~loc (str "The term " ++ pr_qualid qid ++ + str " is not the constructor of an inductive type.") in + ArgArg (kn, knc) + | 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) + +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' -> KerName.print kn + | GCaseTuple n -> str "tuple" + in + user_err ~loc (str "Invalid pattern, expected a pattern for type " ++ + KerName.print kn ++ str ", found a pattern of type " ++ pt) (** FIXME *) + +type pattern_kind = +| PKind_empty +| PKind_variant of KerName.t +| 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 fst p with + | CPatAny _ -> + begin match pl with + | [] -> PKind_any + | p :: pl -> get_kind p pl + end + | CPatRef (_, qid, []) -> + begin match get_constructor env qid with + | ArgVar _ -> + begin match pl with + | [] -> PKind_any + | p :: pl -> get_kind p pl + end + | ArgArg (data, _) -> PKind_variant data.cdata_type + end + | CPatRef (_, qid, _ :: _) -> + begin match get_constructor env qid with + | ArgVar (loc, _) -> + user_err ~loc (str "Unbound constructor " ++ pr_qualid (snd qid)) + | ArgArg (data, _) -> PKind_variant data.cdata_type + end + | CPatTup (_, tp) -> PKind_tuple (List.length tp) + in + get_kind p pl + +let rec intern_rec env = function +| CTacAtm (_, atm) -> intern_atm env atm +| CTacRef qid -> + 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 kn -> + let (_, sch) = Tac2env.interp_global kn in + (GTacRef kn, fresh_type_scheme env sch) + 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 (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, 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, []) -> + (GTacTup [], 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 + (GTacTup 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 = + let loc = loc_of_tacexpr e in + let (e, t) = intern_rec env e in + let () = unify loc env t t0 in + e :: 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 = + let loc = loc_of_tacexpr e in + let (e, t) = intern_rec env e in + let () = unify loc env t t0 in + c_cons e 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 + +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 pat with + | CPatAny _ -> Anonymous + | CPatRef (_, (_, qid), _) -> Name (snd (repr_qualid qid)) + | _ -> 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_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_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_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 (snd data.cdata_args) in + let () = + if not (Int.equal nids nargs) then + user_err ~loc (str "Constructor expects " ++ int nargs ++ + str " arguments, but is applied to " ++ int nids ++ + str " arguments") + 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 (snd data.cdata_args) in + let (br', brT) = intern_rec nenv br in + let () = + let index = data.cdata_indx 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_of_tacexpr br) env ret tbr in + intern_branch rem + in + let () = intern_branch pl in + let map = function + | None -> user_err ~loc (str "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) + +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) + +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) + +(** 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) +| GTacTup el -> + GTacTup (List.map (fun e -> subst_expr subst e) el) +| GTacArr el -> + GTacArr (List.map (fun e -> subst_expr subst e) el) +| GTacCst (kn, n, el) -> + GTacCst (subst_kn subst kn, n, List.map (fun e -> subst_expr subst e) 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') + +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' + +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') diff --git a/tac2intern.mli b/tac2intern.mli new file mode 100644 index 0000000000..a6be01d647 --- /dev/null +++ b/tac2intern.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 pr_glbtype : 'a glb_typexpr -> Pp.std_ppcmds diff --git a/tac2interp.ml b/tac2interp.ml new file mode 100644 index 0000000000..221f107dc8 --- /dev/null +++ b/tac2interp.ml @@ -0,0 +1,108 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 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 fst (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 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 ist 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 +| GTacTup [] -> + return (ValInt 0) +| GTacTup el | 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 +| GTacPrm (ml, el) -> + Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el -> + Tac2env.interp_primitive ml el + +and interp_app ist 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 ist 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 _ -> + 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 _ -> + anomaly (str "Unexpected value shape") diff --git a/tac2interp.mli b/tac2interp.mli new file mode 100644 index 0000000000..b11ee36012 --- /dev/null +++ b/tac2interp.mli @@ -0,0 +1,19 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* glb_tacexpr -> valexpr Proofview.tactic diff --git a/vo.itarget b/vo.itarget new file mode 100644 index 0000000000..776404ad79 --- /dev/null +++ b/vo.itarget @@ -0,0 +1 @@ +Ltac2.vo -- cgit v1.2.3