diff options
| -rw-r--r-- | Ltac2.v | 2 | ||||
| -rw-r--r-- | g_ltac2.ml4 | 30 | ||||
| -rw-r--r-- | tac2entries.ml | 79 | ||||
| -rw-r--r-- | tac2env.ml | 65 | ||||
| -rw-r--r-- | tac2env.mli | 45 | ||||
| -rw-r--r-- | tac2expr.mli | 20 | ||||
| -rw-r--r-- | tac2intern.ml | 180 | ||||
| -rw-r--r-- | tac2interp.ml | 19 |
8 files changed, 360 insertions, 80 deletions
@@ -20,7 +20,7 @@ Ltac2 Type 'a array. (** Pervasive types *) -Ltac2 Type 'a option := | None | Some ('a). +Ltac2 Type 'a option := [ None | Some ('a) ]. (** Primitive tactics *) diff --git a/g_ltac2.ml4 b/g_ltac2.ml4 index b613f22a8d..ce2becd9f9 100644 --- a/g_ltac2.ml4 +++ b/g_ltac2.ml4 @@ -50,6 +50,8 @@ GEXTEND Gram [ 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, qid) + | e = SELF; ".("; qid = Prim.qualid; ")"; ":="; r = tac2expr LEVEL "1" -> CTacSet (!@loc, e, qid, r) | e0 = tac2expr; ","; el = LIST1 tac2expr LEVEL "0" SEP "," -> CTacTup (!@loc, e0 :: el) ] | "0" [ "("; a = tac2expr LEVEL "5"; ")" -> a @@ -57,6 +59,7 @@ GEXTEND Gram | "()" -> CTacTup (!@loc, []) | "("; ")" -> CTacTup (!@loc, []) | "["; a = LIST0 tac2expr LEVEL "1" SEP ";"; "]" -> CTacLst (!@loc, a) + | "{"; a = tac2rec_fieldexprs; "}" -> CTacRec (!@loc, a) | a = tactic_atom -> a ] ] ; @@ -126,16 +129,35 @@ GEXTEND Gram ; tac2typ_knd: [ [ t = tac2type -> CTydDef (Some t) - | t = tac2alg_type -> CTydAlg t ] ] + | "["; t = tac2alg_constructors; "]" -> CTydAlg t + | "{"; t = tac2rec_fields; "}"-> CTydRec t ] ] ; - tac2alg_type: - [ [ -> [] - | "|"; bl = LIST1 tac2alg_constructor SEP "|" -> bl ] ] + 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" -> qid, e ] ] + ; tac2typ_prm: [ [ -> [] | id = typ_param -> [!@loc, id] diff --git a/tac2entries.ml b/tac2entries.ml index 7572270ab3..4098324f12 100644 --- a/tac2entries.ml +++ b/tac2entries.ml @@ -13,6 +13,7 @@ open Names open Libnames open Libobject open Nametab +open Tac2env open Tac2expr open Tac2intern open Vernacexpr @@ -24,14 +25,14 @@ type tacdef = { } let perform_tacdef visibility ((sp, kn), def) = - let () = if not def.tacdef_local then Tac2env.push_ltac visibility sp kn in + 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 kn in + 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) = @@ -71,12 +72,19 @@ let push_typedef visibility sp kn (_, def) = match def with 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 + Tac2env.push_ltac visibility spc (TacConstructor knc) in Tac2env.push_type visibility sp kn; List.iter iter cstrs -| GTydRec _ -> - assert false (** FIXME *) +| 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 let next i = let ans = !i in @@ -95,27 +103,31 @@ let define_typedef kn (params, def as qdef) = match def with 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; + Tac2env.cdata_prms = params; + cdata_type = kn; + cdata_args = args; cdata_indx = tag; } in - Tac2env.define_constructor knc data; - Tac2env.define_global knc (c, (params, cT)) + Tac2env.define_constructor knc data in Tac2env.define_type kn qdef; List.iter iter cstrs -| GTydRec _ -> - assert false (** FIXME *) +| 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 let perform_typdef vs ((sp, kn), def) = let () = if not def.typdef_local then push_typedef vs sp kn def.typdef_expr in @@ -213,8 +225,22 @@ let register_type ?(local = false) isrec types = if isrec then user_err ~loc (str "The type abbreviation " ++ Id.print id ++ str " cannot be recursive") - | CTydAlg _ -> () (** FIXME *) - | CTydRec _ -> assert false (** FIXME *) + | 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 + () in let () = List.iter check types in let self = @@ -275,8 +301,13 @@ let print_ltac ref = 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) + match kn with + | TacConstant kn -> + let (_, (_, t)) = Tac2env.interp_global kn in + Feedback.msg_notice (pr_qualid qid ++ spc () ++ str ":" ++ spc () ++ pr_glbtype t) + | TacConstructor kn -> + let _ = Tac2env.interp_constructor kn in + Feedback.msg_notice (str "Constructor" ++ spc () ++ str ":" ++ spc () ++ pr_qualid qid) (** Calling tactics *) diff --git a/tac2env.ml b/tac2env.ml index 3500b2ef3d..bdb8f41ef8 100644 --- a/tac2env.ml +++ b/tac2env.ml @@ -15,23 +15,35 @@ open Tac2expr type ltac_constant = KerName.t type ltac_constructor = KerName.t +type ltac_projection = KerName.t type type_constant = KerName.t type constructor_data = { + cdata_prms : int; cdata_type : type_constant; - cdata_args : int * int glb_typexpr list; + cdata_args : int glb_typexpr list; cdata_indx : int; } +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; } @@ -51,8 +63,8 @@ let rec eval_pure = function | 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 _ | GTacExt _ -> +| GTacAtm (AtmStr _) | GTacArr _ | GTacLet _ | GTacVar _ | GTacSet _ +| GTacApp _ | GTacCse _ | GTacPrj _ | GTacPrm _ | GTacExt _ -> anomaly (Pp.str "Term is not a syntactical value") let define_global kn e = @@ -69,6 +81,12 @@ let define_constructor kn t = 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 } @@ -103,28 +121,47 @@ struct id, (DirPath.repr dir) end +type 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 : KnTab.t; + tab_ltac : RfTab.t; tab_type : KnTab.t; + tab_proj : KnTab.t; } -let empty_nametab = { tab_ltac = KnTab.empty; tab_type = KnTab.empty } +let empty_nametab = { + tab_ltac = RfTab.empty; + tab_type = KnTab.empty; + tab_proj = 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 } + nametab := { tab with tab_ltac = RfTab.push vis sp kn tab.tab_ltac } let locate_ltac qid = let tab = !nametab in - KnTab.locate qid tab.tab_ltac + RfTab.locate qid tab.tab_ltac let locate_extended_all_ltac qid = let tab = !nametab in - KnTab.find_prefixes qid tab.tab_ltac + RfTab.find_prefixes qid tab.tab_ltac let push_type vis sp kn = let tab = !nametab in @@ -138,6 +175,18 @@ let locate_extended_all_type qid = let tab = !nametab in KnTab.find_prefixes qid tab.tab_type +let push_projection vis sp kn = + let tab = !nametab in + nametab := { tab with tab_proj = KnTab.push vis sp kn tab.tab_proj } + +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 + type 'a ml_object = { ml_type : type_constant; ml_interp : environment -> 'a -> Geninterp.Val.t Proofview.tactic; diff --git a/tac2env.mli b/tac2env.mli index eb471b9abf..bcfa70487a 100644 --- a/tac2env.mli +++ b/tac2env.mli @@ -14,10 +14,6 @@ open Tac2expr (** Ltac2 global environment *) -type ltac_constant = KerName.t -type ltac_constructor = KerName.t -type type_constant = KerName.t - (** {5 Toplevel definition of values} *) val define_global : ltac_constant -> (glb_tacexpr * type_scheme) -> unit @@ -31,24 +27,57 @@ 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; - cdata_args : int * int glb_typexpr list; + (** Inductive definition to which the constructor pertains *) + cdata_args : int glb_typexpr list; + (** Types of the constructor arguments *) cdata_indx : int; + (** 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. *) } 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 -> ltac_constant -> unit -val locate_ltac : qualid -> ltac_constant -val locate_extended_all_ltac : qualid -> ltac_constant list +type tacref = +| TacConstant of ltac_constant +| TacConstructor of ltac_constructor + +val push_ltac : visibility -> full_path -> tacref -> unit +val locate_ltac : qualid -> tacref +val locate_extended_all_ltac : qualid -> tacref 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 +val push_projection : visibility -> full_path -> ltac_projection -> unit +val locate_projection : qualid -> ltac_projection +val locate_extended_all_projection : qualid -> ltac_projection list + (** {5 Toplevel definitions of ML tactics} *) (** This state is not part of the summary, contrarily to the ones above. It is diff --git a/tac2expr.mli b/tac2expr.mli index 15c630ca87..b9b649e481 100644 --- a/tac2expr.mli +++ b/tac2expr.mli @@ -16,6 +16,11 @@ type rec_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 + (** {5 Misc} *) type ml_tactic_name = { @@ -40,7 +45,7 @@ type 'a glb_typexpr = | GTypVar of 'a | GTypArrow of 'a glb_typexpr * 'a glb_typexpr | GTypTuple of 'a glb_typexpr list -| GTypRef of KerName.t * 'a glb_typexpr list +| GTypRef of type_constant * 'a glb_typexpr list type glb_typedef = | GTydDef of int glb_typexpr option @@ -76,25 +81,32 @@ type raw_tacexpr = | 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 * qualid located +| CTacSet of Loc.t * raw_tacexpr * qualid located * raw_tacexpr | CTacExt of Loc.t * raw_generic_argument and raw_taccase = raw_patexpr * raw_tacexpr +and raw_recexpr = (qualid located * raw_tacexpr) list + type case_info = | GCaseTuple of int -| GCaseAlg of KerName.t +| GCaseAlg of type_constant type glb_tacexpr = | GTacAtm of atom | GTacVar of Id.t -| GTacRef of KerName.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 | GTacTup of glb_tacexpr list | GTacArr of glb_tacexpr list -| GTacCst of KerName.t * int * glb_tacexpr list +| GTacCst of type_constant * int * glb_tacexpr list | GTacCse of glb_tacexpr * case_info * glb_tacexpr array * (Name.t array * glb_tacexpr) array +| GTacPrj of glb_tacexpr * int +| GTacSet of glb_tacexpr * int * glb_tacexpr | GTacExt of glob_generic_argument | GTacPrm of ml_tactic_name * glb_tacexpr list diff --git a/tac2intern.ml b/tac2intern.ml index a554f959a0..10fcde6efa 100644 --- a/tac2intern.ml +++ b/tac2intern.ml @@ -174,6 +174,9 @@ let loc_of_tacexpr = function | 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 @@ -181,6 +184,11 @@ let loc_of_patexpr = function | CPatRef (loc, _, _) -> loc | CPatTup (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 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) @@ -320,20 +328,27 @@ let unify loc env t1 t2 = (** Term typing *) +let is_pure_constructor kn = + match snd (Tac2env.interp_type kn) with + | GTydAlg _ -> 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 | 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 _ | GTacExt _ | GTacPrm _ -> false +| GTacCst (kn, _, el) -> is_pure_constructor kn && List.for_all is_value el +| GTacArr _ | GTacCse _ | GTacPrj _ | GTacSet _ | GTacExt _ | GTacPrm _ -> false let is_rec_rhs = function | GTacFun _ -> true -| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ -> false -| GTacTup _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _ | GTacCse _ -> false +| GTacAtm _ | GTacVar _ | GTacRef _ | GTacApp _ | GTacLet _ | GTacPrj _ +| GTacSet _ | GTacTup _ | GTacArr _ | GTacExt _ | GTacPrm _ | GTacCst _ +| GTacCse _ -> false let rec fv_type f t accu = match t with | GTypVar id -> f id accu @@ -438,18 +453,23 @@ let get_variable env (loc, qid) = 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 + | 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) +let get_projection (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 + let intern_atm env = function | AtmInt n -> (GTacAtm (AtmInt n), GTypRef (t_int, [])) | AtmStr s -> (GTacAtm (AtmStr s), GTypRef (t_string, [])) @@ -496,6 +516,10 @@ let get_pattern_kind env pl = match pl with in get_kind p pl +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 -> @@ -503,9 +527,11 @@ let rec intern_rec env = function | ArgVar (_, id) -> let sch = Id.Map.find id env.env_var in (GTacVar id, fresh_mix_type_scheme env sch) - | ArgArg kn -> + | ArgArg (TacConstant kn) -> let (_, sch) = Tac2env.interp_global kn in (GTacRef kn, fresh_type_scheme env sch) + | ArgArg (TacConstructor kn) -> + intern_constructor env (fst qid) kn [] end | CTacFun (loc, bnd, e) -> let fold (env, bnd, tl) ((_, na), t) = @@ -520,6 +546,12 @@ let rec intern_rec env = function 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) when is_constructor env qid -> + let kn = match get_variable env qid with + | ArgArg (TacConstructor kn) -> kn + | _ -> assert false + in + intern_constructor env (fst qid) kn args | CTacApp (loc, f, args) -> let (f, ft) = intern_rec env f in let fold arg (args, t) = @@ -571,12 +603,7 @@ let rec intern_rec env = function (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 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, []) -> @@ -584,12 +611,7 @@ let rec intern_rec env = function (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 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) -> @@ -604,6 +626,34 @@ let rec intern_rec env = function (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 (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, _) = proj 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 (e, pinfo.pdata_indx, r), GTypRef (t_unit, [])) | CTacExt (loc, ext) -> let open Genintern in let GenArg (Rawwit tag, _) = ext in @@ -616,6 +666,12 @@ let rec intern_rec env = function 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 @@ -760,12 +816,9 @@ and intern_case env loc e pl = 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 nargs = List.length 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") + if not (Int.equal nids nargs) then error_nargs_mismatch loc nargs nids in let fold env id tpe = (** Instantiate all arguments *) @@ -773,7 +826,7 @@ and intern_case env loc e pl = 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 nenv = List.fold_left2 fold env ids data.cdata_args in let (br', brT) = intern_rec nenv br in let () = let index = data.cdata_indx in @@ -802,6 +855,64 @@ and intern_case env loc e pl = let ce = GTacCse (e', GCaseAlg kn, const, nonconst) in (ce, 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 + (GTacCst (cstr.cdata_type, cstr.cdata_indx, args), ans) + else + error_nargs_mismatch loc nargs (List.length args) + +and intern_record env loc fs = + let map ((loc, qid), e) = + let proj = get_projection (loc, qid) 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 " ++ KerName.print 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 (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 @@ -907,6 +1018,13 @@ let rec subst_expr subst e = match e with 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') +| GTacPrj (e, p) as e0 -> + let e' = subst_expr subst e in + if e' == e then e0 else GTacPrj (e', p) +| GTacSet (e, p, r) as e0 -> + let e' = subst_expr subst e in + let r' = subst_expr subst r in + if e' == e && r' == r then e0 else GTacSet (e', p, r') | GTacExt ext -> let ext' = Genintern.generic_substitute subst ext in if ext' == ext then e else GTacExt ext' diff --git a/tac2interp.ml b/tac2interp.ml index b868caf963..fedbb13e7d 100644 --- a/tac2interp.ml +++ b/tac2interp.ml @@ -80,6 +80,12 @@ let rec interp ist = function return (ValBlk (n, Array.of_list el)) | GTacCse (e, _, cse0, cse1) -> interp ist e >>= fun e -> interp_case ist e cse0 cse1 +| 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 | GTacPrm (ml, el) -> Proofview.Monad.List.map (fun e -> interp ist e) el >>= fun el -> Tac2env.interp_primitive ml el @@ -110,3 +116,16 @@ and interp_case ist e cse0 cse1 = match e with interp ist e | 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 _ -> + 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 _ -> + anomaly (str "Unexpected value shape") |