diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 18 | ||||
| -rw-r--r-- | src/tac2entries.ml | 4 | ||||
| -rw-r--r-- | src/tac2expr.mli | 2 | ||||
| -rw-r--r-- | src/tac2intern.ml | 170 |
4 files changed, 111 insertions, 83 deletions
diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4 index 7ee9d7e282..21612f9a25 100644 --- a/src/g_ltac2.ml4 +++ b/src/g_ltac2.ml4 @@ -117,10 +117,20 @@ GEXTEND Gram ] ] ; let_clause: - [ [ id = binder; ":="; te = tac2expr -> - (id, None, te) - | id = binder; args = LIST1 input_fun; ":="; te = tac2expr -> - (id, None, CTacFun (!@loc, args, te)) ] ] + [ [ binder = let_binder; ":="; te = tac2expr -> + let (pat, fn) = binder in + let te = match fn with None -> te | Some args -> CTacFun (!@loc, args, te) in + (pat, None, te) + ] ] + ; + let_binder: + [ [ pats = LIST1 input_fun -> + match pats with + | [CPatVar _ as pat, None] -> (pat, None) + | (CPatVar (_, Name id) as pat, None) :: args -> (pat, Some args) + | [pat, None] -> (pat, None) + | _ -> CErrors.user_err ~loc:!@loc (str "Invalid pattern") + ] ] ; tac2type: [ "5" RIGHTA diff --git a/src/tac2entries.ml b/src/tac2entries.ml index 70f1b583e0..7bc4c75510 100644 --- a/src/tac2entries.ml +++ b/src/tac2entries.ml @@ -266,7 +266,7 @@ let inline_rec_tactic tactics = in (** Fresh variables to abstract over the function patterns *) let _, vars = List.fold_left fold_var (avoid, []) pat in - let map_body ((loc, id), _, e) = (loc, Name id), None, e in + let map_body ((loc, id), _, e) = CPatVar (loc, Name id), None, e in let bnd = List.map map_body tactics in let pat_of_id (loc, id) = (CPatVar (loc, Name id), None) @@ -552,7 +552,7 @@ let perform_notation syn st = let mk loc args = let map (na, e) = let loc = loc_of_tacexpr e in - (Loc.tag ~loc na, None, e) + (CPatVar (Loc.tag ~loc na), None, e) in let bnd = List.map map args in CTacLet (loc, false, bnd, syn.synext_exp) diff --git a/src/tac2expr.mli b/src/tac2expr.mli index 668bc0dad1..10d8c1d421 100644 --- a/src/tac2expr.mli +++ b/src/tac2expr.mli @@ -92,7 +92,7 @@ type raw_tacexpr = | CTacCst of Loc.t * ltac_constructor or_tuple or_relid | CTacFun of Loc.t * (raw_patexpr * 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 +| CTacLet of Loc.t * rec_flag * (raw_patexpr * raw_typexpr option * raw_tacexpr) list * raw_tacexpr | CTacArr of raw_tacexpr list located | CTacLst of raw_tacexpr list located | CTacCnv of Loc.t * raw_tacexpr * raw_typexpr diff --git a/src/tac2intern.ml b/src/tac2intern.ml index e460111fc1..16e0bc8cbe 100644 --- a/src/tac2intern.ml +++ b/src/tac2intern.ml @@ -590,13 +590,53 @@ let get_pattern_kind env pl = match pl with (** Internalization *) (** Used to generate a fresh tactic variable for pattern-expansion *) -let fresh_var env = +let fresh_var avoid = let bad id = - Id.Map.mem id env.env_var || + Id.Set.mem id avoid || (try ignore (locate_ltac (qualid_of_ident id)); true with Not_found -> false) in Namegen.next_ident_away_from (Id.of_string "p") bad +let add_name accu = function +| Name id -> Id.Set.add id accu +| Anonymous -> accu + +let rec ids_of_pattern accu = function +| CPatVar (_, Anonymous) -> accu +| CPatVar (_, Name id) -> Id.Set.add id accu +| CPatRef (_, _, pl) -> + List.fold_left ids_of_pattern accu pl + +let loc_of_relid = function +| RelId (loc, _) -> Option.default dummy_loc loc +| AbsKn _ -> dummy_loc + +(** Expand pattern: [p => t] becomes [x => match x with p => t end] *) +let expand_pattern avoid bnd = + let fold (avoid, bnd) (pat, t) = + let na, expand = match pat with + | CPatVar (_, na) -> + (** Don't expand variable patterns *) + na, None + | _ -> + let loc = loc_of_patexpr pat in + let id = fresh_var avoid in + let qid = RelId (Loc.tag ~loc (qualid_of_ident id)) in + Name id, Some qid + in + let avoid = ids_of_pattern avoid pat in + let avoid = add_name avoid na in + (avoid, (na, pat, expand) :: bnd) + in + let (_, bnd) = List.fold_left fold (avoid, []) bnd in + let fold e (na, pat, expand) = match expand with + | None -> e + | Some qid -> CTacCse (loc_of_relid qid, CTacRef qid, [pat, e]) + in + let expand e = List.fold_left fold e bnd in + let nas = List.rev_map (fun (na, _, _) -> na) bnd in + (nas, expand) + let rec intern_rec env = function | CTacAtm (_, atm) -> intern_atm env atm | CTacRef qid -> @@ -612,35 +652,15 @@ let rec intern_rec env = function let kn = get_constructor env qid in intern_constructor env loc kn [] | CTacFun (loc, bnd, e) -> - (** Expand pattern: [fun p => t] becomes [fun x => match x with p => t end] *) - let fold (env, bnd, tl) (pat, t) = - let t = match t with - | None -> GTypVar (fresh_id env) - | Some t -> intern_type env t - in - let na, expand = match pat with - | CPatVar (_, na) -> - (** Don't expand variable patterns *) - na, None - | _ -> - let loc = loc_of_patexpr pat in - let id = fresh_var env in - let qid = RelId (Loc.tag ~loc (qualid_of_ident id)) in - Name id, Some qid - in - let env = push_name na (monomorphic t) env in - (env, (na, pat, expand) :: bnd, t :: tl) + let map (_, t) = match t with + | None -> GTypVar (fresh_id env) + | Some t -> intern_type env t in - let (env, bnd, tl) = List.fold_left fold (env, [], []) bnd in - let fold e (na, pat, expand) = match expand with - | None -> e - | Some qid -> - CTacCse (loc, CTacRef qid, [pat, e]) - in - let e = List.fold_left fold e bnd in - let nas = List.rev_map (fun (na, _, _) -> na) bnd in - let (e, t) = intern_rec env e in - let t = List.fold_left (fun accu t -> GTypArrow (t, accu)) t tl in + let tl = List.map map bnd in + let (nas, exp) = expand_pattern (Id.Map.domain env.env_var) bnd in + let env = List.fold_left2 (fun env na t -> push_name na (monomorphic t) env) env nas tl in + let (e, t) = intern_rec env (exp e) in + let t = List.fold_right (fun t accu -> GTypArrow (t, accu)) tl t in (GTacFun (nas, e), t) | CTacApp (loc, CTacCst (_, qid), args) -> let kn = get_constructor env qid in @@ -656,33 +676,20 @@ let rec intern_rec env = function let (args, t) = List.fold_right fold args ([], []) in let ret = unify_arrow ~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 \ +| CTacLet (loc, is_rec, el, e) -> + let fold accu (pat, _, e) = + let ids = ids_of_pattern Id.Set.empty pat in + let common = Id.Set.inter ids accu in + if Id.Set.is_empty common then Id.Set.union ids accu + else + let id = Id.Set.choose common in + let loc = loc_of_patexpr pat in + 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 + let ids = List.fold_left fold Id.Set.empty el in + if is_rec then intern_let_rec env loc ids el e + else intern_let env loc ids el e | CTacArr (loc, []) -> let id = fresh_id env in (GTacArr [], GTypRef (Other t_int, [GTypVar id])) @@ -760,17 +767,38 @@ and intern_rec_with_constraint env e exp = 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 +and intern_let env loc ids el e = + let avoid = Id.Set.union ids (Id.Map.domain env.env_var) in + let fold (pat, t, e) (avoid, accu) = + let nas, exp = expand_pattern avoid [pat, t] in + let na = match nas with [x] -> x | _ -> assert false in + let avoid = List.fold_left add_name avoid nas in + (avoid, (na, exp, t, e) :: accu) in - let _ = List.fold_left fold Id.Set.empty el in - let map env ((loc, na), t, e) = + let (_, el) = List.fold_right fold el (avoid, []) in + let fold (na, exp, tc, e) (body, el, p) = + let (e, t) = match tc with + | None -> intern_rec env e + | Some tc -> + let tc = intern_type env tc in + (intern_rec_with_constraint env e tc, tc) + in + let t = if is_value e then abstract_var env t else monomorphic t in + (exp body, (na, e) :: el, (na, t) :: p) + in + let (e, el, p) = List.fold_right fold el (e, [], []) in + let env = List.fold_left (fun accu (na, t) -> push_name na t accu) env p in + let (e, t) = intern_rec env e in + (GTacLet (false, el, e), t) + +and intern_let_rec env loc ids el e = + let map env (pat, t, e) = + let loc, na = match pat with + | CPatVar na -> na + | CPatRef _ -> + let loc = loc_of_patexpr pat in + user_err ~loc (str "This kind of pattern is forbidden in let-rec bindings") + in let id = fresh_id env in let env = push_name na (monomorphic (GTypVar id)) env in (env, (loc, na, t, e, id)) @@ -1116,10 +1144,6 @@ let intern_open_type 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 -> @@ -1128,12 +1152,6 @@ let get_projection0 var = match var with kn | AbsKn kn -> kn -let rec ids_of_pattern accu = function -| CPatVar (_, Anonymous) -> accu -| CPatVar (_, Name id) -> Id.Set.add id accu -| CPatRef (_, _, pl) -> - List.fold_left ids_of_pattern accu pl - let rec globalize ids e = match e with | CTacAtm _ -> e | CTacRef ref -> @@ -1160,7 +1178,7 @@ let rec globalize ids e = match e with 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 fold accu (pat, _, _) = ids_of_pattern accu pat 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 |